diff --git a/build.sbt b/build.sbt
index 0c1f4400527fe9f724082d5c83f77bb84a38d141..9b0df3e328387f6987f285e165c42f94d3182b07 100644
--- a/build.sbt
+++ b/build.sbt
@@ -16,8 +16,6 @@ scalacOptions ++= Seq(
scalacOptions in (Compile, doc) ++= Seq("-doc-root-content", baseDirectory.value+"/src/main/scala/root-doc.txt")
-javacOptions += "-Xlint:unchecked"
-
site.settings
site.sphinxSupport()
@@ -50,82 +48,12 @@ libraryDependencies ++= Seq(
//"com.regblanc" %% "scala-smtlib" % "0.2"
)
-lazy val nParallel = {
- val p = System.getProperty("parallel")
- if (p ne null) {
- try {
- p.toInt
- } catch {
- case nfe: NumberFormatException =>
- 1
- }
- } else {
- 1
- }
-}
-
-sourceGenerators in Compile <+= Def.task {
- val build = (sourceManaged in Compile).value / "inox" / "Build.scala";
- IO.write(build, s"""|package inox
- |
- |object Build {
- | val baseDirectory = \"\"\"${baseDirectory.value.toString}\"\"\"
- |}""".stripMargin)
- Seq(build)
-}
-
-
-sourcesInBase in Compile := false
-
Keys.fork in run := true
-
-lazy val testSettings = Seq(
- //Keys.fork := true,
- logBuffered := (nParallel > 1),
- parallelExecution := (nParallel > 1)
- //testForkedParallel := true,
- //javaOptions ++= Seq("-Xss64M", "-Xmx4G")
-)
-
-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)
-
-//testOptions in IntegrTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "inox.integration."))
-
-
-def regressionFilter(name: String, native: Boolean = false): Boolean = name.startsWith("inox.regression") && (name.endsWith("NativeZ3") == native)
-
-// Regression Tests
-lazy val RegressionTest = config("regression") extend(Test)
-
-testOptions in RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(regressionFilter(_)))
-
-// Regression Tests that heavily depend on native Z3
-lazy val NativeZ3RegressionTest = config("native") extend(Test)
-
-testOptions in NativeZ3RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(regressionFilter(_, native = true)))
-
-parallelExecution in NativeZ3RegressionTest := false
-
-logBuffered in NativeZ3RegressionTest := false
-
-
-// Isabelle Tests
-lazy val IsabelleTest = config("isabelle") extend(Test)
-
-testOptions in IsabelleTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "inox.isabelle."))
-
-parallelExecution in IsabelleTest := false
-fork in IsabelleTest := true
-
-
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "10eaaee4ea0ff6567f4f866922cb871bae2da0ac")
@@ -134,6 +62,10 @@ lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "8883
lazy val root = (project in file("."))
.configs(IntegrationTest)
.settings(Defaults.itSettings : _*)
+ .settings(inConfig(IntegrationTest)(Defaults.testTasks ++ Seq(
+ logBuffered := false,
+ parallelExecution := false
+ )) : _*)
.dependsOn(bonsai)
.dependsOn(scalaSmtlib)
diff --git a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
index df07e5468621937b44387befe2445f9878763af4..5385e3a88a3b48cee3e321ed2132eed455699410 100644
--- a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
@@ -35,7 +35,7 @@ class AssociativeQuantifiersSuite extends SolvingTestSuite {
isRotateID -> isRotate
), Map.empty)
- ignore("Pair of associative ==> associative pair") { ctx =>
+ test("Pair of associative ==> associative pair") { ctx =>
val program = InoxProgram(ctx, symbols)
val (aT,bT) = (T("A"), T("B"))
@@ -47,7 +47,7 @@ class AssociativeQuantifiersSuite extends SolvingTestSuite {
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
}
- ignore("Commutative and rotate ==> associative") { ctx =>
+ test("Commutative and rotate ==> associative") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = T("A")
@@ -57,7 +57,7 @@ class AssociativeQuantifiersSuite extends SolvingTestSuite {
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
}
- ignore("Commutative and rotate ==> associative (integer type)") { ctx =>
+ test("Commutative and rotate ==> associative (integer type)") { ctx =>
val program = InoxProgram(ctx, symbols)
val f = ("f" :: ((IntegerType, IntegerType) =>: IntegerType)).toVariable
@@ -66,7 +66,7 @@ class AssociativeQuantifiersSuite extends SolvingTestSuite {
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
}
- ignore("Associatve =!=> commutative") { ctx =>
+ test("Associatve =!=> commutative") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = T("A")
@@ -76,7 +76,7 @@ class AssociativeQuantifiersSuite extends SolvingTestSuite {
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
}
- ignore("Commutative =!=> associative") { ctx =>
+ test("Commutative =!=> associative") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = T("A")
diff --git a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
index aabaeca997e6987049c42b20c8222b87b32a9376..5484297fd89083e9f2779377fa04fbdd8e1d76d8 100644
--- a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
@@ -8,6 +8,110 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
import trees._
import dsl._
-
+ 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)) + let("res" :: IntegerType, E(sizeID)(aT)(l.asInstOf(T(consID)(aT)).getField(tail))) {
+ res => Assume(res >= E(BigInt(0)), res)
+ }
+ } else_ {
+ E(BigInt(0))
+ }
+ })
+ }
+
+ val appendID = FreshIdentifier("append")
+ val append = mkFunDef(appendID)("A") { case Seq(aT) => (
+ Seq("l1" :: T(listID)(aT), "l2" :: T(listID)(aT)), T(listID)(aT), { case Seq(l1, l2) =>
+ if_ (l1.isInstOf(T(consID)(aT))) {
+ let("c" :: T(listID)(aT), l1.asInstOf(T(consID)(aT))) { c =>
+ T(consID)(aT)(c.getField(head), E(appendID)(aT)(c.getField(tail), l2))
+ }
+ } else_ {
+ l2
+ }
+ })
+ }
+
+ val flatMapID = FreshIdentifier("flatMap")
+ val flatMap = mkFunDef(flatMapID)("A","B") { case Seq(aT, bT) => (
+ Seq("l" :: T(listID)(aT), "f" :: (aT =>: T(listID)(bT))), T(listID)(bT), { case Seq(l, f) =>
+ if_ (l.isInstOf(T(consID)(aT))) {
+ let("c" :: T(consID)(aT), l.asInstOf(T(consID)(aT))) { c =>
+ append(bT)(f(c.getField(head)), E(flatMapID)(aT,bT)(c.getField(tail), f))
+ }
+ } else_ {
+ T(nilID)(bT)()
+ }
+ })
+ }
+
+ val assocID = FreshIdentifier("associative_lemma")
+ val associative = mkFunDef(assocID)("A","B","C") { case Seq(aT, bT, cT) => (
+ Seq("l1" :: T(listID)(aT), "l2" :: T(listID)(bT), "l3" :: T(listID)(cT),
+ "f" :: (aT =>: T(listID)(bT)), "g" :: (bT =>: T(listID)(cT))), BooleanType,
+ { case Seq(l1, l2, l3, f, g) =>
+ (if_ (l3.isInstOf(T(consID)(cT))) {
+ Assume(E(assocID)(aT, bT, cT)(l1, l2, l3.asInstOf(T(consID)(cT)).getField(tail), f, g), E(true))
+ } else_ {
+ if_ (l2.isInstOf(T(consID)(bT))) {
+ let("c" :: T(consID)(bT), l2.asInstOf(T(consID)(bT))) { c =>
+ Assume(E(assocID)(aT, bT, cT)(l1, c.getField(tail), g(c.getField(head)), f, g), E(true))
+ }
+ } else_ {
+ if_ (l1.isInstOf(T(consID)(aT))) {
+ let("c" :: T(consID)(aT), l1.asInstOf(T(consID)(aT))) { c =>
+ Assume(E(assocID)(aT, bT, cT)(c.getField(tail), f(c.getField(head)), T(nilID)(cT)(), f, g), E(true))
+ }
+ } else_ {
+ E(true)
+ }
+ }
+ }) && append(cT)(l3, flatMap(bT,cT)(append(bT)(l2, flatMap(aT,bT)(l1, f)), g)) ===
+ append(cT)(append(cT)(l3, flatMap(bT,cT)(l2, g)), flatMap(aT,cT)(l1, \("x" :: aT) { x =>
+ flatMap(bT,cT)(f(x), g)
+ }))
+ })
+ }
+
+ val symbols = new Symbols(
+ Map(sizeID -> sizeFd, appendID -> append, flatMapID -> flatMap, assocID -> associative),
+ Map(listID -> List, consID -> Cons, nilID -> Nil)
+ )
+
+ test("size(x) == 0 is satisfiable") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+ val vd = "x" :: T(listID)(IntegerType)
+ val clause = sizeFd(IntegerType)(vd.toVariable) === E(BigInt(0))
+
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
+ }
+
+ test("size(x) < 0 is unsatisfiable") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+ val vd = "x" :: T(listID)(IntegerType)
+ val clause = sizeFd(IntegerType)(vd.toVariable) < E(BigInt(0))
+
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isUNSAT)
+ }
+
+ test("flatMap is associative") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(Not(associative.fullBody)).isUNSAT)
+ }
}
diff --git a/src/it/scala/inox/solvers/unrolling/SimpleUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/SimpleUnrollingSuite.scala
index 24d46a798a0dacda2d523883bb6fb46813b9dd51..dcc1bcaa286dbf294054d3f967c1d52c014c1a66 100644
--- a/src/it/scala/inox/solvers/unrolling/SimpleUnrollingSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/SimpleUnrollingSuite.scala
@@ -69,7 +69,7 @@ class SimpleUnrollingSuite extends SolvingTestSuite {
SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause) match {
case SatWithModel(model) =>
symbols.valuateWithModel(model)(vd) match {
- case CaseClass(ClassType(`nilID`, Seq(tp)), Seq()) =>
+ case CaseClass(ClassType(`nilID`, Seq(`tp`)), Seq()) =>
// success!!
case r =>
fail("Unexpected valuation: " + r)
diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala
index 08bdff350c56aba311e404175b16b6e643584f0e..52a867c9634d8b29625c27ddf217680b2619ae10 100644
--- a/src/main/scala/inox/ast/DSL.scala
+++ b/src/main/scala/inox/ast/DSL.scala
@@ -93,14 +93,11 @@ trait DSL {
}
// if-then-else
- class DanglingElse private[DSL] (condThens: Seq[(Expr, Expr)]) {
- def else_if (cond2: Expr)(thenn2: Expr) = new DanglingElse(condThens :+ (cond2 -> thenn2))
- def else_ (theElse: Expr) = condThens.foldRight(theElse) {
- case ((cond, thenn), elze) =>IfExpr(cond, thenn, elze)
- }
+ class DanglingElse private[DSL] (theCond: Expr, theThen: Expr) {
+ def else_ (theElse: Expr) = IfExpr(theCond, theThen, theElse)
}
- def if_ (cond: Expr)(thenn: Expr) = new DanglingElse(Seq(cond -> thenn))
+ def if_ (cond: Expr)(thenn: Expr) = new DanglingElse(cond, thenn)
def ite(cond: Expr, thenn: Expr, elze: Expr) = IfExpr(cond, thenn, elze)
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index 37152452c8616e2a47c36b0d49c12f14dddb0e5c..81c60e0dc56b32a15562ee4a3bd18db9c3717ecd 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -104,6 +104,8 @@ trait TreeDeconstructor {
(Seq(t1, t2), Seq(), (es, tps) => t.MapApply(es(0), es(1)))
case s.Let(binder, e, body) =>
(Seq(e, body), Seq(binder.tpe), (es, tps) => t.Let(t.ValDef(binder.id, tps.head), es(0), es(1)))
+ case s.Assume(pred, body) =>
+ (Seq(pred, body), Seq(), (es, tps) => t.Assume(es(0), es(1)))
/* Other operators */
case s.FunctionInvocation(id, tps, args) =>
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index c45a91102740ba3cd59a0468e7309da5fb7bfef7..f26a9be3a25824e2e4f5d52aeb88173d35043381 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -189,23 +189,37 @@ trait SymbolOps { self: TypeOps =>
* quantification instantiations.
*/
def simplifyQuantifications(e: Expr): Expr = {
- val fds = functionCallsOf(e).flatMap { fi =>
- val fd = fi.tfd.fd
- transitiveCallees(fd) + fd
+
+ def inlineFunctions(e: Expr): Expr = {
+ val fds = functionCallsOf(e).flatMap { fi =>
+ val fd = fi.tfd.fd
+ transitiveCallees(fd) + fd
+ }
+
+ val fdsToInline = fds
+ .filterNot(fd => transitivelyCalls(fd, fd))
+ .filter(fd => exists { case _: Forall => true case _ => false }(fd.fullBody))
+
+ def inline(e: Expr): Expr = {
+ val subst = functionCallsOf(e)
+ .filter(fi => fdsToInline(fi.tfd.fd))
+ .map(fi => fi -> fi.inlined)
+ replace(subst.toMap, e)
+ }
+
+ fixpoint(inline)(e)
}
- val fdsToInline = fds
- .filterNot(fd => transitivelyCalls(fd, fd))
- .filter(fd => exists { case _: Forall => true case _ => false }(fd.fullBody))
-
- def inline(e: Expr): Expr = {
- val subst = functionCallsOf(e)
- .filter(fi => fdsToInline(fi.tfd.fd))
- .map(fi => fi -> fi.inlined)
- replace(subst.toMap, e)
+ /* Weaker variant of disjunctive normal form */
+ def normalizeClauses(e: Expr): Expr = e match {
+ case Not(Not(e)) => normalizeClauses(e)
+ case Not(Or(es)) => andJoin(es.map(e => normalizeClauses(Not(e))))
+ case Not(Implies(e1, e2)) => and(normalizeClauses(e1), normalizeClauses(Not(e2)))
+ case And(es) => andJoin(es map normalizeClauses)
+ case _ => e
}
- fixpoint(inline)(e)
+ normalizeClauses(inlineFunctions(e))
}
/** Fully expands all let expressions. */
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 27f1edf537fd4e19cd7644db1f51e502096b3da9..b1333121596cc94a15ccee53a63f7849e2cae6c6 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -198,6 +198,7 @@ trait QuantificationTemplates { self: Templates =>
val ignoredSubsts = new IncrementalMap[Quantification, Set[(Int, Set[Encoded], Map[Encoded,Arg])]]
val handledSubsts = new IncrementalMap[Quantification, Set[(Set[Encoded], Map[Encoded,Arg])]]
+ val ignoredGrounds = new IncrementalMap[Int, Set[Quantification]]
val lambdaAxioms = new IncrementalSet[(LambdaStructure, Seq[(Variable, Encoded)])]
val templates = new IncrementalMap[(Seq[ValDef], Expr, Seq[Encoded]), Map[Encoded, Encoded]]
@@ -217,7 +218,9 @@ trait QuantificationTemplates { self: Templates =>
def refutationAssumptions = assumptions
def unrollGeneration: Option[Int] = {
- val gens: Seq[Int] = ignoredMatchers.toSeq.map(_._1) ++ ignoredSubsts.flatMap(p => p._2.map(_._1))
+ val gens: Seq[Int] = ignoredMatchers.toSeq.map(_._1) ++
+ ignoredSubsts.flatMap(p => p._2.map(_._1)) ++
+ ignoredGrounds.map(_._1)
if (gens.isEmpty) None else Some(gens.min)
}
@@ -227,15 +230,23 @@ trait QuantificationTemplates { self: Templates =>
def unroll: Clauses = {
val clauses = new scala.collection.mutable.ListBuffer[Encoded]
- for (e @ (gen, bs, m) <- ignoredMatchers.toSeq if gen == currentGeneration) {
+ for (e @ (gen, bs, m) <- ignoredMatchers.toSeq if gen <= currentGeneration) {
clauses ++= instantiateMatcher(bs, m)
ignoredMatchers -= e
}
- for (q <- quantifications.toSeq) {
- val (release, keep) = ignoredSubsts(q).partition(_._1 == currentGeneration)
- for ((_, bs, subst) <- release) clauses ++= q.instantiateSubst(bs, subst)
+ for (q <- quantifications.toSeq if ignoredSubsts.isDefinedAt(q)) {
+ val (release, keep) = ignoredSubsts(q).partition(_._1 <= currentGeneration)
ignoredSubsts += q -> keep
+
+ for ((_, bs, subst) <- release) {
+ clauses ++= q.instantiateSubst(bs, subst)
+ }
+ }
+
+ for ((gen, qs) <- ignoredGrounds.toSeq if gen <= currentGeneration; q <- qs) {
+ clauses ++= q.ensureGrounds
+ ignoredGrounds += gen -> (ignoredGrounds.getOrElse(gen, Set.empty) - q)
}
clauses.toSeq
@@ -250,7 +261,6 @@ trait QuantificationTemplates { self: Templates =>
if (handledMatchers(blockers -> matcher)) {
Seq.empty
} else {
- //println(blockers -> matcher)
handledMatchers += blockers -> matcher
quantifications.flatMap(_.instantiate(blockers, matcher))
}
@@ -447,7 +457,8 @@ trait QuantificationTemplates { self: Templates =>
val instantiation = new scala.collection.mutable.ListBuffer[Encoded]
for (p @ (bs, subst) <- substs if !handledSubsts.get(this).exists(_ contains p)) {
if (subst.values.exists(_.isRight)) {
- ignoredSubsts += this -> (ignoredSubsts.getOrElse(this, Set.empty) + ((currentGeneration + 3, bs, subst)))
+ val gen = currentGeneration + 3 * subst.values.collect { case Right(m) => totalDepth(m) }.sum
+ ignoredSubsts += this -> (ignoredSubsts.getOrElse(this, Set.empty) + ((gen, bs, subst)))
} else {
instantiation ++= instantiateSubst(bs, subst)
}
@@ -692,7 +703,8 @@ trait QuantificationTemplates { self: Templates =>
clauses ++= axiom.instantiate(bs, m)
}
- clauses ++= axiom.ensureGrounds
+ val groundGen = currentGeneration + 3
+ ignoredGrounds += groundGen -> (ignoredGrounds.getOrElse(groundGen, Set.empty) + axiom)
Map.empty
case Negative(insts) =>
@@ -747,7 +759,7 @@ trait QuantificationTemplates { self: Templates =>
val diff = (currentGeneration - optGen.get) max 0
val currentMatchers = ignoredMatchers.toSeq
- ignoredMatchers.clear
+ ignoredMatchers.clear()
for ((gen, bs, m) <- currentMatchers) {
ignoredMatchers += ((gen - diff, bs, m))
}
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index dbe6ba29b30e75fa5a5b39e579b1299e73fd9311..4918b5c9ad3eb2997ac0cf89b570badb496e0984 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -215,41 +215,49 @@ trait AbstractUnrollingSolver
}
}.distinct
- val default = if (allImages.isEmpty) {
+ def mkLambda(params: Seq[ValDef], body: Expr): Lambda = body.getType match {
+ case FunctionType(from, to) =>
+ val (rest, curr) = params.splitAt(params.size - from.size)
+ mkLambda(rest, Lambda(curr, body))
+ case _ => Lambda(params, body)
+ }
+
+ if (allImages.isEmpty) {
def rec(e: Expr): Expr = e match {
case Lambda(_, body) => rec(body)
case IfExpr(_, _, elze) => rec(elze)
case e => e
}
- rec(f)
+ mkLambda(params.map(_.toVal), rec(f))
} else {
- val optDefault = allImages.collectFirst {
- case (firstArg +: otherArgs, result) if otherArgs.forall { o =>
- evaluator.eval(Equals(firstArg, o)).result == Some(BooleanLiteral(true))
- } => result
+ val projection: Expr = allImages.head._1.head
+
+ val allResults: Seq[(Seq[Expr], Expr)] =
+ (for (subset <- params.toSet.subsets; (args, _) <- allImages) yield {
+ val (concreteArgs, condOpts) = (params zip args).map { case (v, arg) =>
+ if (!subset(v)) {
+ (arg, Some(Equals(v, arg)))
+ } else {
+ (projection, None)
+ }
+ }.unzip
+
+ val app = templates.mkApplication(f, concreteArgs)
+ val result = evaluator.eval(app).result.getOrElse {
+ scala.sys.error("Unexpectedly failed to evaluate " + app.asString)
+ }
+
+ condOpts.flatten -> result
+ }).toSeq
+
+ val withConds :+ ((Seq(), default)) = allResults
+ val body = withConds.foldRight(default) { case ((conds, result), elze) =>
+ IfExpr(andJoin(conds), result, elze)
}
- optDefault.getOrElse {
- val app = templates.mkApplication(f, Seq.fill(from.size)(allImages.head._1.head))
- evaluator.eval(app).result.getOrElse {
- scala.sys.error("Unexpectedly failed to evaluate " + app.asString)
- }
- }
+ mkLambda(params.map(_.toVal), body)
}
-
- val body = allImages.foldRight(default) { case ((args, result), elze) =>
- IfExpr(andJoin((params zip args).map(p => Equals(p._1, p._2))), result, elze)
- }
-
- def mkLambda(params: Seq[ValDef], body: Expr): Lambda = body.getType match {
- case FunctionType(from, to) =>
- val (rest, curr) = params.splitAt(params.size - from.size)
- mkLambda(rest, Lambda(curr, body))
- case _ => Lambda(params, body)
- }
-
- mkLambda(params.map(_.toVal), body)
}
})
}
@@ -305,7 +313,7 @@ trait AbstractUnrollingSolver
val checkConfig = config
.min(Configuration(model = !templates.requiresFiniteRangeCheck, unsatAssumptions = true))
- .max(Configuration(model = false, unsatAssumptions = unrollAssumptions))
+ .max(Configuration(model = false, unsatAssumptions = unrollAssumptions && templates.canUnroll))
val timer = ctx.timers.solvers.check.start()
val res: SolverResponse[underlying.Model, Set[underlying.Trees]] =
diff --git a/src/main/scala/inox/utils/IncrementalSeq.scala b/src/main/scala/inox/utils/IncrementalSeq.scala
index 737cd224af7c67749326288b77fe14828a6fea49..2d8bee0d4cbe68a20d874758c16f4f7e7dc86a8f 100644
--- a/src/main/scala/inox/utils/IncrementalSeq.scala
+++ b/src/main/scala/inox/utils/IncrementalSeq.scala
@@ -17,11 +17,11 @@ class IncrementalSeq[A] extends IncrementalState
def clear() : Unit = {
stack.clear()
+ stack.push(new ArrayBuffer())
}
def reset(): Unit = {
clear()
- stack.push(new ArrayBuffer())
}
def push(): Unit = {