From d359ba78b36ca5657fcbb812ce628b4aa2209783 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 15 Feb 2016 09:42:23 +0100
Subject: [PATCH] Finished up satisfiability with quantifiers
---
.../scala/leon/codegen/CompilationUnit.scala | 2 +-
.../leon/evaluators/StreamEvaluator.scala | 129 +++++++++++-----
.../solvers/combinators/UnrollingSolver.scala | 34 +++--
.../combinators/Z3StringCapableSolver.scala | 1 -
.../templates/QuantificationManager.scala | 85 +++++++++--
.../leon/solvers/z3/FairZ3Component.scala | 23 ---
.../scala/leon/solvers/z3/FairZ3Solver.scala | 3 +-
.../solvers/QuantifierSolverSuite.scala | 143 ++++++++++++++++++
.../integration/solvers/SolversSuite.scala | 76 +++++-----
9 files changed, 365 insertions(+), 131 deletions(-)
delete mode 100644 src/main/scala/leon/solvers/z3/FairZ3Component.scala
create mode 100644 src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 707eae8fa..ca2510451 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -8,7 +8,7 @@ import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Types._
-import purescala.TypeOps._
+import purescala.TypeOps.typeParamsOf
import purescala.Extractors._
import purescala.Constructors._
import utils.UniqueCounter
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index feb0dd7f2..36509832d 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -11,10 +11,14 @@ import purescala.Types._
import purescala.Common.Identifier
import purescala.Definitions.{TypedFunDef, Program}
import purescala.Expressions._
+import purescala.Quantification._
-import leon.solvers.SolverFactory
+import leon.solvers.{SolverFactory, HenkinModel}
+import leon.solvers.combinators.UnrollingProcedure
import leon.utils.StreamUtils._
+import scala.concurrent.duration._
+
class StreamEvaluator(ctx: LeonContext, prog: Program)
extends ContextualEvaluator(ctx, prog, 50000)
with NDEvaluator
@@ -106,6 +110,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
case Or(args) if args.isEmpty =>
Stream(BooleanLiteral(false))
+
case Or(args) =>
e(args.head).distinct.flatMap {
case BooleanLiteral(true) => Stream(BooleanLiteral(true))
@@ -117,42 +122,93 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
e(Or(Not(lhs), rhs))
case l @ Lambda(_, _) =>
- val (nl, structSubst) = normalizeStructure(l)
val mapping = variablesOf(l).map(id =>
- structSubst(id) -> (e(Variable(id)) match {
+ id -> (e(Variable(id)) match {
case Stream(v) => v
case _ => return Stream()
})
).toMap
- Stream(replaceFromIDs(mapping, nl))
-
- // FIXME
- case FiniteLambda(mapping, dflt, tpe) =>
- def solveOne(pair: (Seq[Expr], Expr)) = {
- val (args, res) = pair
- for {
- as <- cartesianProduct(args map e)
- r <- e(res)
- } yield as -> r
- }
- cartesianProduct(mapping map solveOne) map (FiniteLambda(_, dflt, tpe)) // FIXME!!!
-
- case f @ Forall(fargs, TopLevelAnds(conjuncts)) =>
- Stream() // FIXME
- /*def solveOne(conj: Expr) = {
- val instantiations = forallInstantiations(gctx, fargs, conj)
- for {
- es <- cartesianProduct(instantiations.map { case (enabler, mapping) =>
- e(Implies(enabler, conj))(rctx.withNewVars(mapping), gctx)
- })
- res <- e(andJoin(es))
- } yield res
- }
+ Stream(replaceFromIDs(mapping, l))
- for {
- conj <- cartesianProduct(conjuncts map solveOne)
- res <- e(andJoin(conj))
- } yield res*/
+ case fl @ FiniteLambda(mapping, dflt, tpe) =>
+ // finite lambda should always be ground!
+ Stream(fl)
+
+ case f @ Forall(fargs, body) =>
+
+ // TODO add memoization
+ 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)
+
+ val tStart = System.currentTimeMillis
+
+ val newCtx = ctx.copy(options = ctx.options.map {
+ case LeonOption(optDef, value) if optDef == UnrollingProcedure.optFeelingLucky =>
+ LeonOption(optDef)(false)
+ case opt => opt
+ })
+
+ val solverf = SolverFactory.getFromSettings(newCtx, program).withTimeout(1.second)
+ 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 optMatcher = e(expr) match {
+ case Stream(l: Lambda) => Some(gctx.lambdas.getOrElse(l, l))
+ case Stream(ev) => Some(ev)
+ case _ => None
+ }
+
+ optMatcher.toSeq.flatMap { matcher =>
+ 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)
+ Stream(res)
+ case _ =>
+ Stream()
+ }
+ } catch {
+ case e: Throwable => Stream()
+ } finally {
+ solverf.reclaim(solver)
+ solverf.shutdown()
+ }
case p : Passes =>
e(p.asConstraint)
@@ -168,13 +224,18 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.getFromSettings(ctx, program)
+ val newCtx = ctx.copy(options = ctx.options.map {
+ case LeonOption(optDef, value) if optDef == UnrollingProcedure.optFeelingLucky =>
+ LeonOption(optDef)(false)
+ case opt => opt
+ })
+
+ val solverf = SolverFactory.getFromSettings(newCtx, program)
val solver = solverf.getNewSolver()
try {
val eqs = p.as.map {
- case id =>
- Equals(Variable(id), rctx.mappings(id))
+ case id => Equals(Variable(id), rctx.mappings(id))
}
val cnstr = andJoin(eqs ::: p.pc :: p.phi :: Nil)
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index f97085857..c76eb400b 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -225,7 +225,7 @@ trait AbstractUnrollingSolver[T]
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) =>
+ val funDomains: Map[Identifier, Set[Seq[Expr]]] = freeVars.toMap.map { case (id, idT) =>
id -> partialInsts.get(idT).toSeq.flatten.flatMap { case (b, m) => wrapped.extract(b, m) }.toSet
}
@@ -237,11 +237,16 @@ trait AbstractUnrollingSolver[T]
val value = wrapped.get(id).getOrElse(simplestValue(id.getType))
id -> (funDomains.get(id) match {
case Some(domain) =>
- val FiniteLambda(_, dflt, tpe) = value
+ val dflt = value match {
+ case FiniteLambda(_, dflt, _) => dflt
+ case Lambda(_, IfExpr(_, _, dflt)) => dflt
+ case _ => scala.sys.error("Can't extract default from " + 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)
+ }, dflt, id.getType.asInstanceOf[FunctionType])
case None => postMap {
case p @ FiniteLambda(mapping, dflt, tpe) =>
@@ -287,21 +292,18 @@ trait AbstractUnrollingSolver[T]
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))
- }
+ wrapped.extract(b, m).map { args =>
+ val result = evaluator.eval(application(value, args)).result.getOrElse {
+ scala.sys.error("Unexpectedly failed to evaluate " + application(value, args))
+ }
- 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)
- }
+ val cond = if (m.args.exists(arg => templateGenerator.manager.isQuantifier(arg.encoded))) {
+ extractCond(params, m.args.map(_.encoded) zip args, Map.empty)
+ } else {
+ (params zip args).map(p => Equals(Variable(p._1), p._2))
+ }
- case None => Seq.empty
+ cond -> result
}
}
diff --git a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
index eea7c80a0..e636ff6a7 100644
--- a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala
@@ -15,7 +15,6 @@ import purescala.DefOps
import purescala.TypeOps
import purescala.Extractors._
import utils._
-import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks, optUnfoldFactor}
import templates._
import evaluators._
import Template._
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 84f8b707f..84a3017b8 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -632,6 +632,69 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(m: Matcher[T]) => m.args.collect { case Left(a) if quantified(a) => a }.toSet)
}
+ private def instantiateConstants(quantifiers: Seq[(Identifier, T)], matchers: Set[Matcher[T]]): Instantiation[T] = {
+ val quantifierSubst = uniformSubst(quantifiers)
+ val substituter = encoder.substitute(quantifierSubst)
+ var instantiation: Instantiation[T] = Instantiation.empty
+
+ for {
+ m <- matchers
+ sm = m.substitute(substituter, Map.empty)
+ if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
+ } {
+ instantiation ++= instCtx.instantiate(Set.empty, m)(quantifications.toSeq : _*)
+ instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
+ }
+
+ def unifyMatchers(matchers: Seq[Matcher[T]]): Unit = matchers match {
+ case sm +: others =>
+ for (pm <- others if correspond(pm, sm)) {
+ val encodedArgs = (sm.args zip pm.args).map(p => p._1.encoded -> p._2.encoded)
+ val mismatches = encodedArgs.zipWithIndex.collect {
+ case ((sa, pa), idx) if isQuantifier(sa) && isQuantifier(pa) && sa != pa => (idx, (pa, sa))
+ }.toMap
+
+ def extractChains(indexes: Seq[Int], partials: Seq[Seq[Int]]): Seq[Seq[Int]] = indexes match {
+ case idx +: xs =>
+ val (p1, p2) = mismatches(idx)
+ val newPartials = Seq(idx) +: partials.map { seq =>
+ if (mismatches(seq.head)._1 == p2) idx +: seq
+ else if (mismatches(seq.last)._2 == p1) seq :+ idx
+ else seq
+ }
+
+ val (closed, remaining) = newPartials.partition { seq =>
+ mismatches(seq.head)._1 == mismatches(seq.last)._2
+ }
+ closed ++ extractChains(xs, partials ++ remaining)
+
+ case _ => Seq.empty
+ }
+
+ val chains = extractChains(mismatches.keys.toSeq, Seq.empty)
+ val positions = chains.foldLeft(Map.empty[Int, Int]) { (mapping, seq) =>
+ val res = seq.min
+ mapping ++ seq.map(i => i -> res)
+ }
+
+ def extractArgs(args: Seq[Arg[T]]): Seq[Arg[T]] =
+ (0 until args.size).map(i => args(positions.getOrElse(i, i)))
+
+ instantiation ++= instCtx.instantiate(Set.empty, sm.copy(args = extractArgs(sm.args)))(quantifications.toSeq : _*)
+ instantiation ++= instCtx.instantiate(Set.empty, pm.copy(args = extractArgs(pm.args)))(quantifications.toSeq : _*)
+ }
+
+ unifyMatchers(others)
+
+ case _ =>
+ }
+
+ val substMatchers = matchers.map(_.substitute(substituter, Map.empty))
+ unifyMatchers(substMatchers.toSeq)
+
+ instantiation
+ }
+
def instantiateAxiom(template: LambdaTemplate[T], substMap: Map[T, Arg[T]]): Instantiation[T] = {
def quantifiedMatcher(m: Matcher[T]): Boolean = m.args.exists(a => a match {
case Left(v) => isQuantifier(v)
@@ -738,14 +801,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
instCtx.merge(newCtx)
}
- val quantifierSubst = uniformSubst(quantifiers)
- val substituter = encoder.substitute(quantifierSubst)
-
- for {
- m <- matchers
- sm = m.substitute(substituter, Map.empty)
- if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
- } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
+ instantiation ++= instantiateConstants(quantifiers, matchers)
instantiation
}
@@ -797,14 +853,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
encoder.mkImplies(template.start, encoder.mkEquals(qT, newQs))
}
- val quantifierSubst = uniformSubst(template.quantifiers)
- val substituter = encoder.substitute(quantifierSubst)
-
- for {
- (_, ms) <- template.matchers; m <- ms
- sm = m.substitute(substituter, Map.empty)
- if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
- } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
+ instantiation ++= instantiateConstants(template.quantifiers, template.matchers.flatMap(_._2).toSet)
templates += template.key -> qT
(qT, instantiation)
@@ -932,6 +981,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
} clauses += encoder.mkAnd(quants.map(q => encoder.mkNot(encoder.mkEquals(q, arg))) : _*)
}
+ for ((tpe, base +: rest) <- uniformQuantMap; q <- rest) {
+ clauses += encoder.mkEquals(base, q)
+ }
+
clauses.toSeq
}
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
deleted file mode 100644
index 70ebd260f..000000000
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package solvers.z3
-
-trait FairZ3Component extends LeonComponent {
- val name = "Z3-f"
- val description = "Fair Z3 Solver"
-
- val optEvalGround = LeonFlagOptionDef("evalground", "Use evaluator on functions applied to ground arguments", false)
- val optCheckModels = LeonFlagOptionDef("checkmodels", "Double-check counter-examples with evaluator", false)
- val optFeelingLucky = LeonFlagOptionDef("feelinglucky","Use evaluator to find counter-examples early", false)
- val optUseCodeGen = LeonFlagOptionDef("codegen", "Use compiled evaluator instead of interpreter", false)
- val optUnrollCores = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unrolling while remaining fair", false)
- val optAssumePre = LeonFlagOptionDef("assumepre", "Assume precondition holds (pre && f(x) = body) when unfolding", false)
- val optNoChecks = LeonFlagOptionDef("nochecks", "Disable counter-example check in presence of foralls" , false)
- val optUnfoldFactor = LeonLongOptionDef("unfoldFactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
-
- override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre, optUnfoldFactor)
-}
-
-object FairZ3Component extends FairZ3Component
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index ca1b929e1..5c12fd386 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -26,8 +26,7 @@ import termination._
class FairZ3Solver(val context: LeonContext, val program: Program)
extends AbstractZ3Solver
- with AbstractUnrollingSolver[Z3AST]
- with Z3ModelReconstruction {
+ with AbstractUnrollingSolver[Z3AST] {
enclosing =>
diff --git a/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala b/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
new file mode 100644
index 000000000..0e85b119b
--- /dev/null
+++ b/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
@@ -0,0 +1,143 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.integration.solvers
+
+import leon.test._
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Expressions._
+import leon.purescala.Constructors._
+import leon.purescala.Types._
+import leon.LeonContext
+import leon.LeonOption
+
+import leon.solvers._
+import leon.solvers.smtlib._
+import leon.solvers.combinators._
+import leon.solvers.z3._
+
+class QuantifierSolverSuite extends LeonTestSuiteWithProgram {
+
+ val sources = List()
+
+ override val leonOpts = List("checkmodels")
+
+ val getFactories: Seq[(String, (LeonContext, Program) => Solver)] = {
+ (if (SolverFactory.hasNativeZ3) Seq(
+ ("fairz3", (ctx: LeonContext, pgm: Program) => new FairZ3Solver(ctx, pgm))
+ ) else Nil) ++
+ (if (SolverFactory.hasZ3) Seq(
+ ("smt-z3", (ctx: LeonContext, pgm: Program) => new UnrollingSolver(ctx, pgm, new SMTLIBZ3Solver(ctx, pgm)))
+ ) else Nil) ++
+ (if (SolverFactory.hasCVC4) Seq(
+ ("smt-cvc4", (ctx: LeonContext, pgm: Program) => new UnrollingSolver(ctx, pgm, new SMTLIBCVC4Solver(ctx, pgm)))
+ ) else Nil)
+ }
+
+ val f1: Identifier = FreshIdentifier("f1", FunctionType(Seq(IntegerType, IntegerType), IntegerType))
+ val A = TypeParameter.fresh("A")
+ val f2: Identifier = FreshIdentifier("f2", FunctionType(Seq(A, A), A))
+
+ def app(f: Expr, args: Expr*): Expr = Application(f, args)
+ def bi(i: Int): Expr = InfiniteIntegerLiteral(i)
+
+ def associative(f: Expr): Expr = {
+ val FunctionType(Seq(t1, t2), _) = f.getType
+ assert(t1 == t2, "Can't specify associativity for type " + f.getType)
+
+ val ids @ Seq(x, y, z) = Seq("x", "y", "z").map(name => FreshIdentifier(name, t1, true))
+ Forall(ids.map(ValDef(_)), Equals(
+ app(f, app(f, Variable(x), Variable(y)), Variable(z)),
+ app(f, Variable(x), app(f, Variable(y), Variable(z)))))
+ }
+
+ def commutative(f: Expr): Expr = {
+ val FunctionType(Seq(t1, t2), _) = f.getType
+ assert(t1 == t2, "Can't specify commutativity for type " + f.getType)
+
+ val ids @ Seq(x, y) = Seq("x", "y").map(name => FreshIdentifier(name, t1, true))
+ Forall(ids.map(ValDef(_)), Equals(
+ app(f, Variable(x), Variable(y)), app(f, Variable(y), Variable(x))))
+ }
+
+ def idempotent(f: Expr): Expr = {
+ val FunctionType(Seq(t1, t2), _) = f.getType
+ assert(t1 == t2, "Can't specify idempotency for type " + f.getType)
+
+ val ids @ Seq(x, y, z) = Seq("x", "y", "z").map(name => FreshIdentifier(name, t1, true))
+ Forall(ids.map(ValDef(_)), Equals(
+ app(f, Variable(x), Variable(y)),
+ app(f, Variable(x), app(f, Variable(x), Variable(y)))))
+ }
+
+ def rotative(f: Expr): Expr = {
+ val FunctionType(Seq(t1, t2), _) = f.getType
+ assert(t1 == t2, "Can't specify associativity for type " + f.getType)
+
+ val ids @ Seq(x, y, z) = Seq("x", "y", "z").map(name => FreshIdentifier(name, t1, true))
+ Forall(ids.map(ValDef(_)), Equals(
+ app(f, app(f, Variable(x), Variable(y)), Variable(z)),
+ app(f, app(f, Variable(y), Variable(z)), Variable(x))))
+ }
+
+ val satisfiable = List(
+ "paper 1" -> and(associative(Variable(f1)),
+ Not(Equals(app(Variable(f1), app(Variable(f1), bi(1), bi(2)), bi(3)),
+ app(Variable(f1), bi(1), app(Variable(f1), bi(2), bi(2)))))),
+ "paper 2" -> and(commutative(Variable(f1)), idempotent(Variable(f1)),
+ Not(Equals(app(Variable(f1), app(Variable(f1), bi(1), bi(2)), bi(2)),
+ app(Variable(f1), bi(1), app(Variable(f1), bi(2), app(Variable(f1), bi(1), bi(3))))))),
+ "assoc not comm int" -> and(associative(Variable(f1)), Not(commutative(Variable(f1)))),
+ "assoc not comm generic" -> and(associative(Variable(f2)), Not(commutative(Variable(f2)))),
+ "comm not assoc int" -> and(commutative(Variable(f1)), Not(associative(Variable(f1)))),
+ "comm not assoc generic" -> and(commutative(Variable(f2)), Not(associative(Variable(f2))))
+ )
+
+ val unification: Expr = {
+ val ids @ Seq(x, y) = Seq("x", "y").map(name => FreshIdentifier(name, IntegerType, true))
+ Forall(ids.map(ValDef(_)), Not(Equals(app(Variable(f1), Variable(x), Variable(y)), app(Variable(f1), Variable(y), Variable(x)))))
+ }
+
+ val unsatisfiable = List(
+ "comm + rotate = assoc int" -> and(commutative(Variable(f1)), rotative(Variable(f1)), Not(associative(Variable(f1)))),
+ "comm + rotate = assoc generic" -> and(commutative(Variable(f2)), rotative(Variable(f2)), Not(associative(Variable(f2)))),
+ "unification" -> unification
+ )
+
+ def checkSolver(solver: Solver, expr: Expr, sat: Boolean)(implicit fix: (LeonContext, Program)): Unit = {
+ try {
+ solver.assertCnstr(expr)
+ solver.check match {
+ 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!?")
+ }
+ } finally {
+ solver.free()
+ }
+ }
+
+ for ((sname, sf) <- getFactories; (ename, expr) <- satisfiable) {
+ test(s"Satisfiable quantified formula $ename in $sname") { implicit fix =>
+ val (ctx, pgm) = fix
+ val solver = sf(ctx, pgm)
+ checkSolver(solver, expr, true)
+ }
+
+ test(s"Satisfiable quantified formula $ename in $sname with partial models") { implicit fix =>
+ val (ctx, pgm) = fix
+ val newCtx = ctx.copy(options = ctx.options.filter(_ != UnrollingProcedure.optPartialModels) :+
+ LeonOption(UnrollingProcedure.optPartialModels)(true))
+ val solver = sf(newCtx, pgm)
+ checkSolver(solver, expr, true)
+ }
+ }
+
+ for ((sname, sf) <- getFactories; (ename, expr) <- unsatisfiable) {
+ test(s"Unsatisfiable quantified formula $ename in $sname") { implicit fix =>
+ val (ctx, pgm) = fix
+ val solver = sf(ctx, pgm)
+ checkSolver(solver, expr, false)
+ }
+ }
+}
diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala
index c5571fa4f..c95fb39d3 100644
--- a/src/test/scala/leon/integration/solvers/SolversSuite.scala
+++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala
@@ -32,57 +32,57 @@ class SolversSuite extends LeonTestSuiteWithProgram {
) else Nil)
}
- val types = Seq(
- BooleanType,
- UnitType,
- CharType,
+ val types = Seq(
+ BooleanType,
+ UnitType,
+ CharType,
RealType,
- IntegerType,
- Int32Type,
- StringType,
- TypeParameter.fresh("T"),
- SetType(IntegerType),
- MapType(IntegerType, IntegerType),
+ IntegerType,
+ Int32Type,
+ StringType,
+ TypeParameter.fresh("T"),
+ SetType(IntegerType),
+ MapType(IntegerType, IntegerType),
FunctionType(Seq(IntegerType), IntegerType),
- TupleType(Seq(IntegerType, BooleanType, Int32Type))
- )
+ TupleType(Seq(IntegerType, BooleanType, Int32Type))
+ )
- val vs = types.map(FreshIdentifier("v", _).toVariable)
+ val vs = types.map(FreshIdentifier("v", _).toVariable)
// We need to make sure models are not co-finite
val cnstrs = vs.map(v => v.getType match {
- case UnitType =>
- Equals(v, simplestValue(v.getType))
- case SetType(base) =>
- Not(ElementOfSet(simplestValue(base), v))
- case MapType(from, to) =>
- Not(Equals(MapApply(v, simplestValue(from)), simplestValue(to)))
+ case UnitType =>
+ Equals(v, simplestValue(v.getType))
+ case SetType(base) =>
+ Not(ElementOfSet(simplestValue(base), v))
+ case MapType(from, to) =>
+ Not(Equals(MapApply(v, simplestValue(from)), simplestValue(to)))
case FunctionType(froms, to) =>
Not(Equals(Application(v, froms.map(simplestValue)), simplestValue(to)))
- case _ =>
- not(Equals(v, simplestValue(v.getType)))
+ case _ =>
+ not(Equals(v, simplestValue(v.getType)))
})
def checkSolver(solver: Solver, vs: Set[Variable], cnstr: Expr)(implicit fix: (LeonContext, Program)): Unit = {
- try {
- solver.assertCnstr(cnstr)
+ try {
+ solver.assertCnstr(cnstr)
- solver.check match {
- case Some(true) =>
- val model = solver.getModel
- for (v <- vs) {
- if (model.isDefinedAt(v.id)) {
- assert(model(v.id).getType === v.getType, s"Solver $solver - Extracting value of type "+v.getType)
- } else {
- fail(s"Solver $solver - Model does not contain "+v.id.uniqueName+" of type "+v.getType)
- }
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
+ for (v <- vs) {
+ if (model.isDefinedAt(v.id)) {
+ assert(model(v.id).getType === v.getType, s"Solver $solver - Extracting value of type "+v.getType)
+ } else {
+ fail(s"Solver $solver - Model does not contain "+v.id.uniqueName+" of type "+v.getType)
}
- case _ =>
- fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!? Solver was "+solver.getClass)
- }
- } finally {
- solver.free()
+ }
+ case _ =>
+ fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!? Solver was "+solver.getClass)
}
+ } finally {
+ solver.free()
+ }
}
// Check that we correctly extract several types from solver models
@@ -99,6 +99,6 @@ class SolversSuite extends LeonTestSuiteWithProgram {
for ((v,cnstr) <- vs zip cnstrs) {
val solver = new EnumerationSolver(fix._1, fix._2)
checkSolver(solver, Set(v), cnstr)
-}
+ }
}
}
--
GitLab