From 79178cb063058f1a4f4829fabe3351ac3fc6dff2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 22 Oct 2012 18:36:39 +0200
Subject: [PATCH] Implement case-split
---
src/main/scala/leon/synthesis/Rules.scala | 21 ++++++++++++++++++++-
testcases/Choose.scala | 2 ++
2 files changed, 22 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index da031c5e7..13129acdf 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -8,7 +8,8 @@ import purescala.TypeTrees._
object Rules {
def all(synth: Synthesizer) = List(
new OnePoint(synth),
- new Ground(synth)
+ new Ground(synth),
+ new CaseSplit(synth)
)
}
@@ -90,3 +91,21 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
}
}
}
+
+class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
+ def isApplicable(p: Problem, parent: Task): List[Task] = {
+ p.phi match {
+ case Or(Seq(o1, o2)) =>
+ val sub1 = Problem(p.as, o1, p.xs)
+ val sub2 = Problem(p.as, o2, p.xs)
+
+ val onSuccess: List[Solution] => Solution = {
+ case List(s1, s2) => Solution(Or(s1.pre, s2.pre), IfExpr(s1.pre, s1.term, s2.term))
+ }
+
+ List(new Task(synth, parent, this, p, List(sub1, sub2), onSuccess, 100))
+ case _ =>
+ Nil
+ }
+ }
+}
diff --git a/testcases/Choose.scala b/testcases/Choose.scala
index 336299a0f..09f606b21 100644
--- a/testcases/Choose.scala
+++ b/testcases/Choose.scala
@@ -5,6 +5,8 @@ object ChooseTest {
def c0(): Int = choose{ (x1: Int) => x1 > 13 }
def b0(): Int = choose{ (x1: Int) => x1 > 13 && x1 < 2 }
+ def t0(a: Int): Int = choose{ (x1: Int) => (a > 13 && x1 == 2) || (a < 2 && x1 == 0) }
+
def c1(a: Int): Int = choose{ (x1: Int) => x1 > a }
def c2(a: Int): (Int, Int) = choose{ (x1: Int, x2: Int) => x1 > a && x2 > a }
def c3(a: Int): (Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int) => x1 > a && x2 > a }
--
GitLab