diff --git a/build.sbt b/build.sbt
index 372c4cb07a8a429a2405ab61be47060b457fa63b..0c1f4400527fe9f724082d5c83f77bb84a38d141 100644
--- a/build.sbt
+++ b/build.sbt
@@ -92,6 +92,8 @@ concurrentRestrictions in Global += Tags.limit(Tags.Test, nParallel)
testOptions in Test := Seq(Tests.Argument("-oDF"))
+testOptions in IntegrationTest := Seq(Tests.Argument("-oDF"))
+
// Integration Tests
//lazy val IntegrTest = config("integration") extend(Test)
diff --git a/src/it/scala/inox/InoxTestSuite.scala b/src/it/scala/inox/InoxTestSuite.scala
index 4ca956cf14fe275609357255dc7cc8053b8e3aa8..9abb984f9d91cd9a9c39fb8f44f49d72cf371143 100644
--- a/src/it/scala/inox/InoxTestSuite.scala
+++ b/src/it/scala/inox/InoxTestSuite.scala
@@ -12,12 +12,19 @@ trait InoxTestSuite extends FunSuite with Matchers with Timeouts {
val configurations: Seq[Seq[InoxOption[Any]]] = Seq(Seq.empty)
- protected def test(name: String, tags: Tag*)(test: InoxContext => Unit): Unit = {
+ private def optionsString(options: InoxOptions): String = {
+ "solver=" + options.findOptionOrDefault(InoxOptions.optSelectedSolvers).head + " " +
+ "feelinglucky=" + options.findOptionOrDefault(solvers.unrolling.optFeelingLucky) + " " +
+ "checkmodels=" + options.findOptionOrDefault(solvers.optCheckModels) + " " +
+ "unrollassumptions=" + options.findOptionOrDefault(solvers.unrolling.optUnrollAssumptions)
+ }
+
+ protected def test(name: String, tags: Tag*)(body: InoxContext => Unit): Unit = {
for (config <- configurations) {
val reporter = new TestSilentReporter
val ctx = InoxContext(reporter, new InterruptManager(reporter), InoxOptions(config))
try {
- test(ctx)
+ super.test(name + " " + optionsString(ctx.options))(body(ctx))
} catch {
case err: FatalError =>
reporter.lastErrors :+= err.msg
@@ -25,4 +32,10 @@ trait InoxTestSuite extends FunSuite with Matchers with Timeouts {
}
}
}
+
+ protected def ignore(name: String, tags: Tag*)(body: InoxContext => Unit): Unit = {
+ for (config <- configurations) {
+ super.ignore(name + " " + optionsString(InoxOptions(config)))(())
+ }
+ }
}
diff --git a/src/it/scala/inox/TestSilentReporter.scala b/src/it/scala/inox/TestSilentReporter.scala
index 178262039cd630af9a5b13dfc7adfe01ffd5c413..96deee1c47d6b20025c24707fffc9c3e15c73b37 100644
--- a/src/it/scala/inox/TestSilentReporter.scala
+++ b/src/it/scala/inox/TestSilentReporter.scala
@@ -12,7 +12,7 @@ class TestSilentReporter extends DefaultReporter(Set()) {
}
override def debug(pos: utils.Position, msg: => Any)(implicit section: DebugSection): Unit = {
- println(msg)
+ //println(msg)
}
}
diff --git a/src/it/scala/inox/regression/SimpleSolversSuite.scala b/src/it/scala/inox/regression/SimpleSolversSuite.scala
deleted file mode 100644
index 175cdab263759f6500ed2f0147e28dbbcdd58865..0000000000000000000000000000000000000000
--- a/src/it/scala/inox/regression/SimpleSolversSuite.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package inox
-package regression
-
-class SimpleSolversSuite extends InoxTestSuite {
-
-
-}
diff --git a/src/it/scala/inox/SolvingTestSuite.scala b/src/it/scala/inox/solvers/SolvingTestSuite.scala
similarity index 97%
rename from src/it/scala/inox/SolvingTestSuite.scala
rename to src/it/scala/inox/solvers/SolvingTestSuite.scala
index 348906f82f787e3a6c0c11448c11b80691d802ae..63bc046642c7348fc838adf954a11b79427193b5 100644
--- a/src/it/scala/inox/SolvingTestSuite.scala
+++ b/src/it/scala/inox/solvers/SolvingTestSuite.scala
@@ -1,9 +1,9 @@
/* Copyright 2009-2016 EPFL, Lausanne */
package inox
+package solvers
trait SolvingTestSuite extends InoxTestSuite {
- import solvers._
override val configurations = for {
solverName <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4")
diff --git a/src/it/scala/inox/regression/SimpleQuantifiersSuite.scala b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
similarity index 70%
rename from src/it/scala/inox/regression/SimpleQuantifiersSuite.scala
rename to src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
index a21b07ef51c3049f3164395c0c0b592bfcdddcee..df07e5468621937b44387befe2445f9878763af4 100644
--- a/src/it/scala/inox/regression/SimpleQuantifiersSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
@@ -1,11 +1,10 @@
/* Copyright 2009-2016 EPFL, Lausanne */
package inox
-package regression
+package solvers
+package unrolling
-import solvers._
-
-class SimpleQuantifiersSuite extends SolvingTestSuite {
+class AssociativeQuantifiersSuite extends SolvingTestSuite {
import inox.trees._
import dsl._
@@ -36,7 +35,7 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
isRotateID -> isRotate
), Map.empty)
- test("Pair of associative ==> associative pair") { ctx =>
+ ignore("Pair of associative ==> associative pair") { ctx =>
val program = InoxProgram(ctx, symbols)
val (aT,bT) = (T("A"), T("B"))
@@ -45,55 +44,45 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
\("p1" :: T(aT,bT), "p2" :: T(aT, bT))((p1,p2) => E(f1(p1._1,p2._1), f2(p1._2,p2._2)))
}
- val sf = SolverFactory.default(program)
- val api = SimpleSolverAPI(sf)
- assert(api.solveSAT(clause).isUNSAT)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
}
- test("Commutative and rotate ==> associative") { ctx =>
+ ignore("Commutative and rotate ==> associative") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = T("A")
val f = ("f" :: ((aT, aT) =>: aT)).toVariable
val clause = isCommutative(aT)(f) && isRotate(aT)(f) && !isAssociative(aT)(f)
- val sf = SolverFactory.default(program)
- val api = SimpleSolverAPI(sf)
- assert(api.solveSAT(clause).isUNSAT)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
}
- test("Commutative and rotate ==> associative (integer type)") { ctx =>
+ ignore("Commutative and rotate ==> associative (integer type)") { ctx =>
val program = InoxProgram(ctx, symbols)
val f = ("f" :: ((IntegerType, IntegerType) =>: IntegerType)).toVariable
val clause = isCommutative(IntegerType)(f) && isRotate(IntegerType)(f) && !isAssociative(IntegerType)(f)
- val sf = SolverFactory.default(program)
- val api = SimpleSolverAPI(sf)
- assert(api.solveSAT(clause).isUNSAT)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
}
- test("Associatve =!=> commutative") { ctx =>
+ ignore("Associatve =!=> commutative") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = T("A")
val f = ("f" :: ((aT, aT) =>: aT)).toVariable
val clause = isAssociative(aT)(f) && !isCommutative(aT)(f)
- val sf = SolverFactory.default(program)
- val api = SimpleSolverAPI(sf)
- assert(api.solveSAT(clause).isSAT)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
}
- test("Commutative =!=> associative") { ctx =>
+ ignore("Commutative =!=> associative") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = T("A")
val f = ("f" :: ((aT, aT) =>: aT)).toVariable
val clause = isCommutative(aT)(f) && !isAssociative(aT)(f)
- val sf = SolverFactory.default(program)
- val api = SimpleSolverAPI(sf)
- assert(api.solveSAT(clause).isSAT)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
}
}
diff --git a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..aabaeca997e6987049c42b20c8222b87b32a9376
--- /dev/null
+++ b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+package unrolling
+
+class InductiveUnrollingSuite extends SolvingTestSuite {
+ import trees._
+ import dsl._
+
+
+
+}
diff --git a/src/it/scala/inox/solvers/unrolling/SimpleUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/SimpleUnrollingSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..24d46a798a0dacda2d523883bb6fb46813b9dd51
--- /dev/null
+++ b/src/it/scala/inox/solvers/unrolling/SimpleUnrollingSuite.scala
@@ -0,0 +1,102 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+package unrolling
+
+class SimpleUnrollingSuite extends SolvingTestSuite {
+ import inox.trees._
+ import dsl._
+
+ import SolverResponses._
+
+ val listID = FreshIdentifier("List")
+ val consID = FreshIdentifier("Cons")
+ val nilID = FreshIdentifier("Nil")
+
+ val head = FreshIdentifier("head")
+ val tail = FreshIdentifier("tail")
+
+ val List = mkAbstractClass(listID)("A")(Seq(consID, nilID))
+ val Nil = mkCaseClass(nilID)("A")(Some(listID))(_ => Seq.empty)
+ val Cons = mkCaseClass(consID)("A")(Some(listID)) {
+ case Seq(aT) => Seq(ValDef(head, aT), ValDef(tail, T(listID)(aT)))
+ }
+
+ val sizeID = FreshIdentifier("size")
+ val sizeFd = mkFunDef(sizeID)("A") { case Seq(aT) => (
+ Seq("l" :: T(listID)(aT)), IntegerType, { case Seq(l) =>
+ if_ (l.isInstOf(T(consID)(aT))) {
+ E(BigInt(1)) + E(sizeID)(aT)(l.asInstOf(T(consID)(aT)).getField(tail))
+ } else_ {
+ E(BigInt(0))
+ }
+ })
+ }
+
+ val symbols = new Symbols(
+ Map(sizeID -> sizeFd),
+ Map(listID -> List, consID -> Cons, nilID -> Nil)
+ )
+
+ test("size(x) > 0 is satisfiable") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val vd: ValDef = "x" :: T(listID)(IntegerType)
+ val clause = sizeFd(IntegerType)(vd.toVariable) > E(BigInt(0))
+
+ SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause) match {
+ case SatWithModel(model) =>
+ symbols.valuateWithModel(model)(vd) match {
+ case CaseClass(ClassType(`consID`, Seq(IntegerType)), _) =>
+ // success!!
+ case r =>
+ fail("Unexpected valuation: " + r)
+ }
+
+ case r =>
+ fail("Unexpected response: " + r)
+ }
+ }
+
+ test("size(x) == 0 is satisfiable") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val tp = TypeParameter.fresh("A")
+ val vd: ValDef = "x" :: T(listID)(tp)
+ val clause = sizeFd(tp)(vd.toVariable) === E(BigInt(0))
+
+ SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause) match {
+ case SatWithModel(model) =>
+ symbols.valuateWithModel(model)(vd) match {
+ case CaseClass(ClassType(`nilID`, Seq(tp)), Seq()) =>
+ // success!!
+ case r =>
+ fail("Unexpected valuation: " + r)
+ }
+
+ case r =>
+ fail("Unexpected response: " + r)
+ }
+ }
+
+ test("size(x) < 0 is not satisfiable (unknown)") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val vd: ValDef = "x" :: T(listID)(IntegerType)
+ val clause = sizeFd(IntegerType)(vd.toVariable) < E(BigInt(0))
+
+ assert(!SimpleSolverAPI(SolverFactory.default(program).withTimeout(100)).solveSAT(clause).isSAT)
+ }
+
+ test("size(x) > size(y) is satisfiable") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val x: ValDef = "x" :: T(listID)(IntegerType)
+ val y: ValDef = "y" :: T(listID)(IntegerType)
+ val clause = sizeFd(IntegerType)(x.toVariable) > sizeFd(IntegerType)(y.toVariable)
+
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
+ }
+
+}
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index bd4766373748d195660355797b85f924a0b0cb3f..b14cb7cac96901990bd7b81f91a1c0741fdb67e1 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -240,7 +240,7 @@ trait Expressions { self: Trees =>
/** $encodingof `.isInstanceOf[...]` */
case class IsInstanceOf(expr: Expr, classType: ClassType) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type =
- if (s.isSubtypeOf(expr.getType, classType)) BooleanType else Untyped
+ if (s.typesCompatible(expr.getType, classType)) BooleanType else Untyped
}
/** $encodingof `expr.asInstanceOf[tpe]`
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index 79e0c4fdc9780df0db79e885255e4e14e30db2fa..c6d1a97217975563594f04712c18f852f6e3550b 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -93,6 +93,7 @@ trait TypeOps {
} else {
(cd1 == cd2).option(cd1)
}
+
for {
cd <- bound
(subs, map) <- flatten((ct1.tps zip ct2.tps).map { case (tp1, tp2) =>
@@ -272,7 +273,7 @@ trait TypeOps {
case accd: TypedAbstractClassDef =>
accd.descendants.map(_.toType)
case tccd: TypedCaseClassDef =>
- tccd.fieldsTypes
+ tccd.fieldsTypes ++ tccd.parent.map(_.toType)
}
case NAryType(tps, _) =>
tps
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 7e5ab5c7d0c3a4729278967b182707e38284bb1c..18a7e5c07f049281b26b5f07a56cf91ad8d33256 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -55,7 +55,8 @@ trait SolvingEvaluator extends Evaluator {
val sf = getSolver(
InoxOption(optSilentErrors)(true),
- InoxOption(optCheckModels)(false),
+ InoxOption(optCheckModels)(false), // model is checked manually!! (see below)
+ InoxOption(unrolling.optFeelingLucky)(false),
InoxOption(optForallCache)(cache)
)
diff --git a/src/main/scala/inox/solvers/ADTManagers.scala b/src/main/scala/inox/solvers/ADTManagers.scala
index 2dd2e707877f516836fe692fe52068eb5dcd093c..ca0f74363b83e9478defebb53c9fe5636ddac9c9 100644
--- a/src/main/scala/inox/solvers/ADTManagers.scala
+++ b/src/main/scala/inox/solvers/ADTManagers.scala
@@ -51,7 +51,7 @@ trait ADTManagers {
case _ =>
}
- for (scc <- sccs) {
+ for (scc <- sccs.map(scc => scc.map(bestRealType))) {
val declarations = (for (tpe <- scc if !declared(tpe)) yield (tpe match {
case ct: ClassType =>
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 1d6b48f41851aad983316dd0b14d5e9b174f61ce..c96cc9c351c1f3051d7f58b7cf78e1214851b028 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -37,7 +37,7 @@ object SolverFactory {
import combinators._
private val solverNames = Map(
- "nativez3" -> "Native Z3 with z3-templates for unrolling (default)",
+ "nativez3" -> "Native Z3 with z3-templates for unrolling",
"unrollz3" -> "Native Z3 with leon-templates for unrolling",
"smt-cvc4" -> "CVC4 through SMT-LIB",
"smt-z3" -> "Z3 through SMT-LIB",
@@ -117,6 +117,6 @@ object SolverFactory {
}
}
- def default(p: InoxProgram): SolverFactory { val program: p.type } =
+ def default(p: InoxProgram): SolverFactory { val program: p.type; type S <: TimeoutSolver } =
apply(p, p.ctx.options)
}
diff --git a/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala b/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
index 0c20fddc9d5ec4112588fb82e627e40ab97ba7fc..51c746358736ac9390a417f8a1e8397803a38f2d 100644
--- a/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
+++ b/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
@@ -18,7 +18,7 @@ trait TimeoutSolverFactory extends SolverFactory {
override def getNewSolver() = factory.getNewSolver().setTimeout(to)
- override val name = factory.name+" with t.o"
+ override lazy val name = factory.name+" with t.o"
override def reclaim(s: S) = factory.reclaim(s)
diff --git a/src/main/scala/inox/solvers/package.scala b/src/main/scala/inox/solvers/package.scala
index 2fcab5abac35e61c4a9ddc1357cb4133b59f5121..1a34eae08c15a480763866466db9662937531497 100644
--- a/src/main/scala/inox/solvers/package.scala
+++ b/src/main/scala/inox/solvers/package.scala
@@ -2,31 +2,51 @@
package inox
+import scala.language.implicitConversions
import scala.concurrent.duration._
package object solvers {
import combinators._
- implicit class TimeoutableSolverFactory[S1 <: TimeoutSolver](val sf: SolverFactory { type S = S1 }) {
- def withTimeout(timeout: Long): TimeoutSolverFactory { type S <: S1 } = {
- val innerFactory = (sf match {
+ /* XXX: We use an implicit conversion here instead of an implicit
+ * class in order for dependent types to work correctly. */
+ implicit def factoryToTimeoutableFactory(sf: SolverFactory {
+ type S <: TimeoutSolver
+ }): TimeoutableFactory {
+ val factory: sf.type
+ type S = sf.S { val program: sf.program.type }
+ } = new TimeoutableFactory {
+ val factory: sf.type = sf
+ type S = sf.S { val program:sf.program.type }
+ }
+
+ trait TimeoutableFactory { self =>
+ val factory: SolverFactory { type S <: TimeoutSolver }
+
+ def withTimeout(timeout: Long): TimeoutSolverFactory {
+ val program: self.factory.program.type
+ type S = self.factory.S { val program: self.factory.program.type }
+ } = {
+ val innerFactory = (factory match {
case tsf: TimeoutSolverFactory => tsf.factory
- case _ => sf
+ case _ => factory
}).asInstanceOf[SolverFactory {
- val program: sf.program.type
- type S = S1 { val program: sf.program.type }
+ val program: self.factory.program.type
+ type S = self.factory.S { val program: self.factory.program.type }
}]
new TimeoutSolverFactory {
- val program: sf.program.type = sf.program
- type S = S1 { val program: sf.program.type }
+ val program: self.factory.program.type = innerFactory.program
+ type S = self.factory.S { val program: self.factory.program.type }
val to = timeout
val factory = innerFactory
}
}
- def withTimeout(du: Duration): TimeoutSolverFactory { type S <: S1 } = {
- withTimeout(du.toMillis)
- }
+ def withTimeout(du: Duration): TimeoutSolverFactory {
+ val program: self.factory.program.type
+ type S = self.factory.S { val program: self.factory.program.type }
+ } = withTimeout(du.toMillis)
}
+
}
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
index e19fc66c81935f09bfc05e995eb65ed312e814a8..b76460324fbc3b6e6651eb5428c17a8edfa21d8c 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
@@ -7,6 +7,8 @@ package smtlib
import inox.OptionParsers._
trait CVC4Solver extends SMTLIBSolver with CVC4Target {
+ import program.trees._
+ import SolverResponses._
def interpreterOps(ctx: InoxContext) = {
Seq(
@@ -19,6 +21,19 @@ trait CVC4Solver extends SMTLIBSolver with CVC4Target {
"--lang", "smt2.5"
) ++ options.findOptionOrDefault(optCVC4Options)
}
+
+ override def checkAssumptions(config: Configuration)(assumptions: Set[Expr]) = {
+ push()
+ for (cl <- assumptions) assertCnstr(cl)
+ val res: SolverResponse[Model, Assumptions] = check(Model min config)
+ pop()
+
+ config.cast(res match {
+ case Unsat if config.withUnsatAssumptions =>
+ UnsatWithAssumptions(Set.empty)
+ case _ => res
+ })
+ }
}
object optCVC4Options extends InoxOptionDef[Set[String]] {
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
index 0d4449f40eda45254bea0250221bed31e3a68696..cae4b915a78665bf7860f20a682e8ac340d2e578 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
@@ -53,7 +53,7 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
}
}
- private def extractResponse(config: Configuration, res: SExpr): config.Response[Model, Assumptions] =
+ protected def extractResponse(config: Configuration, res: SExpr): config.Response[Model, Assumptions] = {
config.cast(res match {
case CheckSatStatus(SatStatus) =>
if (config.withModel) {
@@ -101,6 +101,7 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
case CheckSatStatus(UnknownStatus) => Unknown
case e => Unknown
})
+ }
def check(config: CheckConfiguration): config.Response[Model, Assumptions] =
extractResponse(config, emit(CheckSat()))
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index a89a8ab6c66dffc730dcfbf03cef25643e0ced18..c072fda15b720353b417c83ae4194a731b0498c7 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -152,7 +152,6 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
body: Expr)
(implicit bindings: Map[Identifier, Term])
: Term = {
- if (vars.isEmpty) toSMT(body)
if (vars.isEmpty) toSMT(body)(Map())
else {
val sortedVars = vars map { vd =>
diff --git a/src/main/scala/inox/solvers/smtlib/Z3Solver.scala b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
index b8d50712b027379ade7893b3cb1bff63ed434e17..d0b608091ca699e29d4c4371e0de0d83b0ce4c84 100644
--- a/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
@@ -4,4 +4,27 @@ package inox
package solvers
package smtlib
-trait Z3Solver extends SMTLIBSolver with Z3Target
+import _root_.smtlib.parser.Terms.{Identifier => _, _}
+import _root_.smtlib.parser.CommandsResponses._
+
+trait Z3Solver extends SMTLIBSolver with Z3Target {
+ import program.trees._
+ import SolverResponses._
+
+ /** Z3 uses a non-standard syntax for check-sat-assuming, namely
+ * {{{
+ * (check-sat a1 ... an)
+ * }}}
+ * so we have to use a [[_root_.smtlib.parser.Terms.SList]] to actually
+ * send the command to the underlying smtlib solver.
+ */
+ override def checkAssumptions(config: Configuration)(assumptions: Set[Expr]) = {
+ val cmd = SList(SSymbol("check-sat") +: assumptions.toSeq.map(as => toSMT(as)(Map.empty)) : _*)
+ val res = emit(cmd) match {
+ case SSymbol("sat") => CheckSatStatus(SatStatus)
+ case SSymbol("unsat") => CheckSatStatus(UnsatStatus)
+ case res => res
+ }
+ extractResponse(config, res)
+ }
+}
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index d50c5feff0e729011e162372e55ab1a02b358ef5..27f1edf537fd4e19cd7644db1f51e502096b3da9 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -192,7 +192,9 @@ trait QuantificationTemplates { self: Templates =>
val quantifications = new IncrementalSeq[Quantification]
val ignoredMatchers = new IncrementalSeq[(Int, Set[Encoded], Matcher)]
- val handledMatchers = new IncrementalSeq[(Set[Encoded], Matcher)]
+
+ // to avoid [[MatcherSet]] escaping defining context, we must keep this ~private
+ private[QuantificationTemplates] val handledMatchers = new MatcherSet
val ignoredSubsts = new IncrementalMap[Quantification, Set[(Int, Set[Encoded], Map[Encoded,Arg])]]
val handledSubsts = new IncrementalMap[Quantification, Set[(Set[Encoded], Map[Encoded,Arg])]]
@@ -203,6 +205,11 @@ trait QuantificationTemplates { self: Templates =>
val incrementals: Seq[IncrementalState] = Seq(
quantifications, ignoredMatchers, handledMatchers, ignoredSubsts, handledSubsts, lambdaAxioms, templates)
+ override def push(): Unit = { super.push(); for (q <- quantifications) q.push() }
+ override def pop(): Unit = { super.pop(); for (q <- quantifications) q.pop() }
+ override def clear(): Unit = { super.clear(); for (q <- quantifications) q.clear() }
+ override def reset(): Unit = { super.reset(); for (q <- quantifications) q.reset() }
+
private def assumptions: Seq[Encoded] =
quantifications.collect { case q: GeneralQuantification => q.currentQ2Var }
@@ -240,8 +247,13 @@ trait QuantificationTemplates { self: Templates =>
@inline
private def instantiateMatcher(blockers: Set[Encoded], matcher: Matcher): Clauses = {
- handledMatchers += blockers -> matcher
- quantifications.flatMap(_.instantiate(blockers, matcher))
+ if (handledMatchers(blockers -> matcher)) {
+ Seq.empty
+ } else {
+ //println(blockers -> matcher)
+ handledMatchers += blockers -> matcher
+ quantifications.flatMap(_.instantiate(blockers, matcher))
+ }
}
def hasQuantifiers: Boolean = quantifications.nonEmpty
@@ -278,13 +290,11 @@ trait QuantificationTemplates { self: Templates =>
private def correspond(m1: Matcher, m2: Matcher): Boolean =
correspond(matcherKey(m1), matcherKey(m2))
- private class GroundSet private(
- private val map: MutableMap[Arg, MutableSet[Set[Encoded]]]
- ) extends Iterable[(Set[Encoded], Arg)] {
+ private trait BlockedSet[Element] extends Iterable[(Set[Encoded], Element)] with IncrementalState {
+ private var map: MutableMap[Element, MutableSet[Set[Encoded]]] = MutableMap.empty
+ private val stack = new MutableStack[MutableMap[Element, MutableSet[Set[Encoded]]]]
- def this() = this(MutableMap.empty)
-
- def apply(p: (Set[Encoded], Arg)): Boolean = map.get(p._2) match {
+ def apply(p: (Set[Encoded], Element)): Boolean = map.get(p._2) match {
case Some(blockerSets) => blockerSets(p._1) ||
// we assume here that iterating through the powerset of `p._1`
// will be significantly faster then iterating through `blockerSets`
@@ -292,18 +302,18 @@ trait QuantificationTemplates { self: Templates =>
case None => false
}
- def +=(p: (Set[Encoded], Arg)): Unit = if (!this(p)) map.get(p._2) match {
+ def +=(p: (Set[Encoded], Element)): Unit = if (!this(p)) map.get(p._2) match {
case Some(blockerSets) => blockerSets += p._1
case None => map(p._2) = MutableSet.empty + p._1
}
- def iterator: Iterator[(Set[Encoded], Arg)] = new collection.AbstractIterator[(Set[Encoded], Arg)] {
- private val mapIt: Iterator[(Arg, MutableSet[Set[Encoded]])] = GroundSet.this.map.iterator
+ def iterator: Iterator[(Set[Encoded], Element)] = new collection.AbstractIterator[(Set[Encoded], Element)] {
+ private val mapIt: Iterator[(Element, MutableSet[Set[Encoded]])] = BlockedSet.this.map.iterator
private var setIt: Iterator[Set[Encoded]] = Iterator.empty
- private var current: Arg = _
+ private var current: Element = _
def hasNext = mapIt.hasNext || setIt.hasNext
- def next: (Set[Encoded], Arg) = if (setIt.hasNext) {
+ def next: (Set[Encoded], Element) = if (setIt.hasNext) {
val bs = setIt.next
bs -> current
} else {
@@ -314,15 +324,31 @@ trait QuantificationTemplates { self: Templates =>
}
}
- override def clone: GroundSet = {
- val newMap: MutableMap[Arg, MutableSet[Set[Encoded]]] = MutableMap.empty
+ def push(): Unit = {
+ val newMap: MutableMap[Element, MutableSet[Set[Encoded]]] = MutableMap.empty
for ((e, bss) <- map) {
newMap += e -> bss.clone
}
- new GroundSet(newMap)
+ stack.push(map)
+ map = newMap
+ }
+
+ def pop(): Unit = {
+ map = stack.pop()
}
+
+ def clear(): Unit = {
+ stack.clear()
+ map = MutableMap.empty
+ }
+
+ def reset(): Unit = clear()
}
+ private class GroundSet extends BlockedSet[Arg]
+
+ private class MatcherSet extends BlockedSet[Matcher]
+
private def totalDepth(m: Matcher): Int = 1 + m.args.map {
case Right(ma) => totalDepth(ma)
case _ => 0
@@ -331,7 +357,7 @@ trait QuantificationTemplates { self: Templates =>
private def encodeEnablers(es: Set[Encoded]): Encoded =
if (es.isEmpty) trueT else mkAnd(es.toSeq.sortBy(_.toString) : _*)
- private[solvers] trait Quantification {
+ private[solvers] trait Quantification extends IncrementalState {
val pathVar: (Variable, Encoded)
val quantifiers: Seq[(Variable, Encoded)]
val condVars: Map[Variable, Encoded]
@@ -362,6 +388,11 @@ trait QuantificationTemplates { self: Templates =>
private val grounds: Map[Encoded, GroundSet] = quantified.map(q => q -> new GroundSet).toMap
+ def push(): Unit = for (gs <- grounds.values) gs.push()
+ def pop(): Unit = for (gs <- grounds.values) gs.pop()
+ def clear(): Unit = for (gs <- grounds.values) gs.clear()
+ def reset(): Unit = for (gs <- grounds.values) gs.reset()
+
def instantiate(bs: Set[Encoded], m: Matcher): Clauses = {
/* Build mappings from quantifiers to all potential ground values previously encountered. */
@@ -814,7 +845,7 @@ trait QuantificationTemplates { self: Templates =>
def getGroundInstantiations(e: Encoded, tpe: Type): Seq[(Encoded, Seq[Encoded])] = {
val bestTpe = bestRealType(tpe)
- handledMatchers.flatMap { case (bs, m) =>
+ handledMatchers.toSeq.flatMap { case (bs, m) =>
val enabler = encodeEnablers(bs)
val optArgs = matcherKey(m) match {
case TypeKey(tpe) if bestTpe == tpe => Some(m.args.map(_.encoded))
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index 696b3596bb73eeeaeb30fbe3338abeb10ebd2cc0..3e0af30b5d11fb73d77e5fd5068bbe289049ebc9 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -201,7 +201,7 @@ trait Templates extends TemplateGenerator
/** Represents an E-matching matcher that will be used to instantiate relevant quantified propositions */
case class Matcher(key: Either[(Encoded, Type), TypedFunDef], args: Seq[Arg], encoded: Encoded) {
override def toString: String = (key match {
- case Left((c, tpe)) => asString(c) + ":" + tpe.asString
+ case Left((c, tpe)) => asString(c)
case Right(tfd) => tfd.signature
}) + args.map {
case Right(m) => m.toString