From 603f0fbb3d9f1b80af559b74c63a7358a6360def Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 18 Aug 2014 16:40:52 +0200
Subject: [PATCH] Fix IfSplit
---
.../scala/leon/synthesis/rules/IfSplit.scala | 18 +++++++++++-------
1 file changed, 11 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index 45d502ecb..c29ae5ccf 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -15,18 +15,22 @@ case object IfSplit extends Rule("If-Split") {
case _ => Set[IfExpr]()
}(p.phi)
- ifs.toList match {
- case i :: _ =>
- List(split(i, p, "Split top-level If"))
- case _ =>
- Nil
+ val xsSet = p.xs.toSet
+
+ ifs.flatMap {
+ case i @ IfExpr(cond, _, _) =>
+ if ((variablesOf(cond) & xsSet).isEmpty) {
+ List(split(i, p, "Split If("+cond+")"))
+ } else {
+ Nil
+ }
}
}
def split(i: IfExpr, p: Problem, description: String): RuleInstantiation = {
val subs = List(
- Problem(p.as, And(p.pc, i.cond), replace(Map(i -> i.thenn), p.pc), p.xs),
- Problem(p.as, And(p.pc, Not(i.cond)), replace(Map(i -> i.elze), p.pc), p.xs)
+ Problem(p.as, And(p.pc, i.cond), replace(Map(i -> i.thenn), p.phi), p.xs),
+ Problem(p.as, And(p.pc, Not(i.cond)), replace(Map(i -> i.elze), p.phi), p.xs)
)
val onSuccess: List[Solution] => Option[Solution] = {
--
GitLab