diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 7f0e5b0180bd9318cb3b8cd109ae1b01d843b9c1..753b0944c62023257398b09305ed85020eae64b2 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -357,7 +357,7 @@ object DefOps {
})
for (cd <- p.definedClasses if requiresReplacement(cd)) trCd(cd)
- for (fd <- p.definedFunctions if requiresReplacement(fd)) {
+ for (fd <- p.definedFunctions if requiresReplacement(fd) && !(fdMap contains fd)) {
val newId = transformer.transform(fd.id)
val newReturn = transformer.transform(fd.returnType)
val newParams = fd.params map (vd => ValDef(transformer.transform(vd.id)))
@@ -372,8 +372,10 @@ object DefOps {
}
for ((fd,nfd) <- fdMap) {
- val bindings = (fd.params zip nfd.params).map(p => p._1.id -> p._2.id).toMap
- nfd.fullBody = transformer.transform(fd.fullBody)(bindings)
+ val bindings = (fd.params zip nfd.params).map(p => p._1.id -> p._2.id).toMap ++
+ nfd.params.map(vd => vd.id -> vd.id)
+
+ nfd.fullBody = transformer.transform(nfd.fullBody)(bindings)
}
val fdsMap = fdMap.toMap
diff --git a/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala b/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
index 79498f97b0bd3735969ae9f2bd4de58279ec4a01..3ddfca8d9524f9052dc5e6e49266006e9ffa2e3b 100644
--- a/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
@@ -10,4 +10,4 @@ import unrolling._
import theories._
class CVC4UnrollingSolver(context: LeonContext, program: Program, underlying: Solver)
- extends UnrollingSolver(context, program, underlying, theories = NoEncoder)
+ extends UnrollingSolver(context, program, underlying, theories = new NoEncoder)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 4c17f80892dfad288c0522e3c918a31eb4cef9ae..5de74510b465d76cfc152c476cff96321c4758e9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -5,9 +5,12 @@ package solvers.smtlib
import OptionParsers._
+import solvers.theories._
import purescala.Definitions.Program
-class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) with SMTLIBCVC4Target {
+class SMTLIBCVC4Solver(context: LeonContext, program: Program)
+ extends SMTLIBSolver(context, program, new NoEncoder)
+ with SMTLIBCVC4Target {
def targetName = "cvc4"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 99e1070273b762b824fd0b1543f1ecb035b53c3f..9f6f92b93c0cafc7cf73210879d32b3c9defff2b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -16,7 +16,7 @@ import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
import theories._
import utils._
-abstract class SMTLIBSolver(val context: LeonContext, val program: Program, theories: TheoryEncoder = NoEncoder)
+abstract class SMTLIBSolver(val context: LeonContext, val program: Program, theories: TheoryEncoder)
extends Solver with SMTLIBTarget with NaiveAssumptionSolver {
/* Solver name */
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index e12b53fb59d21b60b56f3a1cbcbb4d1b01a31ca7..6a58f9f1a294180182595bcb34d35d1a2ffe08a7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -16,7 +16,8 @@ import _root_.smtlib.theories.Core.{Equals => _, _}
import theories._
class SMTLIBZ3Solver(context: LeonContext, program: Program)
- extends SMTLIBSolver(context, program, StringEncoder) with SMTLIBZ3Target {
+ extends SMTLIBSolver(context, program, new StringEncoder)
+ with SMTLIBZ3Target {
def getProgram: Program = program
}
diff --git a/src/main/scala/leon/solvers/theories/BagEncoder.scala b/src/main/scala/leon/solvers/theories/BagEncoder.scala
index fb66742247aa5a1a2d0534edc59b58bcf724105e..4ba7fcaa42307ae9c1b65bd3b81c4da03ab62b22 100644
--- a/src/main/scala/leon/solvers/theories/BagEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/BagEncoder.scala
@@ -8,7 +8,7 @@ import purescala.Common._
import purescala.Expressions._
import purescala.Types._
-object BagEncoder extends TheoryEncoder {
+class BagEncoder(val context: LeonContext) extends TheoryEncoder {
val encoder = new Encoder
val decoder = new Decoder
}
diff --git a/src/main/scala/leon/solvers/theories/StringEncoder.scala b/src/main/scala/leon/solvers/theories/StringEncoder.scala
index f8b55303b4257e50dfb42e05d634381d2dd40e84..8f33513a64898c17a7a4b2dfda13a037b2d93f5d 100644
--- a/src/main/scala/leon/solvers/theories/StringEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/StringEncoder.scala
@@ -116,7 +116,7 @@ object StringEcoSystem {
val funDefs = Seq(StringSize, StringListConcat, StringTake, StringDrop, StringSlice)
}
-object StringEncoder extends TheoryEncoder {
+class StringEncoder extends TheoryEncoder {
import StringEcoSystem._
private val stringBijection = new Bijection[String, Expr]()
diff --git a/src/main/scala/leon/solvers/theories/TheoryEncoder.scala b/src/main/scala/leon/solvers/theories/TheoryEncoder.scala
index 9cb18effd731d15033397d5fbcb2b58dce2ac83a..39b5a632c5321220416e8142f30eb90c65b887a5 100644
--- a/src/main/scala/leon/solvers/theories/TheoryEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/TheoryEncoder.scala
@@ -75,7 +75,7 @@ trait TheoryEncoder { self =>
}
}
-object NoEncoder extends TheoryEncoder {
+class NoEncoder extends TheoryEncoder {
val encoder = new Encoder
val decoder = new Decoder
}
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 76f18864b453df290c372af35658707525058224..852e125ed88db4327b18cfabc329d31e1366a2f6 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -394,10 +394,11 @@ trait AbstractUnrollingSolver[T]
}
if (!foundDefinitiveAnswer) {
- unrollingBank.decreaseAllGenerations()
+ val promote = templateGenerator.manager.getBlockersToPromote(model.eval)
+ if (promote.nonEmpty) {
+ unrollingBank.decreaseAllGenerations()
- for (b <- templateGenerator.manager.getBlockersToPromote(model.eval)) {
- unrollingBank.promoteBlocker(b, force = true)
+ for (b <- promote) unrollingBank.promoteBlocker(b, force = true)
}
}
}
@@ -449,7 +450,7 @@ class UnrollingSolver(
val context: LeonContext,
val program: Program,
underlying: Solver,
- theories: TheoryEncoder = NoEncoder
+ theories: TheoryEncoder = new NoEncoder
) extends AbstractUnrollingSolver[Expr] {
override val name = "U:"+underlying.name
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 7c79597f21ba61532cc3f826c00efd6019393e0f..f8237a4885fdc459efe261bb4333afc36944b500 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -103,7 +103,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
def asString(implicit ctx: LeonContext) = z3.toString
}
- val theoryEncoder = StringEncoder
+ val theoryEncoder = new StringEncoder
val templateEncoder = new TemplateEncoder[Z3AST] {
def encodeId(id: Identifier): Z3AST = {
diff --git a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
index ec1428e3993c87e20abd77bd24844df242ae96d4..99c75199a7d96b64ce42ba9039dd648032e60888 100644
--- a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
@@ -10,4 +10,4 @@ import unrolling._
import theories._
class Z3UnrollingSolver(context: LeonContext, program: Program, underlying: Solver)
- extends UnrollingSolver(context, program, underlying, theories = StringEncoder)
+ extends UnrollingSolver(context, program, underlying, theories = new StringEncoder)
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index c01fa9fb3afe65e5b798b31db3ebc5cf23e9e626..ef6fde2e21638a9f26117f5ef855f7d9d85ec57f 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -58,11 +58,11 @@ class ChainProcessor(
if (structuralDecreasing || numericDecreasing)
Some(problem.funDefs map Cleared)
else {
- val chainsUnlooping = chains.flatMap(c1 => chains.flatMap(c2 => c1 compose c2)).forall {
- chain => !definitiveSATwithModel(andJoin(chain.loop())).isDefined
+ val maybeReentrant = chains.flatMap(c1 => chains.flatMap(c2 => c1 compose c2)).exists {
+ chain => maybeSAT(andJoin(chain.loop()))
}
- if (chainsUnlooping)
+ if (!maybeReentrant)
Some(problem.funDefs map Cleared)
else
None
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 1d0527127344510b803a21666f0ade2d92537dff..6f998b0edcfb80ed41110596c3c754e411a71cc6 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -34,7 +34,7 @@ trait Solvable extends Processor {
val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size"),Seq(sizeModule))
val newProgram : Program = program.copy( units = sizeUnit :: program.units)
- SolverFactory.getFromSettings(context, newProgram).withTimeout(10.seconds)
+ SolverFactory.getFromSettings(context, newProgram).withTimeout(1.seconds)
}
type Solution = (Option[Boolean], Map[Identifier, Expr])
@@ -52,23 +52,17 @@ trait Solvable extends Processor {
res
}
- def maybeSAT(problem: Expr): Boolean = {
- withoutPosts {
- SimpleSolverAPI(solver).solveSAT(problem)._1 getOrElse true
- }
+ def maybeSAT(problem: Expr): Boolean = withoutPosts {
+ SimpleSolverAPI(solver).solveSAT(problem)._1 getOrElse true
}
- def definitiveALL(problem: Expr): Boolean = {
- withoutPosts {
- SimpleSolverAPI(solver).solveSAT(Not(problem))._1.exists(!_)
- }
+ def definitiveALL(problem: Expr): Boolean = withoutPosts {
+ SimpleSolverAPI(solver).solveSAT(Not(problem))._1.exists(!_)
}
- def definitiveSATwithModel(problem: Expr): Option[Model] = {
- withoutPosts {
- val (sat, model) = SimpleSolverAPI(solver).solveSAT(problem)
- if (sat.isDefined && sat.get) Some(model) else None
- }
+ def definitiveSATwithModel(problem: Expr): Option[Model] = withoutPosts {
+ val (sat, model) = SimpleSolverAPI(solver).solveSAT(problem)
+ if (sat.isDefined && sat.get) Some(model) else None
}
}