From 8d899398ab2adcc9b80738748988f6837771c5f2 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 10 Jun 2015 19:32:47 +0200
Subject: [PATCH] Introducing GroundSolver

---
 .../leon/evaluators/RecursiveEvaluator.scala  |  2 +-
 .../scala/leon/solvers/GroundSolver.scala     | 55 +++++++++++++++++++
 .../scala/leon/solvers/SolverFactory.scala    |  4 ++
 .../verification/NewSolversRegression.scala   |  2 +-
 4 files changed, 61 insertions(+), 2 deletions(-)
 create mode 100644 src/main/scala/leon/solvers/GroundSolver.scala

diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index e96aa69b8..77e74b530 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -70,7 +70,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
     }
   }
 
-  def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
+  protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
     case Variable(id) =>
       rctx.mappings.get(id) match {
         case Some(v) if v != expr =>
diff --git a/src/main/scala/leon/solvers/GroundSolver.scala b/src/main/scala/leon/solvers/GroundSolver.scala
new file mode 100644
index 000000000..fd744bb6e
--- /dev/null
+++ b/src/main/scala/leon/solvers/GroundSolver.scala
@@ -0,0 +1,55 @@
+package leon
+package solvers
+
+import evaluators.DefaultEvaluator
+import evaluators.EvaluationResults._
+import purescala.Common.Identifier
+import purescala.Definitions.Program
+import purescala.Expressions.{BooleanLiteral, Expr}
+import purescala.ExprOps.isGround
+import purescala.Constructors.andJoin
+import utils.Interruptible
+
+// This solver only "solves" ground terms by evaluating them
+class GroundSolver(val context: LeonContext, val program: Program) extends Solver with Interruptible {
+
+  context.interruptManager.registerForInterrupts(this)
+
+  val evaluator = new DefaultEvaluator(context, program)
+  val dbg: Any => Unit = context.reporter.debug(_)
+
+  def name: String = "ground"
+
+  private var assertions: List[Expr] = Nil
+
+  // Ground terms will always have the empty model
+  def getModel: Map[Identifier, Expr] = Map()
+
+  def assertCnstr(expression: Expr): Unit = assertions ::= expression
+
+  def check: Option[Boolean] = {
+    val expr = andJoin(assertions)
+
+    if (isGround(expr)) {
+      evaluator.eval(expr) match {
+        case Successful(BooleanLiteral(result)) =>
+          Some(result)
+        case RuntimeError(message) =>
+          dbg(s"Evaluation of $expr resulted in runtime error")
+          Some(false)
+        case _ =>
+          dbg(s"Solver $name encountered error during evaluation.")
+          None
+      }
+    } else {
+      dbg(s"Non-ground expression $expr given to solver $name")
+      None
+    }
+  }
+
+  def free(): Unit = assertions = Nil
+
+  def interrupt(): Unit = {}
+
+  def recoverInterrupt(): Unit = {}
+}
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 7704bdf38..42479fa01 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -37,6 +37,7 @@ object SolverFactory {
     "smt-cvc4-proof" -> "CVC4 through SMT-LIB, in-solver inductive reasoning, for proofs only",
     "smt-cvc4-cex"   -> "CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only",
     "unrollz3"       -> "Native Z3 with leon-templates for unfolding",
+    "ground"         -> "Only solves ground terms by evaluating them",
     "enum"           -> "Enumeration-based counter-example-finder"
   )
   
@@ -81,6 +82,9 @@ object SolverFactory {
       case "enum"   =>
         SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
 
+      case "ground" =>
+        SolverFactory(() => new GroundSolver(ctx, program) with TimeoutSolver)
+
       case "smt-z3" =>
         SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
 
diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala
index d7793a3b1..929c7e156 100644
--- a/src/test/scala/leon/test/verification/NewSolversRegression.scala
+++ b/src/test/scala/leon/test/verification/NewSolversRegression.scala
@@ -26,7 +26,7 @@ class NewSolversRegression extends VerificationRegression {
     }
 
     if (isCVC4Available)
-      List(List("--solvers=smt-cvc4-cex,smt-cvc4-proof", "--feelinglucky", "--timeout=3"))
+      List(List("--solvers=smt-cvc4-cex,smt-cvc4-proof", "--feelinglucky", "--timeout=5"))
     else Nil
 
   }
-- 
GitLab