/* Copyright 2009-2014 EPFL, Lausanne */

package leon
package synthesis
package rules

import purescala.Expressions._
import purescala.Types._
import purescala.Constructors._

import solvers._

case object InequalitySplit extends Rule("Ineq. Split.") {
  def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
    val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory)

    val candidates = p.as.filter(_.getType == IntegerType).combinations(2).toList.filter {
      case List(a1, a2) =>
        val toValLT = implies(p.pc, LessThan(Variable(a1), Variable(a2)))

        val impliesLT = solver.solveSAT(not(toValLT)) match {
          case (Some(false), _) => true
          case _ => false
        }

        if (!impliesLT) {
          val toValGT = implies(p.pc, GreaterThan(Variable(a1), Variable(a2)))

          val impliesGT = solver.solveSAT(not(toValGT)) match {
            case (Some(false), _) => true
            case _ => false
          }

          if (!impliesGT) {
            val toValEQ = implies(p.pc, Equals(Variable(a1), Variable(a2)))

            val impliesEQ = solver.solveSAT(not(toValEQ)) match {
              case (Some(false), _) => true
              case _ => false
            }

            !impliesEQ
          } else {
            false
          }
        } else {
          false
        }
      case _ => false
    }


    candidates.flatMap {
      case List(a1, a2) =>

        val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc))
        val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc))
        val subGT = p.copy(pc = and(GreaterThan(Variable(a1), Variable(a2)), p.pc))

        val onSuccess: List[Solution] => Option[Solution] = {
          case sols@List(sLT, sEQ, sGT) =>
            val pre = orJoin(sols.map(_.pre))
            val defs = sLT.defs ++ sEQ.defs ++ sGT.defs

            val term = IfExpr(
              LessThan(Variable(a1), Variable(a2)),
              sLT.term,
              IfExpr(
                Equals(Variable(a1), Variable(a2)),
                sEQ.term,
                sGT.term
              )
            )

            Some(Solution(pre, defs, term, sols.forall(_.isTrusted)))
          case _ =>
            None
        }

        Some(decomp(List(subLT, subEQ, subGT), onSuccess, s"Ineq. Split on '$a1' and '$a2'"))
      case _ =>
        None
    }
  }
}