Remove --no-incremental option and enable no-inc: prefix on solvers

Author: jad-hamza

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

@@ -10,17 +10,16 @@ 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("smt-z3")),   optCheckModels(true), optNonIncremental(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 = {
     "solver=" + options.findOptionOrDefault(optSelectedSolvers).head +
-    (if (options.findOptionOrDefault(optAssumeChecked)) " assumechecked" else "") +
-    (if (options.findOptionOrDefault(optNonIncremental)) " --no-incremental" else "")
+    (if (options.findOptionOrDefault(optAssumeChecked)) " assumechecked" else "")
   }
 
   private def ignoreSAT(ctx: Context, file: java.io.File): FilterStatus = 

src/main/scala/inox/Main.scala

@@ -46,13 +46,13 @@ 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: " +
       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>, smt-cvc4, with 'noinc:' to use them in non-incremental mode"
     }),
     optDebug -> Description(General, {
       val sects = debugSections.toSeq.map(_.name).sorted

src/main/scala/inox/Options.scala

@@ -232,5 +232,3 @@ 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

@@ -90,44 +90,24 @@ object SolverFactory {
   // extract <exec> in "smt-z3:<exec>"
   private def getZ3Executable(name: String): String = name.drop(7)
 
-  def getFromName(name: String, force: Boolean = false)
+  def getFromName(noIncName: 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 = 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"
+    val nonIncremental = noIncName.startsWith("no-inc:")
+    val name = if (nonIncremental) noIncName.drop(7) else noIncName
 
-          def underlying() = underlyingSolver()
-        }
-      } else {
-        underlyingSolver()
-      }
-    }
+    if (
+      nonIncremental &&
+      name != "smt-cvc4" &&
+      name != "unrollz3" &&
+      name != "smt-z3" &&
+      !name.startsWith("smt-z3:")
+    )
+      throw FatalError(s"Non incremental mode is not available for solver $name")
 
     val finalName = if (force) {
       name
@@ -161,14 +141,36 @@ 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")
+    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, {
@@ -365,7 +367,9 @@ object SolverFactory {
     }
   }
 
-  def supportedSolver(s: String) = solverNames.contains(s) || s.startsWith("smt-z3:")
+  private def supportedSolverRaw(s: String) = solverNames.contains(s) || s.startsWith("smt-z3:")
+  def supportedSolver(s: String) =
+    supportedSolverRaw(s) || (s.startsWith("no-inc:") && supportedSolverRaw(s.drop(7)))
 
   def getFromSettings(p: Program, ctx: Context)
                      (enc: ProgramTransformer {