From b971b2e11ff2ef5df8297e8df4605cb6bffa686f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 19 May 2016 18:25:10 +0200
Subject: [PATCH] Introduce MutableTree
---
src/main/scala/leon/codegen/CodeGeneration.scala | 3 +++
.../scala/leon/evaluators/RecursiveEvaluator.scala | 3 +++
.../scala/leon/evaluators/StreamEvaluator.scala | 3 +++
src/main/scala/leon/purescala/Expressions.scala | 13 +++++++++++++
src/main/scala/leon/purescala/Types.scala | 2 +-
.../scala/leon/solvers/smtlib/SMTLIBTarget.scala | 3 +++
.../scala/leon/solvers/z3/AbstractZ3Solver.scala | 3 +++
7 files changed, 29 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 40f745a33..47f6f3441 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1195,6 +1195,9 @@ trait CodeGeneration {
mkBranch(b, al, fl, ch, canDelegateToMkExpr = false)
ch << Label(fl) << POP << Ldc(0) << Label(al)
+ case MutableExpr(e) =>
+ mkExpr(e, ch)
+
case _ => throw CompilationException("Unsupported expr " + e + " : " + e.getClass)
}
}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index f5536ee98..5fba0109e 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -831,6 +831,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases:\n"+cases)
}
+ case MutableExpr(ex) =>
+ e(ex)
+
case gl: GenericValue => gl
case fl : FractionalLiteral => normalizeFraction(fl)
case l : Literal[_] => l
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index 7058c9ba1..c49e3941b 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -287,6 +287,9 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
Stream()
}
+ case MutableExpr(ex) =>
+ e(ex)
+
case MatchExpr(scrut, cases) =>
def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Stream[(MatchCase, Map[Identifier, Expr])] = {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 64b0479b3..5da34c789 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -998,6 +998,19 @@ object Expressions {
val getType = ArrayType(tpe).unveilUntyped
}
+ case class MutableExpr(var underlying: Expr) extends Expr with Extractable with PrettyPrintable {
+ def getType = underlying.getType
+
+ def extract: Option[(Seq[Expr], (Seq[Expr]) => Expr)] = Some(
+ Seq(underlying),
+ { case Seq(e) => underlying = e; this }
+ )
+
+ override def printWith(implicit pctx: PrinterContext): Unit = {
+ import PrinterHelpers._
+ p"$underlying"
+ }
+ }
/* Special trees for synthesis */
/** $encodingof `choose(pred)`, the non-deterministic choice in Leon.
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 2ae80beac..a48da5298 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -11,7 +11,7 @@ import TypeOps._
object Types {
trait Typed extends Printable {
- val getType: TypeTree
+ def getType: TypeTree
def isTyped : Boolean = getType != Untyped
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 87d798528..77ed0a9c8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -529,6 +529,9 @@ trait SMTLIBTarget extends Interruptible {
val constructor = constructors.toB(tpe)
FunctionApplication(constructor, Seq(toSMT(InfiniteIntegerLiteral(n))))
+ case MutableExpr(ex) =>
+ toSMT(ex)
+
/**
* ===== Everything else =====
*/
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 95460440e..0eff41ea6 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -520,6 +520,9 @@ trait AbstractZ3Solver extends Z3Solver {
val constructor = constructors.toB(tp)
constructor(rec(InfiniteIntegerLiteral(id)))
+ case MutableExpr(ex) =>
+ rec(ex)
+
case other =>
unsupported(other)
}
--
GitLab