diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 40ecbc08b5dd1e3b6db38bfd35f3fba62a1db66d..8799f320fad7f16eb89581d1d82abeddb89773b7 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -38,6 +38,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
" -P:funcheck:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" -P:funcheck:quickcheck Use QuickCheck-like random search" + "\n" +
" -P:funcheck:parallel Run all solvers in parallel" + "\n" +
+ " -P:funcheck:templates Use new ``FunctionTemplate'' technique" + "\n" +
" -P:funcheck:noLuckyTests Do not perform additional tests to potentially find models early"
)
@@ -60,6 +61,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
case "cores" => purescala.Settings.useCores = true
case "quickcheck" => purescala.Settings.useQuickCheck = true
case "parallel" => purescala.Settings.useParallel = true
+ case "templates" => purescala.Settings.useTemplates = true
case "noLuckyTests" => purescala.Settings.luckyTest = false
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 0336206dcda337adc2d3b0bf0301b191815b7bcf..7f2bfad064c2fe027c945bee813630811f17ccc9 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -23,24 +23,11 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter)
val inductionTactic = new InductionTactic(reporter)
inductionTactic.setProgram(program)
- def analyse : Unit = {
- for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2)) {
- if(funDef.hasImplementation) {
- reporter.info("Creating template for " + funDef.id + "...")
-
- val t : FunctionTemplate = FunctionTemplate.mkTemplate(funDef)
- reporter.info("The template : " + t)
- } else {
- reporter.info("Skipping template creating for " + funDef.id + " as it doesn't have a known implementation.")
- }
- }
- }
-
// Calling this method will run all analyses on the program passed at
// construction time. If at least one solver is loaded, verification
// conditions are generated and passed to all solvers. Otherwise, only the
// Analysis extensions are run on the program.
- def analyseReal : Unit = {
+ def analyse : Unit = {
if(solverExtensions.size > 1) {
reporter.info("Running verification condition generation...")
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index c0d0d48b770a11765ccefac10a88faa45f57dea3..d09b1399e470a21b788538b35d6791f52001d304 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -74,7 +74,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
prepareSorts
prepareFunctions
- unrollingBank = new UnrollingBank
+ unrollingBank = if(Settings.useTemplates) {
+ new NewUnrollingBank
+ } else {
+ new UnrollingBank
+ }
blockingSet = Set.empty
toCheckAgainstModels = BooleanLiteral(true)
varsInVC = Set.empty
@@ -488,17 +492,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
varsInVC ++= variablesOf(expandedVC)
reporter.info(" - Initial unrolling...")
- val (basis, clauses, guards) = unrollingBank.closeUnrollings(expandedVC)
- // println("Here is what we want to check against models : " + toCheckAgainstModels)
- // println("New basis: " + e)
- // println("Bunch of clauses:\n" + se.map(_.toString).mkString("\n"))
- // println("Bunch of blocking bools: " + sib.map(_.toString).mkString(", "))
-
- // println("Basis : " + basis)
- val bb = toZ3Formula(z3, basis).get
- // println("Base : " + bb)
- z3.assertCnstr(bb)
- // println(toZ3Formula(z3, basis).get)
+ val (clauses, guards) = unrollingBank.initialUnrolling(expandedVC)
+
// for(clause <- clauses) {
// println("we're getting a new clause " + clause)
// z3.assertCnstr(toZ3Formula(z3, clause).get)
@@ -1136,7 +1131,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
!filtered.isEmpty
}
- def wasUnrolledBefore(functionInvocation : FunctionInvocation) : Boolean = {
+ private def wasUnrolledBefore(functionInvocation : FunctionInvocation) : Boolean = {
everythingEverUnrolled(functionInvocation)
}
@@ -1144,7 +1139,12 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
everythingEverUnrolled += functionInvocation
}
- def closeUnrollings(formula : Expr) : (Expr, Seq[Expr], Seq[(Identifier,Boolean)]) = {
+ def initialUnrolling(formula : Expr) : (Seq[Expr], Seq[(Identifier,Boolean)]) = {
+ val (e,s,ss) = closeUnrollings(formula)
+ (e +: s, ss)
+ }
+
+ private def closeUnrollings(formula : Expr) : (Expr, Seq[Expr], Seq[(Identifier,Boolean)]) = {
var (basis, clauses, ite2Bools) = clausifyITE(formula)
var unrolledNow : Set[FunctionInvocation] = Set.empty
@@ -1210,6 +1210,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
// takes in a conjunction and returns a new conjunction, where all
// non-recursive function calls are "defined" and "contracted"
+ // NEVER USED !!!
+ /*
def expandAllNonRecursive(exprs: List[Expr]) : List[Expr] = {
val todo : MutableSet[FunctionInvocation] = MutableSet.empty
val todo2 : MutableSet[FunctionInvocation] = MutableSet.empty
@@ -1235,7 +1237,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
resulting
- }
+ }*/
// Returns between 0 and 2 tautologies with respect to the interpretation of
// the function and its postcondition.
@@ -1284,13 +1286,23 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
- private var invocations : List[FunctionInvocation] = Nil
+ // Old junk?
+ /*private var invocations : List[FunctionInvocation] = Nil
def addInvocation(blocker: Identifier, polarity: Boolean, invocation: FunctionInvocation) : Unit = {
invocations = invocation :: invocations
- }
+ }*/
+ }
+ class NewUnrollingBank extends UnrollingBank {
+ // This is called just once, for the "initial unrolling".
+ override def initialUnrolling(formula : Expr) : (Seq[Expr], Seq[(Identifier,Boolean)]) = {
+ sys.error("Not implemented.")
+ }
+ override def unlock(id: Identifier, polarity: Boolean) : (Seq[Expr], Seq[(Identifier,Boolean)]) = {
+ sys.error("Not implemented.")
+ }
}
}
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 900e9062b33102794278345e832e1fc7d23aec80..e2be9ef6e4a5fc8ac7763d43b6bc00eb834acea2 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -26,4 +26,5 @@ object Settings {
var useParallel : Boolean = false
// When this is None, use real integers
var bitvectorBitwidth : Option[Int] = None
+ var useTemplates : Boolean = false
}