From bd2a88b389e37f98a1fdc2e08ac9cc97d3c0f8f9 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 25 May 2016 15:12:49 +0200
Subject: [PATCH] Move MutableExpr to synthesis
---
.../scala/leon/codegen/CodeGeneration.scala | 2 +-
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../leon/evaluators/StreamEvaluator.scala | 2 +-
.../scala/leon/purescala/Expressions.scala | 14 -------------
.../leon/solvers/smtlib/SMTLIBTarget.scala | 2 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 1 +
.../leon/synthesis/utils/MutableExpr.scala | 21 +++++++++++++++++++
8 files changed, 27 insertions(+), 19 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/utils/MutableExpr.scala
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 47f6f3441..b37067de4 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1195,7 +1195,7 @@ trait CodeGeneration {
mkBranch(b, al, fl, ch, canDelegateToMkExpr = false)
ch << Label(fl) << POP << Ldc(0) << Label(al)
- case MutableExpr(e) =>
+ case synthesis.utils.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 5fba0109e..933781bfb 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -831,7 +831,7 @@ 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) =>
+ case synthesis.utils.MutableExpr(ex) =>
e(ex)
case gl: GenericValue => gl
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index c49e3941b..8caf0c9f4 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -287,7 +287,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
Stream()
}
- case MutableExpr(ex) =>
+ case synthesis.utils.MutableExpr(ex) =>
e(ex)
case MatchExpr(scrut, cases) =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 7567132ea..65fbfb0dc 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -998,20 +998,6 @@ 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/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 77ed0a9c8..b37ffacf8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -529,7 +529,7 @@ trait SMTLIBTarget extends Interruptible {
val constructor = constructors.toB(tpe)
FunctionApplication(constructor, Seq(toSMT(InfiniteIntegerLiteral(n))))
- case MutableExpr(ex) =>
+ case synthesis.utils.MutableExpr(ex) =>
toSMT(ex)
/**
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 99567a865..0fef7e87a 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -552,7 +552,7 @@ trait AbstractZ3Solver extends Z3Solver {
val constructor = constructors.toB(tp)
constructor(rec(InfiniteIntegerLiteral(id)))
- case MutableExpr(ex) =>
+ case synthesis.utils.MutableExpr(ex) =>
rec(ex)
case other =>
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index f7ab39d9d..a737d78a6 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -13,6 +13,7 @@ import purescala.TypeOps.depth
import purescala.DefOps._
import purescala.Constructors._
+import utils.MutableExpr
import solvers._
import leon.grammars._
import leon.grammars.aspects._
diff --git a/src/main/scala/leon/synthesis/utils/MutableExpr.scala b/src/main/scala/leon/synthesis/utils/MutableExpr.scala
new file mode 100644
index 000000000..f30fd8104
--- /dev/null
+++ b/src/main/scala/leon/synthesis/utils/MutableExpr.scala
@@ -0,0 +1,21 @@
+package leon
+package synthesis.utils
+
+import purescala.Expressions.Expr
+import purescala.Extractors.Extractable
+import purescala.{PrinterHelpers, PrinterContext, PrettyPrintable}
+
+/** A mutable expression box useful for CEGIS */
+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"
+ }
+}
\ No newline at end of file
--
GitLab