From 3e6458b5eac575e8f3faa5d06046d2de80bcdb95 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 24 Jun 2015 13:59:34 +0200
Subject: [PATCH] Prepatations for sets/arrays/maps
---
.../templates/QuantificationManager.scala | 23 +++++------
.../solvers/templates/TemplateGenerator.scala | 38 +++++++++++--------
2 files changed, 33 insertions(+), 28 deletions(-)
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 57dc368eb..3bb4374bd 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -16,6 +16,9 @@ case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[T]) {
override def toString = "M(" + caller + " : " + tpe + ", " + args.mkString("(",",",")") + ")"
}
+case class IllegalQuantificationException(expr: Expr, msg: String)
+ extends Exception(msg +" @ " + expr)
+
class QuantificationTemplate[T](
val quantificationManager: QuantificationManager[T],
val start: T,
@@ -147,9 +150,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
applications map { case (b, fas) =>
substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
},
- matchers map { case m @ Matcher(caller, _, args) =>
- m.copy(caller = substituter(caller), args = args.map(substituter))
- },
+ matchers map (m => m.copy(caller = substituter(m.caller), args = m.args.map(substituter))),
lambdas map { case (idT, template) => substituter(idT) -> template.substitute(subst) }
)
}
@@ -164,7 +165,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val matcherMappings: Set[Set[(T, Matcher[T], Matcher[T])]] = matchers
// 1. select an application in the quantified proposition for which the current app can
// be bound when generating the new constraints
- .filter(qm => qm.caller == caller || (qm.tpe == tpe && !known(qm.caller)))
+ .filter(_.tpe == tpe)
// 2. build the instantiation mapping associated to the chosen current application binding
.flatMap { bindingMatcher => matchers
// 2.1. select all potential matches for each quantified application
@@ -173,16 +174,12 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
bindingMatcher -> Set(blocker -> matcher)
} else {
val instances: Set[(T, Matcher[T])] = instantiated.filter {
- case (b, m @ Matcher(caller, tpe, _)) => tpe == qtpe && (qcaller == caller || !known(caller))
+ case (b, m @ Matcher(caller, tpe, _)) => tpe == qtpe
}
// concrete applications can appear multiple times in the constraint, and this is also the case
// for the current application for which we are generating the constraints
- val withCurrent = if (tpe == qtpe && (qcaller == caller || !known(caller))) {
- instances + (blocker -> matcher)
- } else instances
-
- println(qm -> withCurrent)
+ val withCurrent = if (tpe == qtpe) instances + (blocker -> matcher) else instances
qm -> withCurrent
}
@@ -234,8 +231,8 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
- val instantiationSubst: Map[T, T] = substMap +
- (template.guardVar -> encoder.encodeExpr(Map.empty)(BooleanLiteral(true)))
+ val trueT = encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
+ val instantiationSubst: Map[T, T] = substMap + (template.guardVar -> trueT)
val substituter = encoder.substitute(instantiationSubst)
val matchers = template.matchers.map { case (b, ms) =>
@@ -288,7 +285,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val eqClause = {
val qs = newQuantifications.map(_.qVar)
- val newQs = if (qs.size > 1) encoder.mkAnd(qs : _*) else qs.head
+ val newQs = if (qs.isEmpty) trueT else if (qs.size == 1) qs.head else encoder.mkAnd(qs : _*)
encoder.mkImplies(substMap(template.start), encoder.mkEquals(template.holdVar, newQs))
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 9b974a8de..9942cc3b7 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -281,26 +281,34 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
Variable(lid)
case f @ Forall(args, body) =>
- val idQuantifiers : Seq[Identifier] = args.map(_.id)
- val trQuantifiers : Seq[T] = idQuantifiers.map(encoder.encodeId)
+ val TopLevelAnds(conjuncts) = body
- val q: Identifier = FreshIdentifier("q", BooleanType)
- val ph: Identifier = FreshIdentifier("ph", BooleanType)
- val guard: Identifier = FreshIdentifier("guard", BooleanType)
+ val conjunctQs = conjuncts.map { conjunct =>
+ val vars = variablesOf(conjunct)
+ val quantifiers = args.map(_.id).filter(vars).toSet
- val clause = Equals(Variable(q), And(Variable(ph), Implies(Variable(guard), body)))
+ val idQuantifiers : Seq[Identifier] = quantifiers.toSeq
+ val trQuantifiers : Seq[T] = idQuantifiers.map(encoder.encodeId)
- val qs: (Identifier, T) = q -> encoder.encodeId(q)
- val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
- val clauseSubst: Map[Identifier, T] = localSubst ++ (idQuantifiers zip trQuantifiers)
- val (qConds, qExprs, qGuarded, qTemplates, qQuants) = mkClauses(pathVar, clause, clauseSubst)
- assert(qQuants.isEmpty, "Unhandled nested quantification in "+clause)
+ val q: Identifier = FreshIdentifier("q", BooleanType)
+ val ph: Identifier = FreshIdentifier("ph", BooleanType)
+ val guard: Identifier = FreshIdentifier("guard", BooleanType)
+
+ val clause = Equals(Variable(q), And(Variable(ph), Implies(Variable(guard), conjunct)))
- val template = QuantificationTemplate[T](encoder, manager, pathVar -> encodedCond(pathVar),
- qs, ph, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qGuarded, qTemplates, localSubst)
- registerQuantification(template)
+ val qs: (Identifier, T) = q -> encoder.encodeId(q)
+ val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
+ val clauseSubst: Map[Identifier, T] = localSubst ++ (idQuantifiers zip trQuantifiers)
+ val (qConds, qExprs, qGuarded, qTemplates, qQuants) = mkClauses(pathVar, clause, clauseSubst)
+ assert(qQuants.isEmpty, "Unhandled nested quantification in "+clause)
+
+ val template = QuantificationTemplate[T](encoder, manager, pathVar -> encodedCond(pathVar),
+ qs, ph, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qGuarded, qTemplates, localSubst)
+ registerQuantification(template)
+ Variable(q)
+ }
- Variable(q)
+ andJoin(conjunctQs)
case Operator(as, r) => r(as.map(a => rec(pathVar, a)))
}
--
GitLab