From 15e9de097c0dd2387ad11f8815a724b78b2ed791 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 9 Aug 2016 11:13:58 +0200
Subject: [PATCH] SolverFactory from name, better options
---
src/main/scala/inox/InoxContext.scala | 14 +---
src/main/scala/inox/InoxOptions.scala | 22 +++--
.../scala/inox/evaluators/Evaluator.scala | 11 +--
.../inox/evaluators/RecursiveEvaluator.scala | 9 +--
.../inox/evaluators/SolvingEvaluator.scala | 2 +-
src/main/scala/inox/solvers/Solver.scala | 17 ++--
.../scala/inox/solvers/SolverFactory.scala | 81 +++++++++++++++++--
.../combinators/PortfolioSolverFactory.scala | 27 ++++---
.../inox/solvers/smtlib/CVC4Solver.scala | 10 +--
.../scala/inox/solvers/smtlib/Z3Solver.scala | 4 +-
.../scala/inox/solvers/theories/package.scala | 20 +++++
.../solvers/unrolling/UnrollingSolver.scala | 33 +++++---
.../inox/solvers/z3/NativeZ3Solver.scala | 2 +
.../solvers/z3/UninterpretedZ3Solver.scala | 5 ++
14 files changed, 169 insertions(+), 88 deletions(-)
create mode 100644 src/main/scala/inox/solvers/theories/package.scala
diff --git a/src/main/scala/inox/InoxContext.scala b/src/main/scala/inox/InoxContext.scala
index 1c3554235..42086b486 100644
--- a/src/main/scala/inox/InoxContext.scala
+++ b/src/main/scala/inox/InoxContext.scala
@@ -11,16 +11,8 @@ import inox.utils._
case class InoxContext(
reporter: Reporter,
interruptManager: InterruptManager,
- options: Seq[InoxOption[Any]] = Seq(),
- timers: TimerStorage = new TimerStorage) extends InoxOptions[InoxContext] {
-
- def build(opts: Seq[InoxOption[Any]]) = InoxContext(reporter, interruptManager, opts, timers)
-
- def toSolver: solvers.SolverOptions = solvers.SolverOptions(
- options.filter(opt => solvers.SolverOptions.options.exists(_ == opt.optionDef)))
- def toEvaluator: evaluators.EvaluatorOptions = evaluators.EvaluatorOptions(
- options.filter(opt => evaluators.EvaluatorOptions.options.exists(_ == opt.optionDef)))
-}
+ options: InoxOptions = InoxOptions(Seq()),
+ timers: TimerStorage = new TimerStorage)
object InoxContext {
def empty = {
@@ -33,7 +25,7 @@ object InoxContext {
InoxContext(
reporter,
new InterruptManager(reporter),
- options = Seq(InoxOption[Set[DebugSection]](InoxOptions.optDebug)(Set(ast.DebugSectionTrees)))
+ options = InoxOptions.empty + InoxOption[Set[DebugSection]](InoxOptions.optDebug)(Set(ast.DebugSectionTrees))
)
}
}
diff --git a/src/main/scala/inox/InoxOptions.scala b/src/main/scala/inox/InoxOptions.scala
index 151a60ba9..8ccdfec4f 100644
--- a/src/main/scala/inox/InoxOptions.scala
+++ b/src/main/scala/inox/InoxOptions.scala
@@ -154,10 +154,7 @@ object OptionsHelpers {
}
}
-trait InoxOptions[Self <: InoxOptions[Self]] {
- val options: Seq[InoxOption[Any]]
-
- protected def build(newOpts: Seq[InoxOption[Any]]): Self
+case class InoxOptions(options: Seq[InoxOption[Any]]) {
def findOption[A: ClassTag](optDef: InoxOptionDef[A]): Option[A] = options.collectFirst {
case InoxOption(`optDef`, value: A) => value
@@ -165,30 +162,31 @@ trait InoxOptions[Self <: InoxOptions[Self]] {
def findOptionOrDefault[A: ClassTag](optDef: InoxOptionDef[A]): A = findOption(optDef).getOrElse(optDef.default)
- def +(newOpt: InoxOption[Any]): Self = build {
+ def +(newOpt: InoxOption[Any]): InoxOptions = InoxOptions(
options.filter(_.optionDef != newOpt.optionDef) :+ newOpt
- }
+ )
- def ++(newOpts: Seq[InoxOption[Any]]): Self = build {
+ def ++(newOpts: Seq[InoxOption[Any]]): InoxOptions = InoxOptions {
val defs = newOpts.map(_.optionDef).toSet
options.filter(opt => !defs(opt.optionDef)) ++ newOpts
}
@inline
- def ++(that: Self): Self = this ++ that.options
+ def ++(that: InoxOptions): InoxOptions = this ++ that.options
}
object InoxOptions {
- /*
+ def empty: InoxOptions = InoxOptions(Seq())
+
val optSelectedSolvers = new InoxOptionDef[Set[String]] {
val name = "solvers"
- val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
- val default = Set("fairz3")
+ val description = "Use solvers s1, s2,...\n" +
+ solvers.SolverFactory.solversPretty
+ val default = Set("nativez3")
val parser = setParser(stringParser)
val usageRhs = "s1,s2,..."
}
- */
val optDebug = new InoxOptionDef[Set[DebugSection]] {
import OptionParsers._
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index af3fc771f..eea69bb55 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -3,23 +3,18 @@
package inox
package evaluators
-case class EvaluatorOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[EvaluatorOptions] {
- protected def build(opts: Seq[InoxOption[Any]]): EvaluatorOptions = EvaluatorOptions(opts)
-}
-
object EvaluatorOptions {
- def empty = EvaluatorOptions(Seq())
-
val options = Seq(
optIgnoreContracts
)
}
-object optIgnoreContracts extends InoxFlagOptionDef("ignorecontracts", "Don't fail on invalid contracts during evaluation", false)
+object optIgnoreContracts extends InoxFlagOptionDef(
+ "ignorecontracts", "Don't fail on invalid contracts during evaluation", false)
trait Evaluator {
val program: Program
- val options: EvaluatorOptions
+ val options: InoxOptions
import program.trees._
/** The type of value that this [[Evaluator]] calculates
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 745b7e1e7..715a8d8dd 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -533,16 +533,15 @@ trait RecursiveEvaluator
}
object RecursiveEvaluator {
- def apply(p: InoxProgram)(evOpts: EvaluatorOptions, solverOpts: solvers.SolverOptions):
- RecursiveEvaluator { val program: p.type } = {
+ def apply(p: InoxProgram, opts: InoxOptions): RecursiveEvaluator { val program: p.type } = {
new {
val program: p.type = p
} with RecursiveEvaluator with HasDefaultGlobalContext with HasDefaultRecContext {
- val options = p.ctx.toEvaluator ++ evOpts
+ val options = opts
val maxSteps = 50000
- def getSolver(opts: InoxOption[Any]*) = solvers.SolverFactory(p)(p.ctx.toSolver ++ opts, options)
+ def getSolver(moreOpts: InoxOption[Any]*) = solvers.SolverFactory(p, opts ++ moreOpts)
}
}
- def default(p: InoxProgram) = apply(p)(EvaluatorOptions.empty, solvers.SolverOptions.empty)
+ def default(p: InoxProgram) = apply(p, p.ctx.options)
}
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index cbe03bda1..9b17eae6b 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -29,7 +29,7 @@ trait SolvingEvaluator extends Evaluator {
val timer = ctx.timers.evaluators.specs.start()
val sf = getSolver(options.options.collect {
- case o@InoxOption(opt, _) if opt == optForallCache => o
+ case o @ InoxOption(opt, _) if opt == optForallCache => o
} : _*)
import SolverResponses._
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index b6874bea6..03dffbcac 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -5,13 +5,7 @@ package solvers
import utils._
-case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[SolverOptions] {
- def build(opts: Seq[InoxOption[Any]]): SolverOptions = SolverOptions(opts)
-}
-
object SolverOptions {
- def empty = SolverOptions(Seq())
-
val options = Seq(
optCheckModels,
optSilentErrors,
@@ -22,15 +16,18 @@ object SolverOptions {
)
}
-case object DebugSectionSolver extends DebugSection("solver")
+object optCheckModels extends InoxFlagOptionDef(
+ "checkmodels", "Double-check counter-examples with evaluator", false)
+
+object optSilentErrors extends InoxFlagOptionDef(
+ "silenterrors", "Fail silently into UNKNOWN when encountering an error", false)
-object optCheckModels extends InoxFlagOptionDef("checkmodels", "Double-check counter-examples with evaluator", false)
-object optSilentErrors extends InoxFlagOptionDef("silenterrors", "Fail silently into UNKNOWN when encountering an error", false)
+case object DebugSectionSolver extends DebugSection("solver")
trait AbstractSolver extends Interruptible {
def name: String
val program: Program
- val options: SolverOptions
+ val options: InoxOptions
import program._
import program.trees._
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index d15218683..392898a05 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -3,8 +3,6 @@
package inox
package solvers
-import scala.reflect.runtime.universe._
-
trait SolverFactory {
val program: Program
@@ -22,7 +20,7 @@ trait SolverFactory {
}
object SolverFactory {
- def create[S1 <: Solver : TypeTag](p: Program)(nme: String, builder: () => S1 { val program: p.type }):
+ def create[S1 <: Solver](p: Program)(nme: String, builder: () => S1 { val program: p.type }):
SolverFactory { val program: p.type; type S = S1 { val program: p.type } } = {
new SolverFactory {
val program: p.type = p
@@ -33,10 +31,79 @@ object SolverFactory {
}
}
- def apply(p: InoxProgram)
- (solverOpts: SolverOptions, evOpts: evaluators.EvaluatorOptions):
- SolverFactory { val program: p.type } = ???
+ import evaluators._
+ import combinators._
+
+ private val solverNames = Map(
+ "nativez3" -> "Native Z3 with z3-templates for unrolling (default)",
+ "unrollz3" -> "Native Z3 with leon-templates for unrolling",
+ "smt-cvc4" -> "CVC4 through SMT-LIB",
+ "smt-z3" -> "Z3 through SMT-LIB"
+ )
+
+ def getFromName(name: String)
+ (p: InoxProgram, opts: InoxOptions)
+ (ev: DeterministicEvaluator with SolvingEvaluator { val program: p.type }):
+ SolverFactory { val program: p.type; type S <: TimeoutSolver } = name match {
+ case "nativez3" => create(p)(name, () => new {
+ val program: p.type = p
+ val options = opts
+ } with z3.NativeZ3Solver with TimeoutSolver {
+ val evaluator = ev
+ })
+
+ case "unrollz3" => create(p)(name, () => new {
+ val program: p.type = p
+ val options = opts
+ } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
+ val evaluator = ev
+
+ object underlying extends {
+ val program: theories.targetProgram.type = theories.targetProgram
+ val options = opts
+ } with z3.UninterpretedZ3Solver
+ })
+
+ case "smt-cvc4" => create(p)(name, () => new {
+ val program: p.type = p
+ val options = opts
+ } with unrolling.UnrollingSolver with theories.CVC4Theories with TimeoutSolver {
+ val evaluator = ev
+
+ object underlying extends {
+ val program: theories.targetProgram.type = theories.targetProgram
+ val options = opts
+ } with smtlib.CVC4Solver
+ })
+
+ case "smt-z3" => create(p)(name, () => new {
+ val program: p.type = p
+ val options = opts
+ } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
+ val evaluator = ev
+
+ object underlying extends {
+ val program: theories.targetProgram.type = theories.targetProgram
+ val options = opts
+ } with smtlib.Z3Solver
+ })
+
+ case _ => throw FatalError("Unknown solver: " + name)
+ }
+
+ val solversPretty = "Available: " + solverNames.toSeq.sortBy(_._1).map {
+ case (name, desc) => f"\n $name%-14s : $desc"
+ }
+
+ def apply(p: InoxProgram, opts: InoxOptions): SolverFactory { val program: p.type; type S <: TimeoutSolver } =
+ p.ctx.options.findOptionOrDefault(InoxOptions.optSelectedSolvers).toSeq match {
+ case Seq() => throw FatalError("No selected solver")
+ case Seq(single) => getFromName(single)(p, opts)(RecursiveEvaluator(p, opts))
+ case multiple => PortfolioSolverFactory(p) {
+ multiple.map(name => getFromName(name)(p, opts)(RecursiveEvaluator(p, opts)))
+ }
+ }
def default(p: InoxProgram): SolverFactory { val program: p.type } =
- apply(p)(SolverOptions.empty, evaluators.EvaluatorOptions.empty)
+ apply(p, p.ctx.options)
}
diff --git a/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala
index f1f682975..dd62ddd6b 100644
--- a/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala
+++ b/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala
@@ -6,19 +6,16 @@ package combinators
trait PortfolioSolverFactory extends SolverFactory { self =>
- final type PT = program.type
- override type S = PortfolioSolver { val program: PT }
- final type SF = SolverFactory { val program: PT }
+ type S = PortfolioSolver with TimeoutSolver { val program: self.program.type }
+ type SF <: SolverFactory { val program: self.program.type }
val sfs: Seq[SF]
- def getNewSolver(): S = {
- new PortfolioSolver {
- val program: PT = self.program
- val solvers = sfs map (_.getNewSolver())
- val options: SolverOptions = solvers.head.options
- }
- }
+ def getNewSolver(): S = new {
+ val program: self.program.type = self.program
+ val solvers = sfs map (_.getNewSolver())
+ val options = solvers.head.options
+ } with PortfolioSolver with TimeoutSolver
// Assumes s is a P/Solver with the correct subsolver types
override def reclaim(s: S) = sfs.zip(s.solvers).foreach { case (sf, s) =>
@@ -28,3 +25,13 @@ trait PortfolioSolverFactory extends SolverFactory { self =>
val name = sfs.map(_.name).mkString("Pfolio(", ",", ")")
}
+object PortfolioSolverFactory {
+ def apply(p: InoxProgram)
+ (factories: Seq[SolverFactory { val program: p.type; type S <: TimeoutSolver }]):
+ PortfolioSolverFactory { val program: p.type; type S <: TimeoutSolver } = new {
+ val program: p.type = p
+ } with PortfolioSolverFactory {
+ type SF = SolverFactory { val program: p.type; type S <: TimeoutSolver }
+ val sfs: Seq[SF] = factories
+ }
+}
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
index 02306d219..e19fc66c8 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
@@ -6,13 +6,7 @@ package smtlib
import inox.OptionParsers._
-class CVC4Solver(val program: Program, val options: SolverOptions)
- extends SMTLIBSolver
- with CVC4Target {
-
- protected val userDefinedOps = {
- options.findOptionOrDefault(optCVC4Options)
- }
+trait CVC4Solver extends SMTLIBSolver with CVC4Target {
def interpreterOps(ctx: InoxContext) = {
Seq(
@@ -23,7 +17,7 @@ class CVC4Solver(val program: Program, val options: SolverOptions)
"--rewrite-divk",
"--print-success",
"--lang", "smt2.5"
- ) ++ userDefinedOps.toSeq
+ ) ++ options.findOptionOrDefault(optCVC4Options)
}
}
diff --git a/src/main/scala/inox/solvers/smtlib/Z3Solver.scala b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
index 64b5b127f..b8d50712b 100644
--- a/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
@@ -4,6 +4,4 @@ package inox
package solvers
package smtlib
-class Z3Solver(val program: Program, val options: SolverOptions)
- extends SMTLIBSolver
- with Z3Target
+trait Z3Solver extends SMTLIBSolver with Z3Target
diff --git a/src/main/scala/inox/solvers/theories/package.scala b/src/main/scala/inox/solvers/theories/package.scala
new file mode 100644
index 000000000..b2bd02c4b
--- /dev/null
+++ b/src/main/scala/inox/solvers/theories/package.scala
@@ -0,0 +1,20 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+
+package object theories {
+
+ trait Z3Theories { self: unrolling.AbstractUnrollingSolver =>
+ object theories extends {
+ val sourceProgram: self.program.type = self.program
+ } with StringEncoder
+ }
+
+ trait CVC4Theories { self: unrolling.AbstractUnrollingSolver =>
+ object theories extends {
+ val sourceProgram: self.program.type = self.program
+ } with BagEncoder
+ }
+}
+
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 9650c3903..1f89dc0cd 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -9,9 +9,14 @@ import utils._
import theories._
import evaluators._
-object optUnrollFactor extends InoxLongOptionDef("unrollfactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
-object optFeelingLucky extends InoxFlagOptionDef("feelinglucky", "Use evaluator to find counter-examples early", false)
-object optUnrollCores extends InoxFlagOptionDef("unrollcores", "Use unsat-cores to drive unfolding while remaining fair", false)
+object optUnrollFactor extends InoxLongOptionDef(
+ "unrollfactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
+
+object optFeelingLucky extends InoxFlagOptionDef(
+ "feelinglucky", "Use evaluator to find counter-examples early", false)
+
+object optUnrollCores extends InoxFlagOptionDef(
+ "unrollcores", "Use unsat-cores to drive unfolding while remaining fair", false)
trait AbstractUnrollingSolver
extends Solver {
@@ -41,11 +46,11 @@ trait AbstractUnrollingSolver
type Cores = Set[Encoded]
}
- lazy val unfoldFactor = options.findOptionOrDefault(optUnrollFactor)
- lazy val feelingLucky = options.findOptionOrDefault(optFeelingLucky)
- lazy val checkModels = options.findOptionOrDefault(optCheckModels)
- lazy val unrollUnsatCores = options.findOptionOrDefault(optUnrollCores)
- lazy val silentErrors = options.findOptionOrDefault(optSilentErrors)
+ lazy val checkModels = options.findOptionOrDefault(optCheckModels)
+ lazy val silentErrors = options.findOptionOrDefault(optSilentErrors)
+ lazy val unrollFactor = options.findOptionOrDefault(optUnrollFactor)
+ lazy val feelingLucky = options.findOptionOrDefault(optFeelingLucky)
+ lazy val unrollCores = options.findOptionOrDefault(optUnrollCores)
def check(config: Configuration): config.Response[Model, Cores] =
checkAssumptions(config)(Set.empty)
@@ -302,7 +307,7 @@ trait AbstractUnrollingSolver
val checkConfig = config
.min(Configuration(model = !templates.requiresFiniteRangeCheck, cores = true))
- .max(Configuration(model = false, cores = unrollUnsatCores))
+ .max(Configuration(model = false, cores = unrollCores))
val timer = ctx.timers.solvers.check.start()
val res: SolverResponse[underlying.Model, underlying.Cores] =
@@ -329,7 +334,7 @@ trait AbstractUnrollingSolver
case _: Unsatisfiable if !templates.canUnroll =>
CheckResult.cast(res)
- case UnsatWithCores(cores) if unrollUnsatCores =>
+ case UnsatWithCores(cores) if unrollCores =>
for (c <- cores) templates.extractNot(c) match {
case Some(b) => templates.promoteBlocker(b)
case None => reporter.fatalError("Unexpected blocker polarity for unsat core unrolling: " + c)
@@ -371,7 +376,9 @@ trait AbstractUnrollingSolver
}
case Validate(model) =>
- val valid = !checkModels || validateModel(model, assumptionsSeq, silenceErrors = silentErrors)
+ val valid: Boolean = !checkModels ||
+ validateModel(model, assumptionsSeq, silenceErrors = silentErrors)
+
if (valid) {
CheckResult(config cast SatWithModel(model))
} else {
@@ -436,8 +443,8 @@ trait AbstractUnrollingSolver
reporter.debug("- We need to keep going")
val timer = ctx.timers.solvers.unroll.start()
- // unfolling `unfoldFactor` times
- for (i <- 1 to unfoldFactor.toInt) {
+ // unfolling `unrollFactor` times
+ for (i <- 1 to unrollFactor.toInt) {
val newClauses = templates.unroll
for (ncl <- newClauses) {
underlying.assertCnstr(ncl)
diff --git a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
index ae3e08eed..a7ce7e3fb 100644
--- a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
@@ -72,6 +72,8 @@ trait NativeZ3Solver
underlying.reset()
}
+ def free(): Unit = underlying.free()
+
protected def declareVariable(v: Variable): Z3AST = underlying.declareVariable(v)
protected def wrapModel(model: Z3Model): super.ModelWrapper = ModelWrapper(model)
diff --git a/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
index 249f08ad7..8f10f1fb2 100644
--- a/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
@@ -49,6 +49,11 @@ trait UninterpretedZ3Solver
freeVars.reset()
}
+ def free(): Unit = underlying.free()
+
+ def interrupt(): Unit = underlying.interrupt()
+ def recoverInterrupt(): Unit = underlying.recoverInterrupt()
+
def assertCnstr(expression: Expr) {
freeVars ++= exprOps.variablesOf(expression)
underlying.assertCnstr(underlying.toZ3Formula(expression))
--
GitLab