diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index b7fefa6b243c653341976633b13779636ea81186..95a8cdd67722660f666a9256a0020fab9d93b5d2 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -9,6 +9,7 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Quantification._
import purescala.Constructors._
+import purescala.Extractors._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Types._
@@ -268,8 +269,67 @@ trait AbstractUnrollingSolver[T]
private def getTotalModel: Model = {
val wrapped = solverGetModel
- templateGenerator.manager.quantifications.map { q =>
- q.holds
+ def checkForalls(quantified: Set[Identifier], body: Expr): Option[String] = {
+ val matchers = collect[(Expr, Seq[Expr])] {
+ case QuantificationMatcher(e, args) => Set(e -> args)
+ case _ => Set.empty
+ } (body)
+
+ if (matchers.isEmpty)
+ return Some("No matchers found.")
+
+ val matcherToQuants = matchers.foldLeft(Map.empty[Expr, Set[Identifier]]) {
+ case (acc, (m, args)) => acc + (m -> (acc.getOrElse(m, Set.empty) ++ args.flatMap {
+ case Variable(id) if quantified(id) => Set(id)
+ case _ => Set.empty[Identifier]
+ }))
+ }
+
+ val bijectiveMappings = matcherToQuants.filter(_._2.nonEmpty).groupBy(_._2)
+ if (bijectiveMappings.size > 1)
+ return Some("Non-bijective mapping for symbol " + bijectiveMappings.head._2.head._1.asString)
+
+ def quantifiedArg(e: Expr): Boolean = e match {
+ case Variable(id) => quantified(id)
+ case QuantificationMatcher(_, args) => args.forall(quantifiedArg)
+ case _ => false
+ }
+
+ postTraversal(m => m match {
+ case QuantificationMatcher(_, args) =>
+ val qArgs = args.filter(quantifiedArg)
+
+ if (qArgs.nonEmpty && qArgs.size < args.size)
+ return Some("Mixed ground and quantified arguments in " + m.asString)
+
+ case Operator(es, _) if es.collect { case Variable(id) if quantified(id) => id }.nonEmpty =>
+ return Some("Invalid operation on quantifiers " + m.asString)
+
+ case (_: Equals) | (_: And) | (_: Or) | (_: Implies) => // OK
+
+ case Operator(es, _) if (es.flatMap(variablesOf).toSet & quantified).nonEmpty =>
+ return Some("Unandled implications from operation " + m.asString)
+
+ case _ =>
+ }) (body)
+
+ body match {
+ case Variable(id) if quantified(id) =>
+ Some("Unexpected free quantifier " + id.asString)
+ case _ => None
+ }
+ }
+
+ val issues: Iterable[(Seq[Identifier], Expr, String)] = for {
+ q <- templateGenerator.manager.quantifications.view
+ if wrapped.eval(q.holds, BooleanType) == Some(BooleanLiteral(true))
+ msg <- checkForalls(q.quantifiers.map(_._1).toSet, q.body)
+ } yield (q.quantifiers.map(_._1), q.body, msg)
+
+ if (issues.nonEmpty) {
+ val (quantifiers, body, msg) = issues.head
+ reporter.warning("Model soundness not guaranteed for \u2200" +
+ quantifiers.map(_.asString).mkString(",") + ". " + body.asString+" :\n => " + msg)
}
val typeInsts = templateGenerator.manager.typeInstantiations
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 541888c8349214ef5190b3c4610ee278bcc73d01..362629388e533bcca567cd826fea9ea84e007b7c 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -75,7 +75,7 @@ object LambdaTemplate {
matchers,
quantifications,
keyDeps,
- key,
+ key -> structSubst,
lambdaString
)
}
@@ -83,7 +83,7 @@ object LambdaTemplate {
trait KeyedTemplate[T, E <: Expr] {
val dependencies: Map[Identifier, T]
- val structuralKey: E
+ val structure: E
lazy val key: (E, Seq[T]) = {
def rec(e: Expr): Seq[Identifier] = e match {
@@ -99,7 +99,7 @@ trait KeyedTemplate[T, E <: Expr] {
case _ => Seq.empty
}
- structuralKey -> rec(structuralKey).distinct.map(dependencies)
+ structure -> rec(structure).distinct.map(dependencies)
}
}
@@ -119,12 +119,13 @@ class LambdaTemplate[T] private (
val matchers: Map[T, Set[Matcher[T]]],
val quantifications: Seq[QuantificationTemplate[T]],
val dependencies: Map[Identifier, T],
- val structuralKey: Lambda,
+ val struct: (Lambda, Map[Identifier, Identifier]),
stringRepr: () => String) extends Template[T] with KeyedTemplate[T, Lambda] {
val args = arguments.map(_._2)
val tpe = bestRealType(ids._1.getType).asInstanceOf[FunctionType]
val functions: Set[(T, FunctionType, T)] = Set.empty
+ val (structure, structSubst) = struct
def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): LambdaTemplate[T] = {
val newStart = substituter(start)
@@ -171,7 +172,7 @@ class LambdaTemplate[T] private (
newMatchers,
newQuantifications,
newDependencies,
- structuralKey,
+ struct,
stringRepr
)
}
@@ -182,7 +183,7 @@ class LambdaTemplate[T] private (
ids._1 -> idT, encoder, manager, pathVar, arguments, condVars, exprVars, condTree,
clauses map substituter, // make sure the body-defining clause is inlined!
blockers, applications, lambdas, matchers, quantifications,
- dependencies, structuralKey, stringRepr
+ dependencies, struct, stringRepr
)
}
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index cd894b5f2953edf168b8fa936770b321f6d4193e..3b7d97a4ff28f5468a02566cbc196cfea54b7404 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -55,8 +55,9 @@ class QuantificationTemplate[T](
val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Seq[LambdaTemplate[T]],
val dependencies: Map[Identifier, T],
- val structuralKey: Forall) extends KeyedTemplate[T, Forall] {
+ val struct: (Forall, Map[Identifier, Identifier])) extends KeyedTemplate[T, Forall] {
+ val structure = struct._1
lazy val start = pathVar._2
def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): QuantificationTemplate[T] = {
@@ -88,7 +89,7 @@ class QuantificationTemplate[T](
},
lambdas.map(_.substitute(substituter, matcherSubst)),
dependencies.map { case (id, value) => id -> substituter(value) },
- structuralKey
+ struct
)
}
}
@@ -127,7 +128,7 @@ object QuantificationTemplate {
new QuantificationTemplate[T](quantificationManager,
pathVar, qs, q2s, insts, guards._2, quantifiers, condVars, exprVars, condTree,
- clauses, blockers, applications, matchers, lambdas, keyDeps, key)
+ clauses, blockers, applications, matchers, lambdas, keyDeps, key -> structSubst)
}
}
@@ -156,7 +157,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private def matcherKey(caller: T, tpe: TypeTree): MatcherKey = tpe match {
case ft: FunctionType if knownFree(ft)(caller) => CallerKey(caller, tpe)
- case _: FunctionType if byID.isDefinedAt(caller) => LambdaKey(byID(caller).structuralKey, tpe)
+ case _: FunctionType if byID.isDefinedAt(caller) => LambdaKey(byID(caller).structure, tpe)
case _ => TypeKey(tpe)
}
@@ -346,7 +347,6 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private[solvers] trait MatcherQuantification {
- val holds: T
val pathVar: (Identifier, T)
val quantifiers: Seq[(Identifier, T)]
val matchers: Set[Matcher[T]]
@@ -359,6 +359,9 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val applications: Map[T, Set[App[T]]]
val lambdas: Seq[LambdaTemplate[T]]
+ val holds: T
+ val body: Expr
+
lazy val quantified: Set[T] = quantifiers.map(_._2).toSet
lazy val start = pathVar._2
@@ -537,10 +540,16 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
- val lambdas: Seq[LambdaTemplate[T]]) extends MatcherQuantification {
+ val lambdas: Seq[LambdaTemplate[T]],
+ val template: QuantificationTemplate[T]) extends MatcherQuantification {
var currentQ2Var: T = qs._2
val holds = qs._2
+ val body = {
+ val quantified = quantifiers.map(_._1).toSet
+ val mapping = template.struct._2.map(p => p._2 -> p._1.toVariable)
+ replaceFromIDs(mapping, template.structure.body)
+ }
protected def instanceSubst(enabler: T): Map[T, T] = {
val nextQ2Var = encoder.encodeId(q2s._1)
@@ -590,10 +599,17 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
- val lambdas: Seq[LambdaTemplate[T]]) extends MatcherQuantification {
+ val lambdas: Seq[LambdaTemplate[T]],
+ val template: LambdaTemplate[T]) extends MatcherQuantification {
val holds = start
+ val body = {
+ val quantified = quantifiers.map(_._1).toSet
+ val mapping = template.structSubst.map(p => p._2 -> p._1.toVariable)
+ replaceFromIDs(mapping, template.structure)
+ }
+
protected def instanceSubst(enabler: T): Map[T, T] = {
Map(guardVar -> start, blocker -> enabler)
}
@@ -734,75 +750,51 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val appT = encoder.encodeExpr((template.arguments.map(_._1) zip encArgs.map(_.encoded)).toMap + template.ids)(app)
val selfMatcher = Matcher(template.ids._2, template.tpe, encArgs, appT)
+ val instMatchers = allMatchers + (template.start -> (allMatchers.getOrElse(template.start, Set.empty) + selfMatcher))
+
val enablingClause = encoder.mkImplies(guardT, blockerT)
- instantiateAxiom(
- template.pathVar._1 -> substituter(template.start),
- blockerT,
- guardT,
- quantifiers,
- qMatchers,
- allMatchers + (template.start -> (allMatchers.getOrElse(template.start, Set.empty) + selfMatcher)),
- template.condVars map { case (id, idT) => id -> substituter(idT) },
- template.exprVars map { case (id, idT) => id -> substituter(idT) },
- template.condTree,
- (template.clauses map substituter) :+ enablingClause,
- template.blockers map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(
- args = fi.args.map(_.substitute(substituter, msubst))
- ))
- },
- template.applications map { case (b, apps) =>
- substituter(b) -> apps.map(app => app.copy(
- caller = substituter(app.caller),
- args = app.args.map(_.substitute(substituter, msubst))
- ))
- },
- template.lambdas map (_.substitute(substituter, msubst))
- )
- }
- }
+ val condVars = template.condVars map { case (id, idT) => id -> substituter(idT) }
+ val exprVars = template.exprVars map { case (id, idT) => id -> substituter(idT) }
+ val clauses = (template.clauses map substituter) :+ enablingClause
+ val blockers = template.blockers map { case (b, fis) =>
+ substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(_.substitute(substituter, msubst))))
+ }
- def instantiateAxiom(
- pathVar: (Identifier, T),
- blocker: T,
- guardVar: T,
- quantifiers: Seq[(Identifier, T)],
- matchers: Set[Matcher[T]],
- allMatchers: Map[T, Set[Matcher[T]]],
- condVars: Map[Identifier, T],
- exprVars: Map[Identifier, T],
- condTree: Map[Identifier, Set[Identifier]],
- clauses: Seq[T],
- blockers: Map[T, Set[TemplateCallInfo[T]]],
- applications: Map[T, Set[App[T]]],
- lambdas: Seq[LambdaTemplate[T]]
- ): Instantiation[T] = {
- val quantified = quantifiers.map(_._2).toSet
- val matchQuorums = extractQuorums(quantified, matchers, lambdas)
+ val applications = template.applications map { case (b, apps) =>
+ substituter(b) -> apps.map(app => app.copy(
+ caller = substituter(app.caller),
+ args = app.args.map(_.substitute(substituter, msubst))
+ ))
+ }
- var instantiation = Instantiation.empty[T]
+ val lambdas = template.lambdas map (_.substitute(substituter, msubst))
- for (matchers <- matchQuorums) {
- val axiom = new LambdaAxiom(pathVar, blocker, guardVar, quantifiers,
- matchers, allMatchers, condVars, exprVars, condTree,
- clauses, blockers, applications, lambdas
- )
+ val quantified = quantifiers.map(_._2).toSet
+ val matchQuorums = extractQuorums(quantified, qMatchers, lambdas)
- quantifications += axiom
- handledSubsts += axiom -> MutableSet.empty
- ignoredSubsts += axiom -> MutableSet.empty
+ var instantiation = Instantiation.empty[T]
- val newCtx = new InstantiationContext()
- for ((b,m) <- instCtx.instantiated) {
- instantiation ++= newCtx.instantiate(b, m)(axiom)
+ for (matchers <- matchQuorums) {
+ val axiom = new LambdaAxiom(template.pathVar._1 -> substituter(template.start),
+ blockerT, guardT, quantifiers, matchers, instMatchers, condVars, exprVars, template.condTree,
+ clauses, blockers, applications, lambdas, template)
+
+ quantifications += axiom
+ handledSubsts += axiom -> MutableSet.empty
+ ignoredSubsts += axiom -> MutableSet.empty
+
+ val newCtx = new InstantiationContext()
+ for ((b,m) <- instCtx.instantiated) {
+ instantiation ++= newCtx.instantiate(b, m)(axiom)
+ }
+ instCtx.merge(newCtx)
}
- instCtx.merge(newCtx)
- }
- instantiation ++= instantiateConstants(quantifiers, matchers)
+ instantiation ++= instantiateConstants(quantifiers, qMatchers)
- instantiation
+ instantiation
+ }
}
def instantiateQuantification(template: QuantificationTemplate[T]): (T, Instantiation[T]) = {
@@ -828,8 +820,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
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
- )
+ template.blockers, template.applications, template.lambdas, template)
quantifications += quantification
handledSubsts += quantification -> MutableSet.empty
diff --git a/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala b/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
index 0e85b119bff11f1925d3a0177826701e0dd700d4..4ff5ccc71d159fd76ec1e48d99bce4be4dbfb125 100644
--- a/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
@@ -108,6 +108,8 @@ class QuantifierSolverSuite extends LeonTestSuiteWithProgram {
try {
solver.assertCnstr(expr)
solver.check match {
+ case Some(true) if sat && fix._1.reporter.warningCount > 0 =>
+ fail(s"Solver $solver - Constraint ${expr.asString} doesn't guarantee model validity!?")
case Some(true) if sat => // checkmodels ensures validity
case Some(false) if !sat => // we were looking for unsat
case res => fail(s"Solver $solver - Constraint ${expr.asString} has result $res!?")