From 0d8569f0baa35f68520abdf9c00aff16bd3ccd2f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 14 Jan 2013 19:43:13 +0100
Subject: [PATCH] Use timeouts in all synthesis rules, we don't want it to hang
on a difficult problem
---
src/main/scala/leon/synthesis/rules/ADTSplit.scala | 6 +++++-
src/main/scala/leon/synthesis/rules/Cegis.scala | 3 ++-
.../scala/leon/synthesis/rules/EqualitySplit.scala | 7 +++++--
src/main/scala/leon/synthesis/rules/Ground.scala | 5 ++++-
.../scala/leon/synthesis/rules/InequalitySplit.scala | 10 +++++++---
.../scala/leon/synthesis/rules/OptimisticGround.scala | 8 ++++++--
6 files changed, 29 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 07347e95b..04cd58c5a 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 2cb41ef38..1bdf8d1cf 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 125b2e606..c59d37aa0 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 953ad5b56..bb74de12a 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 d79bd66f0..11040132b 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 d25db6600..7e65ed797 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
--
GitLab