diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 12d03362a6b34ea021649f56363bf5c85791ef12..4e91b91918b095e5bd83d7d71123e8d42e3c2e6e 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -15,9 +15,12 @@ object Main {
}
// Add whatever you need here.
- lazy val allComponents : List[LeonComponent] = allPhases ++ Nil
+ lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
+ // It's a little unfortunate that we need to build one...
+ new solvers.z3.FairZ3Solver(LeonContext())
+ )
- lazy val allOptions = allPhases.flatMap(_.definedOptions) ++ Set(
+ lazy val topLevelOptions : Set[LeonOptionDef] = Set(
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
LeonFlagOptionDef ("parse", "--parse", "Checks only whether the program is valid PureScala"),
@@ -27,31 +30,26 @@ object Main {
// Unimplemented Options:
//
// LeonFlagOptionDef("uniqid", "--uniqid", "When pretty-printing purescala trees, show identifiers IDs"),
- // LeonValueOptionDef("extensions", "--extensions=ex1:...", "Specifies a list of qualified class names of extensions to be loaded"),
- // LeonFlagOptionDef("nodefaults", "--nodefaults", "Runs only the analyses provided by the extensions"),
- // LeonValueOptionDef("functions", "--functions=fun1:...", "Only generates verification conditions for the specified functions"),
- // LeonFlagOptionDef("unrolling", "--unrolling=[0,1,2]", "Unrolling depth for recursive functions" ),
- // LeonFlagOptionDef("axioms", "--axioms", "Generate simple forall axioms for recursive functions when possible" ),
// LeonFlagOptionDef("tolerant", "--tolerant", "Silently extracts non-pure function bodies as ''unknown''"),
// LeonFlagOptionDef("bapa", "--bapa", "Use BAPA Z3 extension (incompatible with many other things)"),
// LeonFlagOptionDef("impure", "--impure", "Generate testcases only for impure functions"),
// LeonValueOptionDef("testcases", "--testcases=[1,2]", "Number of testcases to generate per function"),
// LeonValueOptionDef("testbounds", "--testbounds=l:u", "Lower and upper bounds for integers in recursive datatypes"),
// LeonValueOptionDef("timeout", "--timeout=N", "Sets a timeout of N seconds"),
- // LeonFlagOptionDef("XP", "--XP", "Enable weird transformations and other bug-producing features"),
// LeonFlagOptionDef("BV", "--BV", "Use bit-vectors for integers"),
- // LeonFlagOptionDef("prune", "--prune", "Use additional SMT queries to rule out some unrollings"),
- // LeonFlagOptionDef("cores", "--cores", "Use UNSAT cores in the unrolling/refinement step"),
// LeonFlagOptionDef("quickcheck", "--quickcheck", "Use QuickCheck-like random search"),
// LeonFlagOptionDef("parallel", "--parallel", "Run all solvers in parallel"),
- // LeonFlagOptionDef("noLuckyTests", "--noLuckyTests", "Do not perform additional tests to potentially find models early"),
- // LeonFlagOptionDef("noverifymodel", "--noverifymodel", "Do not verify the correctness of models returned by Z3"),
// LeonValueOptionDef("tags", "--tags=t1:...", "Filter out debug information that are not of one of the given tags"),
)
+ lazy val allOptions = allComponents.flatMap(_.definedOptions) ++ topLevelOptions
+
def displayHelp(reporter: Reporter) {
reporter.info("usage: leon [--xlang] [--synthesis] [--help] [--debug=<N>] [..] <files>")
reporter.info("")
+ for (opt <- topLevelOptions.toSeq.sortBy(_.name)) {
+ reporter.info("%-20s %s".format(opt.usageOption, opt.usageDesc))
+ }
reporter.info("(By default, Leon verifies PureScala programs.)")
reporter.info("")
reporter.info("Additional options, by component:")
@@ -96,7 +94,7 @@ object Main {
case (false, LeonValueOption(name, value)) =>
Some(leonOpt)
case _ =>
- reporter.error("Invalid option usage: "+opt)
+ reporter.error("Invalid option usage: " + opt)
displayHelp(reporter)
None
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 5536471de0c28dad8eadc8e8b1de7f4dd482252b..ffcf50c8b008d00b49d161cf525e8b2ac5a60fbb 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -5,17 +5,11 @@ package leon
object Settings {
var showIDs: Boolean = false
lazy val reporter: Reporter = new DefaultReporter
- var noForallAxioms: Boolean = true
- var unrollingLevel: Int = 0
var useBAPA: Boolean = false
var impureTestcases: Boolean = false
var nbTestcases: Int = 1
var testBounds: (Int, Int) = (0, 3)
- var useCores : Boolean = false
- var pruneBranches : Boolean = false
var solverTimeout : Option[Int] = None
- var luckyTest : Boolean = true
- var verifyModel : Boolean = true
var useQuickCheck : Boolean = false
var useParallel : Boolean = false
// When this is None, use real integers
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index af25f91d36ae4a653a830fcec6d6d481c9fa76c8..bb03f0d7999cd937d35a7638cc2116b437a1d54c 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -18,7 +18,6 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
" --uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
" --with-code Allows the compiler to keep running after the static analysis" + "\n" +
" --parse Checks only whether the program is valid PureScala" + "\n" +
- " --unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
" --axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
" --tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
" --bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
@@ -27,11 +26,8 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
" --testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
" --timeout=N Sets a timeout of N seconds" + "\n" +
" --BV Use bit-vectors for integers" + "\n" +
- " --prune Use additional SMT queries to rule out some unrollings" + "\n" +
- " --cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" --quickcheck Use QuickCheck-like random search" + "\n" +
" --parallel Run all solvers in parallel" + "\n" +
- " --noverifymodel Do not verify the correctness of models returned by Z3" + "\n" +
" --debug=[1-5] Debug level" + "\n" +
" --imperative Preprocessing and transformation from imperative programs" + "\n" +
" --synthesis Magic!"
@@ -46,15 +42,11 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
case "uniqid" => leon.Settings.showIDs = true
case "parse" => leon.Settings.stopAfterExtraction = true
case "tolerant" => leon.Settings.silentlyTolerateNonPureBodies = true
- case "axioms" => leon.Settings.noForallAxioms = false
case "bapa" => leon.Settings.useBAPA = true
case "impure" => leon.Settings.impureTestcases = true
case "BV" => leon.Settings.bitvectorBitwidth = Some(32)
- case "prune" => leon.Settings.pruneBranches = true
- case "cores" => leon.Settings.useCores = true
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
- case "noverifymodel" => leon.Settings.verifyModel = false
case "imperative" => leon.Settings.synthesis = false;
leon.Settings.transformProgram = true;
case "synthesis" => leon.Settings.synthesis = true;
@@ -62,7 +54,6 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
leon.Settings.stopAfterTransformation = true;
case s if s.startsWith("debug=") => leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
- case s if s.startsWith("unrolling=") => leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("testbounds=") => leon.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
case s if s.startsWith("timeout=") => leon.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
case s if s.startsWith("testcases=") => leon.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 5990c71655a60f9231a470fafd31c4fbf1e483ae..395bf29f067a0454f5fb33d2687f8c531495cae9 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -21,9 +21,29 @@ class FairZ3Solver(context : LeonContext)
with Z3ModelReconstruction
with LeonComponent {
+ enclosing =>
+
val name = "Z3-f"
val description = "Fair Z3 Solver"
+ override val definedOptions : Set[LeonOptionDef] = Set(
+ LeonFlagOptionDef("checkmodels", "--checkmodels", "Double-check counter-examples"),
+ LeonFlagOptionDef("feelinglucky", "--feelinglucky", "Use evaluator to find counter-examples early")
+ )
+
+ val (feelingLucky, checkModels) = locally {
+ var lucky = false
+ var check = false
+
+ for(opt <- context.options) opt match {
+ case LeonFlagOption("checkmodels") => check = true
+ case LeonFlagOption("feelinglucky") => lucky = true
+ case _ =>
+ }
+
+ (lucky,check)
+ }
+
// this is fixed
protected[leon] val z3cfg = new Z3Config(
"MODEL" -> true,
@@ -60,59 +80,6 @@ class FairZ3Solver(context : LeonContext)
}
}
- private def prepareAxioms(solver: Z3Solver): Unit = {
- assert(!Settings.noForallAxioms)
- program.definedFunctions.foreach(_ match {
- case fd @ Catamorphism(acd, cases) => {
- assert(!fd.hasPrecondition && fd.hasImplementation)
- reporter.info("Will attempt to axiomatize the function definition:")
- reporter.info(fd)
- for(cse <- cases) {
- val (cc @ CaseClass(ccd, args), expr) = cse
- assert(args.forall(_.isInstanceOf[Variable]))
- val argsAsIDs = args.map(_.asInstanceOf[Variable].id)
- assert(variablesOf(expr) -- argsAsIDs.toSet == Set.empty)
- val axiom : Z3AST = if(args.isEmpty) {
- val eq = Equals(FunctionInvocation(fd, Seq(cc)), expr)
- toZ3Formula(eq).get
- } else {
- val z3ArgSorts = argsAsIDs.map(i => typeToSort(i.getType))
- val boundVars = z3ArgSorts.zipWithIndex.map(p => z3.mkBound(p._2, p._1))
- val map : Map[Identifier,Z3AST] = (argsAsIDs zip boundVars).toMap
- val eq = Equals(FunctionInvocation(fd, Seq(cc)), expr)
- val z3IzedEq = toZ3Formula(eq, map).get
- val z3IzedCC = toZ3Formula(cc, map).get
- val pattern = z3.mkPattern(functionDefToDecl(fd)(z3IzedCC))
- val nameTypePairs = z3ArgSorts.map(s => (z3.mkFreshIntSymbol, s))
- z3.mkForAll(0, List(pattern), nameTypePairs, z3IzedEq)
- }
- // println("I'll assert now an axiom: " + axiom)
- // println("Case axiom:")
- // println(axiom)
- solver.assertCnstr(axiom)
- }
-
- if(fd.hasPostcondition) {
- // we know it doesn't contain any function invocation
- val cleaned = matchToIfThenElse(expandLets(fd.postcondition.get))
- val argSort = typeToSort(fd.args(0).getType)
- val bound = z3.mkBound(0, argSort)
- val subst = replace(Map(ResultVariable() -> FunctionInvocation(fd, Seq(fd.args(0).toVariable))), cleaned)
- val z3IzedPost = toZ3Formula(subst, Map(fd.args(0).id -> bound)).get
- val pattern = z3.mkPattern(functionDefToDecl(fd)(bound))
- val nameTypePairs = Seq((z3.mkFreshIntSymbol, argSort))
- val postAxiom = z3.mkForAll(0, List(pattern), nameTypePairs, z3IzedPost)
- //println("Post axiom:")
- //println(postAxiom)
- solver.assertCnstr(postAxiom)
- }
-
- axiomatizedFunctions += fd
- }
- case _ => ;
- })
- }
-
override def solve(vc: Expr) = {
val solver = getNewSolver
solver.assertCnstr(Not(vc))
@@ -271,17 +238,12 @@ class FairZ3Solver(context : LeonContext)
val solver = z3.mkSolver
- if(!Settings.noForallAxioms) {
- prepareAxioms(solver)
- }
-
for(funDef <- program.definedFunctions) {
if (funDef.annotations.contains("axiomatize") && !axiomatizedFunctions(funDef)) {
reporter.warning("Function " + funDef.id + " was marked for axiomatization but could not be handled.")
}
}
-
private var frameGuards = List[Z3AST](z3.mkFreshConst("frame", z3.mkBoolSort))
private var frameExpressions = List[List[Expr]](Nil)
private var varsInVC = Set[Identifier]()
@@ -368,10 +330,7 @@ class FairZ3Solver(context : LeonContext)
// these are the optional sequence of assumption literals
val assumptionsAsZ3: Seq[Z3AST] = frameGuards ++ assumptions.map(toZ3Formula(_).get)
- var iterationsLeft : Int = if(Settings.unrollingLevel > 0) Settings.unrollingLevel else 16121984
-
while(!foundDefinitiveAnswer && !forceStop) {
- iterationsLeft -= 1
//val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get)
// println("Blocking set : " + blockingSet)
@@ -398,7 +357,7 @@ class FairZ3Solver(context : LeonContext)
val z3model = solver.getModel
- if (Settings.verifyModel && false) {
+ if (enclosing.checkModels) {
val (isValid, model) = validateAndDeleteModel(z3model, entireFormula, varsInVC)
if (isValid) {
@@ -432,7 +391,7 @@ class FairZ3Solver(context : LeonContext)
reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
if (!forceStop) {
- if (Settings.luckyTest && false) { //TODO: something with false
+ if (enclosing.feelingLucky) {
// we need the model to perform the additional test
reporter.info(" - Running search without blocked literals (w/ lucky test)")
} else {
@@ -449,7 +408,7 @@ class FairZ3Solver(context : LeonContext)
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) =>
//reporter.info("SAT WITHOUT Blockers")
- if (Settings.luckyTest && !forceStop) { //TODO: still with the above "false"
+ if (enclosing.feelingLucky) {
// we might have been lucky :D
luckyTime.start
val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
@@ -470,52 +429,6 @@ class FairZ3Solver(context : LeonContext)
if(!foundDefinitiveAnswer) {
reporter.info("- We need to keep going.")
- // reporter.info(" - toRelease : " + toRelease)
- // reporter.info(" - blockingSet : " + blockingSet)
-
- //var fixedForEver : Set[Expr] = Set.empty
-
- //if(Settings.pruneBranches) {
- // z3Time.start
- // for(ex <- blockingSet) ex match {
- // case Not(Variable(b)) =>
- // solver.push
- // solver.assertCnstr(toZ3Formula(Variable(b)).get)
- // solver.check match {
- // case Some(false) =>
- // //println("We had ~" + b + " in the blocking set. We now know it should stay there forever.")
- // solver.pop(1)
- // solver.assertCnstr(toZ3Formula(Not(Variable(b))).get)
- // fixedForEver = fixedForEver + ex
-
- // case _ =>
- // solver.pop(1)
- // }
-
- // case Variable(b) =>
- // solver.push
- // solver.assertCnstr(toZ3Formula(Not(Variable(b))).get)
- // solver.check match {
- // case Some(false) =>
- // //println("We had " + b + " in the blocking set. We now know it should stay there forever.")
- // solver.pop(1)
- // solver.assertCnstr(toZ3Formula(Variable(b)).get)
- // fixedForEver = fixedForEver + ex
-
- // case _ =>
- // solver.pop(1)
- // }
-
- // case _ =>
- // scala.sys.error("Should not have happened.")
- // }
-
- // if(fixedForEver.size > 0) {
- // reporter.info("- Pruned out " + fixedForEver.size + " branches.")
- // }
- // z3Time.stop
- //}
-
val toReleaseAsPairs = unrollingBank.getBlockersToUnlock
reporter.info(" - more unrollings")
@@ -533,11 +446,6 @@ class FairZ3Solver(context : LeonContext)
reporter.info(" - finished unrolling")
}
}
-
- if(iterationsLeft <= 0) {
- reporter.error(" - Max. number of iterations reached.")
- foundAnswer(None)
- }
}
totalTime.stop