Merge pull request #136 from jad-hamza/more-z3

Add support for smt-z3 with custom executable name

Author: samarion

src/main/scala/inox/Options.scala

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

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

@@ -65,13 +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",
-    "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(
@@ -86,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 {
@@ -109,6 +113,17 @@ object SolverFactory {
           replacement
 
         case Some(_) => 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)
       }
@@ -189,7 +204,7 @@ object SolverFactory {
         }
       })
 
-      case "smt-z3" => create(p)(finalName, {
+      case "smt-z3-opt" => create(p)(finalName, {
         val chooseEnc = ChooseEncoder(p)(enc)
         val fullEnc = enc andThen chooseEnc
         val theoryEnc = theories.Z3(fullEnc.targetProgram)
@@ -201,7 +216,7 @@ object SolverFactory {
           val program: p.type = p
           val context = ctx
           val encoder: enc.type = enc
-        } with UnrollingSolver with TimeoutSolver with tip.TipDebugger {
+        } with UnrollingOptimizer with TimeoutSolver {
           override protected val semantics = sem
           override protected val chooses: chooseEnc.type = chooseEnc
           override protected val theories: theoryEnc.type = theoryEnc
@@ -213,25 +228,26 @@ object SolverFactory {
           protected val underlying = new {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
-          } with smtlib.Z3Solver {
+          } with smtlib.optimization.Z3Optimizer {
             val semantics: program.Semantics = targetSem
           }
         }
       })
 
-      case "smt-z3-opt" => create(p)(finalName, {
+      case _ if finalName == "smt-z3" || finalName.startsWith("smt-z3:") => create(p)(finalName, {
         val chooseEnc = ChooseEncoder(p)(enc)
         val fullEnc = enc andThen chooseEnc
         val theoryEnc = theories.Z3(fullEnc.targetProgram)
         val progEnc = fullEnc andThen theoryEnc
         val targetProg = progEnc.targetProgram
         val targetSem = targetProg.getSemantics
+        val executableName = if (finalName == "smt-z3") "z3" else getZ3Executable(finalName)
 
         () => new {
           val program: p.type = p
           val context = ctx
           val encoder: enc.type = enc
-        } with UnrollingOptimizer with TimeoutSolver {
+        } with UnrollingSolver with TimeoutSolver with tip.TipDebugger {
           override protected val semantics = sem
           override protected val chooses: chooseEnc.type = chooseEnc
           override protected val theories: theoryEnc.type = theoryEnc
@@ -243,8 +259,9 @@ object SolverFactory {
           protected val underlying = new {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
-          } with smtlib.optimization.Z3Optimizer {
+          } with smtlib.Z3Solver {
             val semantics: program.Semantics = targetSem
+            override def targetName = executableName
           }
         }
       })
@@ -307,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 {

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

@@ -58,7 +58,7 @@ trait Z3Target extends SMTLIBTarget with SMTLIBDebugger {
   protected val interpreter = {
     val opts = interpreterOpts
     reporter.debug("Invoking solver "+targetName+" with "+opts.mkString(" "))
-    new Z3Interpreter("z3", opts.toArray) {
+    new Z3Interpreter(targetName, opts.toArray) {
       override lazy val parser: Z3Parser = new Z3Parser(new Lexer(out))
     }
   }