Implement case-split

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
+    }
+  }
+}

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 }