diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala index 2a14a92f5636cab373bfb9f5ca1d496c948050d3..b3e8df10c058e4ef4e1d70067fc44af26e7c121f 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 3523e1ce71703db35dd9346269dd284e5de91d42..641b86c81bfc49aae5fb9baccf67102a1187fc9d 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 2d63996602d92af44b748e81b0bc2de21cedba79..66cb6af25f3008dc2427a41453f8c150fd23ab87 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 74ce1ddc96488bd5a401602de0d788546feac4f5..c7e7122956ecc1835bf9002d0a384c114e6ed336 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) } }