Add support for non-incremental solver

Author: jad-hamza

src/it/scala/inox/tip/TipTestSuite.scala

@@ -13,12 +13,14 @@ class TipTestSuite extends TestSuite with ResourceUtils {
     Seq(optSelectedSolvers(Set("nativez3")), optCheckModels(true)),
     Seq(optSelectedSolvers(Set("smt-z3")),   optCheckModels(true)),
     Seq(optSelectedSolvers(Set("smt-cvc4")), optCheckModels(true)),
-    Seq(optSelectedSolvers(Set("smt-z3")),   optCheckModels(true), optAssumeChecked(true))
+    Seq(optSelectedSolvers(Set("smt-z3")),   optCheckModels(true), optAssumeChecked(true)),
+    Seq(optSelectedSolvers(Set("smt-z3")),   optCheckModels(true), optNonIncremental(true))
   )
 
   override protected def optionsString(options: Options): String = {
     "solver=" + options.findOptionOrDefault(optSelectedSolvers).head +
-    (if (options.findOptionOrDefault(optAssumeChecked)) " assumechecked" else "")
+    (if (options.findOptionOrDefault(optAssumeChecked)) " assumechecked" else "") +
+    (if (options.findOptionOrDefault(optNonIncremental)) " --no-incremental" else "")
   }
 
   private def ignoreSAT(ctx: Context, file: java.io.File): FilterStatus = 

src/main/scala/inox/Main.scala

