From 0bcb1fe895b014c1c544c9ee2016c811f7efa93f Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 25 Mar 2016 00:24:07 +0100
Subject: [PATCH] Replace defs for special cases
---
src/main/scala/leon/purescala/DefOps.scala | 46 +++++++++++--------
.../leon/solvers/smtlib/SMTLIBSolver.scala | 10 ++--
.../solvers/unrolling/DatatypeManager.scala | 5 ++
.../solvers/unrolling/UnrollingSolver.scala | 10 ++--
.../scala/leon/xlang/AntiAliasingPhase.scala | 4 +-
5 files changed, 42 insertions(+), 33 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 7afb63104..7f0e5b018 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -286,11 +286,22 @@ object DefOps {
}
}
- private def defaultFiMap(fi: FunctionInvocation, nfd: FunDef): Option[Expr] = (fi, nfd) match {
- case (FunctionInvocation(old, args), newfd) if old.fd != newfd =>
- Some(FunctionInvocation(newfd.typed(old.tps), args))
- case _ =>
- None
+ def replaceDefsInProgram(p: Program)(fdMap: Map[FunDef, FunDef] = Map.empty,
+ cdMap: Map[ClassDef, ClassDef] = Map.empty): Program = {
+ p.copy(units = for (u <- p.units) yield {
+ u.copy(defs = u.defs.map {
+ case m : ModuleDef =>
+ m.copy(defs = for (df <- m.defs) yield {
+ df match {
+ case cd : ClassDef => cdMap.getOrElse(cd, cd)
+ case fd : FunDef => fdMap.getOrElse(fd, fd)
+ case d => d
+ }
+ })
+ case cd: ClassDef => cdMap.getOrElse(cd, cd)
+ case d => d
+ })
+ })
}
def replaceDefs(p: Program)(fdMapF: FunDef => Option[FunDef],
@@ -365,22 +376,17 @@ object DefOps {
nfd.fullBody = transformer.transform(fd.fullBody)(bindings)
}
- val newP = p.copy(units = for (u <- p.units) yield {
- u.copy(defs = u.defs.map {
- case m : ModuleDef =>
- m.copy(defs = for (df <- m.defs) yield {
- df match {
- case cd : ClassDef => transformer.transform(cd)
- case fd : FunDef => transformer.transform(fd)
- case d => d
- }
- })
- case cd: ClassDef => transformer.transform(cd)
- case d => d
- })
- })
+ val fdsMap = fdMap.toMap
+ val cdsMap = cdMap.toMap
+ val newP = replaceDefsInProgram(p)(fdsMap, cdsMap)
+ (newP, idMap.toMap, fdsMap, cdsMap)
+ }
- (newP, idMap.toMap, fdMap.toMap, cdMap.toMap)
+ private def defaultFiMap(fi: FunctionInvocation, nfd: FunDef): Option[Expr] = (fi, nfd) match {
+ case (FunctionInvocation(old, args), newfd) if old.fd != newfd =>
+ Some(FunctionInvocation(newfd.typed(old.tps), args))
+ case _ =>
+ None
}
/** Clones the given program by replacing some functions by other functions.
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 95f924a46..99e107027 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -91,9 +91,13 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program, theo
for (me <- smodel) me match {
case DefineFun(SMTFunDef(s, args, kind, e)) if syms(s) =>
- val id = variables.toA(s)
- val value = fromSMT(e, id.getType)(Map(), modelFunDefs)
- model += ids.getAorElse(id, id) -> theories.decode(value)(variablesOf(value).map(id => id -> ids.toA(id)).toMap)
+ try {
+ val id = variables.toA(s)
+ val value = fromSMT(e, id.getType)(Map(), modelFunDefs)
+ model += ids.getAorElse(id, id) -> theories.decode(value)(variablesOf(value).map(id => id -> ids.toA(id)).toMap)
+ } catch {
+ case _: Unsupported =>
+ }
case _ =>
}
diff --git a/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala b/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala
index 275621828..554689830 100644
--- a/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/DatatypeManager.scala
@@ -157,6 +157,8 @@ class DatatypeManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(en
case BooleanType | UnitType | CharType | IntegerType |
RealType | Int32Type | StringType | (_: TypeParameter) => false
+ case at: ArrayType => true
+
case NAryType(tpes, _) => tpes.exists(requireTypeUnrolling)
}
@@ -205,6 +207,9 @@ class DatatypeManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(en
case FunctionType(_, _) =>
FreshFunction(expr)
+ case at: ArrayType =>
+ GreaterEquals(ArrayLength(expr), IntLiteral(0))
+
case _ => scala.sys.error("TODO")
}
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 601aa84eb..76f18864b 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -388,13 +388,9 @@ trait AbstractUnrollingSolver[T]
if (this.feelingLucky) {
// we might have been lucky :D
- try {
- val extracted = extractModel(model)
- val valid = validateModel(extracted, assumptionsSeq, silenceErrors = true)
- if (valid) foundAnswer(Some(true), extracted)
- } catch {
- case u: Unsupported =>
- }
+ val extracted = extractModel(model)
+ val valid = validateModel(extracted, assumptionsSeq, silenceErrors = true)
+ if (valid) foundAnswer(Some(true), extracted)
}
if (!foundDefinitiveAnswer) {
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index f1ea90043..0cfc68d50 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -55,9 +55,7 @@ object AntiAliasingPhase extends TransformationPhase {
updateBody(fd, effects, updatedFunctions, varsInScope)(ctx)
}
- val res = replaceFunDefs(pgm)(fd => updatedFunctions.get(fd), (fi, fd) => None)
- //println(res._1)
- res._1
+ replaceDefsInProgram(pgm)(updatedFunctions)
}
/*
--
GitLab