Passing flags to Z3...

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
         }

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

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 }

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