diff --git a/src/main/scala/leon/solvers/QuantificationSolver.scala b/src/main/scala/leon/solvers/QuantificationSolver.scala
index 4f56903c578da6c2d1b71f19268e8885cb93e99e..8ffe0a004cd23c39da6cd373774497ee78835974 100644
--- a/src/main/scala/leon/solvers/QuantificationSolver.scala
+++ b/src/main/scala/leon/solvers/QuantificationSolver.scala
@@ -27,7 +27,6 @@ class HenkinModelBuilder(domains: HenkinDomains)
trait QuantificationSolver extends Solver {
val program: Program
- def getModel: HenkinModel
protected lazy val requireQuantification = program.definedFunctions.exists { fd =>
purescala.ExprOps.exists { case _: Forall => true case _ => false } (fd.fullBody)
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 42d7ead0235a13ad3465dcd1fe64fd80db33ed25..4f8b1f50ae346887c945823ff429761be1a34a78 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -31,13 +31,13 @@ object SolverFactory {
}
val definedSolvers = Map(
- "fairz3" -> "Native Z3 with z3-templates for unfolding (default)",
+ "fairz3" -> "Native Z3 with z3-templates for unrolling (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 reasoning, 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",
+ "unrollz3" -> "Native Z3 with leon-templates for unrolling",
"ground" -> "Only solves ground verification conditions by evaluating them",
"enum" -> "Enumeration-based counter-example-finder",
"isabelle" -> "Isabelle2015 through libisabelle with various automated tactics"
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 1235d69c6d16a2726971cac386732fdcea501b95..5f002ccdacb54b16515fa0d54f7573ba2ebc82cb 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -4,6 +4,7 @@ package leon
package solvers
package combinators
+import purescala.Printable
import purescala.Common._
import purescala.Definitions._
import purescala.Quantification._
@@ -13,118 +14,205 @@ import purescala.ExprOps._
import purescala.Types._
import utils._
-import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks, optUnfoldFactor}
import templates._
import evaluators._
import Template._
-class UnrollingSolver(val context: LeonContext, val program: Program, underlying: Solver)
- extends Solver
- with NaiveAssumptionSolver
- with EvaluatingSolver
- with QuantificationSolver {
+trait UnrollingProcedure extends LeonComponent {
+ val name = "Unroll-P"
+ val description = "Leon Unrolling Procedure"
- val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
- val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
- val assumePreHolds = context.findOptionOrDefault(optAssumePre)
- val disableChecks = context.findOptionOrDefault(optNoChecks)
- val unfoldFactor = context.findOptionOrDefault(optUnfoldFactor)
+ val optUnrollFactor = LeonLongOptionDef("unrollfactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
+ val optFeelingLucky = LeonFlagOptionDef("feelinglucky", "Use evaluator to find counter-examples early", false)
+ val optCheckModels = LeonFlagOptionDef("checkmodels", "Double-check counter-examples with evaluator", false)
+ val optUnrollCores = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unfolding while remaining fair", false)
+ val optUseCodeGen = LeonFlagOptionDef("codegen", "Use compiled evaluator instead of interpreter", false)
+ val optAssumePre = LeonFlagOptionDef("assumepre", "Assume precondition holds (pre && f(x) = body) when unfolding", false)
+ val optPartialModels = LeonFlagOptionDef("partialmodels", "Extract domains for quantifiers and bounded first-class functions", false)
- protected var lastCheckResult : (Boolean, Option[Boolean], Option[HenkinModel]) = (false, None, None)
+ override val definedOptions: Set[LeonOptionDef[Any]] =
+ Set(optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre, optUnrollFactor, optPartialModels)
+}
- private val freeVars = new IncrementalSet[Identifier]()
- private val constraints = new IncrementalSeq[Expr]()
+object UnrollingProcedure extends UnrollingProcedure
- protected var interrupted : Boolean = false
+trait AbstractUnrollingSolver[T]
+ extends UnrollingProcedure
+ with Solver
+ with EvaluatingSolver
+ with QuantificationSolver {
- val reporter = context.reporter
+ val unfoldFactor = context.findOptionOrDefault(optUnrollFactor)
+ val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
+ val checkModels = context.findOptionOrDefault(optCheckModels)
+ val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
+ val unrollUnsatCores = context.findOptionOrDefault(optUnrollCores)
+ val assumePreHolds = context.findOptionOrDefault(optAssumePre)
+ val partialModels = context.findOptionOrDefault(optPartialModels)
- def name = "U:"+underlying.name
+ protected var foundDefinitiveAnswer = false
+ protected var definitiveAnswer : Option[Boolean] = None
+ protected var definitiveModel : Model = Model.empty
+ protected var definitiveCore : Set[Expr] = Set.empty
- def free() {
- underlying.free()
+ def check: Option[Boolean] = {
+ genericCheck(Set.empty)
}
- val templateGenerator = new TemplateGenerator(new TemplateEncoder[Expr] {
- def encodeId(id: Identifier): Expr= {
- Variable(id.freshen)
- }
+ def getModel: Model = if (foundDefinitiveAnswer && definitiveAnswer.getOrElse(false)) {
+ definitiveModel
+ } else {
+ Model.empty
+ }
- def encodeExpr(bindings: Map[Identifier, Expr])(e: Expr): Expr = {
- replaceFromIDs(bindings, e)
- }
+ def getUnsatCore: Set[Expr] = if (foundDefinitiveAnswer && !definitiveAnswer.getOrElse(true)) {
+ definitiveCore
+ } else {
+ Set.empty
+ }
- def substitute(substMap: Map[Expr, Expr]): Expr => Expr = {
- (e: Expr) => replace(substMap, e)
- }
+ private val freeVars = new IncrementalMap[Identifier, T]()
+ private val constraints = new IncrementalSeq[Expr]()
- def mkNot(e: Expr) = not(e)
- def mkOr(es: Expr*) = orJoin(es)
- def mkAnd(es: Expr*) = andJoin(es)
- def mkEquals(l: Expr, r: Expr) = Equals(l, r)
- def mkImplies(l: Expr, r: Expr) = implies(l, r)
- }, assumePreHolds)
+ protected var interrupted : Boolean = false
- val unrollingBank = new UnrollingBank(context, templateGenerator)
+ protected val reporter = context.reporter
- val solver = underlying
+ lazy val templateGenerator = new TemplateGenerator(templateEncoder, assumePreHolds)
+ lazy val unrollingBank = new UnrollingBank(context, templateGenerator)
- def assertCnstr(expression: Expr) {
- constraints += expression
+ def push(): Unit = {
+ unrollingBank.push()
+ constraints.push()
+ freeVars.push()
+ }
- val freeIds = variablesOf(expression)
+ def pop(): Unit = {
+ unrollingBank.pop()
+ constraints.pop()
+ freeVars.pop()
+ }
- freeVars ++= freeIds
+ override def reset() = {
+ foundDefinitiveAnswer = false
+ interrupted = false
- val newVars = freeIds.map(_.toVariable: Expr)
+ unrollingBank.reset()
+ constraints.reset()
+ freeVars.reset()
+ }
- val bindings = newVars.zip(newVars).toMap
+ override def interrupt(): Unit = {
+ interrupted = true
+ }
- val newClauses = unrollingBank.getClauses(expression, bindings)
+ override def recoverInterrupt(): Unit = {
+ interrupted = false
+ }
+ def assertCnstr(expression: Expr, bindings: Map[Identifier, T]): Unit = {
+ constraints += expression
+ freeVars ++= bindings
+
+ val newClauses = unrollingBank.getClauses(expression, bindings.map { case (k, v) => Variable(k) -> v })
for (cl <- newClauses) {
- solver.assertCnstr(cl)
+ solverAssert(cl)
}
}
- override def dbg(msg: => Any) = underlying.dbg(msg)
-
- def push() {
- unrollingBank.push()
- solver.push()
- freeVars.push()
- constraints.push()
+ def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
+ foundDefinitiveAnswer = true
+ definitiveAnswer = res
+ definitiveModel = model
+ definitiveCore = core
}
- def pop() {
- unrollingBank.pop()
- solver.pop()
- freeVars.pop()
- constraints.pop()
+ implicit val printable: T => Printable
+ val templateEncoder: TemplateEncoder[T]
+
+ def solverAssert(cnstr: T): Unit
+
+ /** 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[T])(block: Option[Boolean] => R): R =
+ solverCheck(assumptions)(block)
+
+ def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] =
+ genericCheck(assumptions)
+
+ /** Provides CPS solver.check call. CPS is necessary in order for calls that
+ * depend on solver.getModel to be able to access the model BEFORE the call
+ * to solver.pop() is issued.
+ *
+ * The underlying solver therefore performs the following sequence of
+ * solver calls:
+ * {{{
+ * solver.push()
+ * for (cls <- clauses) solver.assertCnstr(cls)
+ * val res = solver.check
+ * block(res)
+ * solver.pop()
+ * }}}
+ *
+ * This ordering guarantees that [[block]] can safely call solver.getModel.
+ *
+ * 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[T])(block: Option[Boolean] => R): R
+
+ def solverUnsatCore: Option[Seq[T]]
+
+ trait ModelWrapper {
+ def get(id: Identifier): Option[Expr]
+ def eval(elem: T, tpe: TypeTree): Option[Expr]
}
- def check: Option[Boolean] = {
- genericCheck(Set())
- }
+ def solverGetModel: ModelWrapper
- def hasFoundAnswer = lastCheckResult._1
+ private def emit(silenceErrors: Boolean)(msg: String) =
+ if (silenceErrors) reporter.debug(msg) else reporter.warning(msg)
- private def extractModel(model: Model): HenkinModel = {
- val allVars = freeVars.toSet
+ private def extractModel(wrapper: ModelWrapper): Model =
+ new Model(freeVars.toMap.map(p => p._1 -> wrapper.get(p._1).get))
- def extract(b: Expr, m: Matcher[Expr]): Set[Seq[Expr]] = {
- val QuantificationTypeMatcher(fromTypes, _) = m.tpe
- val optEnabler = evaluator.eval(b, model).result
+ private def validateModel(model: Model, assumptions: Seq[Expr], silenceErrors: Boolean): Boolean = {
+ val expr = andJoin(assumptions ++ constraints)
+
+ evaluator.check(expr, model) match {
+ case EvaluationResults.CheckSuccess =>
+ reporter.debug("- Model validated.")
+ true
+
+ case EvaluationResults.CheckValidityFailure =>
+ reporter.debug("- Invalid model.")
+ false
+
+ case EvaluationResults.CheckRuntimeFailure(msg) =>
+ emit(silenceErrors)("- Model leads to evaluation error: " + msg)
+ false
+
+ case EvaluationResults.CheckQuantificationFailure(msg) =>
+ emit(silenceErrors)("- Model leads to quantification error: " + msg)
+ false
+ }
+ }
+
+ private def getPartialModel: HenkinModel = {
+ val wrapped = solverGetModel
- if (optEnabler == Some(BooleanLiteral(true))) {
- val optArgs = m.args.map(arg => evaluator.eval(arg.encoded, model).result)
+ def extract(b: T, m: Matcher[T]): Option[Seq[Expr]] = {
+ val QuantificationTypeMatcher(fromTypes, _) = m.tpe
+ val optEnabler = wrapped.eval(b, BooleanType)
+ optEnabler.filter(_ == BooleanLiteral(true)).flatMap { _ =>
+ val optArgs = (m.args zip fromTypes).map { case (arg, tpe) => wrapped.eval(arg.encoded, tpe) }
if (optArgs.forall(_.isDefined)) {
- Set(optArgs.map(_.get))
+ Some(optArgs.map(_.get))
} else {
- Set.empty
+ None
}
- } else {
- Set.empty
}
}
@@ -134,229 +222,319 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
case (tpe, domain) => tpe -> domain.flatMap { case (b, m) => extract(b, m) }.toSet
}
- val funDomains: Map[Identifier, Set[Seq[Expr]]] = partialInsts.map {
- case (Variable(id), domain) => id -> domain.flatMap { case (b, m) => extract(b, m) }.toSet
+ val funDomains: Map[Identifier, Set[Seq[Expr]]] = freeVars.map { case (id, idT) =>
+ id -> partialInsts.get(idT).toSeq.flatten.flatMap { case (b, m) => extract(b, m) }.toSet
}
val lambdaDomains: Map[Lambda, Set[Seq[Expr]]] = lambdaInsts.map {
case (l, domain) => l -> domain.flatMap { case (b, m) => extract(b, m) }.toSet
}
+ val model = extractModel(wrapped)
val asDMap = purescala.Quantification.extractModel(model.toMap, funDomains, typeDomains, evaluator)
val domains = new HenkinDomains(lambdaDomains, typeDomains)
new HenkinModel(asDMap, domains)
}
- def foundAnswer(res: Option[Boolean], model: Option[HenkinModel] = None) = {
- lastCheckResult = (true, res, model)
- }
+ private def getTotalModel(silenceErrors: Boolean = false): (Boolean, Model) = {
+ if (interrupted) {
+ (false, Model.empty)
+ } else {
+ var valid = false
+ var wrapper = solverGetModel
- def validatedModel(silenceErrors: Boolean = false): (Boolean, HenkinModel) = {
- val lastModel = solver.getModel
- val clauses = templateGenerator.manager.checkClauses
- val optModel = if (clauses.isEmpty) Some(lastModel) else {
- solver.push()
- for (clause <- clauses) {
- solver.assertCnstr(clause)
- }
+ val clauses = templateGenerator.manager.checkClauses
+ if (clauses.isEmpty) {
+ valid = true
+ } else {
+ reporter.debug(" - Verifying model transitivity")
- reporter.debug(" - Verifying model transitivity")
- val solverModel = solver.check match {
- case Some(true) =>
- Some(solver.getModel)
-
- case Some(false) =>
- val msg = "- Transitivity independence not guaranteed for model"
- if (silenceErrors) {
- reporter.debug(msg)
- } else {
- reporter.warning(msg)
- }
- None
+ val timer = context.timers.solvers.check.start()
+ solverCheck(clauses) { res =>
+ timer.stop()
+
+ reporter.debug(" - Finished transitivity check")
- case None =>
- val msg = "- Unknown for transitivity independence!?"
- if (silenceErrors) {
- reporter.debug(msg)
- } else {
- reporter.warning(msg)
+ res match {
+ case Some(true) =>
+ wrapper = solverGetModel
+ valid = true
+
+ case Some(false) =>
+ emit(silenceErrors)(" - Transitivity independence not guaranteed for model")
+
+ case None =>
+ emit(silenceErrors)(" - Unknown for transitivity independence!?")
}
- None
+ }
}
- solver.pop()
- solverModel
+ (valid, extractModel(wrapper))
}
+ }
- optModel match {
- case None =>
- (false, extractModel(lastModel))
+ def genericCheck(assumptions: Set[Expr]): Option[Boolean] = {
+ foundDefinitiveAnswer = false
+
+ val encoder = templateGenerator.encoder.encodeExpr(freeVars.toMap) _
+ val assumptionsSeq : Seq[Expr] = assumptions.toSeq
+ val encodedAssumptions : Seq[T] = assumptionsSeq.map(encoder)
+ val encodedToAssumptions : Map[T, Expr] = (encodedAssumptions zip assumptionsSeq).toMap
+
+ def encodedCoreToCore(core: Seq[T]): Set[Expr] = {
+ core.flatMap(ast => encodedToAssumptions.get(ast) match {
+ case Some(n @ Not(Variable(_))) => Some(n)
+ case Some(v @ Variable(_)) => Some(v)
+ case _ => None
+ }).toSet
+ }
- case Some(m) =>
- val model = extractModel(m)
+ while(!foundDefinitiveAnswer && !interrupted) {
+ reporter.debug(" - Running search...")
- val expr = andJoin(constraints.toSeq)
- val fullModel = model set freeVars.toSet
+ val timer = context.timers.solvers.check.start()
+ solverCheckAssumptions(encodedAssumptions.toSeq ++ unrollingBank.satisfactionAssumptions) { res =>
+ timer.stop()
- (evaluator.check(expr, fullModel) match {
- case EvaluationResults.CheckSuccess =>
- reporter.debug("- Model validated.")
- true
+ reporter.debug(" - Finished search with blocked literals")
- case EvaluationResults.CheckValidityFailure =>
- reporter.debug("- Invalid model.")
- false
+ res match {
+ case None =>
+ foundAnswer(None)
- case EvaluationResults.CheckRuntimeFailure(msg) =>
- if (silenceErrors) {
- reporter.debug("- Model leads to evaluation error: " + msg)
+ case Some(true) => // SAT
+ val (stop, model) = if (!partialModels) {
+ getTotalModel(silenceErrors = true)
} else {
- reporter.warning("- Model leads to evaluation error: " + msg)
+ (true, getPartialModel)
}
- false
- case EvaluationResults.CheckQuantificationFailure(msg) =>
- if (silenceErrors) {
- reporter.debug("- Model leads to quantification error: " + msg)
- } else {
- reporter.warning("- Model leads to quantification error: " + msg)
+ if (!interrupted) {
+ if (!stop) {
+ if (!unrollingBank.canInstantiate) {
+ reporter.error("Something went wrong. The model is not transitive yet we can't instantiate!?")
+ reporter.error(model.asString(context))
+ foundAnswer(None, model)
+ } else {
+ // further quantifier instantiations are required!
+ val newClauses = unrollingBank.instantiateQuantifiers
+ reporter.debug(" - more instantiations")
+
+ for (cls <- newClauses) {
+ solverAssert(cls)
+ }
+
+ reporter.debug(" - finished instantiating")
+ }
+ } else {
+ val valid = !checkModels || validateModel(model, assumptionsSeq, silenceErrors = false)
+
+ if (valid) {
+ foundAnswer(Some(true), model)
+ } else {
+ reporter.error("Something went wrong. The model should have been valid, yet we got this : ")
+ reporter.error(model.asString(context))
+ foundAnswer(None, model)
+ }
+ }
}
- false
- }, fullModel)
- }
- }
-
- def genericCheck(assumptions: Set[Expr]): Option[Boolean] = {
- lastCheckResult = (false, None, None)
- while(!hasFoundAnswer && !interrupted) {
- reporter.debug(" - Running search...")
-
- solver.push()
- solver.assertCnstr(andJoin((assumptions ++ unrollingBank.satisfactionAssumptions).toSeq))
- val res = solver.check
-
- reporter.debug(" - Finished search with blocked literals")
+ if (interrupted) {
+ foundAnswer(None)
+ }
- res match {
- case None =>
- solver.pop()
+ case Some(false) if !unrollingBank.canUnroll =>
+ solverUnsatCore match {
+ case Some(core) =>
+ val exprCore = encodedCoreToCore(core)
+ foundAnswer(Some(false), core = exprCore)
+ case None =>
+ foundAnswer(Some(false))
+ }
- reporter.ifDebug { debug =>
- reporter.debug("Solver returned unknown!?")
- }
- foundAnswer(None)
+ case Some(false) =>
+ if (unrollUnsatCores) {
+ solverUnsatCore match {
+ case Some(core) =>
+ unrollingBank.decreaseAllGenerations()
+
+ for (c <- core) templateGenerator.encoder.extractNot(c) match {
+ case Some(b) => unrollingBank.promoteBlocker(b)
+ case None => reporter.fatalError("Unexpected blocker polarity for unsat core unrolling: " + c)
+ }
+ case None =>
+ reporter.fatalError("Can't unroll unsat core for incompatible solver " + name)
+ }
+ }
- case Some(true) => // SAT
- val (valid, model) = if (!this.disableChecks && requireQuantification) {
- validatedModel(silenceErrors = false)
- } else {
- true -> extractModel(solver.getModel)
- }
+ if (!interrupted) {
+ if (feelingLucky) {
+ reporter.debug(" - Running search without blocked literals (w/ lucky test)")
+ } else {
+ reporter.debug(" - Running search without blocked literals (w/o lucky test)")
+ }
- solver.pop()
- if (valid) {
- foundAnswer(Some(true), Some(model))
- } else {
- reporter.error("Something went wrong. The model should have been valid, yet we got this : ")
- reporter.error(model.asString(context))
- foundAnswer(None, Some(model))
- }
+ val timer = context.timers.solvers.check.start()
+ solverCheckAssumptions(encodedAssumptions.toSeq ++ unrollingBank.refutationAssumptions) { res2 =>
+ timer.stop()
+
+ reporter.debug(" - Finished search without blocked literals")
+
+ res2 match {
+ case Some(false) =>
+ solverUnsatCore match {
+ case Some(core) =>
+ val exprCore = encodedCoreToCore(core)
+ foundAnswer(Some(false), core = exprCore)
+ case None =>
+ foundAnswer(Some(false))
+ }
+
+ case Some(true) =>
+ if (this.feelingLucky && !interrupted) {
+ // we might have been lucky :D
+ val model = extractModel(solverGetModel)
+ val valid = validateModel(model, assumptionsSeq, silenceErrors = true)
+ if (valid) foundAnswer(Some(true), model)
+ }
+
+ case None =>
+ foundAnswer(None)
+ }
+ }
+ }
- case Some(false) if !unrollingBank.canUnroll =>
- solver.pop()
- foundAnswer(Some(false))
+ if (interrupted) {
+ foundAnswer(None)
+ }
- case Some(false) =>
- //debug("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
- //debug("UNSAT BECAUSE: "+core.mkString(" AND "))
- solver.pop()
+ if (!foundDefinitiveAnswer) {
+ reporter.debug("- We need to keep going")
- if (!interrupted) {
- if (feelingLucky) {
- reporter.debug(" - Running search without blocked literals (w/ lucky test)")
- } else {
- reporter.debug(" - Running search without blocked literals (w/o lucky test)")
- }
+ // unfolling `unfoldFactor` times
+ for (i <- 1 to unfoldFactor.toInt) {
+ val toRelease = unrollingBank.getBlockersToUnlock
- solver.push()
- solver.assertCnstr(andJoin(assumptions.toSeq ++ unrollingBank.refutationAssumptions))
- val res2 = solver.check
+ reporter.debug(" - more unrollings")
- res2 match {
- case Some(false) =>
- //reporter.debug("UNSAT WITHOUT Blockers")
- foundAnswer(Some(false))
+ val newClauses = unrollingBank.unrollBehind(toRelease)
- case Some(true) =>
- if (feelingLucky && !interrupted) {
- // we might have been lucky :D
- val (valid, model) = validatedModel(silenceErrors = true)
- if (valid) foundAnswer(Some(true), Some(model))
+ for (ncl <- newClauses) {
+ solverAssert(ncl)
}
+ }
- case None =>
- foundAnswer(None)
+ reporter.debug(" - finished unrolling")
}
- solver.pop()
- }
+ }
+ }
+ }
- if(interrupted) {
- foundAnswer(None)
- }
+ if (interrupted) {
+ None
+ } else {
+ definitiveAnswer
+ }
+ }
+}
- if(!hasFoundAnswer) {
- reporter.debug("- We need to keep going.")
+class UnrollingSolver(val context: LeonContext, val program: Program, underlying: Solver)
+ extends AbstractUnrollingSolver[Expr] {
- // unfolling `unfoldFactor` times
- for (i <- 1 to unfoldFactor.toInt) {
- val toRelease = unrollingBank.getBlockersToUnlock
+ override val name = "U:"+underlying.name
- reporter.debug(" - more unrollings")
+ def free() {
+ underlying.free()
+ }
- val newClauses = unrollingBank.unrollBehind(toRelease)
+ val printable = (e: Expr) => e
- for (ncl <- newClauses) {
- solver.assertCnstr(ncl)
- }
- }
+ val templateEncoder = new TemplateEncoder[Expr] {
+ def encodeId(id: Identifier): Expr= {
+ Variable(id.freshen)
+ }
- reporter.debug(" - finished unrolling")
- }
- }
+ def encodeExpr(bindings: Map[Identifier, Expr])(e: Expr): Expr = {
+ replaceFromIDs(bindings, e)
}
- if(interrupted) {
- None
- } else {
- lastCheckResult._2
+ def substitute(substMap: Map[Expr, Expr]): Expr => Expr = {
+ (e: Expr) => replace(substMap, e)
}
+
+ def mkNot(e: Expr) = not(e)
+ def mkOr(es: Expr*) = orJoin(es)
+ def mkAnd(es: Expr*) = andJoin(es)
+ def mkEquals(l: Expr, r: Expr) = Equals(l, r)
+ def mkImplies(l: Expr, r: Expr) = implies(l, r)
+
+ def extractNot(e: Expr): Option[Expr] = e match {
+ case Not(b) => Some(b)
+ case _ => None
+ }
+ }
+
+ val solver = underlying
+
+ def assertCnstr(expression: Expr): Unit = {
+ assertCnstr(expression, variablesOf(expression).map(id => id -> id.toVariable).toMap)
+ }
+
+ def solverAssert(cnstr: Expr): Unit = {
+ solver.assertCnstr(cnstr)
+ }
+
+ def solverCheck[R](clauses: Seq[Expr])(block: Option[Boolean] => R): R = {
+ solver.push()
+ for (cls <- clauses) solver.assertCnstr(cls)
+ val res = solver.check
+ val r = block(res)
+ solver.pop()
+ r
+ }
+
+ def solverUnsatCore = None
+
+ def solverGetModel: ModelWrapper = new ModelWrapper {
+ val model = solver.getModel
+ def get(id: Identifier): Option[Expr] = model.get(id)
+ def eval(elem: Expr, tpe: TypeTree): Option[Expr] = evaluator.eval(elem, model).result
}
- def getModel: HenkinModel = {
- lastCheckResult match {
- case (true, Some(true), Some(m)) =>
- m.filter(freeVars.toSet)
- case _ =>
- HenkinModel.empty
+ override def dbg(msg: => Any) = underlying.dbg(msg)
+
+ override def push(): Unit = {
+ super.push()
+ solver.push()
+ }
+
+ override def pop(): Unit = {
+ super.pop()
+ solver.pop()
+ }
+
+ override def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
+ super.foundAnswer(res, model, core)
+
+ if (!interrupted && res == None && model == None) {
+ reporter.ifDebug { debug =>
+ debug("Unknown result!?")
+ }
}
}
- override def reset() = {
+ override def reset(): Unit = {
underlying.reset()
- lastCheckResult = (false, None, None)
- freeVars.reset()
- constraints.reset()
- interrupted = false
+ super.reset()
}
override def interrupt(): Unit = {
- interrupted = true
+ super.interrupt()
solver.interrupt()
}
override def recoverInterrupt(): Unit = {
solver.recoverInterrupt()
- interrupted = false
+ super.recoverInterrupt()
}
}
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index bc31267c09d8023390ac541b0cb99ecece6691ea..1662596002ac49202f10206cec6a338fc7377116 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -287,6 +287,16 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
def instantiations: Map[MatcherKey, Matchers] =
(funMap.toMap ++ tpeMap.map { case (tpe,ms) => TypeKey(tpe) -> ms }).mapValues(_.toMatchers)
+
+ def consume: Matchers = {
+ val matchers = funMap.iterator.flatMap(_._2.toMatchers).toSet ++ tpeMap.flatMap(_._2.toMatchers)
+ funMap.clear
+ tpeMap.clear
+ matchers
+ }
+
+ def isEmpty = funMap.isEmpty && tpeMap.isEmpty
+ def nonEmpty = !isEmpty
}
private class InstantiationContext private (
@@ -755,6 +765,16 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
instCtx.instantiate(Set(blocker), matcher)(quantifications.toSeq : _*)
}
+ def hasIgnored: Boolean = ignored.nonEmpty
+
+ def instantiateIgnored: Instantiation[T] = {
+ var instantiation = Instantiation.empty[T]
+ for ((b,m) <- ignored.consume) {
+ instantiation ++= instantiateMatcher(b, m)
+ }
+ instantiation
+ }
+
private type SetDef = (T, (Identifier, T), (Identifier, T), Seq[T], T, T, T)
private val setConstructors: MutableMap[TypeTree, SetDef] = MutableMap.empty
diff --git a/src/main/scala/leon/solvers/templates/TemplateEncoder.scala b/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
index f3eb2ad28f3bab2e72770f388e6ecbe92524dc54..16d7b3cdc7f695eb7524895fd880de4f23a1083c 100644
--- a/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
@@ -18,4 +18,6 @@ trait TemplateEncoder[T] {
def mkAnd(ts: T*): T
def mkEquals(l: T, r: T): T
def mkImplies(l: T, r: T): T
+
+ def extractNot(v: T): Option[T]
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 59be52775406a78c22a55773dfd161db003b21bb..2ab8f2b2b52dbf2cc335519e481ed7954e2fa3d6 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -65,7 +65,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val invocationEqualsBody : Option[Expr] = lambdaBody match {
case Some(body) if isRealFunDef =>
- val b : Expr = And(
+ val b : Expr = and(
liftedEquals(invocation, body, lambdaArguments),
Equals(invocation, body))
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 4543262d74204dd9f77d3eeea8882bf543956a90..893b39cb82e71bace9f4b26c2696188f825a031f 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -91,6 +91,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def refutationAssumptions = manager.assumptions
def canUnroll = callInfos.nonEmpty || appInfos.nonEmpty
+ def canInstantiate = manager.hasIgnored
def currentBlockers = callInfos.map(_._2._3).toSeq ++ appInfos.map(_._2._4).toSeq
@@ -218,9 +219,9 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def promoteBlocker(b: T) = {
if (callInfos contains b) {
- val (_, origGen, ast, fis) = callInfos(b)
+ val (_, origGen, notB, fis) = callInfos(b)
- callInfos += b -> (1, origGen, ast, fis)
+ callInfos += b -> (1, origGen, notB, fis)
}
if (blockerToApps contains b) {
@@ -231,6 +232,22 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
}
}
+ def instantiateQuantifiers: Seq[T] = {
+ val (newExprs, callBlocks, appBlocks) = manager.instantiateIgnored
+ val blockExprs = freshAppBlocks(appBlocks.keys)
+ val gen = (callInfos.values.map(_._1) ++ appInfos.values.map(_._1)).min
+
+ for ((b, newInfos) <- callBlocks) {
+ registerCallBlocker(nextGeneration(gen), b, newInfos)
+ }
+
+ for ((newApp, newInfos) <- appBlocks) {
+ registerAppBlocker(nextGeneration(gen), newApp, newInfos)
+ }
+
+ newExprs ++ blockExprs
+ }
+
def unrollBehind(ids: Seq[T]): Seq[T] = {
assert(ids.forall(id => (callInfos contains id) || (blockerToApps contains id)))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 7c3486ff533a630bbd1bce6bde31d86969163e7c..e2d1ab0fae778878845fa51f85786325a0041c54 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -30,7 +30,7 @@ trait AbstractZ3Solver extends Solver {
val library = program.library
- protected[z3] val reporter : Reporter = context.reporter
+ protected val reporter : Reporter = context.reporter
context.interruptManager.registerForInterrupts(this)
@@ -51,7 +51,7 @@ trait AbstractZ3Solver extends Solver {
protected[leon] val z3cfg : Z3Config
protected[leon] var z3 : Z3Context = null
- override def free() {
+ override def free(): Unit = {
freed = true
if (z3 ne null) {
z3.delete()
@@ -59,18 +59,13 @@ trait AbstractZ3Solver extends Solver {
}
}
- protected[z3] var interrupted = false
-
- override def interrupt() {
- interrupted = true
+ override def interrupt(): Unit = {
if(z3 ne null) {
z3.interrupt()
}
}
- override def recoverInterrupt() {
- interrupted = false
- }
+ override def recoverInterrupt(): Unit = ()
def functionDefToDecl(tfd: TypedFunDef): Z3FuncDecl = {
functions.cachedB(tfd) {
@@ -777,7 +772,7 @@ trait AbstractZ3Solver extends Solver {
z3.mkFreshConst(id.uniqueName, typeToSort(id.getType))
}
- def reset() = {
+ def reset(): Unit = {
throw new CantResetException(this)
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index c975fd2d37e7563137d9b1fd4cbe0f2cbb7892f4..812812aa3f4b39a9f3e2994d46080d4b009c0067 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -17,6 +17,7 @@ import purescala.ExprOps._
import purescala.Types._
import solvers.templates._
+import solvers.combinators._
import Template._
import evaluators._
@@ -25,32 +26,17 @@ import termination._
class FairZ3Solver(val context: LeonContext, val program: Program)
extends AbstractZ3Solver
- with Z3ModelReconstruction
- with FairZ3Component
- with EvaluatingSolver
- with QuantificationSolver {
+ with AbstractUnrollingSolver[Z3AST]
+ with Z3ModelReconstruction {
enclosing =>
- val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
- val checkModels = context.findOptionOrDefault(optCheckModels)
- val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
- val evalGroundApps = context.findOptionOrDefault(optEvalGround)
- val unrollUnsatCores = context.findOptionOrDefault(optUnrollCores)
- val assumePreHolds = context.findOptionOrDefault(optAssumePre)
- val disableChecks = context.findOptionOrDefault(optNoChecks)
-
- assert(!checkModels || !disableChecks, "Options \"checkmodels\" and \"nochecks\" are mutually exclusive")
-
protected val errors = new IncrementalBijection[Unit, Boolean]()
protected def hasError = errors.getB(()) contains true
protected def addError() = errors += () -> true
- protected[z3] def getEvaluator : Evaluator = evaluator
-
- private val terminator : TerminationChecker = new SimpleTerminationChecker(context, program)
-
- protected[z3] def getTerminator : TerminationChecker = terminator
+ override protected val reporter = context.reporter
+ override def reset(): Unit = super[AbstractZ3Solver].reset()
// FIXME: Dirty hack to bypass z3lib bug. Assumes context is the same over all instances of FairZ3Solver
protected[leon] val z3cfg = context.synchronized { new Z3Config(
@@ -60,53 +46,76 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
)}
toggleWarningMessages(true)
- private def extractModel(model: Z3Model, ids: Set[Identifier]): HenkinModel = {
- def extract(b: Z3AST, m: Matcher[Z3AST]): Set[Seq[Expr]] = {
- val QuantificationTypeMatcher(fromTypes, _) = m.tpe
- val optEnabler = model.evalAs[Boolean](b)
-
- if (optEnabler == Some(true)) {
- val optArgs = (m.args zip fromTypes).map {
- p => softFromZ3Formula(model, model.eval(p._1.encoded, true).get, p._2)
- }
-
- if (optArgs.forall(_.isDefined)) {
- Set(optArgs.map(_.get))
- } else {
- Set.empty
- }
- } else {
- Set.empty
- }
- }
+ def solverCheck[R](clauses: Seq[Z3AST])(block: Option[Boolean] => R): R = {
+ solver.push()
+ for (cls <- clauses) solver.assertCnstr(cls)
+ val res = solver.check
+ val r = block(res)
+ solver.pop()
+ r
+ }
- val (typeInsts, partialInsts, lambdaInsts) = templateGenerator.manager.instantiations
+ override def solverCheckAssumptions[R](assumptions: Seq[Z3AST])(block: Option[Boolean] => R): R = {
+ solver.push() // FIXME: remove when z3 bug is fixed
+ val res = solver.checkAssumptions(assumptions : _*)
+ solver.pop() // FIXME: remove when z3 bug is fixed
+ block(res)
+ }
- val typeDomains: Map[TypeTree, Set[Seq[Expr]]] = typeInsts.map {
- case (tpe, domain) => tpe -> domain.flatMap { case (b, m) => extract(b, m) }.toSet
+ def solverGetModel: ModelWrapper = new ModelWrapper {
+ val model = solver.getModel
+
+ /*
+ val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
+ val functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
+ if (functions containsB p._1) {
+ val tfd = functions.toA(p._1)
+ if (!tfd.hasImplementation) {
+ val (cses, default) = p._2
+ val ite = cses.foldLeft(fromZ3Formula(model, default, tfd.returnType))((expr, q) => IfExpr(
+ andJoin(q._1.zip(tfd.params).map(a12 => Equals(fromZ3Formula(model, a12._1, a12._2.getType), Variable(a12._2.id)))),
+ fromZ3Formula(model, q._2, tfd.returnType),
+ expr))
+ Seq((tfd.id, ite))
+ } else Seq()
+ } else Seq()
+ })
+
+ val constantFunctionsAsMap: Map[Identifier, Expr] = model.getModelConstantInterpretations.flatMap(p => {
+ if(functions containsB p._1) {
+ val tfd = functions.toA(p._1)
+ if(!tfd.hasImplementation) {
+ Seq((tfd.id, fromZ3Formula(model, p._2, tfd.returnType)))
+ } else Seq()
+ } else Seq()
+ }).toMap
+
+ val leonModel = extractModel(model, freeVars.toSet)
+ val fullModel = leonModel ++ (functionsAsMap ++ constantFunctionsAsMap)
+ */
+
+ def get(id: Identifier): Option[Expr] = variables.getB(id.toVariable).flatMap {
+ z3ID => eval(z3ID, id.getType)
}
- val funDomains: Map[Identifier, Set[Seq[Expr]]] = partialInsts.flatMap {
- case (c, domain) => variables.getA(c).collect {
- case Variable(id) => id -> domain.flatMap { case (b, m) => extract(b, m) }.toSet
+ def eval(elem: Z3AST, tpe: TypeTree): Option[Expr] = tpe match {
+ case BooleanType => model.evalAs[Boolean](elem).map(BooleanLiteral)
+ case Int32Type => model.evalAs[Int](elem).map(IntLiteral).orElse {
+ model.eval(elem).flatMap(t => softFromZ3Formula(model, t, Int32Type))
+ }
+ case IntegerType => model.evalAs[Int](elem).map(InfiniteIntegerLiteral(_))
+ case other => model.eval(elem) match {
+ case None => None
+ case Some(t) => softFromZ3Formula(model, t, other)
}
}
-
- val lambdaDomains: Map[Lambda, Set[Seq[Expr]]] = lambdaInsts.map {
- case (l, domain) => l -> domain.flatMap { case (b, m) => extract(b, m) }.toSet
- }
-
- val asMap = modelToMap(model, ids)
- val asDMap = purescala.Quantification.extractModel(asMap, funDomains, typeDomains, evaluator)
- val domains = new HenkinDomains(lambdaDomains, typeDomains)
- new HenkinModel(asDMap, domains)
}
- implicit val z3Printable = (z3: Z3AST) => new Printable {
+ val printable = (z3: Z3AST) => new Printable {
def asString(implicit ctx: LeonContext) = z3.toString
}
- val templateGenerator = new TemplateGenerator(new TemplateEncoder[Z3AST] {
+ val templateEncoder = new TemplateEncoder[Z3AST] {
def encodeId(id: Identifier): Z3AST = {
idToFreshZ3Id(id)
}
@@ -127,31 +136,33 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
def mkAnd(es: Z3AST*) = z3.mkAnd(es : _*)
def mkEquals(l: Z3AST, r: Z3AST) = z3.mkEq(l, r)
def mkImplies(l: Z3AST, r: Z3AST) = z3.mkImplies(l, r)
- }, assumePreHolds)
+ def extractNot(l: Z3AST): Option[Z3AST] = z3.getASTKind(l) match {
+ case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
+ case Z3DeclKind.OpNot => Some(args.head)
+ case Z3DeclKind.OpUninterpreted => None
+ }
+ case ast => None
+ }
+ }
initZ3()
val solver = z3.mkSolver()
- private val freeVars = new IncrementalSet[Identifier]()
- private val constraints = new IncrementalSeq[Expr]()
-
- val tr = implicitly[Z3AST => Printable]
-
- val unrollingBank = new UnrollingBank(context, templateGenerator)
-
private val incrementals: List[IncrementalState] = List(
- errors, freeVars, constraints, functions, generics, lambdas, sorts, variables,
- constructors, selectors, testers, unrollingBank
+ errors, functions, generics, lambdas, sorts, variables,
+ constructors, selectors, testers
)
- def push() {
+ override def push(): Unit = {
+ super.push()
solver.push()
incrementals.foreach(_.push())
}
- def pop() {
+ override def pop(): Unit = {
+ super.pop()
solver.pop(1)
incrementals.foreach(_.pop())
}
@@ -160,7 +171,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
if (hasError) {
None
} else {
- fairCheck(Set())
+ super.check
}
}
@@ -168,330 +179,43 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
if (hasError) {
None
} else {
- fairCheck(assumptions)
+ super.checkAssumptions(assumptions)
}
}
- var foundDefinitiveAnswer = false
- var definitiveAnswer : Option[Boolean] = None
- var definitiveModel : HenkinModel = HenkinModel.empty
- var definitiveCore : Set[Expr] = Set.empty
-
- def assertCnstr(expression: Expr) {
+ def assertCnstr(expression: Expr): Unit = {
try {
- val newFreeVars = variablesOf(expression)
- freeVars ++= newFreeVars
+ val bindings = variablesOf(expression).map(id => id -> variables.cachedB(Variable(id)) {
+ templateGenerator.encoder.encodeId(id)
+ }).toMap
- // We make sure all free variables are registered as variables
- freeVars.foreach { v =>
- variables.cachedB(Variable(v)) {
- templateGenerator.encoder.encodeId(v)
- }
- }
-
- constraints += expression
-
- val newClauses = unrollingBank.getClauses(expression, variables.aToB)
-
- for (cl <- newClauses) {
- solver.assertCnstr(cl)
- }
+ assertCnstr(expression, bindings)
} catch {
case _: Unsupported =>
addError()
}
}
- def getModel = {
- definitiveModel
- }
-
- def getUnsatCore = {
- definitiveCore
+ def solverAssert(cnstr: Z3AST): Unit = {
+ solver.assertCnstr(cnstr)
}
- def fairCheck(assumptions: Set[Expr]): Option[Boolean] = {
- foundDefinitiveAnswer = false
-
- def entireFormula = andJoin(assumptions.toSeq ++ constraints.toSeq)
-
- def foundAnswer(answer: Option[Boolean], model: HenkinModel = HenkinModel.empty, core: Set[Expr] = Set.empty) : Unit = {
- foundDefinitiveAnswer = true
- definitiveAnswer = answer
- definitiveModel = model
- definitiveCore = core
- }
-
- // these are the optional sequence of assumption literals
- val assumptionsAsZ3: Seq[Z3AST] = assumptions.map(toZ3Formula(_)).toSeq
- val assumptionsAsZ3Set: Set[Z3AST] = assumptionsAsZ3.toSet
-
- def z3CoreToCore(core: Seq[Z3AST]): Set[Expr] = {
- core.filter(assumptionsAsZ3Set).map(ast => fromZ3Formula(null, ast, BooleanType) match {
- case n @ Not(Variable(_)) => n
- case v @ Variable(_) => v
- case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
- }).toSet
- }
+ def solverUnsatCore = Some(solver.getUnsatCore)
- def validatedModel(silenceErrors: Boolean) : (Boolean, HenkinModel) = {
- if (interrupted) {
- (false, HenkinModel.empty)
- } else {
- val lastModel = solver.getModel
- val clauses = templateGenerator.manager.checkClauses
- val optModel = if (clauses.isEmpty) Some(lastModel) else {
- solver.push()
- for (clause <- clauses) {
- solver.assertCnstr(clause)
- }
-
- reporter.debug(" - Enforcing model transitivity")
- val timer = context.timers.solvers.z3.check.start()
- solver.push() // FIXME: remove when z3 bug is fixed
- val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.satisfactionAssumptions) :_*)
- solver.pop() // FIXME: remove when z3 bug is fixed
- timer.stop()
-
- val solverModel = res match {
- case Some(true) =>
- Some(solver.getModel)
-
- case Some(false) =>
- val msg = "- Transitivity independence not guaranteed for model"
- if (silenceErrors) {
- reporter.debug(msg)
- } else {
- reporter.warning(msg)
- }
- None
-
- case None =>
- val msg = "- Unknown for transitivity independence!?"
- if (silenceErrors) {
- reporter.debug(msg)
- } else {
- reporter.warning(msg)
- }
- None
- }
-
- solver.pop()
- solverModel
- }
+ override def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
+ super.foundAnswer(res, model, core)
- val model = optModel getOrElse lastModel
-
- val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
- val functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
- if (functions containsB p._1) {
- val tfd = functions.toA(p._1)
- if (!tfd.hasImplementation) {
- val (cses, default) = p._2
- val ite = cses.foldLeft(fromZ3Formula(model, default, tfd.returnType))((expr, q) => IfExpr(
- andJoin(
- q._1.zip(tfd.params).map(a12 => Equals(fromZ3Formula(model, a12._1, a12._2.getType), Variable(a12._2.id)))
- ),
- fromZ3Formula(model, q._2, tfd.returnType),
- expr))
- Seq((tfd.id, ite))
- } else Seq()
- } else Seq()
- })
-
- val constantFunctionsAsMap: Map[Identifier, Expr] = model.getModelConstantInterpretations.flatMap(p => {
- if(functions containsB p._1) {
- val tfd = functions.toA(p._1)
- if(!tfd.hasImplementation) {
- Seq((tfd.id, fromZ3Formula(model, p._2, tfd.returnType)))
- } else Seq()
- } else Seq()
- }).toMap
-
- val leonModel = extractModel(model, freeVars.toSet)
- val fullModel = leonModel ++ (functionsAsMap ++ constantFunctionsAsMap)
-
- if (!optModel.isDefined) {
- (false, leonModel)
- } else {
- (evaluator.check(entireFormula, fullModel) match {
- case EvaluationResults.CheckSuccess =>
- reporter.debug("- Model validated.")
- true
-
- case EvaluationResults.CheckValidityFailure =>
- reporter.debug("- Invalid model.")
- false
-
- case EvaluationResults.CheckRuntimeFailure(msg) =>
- if (silenceErrors) {
- reporter.debug("- Model leads to evaluation error: " + msg)
- } else {
- reporter.warning("- Model leads to evaluation error: " + msg)
- }
- false
-
- case EvaluationResults.CheckQuantificationFailure(msg) =>
- if (silenceErrors) {
- reporter.debug("- Model leads to quantification error: " + msg)
- } else {
- reporter.warning("- Model leads to quantification error: " + msg)
- }
- false
- }, leonModel)
+ if (!interrupted && res == None && model == None) {
+ reporter.ifDebug { debug =>
+ if (solver.getReasonUnknown != "canceled") {
+ debug("Z3 returned unknown: " + solver.getReasonUnknown)
}
}
}
+ }
- while(!foundDefinitiveAnswer && !interrupted) {
-
- //val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get)
- // println("Blocking set : " + blockingSet)
-
- reporter.debug(" - Running Z3 search...")
-
- //reporter.debug("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
- //reporter.debug("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
- //reporter.debug("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
-
- val timer = context.timers.solvers.z3.check.start()
- solver.push() // FIXME: remove when z3 bug is fixed
- val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.satisfactionAssumptions) :_*)
- solver.pop() // FIXME: remove when z3 bug is fixed
- timer.stop()
-
- reporter.debug(" - Finished search with blocked literals")
-
- lazy val allVars: Set[Identifier] = freeVars.toSet
-
- res match {
- case None =>
- reporter.ifDebug { debug =>
- if (solver.getReasonUnknown != "canceled") {
- debug("Z3 returned unknown: " + solver.getReasonUnknown)
- }
- }
- foundAnswer(None)
-
- case Some(true) => // SAT
- val (valid, model) = if (!this.disableChecks && (this.checkModels || requireQuantification)) {
- validatedModel(false)
- } else {
- true -> extractModel(solver.getModel, allVars)
- }
-
- if (valid) {
- foundAnswer(Some(true), model)
- } else {
- reporter.error("Something went wrong. The model should have been valid, yet we got this : ")
- reporter.error(model.asString(context))
- foundAnswer(None, model)
- }
-
- case Some(false) if !unrollingBank.canUnroll =>
-
- val core = z3CoreToCore(solver.getUnsatCore())
-
- foundAnswer(Some(false), core = core)
-
- // This branch is both for with and without unsat cores. The
- // distinction is made inside.
- case Some(false) =>
-
- def coreElemToBlocker(c: Z3AST): (Z3AST, Boolean) = {
- z3.getASTKind(c) match {
- case Z3AppAST(decl, args) =>
- z3.getDeclKind(decl) match {
- case Z3DeclKind.OpNot =>
- (args.head, true)
- case Z3DeclKind.OpUninterpreted =>
- (c, false)
- }
-
- case ast =>
- (c, false)
- }
- }
-
- if (unrollUnsatCores) {
- unrollingBank.decreaseAllGenerations()
-
- for (c <- solver.getUnsatCore()) {
- val (z3ast, pol) = coreElemToBlocker(c)
- assert(pol)
-
- unrollingBank.promoteBlocker(z3ast)
- }
-
- }
-
- //debug("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
- //debug("UNSAT BECAUSE: "+core.mkString(" AND "))
-
- if (!interrupted) {
- if (this.feelingLucky) {
- // we need the model to perform the additional test
- reporter.debug(" - Running search without blocked literals (w/ lucky test)")
- } else {
- reporter.debug(" - Running search without blocked literals (w/o lucky test)")
- }
-
- val timer = context.timers.solvers.z3.check.start()
- solver.push() // FIXME: remove when z3 bug is fixed
- val res2 = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.refutationAssumptions) : _*)
- solver.pop() // FIXME: remove when z3 bug is fixed
- timer.stop()
-
- reporter.debug(" - Finished search without blocked literals")
-
- res2 match {
- case Some(false) =>
- //reporter.debug("UNSAT WITHOUT Blockers")
- foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
- case Some(true) =>
- //reporter.debug("SAT WITHOUT Blockers")
- if (this.feelingLucky && !interrupted) {
- // we might have been lucky :D
- val (wereWeLucky, cleanModel) = validatedModel(true)
-
- if(wereWeLucky) {
- foundAnswer(Some(true), cleanModel)
- }
- }
-
- case None =>
- foundAnswer(None)
- }
- }
-
- if(interrupted) {
- foundAnswer(None)
- }
-
- if(!foundDefinitiveAnswer) {
- reporter.debug("- We need to keep going.")
-
- val toRelease = unrollingBank.getBlockersToUnlock
-
- reporter.debug(" - more unrollings")
-
- val newClauses = unrollingBank.unrollBehind(toRelease)
-
- for(ncl <- newClauses) {
- solver.assertCnstr(ncl)
- }
-
- //readLine()
-
- reporter.debug(" - finished unrolling")
- }
- }
- }
-
- if(interrupted) {
- None
- } else {
- definitiveAnswer
- }
+ override def interrupt(): Unit = {
+ super[AbstractZ3Solver].interrupt()
+ super[AbstractUnrollingSolver].interrupt()
}
}