From bfd09b853b9ac62d47d89f612f08c5a11a578d7d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 17 Nov 2015 18:42:09 +0100
Subject: [PATCH] Remove dependencies on solvers
---
.../scala/leon/synthesis/rules/ADTSplit.scala | 39 +++++++-----
.../leon/synthesis/rules/EqualitySplit.scala | 45 +++++++-------
.../synthesis/rules/InequalitySplit.scala | 62 +++++++------------
3 files changed, 72 insertions(+), 74 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 294c6e137..7ed086087 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/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
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index bc62dbba8..132ea9f76 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/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) =>
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 292e99de8..8925276af 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/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) =>
--
GitLab