@@ -11,6 +11,7 @@ trait MainHelpers {
   protected def getDebugSections: Set[DebugSection] = Set(
     utils.DebugSectionTimers,
     solvers.DebugSectionSolver,
+    solvers.smtlib.DebugSectionSMT,
     tip.DebugSectionTip
   )
 
@@ -45,6 +46,7 @@ trait MainHelpers {
   protected def getOptions: Map[OptionDef[_], Description] = Map(
     optHelp -> Description(General, "Show help message"),
     optNoColors -> Description(General, "Disable colored output and non-ascii characters (enable this option for better support in IDEs)"),
+    optNonIncremental -> Description(General, "Disable incremental mode in solvers"),
     optTimeout -> Description(General, "Set a timeout for the solver (in sec.)"),
     optSelectedSolvers -> Description(General, {
       "Use solvers s1,s2,...\nAvailable: " +

src/main/scala/inox/Options.scala

@@ -232,3 +232,5 @@ object optSelectedSolvers extends SetOptionDef[String] {
 }
 
 object optNoColors extends inox.FlagOptionDef("no-colors", false)
+
+object optNonIncremental extends inox.FlagOptionDef("no-incremental", false)

src/main/scala/inox/solvers/SolverFactory.scala

@@ -97,8 +97,40 @@ object SolverFactory {
                     val targetProgram: Program { val trees: inox.trees.type }
                   })(implicit sem: p.Semantics): SolverFactory { val program: p.type; type S <: TimeoutSolver { val program: p.type } } = {
 
+    val nonIncremental = ctx.options.findOptionOrDefault(optNonIncremental)
+    def nonIncrementalWrap[T, M](targetProgram: Program)(
+      nme: String,
+      targetSem: targetProgram.Semantics,
+      underlyingSolver: () => AbstractSolver {
+        val program: targetProgram.type
+        type Trees = T
+        type Model = M
+    }):
+      AbstractSolver {
+        val program: targetProgram.type
+        type Trees = T
+        type Model = M
+      } = {
+
+      if (nonIncremental) {
+        new {
+          val program: targetProgram.type = targetProgram
+          val context = ctx
+        } with NonIncrementalSolver {
+          type Trees = T
+          type Model = M
+          val semantics: targetProgram.Semantics = targetSem
+          def name = s"no-inc:$nme"
+
+          def underlying() = underlyingSolver()
+        }
+      } else {
+        underlyingSolver()
+      }
+    }
+
     val finalName = if (force) {
-      name 
+      name
     } else {
       fallbacks.get(name) match {
         case Some((guard, names, requirement)) if !guard() =>
@@ -129,6 +161,15 @@ object SolverFactory {
       }
     }
 
+    if (
+      nonIncremental &&
+      finalName != "smt-cvc4" &&
+      finalName != "unrollz3" &&
+      finalName != "smt-z3" &&
+      !finalName.startsWith("smt-z3:")
+    )
+      throw FatalError(s"Option --no-incremental is not compatible with solver $finalName")
+
     finalName match {
       case "nativez3" => create(p)(finalName, {
         val chooseEnc = ChooseEncoder(p)(enc)
@@ -195,12 +236,12 @@ object SolverFactory {
           override protected lazy val targetProgram: targetProg.type = targetProg
           override protected val targetSemantics = targetSem
 
-          protected val underlying = new {
+          protected val underlying = nonIncrementalWrap(progEnc.targetProgram)(finalName, targetSem, () => new {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
           } with z3.UninterpretedZ3Solver {
             val semantics: program.Semantics = targetSem
-          }
+          })
         }
       })
 
@@ -256,13 +297,13 @@ object SolverFactory {
           override protected lazy val targetProgram: targetProg.type = targetProg
           override protected val targetSemantics = targetSem
 
-          protected val underlying = new {
+          protected val underlying = nonIncrementalWrap(progEnc.targetProgram)(finalName, targetSem, () => new {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
           } with smtlib.Z3Solver {
             val semantics: program.Semantics = targetSem
             override def targetName = executableName
-          }
+          })
         }
       })
 
@@ -288,12 +329,12 @@ object SolverFactory {
           override protected lazy val targetProgram: targetProg.type = targetProg
           override protected val targetSemantics = targetSem
 
-          protected val underlying = new {
+          protected val underlying = nonIncrementalWrap(progEnc.targetProgram)(finalName, targetSem, () => new {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
           } with smtlib.CVC4Solver {
             val semantics: program.Semantics = targetSem
-          }
+          })
         }
       })
 

src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala

@@ -0,0 +1,49 @@
+/* Copyright 2009-2018 EPFL, Lausanne */
+
+package inox
+package solvers
+package combinators
+
+import utils._
+import scala.concurrent.duration._
+import scala.collection.mutable.ArrayBuffer
+
+trait NonIncrementalSolver extends AbstractSolver { self =>
+  import program.trees._
+  import SolverResponses._
+
+  protected def underlying(): AbstractSolver {
+    val program: self.program.type
+    type Trees = self.Trees
+    type Model = self.Model
+  }
+
+  val assertions: IncrementalSet[Trees] = new IncrementalSet[Trees]
+
+  val allSolvers: ArrayBuffer[AbstractSolver] = ArrayBuffer()
+
+  def assertCnstr(expression: Trees): Unit = assertions += expression
+  def reset(): Unit = assertions.clear()
+  def free(): Unit = for (solver <- allSolvers) solver.free()
+  def interrupt(): Unit = for (solver <- allSolvers) solver.interrupt()
+
+  override def check(config: CheckConfiguration): config.Response[Model, Assumptions] = {
+    val newSolver = underlying()
+    allSolvers.append(newSolver)
+    for (expression <- assertions)
+      newSolver.assertCnstr(expression)
+    newSolver.check(config)
+  }
+
+  override def checkAssumptions(config: Configuration)
+                               (assumptions: Set[Trees]): config.Response[Model, Assumptions] = {
+    val newSolver = underlying()
+    allSolvers.append(newSolver)
+    for (expression <- assertions)
+      newSolver.assertCnstr(expression)
+    newSolver.checkAssumptions(config)(assumptions)
+  }
+
+  def push(): Unit = assertions.push()
+  def pop(): Unit = assertions.pop()
+}

src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala

@@ -7,6 +7,8 @@ package smtlib
 import utils._
 import _root_.smtlib.trees.Terms._
 
+case object DebugSectionSMT extends DebugSection("smt")
+
 trait SMTLIBDebugger extends SMTLIBTarget {
   import context._
   import program._
@@ -22,6 +24,7 @@ trait SMTLIBDebugger extends SMTLIBTarget {
 
   /* Printing VCs */
   protected lazy val debugOut: Option[java.io.FileWriter] = {
+    implicit val debugSection = DebugSectionSMT
     if (reporter.isDebugEnabled) {
       val file = options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
       val n = DebugFileNumbers.next(targetName + file)