Merge pull request #140 from jad-hamza/no-incremental

Add support for non-incremental mode

Author: samarion

build.sbt

@@ -37,13 +37,16 @@ resolvers ++= Seq(
 )
 
 libraryDependencies ++= Seq(
-  "org.scalatest" %% "scalatest" % "3.0.1" % "test;it",
+  "org.scalatest" %% "scalatest" % "3.2.7" % "test;it",
   "org.apache.commons" % "commons-lang3" % "3.4",
   "org.scala-lang" % "scala-reflect" % scalaVersion.value,
-  "com.regblanc" %% "scala-smtlib" % "0.2.2-7-g00a9686",
   "uuverifiers" %% "princess" % "2018-02-26"
 )
 
+def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
+// lazy val smtlib = RootProject(file("../scala-smtlib"))
+lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "5b9503e13d69c7116039a243025b2ce657c32c77")
+
 lazy val scriptName = settingKey[String]("Name of the generated 'inox' script")
 
 scriptName := "inox"
@@ -127,6 +130,8 @@ lazy val root = (project in file("."))
     parallelExecution := false
   )) : _*)
   .settings(compile := ((compile in Compile) dependsOn script dependsOn genDoc).value)
+  .dependsOn(smtlib)
+  
 
 publishMavenStyle := true
 

src/it/scala/inox/ResourceUtils.scala

@@ -2,7 +2,7 @@
 
 package inox
 
-import org.scalatest._
+import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.concurrent._
 
 import java.io.File

src/it/scala/inox/TestSuite.scala

@@ -2,12 +2,15 @@
 
 package inox
 
-import org.scalatest._
+import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.concurrent._
+import org.scalatest.matchers.should.Matchers
+import org.scalatest.Tag
+import org.scalatest.exceptions
 
 import utils._
 
