From 86749646ffbef5cafa728935cb8c5214426849e9 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 5 May 2015 14:05:11 +0200
Subject: [PATCH] Fallback to SMT solver in case native interface is
unavailable
---
.../scala/leon/solvers/SolverFactory.scala | 36 +++++++++++++++++--
.../solvers/smtlib/SMTLIBCVC4Target.scala | 3 ++
.../leon/solvers/smtlib/SMTLIBTarget.scala | 27 +++++++++-----
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 1 +
.../scala/leon/synthesis/Synthesizer.scala | 2 +-
5 files changed, 57 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 2b838b68b..5dd87da9a 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/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
+ }
+ }
+
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index cfc0dee92..7f8d4c3e4 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/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)))
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index fcfe4c801..7d694d10d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/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()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 47088d817..1574e990b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/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)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 9dabc1233..40e6b8bbc 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/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)))
--
GitLab