--evalground makes FairZ3 evaluate ground applications

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.

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)))

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)

src/main/scala/leon/solvers/z3/FunctionTemplate.scala

 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)
   }
 }

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)
     }
   }