Skip to content
Snippets Groups Projects
Commit e889aae3 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Simplify FairZ3Solver, remove old API

parent aaed71ab
No related branches found
No related tags found
No related merge requests found
...@@ -24,10 +24,9 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder { ...@@ -24,10 +24,9 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t) class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t)
protected[leon] val z3cfg : Z3Config
protected[leon] var z3 : Z3Context = null protected[leon] var z3 : Z3Context = null
protected[leon] var solver : Z3Solver = null
protected[leon] var program : Program = null protected[leon] var program : Program = null
protected[leon] val z3cfg : Z3Config
override def setProgram(prog: Program): Unit = { override def setProgram(prog: Program): Unit = {
program = prog program = prog
...@@ -86,7 +85,6 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder { ...@@ -86,7 +85,6 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
private var neverInitialized = true
private var counter = 0 private var counter = 0
private object nextIntForSymbol { private object nextIntForSymbol {
def apply(): Int = { def apply(): Int = {
...@@ -96,18 +94,22 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder { ...@@ -96,18 +94,22 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
} }
} }
var isInitialized = false
protected[leon] def initZ3() {
if (!isInitialized) {
counter = 0
protected[leon] def restartZ3 : Unit = {
counter = 0
if (neverInitialized) {
neverInitialized = false
z3 = new Z3Context(z3cfg) z3 = new Z3Context(z3cfg)
solver = z3.mkSolver
prepareSorts prepareSorts
prepareFunctions prepareFunctions
} else {
solver = z3.mkSolver isInitialized = true
} }
}
protected[leon] def restartZ3() {
isInitialized = false
initZ3()
exprToZ3Id = Map.empty exprToZ3Id = Map.empty
z3IdToExpr = Map.empty z3IdToExpr = Map.empty
......
...@@ -34,20 +34,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ ...@@ -34,20 +34,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
) )
toggleWarningMessages(true) toggleWarningMessages(true)
private var unrollingBank: UnrollingBank = null
private var blockingSet: Set[Expr] = Set.empty
private var toCheckAgainstModels: Expr = BooleanLiteral(true)
private var varsInVC: Set[Identifier] = Set.empty
override def restartZ3 : Unit = {
super.restartZ3
unrollingBank = new UnrollingBank
blockingSet = Set.empty
toCheckAgainstModels = BooleanLiteral(true)
varsInVC = Set.empty
}
def isKnownDef(funDef: FunDef) : Boolean = functionMap.isDefinedAt(funDef) def isKnownDef(funDef: FunDef) : Boolean = functionMap.isDefinedAt(funDef)
def functionDefToDecl(funDef: FunDef) : Z3FuncDecl = def functionDefToDecl(funDef: FunDef) : Z3FuncDecl =
...@@ -73,19 +59,9 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ ...@@ -73,19 +59,9 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
functionMap = functionMap + (funDef -> z3Decl) functionMap = functionMap + (funDef -> z3Decl)
reverseFunctionMap = reverseFunctionMap + (z3Decl -> funDef) reverseFunctionMap = reverseFunctionMap + (z3Decl -> funDef)
} }
if(!Settings.noForallAxioms) {
prepareAxioms
}
for(funDef <- program.definedFunctions) {
if (funDef.annotations.contains("axiomatize") && !axiomatizedFunctions(funDef)) {
reporter.warning("Function " + funDef.id + " was marked for axiomatization but could not be handled.")
}
}
} }
private def prepareAxioms : Unit = { private def prepareAxioms(solver: Z3Solver): Unit = {
assert(!Settings.noForallAxioms) assert(!Settings.noForallAxioms)
program.definedFunctions.foreach(_ match { program.definedFunctions.foreach(_ match {
case fd @ Catamorphism(acd, cases) => { case fd @ Catamorphism(acd, cases) => {
...@@ -138,358 +114,29 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ ...@@ -138,358 +114,29 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
}) })
} }
override def solve(vc: Expr) = decide(vc, true) override def solve(vc: Expr) = {
val solver = getNewSolver
override def solveSAT(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = { solver.assertCnstr(Not(vc))
restartZ3 solver.check.map(!_)
val (res, model, core) = decideWithModel(vc, false)
(res, model)
} }
def decide(vc: Expr, forValidity: Boolean):Option[Boolean] = { override def solveSAT(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
restartZ3 val solver = getNewSolver
decideWithModel(vc, forValidity)._1 solver.assertCnstr(vc)
(solver.check, solver.getModel)
} }
private var foundDefinitiveAnswer : Boolean = false
override def halt() { override def halt() {
if(!foundDefinitiveAnswer) { super.halt
super.halt if(z3 ne null) {
if(z3 != null) z3.softCheckCancel
z3.softCheckCancel
} }
} }
override def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = { override def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
restartZ3 val solver = getNewSolver
decideWithModel(expression, false, None, Some(assumptions)) solver.assertCnstr(expression)
} (solver.checkAssumptions(assumptions), solver.getModel, solver.getUnsatCore)
private[this] def decideWithModel(vc: Expr, forValidity: Boolean, evaluator: Option[(Map[Identifier,Expr]) => Boolean] = None, assumptions: Option[Set[Expr]] = None): (Option[Boolean], Map[Identifier,Expr], Set[Expr]) = {
val initializationStopwatch = new Stopwatch("init", false)
val blocking2Z3Stopwatch = new Stopwatch("blocking-set-to-z3", false)
val z3SearchStopwatch = new Stopwatch("z3-search-1", false)
val secondZ3SearchStopwatch = new Stopwatch("z3-search-2", false)
val unrollingStopwatch = new Stopwatch("unrolling", false)
val luckyStopwatch = new Stopwatch("lucky", false)
val validatingStopwatch = new Stopwatch("validating", false)
val decideTopLevelSw = new Stopwatch("top-level", false).start
// println("Deciding : " + vc)
assumptions match {
case Some(set) => {
if (Settings.useCores)
throw new Exception("Use of cores while checking assumptions is not supported")
if (set.exists(e => e match {
case Variable(_) => false
case Not(Variable(_)) => false
case _ => true
}))
throw new Exception("assumptions may only be boolean literals")
}
case None =>
}
initializationStopwatch.start
foundDefinitiveAnswer = false
var definitiveAnswer : Option[Boolean] = None
var definitiveModel : Map[Identifier,Expr] = Map.empty
var definitiveCore : Set[Expr] = Set.empty
def foundAnswer(answer : Option[Boolean], model : Map[Identifier,Expr] = Map.empty, core: Set[Expr] = Set.empty) : Unit = {
foundDefinitiveAnswer = true
definitiveAnswer = answer
definitiveModel = model
definitiveCore = core
//timer.foreach(t => t.halt)
}
if (program == null) {
reporter.error("Z3 Solver was not initialized with a PureScala Program.")
None
}
// naive implementation of unrolling everything every n-th iteration
val unrollingThreshold = 100
var unrollingCounter = 0
val expandedVC = expandLets(if (forValidity) negate(vc) else vc)
toCheckAgainstModels = And(toCheckAgainstModels,expandedVC)
varsInVC ++= variablesOf(expandedVC)
reporter.info(" - Initial unrolling...")
val (clauses, guards) = unrollingBank.scanForNewTemplates(expandedVC)
val cc = toZ3Formula(And(clauses)).get
solver.assertCnstr(cc)
// these are the optional sequence of assumption literals
val assumptionsAsZ3: Option[Seq[Z3AST]] = assumptions.map(set => set.toSeq.map(toZ3Formula(_).get))
blockingSet ++= Set(guards.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
var iterationsLeft : Int = if(Settings.unrollingLevel > 0) Settings.unrollingLevel else 16121984
initializationStopwatch.stop
while(!foundDefinitiveAnswer && !forceStop) {
iterationsLeft -= 1
blocking2Z3Stopwatch.start
val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get)
// println("Blocking set : " + blockingSet)
blocking2Z3Stopwatch.stop
solver.push
if(!blockingSetAsZ3.isEmpty)
solver.assertCnstr(z3.mkAnd(blockingSetAsZ3 : _*))
reporter.info(" - Running Z3 search...")
val answerModelCore : (Option[Boolean], Z3Model, Set[Expr]) = {
z3SearchStopwatch.start
val res = assumptionsAsZ3 match {
case Some(as) => solver.checkAssumptions(as: _*)
case None => solver.check()
}
val z3model = res match {
case Some(true) => solver.getModel
case _ => null
}
val z3core: Seq[Z3AST] = (res, assumptionsAsZ3) match {
case (Some(false), ass) if ass.isDefined => solver.getUnsatCore.toSeq
case _ => Seq()
}
z3SearchStopwatch.stop
val core: Set[Expr] = z3core.map(ast => fromZ3Formula(z3model, ast, Some(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
(res, z3model, core)
}
val (answer, model, core) = answerModelCore // to work around the stupid type inferer
reporter.info(" - Finished search with blocked literals")
// if (Settings.useCores)
// reporter.info(" - Core is : " + core)
val reinterpretedAnswer = if(!UNKNOWNASSAT) answer else (answer match {
case None | Some(true) => Some(true)
case Some(false) => Some(false)
})
(reinterpretedAnswer, model) match {
case (None, m) => { // UNKNOWN
// reporter.warning("Z3 doesn't know because: " + z3.getSearchFailure.message)
reporter.warning("Z3 doesn't know because ??")
foundAnswer(None)
}
case (Some(true), m) => { // SAT
validatingStopwatch.start
val (trueModel, model) = if(Settings.verifyModel)
validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
else {
val res = (true, modelToMap(m, varsInVC))
lazy val modelAsString = res._2.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
reporter.info("- Found a model:")
reporter.info(modelAsString)
res
}
validatingStopwatch.stop
if (trueModel) {
foundAnswer(Some(false), model)
} else {
reporter.error("Something went wrong. The model should have been valid, yet we got this : ")
reporter.error(model)
foundAnswer(None, model)
}
}
case (Some(false), m) if blockingSet.isEmpty => {
foundAnswer(Some(true), core = core)
solver.pop(1)
}
// This branch is both for with and without unsat cores. The
// distinction is made inside.
case (Some(false), m) => {
solver.pop(1)
if (Settings.luckyTest && !forceStop) {
// we need the model to perform the additional test
reporter.info(" - Running search without blocked literals (w/ lucky test)")
secondZ3SearchStopwatch.start
val res2 = assumptionsAsZ3 match {
case Some(as) => solver.checkAssumptions(as: _*)
case None => solver.check()
}
val z3model2 = res2 match {
case Some(true) => solver.getModel
case _ => null
}
val z3core2: Seq[Z3AST] = (res2, assumptionsAsZ3) match {
case (Some(false), ass) if ass.isDefined => solver.getUnsatCore.toSeq
case _ => Seq()
}
secondZ3SearchStopwatch.stop
reporter.info(" - Finished search without blocked literals")
if (res2 == Some(false)) {
val core2: Set[Expr] = z3core2.map(ast => fromZ3Formula(z3model2, ast, Some(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
foundAnswer(Some(true), core = core2)
} else {
luckyStopwatch.start
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(z3model2, toCheckAgainstModels, varsInVC, evaluator)
if(wereWeLucky) {
foundAnswer(Some(false), cleanModel)
}
luckyStopwatch.stop
}
} else {
// only checking will suffice
reporter.info(" - Running search without blocked literals (w/o lucky test)")
secondZ3SearchStopwatch.start
val result2 = assumptionsAsZ3 match {
case Some(as) => solver.checkAssumptions(as: _*)
case None => solver.check()
}
secondZ3SearchStopwatch.stop
reporter.info(" - Finished search without blocked literals")
if (result2 == Some(false)) {
val z3model = solver.getModel()
val core: Set[Expr] = solver.getUnsatCore.map(ast => fromZ3Formula(z3model, ast, Some(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
foundAnswer(Some(true), core = core)
}
}
if(forceStop) {
foundAnswer(None)
}
if(!foundDefinitiveAnswer) {
reporter.info("- We need to keep going.")
unrollingStopwatch.start
val toRelease : Set[Expr] = blockingSet
// reporter.info(" - toRelease : " + toRelease)
// reporter.info(" - blockingSet : " + blockingSet)
var fixedForEver : Set[Expr] = Set.empty
if(Settings.pruneBranches) {
for(ex <- blockingSet) ex match {
case Not(Variable(b)) => {
solver.push
solver.assertCnstr(toZ3Formula(Variable(b)).get)
solver.check match {
case Some(false) => {
//println("We had ~" + b + " in the blocking set. We now know it should stay there forever.")
solver.pop(1)
solver.assertCnstr(toZ3Formula(Not(Variable(b))).get)
fixedForEver = fixedForEver + ex
}
case _ => solver.pop(1)
}
}
case Variable(b) => {
solver.push
solver.assertCnstr(toZ3Formula(Not(Variable(b))).get)
solver.check match {
case Some(false) => {
//println("We had " + b + " in the blocking set. We now know it should stay there forever.")
solver.pop(1)
solver.assertCnstr(toZ3Formula(Variable(b)).get)
fixedForEver = fixedForEver + ex
}
case _ => solver.pop(1)
}
}
case _ => scala.sys.error("Should not have happened.")
}
if(fixedForEver.size > 0) {
reporter.info("- Pruned out " + fixedForEver.size + " branches.")
}
}
blockingSet = blockingSet -- toRelease
val toReleaseAsPairs : Set[(Identifier,Boolean)] = (toRelease -- fixedForEver).map(b => b match {
case Variable(id) => (id, true)
case Not(Variable(id)) => (id, false)
case _ => scala.sys.error("Impossible value in release set: " + b)
})
reporter.info(" - more unrollings")
for((id,polarity) <- toReleaseAsPairs) {
val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity)
for(ncl <- newClauses) {
solver.assertCnstr(toZ3Formula(ncl).get)
}
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
reporter.info(" - finished unrolling")
unrollingStopwatch.stop
}
}
}
if(iterationsLeft <= 0) {
reporter.error(" - Max. number of iterations reached.")
foundAnswer(None)
}
}
decideTopLevelSw.stop
decideTopLevelSw.writeToSummary
initializationStopwatch.writeToSummary
blocking2Z3Stopwatch.writeToSummary
z3SearchStopwatch.writeToSummary
secondZ3SearchStopwatch.writeToSummary
unrollingStopwatch.writeToSummary
luckyStopwatch.writeToSummary
validatingStopwatch.writeToSummary
if(forceStop) {
(None, Map.empty, Set.empty)
} else {
val realAnswer = if(forValidity) {
definitiveAnswer
} else {
definitiveAnswer.map(!_)
}
(realAnswer, definitiveModel, definitiveCore)
}
} }
private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier], evaluator: Option[(Map[Identifier,Expr])=>Boolean] = None) : (Boolean, Map[Identifier,Expr]) = { private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier], evaluator: Option[(Map[Identifier,Expr])=>Boolean] = None) : (Boolean, Map[Identifier,Expr]) = {
...@@ -622,8 +269,22 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ ...@@ -622,8 +269,22 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
} }
def getNewSolver = new solvers.IncrementalSolver { def getNewSolver = new solvers.IncrementalSolver {
initZ3
val solver = z3.mkSolver val solver = z3.mkSolver
if(!Settings.noForallAxioms) {
prepareAxioms(solver)
}
for(funDef <- program.definedFunctions) {
if (funDef.annotations.contains("axiomatize") && !axiomatizedFunctions(funDef)) {
reporter.warning("Function " + funDef.id + " was marked for axiomatization but could not be handled.")
}
}
private var frameGuards = List[Z3AST](z3.mkFreshConst("frame", z3.mkBoolSort)) private var frameGuards = List[Z3AST](z3.mkFreshConst("frame", z3.mkBoolSort))
private var frameExpressions = List[List[Expr]](Nil) private var frameExpressions = List[List[Expr]](Nil)
private var varsInVC = Set[Identifier]() private var varsInVC = Set[Identifier]()
...@@ -669,8 +330,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ ...@@ -669,8 +330,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
frameExpressions = (expression :: frameExpressions.head) :: frameExpressions.tail frameExpressions = (expression :: frameExpressions.head) :: frameExpressions.tail
solver.assertCnstr(z3.mkImplies(guard, toZ3Formula(expression).get))
val (newClauses, newGuards) = unrollingBank.scanForNewTemplates(expression) val (newClauses, newGuards) = unrollingBank.scanForNewTemplates(expression)
for (cl <- newClauses) { for (cl <- newClauses) {
......
...@@ -54,34 +54,32 @@ class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with ...@@ -54,34 +54,32 @@ class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with
// Where the solving occurs // Where the solving occurs
override def solveSAT(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = { override def solveSAT(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
restartZ3 val solver = getNewSolver
val emptyModel = Map.empty[Identifier,Expr] val emptyModel = Map.empty[Identifier,Expr]
val unknownResult = (None, emptyModel) val unknownResult = (None, emptyModel)
val unsatResult = (Some(false), emptyModel) val unsatResult = (Some(false), emptyModel)
val result = toZ3Formula(expression).map { asZ3 => solver.assertCnstr(expression)
solver.assertCnstr(asZ3)
solver.check match { val result = solver.check match {
case Some(false) => unsatResult case Some(false) => unsatResult
case Some(true) => { case Some(true) => {
val model = solver.getModel if(containsFunctionCalls(expression)) {
unknownResult
if(containsFunctionCalls(expression)) { } else {
unknownResult (Some(true), solver.getModel)
} else {
val variables = variablesOf(expression)
(Some(true), modelToMap(model, variables))
}
} }
case _ => unknownResult
} }
} getOrElse unknownResult case _ => unknownResult
}
result result
} }
def getNewSolver = new solvers.IncrementalSolver { def getNewSolver = new solvers.IncrementalSolver {
initZ3
val solver = z3.mkSolver val solver = z3.mkSolver
def push() { def push() {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment