diff --git a/cp-demo/FirstClassConstraints.scala b/cp-demo/FirstClassConstraints.scala
index ed8285df6925419ad88d47afb95200b930c5bc62..8aa77372e1fff11504ac18f40c674aaba2bdbdc4 100644
--- a/cp-demo/FirstClassConstraints.scala
+++ b/cp-demo/FirstClassConstraints.scala
@@ -44,7 +44,9 @@ object FirstClassConstraints {
// println("has size 5: " + hasSize(5).expr)
- println(hasSize(5).solve)
+ // println(hasSize(5).solve)
+ val p : Term1[Int,Boolean] = ((x: Int) => x > 5)
+ println(p.solve)
// for (s <- hasSize(3).findAll)
// println(s)
}
diff --git a/cp-demo/RedBlackTree.scala b/cp-demo/RedBlackTree.scala
index f4b7edf230f0b1045aca9e70402fed854e0cb695..ec70cf978ea26c2d600dbbd92ed88b6a0dcb78d3 100644
--- a/cp-demo/RedBlackTree.scala
+++ b/cp-demo/RedBlackTree.scala
@@ -89,7 +89,7 @@ object RedBlackTree {
val defaultBound = 3
val bound = if (args.isEmpty) defaultBound else args(0).toInt
- enumerateAllUpTo(bound)
+ // enumerateAllUpTo(bound)
val solutionSet = scala.collection.mutable.Set[Tree]()
println("Fixing size of trees to " + (bound))
diff --git a/eval/cp/scripts/run-cp-evaluation b/eval/cp/scripts/run-cp-evaluation
index 139df7cdf6463cd9949dc6933f12a1db6054fc9a..5953844c3417c07e39bcda25b085163a360bef60 100755
--- a/eval/cp/scripts/run-cp-evaluation
+++ b/eval/cp/scripts/run-cp-evaluation
@@ -3,7 +3,6 @@
cd ../../..
ts=`date +%F-%R`
-evalFolder="eval/cp/data"
demoFolder="cp-demo"
#classes=( "RedBlackTree" "SortedList" )
@@ -18,6 +17,8 @@ class=${1}
base=${2}
limit=${3}
+evalFolder="eval/cp/data/${ts}-${class}"
+
mkdir -p ${evalFolder}
evalFileBase=${evalFolder}/${class}-${ts}-CAV
@@ -31,3 +32,17 @@ do
./generate-graph ../../../${currentFile}
cd ../../..
done
+
+evalFileBase=${evalFolder}/${class}-${ts}-CAV-scalaEval
+./cp CAV scalaEval ${demoFolder}/${class}.scala || (echo "Could not compile..." && exit 1)
+
+for (( i=${base}; i<=${limit}; i++ ))
+do
+ currentFile=${evalFileBase}-${i}
+ ./cp-runner ${class} $i | tee -a ${currentFile}
+ cd eval/cp/scripts
+ ./generate-graph ../../../${currentFile}
+ cd ../../..
+done
+
+mv eval/cp/graphs/${class}-${ts}-* ${evalFolder}
diff --git a/src/cp/CPPlugin.scala b/src/cp/CPPlugin.scala
index 6c0db086f8ef3a8fac3382e1782b092e8c835e39..3c8a1441859de0069129c7f22064a1ce3341ef29 100644
--- a/src/cp/CPPlugin.scala
+++ b/src/cp/CPPlugin.scala
@@ -27,7 +27,8 @@ class CPPlugin(val global: Global) extends Plugin {
" -P:constraint-programming:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
" -P:constraint-programming:CAV CAV 2011 settings. In progress." + "\n" +
" -P:constraint-programming:prune (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
- " -P:constraint-programming:cores (with CAV) Use UNSAT cores in the unrolling/refinement step."
+ " -P:constraint-programming:cores (with CAV) Use UNSAT cores in the unrolling/refinement step." + "\n" +
+ " -P:constraint-programming:scalaEval (with CAV) Use functions stored in constraints to evaluate models."
)
/** Processes the command-line options. */
@@ -46,6 +47,7 @@ class CPPlugin(val global: Global) extends Plugin {
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 "scalaEval" => cp.Settings.useScalaEvaluator = 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/cp/Converter.scala b/src/cp/Converter.scala
index 05c14b73adc9e4ef3c870b67b2910996500305aa..ae68a22ad362b493e1ba869463330f7fa4758b42 100644
--- a/src/cp/Converter.scala
+++ b/src/cp/Converter.scala
@@ -4,7 +4,7 @@ import purescala.Trees._
/** A converter has functions for converting FunCheck expressions into Scala
* values */
-class Converter(expr2scala : (Expr => Any)) {
+class Converter(val expr2scala : (Expr => Any)) {
def exprSeq2scala1[T1](exprs : Seq[Expr]) : (T1) =
(expr2scala(exprs(0)).asInstanceOf[T1])
diff --git a/src/cp/RuntimeMethods.scala b/src/cp/RuntimeMethods.scala
index 2905bbf25bcd9992f9927236d2537cd5bbf35887..a3a820860400a1bacbb8bbad787445e82b040577 100644
--- a/src/cp/RuntimeMethods.scala
+++ b/src/cp/RuntimeMethods.scala
@@ -105,6 +105,8 @@ object RuntimeMethods {
purescala.Settings.useCores = recovered.useCores
purescala.Settings.pruneBranches = recovered.pruneBranches
purescala.Settings.solverTimeout = recovered.solverTimeout
+
+ Settings.useScalaEvaluator = recovered.useScalaEvaluator
}
def inputVar(inputVarList : List[Variable], varName : String) : Variable = {
diff --git a/src/cp/RuntimeSettings.scala b/src/cp/RuntimeSettings.scala
index 205d85593befb834d8019b90347fa6818c772b9d..813ebb88470e61db972ff62f307bc1a20d0b91f5 100644
--- a/src/cp/RuntimeSettings.scala
+++ b/src/cp/RuntimeSettings.scala
@@ -12,4 +12,10 @@ package cp
var useCores : Boolean = purescala.Settings.useCores
var pruneBranches : Boolean = purescala.Settings.pruneBranches
var solverTimeout : Option[Int] = purescala.Settings.solverTimeout
+
+ var useScalaEvaluator : Boolean = Settings.useScalaEvaluator
+}
+
+object Settings {
+ var useScalaEvaluator : Boolean = false
}
diff --git a/src/cp/Terms.scala b/src/cp/Terms.scala
index f3752ff4264d6e57a18e93edfdbddcf8b96e9bcd..e87074319f5eee28086aeb5045ca7ad724752372 100644
--- a/src/cp/Terms.scala
+++ b/src/cp/Terms.scala
@@ -16,12 +16,13 @@ object Terms {
/** The converting function defines how Expr values returned by the solver
* will be converted back to Scala values */
val convertingFunction : (Seq[Expr] => T)
+ val evaluator : (Seq[Expr]) => R
- def solve(implicit asBoolean: (R) => Boolean) : T = {
- convertingFunction(solveExprSeq(this))
+ def solve(implicit asConstraint: (Term[T,R]) => Term[T,Boolean]) : T = {
+ convertingFunction(solveExprSeq(asConstraint(this)))
}
- def find(implicit asBoolean: (R) => Boolean) : Option[T] = {
+ def find(implicit asConstraint: (Term[T,R]) => Term[T,Boolean]) : Option[T] = {
try {
Some(this.solve)
} catch {
@@ -30,8 +31,8 @@ object Terms {
}
}
- def findAll(implicit asBoolean: (R) => Boolean) : Iterator[T] = {
- findAllExprSeq(this).map(convertingFunction(_))
+ def findAll(implicit asConstraint: (Term[T,R]) => Term[T,Boolean]) : Iterator[T] = {
+ findAllExprSeq(asConstraint(this)).map(convertingFunction(_))
}
}
@@ -118,6 +119,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala1[T1] _
type t2c = (Term1[T1,R]) => Term1[T1,Boolean]
val scalaFunction : (T1) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1])
override def apply(x_0 : T1) : R = scalaFunction(x_0)
@@ -184,6 +186,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala2[T1,T2] _
type t2c = (Term2[T1,T2,R]) => Term2[T1,T2,Boolean]
val scalaFunction : (T1,T2) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2])
override def apply(x_0 : T1, x_1 : T2) : R = scalaFunction(x_0, x_1)
@@ -285,6 +288,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala3[T1,T2,T3] _
type t2c = (Term3[T1,T2,T3,R]) => Term3[T1,T2,T3,Boolean]
val scalaFunction : (T1,T2,T3) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3) : R = scalaFunction(x_0, x_1, x_2)
@@ -411,6 +415,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala4[T1,T2,T3,T4] _
type t2c = (Term4[T1,T2,T3,T4,R]) => Term4[T1,T2,T3,T4,Boolean]
val scalaFunction : (T1,T2,T3,T4) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4) : R = scalaFunction(x_0, x_1, x_2, x_3)
@@ -552,6 +557,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala5[T1,T2,T3,T4,T5] _
type t2c = (Term5[T1,T2,T3,T4,T5,R]) => Term5[T1,T2,T3,T4,T5,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4)
@@ -698,6 +704,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala6[T1,T2,T3,T4,T5,T6] _
type t2c = (Term6[T1,T2,T3,T4,T5,T6,R]) => Term6[T1,T2,T3,T4,T5,T6,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5)
@@ -839,6 +846,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala7[T1,T2,T3,T4,T5,T6,T7] _
type t2c = (Term7[T1,T2,T3,T4,T5,T6,T7,R]) => Term7[T1,T2,T3,T4,T5,T6,T7,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6,T7) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6, x_6 : T7) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5, x_6)
@@ -965,6 +973,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala8[T1,T2,T3,T4,T5,T6,T7,T8] _
type t2c = (Term8[T1,T2,T3,T4,T5,T6,T7,T8,R]) => Term8[T1,T2,T3,T4,T5,T6,T7,T8,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6,T7,T8) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7],converter.expr2scala(s(7)).asInstanceOf[T8])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6, x_6 : T7, x_7 : T8) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7)
@@ -1066,6 +1075,7 @@ object Terms {
val convertingFunction = converterOf(this).exprSeq2scala9[T1,T2,T3,T4,T5,T6,T7,T8,T9] _
type t2c = (Term9[T1,T2,T3,T4,T5,T6,T7,T8,T9,R]) => Term9[T1,T2,T3,T4,T5,T6,T7,T8,T9,Boolean]
val scalaFunction : (T1,T2,T3,T4,T5,T6,T7,T8,T9) => R
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(converter.expr2scala(s(0)).asInstanceOf[T1],converter.expr2scala(s(1)).asInstanceOf[T2],converter.expr2scala(s(2)).asInstanceOf[T3],converter.expr2scala(s(3)).asInstanceOf[T4],converter.expr2scala(s(4)).asInstanceOf[T5],converter.expr2scala(s(5)).asInstanceOf[T6],converter.expr2scala(s(6)).asInstanceOf[T7],converter.expr2scala(s(7)).asInstanceOf[T8],converter.expr2scala(s(8)).asInstanceOf[T9])
override def apply(x_0 : T1, x_1 : T2, x_2 : T3, x_3 : T4, x_4 : T5, x_5 : T6, x_6 : T7, x_7 : T8, x_8 : T9) : R = scalaFunction(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8)
@@ -1351,14 +1361,20 @@ object Terms {
case None => simplestValue(varId.getType)
}
+ private def evaluator(constraint : Term[_,Boolean], ids : Seq[Identifier]) : Option[(Map[Identifier,Expr])=>Boolean] = {
+ if (cp.Settings.useScalaEvaluator) {
+ Some((m : Map[Identifier,Expr]) => constraint.evaluator(ids.map(modelValue(_, m))))
+ } else None
+ }
+
/** Return a solution as a sequence of expressions */
- private def solveExprSeq(c : Term[_,_]) : Seq[Expr] = {
- val constraint = c.asInstanceOf[Constraint[_]]
+ private def solveExprSeq(constraint : Term[_,Boolean]) : Seq[Expr] = {
val solver = newSolver(programOf(constraint))
val (freshOutputIDs, expr) = combineConstraint(constraint)
- val (outcome, model) = solver.restartAndDecideWithModel(expr, false)
+ solver.restartZ3
+ val (outcome, model) = solver.decideWithModel(expr, false, evaluator(constraint, freshOutputIDs))
outcome match {
case Some(false) =>
@@ -1385,12 +1401,11 @@ object Terms {
}
/** Return an iterator of solutions as sequences of expressions */
- private def findAllExprSeq(c : Term[_,_]) : Iterator[Seq[Expr]] = {
- val constraint = c.asInstanceOf[Constraint[_]]
+ private def findAllExprSeq(constraint : Term[_,Boolean]) : Iterator[Seq[Expr]] = {
val program = programOf(constraint)
val (freshOutputIDs, expr) = combineConstraint(constraint)
- val modelIterator = solutionsIterator(program, expr, freshOutputIDs.toSet)
+ val modelIterator = solutionsIterator(program, expr, freshOutputIDs, evaluator(constraint, freshOutputIDs))
val exprIterator = modelIterator.map(model => freshOutputIDs.map(id => model(id)))
exprIterator
@@ -1419,7 +1434,7 @@ object Terms {
val minValue = minimizingModelAndValue(program, toCheck, outputVars, minExpr)._2
val minValConstraint = And(expr, Equals(minExpr, IntLiteral(minValue)))
- val minValModelIterator = solutionsIterator(program, minValConstraint, outputVars.toSet)
+ val minValModelIterator = solutionsIterator(program, minValConstraint, outputVars)
val minValExprIterator = minValModelIterator.map(model => outputVars.map(id => model(id)))
minValExprIterator ++ findAllMinimizingExprSeq(program, expr, outputVars, minExpr, Some(minValue))
@@ -1447,7 +1462,8 @@ object Terms {
// println(" hi : " + hi)
// println
val toCheck = expr :: LessEquals(minExpr, IntLiteral(pivot)) :: Nil
- val (outcome, model) = solver.restartAndDecideWithModel(And(toCheck), false)
+ solver.restartZ3
+ val (outcome, model) = solver.decideWithModel(And(toCheck), false)
outcome match {
case Some(false) =>
@@ -1484,7 +1500,8 @@ object Terms {
// We declare a variable to hold the value to minimize:
val minExprID = purescala.Common.FreshIdentifier("minExpr").setType(purescala.TypeTrees.Int32Type)
- solver.restartAndDecideWithModel(And(expr :: Equals(minExpr, Variable(minExprID)) :: Nil), false) match {
+ solver.restartZ3
+ solver.decideWithModel(And(expr :: Equals(minExpr, Variable(minExprID)) :: Nil), false) match {
case (Some(false), model) =>
// there is a satisfying assignment
val minExprVal = modelValue(minExprID, model) match {
@@ -1501,7 +1518,7 @@ object Terms {
}
}
/** Returns an iterator of interpretations for each identifier in the specified set */
- private def solutionsIterator(program : Program, predicate : Expr, outputVariables : Set[Identifier]) : Iterator[Map[Identifier, Expr]] = {
+ private def solutionsIterator(program : Program, predicate : Expr, outputVariables : Seq[Identifier], evaluator : Option[(Map[Identifier,Expr]) => Boolean] = None) : Iterator[Map[Identifier, Expr]] = {
val solver = newSolver(program)
solver.restartZ3
@@ -1514,12 +1531,13 @@ object Terms {
var addedNegations: Expr = BooleanLiteral(true)
var toCheck: Expr = predicate
+ var toUseAsEvaluator : Option[(Map[Identifier,Expr]) => Boolean] = evaluator
override def hasNext : Boolean = nextModel match {
case None =>
// Check whether there are any more models
val stopwatch = new Stopwatch("hasNext", false).start
- val (outcome, model) = solver.decideWithModel(toCheck, false)
+ val (outcome, model) = solver.decideWithModel(toCheck, false, toUseAsEvaluator)
stopwatch.stop
stopwatch.writeToSummary
val toReturn = (outcome match {
@@ -1535,8 +1553,9 @@ object Terms {
}
}
nextModel = Some(Some(completeModel))
- val newModelEqualities = And(outputVariables.map(ov => Equals(Variable(ov), completeModel(ov))).toList)
+ val newModelEqualities = And(outputVariables.map(ov => Equals(Variable(ov), completeModel(ov))))
toCheck = negate(newModelEqualities)
+ toUseAsEvaluator = toUseAsEvaluator.map(e => ((m : Map[Identifier,Expr]) => e(m) && !m.forall{ case (k,v) => completeModel.get(k) == Some(v) }))
true
case Some(true) =>
// there are definitely no more solutions
@@ -1572,8 +1591,9 @@ object Terms {
}
}
- val newModelEqualities = And(outputVariables.map(ov => Equals(Variable(ov), completeModel(ov))).toList)
+ val newModelEqualities = And(outputVariables.map(ov => Equals(Variable(ov), completeModel(ov))))
toCheck = negate(newModelEqualities)
+ toUseAsEvaluator = toUseAsEvaluator.map(e => ((m : Map[Identifier,Expr]) => e(m) && !m.forall{ case (k,v) => completeModel.get(k) == Some(v) }))
completeModel
case Some(true) =>
// Definitely no more solutions
diff --git a/src/cp/Utils.scala b/src/cp/Utils.scala
index d372744289f4cb1e89073db9ac354605a22d7aa7..a362eff4b4d25db2579e4603e2e2dff627348cb7 100644
--- a/src/cp/Utils.scala
+++ b/src/cp/Utils.scala
@@ -59,11 +59,13 @@ object Utils {
val (applyParams, applyArgs) = traitArgParams.zipWithIndex.map{ case (p, i) => ("x_%d : %s" format (i, p), "x_%d" format (i)) }.unzip
+ val evaluatorArgs = traitArgParams.zipWithIndex.map{ case (p, i) => "converter.expr2scala(s(%d)).asInstanceOf[%s]" format (i, p) }
val termTraitString =
"""sealed trait %s extends Term[%s,%s] with Function%d[%s] {
val convertingFunction = converterOf(this).exprSeq2scala%d[%s] _
type t2c = (%s) => %s
val scalaFunction : %s => %s
+ val evaluator : (Seq[Expr]) => R = (s : Seq[Expr]) => scalaFunction(%s)
override def apply(%s) : R = scalaFunction(%s)
@@ -76,7 +78,13 @@ object Utils {
%s
%s
-}""" format (traitName, termClassParamTuple, "R", arity, traitParams.mkString(","), arity, traitArgParamsString, traitName, booleanTraitName, termClassParamTuple, "R", applyParams.mkString(", "), applyArgs.mkString(", "), indent(orMethod), indent(andMethod), indent(notMethod), indent(minimizingMethod), indent(composeMethods))
+}""" format (traitName, termClassParamTuple, "R", arity, traitParams.mkString(","),
+ arity, traitArgParamsString,
+ traitName, booleanTraitName,
+ termClassParamTuple, "R",
+ evaluatorArgs.mkString(","),
+ applyParams.mkString(", "), applyArgs.mkString(", "),
+ indent(orMethod), indent(andMethod), indent(notMethod), indent(minimizingMethod), indent(composeMethods))
termTraitString
}
diff --git a/src/purescala/Evaluator.scala b/src/purescala/Evaluator.scala
index c624b4f9b01736f9ba76f7b8cadc0ced64568277..3a9ab97acf8d4cb6948ae69c1a83a599bc2e6f48 100644
--- a/src/purescala/Evaluator.scala
+++ b/src/purescala/Evaluator.scala
@@ -25,7 +25,7 @@ object Evaluator {
val finalResult = None
}
- def eval(context: EvaluationContext, expression: Expr, maxSteps: Int=500000) : EvaluationResult = {
+ def eval(context: EvaluationContext, expression: Expr, evaluator: Option[(EvaluationContext)=>Boolean], maxSteps: Int=500000) : EvaluationResult = {
case class RuntimeErrorEx(msg: String) extends Exception
case class InfiniteComputationEx() extends Exception
case class TypeErrorEx(typeError: TypeError) extends Exception
@@ -240,12 +240,21 @@ object Evaluator {
}
}
- try {
- OK(rec(context, expression))
- } catch {
- case RuntimeErrorEx(msg) => RuntimeError(msg)
- case InfiniteComputationEx() => InfiniteComputation()
- case TypeErrorEx(te) => te
+ evaluator match {
+ case Some(evalFun) =>
+ try {
+ OK(BooleanLiteral(evalFun(context)))
+ } catch {
+ case e: Exception => RuntimeError(e.getMessage)
+ }
+ case None =>
+ try {
+ OK(rec(context, expression))
+ } catch {
+ case RuntimeErrorEx(msg) => RuntimeError(msg)
+ case InfiniteComputationEx() => InfiniteComputation()
+ case TypeErrorEx(te) => te
+ }
}
}
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 6371d0a309372832a1270b958ffe5e1e43f263ea..37d8d2f36d026844e36300d4e247ee64f827f96e 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -304,12 +304,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
decideWithModel(vc, forValidity)._1
}
- def restartAndDecideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
- restartZ3
- decideWithModel(vc, forValidity)
- }
-
- def decideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
+ def decideWithModel(vc: Expr, forValidity: Boolean, evaluator: Option[(Map[Identifier,Expr])=> Boolean] = None): (Option[Boolean], Map[Identifier,Expr]) = {
val initializationStopwatch = new Stopwatch("init", false)
val blocking2Z3Stopwatch = new Stopwatch("blocking-set-to-z3", false)
val z3SearchStopwatch = new Stopwatch("z3-search-1", false)
@@ -423,7 +418,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
case (Some(true), m) => { // SAT
validatingStopwatch.start
- val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC)
+ val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
validatingStopwatch.stop
if (trueModel) {
@@ -464,7 +459,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
foundAnswer(Some(true))
} else {
// we might have been lucky :D
- val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC)
+ val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC, evaluator)
if(wereWeLucky) {
foundAnswer(Some(false), cleanModel)
}
@@ -581,14 +576,14 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
}
- private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier]) : (Boolean, Map[Identifier,Expr]) = {
+ private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier], evaluator: Option[(Map[Identifier,Expr])=>Boolean]) : (Boolean, Map[Identifier,Expr]) = {
import Evaluator._
val asMap = modelToMap(model, variables)
model.delete
lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
- val evalResult = eval(asMap, formula)
+ val evalResult = eval(asMap, formula, evaluator)
evalResult match {
case OK(BooleanLiteral(true)) => {
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index bcb868d46b2c4daaf943c12cfc97b258bc6ee000..f6f9a424fd2fa6c17d873e9d69e5b7eb5b7c959e 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -470,7 +470,7 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
//println("(I'm going to pretend this never happened...)")
- val evalResult = eval(asMap, toCheckAgainstModels)
+ val evalResult = eval(asMap, toCheckAgainstModels, None)
evalResult match {