From c8d6c9a1b9149c0703330c3672e656a353bf0da8 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 1 Jul 2015 15:34:10 +0200
Subject: [PATCH] Do not propagate tests if not properly implemented (yet)
---
.../scala/leon/synthesis/rules/ADTDual.scala | 2 +-
.../leon/synthesis/rules/CaseSplit.scala | 2 +-
.../leon/synthesis/rules/Disunification.scala | 2 +-
.../scala/leon/synthesis/rules/IfSplit.scala | 46 ++++++++++---------
.../synthesis/rules/InequalitySplit.scala | 9 ++--
5 files changed, 33 insertions(+), 28 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 45a28dd30..6b33597ca 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -26,7 +26,7 @@ case object ADTDual extends NormalizingRule("ADTDual") {
}.unzip
if (toRemove.nonEmpty) {
- val sub = p.copy(phi = andJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
+ val sub = p.copy(phi = andJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq), tb = TestBank.empty)
Some(decomp(List(sub), forward, "ADTDual"))
} else {
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 8338d95ae..9140eaf23 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -18,7 +18,7 @@ case object CaseSplit extends Rule("Case-Split") {
}
def split(alts: Seq[Expr], description: String)(implicit p: Problem): RuleInstantiation = {
- val subs = alts.map(a => Problem(p.as, p.ws, p.pc, a, p.xs)).toList
+ val subs = alts.map(a => Problem(p.as, p.ws, p.pc, a, p.xs, p.tb)).toList
val onSuccess: List[Solution] => Option[Solution] = {
case sols if sols.size == subs.size =>
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 5bdfe1d1b..402f59bf7 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -25,7 +25,7 @@ object Disunification {
}.unzip
if (toRemove.nonEmpty) {
- val sub = p.copy(phi = orJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
+ val sub = p.copy(phi = orJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq), tb = TestBank.empty)
Some(decomp(List(sub), forward, this.name))
} else {
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index c0d15a22e..2016570b5 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -10,6 +10,30 @@ import purescala.Constructors._
case object IfSplit extends Rule("If-Split") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+
+ def split(i: IfExpr, description: String): RuleInstantiation = {
+ val subs = List(
+ Problem(p.as, p.ws, and(p.pc, i.cond), replace(Map(i -> i.thenn), p.phi), p.xs, p.tbOps.filterIns(i.cond)),
+ Problem(p.as, p.ws, and(p.pc, not(i.cond)), replace(Map(i -> i.elze), p.phi), p.xs, p.tbOps.filterIns(not(i.cond)))
+ )
+
+ val onSuccess: List[Solution] => Option[Solution] = {
+ case sols if sols.size == 2 =>
+ val List(ts, es) = sols
+
+ val pre = or(and(i.cond, ts.pre), and(not(i.cond), es.pre))
+ val defs = ts.defs ++ es.defs
+ val term = IfExpr(i.cond, ts.term, es.term)
+
+ Some(Solution(pre, defs, term, sols.forall(_.isTrusted)))
+
+ case _ =>
+ None
+ }
+
+ decomp(subs, onSuccess, description)
+ }
+
val ifs = collect{
case i: IfExpr => Set(i)
case _ => Set[IfExpr]()
@@ -25,29 +49,7 @@ case object IfSplit extends Rule("If-Split") {
Nil
}
}
- }
-
- def split(i: IfExpr, description: String)(implicit p: Problem): RuleInstantiation = {
- val subs = List(
- Problem(p.as, p.ws, and(p.pc, i.cond), replace(Map(i -> i.thenn), p.phi), p.xs),
- Problem(p.as, p.ws, and(p.pc, not(i.cond)), replace(Map(i -> i.elze), p.phi), p.xs)
- )
-
- val onSuccess: List[Solution] => Option[Solution] = {
- case sols if sols.size == 2 =>
- val List(ts, es) = sols
-
- val pre = or(and(i.cond, ts.pre), and(not(i.cond), es.pre))
- val defs = ts.defs ++ es.defs
- val term = IfExpr(i.cond, ts.term, es.term)
-
- Some(Solution(pre, defs, term, sols.forall(_.isTrusted)))
-
- case _ =>
- None
- }
- decomp(subs, onSuccess, description)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 02475d69d..741b4d02e 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -56,9 +56,12 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
candidates.flatMap {
case List(a1, a2) =>
- val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc))
- val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc))
- val subGT = p.copy(pc = and(GreaterThan(Variable(a1), Variable(a2)), p.pc))
+ val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc),
+ tb = p.tbOps.filterIns(LessThan(Variable(a1), Variable(a2))))
+ val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc),
+ tb = p.tbOps.filterIns(Equals(Variable(a1), Variable(a2))))
+ val subGT = p.copy(pc = and(GreaterThan(Variable(a1), Variable(a2)), p.pc),
+ tb = p.tbOps.filterIns(GreaterThan(Variable(a1), Variable(a2))))
val onSuccess: List[Solution] => Option[Solution] = {
case sols@List(sLT, sEQ, sGT) =>
--
GitLab