Improvements for Z3 custom executables

Author: jad-hamza

src/main/scala/inox/Options.scala

@@ -223,10 +223,7 @@ object optSelectedSolvers extends SetOptionDef[String] {
   val name = "solvers"
   val default = Set("nativez3")
   val elementParser: OptionParser[String] = { s =>
-    stringParser(s).filter(name =>
-      solvers.SolverFactory.solverNames.contains(name) ||
-      name.startsWith("smt-z3:")
-    )
+    stringParser(s).filter(solvers.SolverFactory.supportedSolver)
   }
 
   val usageRhs = "s1,s2,..."

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

@@ -65,14 +65,14 @@ object SolverFactory {
   import unrolling._
 
   val solverNames = Map(
-    "nativez3"     -> "Native Z3 with z3-templates for unrolling",
-    "nativez3-opt" -> "Native Z3 optimizer with z3-templates for unrolling",
-    "unrollz3"     -> "Native Z3 with inox-templates for unrolling",
-    "smt-cvc4"     -> "CVC4 through SMT-LIB",
-    "smt-z3"       -> "Z3 through SMT-LIB",
-    "smt-z3-opt"   -> "Z3 optimizer through SMT-LIB",
-    "smt-z3:EXEC"  -> "Z3 through SMT-LIB with custom executable name",
-    "princess"     -> "Princess with inox unrolling"
+    "nativez3"      -> "Native Z3 with z3-templates for unrolling",
+    "nativez3-opt"  -> "Native Z3 optimizer with z3-templates for unrolling",
+    "unrollz3"      -> "Native Z3 with inox-templates for unrolling",
+    "smt-cvc4"      -> "CVC4 through SMT-LIB",
+    "smt-z3"        -> "Z3 through SMT-LIB",
+    "smt-z3-opt"    -> "Z3 optimizer through SMT-LIB",
+    "smt-z3:<exec>" -> "Z3 through SMT-LIB with custom executable name",
+    "princess"      -> "Princess with inox unrolling"
   )
 
   private val fallbacks = Map(
@@ -87,6 +87,9 @@ object SolverFactory {
 
   private var reported: Boolean = false
 
+  // extract <exec> in "smt-z3:<exec>"
+  private def getZ3Executable(name: String): String = name.drop(7)
+
   def getFromName(name: String, force: Boolean = false)
                  (p: Program, ctx: Context)
                  (enc: ProgramTransformer {
@@ -110,7 +113,17 @@ object SolverFactory {
           replacement
 
         case Some(_) => name
-        case None if name.startsWith("smt-z3:") => name
+        case None if name.startsWith("smt-z3:") =>
+          val z3Exec = getZ3Executable(name)
+          val hasZ3Exec = try {
+            new Z3Interpreter(z3Exec, Array("-in", "-smt2"))
+            true
+          } catch {
+            case _: java.io.IOException => false
+          }
+
+          if (hasZ3Exec) name
+          else throw FatalError("Unknown solver: " + z3Exec)
 
         case _ => throw FatalError("Unknown solver: " + name)
       }
@@ -228,7 +241,7 @@ object SolverFactory {
         val progEnc = fullEnc andThen theoryEnc
         val targetProg = progEnc.targetProgram
         val targetSem = targetProg.getSemantics
-        val executableName = if (finalName == "smt-z3") "z3" else finalName.drop(7)
+        val executableName = if (finalName == "smt-z3") "z3" else getZ3Executable(finalName)
 
         () => new {
           val program: p.type = p
@@ -311,7 +324,7 @@ object SolverFactory {
     }
   }
 
-  val solvers: Set[String] = solverNames.map(_._1).toSet
+  def supportedSolver(s: String) = solverNames.contains(s) || s.startsWith("smt-z3:")
 
   def getFromSettings(p: Program, ctx: Context)
                      (enc: ProgramTransformer {