diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 3d8e64fe51feb5ce98f5eac98747fbc798c4bc9b..eb791cf360165c818cd31be39f7d46bbdc042b8f 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -33,14 +33,14 @@ trait SolvingEvaluator extends Evaluator {
case o @ InoxOption(opt, _) if opt == optForallCache => o
}.toSeq : _*)
- import solver.SolverResponses._
+ import SolverResponses._
solver.assertCnstr(body)
- val res = solver.check(model = true)
+ val res = solver.check(solver.Model)
timer.stop()
res match {
- case Model(model) =>
+ case SatWithModel(model) =>
valuateWithModel(model)(vd)
case _ =>
@@ -62,18 +62,18 @@ trait SolvingEvaluator extends Evaluator {
InoxOption(optForallCache)(cache)
)
- import solver.SolverResponses._
+ import SolverResponses._
solver.assertCnstr(Not(forall.body))
- val res = solver.check(model = true)
+ val res = solver.check(solver.Model)
timer.stop()
res match {
- case Unsat() =>
+ case Unsat =>
cache(forall) = true
true
- case Model(model) =>
+ case SatWithModel(model) =>
cache(forall) = false
eval(Not(forall.body), model) match {
case EvaluationResults.Successful(BooleanLiteral(true)) => false
diff --git a/src/main/scala/inox/solvers/SimpleSolverAPI.scala b/src/main/scala/inox/solvers/SimpleSolverAPI.scala
index 8f7c4b404cd9cec770800ad93d708cd844b1d71a..deb96092b6c93f01291fd4a04de4032aceb3c479 100644
--- a/src/main/scala/inox/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/inox/solvers/SimpleSolverAPI.scala
@@ -1,58 +1,54 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
package solvers
-import purescala.Expressions._
+trait SimpleSolverAPI {
+ protected val factory: SolverFactory
+
+ import factory.program.trees._
+ import SolverResponses._
-class SimpleSolverAPI(sf: SolverFactory[Solver]) {
def solveVALID(expression: Expr): Option[Boolean] = {
- val s = sf.getNewSolver()
+ val s = factory.getNewSolver()
+ import s._
try {
s.assertCnstr(Not(expression))
- s.check.map(r => !r)
+ s.check(Simple) match {
+ case Check(r) => Some(!r)
+ case _ => None
+ }
} finally {
- sf.reclaim(s)
+ factory.reclaim(s)
}
}
- def solveSAT(expression: Expr): (Option[Boolean], Model) = {
- val s = sf.getNewSolver()
+ def solveSAT(expression: Expr): ResponseWithModel[Map[ValDef, Expr]] = {
+ val s = factory.getNewSolver()
+ import s._
try {
s.assertCnstr(expression)
- s.check match {
- case Some(true) =>
- (Some(true), s.getModel)
- case Some(false) =>
- (Some(false), Model.empty)
- case None =>
- (None, Model.empty)
- }
+ s.check(Model)
} finally {
- sf.reclaim(s)
+ factory.reclaim(s)
}
}
- def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): Option[Either[Set[Expr], Model]] = {
- val s = sf.getNewSolver()
+ def solveSATWithCores(expression: Expr, assumptions: Set[Expr]):
+ ResponseWithModelAndCores[Map[ValDef, Expr], Set[Expr]] = {
+ val s = factory.getNewSolver()
+ import s._
try {
s.assertCnstr(expression)
- s.checkAssumptions(assumptions) match {
- case Some(false) =>
- Some(Left(s.getUnsatCore))
- case Some(true) =>
- Some(Right(s.getModel))
- case None =>
- None
- }
+ s.checkAssumptions(All)(assumptions)
} finally {
- sf.reclaim(s)
+ factory.reclaim(s)
}
}
}
object SimpleSolverAPI {
- def apply(sf: SolverFactory[Solver]) = {
- new SimpleSolverAPI(sf)
+ def apply(sf: SolverFactory) = new SimpleSolverAPI {
+ val factory: sf.type = sf
}
}
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index d4bf0d11b1febdeaf6a7c66cfb1423b3bf0f283d..a353f24596fc5042113775daeedcc043fa9c0a6c 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -29,60 +29,62 @@ trait Solver extends Interruptible {
import program._
import program.trees._
- object SolverResponses {
- sealed trait 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
- }
- }
+ import SolverResponses._
- object Sat {
- def unapply(resp: SolverSatResponse): Boolean = resp match {
- case SatResponse => true
- case SatResponseWithModel(_) => throw FatalError("Unexpected sat response with model")
- case _ => false
- }
+ sealed trait Configuration {
+ type Response <: SolverResponse[Map[ValDef, Expr], Set[Expr]]
+
+ def max(that: Configuration): Configuration = (this, that) match {
+ case (All , _ ) => All
+ case (_ , All ) => All
+ case (Model, Cores) => All
+ case (Cores, Model) => All
+ case (Model, _ ) => Model
+ case (_ , Model) => Model
+ case (Cores, _ ) => Cores
+ case (_ , Cores) => Cores
+ case _ => Simple
}
- 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
- }
+ def min(that: Configuration): Configuration = (this, that) match {
+ case (o1, o2) if o1 == o2 => o1
+ case (Simple, _) => Simple
+ case (_, Simple) => Simple
+ case (Model, Cores) => Simple
+ case (Cores, Model) => Simple
+ case (All, o) => o
+ case (o, All) => o
}
- object Unsat {
- def unapply(resp: SolverUnsatResponse): Boolean = resp match {
- case UnsatResponse => true
- case UnsatResponseWithCores(_) => throw FatalError("Unexpected unsat response with cores")
- case _ => false
- }
+ def in(solver: Solver): solver.Configuration = this match {
+ case Simple => solver.Simple
+ case Model => solver.Model
+ case Cores => solver.Cores
+ case All => solver.All
}
- 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
- }
- }
+ def cast(resp: SolverResponse[Map[ValDef, Expr], Set[Expr]]): Response = ((this, resp) match {
+ case (_ , Unknown) => Unknown
+ case (Simple | Cores, Sat) => Sat
+ case (Model | All , s @ SatWithModel(_)) => s
+ case (Simple | Model, Unsat) => Unsat
+ case (Cores | All , u @ UnsatWithCores(_)) => u
+ case _ => throw FatalError("Unexpected response " + resp + " for configuration " + this)
+ }).asInstanceOf[Response]
}
- import SolverResponses._
+ object Configuration {
+ def apply(model: Boolean = false, cores: Boolean = false): Configuration =
+ if (model && cores) All
+ else if (model) Model
+ else if (cores) Cores
+ else Simple
+ }
+
+ case object Simple extends Configuration { type Response = SimpleResponse }
+ case object Model extends Configuration { type Response = ResponseWithModel[Map[ValDef, Expr]] }
+ case object Cores extends Configuration { type Response = ResponseWithCores[Set[Expr]] }
+ case object All extends Configuration { type Response = ResponseWithModelAndCores[Map[ValDef, Expr], Set[Expr]] }
object SolverUnsupportedError {
def msg(t: Tree, reason: Option[String]) = {
@@ -100,9 +102,9 @@ trait Solver extends Interruptible {
def assertCnstr(expression: Expr): Unit
- def check(model: Boolean = false, cores: Boolean = false): SolverResponse
- def checkAssumptions(model: Boolean = false, cores: Boolean = false)(assumptions: Set[Expr]): SolverResponse
-
+ def check[R](config: Configuration { type Response <: R }): R
+ def checkAssumptions[R](config: Configuration { type Response <: R })(assumptions: Set[Expr]): R
+
def getResultSolver: Option[Solver] = Some(this)
def free()
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 6409e544cef3ba3545fc8dbfbbf671d4cdf9516e..c82a9b0d4dc4c351373e7611ab8bf51ac1ee7abf 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -5,7 +5,13 @@ package solvers
import scala.reflect.runtime.universe._
-abstract class SolverFactory[+S <: Solver] {
+trait SolverFactory {
+ val program: Program
+
+ type S <: Solver { val program: SolverFactory.this.program.type }
+
+ val name: String
+
def getNewSolver(): S
def shutdown(): Unit = {}
@@ -13,13 +19,15 @@ abstract class SolverFactory[+S <: Solver] {
def reclaim(s: Solver) {
s.free()
}
-
- val name: String
}
object SolverFactory {
- def apply[S <: Solver : TypeTag](nme: String, builder: () => S): SolverFactory[S] = {
- new SolverFactory[S] {
+ def apply[S1 <: Solver : TypeTag](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
+ type S = S1 { val program: p.type }
+
val name = nme
def getNewSolver() = builder()
}
diff --git a/src/main/scala/inox/solvers/SolverResponses.scala b/src/main/scala/inox/solvers/SolverResponses.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0f5f7f87faa89e8d12aa75db8b30b776fcede277
--- /dev/null
+++ b/src/main/scala/inox/solvers/SolverResponses.scala
@@ -0,0 +1,46 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+
+object SolverResponses {
+ sealed trait SolverResponse[+Model,+Cores]
+
+ sealed trait Satisfiable
+ sealed trait Unsatisfiable
+
+ sealed trait SimpleResponse extends SolverResponse[Nothing, Nothing]
+ sealed trait ResponseWithModel[+Model] extends SolverResponse[Model, Nothing]
+ sealed trait ResponseWithCores[+Cores] extends SolverResponse[Nothing, Cores]
+ sealed trait ResponseWithModelAndCores[+Model,+Cores] extends SolverResponse[Model, Cores]
+
+ case object Sat extends Satisfiable
+ with SimpleResponse
+ with ResponseWithCores[Nothing]
+
+ case object Unsat extends Unsatisfiable
+ with SimpleResponse
+ with ResponseWithModel[Nothing]
+
+ case class SatWithModel[Model](model: Model) extends Satisfiable
+ with ResponseWithModel[Model]
+ with ResponseWithModelAndCores[Model, Nothing]
+
+ case class UnsatWithCores[Cores](cores: Cores) extends Unsatisfiable
+ with ResponseWithCores[Cores]
+ with ResponseWithModelAndCores[Nothing, Cores]
+
+ case object Unknown extends SimpleResponse
+ with ResponseWithModel[Nothing]
+ with ResponseWithCores[Nothing]
+ with ResponseWithModelAndCores[Nothing, Nothing]
+
+ object Check {
+ def unapply[Core,Model](resp: SolverResponse[Core,Model]): Option[Boolean] = resp match {
+ case _: Satisfiable => Some(true)
+ case _: Unsatisfiable => Some(false)
+ case Unknown => None
+ }
+ }
+}
+
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index adfdf3a9ff838bb3fcbaec4316498e0aeb766738..2b3f4079438ae65ca5369418db0836205cd9f890 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -42,8 +42,8 @@ trait AbstractUnrollingSolver
val assumePreHolds = options.findOptionOrDefault(optAssumePre)
val silentErrors = options.findOptionOrDefault(optSilentErrors)
- def check(model: Boolean = false, cores: Boolean = false): SolverResponses.SolverResponse =
- checkAssumptions(model = model, cores = cores)(Set.empty)
+ def check[R](config: Configuration { type Response <: R }): R =
+ checkAssumptions(config)(Set.empty)
private val constraints = new IncrementalSeq[Expr]()
private val freeVars = new IncrementalMap[Variable, Encoded]()
@@ -124,15 +124,17 @@ trait AbstractUnrollingSolver
* This sequence of calls can also be used to mimic solver.checkAssumptions()
* for solvers that don't support the construct natively.
*/
- def solverCheck[R](clauses: Seq[Encoded], model: Boolean = false, cores: Boolean = false)
+ def solverCheck[R](config: Configuration)
+ (clauses: Seq[Encoded])
(block: Response => R): R
/** We define solverCheckAssumptions in CPS in order for solvers that don't
* support this feature to be able to use the provided [[solverCheck]] CPS
* construction.
*/
- def solverCheckAssumptions[R](assumptions: Seq[Encoded], model: Boolean = false, cores: Boolean = false)
- (block: Response => R): R = solverCheck(assumptions)(block)
+ def solverCheckAssumptions[R](config: Configuration)
+ (assumptions: Seq[Encoded])
+ (block: Response => R): R = solverCheck(config)(assumptions)(block)
trait ModelWrapper {
def modelEval(elem: Encoded, tpe: Type): Option[Expr]
@@ -284,7 +286,7 @@ trait AbstractUnrollingSolver
}
}
- def checkAssumptions(model: Boolean = false, cores: Boolean = false)(assumptions: Set[Expr]) = {
+ def checkAssumptions[R](config: Configuration { type Response <: R })(assumptions: Set[Expr]): R = {
val assumptionsSeq : Seq[Expr] = assumptions.toSeq
val encodedAssumptions : Seq[Encoded] = assumptionsSeq.map { expr =>
@@ -302,7 +304,7 @@ trait AbstractUnrollingSolver
}
sealed abstract class CheckState
- class CheckResult(val response: SolverResponses.SolverResponse) extends CheckState
+ class CheckResult(val response: config.Response) extends CheckState
case class Validate(model: Option[Map[ValDef, Expr]]) extends CheckState
case object ModelCheck extends CheckState
case object FiniteRangeCheck extends CheckState
@@ -311,15 +313,18 @@ trait AbstractUnrollingSolver
case object Unroll extends CheckState
object CheckResult {
- def apply(resp: SolverResponses.SolverResponse) = new CheckResult(resp)
- def apply(resp: Response): CheckResult = new CheckResult(resp match {
- case Unknown => SolverResponses.Unknown
- case Sat(None) => SolverResponses.SatResponse
- case Sat(Some(model)) => SolverResponses.SatResponseWithModel(extractSimpleModel(model))
- case Unsat(None) => SolverResponses.UnsatResponse
- case Unsat(Some(core)) => SolverResponses.UnsatResponseWithCores(encodedCoreToCore(core))
- })
- def unapply(res: CheckResult): Option[SolverResponses.SolverResponse] = Some(res.response)
+ def apply(resp: config.Response) = new CheckResult(resp)
+
+ def apply(resp: Response): CheckResult = new CheckResult(config.cast(resp match {
+ case Unknown => SolverResponses.Unknown
+ case Sat(None) => SolverResponses.Sat
+ case Sat(Some(model)) => SolverResponses.SatWithModel(extractSimpleModel(model))
+ case Unsat(None) => SolverResponses.Unsat
+ case Unsat(Some(cores)) => SolverResponses.UnsatWithCores(encodedCoreToCore(cores))
+ case _ => throw FatalError("Unexpected response " + resp + " for configuration " + config)
+ }))
+
+ def unapply(res: CheckResult): Option[config.Response] = Some(res.response)
}
object Abort {
@@ -335,14 +340,13 @@ trait AbstractUnrollingSolver
case ModelCheck =>
reporter.debug(" - Running search...")
- val withModel = model && !templates.requiresFiniteRangeCheck
- val withCores = cores || unrollUnsatCores
+ val checkConfig = config
+ .min(Configuration(model = !templates.requiresFiniteRangeCheck, cores = true))
+ .max(Configuration(model = false, cores = unrollUnsatCores))
val timer = ctx.timers.solvers.check.start()
- solverCheckAssumptions(
- encodedAssumptions.toSeq ++ templates.satisfactionAssumptions,
- model = withModel,
- cores = withCores
+ solverCheckAssumptions(checkConfig)(
+ encodedAssumptions.toSeq ++ templates.satisfactionAssumptions
) { res =>
timer.stop()
@@ -379,9 +383,8 @@ trait AbstractUnrollingSolver
val clauses = templates.getFiniteRangeClauses
val timer = ctx.timers.solvers.check.start()
- solverCheck(
- encodedAssumptions.toSeq ++ templates.satisfactionAssumptions ++ clauses,
- model = model
+ solverCheck(config min Model)(
+ encodedAssumptions.toSeq ++ templates.satisfactionAssumptions ++ clauses
) { res =>
timer.stop()
@@ -400,11 +403,11 @@ trait AbstractUnrollingSolver
}
case Validate(optModel) => optModel match {
- case None => CheckResult(SolverResponses.SatResponse)
+ case None => CheckResult(config cast SolverResponses.Sat)
case Some(model) =>
val valid = !checkModels || validateModel(model, assumptionsSeq, silenceErrors = silentErrors)
if (valid) {
- CheckResult(SolverResponses.SatResponseWithModel(model))
+ CheckResult(config cast SolverResponses.SatWithModel(model))
} else {
reporter.error(
"Something went wrong. The model should have been valid, yet we got this: " +
@@ -431,10 +434,8 @@ trait AbstractUnrollingSolver
}
val timer = ctx.timers.solvers.check.start()
- solverCheckAssumptions(
- encodedAssumptions.toSeq ++ templates.refutationAssumptions,
- model = feelingLucky,
- cores = cores
+ solverCheckAssumptions(config max Configuration(model = feelingLucky))(
+ encodedAssumptions.toSeq ++ templates.refutationAssumptions
) { res =>
timer.stop()
@@ -532,20 +533,21 @@ trait UnrollingSolver extends AbstractUnrollingSolver {
solver.assertCnstr(cnstr)
}
- case class Model(model: Map[ValDef, Expr]) extends ModelWrapper {
+ case class ModelWrapper(model: Map[ValDef, Expr]) extends super.ModelWrapper {
def modelEval(elem: Expr, tpe: Type): Option[Expr] = evaluator.eval(elem, model).result
override def toString = model.mkString("\n")
}
- def solverCheck[R](clauses: Seq[Expr], model: Boolean = false, cores: Boolean = false)(block: Response => R): R = {
+ def solverCheck[R](config: Configuration)(clauses: Seq[Expr])(block: Response => R): R = {
solver.push()
for (cls <- clauses) solver.assertCnstr(cls)
- val res = solver.check(model = model, cores = cores) match {
- case solver.SolverResponses.Unknown => Unknown
- case solver.SolverResponses.UnsatResponse => Unsat(None)
- case solver.SolverResponses.UnsatResponseWithCores(cores) => Unsat(Some(cores))
- case solver.SolverResponses.SatResponse => Sat(None)
- case solver.SolverResponses.SatResponseWithModel(model) => Sat(Some(Model(model)))
+ import SolverResponses.{SolverResponse => SR}
+ val res = solver.check[SR[Map[ValDef, Expr], Set[Expr]]](config in solver) match {
+ case SolverResponses.Unknown => Unknown
+ case SolverResponses.Unsat => Unsat(None)
+ case SolverResponses.UnsatWithCores(cores) => Unsat(Some(cores))
+ case SolverResponses.Sat => Sat(None)
+ case SolverResponses.SatWithModel(model) => Sat(Some(ModelWrapper(model)))
}
val r = block(res)
solver.pop()