diff --git a/project/Build.scala b/project/Build.scala
index 284491fff92a1fb8348dd81874099ff4be7019fe..002494c53806c763a01bbf79fb20525622608b8c 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -80,6 +80,6 @@ object Leon extends Build {
def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = project("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
- lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "9f88509b13e7e64214c0b9b6a9124fc6c29e2084")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "24a8b85949c69189f37c5fdfab3265801a084ee8")
}
}
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index bec459b59568dff077061628db5a15f84b15b308..f481904558a7eba94e349814e6edd36de69770f9 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -45,6 +45,8 @@ sealed abstract class LeonOptionDef {
val name: String
val usageOption: String
val usageDesc: String
+
+ def usageDescs = usageDesc.split("\n").toList
}
case class LeonFlagOptionDef(name: String,
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 2a6c90dcb3873c87e2cd3026d04ed5874f7ea85d..daff9774815c2718a4d8c51256705f3ae69616c9 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -28,7 +28,8 @@ object Main {
// Add whatever you need here.
lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
- new solvers.z3.FairZ3Component{}
+ new solvers.z3.FairZ3Component{},
+ solvers.smtlib.SMTLIBCVC4Component
)
lazy val topLevelOptions : Set[LeonOptionDef] = Set(
@@ -37,7 +38,10 @@ object Main {
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
LeonFlagOptionDef ("watch", "--watch", "Rerun pipeline when file changes"),
- LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt-z3,smt-cvc4)"),
+ LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 \nAvailable:"+
+ SolverFactory.definedSolvers.toSeq.sortBy(_._1).map {
+ case (name, desc) => f"\n $name%-14s : $desc"
+ }.mkString("")),
LeonValueOptionDef("debug", "--debug=<sections..>", "Enables specific messages"),
LeonFlagOptionDef ("noop", "--noop", "No operation performed, just output program"),
LeonFlagOptionDef ("help", "--help", "Show help")
@@ -49,9 +53,13 @@ object Main {
reporter.info("usage: leon [--xlang] [--termination] [--synthesis] [--help] [--debug=<N>] [..] <files>")
reporter.info("")
for (opt <- topLevelOptions.toSeq.sortBy(_.name)) {
- reporter.info(f"${opt.usageOption}%-20s ${opt.usageDesc}")
+ val (uhead :: utail) = opt.usageDescs
+ reporter.info(f"${opt.usageOption}%-20s ${uhead}")
+ for(u <- utail) {
+ reporter.info(f"${""}%-20s ${u}")
+ }
+
}
- reporter.info("(By default, Leon verifies PureScala programs.)")
reporter.info("")
reporter.info("Additional options, by component:")
@@ -151,7 +159,7 @@ object Main {
case LeonFlagOption("xlang", value) =>
settings = settings.copy(xlang = value)
case LeonValueOption("solvers", ListValue(ss)) =>
- val available = SolverFactory.definedSolvers
+ val available = SolverFactory.definedSolvers.keySet
val unknown = ss.toSet -- available
if (unknown.nonEmpty) {
initReporter.error("Unknown solver(s): "+unknown.mkString(", ")+" (Available: "+available.mkString(", ")+")")
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index ec417d847b1a25d2d2a6835d4b679f4f83ecb0e5..19e2f20ea74552c5be641898e07bd26e7f672662 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -19,7 +19,16 @@ object SolverFactory {
}
}
- val definedSolvers = Set("fairz3", "unrollz3", "enum", "smt", "smt-z3", "smt-z3-quantified", "smt-cvc4", "smt-2.5-cvc4")
+ val definedSolvers = Map(
+ "fairz3" -> "Native Z3 with z3-templates for unfolding (default)",
+ "smt-cvc4" -> "CVC4 through SMT-LIB",
+ "smt-z3" -> "Z3 through SMT-LIB",
+ "smt-z3-q" -> "Z3 through SMT-LIB, with quantified encoding",
+ "smt-cvc4-proof" -> "CVC4 through SMT-LIB, in-solver inductive reasonning, for proofs only",
+ "smt-cvc4-cex" -> "CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only",
+ "unrollz3" -> "Native Z3 with leon-templates for unfolding",
+ "enum" -> "Enumeration-based counter-example-finder"
+ )
def getFromSettings[S](ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
import combinators._
@@ -36,17 +45,20 @@ object SolverFactory {
case "enum" =>
SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
- case "smt" | "smt-z3" =>
+ case "smt-z3" =>
SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBSolver(ctx, program) with SMTLIBZ3Target) with TimeoutSolver)
- case "smt-z3-quantified" =>
+ case "smt-z3-q" =>
SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBZ3QuantifiedTarget with TimeoutSolver)
case "smt-cvc4" =>
SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBSolver(ctx, program) with SMTLIBCVC4Target) with TimeoutSolver)
- case "smt-2.5-cvc4" =>
- SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBUnrollingCVC4Target with TimeoutSolver)
+ case "smt-cvc4-proof" =>
+ SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBCVC4ProofTarget with TimeoutSolver)
+
+ case "smt-cvc4-cex" =>
+ SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBCVC4CounterExampleTarget with TimeoutSolver)
case _ =>
ctx.reporter.fatalError("Unknown solver "+name)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
new file mode 100644
index 0000000000000000000000000000000000000000..62bd9307881ef29d22e0a3578eb3f8fe84b6aa67
--- /dev/null
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers.smtlib
+
+import purescala.Common.FreshIdentifier
+import purescala.Expressions.{FunctionInvocation, BooleanLiteral, Expr, Implies}
+import purescala.Definitions.TypedFunDef
+import purescala.Constructors.application
+import purescala.DefOps.typedTransitiveCallees
+import leon.purescala.ExprOps.matchToIfThenElse
+import smtlib.parser.Commands._
+import smtlib.parser.Terms._
+
+trait SMTLIBCVC4CounterExampleTarget extends SMTLIBCVC4QuantifiedTarget {
+ this: SMTLIBSolver =>
+
+ override def interpreterOps(ctx: LeonContext) = {
+ Seq(
+ "-q",
+ "--print-success",
+ "--lang", "smt",
+ "--fmf-fun"
+ ) ++ userDefinedOps(ctx)
+ }
+
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1df96a80d44be45e565f22e8bc8fd59b9fb0cd29
--- /dev/null
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala
@@ -0,0 +1,31 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers.smtlib
+
+import purescala.Common.FreshIdentifier
+import purescala.Expressions.{FunctionInvocation, BooleanLiteral, Expr, Implies}
+import purescala.Definitions.TypedFunDef
+import purescala.Constructors.application
+import purescala.DefOps.typedTransitiveCallees
+import leon.purescala.ExprOps.matchToIfThenElse
+import smtlib.parser.Commands._
+import smtlib.parser.Terms._
+
+trait SMTLIBCVC4ProofTarget extends SMTLIBCVC4QuantifiedTarget {
+ this: SMTLIBSolver =>
+
+ override def interpreterOps(ctx: LeonContext) = {
+ Seq(
+ "-q",
+ "--print-success",
+ "--lang", "smt",
+ "--quant-ind",
+ "--conjecture-gen",
+ "--conjecture-gen-per-round=3",
+ "--conjecture-gen-gt-enum=40",
+ "--full-saturate-quant"
+ ) ++ userDefinedOps(ctx)
+ }
+
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
similarity index 96%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index 4a72c468d49e30b992549e483e4ceb3d5aa11ef5..c792aed5542a98e25195e47503371cb6e159eb61 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -12,12 +12,11 @@ import leon.purescala.ExprOps.matchToIfThenElse
import smtlib.parser.Commands._
import smtlib.parser.Terms._
-trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
+trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target {
this: SMTLIBSolver =>
private val typedFunDefExplorationLimit = 10000
- override def targetName = "2.5-cvc4"
override def declareFunction(tfd: TypedFunDef): SSymbol = {
if (tfd.params.isEmpty) {
super[SMTLIBCVC4Target].declareFunction(tfd)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index fcca0aad1de214367a01117e25a09e718cbe4244..e1c8c1d2662d098cd1bedc1a017267b5edc92aaa 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -21,7 +21,29 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
def targetName = "cvc4"
- def getNewInterpreter() = CVC4Interpreter.buildDefault
+ def userDefinedOps(ctx: LeonContext) = {
+ ctx.options.collect {
+ case LeonValueOption("solver:cvc4", value) => value
+ }
+ }
+
+ def interpreterOps(ctx: LeonContext) = {
+ Seq(
+ "-q",
+ "--produce-models",
+ "--no-incremental",
+ "--tear-down-incremental",
+ "--dt-rewrite-error-sel",
+ "--print-success",
+ "--lang", "smt"
+ ) ++ userDefinedOps(ctx)
+ }
+
+ def getNewInterpreter(ctx: LeonContext) = {
+ val opts = interpreterOps(ctx)
+ reporter.debug("Invoking solver with "+opts.mkString(" "))
+ new CVC4Interpreter("cvc4", opts.toArray)
+ }
override def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
@@ -160,3 +182,13 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
super[SMTLIBTarget].toSMT(e)
}
}
+
+object SMTLIBCVC4Component extends LeonComponent {
+ val name = "cvc4 solver"
+
+ val description = "Solver invoked when --solvers=smt-cvc4"
+
+ override val definedOptions : Set[LeonOptionDef] = Set(
+ LeonValueOptionDef("solver:cvc4", "--solver:cvc4=<cvc4-opt>", "Pass extra arguments to CVC4")
+ )
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 8a38fd562998ef414ce1ec7743f98eeb61e3d4e4..fd687b77808ac57cc1decb6a889d6eb1b4393be1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -34,9 +34,12 @@ trait SMTLIBTarget {
val reporter = context.reporter
def targetName: String
- def getNewInterpreter(): SMTInterpreter
- val interpreter = getNewInterpreter()
+ def interpreterOps(ctx: LeonContext): Seq[String]
+
+ def getNewInterpreter(ctx: LeonContext): SMTInterpreter
+
+ val interpreter = getNewInterpreter(context)
var out: java.io.FileWriter = _
@@ -694,7 +697,7 @@ trait SMTLIBTarget {
case CheckSatStatus(SatStatus) => Some(true)
case CheckSatStatus(UnsatStatus) => Some(false)
case CheckSatStatus(UnknownStatus) => None
- case _ => None
+ case e => None
}
override def getModel: Map[Identifier, Expr] = {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 44caf7c3b25d14afcc2aa57c4c64d2bce008e4ba..47088d817dfda6dfc9fe5cb4ef9e99118fd222b7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -23,7 +23,14 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
def targetName = "z3"
- def getNewInterpreter() = Z3Interpreter.buildDefault
+ def interpreterOps(ctx: LeonContext) = {
+ Seq(
+ "-in",
+ "-smt2"
+ )
+ }
+
+ def getNewInterpreter(ctx: LeonContext) = new Z3Interpreter("z3", interpreterOps(ctx).toArray)
val extSym = SSymbol("_")