From 2b09cd4c29443f4696120aa1728be47323a187d3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 14 Jan 2013 02:29:24 +0100
Subject: [PATCH] Export userland flag to use unsat cores to drive the fairz3
unrolling
---
.../scala/leon/solvers/z3/FairZ3Solver.scala | 22 ++++++++++---------
1 file changed, 12 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 0b79871ba..63da53068 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -29,26 +29,28 @@ class FairZ3Solver(context : LeonContext)
val description = "Fair Z3 Solver"
override val definedOptions : Set[LeonOptionDef] = Set(
- LeonFlagOptionDef("evalground", "--evalground", "Use evaluator on functions applied to ground arguments"),
- LeonFlagOptionDef("checkmodels", "--checkmodels", "Double-check counter-examples with evaluator"),
- LeonFlagOptionDef("feelinglucky", "--feelinglucky", "Use evaluator to find counter-examples early"),
- LeonFlagOptionDef("codegen", "--codegen", "Use compiled evaluator instead of interpreter")
+ LeonFlagOptionDef("evalground", "--evalground", "Use evaluator on functions applied to ground arguments"),
+ LeonFlagOptionDef("checkmodels", "--checkmodels", "Double-check counter-examples with evaluator"),
+ LeonFlagOptionDef("feelinglucky", "--feelinglucky", "Use evaluator to find counter-examples early"),
+ LeonFlagOptionDef("codegen", "--codegen", "Use compiled evaluator instead of interpreter"),
+ LeonFlagOptionDef("fairz3:unrollcores", "--fairz3:unrollcores", "Use unsat-cores to drive unrolling while remaining fair")
)
// What wouldn't we do to avoid defining vars?
val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores, pruneUnsatCores) = locally {
- var lucky = true
+ var lucky = false
var check = false
var codegen = false
var evalground = false
- var unrollUnsatCores = true
+ var unrollUnsatCores = false
var pruneUnsatCores = true
for(opt <- context.options) opt match {
- case LeonFlagOption("checkmodels") => check = true
- case LeonFlagOption("feelinglucky") => lucky = true
- case LeonFlagOption("codegen") => codegen = true
- case LeonFlagOption("evalground") => evalground = true
+ case LeonFlagOption("checkmodels") => check = true
+ case LeonFlagOption("feelinglucky") => lucky = true
+ case LeonFlagOption("codegen") => codegen = true
+ case LeonFlagOption("evalground") => evalground = true
+ case LeonFlagOption("fairz3:unrollcores") => unrollUnsatCores = true
case _ =>
}
--
GitLab