diff --git a/src/main/java/leon/codegen/runtime/PartialLambda.java b/src/main/java/leon/codegen/runtime/FiniteLambda.java
similarity index 64%
rename from src/main/java/leon/codegen/runtime/PartialLambda.java
rename to src/main/java/leon/codegen/runtime/FiniteLambda.java
index b04036db5e9f81d1eaf7fa2c9a047bfef45a4df8..d249392384c1cf99cf6ebc5ae0677a4a41c73819 100644
--- a/src/main/java/leon/codegen/runtime/PartialLambda.java
+++ b/src/main/java/leon/codegen/runtime/FiniteLambda.java
@@ -4,15 +4,11 @@ package leon.codegen.runtime;
import java.util.HashMap;
-public final class PartialLambda extends Lambda {
+public final class FiniteLambda extends Lambda {
final HashMap<Tuple, Object> mapping = new HashMap<Tuple, Object>();
private final Object dflt;
- public PartialLambda() {
- this(null);
- }
-
- public PartialLambda(Object dflt) {
+ public FiniteLambda(Object dflt) {
super();
this.dflt = dflt;
}
@@ -26,18 +22,16 @@ public final class PartialLambda extends Lambda {
Tuple tuple = new Tuple(args);
if (mapping.containsKey(tuple)) {
return mapping.get(tuple);
- } else if (dflt != null) {
- return dflt;
} else {
- throw new LeonCodeGenRuntimeException("Partial function apply on undefined arguments " + tuple);
+ return dflt;
}
}
@Override
public boolean equals(Object that) {
- if (that != null && (that instanceof PartialLambda)) {
- PartialLambda l = (PartialLambda) that;
- return ((dflt != null && dflt.equals(l.dflt)) || (dflt == null && l.dflt == null)) && mapping.equals(l.mapping);
+ if (that != null && (that instanceof FiniteLambda)) {
+ FiniteLambda l = (FiniteLambda) that;
+ return dflt.equals(l.dflt) && mapping.equals(l.mapping);
} else {
return false;
}
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor.java
index 597beec44b6a1a1719909e00ecb7d7916f0c7c03..76030a6129ac4c62115daf62162bffb658c891fd 100644
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor.java
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHenkinMonitor.java
@@ -32,8 +32,8 @@ public class LeonCodeGenRuntimeHenkinMonitor extends LeonCodeGenRuntimeMonitor {
public List<Tuple> domain(Object obj, int type) {
List<Tuple> domain = new LinkedList<Tuple>();
- if (obj instanceof PartialLambda) {
- PartialLambda l = (PartialLambda) obj;
+ if (obj instanceof FiniteLambda) {
+ FiniteLambda l = (FiniteLambda) obj;
for (Tuple key : l.mapping.keySet()) {
domain.add(key);
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index db49d0425e39ac888badb90c97aa7c8432d0ee96..4eb880cee176ce56f74dbf770fb2a540faf16ea2 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -34,7 +34,7 @@ object Main {
// Add whatever you need here.
lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
- solvers.z3.FairZ3Component, MainComponent, SharedOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
+ solvers.combinators.UnrollingProcedure, MainComponent, SharedOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
)
/*
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index d99a9a1a951edeb2260874d004e911de9628ab7d..d703c736d6c3442ae8ea23710287ba148389d876 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -74,7 +74,7 @@ trait CodeGeneration {
private[codegen] val CaseClassClass = "leon/codegen/runtime/CaseClass"
private[codegen] val LambdaClass = "leon/codegen/runtime/Lambda"
private[codegen] val ForallClass = "leon/codegen/runtime/Forall"
- private[codegen] val PartialLambdaClass = "leon/codegen/runtime/PartialLambda"
+ private[codegen] val FiniteLambdaClass = "leon/codegen/runtime/FiniteLambda"
private[codegen] val ErrorClass = "leon/codegen/runtime/LeonCodeGenRuntimeException"
private[codegen] val InvalidForallClass = "leon/codegen/runtime/LeonCodeGenQuantificationException"
private[codegen] val ImpossibleEvaluationClass = "leon/codegen/runtime/LeonCodeGenEvaluationException"
@@ -1133,21 +1133,16 @@ trait CodeGeneration {
ch << InvokeVirtual(LambdaClass, "apply", s"([L$ObjectClass;)L$ObjectClass;")
mkUnbox(app.getType, ch)
- case p @ PartialLambda(mapping, optDflt, _) =>
- ch << New(PartialLambdaClass) << DUP
- optDflt match {
- case Some(dflt) =>
- mkBoxedExpr(dflt, ch)
- ch << InvokeSpecial(PartialLambdaClass, constructorName, s"(L$ObjectClass;)V")
- case None =>
- ch << InvokeSpecial(PartialLambdaClass, constructorName, "()V")
- }
+ case p @ FiniteLambda(mapping, dflt, _) =>
+ ch << New(FiniteLambdaClass) << DUP
+ mkBoxedExpr(dflt, ch)
+ ch << InvokeSpecial(FiniteLambdaClass, constructorName, s"(L$ObjectClass;)V")
for ((es,v) <- mapping) {
ch << DUP
mkTuple(es, ch)
mkBoxedExpr(v, ch)
- ch << InvokeVirtual(PartialLambdaClass, "add", s"(L$TupleClass;L$ObjectClass;)V")
+ ch << InvokeVirtual(FiniteLambdaClass, "add", s"(L$TupleClass;L$ObjectClass;)V")
}
case l @ Lambda(args, body) =>
@@ -1407,6 +1402,8 @@ trait CodeGeneration {
ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
ch << ATHROW
+ case forall @ Forall(fargs, body) =>
+
case choose: Choose =>
val prob = synthesis.Problem.fromSpec(choose.pred)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 18a0b607589f334fa021ab31ab4163201b5ba888..6af6aa9e50686244581de931f793f00c34c94ed9 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -237,12 +237,8 @@ class CompilationUnit(val ctx: LeonContext,
}
m
- case f @ PartialLambda(mapping, dflt, _) =>
- val l = if (dflt.isDefined) {
- new leon.codegen.runtime.PartialLambda(dflt.get)
- } else {
- new leon.codegen.runtime.PartialLambda()
- }
+ case f @ FiniteLambda(mapping, dflt, _) =>
+ val l = new leon.codegen.runtime.FiniteLambda(dflt)
for ((ks,v) <- mapping) {
// Force tuple even with 1/0 elems.
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index af315aacade7e06eeb346dcbb94f56f53f9d5f87..1975400500b741a8fb59fe953b72faf08bf8968e 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -131,7 +131,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
Constructor[Expr, TypeTree](subs, ft, { s =>
val grouped = s.grouped(from.size + 1).toSeq
val mapping = grouped.init.map { case args :+ res => (args -> res) }
- PartialLambda(mapping, Some(grouped.last.last), ft)
+ FiniteLambda(mapping, grouped.last.last, ft)
}, ft.asString(ctx) + "@" + size)
}
constructors += ft -> cs
diff --git a/src/main/scala/leon/evaluators/AngelicEvaluator.scala b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
index 99d704f67c7485ba8e00727c4edcc5d30644b4cc..57f233cf44caa63dd587e0d792eb33ec62b89d55 100644
--- a/src/main/scala/leon/evaluators/AngelicEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
@@ -22,9 +22,6 @@ class AngelicEvaluator(underlying: NDEvaluator)
case other@(RuntimeError(_) | EvaluatorError(_)) =>
other.asInstanceOf[Result[Nothing]]
}
-
- /** Checks that `model |= expr` and that quantifications are all valid */
- def check(expr: Expr, model: Model): CheckResult = underlying.check(expr, model)
}
class DemonicEvaluator(underlying: NDEvaluator)
@@ -42,7 +39,4 @@ class DemonicEvaluator(underlying: NDEvaluator)
case other@(RuntimeError(_) | EvaluatorError(_)) =>
other.asInstanceOf[Result[Nothing]]
}
-
- /** Checks that `model |= expr` and that quantifications are all valid */
- def check(expr: Expr, model: Model): CheckResult = underlying.check(expr, model)
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index e6bb722aedde0b6faecdcc2bf11651c0a7353859..f63bed50fb2835eca2ebf91102992b0e5951968e 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -38,50 +38,6 @@ class CodeGenEvaluator(ctx: LeonContext, val unit : CompilationUnit) extends Eva
}
}
-
- def check(expression: Expr, fullModel: solvers.Model) : CheckResult = {
- val (_, assign) = fullModel.toSeq.partition {
- case (id, v) => unit.abstractFunDefs(id)
- }
-
- compileExpr(expression, assign.map(_._1)).map { ce =>
- ctx.timers.evaluators.codegen.runtime.start()
-
- try {
- val res = ce.eval(fullModel, check = true)
-
- if (res == BooleanLiteral(true)) {
- EvaluationResults.CheckSuccess
- } else {
- EvaluationResults.CheckValidityFailure
- }
- } catch {
- case e : ArithmeticException =>
- EvaluationResults.CheckRuntimeFailure(e.getMessage)
-
- case e : ArrayIndexOutOfBoundsException =>
- EvaluationResults.CheckRuntimeFailure(e.getMessage)
-
- case e : LeonCodeGenRuntimeException =>
- EvaluationResults.CheckRuntimeFailure(e.getMessage)
-
- case e : LeonCodeGenEvaluationException =>
- EvaluationResults.CheckRuntimeFailure(e.getMessage)
-
- case e : java.lang.ExceptionInInitializerError =>
- EvaluationResults.CheckRuntimeFailure(e.getException.getMessage)
-
- case so : java.lang.StackOverflowError =>
- EvaluationResults.CheckRuntimeFailure("Stack overflow")
-
- case e : LeonCodeGenQuantificationException =>
- EvaluationResults.CheckQuantificationFailure(e.getMessage)
- } finally {
- ctx.timers.evaluators.codegen.runtime.stop()
- }
- }.getOrElse(EvaluationResults.CheckRuntimeFailure("Couldn't compile expression."))
- }
-
def eval(expression: Expr, model: solvers.Model) : EvaluationResult = {
compile(expression, model.toSeq.map(_._1)).map { e =>
ctx.timers.evaluators.codegen.runtime.start()
diff --git a/src/main/scala/leon/evaluators/ContextualEvaluator.scala b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
index eb57bbbf3550d8d177f92188d12d1ff3a3abbbd5..76f5c500890135fc7fc7d3e75814c2d92020e2b0 100644
--- a/src/main/scala/leon/evaluators/ContextualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
@@ -48,30 +48,6 @@ abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps
}
}
- def check(ex: Expr, model: Model): CheckResult = {
- assert(ex.getType == BooleanType, "Can't check non-boolean expression " + ex.asString)
- try {
- lastGC = Some(initGC(model, check = true))
- ctx.timers.evaluators.recursive.runtime.start()
- val res = e(ex)(initRC(model.toMap), lastGC.get)
- if (res == BooleanLiteral(true)) EvaluationResults.CheckSuccess
- else EvaluationResults.CheckValidityFailure
- } catch {
- case so: StackOverflowError =>
- EvaluationResults.CheckRuntimeFailure("Stack overflow")
- case e @ EvalError(msg) =>
- EvaluationResults.CheckRuntimeFailure(msg)
- case e @ RuntimeError(msg) =>
- EvaluationResults.CheckRuntimeFailure(msg)
- case jre: java.lang.RuntimeException =>
- EvaluationResults.CheckRuntimeFailure(jre.getMessage)
- case qe @ QuantificationError(msg) =>
- EvaluationResults.CheckQuantificationFailure(msg)
- } finally {
- ctx.timers.evaluators.recursive.runtime.stop()
- }
- }
-
protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Value
def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected ${expected.asString}, found ${tree.asString} of type ${tree.getType}."
@@ -138,4 +114,4 @@ private[evaluators] trait CEvalHelpers {
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/evaluators/EvaluationResults.scala b/src/main/scala/leon/evaluators/EvaluationResults.scala
index 18f7a0c92d448f98c8f6a271d91e021a649e3b9c..b9cbecdde4cdd31b2b29dcb82fdd23c50aaf9a24 100644
--- a/src/main/scala/leon/evaluators/EvaluationResults.scala
+++ b/src/main/scala/leon/evaluators/EvaluationResults.scala
@@ -15,21 +15,4 @@ object EvaluationResults {
/** Represents an evaluation that failed (in the evaluator). */
case class EvaluatorError(message : String) extends Result(None)
-
- /** Results of checking proposition evaluation.
- * Useful for verification of model validity in presence of quantifiers. */
- sealed abstract class CheckResult(val success: Boolean)
-
- /** Successful proposition evaluation (model |= expr) */
- case object CheckSuccess extends CheckResult(true)
-
- /** Check failed with `model |= !expr` */
- case object CheckValidityFailure extends CheckResult(false)
-
- /** Check failed due to evaluation or runtime errors.
- * @see [[RuntimeError]] and [[EvaluatorError]] */
- case class CheckRuntimeFailure(msg: String) extends CheckResult(false)
-
- /** Check failed due to inconsistence of model with quantified propositions. */
- case class CheckQuantificationFailure(msg: String) extends CheckResult(false)
}
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index ff0f35f1241547d66f81f0b341fca508276b40ea..400409577ac7aebf490d8a961ac44c67036989c7 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -18,7 +18,6 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
type Value
type EvaluationResult = EvaluationResults.Result[Value]
- type CheckResult = EvaluationResults.CheckResult
/** Evaluates an expression, using [[Model.mapping]] as a valuation function for the free variables. */
def eval(expr: Expr, model: Model) : EvaluationResult
@@ -31,9 +30,6 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
/** Evaluates a ground expression. */
final def eval(expr: Expr) : EvaluationResult = eval(expr, Model.empty)
- /** Checks that `model |= expr` and that quantifications are all valid */
- def check(expr: Expr, model: Model) : CheckResult
-
/** Compiles an expression into a function, where the arguments are the free variables in the expression.
* `argorder` specifies in which order the arguments should be passed.
* The default implementation uses the evaluation function each time, but evaluators are free
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index e4eeb2e8ca42220f39a9adb00263196046d91c60..ad705725688dbccc5c858fd745980a9719c0ad53 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -28,7 +28,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
lazy val scalaEv = new ScalacEvaluator(this, ctx, prog)
protected var clpCache = Map[(Choose, Seq[Expr]), Expr]()
-
+ protected var frlCache = Map[(Forall, Seq[Expr]), Expr]()
+
private var evaluationFailsOnChoose = false
/** Sets the flag if when encountering a Choose, it should fail instead of solving it. */
def setEvaluationFailOnChoose(b: Boolean) = { this.evaluationFailsOnChoose = b; this }
@@ -50,13 +51,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val newArgs = args.map(e)
val mapping = l.paramSubst(newArgs)
e(body)(rctx.withNewVars(mapping), gctx)
- case PartialLambda(mapping, dflt, _) =>
+ case FiniteLambda(mapping, dflt, _) =>
mapping.find { case (pargs, res) =>
(args zip pargs).forall(p => e(Equals(p._1, p._2)) == BooleanLiteral(true))
- }.map(_._2).orElse(dflt).getOrElse {
- throw EvalError("Cannot apply partial lambda outside of domain : " +
- args.map(e(_).asString(ctx)).mkString("(", ", ", ")"))
- }
+ }.map(_._2).getOrElse(dflt)
case f =>
throw EvalError("Cannot apply non-lambda function " + f.asString)
}
@@ -187,7 +185,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(lv,rv) match {
case (FiniteSet(el1, _),FiniteSet(el2, _)) => BooleanLiteral(el1 == el2)
case (FiniteMap(el1, _, _),FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
- case (PartialLambda(m1, d1, _), PartialLambda(m2, d2, _)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
+ case (FiniteLambda(m1, d1, _), FiniteLambda(m2, d2, _)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
case _ => BooleanLiteral(lv == rv)
}
@@ -509,11 +507,78 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
newLambda
- case PartialLambda(mapping, dflt, tpe) =>
- PartialLambda(mapping.map(p => p._1.map(e) -> e(p._2)), dflt.map(e), tpe)
+ case FiniteLambda(mapping, dflt, tpe) =>
+ FiniteLambda(mapping.map(p => p._1.map(e) -> e(p._2)), e(dflt), tpe)
+
+ case f @ Forall(fargs, body) =>
+
+ implicit val debugSection = utils.DebugSectionVerification
+
+ ctx.reporter.debug("Executing forall!")
+
+ val mapping = variablesOf(f).map(id => id -> rctx.mappings(id)).toMap
+ val context = mapping.toSeq.sortBy(_._1.uniqueName).map(_._2)
+ frlCache.getOrElse((f, context), {
+ val tStart = System.currentTimeMillis
+
+ val solverf = SolverFactory.getFromSettings(ctx, program)
+ val solver = solverf.getNewSolver()
+
+ try {
+ val cnstr = Not(replaceFromIDs(mapping, body))
+ solver.assertCnstr(cnstr)
+
+ gctx.model match {
+ case pm: HenkinModel =>
+ val quantifiers = fargs.map(_.id).toSet
+ val quorums = extractQuorums(body, quantifiers)
+
+ val domainCnstr = orJoin(quorums.map { quorum =>
+ val quantifierDomains = quorum.flatMap { case (path, caller, args) =>
+ val matcher = e(expr) match {
+ case l: Lambda => gctx.lambdas.getOrElse(l, l)
+ case ev => ev
+ }
+
+ val domain = pm.domain(matcher)
+ args.zipWithIndex.flatMap {
+ case (Variable(id),idx) if quantifiers(id) =>
+ Some(id -> domain.map(cargs => path -> cargs(idx)))
+ case _ => None
+ }
+ }
+
+ val domainMap = quantifierDomains.groupBy(_._1).mapValues(_.map(_._2).flatten)
+ andJoin(domainMap.toSeq.map { case (id, dom) =>
+ orJoin(dom.toSeq.map { case (path, value) => and(path, Equals(Variable(id), value)) })
+ })
+ })
+
+ solver.assertCnstr(domainCnstr)
+
+ case _ =>
+ }
+
+ solver.check match {
+ case Some(negRes) =>
+ val total = System.currentTimeMillis-tStart
+ val res = BooleanLiteral(!negRes)
+ ctx.reporter.debug("Verification took "+total+"ms")
+ ctx.reporter.debug("Finished forall evaluation with: "+res)
- case Forall(fargs, body) =>
- evalForall(fargs.map(_.id).toSet, body)
+ frlCache += (f, context) -> res
+ res
+ case _ =>
+ throw RuntimeError("Timeout exceeded")
+ }
+ } catch {
+ case e: Throwable =>
+ throw EvalError("Runtime verification of forall failed: "+e.getMessage)
+ } finally {
+ solverf.reclaim(solver)
+ solverf.shutdown()
+ }
+ })
case ArrayLength(a) =>
val FiniteArray(_, _, IntLiteral(length)) = e(a)
@@ -555,6 +620,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (l,r) =>
throw EvalError(typeErrorMsg(l, MapType(r.getType, g.getType)))
}
+
case u @ MapUnion(m1,m2) => (e(m1), e(m2)) match {
case (f1@FiniteMap(ss1, _, _), FiniteMap(ss2, _, _)) =>
val newSs = ss1 ++ ss2
@@ -563,6 +629,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (l, r) =>
throw EvalError(typeErrorMsg(l, m1.getType))
}
+
case i @ MapIsDefinedAt(m,k) => (e(m), e(k)) match {
case (FiniteMap(ss, _, _), e) => BooleanLiteral(ss.contains(e))
case (l, r) => throw EvalError(typeErrorMsg(l, m.getType))
@@ -590,7 +657,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val solverf = SolverFactory.getFromSettings(ctx, program)
val solver = solverf.getNewSolver()
-
try {
val eqs = p.as.map {
case id =>
@@ -719,142 +785,5 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
} yield (caze, r)
}
}
-
-
- protected def evalForall(quants: Set[Identifier], body: Expr, check: Boolean = true)(implicit rctx: RC, gctx: GC): Expr = {
- val henkinModel: HenkinModel = gctx.model match {
- case hm: HenkinModel => hm
- case _ => throw EvalError("Can't evaluate foralls without henkin model")
-}
-
- val TopLevelAnds(conjuncts) = body
- e(andJoin(conjuncts.flatMap { conj =>
- val vars = variablesOf(conj)
- val quantified = quants.filter(vars)
-
- extractQuorums(conj, quantified).flatMap { case (qrm, others) =>
- val quorum = qrm.toList
-
- if (quorum.exists { case (TopLevelAnds(paths), _, _) =>
- val p = andJoin(paths.filter(path => (variablesOf(path) & quantified).isEmpty))
- e(p) == BooleanLiteral(false)
- }) List(BooleanLiteral(true)) else {
-
- var mappings: Seq[(Identifier, Int, Int)] = Seq.empty
- var constraints: Seq[(Expr, Int, Int)] = Seq.empty
- var equalities: Seq[((Int, Int), (Int, Int))] = Seq.empty
-
- for (((_, expr, args), qidx) <- quorum.zipWithIndex) {
- val (qmappings, qconstraints) = args.zipWithIndex.partition {
- case (Variable(id),aidx) => quantified(id)
- case _ => false
- }
-
- mappings ++= qmappings.map(p => (p._1.asInstanceOf[Variable].id, qidx, p._2))
- constraints ++= qconstraints.map(p => (p._1, qidx, p._2))
- }
-
- val mapping = for ((id, es) <- mappings.groupBy(_._1)) yield {
- val base :: others = es.toList.map(p => (p._2, p._3))
- equalities ++= others.map(p => base -> p)
- (id -> base)
- }
-
- def domain(expr: Expr): Set[Seq[Expr]] = henkinModel.domain(e(expr) match {
- case l: Lambda => gctx.lambdas.getOrElse(l, l)
- case ev => ev
- })
-
- val argSets = quorum.foldLeft[List[Seq[Seq[Expr]]]](List(Seq.empty)) {
- case (acc, (_, expr, _)) => acc.flatMap(s => domain(expr).map(d => s :+ d))
- }
-
- argSets.map { args =>
- val argMap: Map[(Int, Int), Expr] = args.zipWithIndex.flatMap {
- case (a, qidx) => a.zipWithIndex.map { case (e, aidx) => (qidx, aidx) -> e }
- }.toMap
-
- val map = mapping.map { case (id, key) => id -> argMap(key) }
- val enabler = andJoin(constraints.map {
- case (e, qidx, aidx) => Equals(e, argMap(qidx -> aidx))
- } ++ equalities.map {
- case (k1, k2) => Equals(argMap(k1), argMap(k2))
- })
-
- val ctx = rctx.withNewVars(map)
- if (e(enabler)(ctx, gctx) == BooleanLiteral(true)) {
- if (gctx.check) {
- for ((b,caller,args) <- others if e(b)(ctx, gctx) == BooleanLiteral(true)) {
- val evArgs = args.map(arg => e(arg)(ctx, gctx))
- if (!domain(caller)(evArgs))
- throw QuantificationError("Unhandled transitive implication in " + replaceFromIDs(map, conj))
- }
- }
-
- e(conj)(ctx, gctx)
- } else {
- BooleanLiteral(true)
- }
- }
- }
- }
- })) match {
- case res @ BooleanLiteral(true) if check =>
- if (gctx.check) {
- checkForall(quants, body) match {
- case status: ForallInvalid =>
- throw QuantificationError("Invalid forall: " + status.getMessage)
- case _ =>
- // make sure the body doesn't contain matches or lets as these introduce new locals
- val cleanBody = expandLets(matchToIfThenElse(body))
- val calls = new CollectorWithPaths[(Expr, Seq[Expr], Seq[Expr])] {
- def collect(e: Expr, path: Seq[Expr]): Option[(Expr, Seq[Expr], Seq[Expr])] = e match {
- case QuantificationMatcher(IsTyped(caller, _: FunctionType), args) => Some((caller, args, path))
- case _ => None
- }
-
- override def rec(e: Expr, path: Seq[Expr]): Expr = e match {
- case l : Lambda => l
- case _ => super.rec(e, path)
- }
- }.traverse(cleanBody)
-
- for ((caller, appArgs, paths) <- calls) {
- val path = andJoin(paths.filter(expr => (variablesOf(expr) & quants).isEmpty))
- if (e(path) == BooleanLiteral(true)) e(caller) match {
- case _: PartialLambda => // OK
- case l: Lambda =>
- val nl @ Lambda(args, body) = gctx.lambdas.getOrElse(l, l)
- val lambdaQuantified = (appArgs zip args).collect {
- case (Variable(id), vd) if quants(id) => vd.id
- }.toSet
-
- if (lambdaQuantified.nonEmpty) {
- checkForall(lambdaQuantified, body) match {
- case lambdaStatus: ForallInvalid =>
- throw QuantificationError("Invalid forall: " + lambdaStatus.getMessage)
- case _ => // do nothing
- }
-
- val axiom = Equals(Application(nl, args.map(_.toVariable)), nl.body)
- if (evalForall(args.map(_.id).toSet, axiom, check = false) == BooleanLiteral(false)) {
- throw QuantificationError("Unaxiomatic lambda " + l)
- }
- }
- case f =>
- throw EvalError("Cannot apply non-lambda function " + f.asString)
- }
- }
- }
- }
-
- res
-
- // `res == false` means the quantification is valid since there effectivelly must
- // exist an input for which the proposition doesn't hold
- case res => res
- }
- }
-
}
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index 3035e6541e1f48bf51c472415aaafe7b0d1d02b0..feb0dd7f2590674ca231a29a8f7e8ba91945a2e3 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -37,12 +37,12 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
case l @ Lambda(params, body) =>
val mapping = l.paramSubst(newArgs)
e(body)(rctx.withNewVars(mapping), gctx).distinct
- case PartialLambda(mapping, _, _) =>
+ case FiniteLambda(mapping, dflt, _) =>
// FIXME
- mapping.collectFirst {
+ Stream(mapping.collectFirst {
case (pargs, res) if (newArgs zip pargs).forall { case (f, r) => f == r } =>
res
- }.toStream
+ }.getOrElse(dflt))
case _ =>
Stream()
}
@@ -127,7 +127,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
Stream(replaceFromIDs(mapping, nl))
// FIXME
- case PartialLambda(mapping, tpe, df) =>
+ case FiniteLambda(mapping, dflt, tpe) =>
def solveOne(pair: (Seq[Expr], Expr)) = {
val (args, res) = pair
for {
@@ -135,7 +135,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
r <- e(res)
} yield as -> r
}
- cartesianProduct(mapping map solveOne) map (PartialLambda(_, tpe, df)) // FIXME!!!
+ cartesianProduct(mapping map solveOne) map (FiniteLambda(_, dflt, tpe)) // FIXME!!!
case f @ Forall(fargs, TopLevelAnds(conjuncts)) =>
Stream() // FIXME
@@ -337,7 +337,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
(lv, rv) match {
case (FiniteSet(el1, _), FiniteSet(el2, _)) => BooleanLiteral(el1 == el2)
case (FiniteMap(el1, _, _), FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
- case (PartialLambda(m1, _, d1), PartialLambda(m2, _, d2)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
+ case (FiniteLambda(m1, d1, _), FiniteLambda(m2, d2, _)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
case _ => BooleanLiteral(lv == rv)
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 19d20604ddc9ff9c3187c2fe24ee50f46e658850..ce6b7fb4d863f290dd087074e8734cdc6f8b5013 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -884,7 +884,7 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
GenericValue(tp, 0)
case ft @ FunctionType(from, to) =>
- PartialLambda(Seq.empty, Some(simplestValue(to)), ft)
+ FiniteLambda(Seq.empty, simplestValue(to), ft)
case _ => throw LeonFatalError("I can't choose simplest value for type " + tpe)
}
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 88edef68586474c24e7a13b70a22e9beed7441b8..609f5cda04dcd1a1e5e0e55d1c5f01475236fd94 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -227,7 +227,7 @@ object Expressions {
}
}
- case class PartialLambda(mapping: Seq[(Seq[Expr], Expr)], default: Option[Expr], tpe: FunctionType) extends Expr {
+ case class FiniteLambda(mapping: Seq[(Seq[Expr], Expr)], default: Expr, tpe: FunctionType) extends Expr {
val getType = tpe
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index cfa4780efccad338b5df44400b53da7264a2c2d7..00541f4450f40585782d3f6b82d7f7665c78f8cd 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -52,7 +52,7 @@ object Extractors {
Some((Seq(a), (es: Seq[Expr]) => ArrayLength(es.head)))
case Lambda(args, body) =>
Some((Seq(body), (es: Seq[Expr]) => Lambda(args, es.head)))
- case PartialLambda(mapping, dflt, tpe) =>
+ case FiniteLambda(mapping, dflt, tpe) =>
val sze = tpe.from.size + 1
val subArgs = mapping.flatMap { case (args, v) => args :+ v }
val builder = (as: Seq[Expr]) => {
@@ -63,10 +63,9 @@ object Extractors {
case Seq() => Seq.empty
case _ => sys.error("unexpected number of key/value expressions")
}
- val (nas, nd) = if (dflt.isDefined) (as.init, Some(as.last)) else (as, None)
- PartialLambda(rec(nas), nd, tpe)
+ FiniteLambda(rec(as.init), as.last, tpe)
}
- Some((subArgs ++ dflt, builder))
+ Some((subArgs :+ dflt, builder))
case Forall(args, body) =>
Some((Seq(body), (es: Seq[Expr]) => Forall(args, es.head)))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 44d454a9c0a4f1127ed0533f872c66f1ec6bc067..67296c3dc4f2cc130915d7adfdb3cc186447d7df 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -270,19 +270,15 @@ class PrettyPrinter(opts: PrinterOptions,
case Lambda(args, body) =>
optP { p"($args) => $body" }
- case PartialLambda(mapping, dflt, _) =>
+ case FiniteLambda(mapping, dflt, _) =>
optP {
def pm(p: (Seq[Expr], Expr)): PrinterHelpers.Printable =
(pctx: PrinterContext) => p"${purescala.Constructors.tupleWrap(p._1)} => ${p._2}"(pctx)
if (mapping.isEmpty) {
- p"{}"
+ p"{ * => ${dflt} }"
} else {
- p"{ ${nary(mapping map pm)} }"
- }
-
- if (dflt.isDefined) {
- p" getOrElse ${dflt.get}"
+ p"{ ${nary(mapping map pm)}, * => ${dflt} }"
}
}
diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index bb5115baab042a1bd524fdb2f73deeabefa59243..3efdc9df7e5b92b0e5d87faf9205c1ef8f3e90af 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -49,7 +49,7 @@ object Quantification {
res.filter(ms => ms.forall(m => reverseMap(m) subsetOf ms))
}
- def extractQuorums(expr: Expr, quantified: Set[Identifier]): Seq[(Set[(Expr, Expr, Seq[Expr])], Set[(Expr, Expr, Seq[Expr])])] = {
+ def extractQuorums(expr: Expr, quantified: Set[Identifier]): Seq[Set[(Expr, Expr, Seq[Expr])]] = {
object QMatcher {
def unapply(e: Expr): Option[(Expr, Seq[Expr])] = e match {
case QuantificationMatcher(expr, args) =>
@@ -65,38 +65,9 @@ object Quantification {
val allMatchers = CollectorWithPaths { case QMatcher(expr, args) => expr -> args }.traverse(expr)
val matchers = allMatchers.map { case ((caller, args), path) => (path, caller, args) }.toSet
- val quorums = extractQuorums(matchers, quantified,
+ extractQuorums(matchers, quantified,
(p: (Expr, Expr, Seq[Expr])) => p._3.collect { case QMatcher(e, a) => (p._1, e, a) }.toSet,
(p: (Expr, Expr, Seq[Expr])) => p._3.collect { case Variable(id) if quantified(id) => id }.toSet)
-
- quorums.map(quorum => quorum -> matchers.filter(m => !quorum(m)))
- }
-
- def extractModel(
- asMap: Map[Identifier, Expr],
- funDomains: Map[Identifier, Set[Seq[Expr]]],
- typeDomains: Map[TypeTree, Set[Seq[Expr]]],
- evaluator: DeterministicEvaluator
- ): Map[Identifier, Expr] = asMap.map { case (id, expr) =>
- id -> (funDomains.get(id) match {
- case Some(domain) =>
- PartialLambda(domain.toSeq.map { es =>
- val optEv = evaluator.eval(Application(expr, es)).result
- es -> optEv.getOrElse(scala.sys.error("Unexpectedly failed to evaluate " + Application(expr, es)))
- }, None, id.getType.asInstanceOf[FunctionType])
-
- case None => postMap {
- case p @ PartialLambda(mapping, dflt, tpe) =>
- Some(PartialLambda(typeDomains.get(tpe) match {
- case Some(domain) => domain.toSeq.map { es =>
- val optEv = evaluator.eval(Application(p, es)).result
- es -> optEv.getOrElse(scala.sys.error("Unexpectedly failed to evaluate " + Application(p, es)))
- }
- case _ => Seq.empty
- }, None, tpe))
- case _ => None
- } (expr)
- })
}
object HenkinDomains {
@@ -106,8 +77,7 @@ object Quantification {
class HenkinDomains (val lambdas: Map[Lambda, Set[Seq[Expr]]], val tpes: Map[TypeTree, Set[Seq[Expr]]]) {
def get(e: Expr): Set[Seq[Expr]] = {
val specialized: Set[Seq[Expr]] = e match {
- case PartialLambda(_, Some(dflt), _) => scala.sys.error("No domain for non-partial lambdas")
- case PartialLambda(mapping, _, _) => mapping.map(_._1).toSet
+ case FiniteLambda(mapping, _, _) => mapping.map(_._1).toSet
case l: Lambda => lambdas.getOrElse(l, Set.empty)
case _ => Set.empty
}
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 5f002ccdacb54b16515fa0d54f7573ba2ebc82cb..bba8ba20d9bbf849874052924647d55cb6420d2d 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -12,6 +12,7 @@ import purescala.Constructors._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Types._
+import purescala.TypeOps.bestRealType
import utils._
import templates._
@@ -168,6 +169,19 @@ trait AbstractUnrollingSolver[T]
trait ModelWrapper {
def get(id: Identifier): Option[Expr]
def eval(elem: T, tpe: TypeTree): Option[Expr]
+
+ private[AbstractUnrollingSolver] def extract(b: T, m: Matcher[T]): Option[Seq[Expr]] = {
+ val QuantificationTypeMatcher(fromTypes, _) = m.tpe
+ val optEnabler = eval(b, BooleanType)
+ optEnabler.filter(_ == BooleanLiteral(true)).flatMap { _ =>
+ val optArgs = (m.args zip fromTypes).map { case (arg, tpe) => eval(arg.encoded, tpe) }
+ if (optArgs.forall(_.isDefined)) {
+ Some(optArgs.map(_.get))
+ } else {
+ None
+ }
+ }
+ }
}
def solverGetModel: ModelWrapper
@@ -181,21 +195,21 @@ trait AbstractUnrollingSolver[T]
private def validateModel(model: Model, assumptions: Seq[Expr], silenceErrors: Boolean): Boolean = {
val expr = andJoin(assumptions ++ constraints)
- evaluator.check(expr, model) match {
- case EvaluationResults.CheckSuccess =>
+ evaluator.eval(expr, model) match {
+ case EvaluationResults.Successful(BooleanLiteral(true)) =>
reporter.debug("- Model validated.")
true
- case EvaluationResults.CheckValidityFailure =>
+ case EvaluationResults.Successful(_) =>
reporter.debug("- Invalid model.")
false
- case EvaluationResults.CheckRuntimeFailure(msg) =>
- emit(silenceErrors)("- Model leads to evaluation error: " + msg)
+ case EvaluationResults.RuntimeError(msg) =>
+ emit(silenceErrors)("- Model leads to runtime error: " + msg)
false
- case EvaluationResults.CheckQuantificationFailure(msg) =>
- emit(silenceErrors)("- Model leads to quantification error: " + msg)
+ case EvaluationResults.EvaluatorError(msg) =>
+ emit(silenceErrors)("- Model leads to evaluation error: " + msg)
false
}
}
@@ -203,74 +217,109 @@ trait AbstractUnrollingSolver[T]
private def getPartialModel: HenkinModel = {
val wrapped = solverGetModel
- 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)) {
- Some(optArgs.map(_.get))
- } else {
- None
- }
- }
- }
-
- val (typeInsts, partialInsts, lambdaInsts) = templateGenerator.manager.instantiations
+ val typeInsts = templateGenerator.manager.typeInstantiations
+ val partialInsts = templateGenerator.manager.partialInstantiations
+ val lambdaInsts = templateGenerator.manager.lambdaInstantiations
val typeDomains: Map[TypeTree, Set[Seq[Expr]]] = typeInsts.map {
- case (tpe, domain) => tpe -> domain.flatMap { case (b, m) => extract(b, m) }.toSet
+ case (tpe, domain) => tpe -> domain.flatMap { case (b, m) => wrapped.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
+ id -> partialInsts.get(idT).toSeq.flatten.flatMap { case (b, m) => wrapped.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
+ case (l, domain) => l -> domain.flatMap { case (b, m) => wrapped.extract(b, m) }.toSet
}
- val model = extractModel(wrapped)
- val asDMap = purescala.Quantification.extractModel(model.toMap, funDomains, typeDomains, evaluator)
+ val model = new Model(freeVars.toMap.map { case (id, _) =>
+ val value = wrapped.get(id).get
+ id -> (funDomains.get(id) match {
+ case Some(domain) =>
+ val FiniteLambda(_, dflt, tpe) = value
+ FiniteLambda(domain.toSeq.map { es =>
+ val optEv = evaluator.eval(application(value, es)).result
+ es -> optEv.getOrElse(scala.sys.error("Unexpectedly failed to evaluate " + application(value, es)))
+ }, dflt, tpe)
+
+ case None => postMap {
+ case p @ FiniteLambda(mapping, dflt, tpe) =>
+ Some(FiniteLambda(typeDomains.get(tpe) match {
+ case Some(domain) => domain.toSeq.map { es =>
+ val optEv = evaluator.eval(application(value, es)).result
+ es -> optEv.getOrElse(scala.sys.error("Unexpectedly failed to evaluate " + application(value, es)))
+ }
+ case _ => Seq.empty
+ }, dflt, tpe))
+ case _ => None
+ } (value)
+ })
+ })
+
val domains = new HenkinDomains(lambdaDomains, typeDomains)
- new HenkinModel(asDMap, domains)
+ new HenkinModel(model.toMap, domains)
}
- private def getTotalModel(silenceErrors: Boolean = false): (Boolean, Model) = {
- if (interrupted) {
- (false, Model.empty)
- } else {
- var valid = false
- var wrapper = solverGetModel
+ private def getTotalModel: Model = {
+ val wrapped = solverGetModel
- val clauses = templateGenerator.manager.checkClauses
- if (clauses.isEmpty) {
- valid = true
- } else {
- reporter.debug(" - Verifying model transitivity")
+ val typeInsts = templateGenerator.manager.typeInstantiations
+ val partialInsts = templateGenerator.manager.partialInstantiations
- val timer = context.timers.solvers.check.start()
- solverCheck(clauses) { res =>
- timer.stop()
+ def extractCond(params: Seq[Identifier], args: Seq[(T, Expr)], structure: Map[T, Identifier]): Seq[Expr] = (params, args) match {
+ case (id +: rparams, (v, arg) +: rargs) =>
+ if (templateGenerator.manager.isQuantifier(v)) {
+ structure.get(v) match {
+ case Some(pid) => Equals(Variable(id), Variable(pid)) +: extractCond(rparams, rargs, structure)
+ case None => extractCond(rparams, rargs, structure + (v -> id))
+ }
+ } else {
+ Equals(Variable(id), arg) +: extractCond(rparams, rargs, structure)
+ }
+ case _ => Seq.empty
+ }
- reporter.debug(" - Finished transitivity check")
+ new Model(freeVars.toMap.map { case (id, idT) =>
+ val value = wrapped.get(id).get
+ id -> (id.getType match {
+ case FunctionType(from, to) =>
+ val params = from.map(tpe => FreshIdentifier("x", tpe, true))
+ val domain = partialInsts.get(idT).orElse(typeInsts.get(bestRealType(id.getType))).toSeq.flatten
+ val conditionals = domain.flatMap { case (b, m) =>
+ wrapped.extract(b, m) match {
+ case Some(args) =>
+ val result = evaluator.eval(application(value, args)).result.getOrElse {
+ scala.sys.error("Unexpectedly failed to evaluate " + application(value, args))
+ }
- res match {
- case Some(true) =>
- wrapper = solverGetModel
- valid = true
+ val c1 = (params zip args).map(p => Equals(Variable(p._1), p._2))
+ if (m.args.exists(arg => templateGenerator.manager.isQuantifier(arg.encoded))) {
+ val c2 = extractCond(params, m.args.map(_.encoded) zip args, Map.empty)
+ Seq(c1 -> result, c2 -> result)
+ } else {
+ Seq(c1 -> result)
+ }
- case Some(false) =>
- emit(silenceErrors)(" - Transitivity independence not guaranteed for model")
+ case None => Seq.empty
+ }
+ }
- case None =>
- emit(silenceErrors)(" - Unknown for transitivity independence!?")
+ val filteredConds = conditionals
+ .foldLeft(Map.empty[Seq[Expr], Expr]) { case (mapping, (conds, result)) =>
+ if (mapping.isDefinedAt(conds)) mapping else mapping + (conds -> result)
+ }
+
+ val rest :+ ((_, dflt)) = filteredConds.toSeq.sortBy(_._1.size)
+ val body = rest.foldLeft(dflt) { case (elze, (conds, res)) =>
+ if (conds.isEmpty) elze else IfExpr(andJoin(conds), res, elze)
}
- }
- }
- (valid, extractModel(wrapper))
- }
+ Lambda(params.map(ValDef(_)), body)
+
+ case _ => value
+ })
+ })
}
def genericCheck(assumptions: Set[Expr]): Option[Boolean] = {
@@ -291,9 +340,13 @@ trait AbstractUnrollingSolver[T]
while(!foundDefinitiveAnswer && !interrupted) {
reporter.debug(" - Running search...")
+ var quantify = false
+
+ def check[R](clauses: Seq[T])(block: Option[Boolean] => R) =
+ if (partialModels) solverCheckAssumptions(clauses)(block) else solverCheck(clauses)(block)
val timer = context.timers.solvers.check.start()
- solverCheckAssumptions(encodedAssumptions.toSeq ++ unrollingBank.satisfactionAssumptions) { res =>
+ check(encodedAssumptions.toSeq ++ unrollingBank.satisfactionAssumptions) { res =>
timer.stop()
reporter.debug(" - Finished search with blocked literals")
@@ -303,10 +356,37 @@ trait AbstractUnrollingSolver[T]
foundAnswer(None)
case Some(true) => // SAT
- val (stop, model) = if (!partialModels) {
- getTotalModel(silenceErrors = true)
- } else {
+ val (stop, model) = if (interrupted) {
+ (true, Model.empty)
+ } else if (partialModels) {
(true, getPartialModel)
+ } else {
+ val clauses = templateGenerator.manager.checkClauses
+ if (clauses.isEmpty) {
+ (true, extractModel(solverGetModel))
+ } else {
+ reporter.debug(" - Verifying model transitivity")
+
+ val timer = context.timers.solvers.check.start()
+ solverCheck(clauses) { res =>
+ timer.stop()
+
+ reporter.debug(" - Finished transitivity check")
+
+ res match {
+ case Some(true) =>
+ (true, getTotalModel)
+
+ case Some(false) =>
+ reporter.debug(" - Transitivity not guaranteed for model")
+ (false, Model.empty)
+
+ case None =>
+ reporter.warning(" - Unknown for transitivity!?")
+ (false, Model.empty)
+ }
+ }
+ }
}
if (!interrupted) {
@@ -316,15 +396,7 @@ trait AbstractUnrollingSolver[T]
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")
+ quantify = true
}
} else {
val valid = !checkModels || validateModel(model, assumptionsSeq, silenceErrors = false)
@@ -366,66 +438,74 @@ trait AbstractUnrollingSolver[T]
reporter.fatalError("Can't unroll unsat core for incompatible solver " + name)
}
}
+ }
+ }
- 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)")
+ if (!quantify && !foundDefinitiveAnswer && !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)")
+ }
+
+ 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))
}
- 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(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)
}
- }
- if (interrupted) {
+ case None =>
foundAnswer(None)
- }
+ }
+ }
+ }
- if (!foundDefinitiveAnswer) {
- reporter.debug("- We need to keep going")
+ if (!foundDefinitiveAnswer && !interrupted) {
+ reporter.debug("- We need to keep going")
- // unfolling `unfoldFactor` times
- for (i <- 1 to unfoldFactor.toInt) {
- val toRelease = unrollingBank.getBlockersToUnlock
+ if (quantify) {
+ // further quantifier instantiations are required!
+ val newClauses = unrollingBank.instantiateQuantifiers
+ reporter.debug(" - more instantiations")
- reporter.debug(" - more unrollings")
+ for (cls <- newClauses) {
+ solverAssert(cls)
+ }
- val newClauses = unrollingBank.unrollBehind(toRelease)
+ reporter.debug(" - finished instantiating")
+ } else {
+ // unfolling `unfoldFactor` times
+ for (i <- 1 to unfoldFactor.toInt) {
+ val toRelease = unrollingBank.getBlockersToUnlock
- for (ncl <- newClauses) {
- solverAssert(ncl)
- }
- }
+ reporter.debug(" - more unrollings")
+
+ val newClauses = unrollingBank.unrollBehind(toRelease)
- reporter.debug(" - finished unrolling")
+ for (ncl <- newClauses) {
+ solverAssert(ncl)
}
+ }
+
+ reporter.debug(" - finished unrolling")
}
}
}
diff --git a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
index 602873aba9df1859650ee94486c59d9487ec7fbd..eea7c80a08dc5c6a05ebb448671b41735ea0c2d8 100644
--- a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
@@ -128,7 +128,7 @@ trait Z3StringEvaluatingSolver[TUnderlying <: EvaluatingSolver] extends Evaluati
trait Z3StringQuantificationSolver[TUnderlying <: QuantificationSolver] extends QuantificationSolver { self: Z3StringCapableSolver[TUnderlying] =>
// Members declared in leon.solvers.QuantificationSolver
- override def getModel: leon.solvers.HenkinModel = {
+ override def getModel = {
val model = underlying.getModel
someConverter map { converter =>
val ids = model.ids.toSeq
@@ -136,41 +136,39 @@ trait Z3StringQuantificationSolver[TUnderlying <: QuantificationSolver] extends
import converter.Backward._
val original_ids = ids.map(convertId)
val original_exprs = exprs.map{ case e => convertExpr(e)(Map()) }
+
+ model match {
+ case hm: HenkinModel =>
+ val new_domain = new HenkinDomains(
+ hm.doms.lambdas.map(kv =>
+ (convertExpr(kv._1)(Map()).asInstanceOf[Lambda],
+ kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap,
+ hm.doms.tpes.map(kv =>
+ (convertType(kv._1),
+ kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap
+ )
- val new_domain = new HenkinDomains(
- model.doms.lambdas.map(kv =>
- (convertExpr(kv._1)(Map()).asInstanceOf[Lambda],
- kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap,
- model.doms.tpes.map(kv =>
- (convertType(kv._1),
- kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap
- )
-
- new HenkinModel(original_ids.zip(original_exprs).toMap, new_domain)
+ new HenkinModel(original_ids.zip(original_exprs).toMap, new_domain)
+ case _ => model
+ }
} getOrElse model
}
}
-trait EvaluatorCheckConverter extends DeterministicEvaluator {
- def converter: Z3StringConversion
- abstract override def check(expression: Expr, model: solvers.Model) : CheckResult = {
- val c = converter
- import c.Backward._ // Because the evaluator is going to be called by the underlying solver, but it will use the original program
- super.check(convertExpr(expression)(Map()), convertModel(model))
- }
-}
-
class ConvertibleCodeGenEvaluator(context: LeonContext, originalProgram: Program, val converter: Z3StringConversion)
- extends CodeGenEvaluator(context, originalProgram) with EvaluatorCheckConverter {
+ extends CodeGenEvaluator(context, originalProgram) {
+
override def compile(expression: Expr, args: Seq[Identifier]) : Option[solvers.Model=>EvaluationResult] = {
import converter._
super.compile(Backward.convertExpr(expression)(Map()), args.map(Backward.convertId))
- .map(evaluator => (m: Model) => Forward.convertResult(evaluator(Backward.convertModel(m)))
+ .map(evaluator => (m: Model) => Forward.convertResult(evaluator(Backward.convertModel(m)))
)
}
}
-class ConvertibleDefaultEvaluator(context: LeonContext, originalProgram: Program, val converter: Z3StringConversion) extends DefaultEvaluator(context, originalProgram) with EvaluatorCheckConverter {
+class ConvertibleDefaultEvaluator(context: LeonContext, originalProgram: Program, val converter: Z3StringConversion)
+ extends DefaultEvaluator(context, originalProgram) {
+
override def eval(ex: Expr, model: Model): EvaluationResults.Result[Expr] = {
import converter._
Forward.convertResult(super.eval(Backward.convertExpr(ex)(Map()), Backward.convertModel(model)))
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 87cc849b41d2507d7e0ca53a351b2f605d387b46..03cf3aef32fc59c33283c70cebfa2f918e549e76 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -63,7 +63,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
RawArrayValue(k, Map(), fromSMT(elem, v))
case ft @ FunctionType(from, to) =>
- PartialLambda(Seq.empty, Some(fromSMT(elem, to)), ft)
+ FiniteLambda(Seq.empty, fromSMT(elem, to), ft)
case MapType(k, v) =>
FiniteMap(Map(), k, v)
@@ -75,7 +75,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
RawArrayValue(k, Map(), fromSMT(elem, v))
case ft @ FunctionType(from, to) =>
- PartialLambda(Seq.empty, Some(fromSMT(elem, to)), ft)
+ FiniteLambda(Seq.empty, fromSMT(elem, to), ft)
case MapType(k, v) =>
FiniteMap(Map(), k, v)
@@ -88,9 +88,9 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
RawArrayValue(k, elems + (fromSMT(key, k) -> fromSMT(elem, v)), base)
case FunctionType(from, v) =>
- val PartialLambda(mapping, dflt, ft) = fromSMT(arr, otpe)
+ val FiniteLambda(mapping, dflt, ft) = fromSMT(arr, otpe)
val args = unwrapTuple(fromSMT(key, tupleTypeWrap(from)), from.size)
- PartialLambda(mapping :+ (args -> fromSMT(elem, v)), dflt, ft)
+ FiniteLambda(mapping :+ (args -> fromSMT(elem, v)), dflt, ft)
case MapType(k, v) =>
val FiniteMap(elems, k, v) = fromSMT(arr, otpe)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index d05b45c35e2e3847be4e1a6650c779de91da91d9..d239de90dd2b7060d92fe407a7070f8a6b88d74d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -206,7 +206,7 @@ trait SMTLIBTarget extends Interruptible {
case ft @ FunctionType(from, to) =>
val elems = r.elems.toSeq.map { case (k, v) => unwrapTuple(k, from.size) -> v }
- PartialLambda(elems, Some(r.default), ft)
+ FiniteLambda(elems, r.default, ft)
case MapType(from, to) =>
// We expect a RawArrayValue with keys in from and values in Option[to],
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 1662596002ac49202f10206cec6a338fc7377116..5262ab9c72aaf3ccc677ad1124ad8a28fd424fa8 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -11,6 +11,7 @@ import purescala.Constructors._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Types._
+import purescala.TypeOps._
import purescala.Quantification.{QuantificationTypeMatcher => QTM}
import Instantiation._
@@ -134,15 +135,23 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private val quantifications = new IncrementalSeq[MatcherQuantification]
private val instCtx = new InstantiationContext
- private val handled = new ContextMap
- private val ignored = new ContextMap
+ private val ignoredMatchers = new ContextMap
+ private val ignoredSubsts = new IncrementalMap[MatcherQuantification, MutableSet[(Int, Set[T], Map[T,Arg[T]])]]
+ private val handledSubsts = new IncrementalMap[MatcherQuantification, MutableSet[(Set[T], Map[T,Arg[T]])]]
private val known = new IncrementalSet[T]
- private val lambdaAxioms = new IncrementalSet[(LambdaTemplate[T], Seq[(Identifier, T)])]
+ private val lambdaAxioms = new IncrementalSet[((Expr, Seq[T]), Seq[(Identifier, T)])]
private val templates = new IncrementalMap[(Expr, Seq[T]), T]
override protected def incrementals: List[IncrementalState] =
- List(quantifications, instCtx, handled, ignored, known, lambdaAxioms, templates) ++ super.incrementals
+ List(quantifications, instCtx, ignoredMatchers, ignoredSubsts,
+ handledSubsts, known, lambdaAxioms, templates) ++ super.incrementals
+
+ private var currentGen = 0
+ private def minGen = {
+ val gens = ignoredSubsts.toSeq.flatMap(_._2).map(_._1)
+ if (gens.isEmpty) currentGen else gens.min
+ }
private sealed abstract class MatcherKey(val tpe: TypeTree)
private case class CallerKey(caller: T, tt: TypeTree) extends MatcherKey(tt)
@@ -167,42 +176,45 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private val uniformQuantSet: MutableSet[T] = MutableSet.empty
def isQuantifier(idT: T): Boolean = uniformQuantSet(idT)
- private def uniformSubst(qs: Seq[(Identifier, T)]): Map[T, T] = {
- qs.groupBy(_._1.getType).flatMap { case (tpe, qst) =>
+ def uniformQuants(ids: Seq[Identifier]): Seq[T] = {
+ val mapping = ids.groupBy(id => bestRealType(id.getType)).flatMap { case (tpe, idst) =>
val prev = uniformQuantMap.get(tpe) match {
case Some(seq) => seq
case None => Seq.empty
}
- if (prev.size >= qst.size) {
- qst.map(_._2) zip prev.take(qst.size)
+ if (prev.size >= idst.size) {
+ idst zip prev.take(idst.size)
} else {
- val (handled, newQs) = qst.splitAt(prev.size)
- val uQs = newQs.map(p => p._2 -> encoder.encodeId(p._1))
+ val (handled, newIds) = idst.splitAt(prev.size)
+ val uIds = newIds.map(id => id -> encoder.encodeId(id))
- uniformQuantMap(tpe) = prev ++ uQs.map(_._2)
- uniformQuantSet ++= uQs.map(_._2)
+ uniformQuantMap(tpe) = prev ++ uIds.map(_._2)
+ uniformQuantSet ++= uIds.map(_._2)
- (handled.map(_._2) zip prev) ++ uQs
+ (handled zip prev) ++ uIds
}
}.toMap
+
+ ids.map(mapping)
+ }
+
+ private def uniformSubst(qs: Seq[(Identifier, T)]): Map[T, T] = {
+ (qs.map(_._2) zip uniformQuants(qs.map(_._1))).toMap
}
def assumptions: Seq[T] = quantifications.collect { case q: Quantification => q.currentQ2Var }.toSeq
- def instantiations: (Map[TypeTree, Matchers], Map[T, Matchers], Map[Lambda, Matchers]) = {
- var typeInsts: Map[TypeTree, Matchers] = Map.empty
- var partialInsts: Map[T, Matchers] = Map.empty
- var lambdaInsts: Map[Lambda, Matchers] = Map.empty
+ def typeInstantiations: Map[TypeTree, Matchers] = instCtx.map.instantiations.collect {
+ case (TypeKey(tpe), matchers) => tpe -> matchers
+ }
- val instantiations = handled.instantiations ++ instCtx.map.instantiations
- for ((key, matchers) <- instantiations) key match {
- case TypeKey(tpe) => typeInsts += tpe -> matchers
- case CallerKey(caller, _) => partialInsts += caller -> matchers
- case LambdaKey(lambda, _) => lambdaInsts += lambda -> matchers
- }
+ def lambdaInstantiations: Map[Lambda, Matchers] = instCtx.map.instantiations.collect {
+ case (LambdaKey(lambda, tpe), matchers) => lambda -> (matchers ++ instCtx.map.get(TypeKey(tpe)).toMatchers)
+ }
- (typeInsts, partialInsts, lambdaInsts)
+ def partialInstantiations: Map[T, Matchers] = instCtx.map.instantiations.collect {
+ case (CallerKey(caller, tpe), matchers) => caller -> (matchers ++ instCtx.map.get(TypeKey(tpe)).toMatchers)
}
override def registerFree(ids: Seq[(Identifier, T)]): Unit = {
@@ -351,7 +363,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private trait MatcherQuantification {
val pathVar: (Identifier, T)
- val quantified: Set[T]
+ val quantifiers: Seq[(Identifier, T)]
val matchers: Set[Matcher[T]]
val allMatchers: Map[T, Set[Matcher[T]]]
val condVars: Map[Identifier, T]
@@ -362,6 +374,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val applications: Map[T, Set[App[T]]]
val lambdas: Seq[LambdaTemplate[T]]
+ lazy val quantified: Set[T] = quantifiers.map(_._2).toSet
lazy val start = pathVar._2
private lazy val depth = matchers.map(matcherDepth).max
@@ -455,43 +468,68 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
for (mapping <- mappings(bs, matcher)) {
val (enablers, subst, isStrict) = extractSubst(mapping)
+
+ if (!skip(subst)) {
+ if (!isStrict) {
+ ignoreSubst(enablers, subst)
+ } else {
+ instantiation ++= instantiateSubst(enablers, subst, strict = true)
+ }
+ }
+ }
+
+ instantiation
+ }
+
+ def instantiateSubst(enablers: Set[T], subst: Map[T, Arg[T]], strict: Boolean = false): Instantiation[T] = {
+ if (handledSubsts(this)(enablers -> subst)) {
+ Instantiation.empty[T]
+ } else {
+ handledSubsts(this) += enablers -> subst
+
+ var instantiation = Instantiation.empty[T]
val (enabler, optEnabler) = freshBlocker(enablers)
+ if (optEnabler.isDefined) {
+ instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
+ }
- val baseSubst = subst ++ instanceSubst(enablers).mapValues(Left(_))
+ val baseSubst = subst ++ instanceSubst(enabler).mapValues(Left(_))
val (substMap, inst) = Template.substitution(encoder, QuantificationManager.this,
condVars, exprVars, condTree, Seq.empty, lambdas, baseSubst, pathVar._1, enabler)
+ instantiation ++= inst
- if (!skip(substMap)) {
- if (optEnabler.isDefined) {
- instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
- }
+ val msubst = substMap.collect { case (c, Right(m)) => c -> m }
+ val substituter = encoder.substitute(substMap.mapValues(_.encoded))
+ instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
+ clauses, blockers, applications, Seq.empty, Map.empty, lambdas, substMap)
- instantiation ++= inst
- instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
- clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
+ for ((b,ms) <- allMatchers; m <- ms) {
+ val sb = enablers ++ (if (b == start) Set.empty else Set(substituter(b)))
+ val sm = m.substitute(substituter, msubst)
- val msubst = substMap.collect { case (c, Right(m)) => c -> m }
- val substituter = encoder.substitute(substMap.mapValues(_.encoded))
-
- for ((b,ms) <- allMatchers; m <- ms) {
- val sb = enablers ++ (if (b == start) Set.empty else Set(substituter(b)))
- val sm = m.substitute(substituter, msubst)
-
- if (matchers(m)) {
- handled += sb -> sm
- } else if (transMatchers(m) && isStrict) {
- instantiation ++= instCtx.instantiate(sb, sm)(quantifications.toSeq : _*)
- } else {
- ignored += sb -> sm
- }
+ if (strict && (matchers(m) || transMatchers(m))) {
+ instantiation ++= instCtx.instantiate(sb, sm)(quantifications.toSeq : _*)
+ } else if (!matchers(m)) {
+ ignoredMatchers += sb -> sm
}
}
+
+ instantiation
}
+ }
- instantiation
+ def ignoreSubst(enablers: Set[T], subst: Map[T, Arg[T]]): Unit = {
+ val msubst = subst.collect { case (c, Right(m)) => c -> m }
+ val substituter = encoder.substitute(subst.mapValues(_.encoded))
+ val nextGen = (if (matchers.forall { m =>
+ val sm = m.substitute(substituter, msubst)
+ instCtx(enablers -> sm)
+ }) currentGen + 3 else currentGen + 5)
+
+ ignoredSubsts(this) += ((nextGen, enablers, subst))
}
- protected def instanceSubst(enablers: Set[T]): Map[T, T]
+ protected def instanceSubst(enabler: T): Map[T, T]
protected def skip(subst: Map[T, Arg[T]]): Boolean = false
}
@@ -502,7 +540,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val q2s: (Identifier, T),
val insts: (Identifier, T),
val guardVar: T,
- val quantified: Set[T],
+ val quantifiers: Seq[(Identifier, T)],
val matchers: Set[Matcher[T]],
val allMatchers: Map[T, Set[Matcher[T]]],
val condVars: Map[Identifier, T],
@@ -515,10 +553,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
var currentQ2Var: T = qs._2
- protected def instanceSubst(enablers: Set[T]): Map[T, T] = {
+ protected def instanceSubst(enabler: T): Map[T, T] = {
val nextQ2Var = encoder.encodeId(q2s._1)
- val subst = Map(qs._2 -> currentQ2Var, guardVar -> encodeEnablers(enablers),
+ val subst = Map(qs._2 -> currentQ2Var, guardVar -> enabler,
q2s._2 -> nextQ2Var, insts._2 -> encoder.encodeId(insts._1))
currentQ2Var = nextQ2Var
@@ -547,7 +585,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val pathVar: (Identifier, T),
val blocker: T,
val guardVar: T,
- val quantified: Set[T],
+ val quantifiers: Seq[(Identifier, T)],
val matchers: Set[Matcher[T]],
val allMatchers: Map[T, Set[Matcher[T]]],
val condVars: Map[Identifier, T],
@@ -558,11 +596,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val applications: Map[T, Set[App[T]]],
val lambdas: Seq[LambdaTemplate[T]]) extends MatcherQuantification {
- protected def instanceSubst(enablers: Set[T]): Map[T, T] = {
- // no need to add an equality clause here since it is already contained in the Axiom clauses
- val (newBlocker, optEnabler) = freshBlocker(enablers)
- val guardT = if (optEnabler.isDefined) encoder.mkAnd(start, optEnabler.get) else start
- Map(guardVar -> guardT, blocker -> newBlocker)
+ protected def instanceSubst(enabler: T): Map[T, T] = {
+ Map(guardVar -> start, blocker -> enabler)
}
override protected def skip(subst: Map[T, Arg[T]]): Boolean = {
@@ -599,14 +634,26 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
def instantiateAxiom(template: LambdaTemplate[T], substMap: Map[T, Arg[T]]): Instantiation[T] = {
- val quantifiers = template.arguments flatMap {
- case (id, idT) => substMap(idT).left.toOption.map(id -> _)
- } filter (p => isQuantifier(p._2))
+ def quantifiedMatcher(m: Matcher[T]): Boolean = m.args.exists(a => a match {
+ case Left(v) => isQuantifier(v)
+ case Right(m) => quantifiedMatcher(m)
+ })
+
+ val quantified = template.arguments flatMap {
+ case (id, idT) => substMap(idT) match {
+ case Left(v) if isQuantifier(v) => Some(id)
+ case Right(m) if quantifiedMatcher(m) => Some(id)
+ case _ => None
+ }
+ }
+
+ val quantifiers = quantified zip uniformQuants(quantified)
+ val key = template.key -> quantifiers
- if (quantifiers.isEmpty || lambdaAxioms(template -> quantifiers)) {
+ if (quantifiers.isEmpty || lambdaAxioms(key)) {
Instantiation.empty[T]
} else {
- lambdaAxioms += template -> quantifiers
+ lambdaAxioms += key
val blockerT = encoder.encodeId(blockerId)
val guard = FreshIdentifier("guard", BooleanType, true)
@@ -676,12 +723,14 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
var instantiation = Instantiation.empty[T]
for (matchers <- matchQuorums) {
- val axiom = new LambdaAxiom(pathVar, blocker, guardVar, quantified,
+ val axiom = new LambdaAxiom(pathVar, blocker, guardVar, quantifiers,
matchers, allMatchers, condVars, exprVars, condTree,
clauses, blockers, applications, lambdas
)
quantifications += axiom
+ handledSubsts += axiom -> MutableSet.empty
+ ignoredSubsts += axiom -> MutableSet.empty
val newCtx = new InstantiationContext()
for ((b,m) <- instCtx.instantiated) {
@@ -722,13 +771,15 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
template.pathVar,
template.qs._1 -> newQ,
template.q2s, template.insts, template.guardVar,
- quantified, matchers, template.matchers,
+ template.quantifiers, matchers, template.matchers,
template.condVars, template.exprVars, template.condTree,
template.clauses map substituter, // one clause depends on 'q' (and therefore 'newQ')
template.blockers, template.applications, template.lambdas
)
quantifications += quantification
+ handledSubsts += quantification -> MutableSet.empty
+ ignoredSubsts += quantification -> MutableSet.empty
val newCtx = new InstantiationContext()
for ((b,m) <- instCtx.instantiated) {
@@ -765,71 +816,108 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
instCtx.instantiate(Set(blocker), matcher)(quantifications.toSeq : _*)
}
- def hasIgnored: Boolean = ignored.nonEmpty
+ def hasIgnored: Boolean = ignoredSubsts.nonEmpty || ignoredMatchers.nonEmpty
def instantiateIgnored: Instantiation[T] = {
var instantiation = Instantiation.empty[T]
- for ((b,m) <- ignored.consume) {
+ for ((b,m) <- ignoredMatchers.consume) {
instantiation ++= instantiateMatcher(b, m)
}
+
+ val min = minGen
+ val toRelease = quantifications.toList.flatMap { q =>
+ val qsubsts = ignoredSubsts(q)
+ qsubsts.toList.flatMap { case e @ (gen, enablers, subst) =>
+ if (gen == min) {
+ qsubsts -= e
+ Some((q, enablers, subst))
+ } else {
+ None
+ }
+ }
+ }
+
+ for ((q, enablers, subst) <- toRelease) {
+ instantiation ++= q.instantiateSubst(enablers, subst, strict = false)
+ }
+
+ // Note that minGen changed after removing stuff from ignoredSubsts!
+ currentGen = minGen
instantiation
}
- private type SetDef = (T, (Identifier, T), (Identifier, T), Seq[T], T, T, T)
- private val setConstructors: MutableMap[TypeTree, SetDef] = MutableMap.empty
-
def checkClauses: Seq[T] = {
val clauses = new scala.collection.mutable.ListBuffer[T]
+ //val keySets = scala.collection.mutable.Map.empty[MatcherKey, T]
+ val keyClause = MutableMap.empty[MatcherKey, (Seq[T], T)]
- for ((key, ctx) <- ignored.instantiations) {
- val insts = instCtx.map.get(key).toMatchers
-
+ for ((key, ctx) <- ignoredMatchers.instantiations) {
val QTM(argTypes, _) = key.tpe
- val tupleType = tupleTypeWrap(argTypes)
-
- val (guardT, (setPrev, setPrevT), (setNext, setNextT), elems, containsT, emptyT, setT) =
- setConstructors.getOrElse(tupleType, {
- val guard = FreshIdentifier("guard", BooleanType)
- val setPrev = FreshIdentifier("prevSet", SetType(tupleType))
- val setNext = FreshIdentifier("nextSet", SetType(tupleType))
- val elems = argTypes.map(tpe => FreshIdentifier("elem", tpe))
-
- val elemExpr = tupleWrap(elems.map(_.toVariable))
- val contextExpr = And(
- Implies(Variable(guard), Equals(Variable(setNext),
- SetUnion(Variable(setPrev), FiniteSet(Set(elemExpr), tupleType)))),
- Implies(Not(Variable(guard)), Equals(Variable(setNext), Variable(setPrev))))
-
- val guardP = guard -> encoder.encodeId(guard)
- val setPrevP = setPrev -> encoder.encodeId(setPrev)
- val setNextP = setNext -> encoder.encodeId(setNext)
- val elemsP = elems.map(e => e -> encoder.encodeId(e))
-
- val containsT = encoder.encodeExpr(elemsP.toMap + setPrevP)(ElementOfSet(elemExpr, setPrevP._1.toVariable))
- val emptyT = encoder.encodeExpr(Map.empty)(FiniteSet(Set.empty, tupleType))
- val contextT = encoder.encodeExpr(Map(guardP, setPrevP, setNextP) ++ elemsP)(contextExpr)
-
- val setDef = (guardP._2, setPrevP, setNextP, elemsP.map(_._2), containsT, emptyT, contextT)
- setConstructors += key.tpe -> setDef
- setDef
- })
-
- var prev = emptyT
- for ((b, m) <- insts.toSeq) {
- val next = encoder.encodeId(setNext)
- val argsMap = (elems zip m.args).map { case (idT, arg) => idT -> arg.encoded }
- val substMap = Map(guardT -> b, setPrevT -> prev, setNextT -> next) ++ argsMap
- prev = next
- clauses += encoder.substitute(substMap)(setT)
- }
- val setMap = Map(setPrevT -> prev)
+ val (values, clause) = keyClause.getOrElse(key, {
+ val insts = instCtx.map.get(key).toMatchers
+
+ val guard = FreshIdentifier("guard", BooleanType)
+ val elems = argTypes.map(tpe => FreshIdentifier("elem", tpe))
+ val values = argTypes.map(tpe => FreshIdentifier("value", tpe))
+ val expr = andJoin(Variable(guard) +: (elems zip values).map(p => Equals(Variable(p._1), Variable(p._2))))
+
+ val guardP = guard -> encoder.encodeId(guard)
+ val elemsP = elems.map(e => e -> encoder.encodeId(e))
+ val valuesP = values.map(v => v -> encoder.encodeId(v))
+ val exprT = encoder.encodeExpr(elemsP.toMap ++ valuesP + guardP)(expr)
+
+ val disjuncts = insts.toSeq.map { case (b, m) =>
+ val subst = (elemsP.map(_._2) zip m.args.map(_.encoded)).toMap + (guardP._2 -> b)
+ encoder.substitute(subst)(exprT)
+ }
+
+ val res = (valuesP.map(_._2), encoder.mkOr(disjuncts : _*))
+ keyClause += key -> res
+ res
+ })
+
for ((b, m) <- ctx.toSeq) {
- val substMap = setMap ++ (elems zip m.args).map(p => p._1 -> p._2.encoded)
- clauses += encoder.substitute(substMap)(encoder.mkImplies(b, containsT))
+ val substMap = (values zip m.args.map(_.encoded)).toMap
+ clauses += encoder.substitute(substMap)(encoder.mkImplies(b, clause))
}
}
+ for (q <- quantifications) {
+ val guard = FreshIdentifier("guard", BooleanType)
+ val elems = q.quantifiers.map(_._1)
+ val values = elems.map(id => id.freshen)
+ val expr = andJoin(Variable(guard) +: (elems zip values).map(p => Equals(Variable(p._1), Variable(p._2))))
+
+ val guardP = guard -> encoder.encodeId(guard)
+ val elemsP = elems.map(e => e -> encoder.encodeId(e))
+ val valuesP = values.map(v => v -> encoder.encodeId(v))
+ val exprT = encoder.encodeExpr(elemsP.toMap ++ valuesP + guardP)(expr)
+
+ val disjunction = encoder.mkOr(handledSubsts(q).toSeq.map { case (enablers, subst) =>
+ val b = if (enablers.isEmpty) trueT else encoder.mkAnd(enablers.toSeq : _*)
+ val substMap = (elemsP.map(_._2) zip q.quantifiers.map(p => subst(p._2).encoded)).toMap + (guardP._2 -> b)
+ encoder.substitute(substMap)(exprT)
+ } : _*)
+
+ for ((_, enablers, subst) <- ignoredSubsts(q)) {
+ val b = if (enablers.isEmpty) trueT else encoder.mkAnd(enablers.toSeq : _*)
+ val substMap = (valuesP.map(_._2) zip q.quantifiers.map(p => subst(p._2).encoded)).toMap
+ clauses += encoder.substitute(substMap)(encoder.mkImplies(b, disjunction))
+ }
+ }
+
+ for ((key, ctx) <- instCtx.map.instantiations) {
+ val QTM(argTypes, _) = key.tpe
+
+ for {
+ (tpe,idx) <- argTypes.zipWithIndex
+ quants <- uniformQuantMap.get(tpe) if quants.nonEmpty
+ (b, m) <- ctx
+ arg = m.args(idx).encoded if !isQuantifier(arg)
+ } clauses += encoder.mkAnd(quants.map(q => encoder.mkNot(encoder.mkEquals(q, arg))) : _*)
+ }
+
clauses.toSeq
}
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 2ab8f2b2b52dbf2cc335519e481ed7954e2fa3d6..b9c95ba768064133a64c61ae64efd85360d1fb07 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -398,7 +398,6 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
}
case c @ Choose(Lambda(params, cond)) =>
-
val cs = params.map(_.id.freshen.toVariable)
for (c <- cs) {
@@ -411,6 +410,14 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
tupleWrap(cs)
+ case FiniteLambda(mapping, dflt, FunctionType(from, to)) =>
+ val args = from.map(tpe => FreshIdentifier("x", tpe))
+ val body = mapping.toSeq.foldLeft(dflt) { case (elze, (exprs, res)) =>
+ IfExpr(andJoin((args zip exprs).map(p => Equals(Variable(p._1), p._2))), res, elze)
+ }
+
+ rec(pathVar, Lambda(args.map(ValDef(_)), body))
+
case l @ Lambda(args, body) =>
val idArgs : Seq[Identifier] = lambdaArgs(l)
val trArgs : Seq[T] = idArgs.map(id => substMap.getOrElse(id, encoder.encodeId(id)))
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 893b39cb82e71bace9f4b26c2696188f825a031f..ce2af7c9e29634ff5a50dc4b493477c63f774229 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -235,7 +235,8 @@ 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
+ val gens = (callInfos.values.map(_._1) ++ appInfos.values.map(_._1))
+ val gen = if (gens.nonEmpty) gens.min else 0
for ((b, newInfos) <- callBlocks) {
registerCallBlocker(nextGeneration(gen), b, newInfos)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index e2d1ab0fae778878845fa51f85786325a0041c54..f1ee6bfba315c53f4e094a95959039f2c6f7ed72 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -678,13 +678,13 @@ trait AbstractZ3Solver extends Solver {
case None => simplestValue(ft)
case Some((_, mapping, elseValue)) =>
val leonElseValue = rec(elseValue, tt)
- PartialLambda(mapping.flatMap { case (z3Args, z3Result) =>
+ FiniteLambda(mapping.flatMap { case (z3Args, z3Result) =>
if (t == z3Args.head) {
List((z3Args.tail zip fts).map(p => rec(p._1, p._2)) -> rec(z3Result, tt))
} else {
Nil
}
- }, Some(leonElseValue), ft)
+ }, leonElseValue, ft)
}
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 812812aa3f4b39a9f3e2994d46080d4b009c0067..7ba4bf9eade43bc1f567e447c067a1e61bf16360 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -35,6 +35,9 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
protected def hasError = errors.getB(()) contains true
protected def addError() = errors += () -> true
+ override val name = "Z3-f"
+ override val description = "Fair Z3 Solver"
+
override protected val reporter = context.reporter
override def reset(): Unit = super[AbstractZ3Solver].reset()
@@ -55,12 +58,14 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
r
}
+ /*
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)
}
+ */
def solverGetModel: ModelWrapper = new ModelWrapper {
val model = solver.getModel
diff --git a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
index 21df018db70935ad63b6c22e7d6bc77894005b23..be5f61fe997c7223fee7ad548c4a700b74597062 100644
--- a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
+++ b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
@@ -185,11 +185,11 @@ trait Z3StringConverters { self: Z3StringConversion =>
case Variable(id) if bindings contains id => bindings(id).copiedFrom(e)
case Variable(id) if hasIdConversion(id) => Variable(convertId(id)).copiedFrom(e)
case Variable(id) => e
- case pl@PartialLambda(mappings, default, tpe) =>
- PartialLambda(
+ case pl @ FiniteLambda(mappings, default, tpe) =>
+ FiniteLambda(
mappings.map(kv => (kv._1.map(argtpe => convertExpr(argtpe)),
convertExpr(kv._2))),
- default.map(d => convertExpr(d)), convertType(tpe).asInstanceOf[FunctionType])
+ convertExpr(default), convertType(tpe).asInstanceOf[FunctionType])
case Lambda(args, body) =>
println("Converting Lambda :" + e)
val new_bindings = scala.collection.mutable.ListBuffer[(Identifier, Identifier)]()
@@ -370,4 +370,4 @@ trait Z3StringConverters { self: Z3StringConversion =>
case ExprConverted(e) => e
}
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 78a483446624a28482772efe5752a4f6f44e1995..fef98f7d79920b9edcca0e0375a84f253b2f79c6 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -25,7 +25,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
private var keepAbstractExamples = false
/** If true, will not evaluate examples to check them. */
- def setKeepAbstractExamples(b: Boolean) = { this.keepAbstractExamples = b; this}
+ def setKeepAbstractExamples(b: Boolean) = { this.keepAbstractExamples = b; this }
/** Sets if evalution of the result of tests should stop on choose statements.
* Useful for programming by Example */
def setEvaluationFailOnChoose(b: Boolean) = { evaluator.setEvaluationFailOnChoose(b); this }