From d2303d96ddb8b4cc4d08be3c8dad4e43f60c31a0 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 20 Jul 2016 17:07:43 +0200
Subject: [PATCH] Compiles!! Wouhoouuuuu!!
---
src/main/scala/inox/InoxContext.scala | 12 +-
src/main/scala/inox/InoxOptions.scala | 27 +++-
src/main/scala/inox/ast/Definitions.scala | 37 ++++-
src/main/scala/inox/ast/ExprOps.scala | 11 +-
src/main/scala/inox/ast/Expressions.scala | 16 +-
src/main/scala/inox/ast/Extractors.scala | 2 +-
src/main/scala/inox/ast/Trees.scala | 2 +-
.../scala/inox/evaluators/Evaluator.scala | 3 +
.../evaluators/SolvingEvalInterface.scala | 37 -----
.../inox/evaluators/SolvingEvaluator.scala | 141 ++++++++----------
src/main/scala/inox/solvers/Solver.scala | 73 +++++++--
11 files changed, 197 insertions(+), 164 deletions(-)
delete mode 100644 src/main/scala/inox/evaluators/SolvingEvalInterface.scala
diff --git a/src/main/scala/inox/InoxContext.scala b/src/main/scala/inox/InoxContext.scala
index 5eda99d46..6abc7d3e1 100644
--- a/src/main/scala/inox/InoxContext.scala
+++ b/src/main/scala/inox/InoxContext.scala
@@ -4,8 +4,6 @@ package inox
import inox.utils._
-import scala.reflect.ClassTag
-
/** Everything that is part of a compilation unit, except the actual program tree.
* Contexts are immutable, and so should all their fields (with the possible
* exception of the reporter).
@@ -14,15 +12,7 @@ case class InoxContext(
reporter: Reporter,
interruptManager: InterruptManager,
options: Seq[InoxOption[Any]] = Seq(),
- timers: TimerStorage = new TimerStorage) {
-
- def findOption[A: ClassTag](optDef: InoxOptionDef[A]): Option[A] = options.collectFirst {
- case InoxOption(`optDef`, value:A) => value
- }
-
- def findOptionOrDefault[A: ClassTag](optDef: InoxOptionDef[A]): A =
- findOption(optDef).getOrElse(optDef.default)
-}
+ timers: TimerStorage = new TimerStorage) extends InoxOptions
object InoxContext {
def empty = {
diff --git a/src/main/scala/inox/InoxOptions.scala b/src/main/scala/inox/InoxOptions.scala
index c50fb8646..4ae72dcda 100644
--- a/src/main/scala/inox/InoxOptions.scala
+++ b/src/main/scala/inox/InoxOptions.scala
@@ -5,11 +5,12 @@ package inox
import OptionParsers._
import scala.util.Try
+import scala.reflect.ClassTag
abstract class InoxOptionDef[+A] {
val name: String
val description: String
- val default: A
+ def default: A
val parser: OptionParser[A]
val usageRhs: String
@@ -153,8 +154,19 @@ object OptionsHelpers {
}
}
+trait InoxOptions {
+ val options: Seq[InoxOption[Any]]
+
+ def findOption[A: ClassTag](optDef: InoxOptionDef[A]): Option[A] = options.collectFirst {
+ case InoxOption(`optDef`, value: A) => value
+ }
+
+ def findOptionOrDefault[A: ClassTag](optDef: InoxOptionDef[A]): A = findOption(optDef).getOrElse(optDef.default)
+}
+
object InoxOptions {
+ /*
val optSelectedSolvers = new InoxOptionDef[Set[String]] {
val name = "solvers"
val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
@@ -162,25 +174,32 @@ object InoxOptions {
val parser = setParser(stringParser)
val usageRhs = "s1,s2,..."
}
+ */
val optDebug = new InoxOptionDef[Set[DebugSection]] {
import OptionParsers._
val name = "debug"
val description = {
+ /*
val sects = DebugSections.all.toSeq.map(_.name).sorted
val (first, second) = sects.splitAt(sects.length/2 + 1)
- "Enable detailed messages per component.\nAvailable:\n" +
+ */
+ "Enable detailed messages per component." /* +
+ "\nAvailable:\n" +
" " + first.mkString(", ") + ",\n" +
- " " + second.mkString(", ")
+ " " + second.mkString(", ")*/
}
val default = Set[DebugSection]()
val usageRhs = "d1,d2,..."
private val debugParser: OptionParser[Set[DebugSection]] = s => {
+ /*
if (s == "all") {
Some(DebugSections.all)
} else {
DebugSections.all.find(_.name == s).map(Set(_))
- }
+ }*/
+ None
+
}
val parser: String => Option[Set[DebugSection]] = {
setParser[Set[DebugSection]](debugParser)(_).map(_.flatten)
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 87eaed93f..d7fab61ee 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -3,9 +3,10 @@
package inox
package ast
+import scala.reflect._
import scala.collection.mutable.{Map => MutableMap}
-trait Definitions { self0: Trees =>
+trait Definitions { self: Trees =>
sealed trait Definition extends Tree {
val id: Identifier
@@ -37,12 +38,32 @@ trait Definitions { self0: Trees =>
def getType(implicit s: Symbols): Type = tpe
+ def to[A <: VariableSymbol](implicit ev: VariableConverter[A]): A = ev.convert(this)
+
override def equals(that: Any): Boolean = that match {
case vs: VariableSymbol => id == vs.id && tpe == vs.tpe
case _ => false
}
- def hashCode: Int = 61 * id.hashCode + tpe.hashCode
+ override def hashCode: Int = 61 * id.hashCode + tpe.hashCode
+ }
+
+ sealed abstract class VariableConverter[B <: VariableSymbol] {
+ def convert(a: VariableSymbol): B
+ }
+
+ implicit def convertToVal = new VariableConverter[ValDef] {
+ def convert(vs: VariableSymbol): ValDef = vs match {
+ case v: ValDef => v
+ case _ => ValDef(vs.id, vs.tpe)
+ }
+ }
+
+ implicit def convertToVar = new VariableConverter[Variable] {
+ def convert(vs: VariableSymbol): Variable = vs match {
+ case v: Variable => v
+ case _ => Variable(vs.id, vs.tpe)
+ }
}
/**
@@ -50,8 +71,11 @@ trait Definitions { self0: Trees =>
*/
case class ValDef(id: Identifier, tpe: Type) extends Definition with VariableSymbol {
/** Transform this [[ValDef]] into a [[Expressions.Variable Variable]] */
- def toVariable: Variable = Variable(id, tpe)
+ def toVariable: Variable = to[Variable]
def freshen: ValDef = ValDef(id.freshen, tpe).copiedFrom(this)
+
+ override def equals(that: Any): Boolean = super[VariableSymbol].equals(that)
+ override def hashCode: Int = super[VariableSymbol].hashCode
}
/** A wrapper for a program. For now a program is simply a single object. */
@@ -63,7 +87,8 @@ trait Definitions { self0: Trees =>
with Constructors
with Paths {
- val trees: self0.type = self0
+ val trees: self.type = self
+ val symbols: this.type = this
// @nv: this is a hack to reinject `this` into the set of implicits
// in scope when using the pattern:
@@ -248,12 +273,12 @@ trait Definitions { self0: Trees =>
}
}
- case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit symbols: Symbols) extends TypedClassDef {
+ case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
def descendants: Seq[TypedClassDef] = cd.descendants.map(_.typed(tps))
def ccDescendants: Seq[TypedCaseClassDef] = cd.ccDescendants.map(_.typed(tps))
}
- case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit symbols: Symbols) extends TypedClassDef {
+ case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
lazy val fields: Seq[ValDef] = {
val tmap = (cd.typeArgs zip tps).toMap
if (tmap.isEmpty) cd.fields
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 81555ad82..9fdc9329d 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -4,6 +4,7 @@ package inox
package ast
import utils._
+import scala.reflect._
/** Provides functions to manipulate [[purescala.Expressions]].
*
@@ -33,10 +34,12 @@ trait ExprOps extends GenTreeOps {
val Deconstructor = Operator
/** Replaces bottom-up variables by looking up for them in a map */
- def replaceFromSymbols(substs: Map[Variable, Expr], expr: Expr): Expr = postMap {
- case v: Variable => substs.get(v)
- case _ => None
- } (expr)
+ def replaceFromSymbols[V <: VariableSymbol](substs: Map[V, Expr], expr: Expr)(implicit ev: VariableConverter[V]): Expr = {
+ postMap {
+ case v: Variable => substs.get(v.to[V])
+ case _ => None
+ } (expr)
+ }
/** Replaces bottom-up variables by looking them up in a map from [[ValDef]] to expressions */
def replaceFromSymbols(substs: Map[ValDef, Expr], expr: Expr): Expr = postMap {
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 1bfd1b342..d5d21dfbc 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -47,7 +47,7 @@ trait Expressions { self: Trees =>
/** Stands for an undefined Expr, similar to `???` or `null` */
case class NoTree(tpe: Type) extends Expr with Terminal {
- val getType = tpe
+ def getType(implicit s: Symbols): Type = tpe
}
@@ -121,7 +121,7 @@ trait Expressions { self: Trees =>
*/
case class Variable(id: Identifier, tpe: Type) extends Expr with Terminal with VariableSymbol {
/** Transforms this [[Variable]] into a [[Definitions.ValDef ValDef]] */
- def toVal = ValDef(id, tpe)
+ def toVal = to[ValDef]
}
@@ -487,7 +487,7 @@ trait Expressions { self: Trees =>
* you should use [[purescala.Constructors#or purescala's constructor or]] or
* [[purescala.Constructors#orJoin purescala's constructor orJoin]]
*/
- case class Or(exprs: Seq[Expr]) extends Expr {
+ case class Or(exprs: Seq[Expr]) extends Expr with CachingTyped {
require(exprs.size >= 2)
protected def computeType(implicit s: Symbols): Type = {
if (exprs forall (_.getType == BooleanType)) BooleanType
@@ -506,7 +506,7 @@ trait Expressions { self: Trees =>
*
* @see [[leon.purescala.Constructors.implies]]
*/
- case class Implies(lhs: Expr, rhs: Expr) extends Expr {
+ case class Implies(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type = {
if(lhs.getType == BooleanType && rhs.getType == BooleanType) BooleanType
else Untyped
@@ -517,7 +517,7 @@ trait Expressions { self: Trees =>
*
* @see [[leon.purescala.Constructors.not]]
*/
- case class Not(expr: Expr) extends Expr {
+ case class Not(expr: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type = {
if (expr.getType == BooleanType) BooleanType
else bitVectorType(expr.getType)
@@ -683,19 +683,19 @@ trait Expressions { self: Trees =>
}
/** $encodingof `... > ...`*/
- case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr {
+ case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr with CachingTyped{
protected def computeType(implicit s: Symbols): Type =
if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
}
/** $encodingof `... <= ...`*/
- case class LessEquals(lhs: Expr, rhs: Expr) extends Expr {
+ case class LessEquals(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type =
if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
}
/** $encodingof `... >= ...`*/
- case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr {
+ case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type =
if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
}
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index a02aec449..050f9a485 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -299,7 +299,7 @@ trait Extractors { self: Trees =>
def unapply(me: MatchExpr) : Option[(Pattern, Expr, Expr)] = {
Option(me) collect {
- case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliased(pattern.binders, exprOps.variablesOf(scrut)) =>
+ case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliasedSymbols(pattern.binders, exprOps.variablesOf(scrut)) =>
( pattern, scrut, body )
}
}
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index 9295687bb..a8a6bdf3a 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -109,7 +109,7 @@ trait Trees extends Expressions with Extractors with Types with Definitions with
(s1 & s2).nonEmpty
}
- def aliased[T1 <: VariableSymbol,T2 <: VariableSymbol](vs1: Set[T1], vs2: Set[T2]): Boolean = {
+ def aliasedSymbols[T1 <: VariableSymbol,T2 <: VariableSymbol](vs1: Set[T1], vs2: Set[T2]): Boolean = {
aliased(vs1.map(_.id), vs2.map(_.id))
}
}
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index ce913f77f..b9069f65f 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -3,8 +3,11 @@
package inox
package evaluators
+case class EvaluatorOptions(options: Seq[InoxOption[Any]]) extends InoxOptions
+
trait Evaluator {
val program: Program
+ val options: EvaluatorOptions
import program.trees._
/** The type of value that this [[Evaluator]] calculates
diff --git a/src/main/scala/inox/evaluators/SolvingEvalInterface.scala b/src/main/scala/inox/evaluators/SolvingEvalInterface.scala
deleted file mode 100644
index 55e8b84db..000000000
--- a/src/main/scala/inox/evaluators/SolvingEvalInterface.scala
+++ /dev/null
@@ -1,37 +0,0 @@
-
-package inox
-package evaluators
-
-import scala.collection.mutable.{Map => MutableMap}
-
-trait SolvingEvalInterface {
- val program: Program
- import program._
- import program.trees._
- import program.symbols._
-
- val evaluator: DeterministicEvaluator with SolvingEvaluator { val program: SolvingEvalInterface.this.program.type }
- val bodies: Map[Identifier, (Seq[ValDef], Expr)]
-
- private val inputCache: MutableMap[(Identifier, Seq[Expr]), Expr] = MutableMap.empty
- private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
-
- def onInputInvocation(id: Identifier, args: Seq[Expr]): Expr = inputCache.getOrElseUpdate((id, args), {
- val (vds, body) = bodies.getOrElse(id, throw new RuntimeException("Body for " + id + " not found"))
- val tpSubst = canBeSupertypeOf(tupleTypeWrap(vds.map(_.tpe)), tupleTypeWrap(args.map(_.getType))).getOrElse {
- throw new RuntimeException("Cannot construct typing substitution from " + vds.map(_.asString).mkString(",") + " to " + args.map(_.asString))
- }
-
- val model = (vds.map(vd => vd.copy(tpe = instantiateType(vd.tpe, tpSubst))) zip args).toMap
- val instBody = instantiateType(body, tpSubst)
- evaluator.eval(instBody, model).result.getOrElse {
- throw new RuntimeException("Couldn't evaluate " + instBody.asString + " with model " +
- model.map(p => p._1.asString -> p._2.asString).mkString("{", ", ", "}"))
- }
- })
-
- def onForallInvocation(forall: Forall): Expr = forallCache.getOrElseUpdate(forall, {
-
-
- })
-}
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index e05333f49..9b5aee6ae 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -3,101 +3,88 @@
package inox
package evaluators
+import solvers._
+
import scala.collection.mutable.{Map => MutableMap}
trait SolvingEvaluator extends Evaluator {
- object bankOption extends InoxOptionDef[EvaluationBank] {
+ object optForallCache extends InoxOptionDef[MutableMap[program.trees.Forall, Boolean]] {
val parser = { (_: String) => throw FatalError("Unparsable option \"bankOption\"") }
val name = "bank-option"
val description = "Evaluation bank shared between solver and evaluator"
val usageRhs = ""
- def default = new EvaluationBank {
- val program: SolvingEvaluator.this.program.type = SolvingEvaluator.this.program
- }
+ def default = MutableMap.empty
}
- val solver: SolverFactory[Solver]
+ def getSolver(opts: InoxOption[Any]*): Solver { val program: SolvingEvaluator.this.program.type }
}
-/* Status of invariant checking
- *
- * For a given invariant, its checking status can be either
- * - Complete(success) : checking has been performed previously and
- * resulted in a value of `success`.
- * - Pending : invariant is currently being checked somewhere
- * in the program. If it fails, the failure is
- * assumed to be bubbled up to all relevant failure
- * points.
- * - NoCheck : invariant has never been seen before. Discovering
- * NoCheck for an invariant will automatically update
- * the status to `Pending` as this creates a checking
- * obligation.
- */
-sealed abstract class CheckStatus {
- /* The invariant was invalid and this particular case class can't exist */
- def isFailure: Boolean = this match {
- case Complete(status) => !status
- case _ => false
- }
+trait SolvingEvalInterface {
+ val program: Program
+ import program._
+ import program.trees._
+ import program.symbols._
- /* The invariant has never been checked before and the checking obligation
- * therefore falls onto the first caller of this method. */
- def isRequired: Boolean = this == NoCheck
-}
+ val evaluator: DeterministicEvaluator with SolvingEvaluator { val program: SolvingEvalInterface.this.program.type }
-case class Complete(success: Boolean) extends CheckStatus
-case object Pending extends CheckStatus
-case object NoCheck extends CheckStatus
+ private val specCache: MutableMap[Expr, Expr] = MutableMap.empty
+ private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
-object EvaluationBank {
- def empty(p: Program): EvaluationBank { val program: p.type } = new EvaluationBank {
- val program: p.type = p
- val checkCache = MutableMap.empty
- }
+ def onSpecInvocation(specs: Expr): Expr = specCache.getOrElseUpdate(specs, {
+ val Seq(free) = exprOps.variablesOf(specs).toSeq
+ val timer = ctx.timers.evaluators.specs.start()
- private def apply(p: Program)(cache: MutableMap[p.trees.CaseClass, CheckStatus]): EvaluationBank { val program: p.type } = new EvaluationBank {
- val program: p.type = p
- val checkCache = cache
- }
-}
+ val solver = evaluator.getSolver(evaluator.options.options.collect {
+ case o @ InoxOption(opt, _) if opt == evaluator.optForallCache => o
+ }.toSeq : _*)
-trait EvaluationBank {
- implicit val program: Program
- import program._
- import program.trees._
+ solver.assertCnstr(specs)
+ val res = solver.check(model = true)
+ timer.stop()
- /* Shared set that tracks checked case-class invariants
- *
- * Checking case-class invariants can require invoking a solver
- * on a ground formula that contains a reference to `this` (the
- * current case class). If we then wish to check the model
- * returned by the solver, the expression given to the evaluator
- * will again contain the constructor for the current case-class.
- * This will create an invariant-checking loop.
- *
- * To avoid this problem, we introduce a set of invariants
- * that have already been checked that is shared between related
- * solvers and evaluators. This set is used by the evaluators to
- * determine whether the invariant of a given case
- * class should be checked.
- */
- val checkCache: MutableMap[CaseClass, CheckStatus]
-
- /* Status of the invariant checking for `cc` */
- def invariantCheck(cc: CaseClass): CheckStatus = synchronized {
- if (!cc.ct.tcd.hasInvariant) Complete(true)
- else checkCache.getOrElse(cc, {
- checkCache(cc) = Pending
- NoCheck
- })
- }
+ res match {
+ case solver.Model(model) =>
+ valuateWithModel(model)(free.toVal)
- /* Update the cache with the invariant check result for `cc` */
- def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
- checkCache(cc) = Complete(success)
- }
+ case _ =>
+ throw new RuntimeException("Failed to evaluate specs " + specs.asString)
+ }
+ })
+
+ def onForallInvocation(forall: Forall): Expr = {
+ val cache = evaluator.options.findOption(evaluator.optForallCache).getOrElse {
+ throw new RuntimeException("Couldn't find evaluator's forall cache")
+ }
+
+ BooleanLiteral(cache.getOrElse(forall, {
+ val timer = ctx.timers.evaluators.forall.start()
- override def clone: EvaluationBank { val program: EvaluationBank.this.program.type } =
- EvaluationBank(program)(checkCache.clone)
+ val solver = evaluator.getSolver(
+ InoxOption(optSilentErrors)(true),
+ InoxOption(optCheckModels)(false),
+ InoxOption(evaluator.optForallCache)(cache)
+ )
+
+ solver.assertCnstr(Not(forall.body))
+ val res = solver.check(model = true)
+ timer.stop()
+
+ res match {
+ case solver.Unsat() =>
+ cache(forall) = true
+ true
+
+ case solver.Model(model) =>
+ cache(forall) = false
+ evaluator.eval(Not(forall.body), model) match {
+ case EvaluationResults.Successful(BooleanLiteral(true)) => false
+ case _ => throw new RuntimeException("Forall model check failed")
+ }
+
+ case _ =>
+ throw new RuntimeException("Failed to evaluate forall " + forall.asString)
+ }
+ }))
+ }
}
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 549d5ca75..20d6efe7a 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -6,16 +6,21 @@ package solvers
import utils._
import evaluators._
-case class SolverOptions(options: Seq[InoxOption[Any]]) {
- def set(opts: Seq[LeonOption[Any]]): SolverOptions = {
+case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions {
+ def set(opts: Seq[InoxOption[Any]]): SolverOptions = {
val changed = opts.map(_.optionDef).toSet
val remainingOpts = options.filter { case InoxOption(optDef, _) => !changed(optDef) }
copy(options = remainingOpts ++ opts)
}
+
+ def set(opt: InoxOption[Any], opts: InoxOption[Any]*): SolverOptions = set(opt +: opts)
}
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)
+
trait Solver extends Interruptible {
def name: String
val program: Program
@@ -25,13 +30,55 @@ trait Solver extends Interruptible {
import program.trees._
sealed trait SolverResponse
- sealed trait SolverCheckResponse extends SolverResponse
- sealed trait SolverModelResponse extends SolverResponse
+ case object Unknown extends SolverResponse
+
+ sealed trait SolverUnsatResponse extends SolverResponse
+ case object UnsatResponse extends SolverUnsatResponse
+ case class UnsatResponseWithCores(cores: Set[Expr]) extends SolverUnsatResponse
+
+ sealed trait SolverSatResponse extends SolverResponse
+ case object SatResponse extends SolverSatResponse
+ case class SatResponseWithModel(model: Map[ValDef, Expr]) extends SolverSatResponse
+
+ object Check {
+ def unapply(resp: SolverResponse): Option[Boolean] = resp match {
+ case _: SolverUnsatResponse => Some(false)
+ case _: SolverSatResponse => Some(true)
+ case Unknown => None
+ }
+ }
- case object Unknown extends SolverCheckResponse with SolverModelResponse
- case object UNSAT extends SolverCheckResponse with SolverModelResponse
- case object SAT extends SolverCheckResponse
- case class Model(model: Map[ValDef, Expr]) extends SolverModelResponse
+ object Sat {
+ def unapply(resp: SolverSatResponse): Boolean = resp match {
+ case SatResponse => true
+ case SatResponseWithModel(_) => throw FatalError("Unexpected sat response with model")
+ case _ => false
+ }
+ }
+
+ object Model {
+ def unapply(resp: SolverSatResponse): Option[Map[ValDef, Expr]] = resp match {
+ case SatResponseWithModel(model) => Some(model)
+ case SatResponse => throw FatalError("Unexpected sat response without model")
+ case _ => None
+ }
+ }
+
+ object Unsat {
+ def unapply(resp: SolverUnsatResponse): Boolean = resp match {
+ case UnsatResponse => true
+ case UnsatResponseWithCores(_) => throw FatalError("Unexpected unsat response with cores")
+ case _ => false
+ }
+ }
+
+ object Core {
+ def unapply(resp: SolverUnsatResponse): Option[Set[Expr]] = resp match {
+ case UnsatResponseWithCores(cores) => Some(cores)
+ case UnsatResponse => throw FatalError("Unexpected unsat response with cores")
+ case _ => None
+ }
+ }
object SolverUnsupportedError {
def msg(t: Tree, reason: Option[String]) = {
@@ -49,10 +96,9 @@ trait Solver extends Interruptible {
def assertCnstr(expression: Expr): Unit
- /** Returns Some(true) if it found a satisfying model, Some(false) if no model exists, and None otherwise */
- def check: Option[Boolean]
- /** Returns the model if it exists */
- def getModel: Model
+ def check(model: Boolean = false, cores: Boolean = false): SolverResponse
+ def checkAssumptions(model: Boolean = false, cores: Boolean = false)(assumptions: Set[Expr]): SolverResponse
+
def getResultSolver: Option[Solver] = Some(this)
def free()
@@ -62,9 +108,6 @@ trait Solver extends Interruptible {
def push(): Unit
def pop(): Unit
- def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
- def getUnsatCore: Set[Expr]
-
protected def unsupported(t: Tree): Nothing = {
val err = SolverUnsupportedError(t, None)
reporter.warning(err.getMessage)
--
GitLab