diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index b3e8df10c058e4ef4e1d70067fc44af26e7c121f..0a53b4c908ee4a5b3b7d58654fcb9351e15f7cb8 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -413,7 +413,8 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
val rl = rec(l)
val rr = rec(r)
// z3.mkIff used to trigger a bug
- z3.mkAnd(z3.mkImplies(rl, rr), z3.mkImplies(rr, rl))
+ // z3.mkAnd(z3.mkImplies(rl, rr), z3.mkImplies(rr, rl))
+ z3.mkIff(rl, rr)
}
case Not(Iff(l, r)) => z3.mkXor(rec(l), rec(r))
case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r))
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 63da5306845402b6ff2ba05a5529a863c1da1bf2..3258128f8774807ac1bc7d4980a1350c85e08f0b 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -14,6 +14,8 @@ import purescala.TypeTrees._
import evaluators._
+import termination._
+
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
@@ -37,13 +39,12 @@ class FairZ3Solver(context : LeonContext)
)
// What wouldn't we do to avoid defining vars?
- val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores, pruneUnsatCores) = locally {
+ val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores) = locally {
var lucky = false
var check = false
var codegen = false
var evalground = false
var unrollUnsatCores = false
- var pruneUnsatCores = true
for(opt <- context.options) opt match {
case LeonFlagOption("checkmodels") => check = true
@@ -54,12 +55,15 @@ class FairZ3Solver(context : LeonContext)
case _ =>
}
- (lucky, check, codegen, evalground, unrollUnsatCores, pruneUnsatCores)
+ (lucky, check, codegen, evalground, unrollUnsatCores)
}
private var evaluator : Evaluator = null
protected[z3] def getEvaluator : Evaluator = evaluator
+ private var terminator : TerminationChecker = null
+ protected[z3] def getTerminator : TerminationChecker = terminator
+
override def setProgram(prog : Program) {
super.setProgram(prog)
@@ -70,6 +74,8 @@ class FairZ3Solver(context : LeonContext)
} else {
new DefaultEvaluator(context, prog)
}
+
+ terminator = new SimpleTerminationChecker(context, prog)
}
// This is fixed.
@@ -211,10 +217,10 @@ class FairZ3Solver(context : LeonContext)
}
class UnrollingBank {
- // Keep which function invocation is guarded by which guard with polarity,
- // also specify the generation of the blocker
+ // Keep which function invocation is guarded by which guard,
+ // also specify the generation of the blocker.
- private var blockersInfoStack : List[MutableMap[(Z3AST,Boolean), (Int, Int, Z3AST, Set[Z3FunctionInvocation])]] = List(MutableMap())
+ private var blockersInfoStack : List[MutableMap[Z3AST,(Int,Int,Z3AST,Set[Z3FunctionInvocation])]] = List(MutableMap())
def blockersInfo = blockersInfoStack.head
@@ -232,15 +238,15 @@ class FairZ3Solver(context : LeonContext)
blockersInfo.groupBy(_._2._1).toSeq.sortBy(_._1).foreach { case (gen, entries) =>
reporter.info("--- "+gen)
- for (((bast, bpol), (gen, origGen, ast, fis)) <- entries) {
- reporter.info(". "+(if(!bpol) "¬" else "")+bast +" ~> "+fis.map(_.funDef.id))
+ for (((bast), (gen, origGen, ast, fis)) <- entries) {
+ reporter.info(". "+bast +" ~> "+fis.map(_.funDef.id))
}
}
}
def canUnroll = !blockersInfo.isEmpty
- def getZ3BlockersToUnlock: Seq[(Z3AST, Boolean)] = {
+ def getZ3BlockersToUnlock: Seq[Z3AST] = {
if (!blockersInfo.isEmpty) {
val minGeneration = blockersInfo.values.map(_._1).min
@@ -250,22 +256,22 @@ class FairZ3Solver(context : LeonContext)
}
}
- private def registerBlocker(gen: Int, id: Z3AST, pol: Boolean, fis: Set[Z3FunctionInvocation]) {
- val pair = (id, pol)
-
- val z3ast = if (pol) z3.mkNot(id) else id
-
- blockersInfo.get(pair) match {
+ private def registerBlocker(gen: Int, id: Z3AST, fis: Set[Z3FunctionInvocation]) {
+ val z3ast = z3.mkNot(id)
+ blockersInfo.get(id) match {
case Some((exGen, origGen, _, exFis)) =>
- assert(exGen == gen, "Mixing the same pair "+pair+" with various generations "+ exGen+" and "+gen)
+ assert(exGen == gen, "Mixing the same id "+id+" with various generations "+ exGen+" and "+gen)
- blockersInfo(pair) = ((gen, origGen, z3ast, fis++exFis))
+ blockersInfo(id) = ((gen, origGen, z3ast, fis++exFis))
case None =>
- blockersInfo(pair) = ((gen, gen, z3ast, fis))
+ blockersInfo(id) = ((gen, gen, z3ast, fis))
}
}
def scanForNewTemplates(expr: Expr): Seq[Z3AST] = {
+ // OK, now this is subtle. This `getTemplate` will return
+ // a template for a "fake" function. Now, this template will
+ // define an activating boolean...
val template = getTemplate(expr)
val z3args = for (vd <- template.funDef.args) yield {
@@ -280,15 +286,18 @@ class FairZ3Solver(context : LeonContext)
}
}
- val (newClauses, newBlocks) = template.instantiate(template.z3ActivatingBool, true, z3args)
+ // ...now this template defines clauses that are all guarded
+ // by that activating boolean. If that activating boolean is
+ // undefined (or false) these clauses have no effect...
+ val (newClauses, newBlocks) =
+ template.instantiate(template.z3ActivatingBool, z3args)
- val extraClauses = for(((i, p), fis) <- newBlocks) yield {
- registerBlocker(nextGeneration(0), i, p, fis)
- //unlock(i, p)
- Nil
+ for((i, fis) <- newBlocks) {
+ registerBlocker(nextGeneration(0), i, fis)
}
-
- newClauses ++ extraClauses.flatten
+
+ // ...so we must force it to true!
+ template.z3ActivatingBool +: newClauses
}
def nextGeneration(gen: Int) = gen + 3
@@ -300,35 +309,31 @@ class FairZ3Solver(context : LeonContext)
}
}
- def prune(ast: Z3AST, pol: Boolean) = {
- val b = (ast, pol)
- blockersInfo -= b
- }
-
- def promoteBlocker(bast: Z3AST, pol: Boolean) = {
- val b = (bast, pol)
+ def promoteBlocker(b: Z3AST) = {
if (blockersInfo contains b) {
val (gen, origGen, ast, finvs) = blockersInfo(b)
blockersInfo(b) = (1, origGen, ast, finvs)
}
}
- def unlock(id: Z3AST, pol: Boolean) : Seq[Z3AST] = {
- val pair = (id, pol)
- assert(blockersInfo contains pair)
+ def unlock(id: Z3AST) : Seq[Z3AST] = {
+ assert(blockersInfo contains id)
- val (gen, origGen, _, fis) = blockersInfo(pair)
- blockersInfo -= pair
+ val (gen, origGen, _, fis) = blockersInfo(id)
+ blockersInfo -= id
var newClauses : Seq[Z3AST] = Seq.empty
for(fi <- fis) {
val template = getTemplate(fi.funDef)
- val (newExprs, newBlocks) = template.instantiate(id, pol, fi.args)
+ val (newExprs, newBlocks) = template.instantiate(id, fi.args)
- for(((i, p), fis) <- newBlocks) {
- // We use origGen here
- registerBlocker(nextGeneration(origGen), i, p, fis)
+ // println("In unlock :")
+ // println("CLAUSES")
+ // newExprs.foreach(println)
+
+ for((i, fis) <- newBlocks) {
+ registerBlocker(nextGeneration(gen), i, fis)
}
newClauses ++= newExprs
@@ -440,7 +445,6 @@ class FairZ3Solver(context : LeonContext)
}).toSet
}
-
while(!foundDefinitiveAnswer && !forceStop) {
//val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get)
@@ -524,24 +528,13 @@ class FairZ3Solver(context : LeonContext)
for (c <- solver.getUnsatCore) {
val (z3ast, pol) = coreElemToBlocker(c)
+ assert(pol == true)
- unrollingBank.promoteBlocker(z3ast, pol)
+ unrollingBank.promoteBlocker(z3ast)
}
}
- if (pruneUnsatCores) {
- z3Core.toSeq match {
- case Seq(c) =>
- // If there is only one element in the Seq, we can prune
- val (z3ast, pol) = coreElemToBlocker(c)
-
- unrollingBank.prune(z3ast, !pol)
- solver.assertCnstr(if (pol) z3ast else z3.mkNot(z3ast))
- case _ =>
- }
- }
-
reporter.info("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
//reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
@@ -593,16 +586,10 @@ class FairZ3Solver(context : LeonContext)
reporter.info(" - more unrollings")
- unrollingBank.dumpBlockers
-
- for((id, polarity) <- toReleaseAsPairs) {
+ for(id <- toReleaseAsPairs) {
unlockingTime.start
- val newClauses = unrollingBank.unlock(id, polarity)
+ val newClauses = unrollingBank.unlock(id)
unlockingTime.stop
- reporter.info(" - - Unrolling behind "+(if(!polarity) "¬" else "")+id)
- //for (cl <- newClauses) {
- // reporter.info(" - - - "+cl)
- //}
unrollingTime.start
for(ncl <- newClauses) {
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index da4de64711a03fc1a8c068263b673ba81232c37a..f4e3724c45d6d26d6d41475ca18694cf0d1fb209 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -22,14 +22,24 @@ class FunctionTemplate private(
activatingBool : Identifier,
condVars : Set[Identifier],
exprVars : Set[Identifier],
- guardedExprs : Map[(Identifier,Boolean),Seq[Expr]],
+ guardedExprs : Map[Identifier,Seq[Expr]],
isRealFunDef : Boolean) {
+ private val isTerminatingForAllInputs : Boolean = (
+ isRealFunDef
+ && !funDef.hasPrecondition
+ && solver.getTerminator.terminates(funDef).isGuaranteed
+ )
+
+ // if(isRealFunDef) {
+ // println("Just created template for %s... Safe? %s".format(funDef.id.name, isTerminatingForAllInputs.toString))
+ // }
+
private val z3 = solver.z3
private val asClauses : Seq[Expr] = {
- (for(((b,p),es) <- guardedExprs; e <- es) yield {
- Implies(if(!p) Not(Variable(b)) else Variable(b), e)
+ (for((b,es) <- guardedExprs; e <- es) yield {
+ Implies(Variable(b), e)
}).toSeq
}
@@ -50,27 +60,29 @@ class FunctionTemplate private(
val asZ3Clauses: Seq[Z3AST] = asClauses.map(solver.toZ3Formula(_, idToZ3Ids).get)
- private val blockers : Map[(Identifier,Boolean),Set[FunctionInvocation]] = {
+ private val blockers : Map[Identifier,Set[FunctionInvocation]] = {
val idCall = FunctionInvocation(funDef, funDef.args.map(_.toVariable))
- Map((for((p, es) <- guardedExprs) yield {
+ Map((for((b, es) <- guardedExprs) yield {
val calls = es.foldLeft(Set.empty[FunctionInvocation])((s,e) => s ++ functionCallsOf(e)) - idCall
if(calls.isEmpty) {
None
} else {
- Some((p, calls))
+ Some((b, calls))
}
}).flatten.toSeq : _*)
}
- val z3Blockers: Map[(Z3AST, Boolean), Set[Z3FunctionInvocation]] = blockers.map {
- case ((b, p), funs) => ((idToZ3Ids(b), p) -> funs.map(fi => Z3FunctionInvocation(fi.funDef, fi.args.map(solver.toZ3Formula(_, idToZ3Ids).get))))
+ val z3Blockers: Map[Z3AST,Set[Z3FunctionInvocation]] = blockers.map {
+ case (b, funs) =>
+ (idToZ3Ids(b) -> funs.map(fi => Z3FunctionInvocation(fi.funDef, fi.args.map(solver.toZ3Formula(_, idToZ3Ids).get))))
}
- def instantiate(aVar : Z3AST, aPol : Boolean, args : Seq[Z3AST]) : (Seq[Z3AST], Map[(Z3AST, Boolean), Set[Z3FunctionInvocation]]) = {
+ def instantiate(aVar : Z3AST, args : Seq[Z3AST]) : (Seq[Z3AST], Map[Z3AST,Set[Z3FunctionInvocation]]) = {
assert(args.size == funDef.args.size)
- // The "isRealFunDef" part is to prevent evaluation of "fake" function templates, as generated from FairZ3Solver.
+ // The "isRealFunDef" part is to prevent evaluation of "fake"
+ // function templates, as generated from FairZ3Solver.
if(solver.evalGroundApps && isRealFunDef) {
val ga = args.view.map(solver.asGround)
if(ga.forall(_.isDefined)) {
@@ -89,7 +101,7 @@ class FunctionTemplate private(
}
val idSubstMap : Map[Z3AST, Z3AST] =
- Map(z3ActivatingBool -> (if (aPol) aVar else z3.mkNot(aVar))) ++
+ Map(z3ActivatingBool -> aVar) ++
(zippedExprVars ++ zippedCondVars).map{ case (id, c) => c -> solver.idToFreshZ3Id(id) } ++
(z3FunDefArgs zip args)
@@ -97,11 +109,11 @@ class FunctionTemplate private(
val (fromArray, toArray) = (from.toArray, to.toArray)
val newClauses = asZ3Clauses.map(z3.substitute(_, fromArray, toArray))
- val newBlockers = z3Blockers.map { case ((b, p), funs) =>
+ val newBlockers = z3Blockers.map { case (b, funs) =>
val bp = if (b == z3ActivatingBool) {
- (aVar, p == aPol)
+ aVar
} else {
- (idSubstMap(b), p)
+ idSubstMap(b)
}
val newFuns = funs.map(fi => fi.copy(args = fi.args.map(z3.substitute(_, fromArray, toArray))))
@@ -127,18 +139,17 @@ object FunctionTemplate {
val condVars : MutableSet[Identifier] = MutableSet.empty
val exprVars : MutableSet[Identifier] = MutableSet.empty
- // represents clauses of the form:
- // (~)id => expr && ... && expr
- val guardedExprs : MutableMap[(Identifier,Boolean),Seq[Expr]] = MutableMap.empty
+ // Represents clauses of the form:
+ // id => expr && ... && expr
+ val guardedExprs : MutableMap[Identifier,Seq[Expr]] = MutableMap.empty
- def storeGuarded(guardVar : Identifier, guardPol : Boolean, expr : Expr) : Unit = {
+ def storeGuarded(guardVar : Identifier, expr : Expr) : Unit = {
assert(expr.getType == BooleanType)
- val p : (Identifier,Boolean) = (guardVar,guardPol)
- if(guardedExprs.isDefinedAt(p)) {
- val prev : Seq[Expr] = guardedExprs(p)
- guardedExprs(p) = expr +: prev
+ if(guardedExprs.isDefinedAt(guardVar)) {
+ val prev : Seq[Expr] = guardedExprs(guardVar)
+ guardedExprs(guardVar) = expr +: prev
} else {
- guardedExprs(p) = Seq(expr)
+ guardedExprs(guardVar) = Seq(expr)
}
}
@@ -165,21 +176,21 @@ object FunctionTemplate {
res
}
- def rec(pathVar : Identifier, pathPol : Boolean, expr : Expr) : Expr = {
+ def rec(pathVar : Identifier, expr : Expr) : Expr = {
expr match {
case l @ Let(i, e, b) =>
val newExpr : Identifier = FreshIdentifier("lt", true).setType(i.getType)
exprVars += newExpr
- val re = rec(pathVar, pathPol, e)
- storeGuarded(pathVar, pathPol, Equals(Variable(newExpr), re))
- val rb = rec(pathVar, pathPol, replace(Map(Variable(i) -> Variable(newExpr)), b))
+ val re = rec(pathVar, e)
+ storeGuarded(pathVar, Equals(Variable(newExpr), re))
+ val rb = rec(pathVar, replace(Map(Variable(i) -> Variable(newExpr)), b))
rb
case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
case i @ Implies(lhs, rhs) =>
if (containsFunctionCalls(i)) {
- rec(pathVar, pathPol, IfExpr(lhs, rhs, BooleanLiteral(true)))
+ rec(pathVar, IfExpr(lhs, rhs, BooleanLiteral(true)))
} else {
i
}
@@ -190,7 +201,7 @@ object FunctionTemplate {
val ifExpr = partitions.map(And(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, b, BooleanLiteral(false)) }
- rec(pathVar, pathPol, ifExpr)
+ rec(pathVar, ifExpr)
} else {
a
}
@@ -201,7 +212,7 @@ object FunctionTemplate {
val ifExpr = partitions.map(Or(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, BooleanLiteral(true), b) }
- rec(pathVar, pathPol, ifExpr)
+ rec(pathVar, ifExpr)
} else {
o
}
@@ -210,27 +221,35 @@ object FunctionTemplate {
if(!containsFunctionCalls(cond) && !containsFunctionCalls(then) && !containsFunctionCalls(elze)) {
i
} else {
- val newBool : Identifier = FreshIdentifier("b", true).setType(BooleanType)
+ val newBool1 : Identifier = FreshIdentifier("b", true).setType(BooleanType)
+ val newBool2 : Identifier = FreshIdentifier("b", true).setType(BooleanType)
val newExpr : Identifier = FreshIdentifier("e", true).setType(i.getType)
- condVars += newBool
+
+ condVars += newBool1
+ condVars += newBool2
+
exprVars += newExpr
-
- val crec = rec(pathVar, pathPol, cond)
- val trec = rec(newBool, true, then)
- val erec = rec(newBool, false, elze)
-
- storeGuarded(pathVar, pathPol, Iff(Variable(newBool), crec))
- storeGuarded(newBool, true, Equals(Variable(newExpr), trec))
- storeGuarded(newBool, false, Equals(Variable(newExpr), erec))
+
+ val crec = rec(pathVar, cond)
+ val trec = rec(newBool1, then)
+ val erec = rec(newBool2, elze)
+
+ storeGuarded(pathVar, Or(Variable(newBool1), Variable(newBool2)))
+ storeGuarded(pathVar, Or(Not(Variable(newBool1)), Not(Variable(newBool2))))
+ // TODO can we improve this? i.e. make it more symmetrical?
+ // Probably it's symmetrical enough to Z3.
+ storeGuarded(pathVar, Iff(Variable(newBool1), crec))
+ storeGuarded(newBool1, Equals(Variable(newExpr), trec))
+ storeGuarded(newBool2, Equals(Variable(newExpr), erec))
Variable(newExpr)
}
}
case c @ Choose(_, _) => Variable(FreshIdentifier("choose", true).setType(c.getType))
- case n @ NAryOperator(as, r) => r(as.map(a => rec(pathVar, pathPol, a))).setType(n.getType)
- case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, pathPol, a1), rec(pathVar, pathPol, a2)).setType(b.getType)
- case u @ UnaryOperator(a, r) => r(rec(pathVar, pathPol, a)).setType(u.getType)
+ case n @ NAryOperator(as, r) => r(as.map(a => rec(pathVar, a))).setType(n.getType)
+ case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, a1), rec(pathVar, a2)).setType(b.getType)
+ case u @ UnaryOperator(a, r) => r(rec(pathVar, a)).setType(u.getType)
case t : Terminal => t
}
}
@@ -259,12 +278,11 @@ object FunctionTemplate {
val activatingBool : Identifier = FreshIdentifier("start", true).setType(BooleanType)
if (isRealFunDef) {
- val finalPred : Option[Expr] = invocationEqualsBody.map(expr => rec(activatingBool, true, expr))
- finalPred.foreach(p => storeGuarded(activatingBool, true, p))
+ val finalPred : Option[Expr] = invocationEqualsBody.map(expr => rec(activatingBool, expr))
+ finalPred.foreach(p => storeGuarded(activatingBool, p))
} else {
- storeGuarded(activatingBool, false, BooleanLiteral(false))
- val newFormula = rec(activatingBool, true, newBody.get)
- storeGuarded(activatingBool, true, newFormula)
+ val newFormula = rec(activatingBool, newBody.get)
+ storeGuarded(activatingBool, newFormula)
}
// Now the postcondition.
@@ -279,8 +297,8 @@ object FunctionTemplate {
post
}
- val finalPred2 : Expr = rec(activatingBool, true, postHolds)
- storeGuarded(activatingBool, true, finalPred2)
+ val finalPred2 : Expr = rec(activatingBool, postHolds)
+ storeGuarded(activatingBool, finalPred2)
}
new FunctionTemplate(solver, funDef, activatingBool, Set(condVars.toSeq : _*), Set(exprVars.toSeq : _*), Map(guardedExprs.toSeq : _*),
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index 840c16f2518de7df54b3f627d5ed7146dc4cf158..43d18726fbffd9af99d4b6643db3f36fdb1004e5 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -44,7 +44,9 @@ class SimpleTerminationChecker(context : LeonContext, program : Program) extends
if(!funDef.hasImplementation)
return NoGuarantee
- val sccIndex = funDefToSCCIndex(funDef)
+ val sccIndex = funDefToSCCIndex.getOrElse(funDef, {
+ return NoGuarantee
+ })
val sccCallees = sccGraph(sccIndex)
// We check all functions that are in a "lower" scc. These must