diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 07347e95ba51f78d3603807ea3a95c3dbfcbdb62..04cd58c5a70b6a2bbbec25ce9807e00457a746a8 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -2,6 +2,8 @@ package leon
package synthesis
package rules
+import solvers.TimeoutSolver
+
import purescala.Trees._
import purescala.Common._
import purescala.TypeTrees._
@@ -11,6 +13,8 @@ import purescala.Definitions._
case object ADTSplit extends Rule("ADT Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
+ val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
@@ -18,7 +22,7 @@ case object ADTSplit extends Rule("ADT Split.") {
case ccd : CaseClassDef =>
val toSat = And(p.pc, Not(CaseClassInstanceOf(ccd, Variable(id))))
- val isImplied = sctx.solver.solveSAT(toSat) match {
+ val isImplied = solver.solveSAT(toSat) match {
case (Some(false), _) => true
case _ => false
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 2cb41ef38293fc445c65a3b45f8191ae8f5d4e6e..1bdf8d1cfb68026d0257d74e189752ae15949a33 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -2,6 +2,7 @@ package leon
package synthesis
package rules
+import solvers.TimeoutSolver
import purescala.Trees._
import purescala.Common._
import purescala.Definitions._
@@ -384,7 +385,7 @@ case object CEGIS extends Rule("CEGIS") {
var unrolings = 0
val maxUnrolings = 3
- val mainSolver: FairZ3Solver = sctx.solver.asInstanceOf[FairZ3Solver]
+ val mainSolver = new TimeoutSolver(sctx.solver, 2000L) // 2sec
var exampleInputs = Set[Seq[Expr]]()
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 125b2e6060f115f699b45bd5bb682e785c486c6b..c59d37aa014af86df043465d4db59194fe86ff0e 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -2,6 +2,7 @@ package leon
package synthesis
package rules
+import solvers.TimeoutSolver
import purescala.Trees._
import purescala.Common._
import purescala.TypeTrees._
@@ -10,11 +11,13 @@ import purescala.Extractors._
case object EqualitySplit extends Rule("Eq. Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+ val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+
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 = sctx.solver.solveSAT(Not(toValEQ)) match {
+ val impliesEQ = solver.solveSAT(Not(toValEQ)) match {
case (Some(false), _) => true
case _ => false
}
@@ -22,7 +25,7 @@ case object EqualitySplit extends Rule("Eq. Split.") {
if (!impliesEQ) {
val toValNE = Implies(p.pc, Not(Equals(Variable(a1), Variable(a2))))
- val impliesNE = sctx.solver.solveSAT(Not(toValNE)) match {
+ val impliesNE = solver.solveSAT(Not(toValNE)) match {
case (Some(false), _) => true
case _ => false
}
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 953ad5b56f6d0a7dfa7b5551be27fb4d8554079a..bb74de12aba2f3a80861261cc221e045edd3f11f 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -2,6 +2,7 @@ package leon
package synthesis
package rules
+import solvers.TimeoutSolver
import purescala.Trees._
import purescala.TypeTrees._
import purescala.TreeOps._
@@ -11,9 +12,11 @@ case object Ground extends Rule("Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
+ val solver = new TimeoutSolver(sctx.solver, 1000L) // We give that 1s
+
val tpe = TupleType(p.xs.map(_.getType))
- sctx.solver.solveSAT(p.phi) match {
+ solver.solveSAT(p.phi) match {
case (Some(true), model) =>
val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
Some(RuleInstantiation.immediateSuccess(p, this, sol))
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index d79bd66f06bfaac93de04e2288ed766d29e9c52b..11040132becd8790fbfb93ebf84a5163d41e0a8a 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -2,6 +2,8 @@ package leon
package synthesis
package rules
+import solvers.TimeoutSolver
+
import purescala.Trees._
import purescala.TypeTrees._
import purescala.Common._
@@ -11,11 +13,13 @@ import purescala.Extractors._
case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+ val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+
val candidates = p.as.filter(_.getType == Int32Type).combinations(2).toList.filter {
case List(a1, a2) =>
val toValLT = Implies(p.pc, LessThan(Variable(a1), Variable(a2)))
- val impliesLT = sctx.solver.solveSAT(Not(toValLT)) match {
+ val impliesLT = solver.solveSAT(Not(toValLT)) match {
case (Some(false), _) => true
case _ => false
}
@@ -23,7 +27,7 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
if (!impliesLT) {
val toValGT = Implies(p.pc, GreaterThan(Variable(a1), Variable(a2)))
- val impliesGT = sctx.solver.solveSAT(Not(toValGT)) match {
+ val impliesGT = solver.solveSAT(Not(toValGT)) match {
case (Some(false), _) => true
case _ => false
}
@@ -31,7 +35,7 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
if (!impliesGT) {
val toValEQ = Implies(p.pc, Equals(Variable(a1), Variable(a2)))
- val impliesEQ = sctx.solver.solveSAT(Not(toValEQ)) match {
+ val impliesEQ = solver.solveSAT(Not(toValEQ)) match {
case (Some(false), _) => true
case _ => false
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index d25db6600047ae1f607b7023bf26735a51cb5783..7e65ed7970c6e9d5c67e25b997c8f9c8d3f48f16 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -2,6 +2,7 @@ package leon
package synthesis
package rules
+import solvers.TimeoutSolver
import purescala.Trees._
import purescala.TypeTrees._
import purescala.TreeOps._
@@ -12,6 +13,9 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
if (!p.as.isEmpty && !p.xs.isEmpty) {
val res = new RuleInstantiation(p, this, SolutionBuilder.none) {
def apply(sctx: SynthesisContext) = {
+
+ val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+
val xss = p.xs.toSet
val ass = p.as.toSet
@@ -27,14 +31,14 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
while (result.isEmpty && i < maxTries && continue) {
val phi = And(p.pc +: p.phi +: predicates)
//println("SOLVING " + phi + " ...")
- sctx.solver.solveSAT(phi) match {
+ solver.solveSAT(phi) match {
case (Some(true), satModel) =>
val satXsModel = satModel.filterKeys(xss)
val newPhi = valuateWithModelIn(phi, xss, satModel)
//println("REFUTING " + Not(newPhi) + "...")
- sctx.solver.solveSAT(Not(newPhi)) match {
+ solver.solveSAT(Not(newPhi)) match {
case (Some(true), invalidModel) =>
// Found as such as the xs break, refine predicates
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates