Skip to content
Snippets Groups Projects
Commit 603f0fbb authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Fix IfSplit

parent d5eb3cc7
No related branches found
No related tags found
No related merge requests found
...@@ -15,18 +15,22 @@ case object IfSplit extends Rule("If-Split") { ...@@ -15,18 +15,22 @@ case object IfSplit extends Rule("If-Split") {
case _ => Set[IfExpr]() case _ => Set[IfExpr]()
}(p.phi) }(p.phi)
ifs.toList match { val xsSet = p.xs.toSet
case i :: _ =>
List(split(i, p, "Split top-level If")) ifs.flatMap {
case _ => case i @ IfExpr(cond, _, _) =>
Nil if ((variablesOf(cond) & xsSet).isEmpty) {
List(split(i, p, "Split If("+cond+")"))
} else {
Nil
}
} }
} }
def split(i: IfExpr, p: Problem, description: String): RuleInstantiation = { def split(i: IfExpr, p: Problem, description: String): RuleInstantiation = {
val subs = List( 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, 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.pc), 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] = { val onSuccess: List[Solution] => Option[Solution] = {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment