Fallback to SMT solver in case native interface is unavailable

src/main/scala/leon/solvers/SolverFactory.scala

@@ -40,10 +40,20 @@ object SolverFactory {
     }.mkString("")
 
   def getFromSettings(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
-    getFromName(ctx, program)(ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers).toSeq : _*)
+    val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
+
+    if (((names contains "fairz3") || (names contains "unrollz3")) && !hasNativeZ3) {
+      if (!reported) {
+        ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-based solver.")
+        reported = true
+      }
+      getFromName(ctx, program)("smt-z3")
+    } else {
+      getFromName(ctx, program)(names.toSeq : _*)
+    }
   }
 
-  def getFromName(ctx: LeonContext, program: Program)(names: String*): SolverFactory[TimeoutSolver] = {
+  private def getFromName(ctx: LeonContext, program: Program)(names: String*): SolverFactory[TimeoutSolver] = {
 
     def getSolver(name: String): SolverFactory[TimeoutSolver] = name match {
       case "fairz3" =>
@@ -95,9 +105,19 @@ object SolverFactory {
 
   // Solver qualifiers that get used internally:
 
+  private var reported = false
+
   // Fast solver used by simplifiactions, to discharge simple tautologies
   def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
-    SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBZ3Target with TimeoutSolver)
+    if (hasNativeZ3) {
+      SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
+    } else {
+      if (!reported) {
+        ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-based solver.")
+        reported = true
+      }
+      SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBZ3Target with TimeoutSolver)
+    }
   }
 
   // Full featured solver used by default
@@ -105,4 +125,14 @@ object SolverFactory {
     getFromName(ctx, program)("fairz3")
   }
 
+  lazy val hasNativeZ3 = {
+    try {
+      new _root_.z3.scala.Z3Config
+      true
+    } catch {
+      case _: java.lang.UnsatisfiedLinkError =>
+        false
+    }
+  }
+
 }

src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala

@@ -144,9 +144,12 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
       }
 
       m
+
     /**
      * ===== Set operations =====
      */
+
+
     case fs @ FiniteSet(elems) =>
       if (elems.isEmpty) {
         QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset")), Some(declareSort(fs.getType)))

src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala

@@ -57,12 +57,13 @@ trait SMTLIBTarget {
   def id2sym(id: Identifier): SSymbol = SSymbol(id.name+"!"+id.globalId)
 
   // metadata for CC, and variables
-  val constructors = new IncrementalBijection[TypeTree, SSymbol]()
-  val selectors    = new IncrementalBijection[(TypeTree, Int), SSymbol]()
-  val testers      = new IncrementalBijection[TypeTree, SSymbol]()
-  val variables    = new IncrementalBijection[Identifier, SSymbol]()
-  val sorts        = new IncrementalBijection[TypeTree, Sort]()
-  val functions    = new IncrementalBijection[TypedFunDef, SSymbol]()
+  val constructors  = new IncrementalBijection[TypeTree, SSymbol]()
+  val selectors     = new IncrementalBijection[(TypeTree, Int), SSymbol]()
+  val testers       = new IncrementalBijection[TypeTree, SSymbol]()
+  val variables     = new IncrementalBijection[Identifier, SSymbol]()
+  val genericValues = new IncrementalBijection[GenericValue, SSymbol]()
+  val sorts         = new IncrementalBijection[TypeTree, Sort]()
+  val functions     = new IncrementalBijection[TypedFunDef, SSymbol]()
 
   protected object OptionManager {
     lazy val leonOption = program.library.Option.get
@@ -151,7 +152,8 @@ trait SMTLIBTarget {
 
   def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
     case SetType(base) =>
-      require(r.default == BooleanLiteral(false) && r.keyTpe == base)
+      require(r.default == BooleanLiteral(false), "Co-finite sets are not supported.")
+      require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
 
       finiteSet(r.elems.keySet, base)
 
@@ -512,6 +514,12 @@ trait SMTLIBTarget {
       case m : MatchExpr =>
         toSMT(matchToIfThenElse(m))
 
+
+      case gv @ GenericValue(tpe, n) =>
+        genericValues.cachedB(gv) {
+          declareVariable(FreshIdentifier("gv"+n, tpe))
+        }
+
       /**
        * ===== Everything else =====
        */
@@ -582,7 +590,8 @@ trait SMTLIBTarget {
           case _ => reporter.fatalError("Unhandled nary "+e)
         }
 
-      case o => unsupported("Tree: " + o)
+      case o =>
+        unsupported("Tree: " + o)
     }
   }
 
@@ -731,6 +740,7 @@ trait SMTLIBTarget {
     selectors.push()
     testers.push()
     variables.push()
+    genericValues.push()
     sorts.push()
     functions.push()
 
@@ -744,6 +754,7 @@ trait SMTLIBTarget {
     selectors.pop()
     testers.pop()
     variables.pop()
+    genericValues.pop()
     sorts.pop()
     functions.pop()
 

src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala

@@ -41,6 +41,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
     sorts.cachedB(tpe) {
       tpe match {
         case SetType(base) =>
+          super.declareSort(BooleanType)
           declareSetSort(base)
         case _ =>
           super.declareSort(t)

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -73,7 +73,7 @@ class Synthesizer(val context : LeonContext,
 
     val (npr, fds) = solutionToProgram(sol)
 
-    val solverf = SolverFactory.getFromName(context, npr)("fairz3").withTimeout(timeout)
+    val solverf = SolverFactory.default(context, npr).withTimeout(timeout)
 
     val vctx = VerificationContext(context, npr, solverf, context.reporter)
     val vcs = generateVCs(vctx, Some(fds.map(_.id.name)))