From 6572e27714f9c70cab3b3224a2f5cf7bfda9b032 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 26 Mar 2016 16:45:07 +0100
Subject: [PATCH] Termination checker fixes for new DefOps and theory encoders
---
src/main/scala/leon/purescala/DefOps.scala | 8 ++++---
.../solvers/cvc4/CVC4UnrollingSolver.scala | 2 +-
.../solvers/smtlib/SMTLIBCVC4Solver.scala | 5 ++++-
.../leon/solvers/smtlib/SMTLIBSolver.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBZ3Solver.scala | 3 ++-
.../leon/solvers/theories/BagEncoder.scala | 2 +-
.../leon/solvers/theories/StringEncoder.scala | 2 +-
.../leon/solvers/theories/TheoryEncoder.scala | 2 +-
.../solvers/unrolling/UnrollingSolver.scala | 9 ++++----
.../scala/leon/solvers/z3/FairZ3Solver.scala | 2 +-
.../leon/solvers/z3/Z3UnrollingSolver.scala | 2 +-
.../leon/termination/ChainProcessor.scala | 6 ++---
.../scala/leon/termination/Processor.scala | 22 +++++++------------
13 files changed, 34 insertions(+), 33 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 7f0e5b018..753b0944c 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 79498f97b..3ddfca8d9 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 4c17f8089..5de74510b 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 99e107027..9f6f92b93 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 e12b53fb5..6a58f9f1a 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 fb6674224..4ba7fcaa4 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 f8b55303b..8f33513a6 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 9cb18effd..39b5a632c 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 76f18864b..852e125ed 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 7c79597f2..f8237a488 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 ec1428e39..99c75199a 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 c01fa9fb3..ef6fde2e2 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 1d0527127..6f998b0ed 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
}
}
--
GitLab