From 3dc2bb81c2dc9ab71486bc3000b44b8511f2ed08 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 21 Jan 2011 21:27:06 +0000
Subject: [PATCH]
---
src/funcheck/FunCheckPlugin.scala | 4 ++-
src/purescala/FairZ3Solver.scala | 58 +++++++++++++++++++++++++------
src/purescala/Settings.scala | 1 +
3 files changed, 51 insertions(+), 12 deletions(-)
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 9337fb700..863ac8a16 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -33,7 +33,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
" -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
- " -P:funcheck:CAV CAV 2011 settings. In progress."
+ " -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" +
+ " -P:funcheck:prune (with CAV) Use additional SMT queries to rule out some unrollings."
)
/** Processes the command-line options. */
@@ -54,6 +55,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "XP" => purescala.Settings.experimental = true
case "PLDI" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = true; purescala.Settings.useFairInstantiator = false; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
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 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 9dbdfd178..de6e68676 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -327,19 +327,52 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
definitiveAnswer = Some(false)
definitiveModel = cleanModel
} else {
- reporter.info("We need to keep going.")
-
- val toRelease : Set[Expr] = if(USEUNSATCORE) {
- blockingSet//core.map(fromZ3Formula(_)).toSet
- } else {
- blockingSet
+ reporter.info("- We need to keep going.")
+
+ val toRelease : Set[Expr] = blockingSet
+
+ var fixedForEver : Set[Expr] = Set.empty
+
+ if(Settings.pruneBranches) {
+ for(ex <- blockingSet) ex match {
+ case Not(Variable(b)) => {
+ z3.push
+ z3.assertCnstr(toZ3Formula(z3, Variable(b)).get)
+ z3.check match {
+ case Some(false) => {
+ //println("We had ~" + b + " in the blocking set. We now know it should stay there forever.")
+ z3.pop(1)
+ z3.assertCnstr(toZ3Formula(z3, Not(Variable(b))).get)
+ fixedForEver = fixedForEver + ex
+ }
+ case _ => z3.pop(1)
+ }
+ }
+ case Variable(b) => {
+ z3.push
+ z3.assertCnstr(toZ3Formula(z3, Not(Variable(b))).get)
+ z3.check match {
+ case Some(false) => {
+ //println("We had " + b + " in the blocking set. We now know it should stay there forever.")
+ z3.pop(1)
+ z3.assertCnstr(toZ3Formula(z3, Variable(b)).get)
+ fixedForEver = fixedForEver + ex
+ }
+ case _ => z3.pop(1)
+ }
+ }
+ case _ => scala.Predef.error("Should not have happened.")
+ }
+ if(fixedForEver.size > 0) {
+ reporter.info("- Pruned out " + fixedForEver.size + " branches.")
+ }
}
// println("Release set : " + toRelease)
blockingSet = blockingSet -- toRelease
- val toReleaseAsPairs : Set[(Identifier,Boolean)] = toRelease.map(b => b match {
+ val toReleaseAsPairs : Set[(Identifier,Boolean)] = (toRelease -- fixedForEver).map(b => b match {
case Variable(id) => (id, true)
case Not(Variable(id)) => (id, false)
case _ => scala.Predef.error("Impossible value in release set: " + b)
@@ -353,7 +386,10 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
// z3.assertCnstr(toZ3Formula(z3, clause).get)
// }
- z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
+ for(ncl <- newClauses) {
+ z3.assertCnstr(toZ3Formula(z3, ncl).get)
+ }
+ //z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
}
@@ -377,17 +413,17 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
evalResult match {
case OK(BooleanLiteral(true)) => {
- reporter.info("Model validated:")
+ reporter.info("- Model validated:")
reporter.info(modelAsString)
(true, asMap)
}
case RuntimeError(msg) => {
- reporter.info("Model leads to runtime error: " + msg)
+ reporter.info("- Model leads to runtime error: " + msg)
reporter.error(modelAsString)
(true, asMap)
}
case OK(BooleanLiteral(false)) => {
- reporter.info("Invalid model.")
+ reporter.info("- Invalid model.")
(false, Map.empty)
}
case other => {
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index c1e378783..5510626eb 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -19,5 +19,6 @@ object Settings {
var testBounds: (Int, Int) = (0, 3)
var useInstantiator: Boolean = false
var useFairInstantiator: Boolean = false
+ var pruneBranches : Boolean = false
def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
}
--
GitLab