diff --git a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala b/src/it/scala/inox/solvers/unrolling/QuantifiersSuite.scala
similarity index 75%
rename from src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
rename to src/it/scala/inox/solvers/unrolling/QuantifiersSuite.scala
index bb914c0536ec0418264b5d56af4479149f665673..b8f15db74140cc0888c2bb7f8e2077eedbd35b07 100644
--- a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/QuantifiersSuite.scala
@@ -4,7 +4,7 @@ package inox
package solvers
package unrolling
-class AssociativeQuantifiersSuite extends TestSuite {
+class QuantifiersSuite extends TestSuite {
import inox.trees._
import dsl._
@@ -45,10 +45,18 @@ class AssociativeQuantifiersSuite extends TestSuite {
})
}
+ val isIdempotentID = FreshIdentifier("isIdempotent")
+ val isIdempotent = mkFunDef(isIdempotentID)("A") { case Seq(aT) => (
+ Seq("f" :: ((aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
+ forall("x" :: aT, "y" :: aT)((x,y) => f(x,y) === f(x,f(x,y)))
+ })
+ }
+
val symbols = new Symbols(Map(
isAssociativeID -> isAssociative,
isCommutativeID -> isCommutative,
- isRotateID -> isRotate
+ isRotateID -> isRotate,
+ isIdempotentID -> isIdempotent
), Map.empty)
test("Pair of associative ==> associative pair") { ctx =>
@@ -101,4 +109,25 @@ class AssociativeQuantifiersSuite extends TestSuite {
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
}
+
+ test("Commutative + idempotent satisfiable") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val f = ("f" :: ((IntegerType, IntegerType) =>: IntegerType)).toVariable
+ val clause = isCommutative(IntegerType)(f) && isIdempotent(IntegerType)(f) &&
+ !(f(E(BigInt(1)), E(BigInt(2))) ===
+ f(f(E(BigInt(2)), E(BigInt(1))), E(BigInt(3))))
+
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
+ }
+
+ test("Unification is unsatisfiable") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val aT = T("A")
+ val f = ("f" :: ((aT, aT) =>: aT)).toVariable
+ val clause = forall("x" :: aT, "y" :: aT)((x,y) => !(f(x,y) === f(y,x)))
+
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
+ }
}
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 4e5bed2d032faf1933f3297bf4e5fe288d71e36d..6eca9bbb0ab26893ff1e9275463e787682e11f40 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -591,13 +591,20 @@ trait QuantificationTemplates { self: Templates =>
} else {
val substituter = mkSubstituter(map.mapValues(_.encoded))
val msubst = map.collect { case (q, Right(m)) => q -> m }
- val isOpt = optimizationQuorums.exists { ms =>
- handledMatchers.containsAll(ms.map(_.substitute(substituter, msubst)))
+ val opts = optimizationQuorums.flatMap { ms =>
+ val sms = ms.map(_.substitute(substituter, msubst))
+ if (handledMatchers.containsAll(sms)) sms.toList else Nil
}
- if (isOpt) 0
- else if (grounds(q)(bs, m.args(i))) 10
- else 3
+ if (opts.nonEmpty) {
+ val tms = matchers.flatMap(_._2.map(_.substitute(substituter, msubst)))
+ if (opts.map(totalDepth).max >= tms.map(totalDepth).max) 0
+ else 3
+ } else if (grounds(q)(bs, m.args(i))) {
+ 10
+ } else {
+ 3
+ }
}
(bs, map, c + cost)
diff --git a/src/test/scala/inox/solvers/SolverPoolSuite.scala b/src/test/scala/inox/solvers/SolverPoolSuite.scala
index 12d9a1417edb47c8e2f6f4d416fb1db312323a15..452fffcc98e1dfb7f07d923086266b8a4c68f28d 100644
--- a/src/test/scala/inox/solvers/SolverPoolSuite.scala
+++ b/src/test/scala/inox/solvers/SolverPoolSuite.scala
@@ -1,85 +1,86 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-//
-//package inox
-//package solvers
-//
-//import org.scalatest._
-//
-//import inox._
-//import inox.solvers._
-//import inox.solvers.combinators._
-//
-//class SolverPoolSuite extends FunSuite {
-// import inox.trees._
-//
-// implicit val ctx = InoxContext.empty
-//
-// private trait DummySolver extends Solver {
-// val name = "Dummy"
-// val description = "dummy"
-//
-// def check: Option[Boolean] = None
-// def assertCnstr(e: Expr) = {}
-// def free() {}
-// def reset() {}
-// def getModel = ???
-// def push() {}
-// def pop() {}
-// def interrupt() {}
-// def recoverInterrupt() {}
-// }
-//
-// def sfactory(implicit ctx: InoxContext): SolverFactory { val program: InoxProgram } = {
-// val p = InoxProgram(ctx, new Symbols(Map.empty, Map.empty))
-// SolverFactory.create(p)("dummy", () => new DummySolver {
-// val program: p.type = p
-// })
-// }
-//
-// val poolSize = 5;
-//
-// test(s"SolverPool has at least $poolSize solvers") {
-//
-// val sp = SolverPoolFactory(sfactory)
-//
-// var solvers = Set[Solver]()
-//
-// for (i <- 1 to poolSize) {
-// solvers += sp.getNewSolver()
-// }
-//
-// solvers.size === poolSize
-// }
-//
-// test("SolverPool reuses solvers") {
-//
-// val sp = SolverPoolFactory(sfactory)
-//
-// var solvers = Set[Solver]()
-//
-// for (i <- 1 to poolSize) {
-// val s = sp.getNewSolver()
-// solvers += s
-// sp.reclaim(s)
-// }
-//
-// for (i <- 1 to poolSize) {
-// val s = sp.getNewSolver()
-// assert(solvers contains s, "Solver not reused?")
-// sp.reclaim(s)
-// }
-// }
-//
-// test(s"SolverPool can grow") {
-//
-// val sp = SolverPoolFactory(sfactory)
-//
-// var solvers = Set[Solver]()
-//
-// for (i <- 1 to poolSize+3) {
-// solvers += sp.getNewSolver()
-// }
-//
-// solvers.size === poolSize+3
-// }
-//}
+
+package inox
+package solvers
+
+import org.scalatest._
+
+import inox.solvers.combinators._
+
+class SolverPoolSuite extends FunSuite {
+ import inox.trees._
+ import SolverResponses._
+
+ implicit val ctx = Context.empty
+
+ private trait DummySolver extends Solver {
+ val name = "Dummy"
+ val description = "dummy"
+ val program: InoxProgram
+
+ def assertCnstr(e: Expr) = ()
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions] = config.cast(Unknown)
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = config.cast(Unknown)
+ def free() = ()
+ def reset() = ()
+ def push() = ()
+ def pop() = ()
+ def interrupt() = ()
+ def recoverInterrupt() = ()
+ }
+
+ def sfactory(implicit ctx: Context): SolverFactory { val program: InoxProgram } = {
+ val p = InoxProgram(ctx, new Symbols(Map.empty, Map.empty))
+ SolverFactory.create(p)("dummy", () => new DummySolver {
+ val program: p.type = p
+ val options = ctx.options
+ })
+ }
+
+ val poolSize = 5
+
+ test(s"SolverPool has at least $poolSize solvers") {
+
+ val sp = SolverPoolFactory(sfactory)
+
+ var solvers = Set[Solver]()
+
+ for (i <- 1 to poolSize) {
+ solvers += sp.getNewSolver()
+ }
+
+ solvers.size === poolSize
+ }
+
+ test("SolverPool reuses solvers") {
+
+ val sp = SolverPoolFactory(sfactory)
+
+ var solvers = Set[Solver]()
+
+ for (i <- 1 to poolSize) {
+ val s = sp.getNewSolver()
+ solvers += s
+ sp.reclaim(s)
+ }
+
+ for (i <- 1 to poolSize) {
+ val s = sp.getNewSolver()
+ assert(solvers contains s, "Solver not reused?")
+ sp.reclaim(s)
+ }
+ }
+
+ test(s"SolverPool can grow") {
+
+ val sp = SolverPoolFactory(sfactory)
+
+ var solvers = Set[Solver]()
+
+ for (i <- 1 to poolSize+3) {
+ solvers += sp.getNewSolver()
+ }
+
+ solvers.size === poolSize+3
+ }
+}