From 617aa98193eb2188aa76fb27aa12a4ddb8eac0d7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 30 Mar 2015 14:31:28 +0200
Subject: [PATCH] Various fixes
---
src/main/scala/leon/purescala/DefOps.scala | 2 +-
.../scala/leon/purescala/Definitions.scala | 9 +++++++
.../leon/solvers/smtlib/SMTLIBTarget.scala | 2 --
.../smtlib/SMTLIBUnrollingCVC4Target.scala | 26 ++++++++++---------
4 files changed, 24 insertions(+), 15 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 8edf77f51..6daf732ef 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -394,7 +394,7 @@ object DefOps {
import leon.utils.SearchSpace.reachable
reachable(
sources,
- (tfd: TypedFunDef) => functionCallsOf(tfd.fd.fullBody) map { _.tfd },
+ (tfd: TypedFunDef) => functionCallsOf(tfd.fullBody) map { _.tfd },
limit
)
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index ee0f6a03c..fe162c455 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -498,6 +498,15 @@ object Definitions {
private var trCache = Map[Expr, Expr]()
private var postCache = Map[Expr, Expr]()
+ def fullBody = {
+ val fb = fd.fullBody
+ trCache.getOrElse(fb, {
+ val res = translated(fb)
+ trCache += fb -> res
+ res
+ })
+ }
+
def body = fd.body.map { b =>
trCache.getOrElse(b, {
val res = translated(b)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 47cebfd05..43e1dd91c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -52,7 +52,6 @@ trait SMTLIBTarget {
val selectors = new IncrementalBijection[(TypeTree, Int), SSymbol]()
val testers = new IncrementalBijection[TypeTree, SSymbol]()
val variables = new IncrementalBijection[Identifier, SSymbol]()
- val classes = new IncrementalBijection[CaseClassDef, SSymbol]()
val sorts = new IncrementalBijection[TypeTree, Sort]()
val functions = new IncrementalBijection[TypedFunDef, SSymbol]()
@@ -646,7 +645,6 @@ trait SMTLIBTarget {
out.write("\n")
out.flush()
}
-
interpreter.eval(cmd) match {
case err@ErrorResponse(msg) if !interrupted =>
reporter.fatalError("Unexpected error from smt-"+targetName+" solver: "+msg)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
index 9fd5eeba2..0600de6cb 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
@@ -26,7 +26,7 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
)
}
- val (smtFunDecls, smtBodies) = funs.toSeq.collect {
+ val smtFunDecls = funs.toSeq.collect {
case tfd if !functions.containsA(tfd) && tfd.params.nonEmpty =>
val id = if (tfd.tps.isEmpty) {
tfd.id
@@ -35,17 +35,19 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
}
val sym = id2sym(id)
functions +=(tfd, sym)
- (
- FunDec(
- sym,
- tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
- declareSort(tfd.returnType)
- ),
- toSMT(matchToIfThenElse(tfd.body.get))(tfd.params.map { p =>
- (p.id, id2sym(p.id): Term)
- }.toMap)
- )
- }.unzip
+ FunDec(
+ sym,
+ tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
+ declareSort(tfd.returnType)
+ )
+ }
+ val smtBodies = smtFunDecls map { case FunDec(sym, _, _) =>
+ val tfd = functions.toA(sym)
+ toSMT(matchToIfThenElse(tfd.body.get))(tfd.params.map { p =>
+ (p.id, id2sym(p.id): Term)
+ }.toMap
+ )
+ }
if (smtFunDecls.nonEmpty) sendCommand(DefineFunsRec(smtFunDecls, smtBodies))
functions.toB(tfd)
--
GitLab