Add support for smt-z3 with custom executable name

Author: jad-hamza

src/main/scala/inox/Options.scala

@@ -223,7 +223,10 @@ 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(name =>
+      solvers.SolverFactory.solverNames.contains(name) ||
+      name.startsWith("smt-z3:")
+    )
   }
 
   val usageRhs = "s1,s2,..."

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

@@ -71,6 +71,7 @@ object SolverFactory {
     "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"
   )
 
@@ -109,6 +110,7 @@ object SolverFactory {
           replacement
 
         case Some(_) => name
+        case None if name.startsWith("smt-z3:") => name
 
         case _ => throw FatalError("Unknown solver: " + name)
       }
@@ -189,13 +191,14 @@ object SolverFactory {
         }
       })
 
-      case "smt-z3" => create(p)(finalName, {
+      case _ if 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 finalName.drop(7)
 
         () => new {
           val program: p.type = p
@@ -215,6 +218,7 @@ object SolverFactory {
             val context = ctx
           } with smtlib.Z3Solver {
             val semantics: program.Semantics = targetSem
+            override def targetName = executableName
           }
         }
       })

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))
     }
   }