From 1a0b9f9387fbbf48c39757c9bb2e2389b37597df Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 4 Jan 2013 00:44:09 +0100
Subject: [PATCH] --evalground makes FairZ3 evaluate ground applications
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Without the flag, functions applied to ground arguments are treated the
same way as every other one: by unrolling their body. This is
suboptimal, as we can instead pass to Z3 the equality f(a0, a1) = v,
instead of letting it "discover" it by itself.
Note that this hasn't been shown to bring any major performance
improvement; ground applications hardly show up in verification, for
instance. But think about it, you'll agree using evaluation there is
"The right thing to do.™".
Note that testing --evalground currently highlights some bugs.
---
.../leon/solvers/z3/AbstractZ3Solver.scala | 42 +++++++++++++++++++
.../scala/leon/solvers/z3/FairZ3Solver.scala | 20 +++++----
.../leon/solvers/z3/FunctionTemplate.scala | 34 ++++++++++++---
.../PureScalaVerificationRegression.scala | 2 +-
4 files changed, 83 insertions(+), 15 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 2a14a92f5..b3e8df10c 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -690,6 +690,48 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
rec(tree, expectedType)
}
+ // Tries to convert a Z3AST into a *ground* Expr. Doesn't try very hard, because
+ // 1) we assume Z3 simplifies ground terms, so why match for +, etc, and
+ // 2) we use this precisely in one context, where we know function invocations won't show up, etc.
+ protected[leon] def asGround(tree : Z3AST) : Option[Expr] = {
+ val e = new Exception("Not ground.")
+
+ def rec(t : Z3AST) : Expr = z3.getASTKind(t) match {
+ case Z3AppAST(decl, args) => {
+ val argsSize = args.size
+ if(isKnownDecl(decl)) {
+ val fd = functionDeclToDef(decl)
+ FunctionInvocation(fd, args.map(rec))
+ } else if(argsSize == 1 && reverseADTTesters.isDefinedAt(decl)) {
+ CaseClassInstanceOf(reverseADTTesters(decl), rec(args(0)))
+ } else if(argsSize == 1 && reverseADTFieldSelectors.isDefinedAt(decl)) {
+ val (ccd, fid) = reverseADTFieldSelectors(decl)
+ CaseClassSelector(ccd, rec(args(0)), fid)
+ } else if(reverseADTConstructors.isDefinedAt(decl)) {
+ val ccd = reverseADTConstructors(decl)
+ CaseClass(ccd, args.map(rec))
+ } else if(reverseTupleConstructors.isDefinedAt(decl)) {
+ Tuple(args.map(rec))
+ } else {
+ import Z3DeclKind._
+ z3.getDeclKind(decl) match {
+ case OpTrue => BooleanLiteral(true)
+ case OpFalse => BooleanLiteral(false)
+ case _ => throw e
+ }
+ }
+ }
+ case Z3NumeralAST(Some(v)) => IntLiteral(v)
+ case _ => throw e
+ }
+
+ try {
+ Some(rec(tree))
+ } catch {
+ case e : Exception => None
+ }
+ }
+
protected[leon] def softFromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: TypeTree) : Option[Expr] = {
try {
Some(fromZ3Formula(model, tree, Some(expectedType)))
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3523e1ce7..641b86c81 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -29,28 +29,32 @@ 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")
)
// What wouldn't we do to avoid defining vars?
- val (feelingLucky, checkModels, useCodeGen) = locally {
- var lucky = false
- var check = false
- var codegen = false
+ val (feelingLucky, checkModels, useCodeGen, evalGroundApps) = locally {
+ var lucky = false
+ var check = false
+ var codegen = false
+ var evalground = false
for(opt <- context.options) opt match {
- case LeonFlagOption("checkmodels") => check = true
- case LeonFlagOption("feelinglucky") => lucky = true
- case LeonFlagOption("codegen") => codegen = true
+ case LeonFlagOption("checkmodels") => check = true
+ case LeonFlagOption("feelinglucky") => lucky = true
+ case LeonFlagOption("codegen") => codegen = true
+ case LeonFlagOption("evalground") => evalground = true
case _ =>
}
- (lucky,check,codegen)
+ (lucky,check,codegen,evalground)
}
private var evaluator : Evaluator = null
+ protected[z3] def getEvaluator : Evaluator = evaluator
override def setProgram(prog : Program) {
super.setProgram(prog)
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 2d6399660..66cb6af25 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -1,7 +1,6 @@
package leon
package solvers.z3
-import z3.scala._
import purescala.Common._
import purescala.Trees._
import purescala.Extractors._
@@ -9,18 +8,22 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
+import evaluators._
+
+import z3.scala._
+
import scala.collection.mutable.{Set=>MutableSet,Map=>MutableMap}
case class Z3FunctionInvocation(funDef: FunDef, args: Seq[Z3AST])
-// TODO: maybe a candidate for moving into purescala package?
class FunctionTemplate private(
- solver: AbstractZ3Solver,
+ solver: FairZ3Solver,
val funDef : FunDef,
activatingBool : Identifier,
condVars : Set[Identifier],
exprVars : Set[Identifier],
- guardedExprs : Map[(Identifier,Boolean),Seq[Expr]]) {
+ guardedExprs : Map[(Identifier,Boolean),Seq[Expr]],
+ isRealFunDef : Boolean) {
private val z3 = solver.z3
@@ -67,6 +70,24 @@ class FunctionTemplate private(
def instantiate(aVar : Z3AST, aPol : Boolean, args : Seq[Z3AST]) : (Seq[Z3AST], Map[(Z3AST, Boolean), Set[Z3FunctionInvocation]]) = {
assert(args.size == funDef.args.size)
+ // The "isRealFunDef" part is to prevent evaluation of "fake" function templates, as generated from FairZ3Solver.
+ if(solver.evalGroundApps && isRealFunDef) {
+ val ga = args.view.map(solver.asGround)
+ if(ga.forall(_.isDefined)) {
+ val leonArgs = ga.map(_.get).force
+ val invocation = FunctionInvocation(funDef, leonArgs)
+ solver.getEvaluator.eval(invocation) match {
+ case EvaluationSuccessful(result) =>
+ val z3Invocation = z3.mkApp(solver.functionDefToDecl(funDef), args: _*)
+ val z3Value = solver.toZ3Formula(result).get
+ val asZ3 = z3.mkEq(z3Invocation, z3Value)
+ return (Seq(asZ3), Map.empty)
+
+ case _ => throw new Exception("Evaluation of ground term should have succeeded.")
+ }
+ }
+ }
+
val idSubstMap : Map[Z3AST, Z3AST] =
Map(z3ActivatingBool -> (if (aPol) aVar else z3.mkNot(aVar))) ++
(zippedExprVars ++ zippedCondVars).map{ case (id, c) => c -> solver.idToFreshZ3Id(id) } ++
@@ -102,7 +123,7 @@ class FunctionTemplate private(
}
object FunctionTemplate {
- def mkTemplate(solver: AbstractZ3Solver, funDef: FunDef, isRealFunDef : Boolean = true) : FunctionTemplate = {
+ def mkTemplate(solver: FairZ3Solver, funDef: FunDef, isRealFunDef : Boolean = true) : FunctionTemplate = {
val condVars : MutableSet[Identifier] = MutableSet.empty
val exprVars : MutableSet[Identifier] = MutableSet.empty
@@ -210,6 +231,7 @@ object FunctionTemplate {
storeGuarded(activatingBool, true, finalPred2)
}
- new FunctionTemplate(solver, funDef, activatingBool, Set(condVars.toSeq : _*), Set(exprVars.toSeq : _*), Map(guardedExprs.toSeq : _*))
+ new FunctionTemplate(solver, funDef, activatingBool, Set(condVars.toSeq : _*), Set(exprVars.toSeq : _*), Map(guardedExprs.toSeq : _*),
+isRealFunDef)
}
}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 74ce1ddc9..c7e712295 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -68,7 +68,7 @@ class PureScalaVerificationRegression extends FunSuite {
for(f <- fs) {
mkTest(f, List(LeonFlagOption("feelinglucky")), forError)(block)
- mkTest(f, List(LeonFlagOption("codegen"), LeonFlagOption("feelinglucky")), forError)(block)
+ mkTest(f, List(LeonFlagOption("codegen"), LeonFlagOption("evalground"), LeonFlagOption("feelinglucky")), forError)(block)
}
}
--
GitLab