diff --git a/src/main/scala/leon/purescala/CheckForalls.scala b/src/main/scala/leon/purescala/CheckForalls.scala
new file mode 100644
index 0000000000000000000000000000000000000000..600b0ea26e8831779af4418a9c325692870e5fde
--- /dev/null
+++ b/src/main/scala/leon/purescala/CheckForalls.scala
@@ -0,0 +1,93 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package purescala
+
+import Common._
+import Definitions._
+import Expressions._
+import Extractors._
+import ExprOps._
+
+object CheckForalls extends UnitPhase[Program] {
+
+ val name = "Foralls"
+ val description = "Check syntax of foralls to guarantee sound instantiations"
+
+ def apply(ctx: LeonContext, program: Program) = {
+ program.definedFunctions.foreach { fd =>
+ if (fd.body.exists(b => exists {
+ case f: Forall => true
+ case _ => false
+ } (b))) ctx.reporter.warning("Universal quantification in function bodies is not supported in " + fd)
+
+ val foralls = (fd.precondition.toSeq ++ fd.postcondition.toSeq).flatMap { prec =>
+ collect[Forall] {
+ case f: Forall => Set(f)
+ case _ => Set.empty
+ } (prec)
+ }
+
+ val free = fd.params.map(_.id).toSet ++ (fd.postcondition match {
+ case Some(Lambda(args, _)) => args.map(_.id)
+ case _ => Seq.empty
+ })
+
+ object Matcher {
+ def unapply(e: Expr): Option[(Identifier, Seq[Expr])] = e match {
+ case Application(Variable(id), args) if free(id) => Some(id -> args)
+ case ArraySelect(Variable(id), index) if free(id) => Some(id -> Seq(index))
+ case MapGet(Variable(id), key) if free(id) => Some(id -> Seq(key))
+ case _ => None
+ }
+ }
+
+ for (Forall(args, TopLevelAnds(conjuncts)) <- foralls) {
+ val quantified = args.map(_.id).toSet
+
+ for (conjunct <- conjuncts) {
+ val matchers = collect[(Identifier, Seq[Expr])] {
+ case Matcher(id, args) => Set(id -> args)
+ case _ => Set.empty
+ } (conjunct)
+
+ if (matchers.exists { case (id, args) =>
+ args.exists(arg => arg match {
+ case Matcher(_, _) => false
+ case Variable(id) => false
+ case _ if (variablesOf(arg) & quantified).nonEmpty => true
+ case _ => false
+ })
+ }) ctx.reporter.warning("Matcher arguments must have simple form in " + conjunct)
+
+ if (matchers.map(_._1).toSet.size != 1)
+ ctx.reporter.warning("Quantification conjuncts must contain exactly one matcher in " + conjunct)
+
+ preTraversal {
+ case Matcher(_, _) => // OK
+ case LessThan(_: Variable, _: Variable) => // OK
+ case LessEquals(_: Variable, _: Variable) => // OK
+ case GreaterThan(_: Variable, _: Variable) => // OK
+ case GreaterEquals(_: Variable, _: Variable) => // OK
+ case And(_) => // OK
+ case Or(_) => // OK
+ case Implies(_, _) => // OK
+ case BinaryOperator(Matcher(_, _), _, _) => // OK
+ case BinaryOperator(_, Matcher(_, _), _) => // OK
+ case BinaryOperator(e1, _, _) if (variablesOf(e1) & quantified).isEmpty => // OK
+ case BinaryOperator(_, e2, _) if (variablesOf(e2) & quantified).isEmpty => // OK
+ case FunctionInvocation(_, args) if {
+ val argVars = args.flatMap(variablesOf).toSet
+ (argVars & quantified).size <= 1 && (argVars & free).isEmpty
+ } => // OK
+ case UnaryOperator(_, _) => // OK
+ case BinaryOperator(e1, e2, _) if ((variablesOf(e1) ++ variablesOf(e2)) & quantified).isEmpty => // OK
+ case NAryOperator(es, _) if (es.flatMap(variablesOf).toSet & quantified).isEmpty => // OK
+ case _: Terminal => // OK
+ case e => ctx.reporter.warning("Invalid operation " + e + " on quantified variables")
+ } (conjunct)
+ }
+ }
+ }
+ }
+}
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 3bb4374bdb3ca46e49f2b5742a080b7b783b52da..9d19ea839601d631fe7210786c1c9d49894503af 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -94,6 +94,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private var knownStack: List[Set[T]] = List(Set.empty)
private def known(idT: T): Boolean = knownStack.head(idT) || byID.isDefinedAt(idT)
+ private def correspond(qm: Matcher[T], m: Matcher[T]): Boolean = qm.tpe match {
+ case _: FunctionType => qm.tpe == m.tpe && (qm.caller == m.caller || !known(m.caller))
+ case _ => qm.tpe == m.tpe
+ }
override def push(): Unit = {
quantificationsStack = quantifications :: quantificationsStack
@@ -156,7 +160,6 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
def instantiate(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
- val Matcher(caller, tpe, args) = matcher
// Build a mapping from applications in the quantified statement to all potential concrete
// applications previously encountered. Also make sure the current `app` is in the mapping
@@ -165,25 +168,21 @@ 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(_.tpe == tpe)
+ .filter(qm => correspond(qm, matcher))
// 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
- .map { case qm @ Matcher(qcaller, qtpe, qargs) =>
- if (qm == bindingMatcher) {
- bindingMatcher -> Set(blocker -> matcher)
- } else {
- val instances: Set[(T, Matcher[T])] = instantiated.filter {
- 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) instances + (blocker -> matcher) else instances
-
- qm -> withCurrent
- }
- }
+ .map(qm => if (qm == bindingMatcher) {
+ bindingMatcher -> Set(blocker -> matcher)
+ } else {
+ val instances: Set[(T, Matcher[T])] = instantiated.filter { case (b, m) => correspond(qm, m) }
+
+ // 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 (correspond(qm, matcher)) instances + (blocker -> matcher) else instances
+
+ qm -> withCurrent
+ })
// 2.2. based on the possible bindings for each quantified application, build a set of
// instantiation mappings that can be used to instantiate all necessary constraints
.foldLeft[Set[Set[(T, Matcher[T], Matcher[T])]]] (Set(Set.empty)) {
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index 376c411c2fcbb9fbfc53be6549ae60f624c34cc0..d727a2b9f0000eb17fe6b1173e7cdab07dc225ef 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -126,6 +126,8 @@ object Template {
private def matchersOf[T](encodeExpr: Expr => T)(expr: Expr): Set[Matcher[T]] = collect[Matcher[T]] {
case Application(caller, args) => Set(Matcher(encodeExpr(caller), caller.getType, args.map(encodeExpr)))
+ case ArraySelect(arr, index) => Set(Matcher(encodeExpr(arr), arr.getType, Seq(encodeExpr(index))))
+ case MapGet(map, key) => Set(Matcher(encodeExpr(map), map.getType, Seq(encodeExpr(key))))
case _ => Set.empty
}(expr)
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index fb08be9ce3bc4426997c64ae00f2a1b77fcb727a..7c91fa436fd5e804fb35830e113913264e27d235 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -34,7 +34,8 @@ class PreprocessingPhase(private val desugarXLang: Boolean = false) extends Tran
CompleteAbstractDefinitions andThen
CheckADTFieldsTypes andThen
InjectAsserts andThen
- InliningPhase
+ InliningPhase andThen
+ CheckForalls
val pipeX = if(desugarXLang) {
XLangDesugaringPhase andThen