From 0d5cf1e5771296c3ac31cfc81670a9219a94401e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 25 Apr 2016 13:50:11 +0200
Subject: [PATCH] Refactor simplifiers to take initial PC, make it a proper
Path
---
src/main/scala/leon/purescala/ExprOps.scala | 16 ++++++++--------
.../leon/purescala/SimplifierWithPaths.scala | 2 +-
.../scala/leon/purescala/TransformerWithPC.scala | 6 ++----
src/main/scala/leon/synthesis/Solution.scala | 3 ++-
.../leon/synthesis/rules/EquivalentInputs.scala | 2 +-
src/main/scala/leon/utils/Simplifiers.scala | 5 +++--
6 files changed, 17 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 228158152..c24201f71 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1003,8 +1003,8 @@ object ExprOps extends GenTreeOps[Expr] {
postMap(transform, applyRec = true)(expr)
}
- def simplifyPaths(sf: SolverFactory[Solver], initC: List[Expr] = Nil): Expr => Expr = {
- new SimplifierWithPaths(sf, initC).transform
+ def simplifyPaths(sf: SolverFactory[Solver], initPC: Path = Path.empty): Expr => Expr = {
+ new SimplifierWithPaths(sf, initPC).transform
}
trait Traverser[T] {
@@ -1020,7 +1020,7 @@ object ExprOps extends GenTreeOps[Expr] {
}
trait CollectorWithPaths[T] extends TransformerWithPC with Traverser[Seq[T]] {
- protected val initPath: Seq[Expr] = Nil
+ protected val initPath: Path = Path.empty
private var results: Seq[T] = Nil
@@ -1040,11 +1040,11 @@ object ExprOps extends GenTreeOps[Expr] {
def traverse(e: Expr): Seq[T] = traverse(e, initPath)
- def traverse(e: Expr, init: Expr): Seq[T] = traverse(e, Seq(init))
+ def traverse(e: Expr, init: Expr): Seq[T] = traverse(e, Path(init))
- def traverse(e: Expr, init: Seq[Expr]): Seq[T] = {
+ def traverse(e: Expr, init: Path): Seq[T] = {
results = Nil
- rec(e, Path(init))
+ rec(e, init)
results
}
}
@@ -1765,7 +1765,7 @@ object ExprOps extends GenTreeOps[Expr] {
val newFd = fdOuter.duplicate()
- val simp = Simplifiers.bestEffort(ctx, p) _
+ val simp = Simplifiers.bestEffort(ctx, p)((_: Expr))
newFd.body = fdInner.body.map(b => simplePreTransform(pre)(b))
newFd.precondition = mergePre(fdOuter.precondition, fdInner.precondition).map(simp)
@@ -2127,7 +2127,7 @@ object ExprOps extends GenTreeOps[Expr] {
}
- def simpleCorrectnessCond(e: Expr, path: List[Expr], sf: SolverFactory[Solver]): Expr = {
+ def simpleCorrectnessCond(e: Expr, path: Path, sf: SolverFactory[Solver]): Expr = {
simplifyPaths(sf, path)(
andJoin( collectCorrectnessConditions(e) map { _._2 } )
)
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index b6cf9e657..ad56da7f4 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -10,7 +10,7 @@ import Extractors._
import Constructors._
import solvers._
-class SimplifierWithPaths(sf: SolverFactory[Solver], override val initPath: List[Expr] = Nil) extends TransformerWithPC {
+class SimplifierWithPaths(sf: SolverFactory[Solver], val initPath: Path = Path.empty) extends TransformerWithPC {
val solver = SimpleSolverAPI(sf)
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index 53e675684..95b2c89d4 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -3,12 +3,10 @@
package leon
package purescala
-import Common._
import Expressions._
import Constructors._
import Extractors._
import ExprOps._
-import Types._
/** Traverses/ transforms expressions with path condition awareness.
*
@@ -19,7 +17,7 @@ import Types._
abstract class TransformerWithPC extends Transformer {
/** The initial path condition */
- protected val initPath: Seq[Expr]
+ protected val initPath: Path
protected def rec(e: Expr, path: Path): Expr = e match {
case Let(i, v, b) =>
@@ -108,7 +106,7 @@ abstract class TransformerWithPC extends Transformer {
}
def transform(e: Expr): Expr = {
- rec(e, Path(initPath))
+ rec(e, initPath)
}
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index bb0b047fd..ec009623d 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -9,6 +9,7 @@ import purescala.Types.{TypeTree,TupleType}
import purescala.Definitions._
import purescala.ExprOps._
import purescala.Constructors._
+import purescala.Path
import leon.utils.Simplifiers
@@ -55,7 +56,7 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
def toSimplifiedExpr(ctx: LeonContext, p: Program, within: FunDef): Expr = {
- withoutSpec(Simplifiers.bestEffort(ctx, p)(req(within.precOrTrue, toExpr))).get
+ Simplifiers.bestEffort(ctx, p)(toExpr, Path(within.precOrTrue))
}
}
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 90c4ecbb3..65e5dd1ac 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -16,7 +16,7 @@ import purescala.Types.CaseClassType
case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val simplifier = Simplifiers.bestEffort(hctx, hctx.program) _
+ val simplifier = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, p.pc)
var subst = Map.empty[Identifier, Expr]
var reverseSubst = Map.empty[Identifier, Expr]
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 6fdcbc9da..d1fe99282 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -7,16 +7,17 @@ import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.ScopeSimplifier
+import purescala.Path
import solvers._
object Simplifiers {
- def bestEffort(ctx: LeonContext, p: Program)(e: Expr): Expr = {
+ def bestEffort(ctx: LeonContext, p: Program)(e: Expr, pc: Path = Path.empty): Expr = {
val solverf = SolverFactory.uninterpreted(ctx, p)
try {
val simplifiers = (simplifyLets _).
- andThen(simplifyPaths(solverf)).
+ andThen(simplifyPaths(solverf, pc)).
andThen(simplifyArithmetic).
andThen(evalGround(ctx, p)).
andThen(normalizeExpression)
--
GitLab