Remove dependencies on solvers

src/main/scala/leon/synthesis/rules/ADTSplit.scala

@@ -11,32 +11,43 @@ import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Definitions._
-import solvers._
 
 case object ADTSplit extends Rule("ADT Split.") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(200L))
+    // We approximate knowledge of types based on facts found at the top-level
+    // we don't care if the variables are known to be equal or not, we just
+    // don't want to split on two variables for which only one split
+    // alternative is viable. This should be much less expensive than making
+    //  calls to a solver for each pair.
+    var facts = Map[Identifier, CaseClassType]()
+
+    def addFacts(e: Expr): Unit = e match {
+      case Equals(Variable(a), CaseClass(cct, _))         => facts += a -> cct
+      case IsInstanceOf(Variable(a), cct: CaseClassType)  => facts += a -> cct
+      case _ =>
+    }
+
+    val TopLevelAnds(as) = and(p.pc, p.phi)
+    for (e <- as) {
+      addFacts(e)
+    }
 
     val candidates = p.as.collect {
       case IsTyped(id, act @ AbstractClassType(cd, tpes)) =>
 
-        val optCases = for (dcd <- cd.knownDescendants.sortBy(_.id.name)) yield dcd match {
+        val optCases = cd.knownDescendants.sortBy(_.id.name).collect {
           case ccd : CaseClassDef =>
             val cct = CaseClassType(ccd, tpes)
-            val toSat = and(p.pc, IsInstanceOf(Variable(id), cct))
 
-            val isImplied = solver.solveSAT(toSat) match {
-              case (Some(false), _) => true
-              case _ => false
-            }
-
-            if (!isImplied) {
-              Some(ccd)
+            if (facts contains id) {
+              if (cct == facts(id)) {
+                Seq(ccd)
+              } else {
+                Nil
+              }
             } else {
-              None
+              Seq(ccd)
             }
-          case _ =>
-            None
         }
 
         val cases = optCases.flatten

src/main/scala/leon/synthesis/rules/EqualitySplit.scala

@@ -6,6 +6,7 @@ package rules
 
 import leon.purescala.Common.Identifier
 import purescala.Expressions._
+import purescala.Extractors._
 import purescala.Constructors._
 
 import solvers._
@@ -14,31 +15,31 @@ import scala.concurrent.duration._
 
 case object EqualitySplit extends Rule("Eq. Split") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
+    // We approximate knowledge of equality based on facts found at the top-level
+    // we don't care if the variables are known to be equal or not, we just
+    // don't want to split on two variables for which only one split
+    // alternative is viable. This should be much less expensive than making
+    //  calls to a solver for each pair.
+    var facts = Set[Set[Identifier]]()
 
-    val candidates = p.as.groupBy(_.getType).mapValues(_.combinations(2).filter {
-      case List(a1, a2) =>
-        val toValEQ = implies(p.pc, Equals(Variable(a1), Variable(a2)))
-
-        val impliesEQ = solver.solveSAT(Not(toValEQ)) match {
-          case (Some(false), _) => true
-          case _ => false
-        }
-
-        if (!impliesEQ) {
-          val toValNE = implies(p.pc, not(Equals(Variable(a1), Variable(a2))))
+    def addFacts(e: Expr): Unit = e match {
+      case Not(e) => addFacts(e)
+      case LessThan(Variable(a), Variable(b))      => facts += Set(a,b)
+      case LessEquals(Variable(a), Variable(b))    => facts += Set(a,b)
+      case GreaterThan(Variable(a), Variable(b))   => facts += Set(a,b)
+      case GreaterEquals(Variable(a), Variable(b)) => facts += Set(a,b)
+      case Equals(Variable(a), Variable(b))        => facts += Set(a,b)
+      case _ =>
+    }
 
-          val impliesNE = solver.solveSAT(Not(toValNE)) match {
-            case (Some(false), _) => true
-            case _ => false
-          }
+    val TopLevelAnds(as) = and(p.pc, p.phi)
+    for (e <- as) {
+      addFacts(e)
+    }
 
-          !impliesNE
-        } else {
-          false
-        }
-      case _ => false
-    }).values.flatten
+    val candidates = p.as.groupBy(_.getType).mapValues{ as =>
+      as.combinations(2).filterNot(facts contains _.toSet)
+    }.values.flatten
 
     candidates.flatMap {
       case List(a1, a2) =>

src/main/scala/leon/synthesis/rules/InequalitySplit.scala

@@ -7,53 +7,39 @@ package rules
 import purescala.Expressions._
 import purescala.Types._
 import purescala.Constructors._
-
-import solvers._
+import purescala.Extractors._
+import purescala.Common._
 
 import scala.concurrent.duration._
 
 case object InequalitySplit extends Rule("Ineq. Split.") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
+    // We approximate knowledge of equality based on facts found at the top-level
+    // we don't care if the variables are known to be equal or not, we just
+    // don't want to split on two variables for which only one split
+    // alternative is viable. This should be much less expensive than making
+    //  calls to a solver for each pair.
+    var facts = Set[Set[Identifier]]()
+
+    def addFacts(e: Expr): Unit = e match {
+      case Not(e) => addFacts(e)
+      case LessThan(Variable(a), Variable(b))      => facts += Set(a,b)
+      case LessEquals(Variable(a), Variable(b))    => facts += Set(a,b)
+      case GreaterThan(Variable(a), Variable(b))   => facts += Set(a,b)
+      case GreaterEquals(Variable(a), Variable(b)) => facts += Set(a,b)
+      case Equals(Variable(a), Variable(b))        => facts += Set(a,b)
+      case _ =>
+    }
+
+    val TopLevelAnds(as) = and(p.pc, p.phi)
+    for (e <- as) {
+      addFacts(e)
+    }
 
     val argsPairs = p.as.filter(_.getType == IntegerType).combinations(2) ++
                     p.as.filter(_.getType == Int32Type).combinations(2)
 
-    val candidates = argsPairs.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
-    }
-
+    val candidates = argsPairs.toList.filter { case List(a1, a2) => !(facts contains Set(a1, a2)) }
 
     candidates.flatMap {
       case List(a1, a2) =>