From e9f6c3ac2f20005f65fa061b002f68450029d341 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Oct 2012 19:31:31 +0200
Subject: [PATCH] slightly better
---
src/main/scala/leon/synthesis/Rules.scala | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 83ed51723..408b2395e 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -1,6 +1,7 @@
package leon
package synthesis
+import purescala.Common._
import purescala.Trees._
object Rules {
@@ -12,6 +13,9 @@ object Rules {
abstract class Rule(val name: String) {
def isApplicable(p: Problem, parent: Task): List[Task]
+
+
+ def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
}
object OnePoint extends Rule("One-point") {
@@ -32,14 +36,14 @@ object OnePoint extends Rule("One-point") {
val others = exprs.filter(_ != eq)
val oxs = p.xs.filter(_ != x)
- val newProblem = Problem(p.as, replace(Map(Variable(x) -> e), And(others)), oxs)
+ val newProblem = Problem(p.as, subst(x -> e, And(others)), oxs)
val onSuccess: List[Solution] => Solution = {
case List(Solution(pre, term)) =>
if (oxs.isEmpty) {
Solution(pre, e)
} else {
- Solution(pre, LetTuple(oxs, term, replace(Map(Variable(x) -> e), Tuple(p.xs.map(Variable(_))))) )
+ Solution(pre, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))) )
}
case _ => Solution.none
}
--
GitLab