-trait TestSuite extends FunSuite with Matchers with TimeLimits {
+trait TestSuite extends AnyFunSuite with Matchers with TimeLimits {
 
   protected def configurations: Seq[Seq[OptionValue[_]]] = Seq(Seq.empty)
 

src/it/scala/inox/tip/TipPrintingSuite.scala

@@ -3,9 +3,9 @@
 package inox
 package tip
 
-import org.scalatest._
+import org.scalatest.funsuite.AnyFunSuite
 
-class TipPrintingSuite extends FunSuite with ResourceUtils {
+class TipPrintingSuite extends AnyFunSuite with ResourceUtils {
   import inox.trees._
 
   val ctx = TestContext.empty

src/it/scala/inox/tip/TipSerializationSuite.scala

@@ -3,9 +3,9 @@
 package inox
 package tip
 
-import org.scalatest._
+import org.scalatest.funspec.AnyFunSpec
 
-class TipSerializationSuite extends FunSpec with ResourceUtils {
+class TipSerializationSuite extends AnyFunSpec with ResourceUtils {
   import inox.trees._
 
   val ctx = TestContext.empty

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

@@ -10,10 +10,11 @@ import scala.language.existentials
 class TipTestSuite extends TestSuite with ResourceUtils {
 
   override def configurations = Seq(
-    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("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("no-inc:smt-z3")), optCheckModels(true))
   )
 
   override protected def optionsString(options: Options): String = {

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
   )
 
@@ -50,7 +51,8 @@ trait MainHelpers {
       "Use solvers s1,s2,...\nAvailable: " +
       solvers.SolverFactory.solverNames.toSeq.sortBy(_._1).map {
         case (name, desc) => f"\n  $name%-14s : $desc"
-      }.mkString("")
+      }.mkString("") +
+      "\nYou can prefix the solvers unrollz3, smt-z3, smt-z3:<exec> and smt-cvc4, with 'no-inc:' to use them in non-incremental mode"
     }),
     optDebug -> Description(General, {
       val sects = debugSections.toSeq.map(_.name).sorted

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

@@ -90,17 +90,32 @@ object SolverFactory {
   // extract <exec> in "smt-z3:<exec>"
   private def getZ3Executable(name: String): String = name.drop(7)
 
+  // extract solver in "no-inc:solver"
+  private def removeNoInc(name: String): String = name.drop(7)
+
   def getFromName(name: String, force: Boolean = false)
                  (p: Program, ctx: Context)
                  (enc: ProgramTransformer {
                     val sourceProgram: p.type
                     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 = name.startsWith("no-inc:")
+    val noPrefixName = if (nonIncremental) removeNoInc(name) else name
+
+    if (
+      nonIncremental &&
+      noPrefixName != "smt-cvc4" &&
+      noPrefixName != "unrollz3" &&
+      noPrefixName != "smt-z3" &&
+      !noPrefixName.startsWith("smt-z3:")
+    )
+      throw FatalError(s"Non incremental mode is not available for solver $name")
+
     val finalName = if (force) {
-      name 
+      noPrefixName
     } else {
-      fallbacks.get(name) match {
+      fallbacks.get(noPrefixName) match {
         case Some((guard, names, requirement)) if !guard() =>
           val replacement = names.collectFirst {
             case name if fallbacks(name)._1() => name
@@ -112,23 +127,54 @@ object SolverFactory {
           }
           replacement
 
-        case Some(_) => name
-        case None if name.startsWith("smt-z3:") =>
-          val z3Exec = getZ3Executable(name)
+        case Some(_) => noPrefixName
+        case None if noPrefixName.startsWith("smt-z3:") =>
+          val z3Exec = getZ3Executable(noPrefixName)
           val hasZ3Exec = try {
             new Z3Interpreter(z3Exec, Array("-in", "-smt2"))
             true
           } catch {
             case _: java.io.IOException => false
           }
 
-          if (hasZ3Exec) name
+          if (hasZ3Exec) noPrefixName
           else throw FatalError("Unknown solver: " + z3Exec)
 
-        case _ => throw FatalError("Unknown solver: " + name)
+        case _ => throw FatalError("Unknown solver: " + noPrefixName)
+      }
+    }
+
+    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()
       }
     }
 
+
     finalName match {
       case "nativez3" => create(p)(finalName, {
         val chooseEnc = ChooseEncoder(p)(enc)
@@ -195,12 +241,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 +302,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 +334,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
-          }
+          })
         }
       })
 
@@ -324,7 +370,13 @@ object SolverFactory {
     }
   }
 
-  def supportedSolver(s: String) = solverNames.contains(s) || s.startsWith("smt-z3:")
+  def supportedSolver(s: String) =
+    solverNames.contains(s) ||
+    s.startsWith("smt-z3:") ||
+    s.startsWith("no-inc:smt-z3:") ||
+    s == "no-inc:smt-z3" ||
+    s == "no-inc:smt-cvc4" ||
+    s == "no-inc:unrollz3"
 
   def getFromSettings(p: Program, ctx: Context)
                      (enc: ProgramTransformer {

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

@@ -0,0 +1,65 @@
+/* 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: IncrementalSeq[Trees] = new IncrementalSeq[Trees]
+
+  var currentSolver: Option[AbstractSolver] = None
+
+  def assertCnstr(expression: Trees): Unit = assertions += expression
+  def reset(): Unit = assertions.clear()
+  def free(): Unit = for (solver <- currentSolver) solver.free()
+  def interrupt(): Unit = for (solver <- currentSolver) solver.interrupt()
+
+  override def check(config: CheckConfiguration): config.Response[Model, Assumptions] = {
+    assert(currentSolver.isEmpty,
+      "`currentSolver` should be empty when invoking `check` in NonIncrementalSolver")
+    val newSolver = underlying()
+    try {
+      currentSolver = Some(newSolver)
+      for (expression <- assertions)
+        newSolver.assertCnstr(expression)
+      val res = newSolver.check(config)
+      currentSolver = None
+      res
+    } finally {
+      newSolver.free()
+    }
+  }
+
+  override def checkAssumptions(config: Configuration)
+                               (assumptions: Set[Trees]): config.Response[Model, Assumptions] = {
+    assert(currentSolver.isEmpty,
+      "`currentSolver` should be empty when invoking `checkAssumptions` in NonIncrementalSolver")
+    val newSolver = underlying()
+    try {
+      currentSolver = Some(newSolver)
+      for (expression <- assertions)
+        newSolver.assertCnstr(expression)
+      val res = newSolver.checkAssumptions(config)(assumptions)
+      currentSolver = None
+      res
+    } finally {
+      newSolver.free()
+    }
+  }
+
+  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)