package leon
package synthesis
package rules

import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._

class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
  def applyOn(task: Task): RuleResult = {
    val p = task.problem
    p.phi match {
      case Or(Seq(o1, o2)) =>
        val sub1 = Problem(p.as, p.c, o1, p.xs)
        val sub2 = Problem(p.as, p.c, o2, p.xs)

        val onSuccess: List[Solution] => Solution = { 
          case List(Solution(p1, d1, t1), Solution(p2, d2, t2)) => Solution(Or(p1, p2), d1++d2, IfExpr(p1, t1, t2))
          case _ => Solution.none
        }

        RuleOneStep(List(sub1, sub2), onSuccess)
      case _ =>
        RuleInapplicable
    }
  }
}