diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index f9ed093844f524c128242f3a4b9100c5f9710475..08945e8d82f0581c761b7f8db31fa99f90cd8bc1 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -36,7 +36,8 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
" -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
" -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" +
" -P:funcheck:prune (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
- " -P:funcheck:cores (with CAV) Use UNSAT cores in the unrolling/refinement step."
+ " -P:funcheck:cores (with CAV) Use UNSAT cores in the unrolling/refinement step." + "\n" +
+ " -P:funcheck:lucky (with CAV) Perform additional tests to potentially find models early."
)
/** Processes the command-line options. */
@@ -58,6 +59,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
case "CAV" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case "prune" => purescala.Settings.pruneBranches = true
case "cores" => purescala.Settings.useCores = true
+ case "lucky" => purescala.Settings.luckyTest = true
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)): _*)
case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 2f4c0c9f27c460c660f24c7b31a62147ed5be328..5e5c17f93c9e492ed57da45190b92de94f49f9b5 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -215,6 +215,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
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]))
@@ -352,6 +354,10 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
None
}
+ // naive implementation of unrolling everything every n-th iteration
+ val unrollingThreshold = 100
+ var unrollingCounter = 0
+
val expandedVC = expandLets(if (forValidity) negate(vc) else vc)
toCheckAgainstModels = And(toCheckAgainstModels,expandedVC)
@@ -408,6 +414,10 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
z3SearchStopwatch.stop
(a, m, Seq.empty[Z3AST])
}
+ reporter.info(" - Finished search with blocked literals")
+
+ // if (Settings.useCores)
+ // reporter.info(" - Core is : " + core)
val reinterpretedAnswer = if(!UNKNOWNASSAT) answer else (answer match {
case None | Some(true) => Some(true)
@@ -455,24 +465,35 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
case (Some(false), m) => {
//m.delete
- if(!Settings.useCores) {
+ if(!Settings.useCores)
z3.pop(1)
+ if (Settings.luckyTest) {
+ // we need the model to perform the additional test
secondZ3SearchStopwatch.start
val (result2,m2) = z3.checkAndGetModel()
secondZ3SearchStopwatch.stop
- luckyStopwatch.start
if (result2 == Some(false)) {
foundAnswer(Some(true))
} else {
+ luckyStopwatch.start
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC, evaluator)
if(wereWeLucky) {
foundAnswer(Some(false), cleanModel)
}
+ luckyStopwatch.stop
+ }
+ } else {
+ // only checking will suffice
+ secondZ3SearchStopwatch.start
+ val result2 = z3.check()
+ secondZ3SearchStopwatch.stop
+
+ if (result2 == Some(false)) {
+ foundAnswer(Some(true))
}
- luckyStopwatch.stop
}
if(forceStop) {
@@ -485,15 +506,26 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
unrollingStopwatch.start
val toRelease : Set[Expr] = if(Settings.useCores) {
- core.map(ast => fromZ3Formula(ast) match {
- case n @ Not(Variable(_)) => n
- case v @ Variable(_) => v
- case _ => scala.Predef.error("Impossible element extracted from core: " + ast)
- }).toSet
+ unrollingCounter = unrollingCounter + 1
+ if (unrollingCounter > unrollingThreshold) {
+ reporter.info(" - Reached threshold for unrolling all blocked literals, will unroll all now.")
+ unrollingCounter = 0
+ blockingSet
+ } else {
+ // reporter.info(" - Will only unroll literals from core")
+ core.map(ast => fromZ3Formula(ast) match {
+ case n @ Not(Variable(_)) => n
+ case v @ Variable(_) => v
+ case _ => scala.Predef.error("Impossible element extracted from core: " + ast)
+ }).toSet
+ }
} else {
blockingSet
}
+ // reporter.info(" - toRelease : " + toRelease)
+ // reporter.info(" - blockingSet : " + blockingSet)
+
var fixedForEver : Set[Expr] = Set.empty
if(Settings.pruneBranches) {
@@ -885,7 +917,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
// stores the invocations that boolean literals are guarding.
private val blocked : MutableMap[(Identifier,Boolean),Set[FunctionInvocation]] = MutableMap.empty
-
+
// Returns whether some invocations were actually blocked in the end.
private def registerBlocked(blockingAtom : Identifier, polarity : Boolean, invocations : Set[FunctionInvocation]) : Boolean = {
val filtered = invocations.filter(i => {
@@ -1046,6 +1078,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
// TODO this is probably where the unrolling of the recursive call
// should actually occur, rather than delegating that to
// closeUnrollings.
+ // reporter.info("Unlocking : " + functionInvocation)
val (_, clauses, blockers) = closeUnrollings(functionInvocation)
newClauses = newClauses ++ clauses
newBlockers = newBlockers ++ blockers
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 8926d06ee921575468e52c8b4648d741b32ef137..a872ad20ed6d9151ea56257f09884102f75da370 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -21,4 +21,5 @@ object Settings {
var pruneBranches : Boolean = false
def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
var solverTimeout : Option[Int] = None
+ var luckyTest : Boolean = false
}