diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2e4a3946ae55b6676592c11c3d175ff167cf569e
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -0,0 +1,88 @@
+package leon
+package synthesis
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+
+object Heuristics {
+ def all(synth: Synthesizer) = Set(
+ new IntInduction(synth)
+ )
+}
+
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) {
+ def applyOn(task: Task): RuleResult = {
+ val p = task.problem
+
+ if (!p.as.isEmpty && !p.xs.isEmpty) {
+ val xss = p.xs.toSet
+ val ass = p.as.toSet
+
+ val tpe = TupleType(p.xs.map(_.getType))
+
+ var i = 0;
+ var maxTries = 3;
+
+ var result: Option[RuleResult] = None
+ var predicates: Seq[Expr] = Seq()
+
+ while (result.isEmpty && i < maxTries) {
+ val phi = And(p.phi +: predicates)
+ synth.solveSAT(phi) match {
+ case (Some(true), satModel) =>
+ val satXsModel = satModel.filterKeys(xss)
+
+ val newPhi = valuateWithModelIn(phi, xss, satModel)
+
+ synth.solveSAT(Not(newPhi)) match {
+ case (Some(true), invalidModel) =>
+ // Found as such as the xs break, refine predicates
+ predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
+
+ case (Some(false), _) =>
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+
+ case _ =>
+ result = Some(RuleInapplicable)
+ }
+
+ case (Some(false), _) =>
+ if (predicates.isEmpty) {
+ result = Some(RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))))
+ } else {
+ result = Some(RuleInapplicable)
+ }
+ case _ =>
+ result = Some(RuleInapplicable)
+ }
+
+ i += 1
+ }
+
+ result.getOrElse(RuleInapplicable)
+ } else {
+ RuleInapplicable
+ }
+ }
+}
+
+
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) {
+ def applyOn(task: Task): RuleResult = {
+ val p = task.problem
+
+ p.as.find(_.getType == Int32Type) match {
+ case Some(inductOn) =>
+
+ val subBase = Problem(p.as.filterNot(_ == inductOn), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
+ // val subGT = Problem(p.as + tmpGT, And(Seq(p.phi, GreaterThan(Variable(inductOn), IntLiteral(0)), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
+
+ RuleDecomposed(List(subBase), forward)
+ case None =>
+ RuleInapplicable
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 8b78e8429bc0a558079b1d5a3e11bce932af5598..7fb8a3c8eae2f5f0e716e4574074e7d325219c4a 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -8,13 +8,12 @@ import purescala.TreeOps._
import purescala.TypeTrees._
object Rules {
- def all(synth: Synthesizer) = List(
+ def all(synth: Synthesizer) = Set(
new Unification.DecompTrivialClash(synth),
new Unification.OccursCheck(synth),
new ADTDual(synth),
new OnePoint(synth),
new Ground(synth),
- new OptimisticGround(synth),
new CaseSplit(synth),
new UnusedInput(synth),
new UnconstrainedOutput(synth),
@@ -103,62 +102,6 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
}
}
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
- if (!p.as.isEmpty && !p.xs.isEmpty) {
- val xss = p.xs.toSet
- val ass = p.as.toSet
-
- val tpe = TupleType(p.xs.map(_.getType))
-
- var i = 0;
- var maxTries = 3;
-
- var result: Option[RuleResult] = None
- var predicates: Seq[Expr] = Seq()
-
- while (result.isEmpty && i < maxTries) {
- val phi = And(p.phi +: predicates)
- synth.solveSAT(phi) match {
- case (Some(true), satModel) =>
- val satXsModel = satModel.filterKeys(xss)
-
- val newPhi = valuateWithModelIn(phi, xss, satModel)
-
- synth.solveSAT(Not(newPhi)) match {
- case (Some(true), invalidModel) =>
- // Found as such as the xs break, refine predicates
- predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
-
- case (Some(false), _) =>
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
-
- case _ =>
- result = Some(RuleInapplicable)
- }
-
- case (Some(false), _) =>
- if (predicates.isEmpty) {
- result = Some(RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))))
- } else {
- result = Some(RuleInapplicable)
- }
- case _ =>
- result = Some(RuleInapplicable)
- }
-
- i += 1
- }
-
- result.getOrElse(RuleInapplicable)
- } else {
- RuleInapplicable
- }
- }
-}
-
class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -332,21 +275,3 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
}
}
-object Heuristics {
- class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
- p.as.find(_.getType == Int32Type) match {
- case Some(inductOn) =>
-
- val subBase = Problem(p.as.filterNot(_ == inductOn), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
- // val subGT = Problem(p.as + tmpGT, And(Seq(p.phi, GreaterThan(Variable(inductOn), IntLiteral(0)), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
-
- RuleDecomposed(List(subBase), forward)
- case None =>
- RuleInapplicable
- }
- }
- }
-}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 7fc3fa8844e250b84a822ff6fb812c75c543d3be..918b6584a08e2f0a29615fc2b7e3c075e9c3f21d 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -18,7 +18,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
var derivationCounter = 1;
- def synthesize(p: Problem, rules: List[Rule]): Solution = {
+ def synthesize(p: Problem, rules: Set[Rule]): Solution = {
val workList = new PriorityQueue[Task]()
val rootTask = new RootTask(this, p)
@@ -56,7 +56,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
(None, Map())
}
- val rules = Rules.all(this)
+ val rules = Rules.all(this) ++ Heuristics.all(this)
import purescala.Trees._
def synthesizeAll(program: Program): Map[Choose, Solution] = {
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 3584447e27021c46f7005926b7d4852fc40cb096..ee579b1a1ee62281ee24eb92b62354e0cb6d2d8b 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -33,7 +33,7 @@ class SimpleTask(synth: Synthesizer,
}
def run: List[Task] = {
- synth.rules.map(r => new ApplyRuleTask(synth, this, problem, r))
+ synth.rules.map(r => new ApplyRuleTask(synth, this, problem, r)).toList
}
var failed = Set[Rule]()
diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/SortedList.scala
index 2e5a42ff979688704928410e1addcbd75ae6c8d0..09f664a12f57c5506d72fcd7615f2093d9938f99 100644
--- a/testcases/synthesis/SortedList.scala
+++ b/testcases/synthesis/SortedList.scala
@@ -24,6 +24,9 @@ object SortedList {
def insertSynth(in: List, v: Int) = choose{ (out: List) => content(out) == content(in) ++ Set(v) }
+ def tailSynth(in: List) = choose{out: List => size(out)+1 == size(in)}
+ def consSynth(in: List) = choose{out: List => size(out) == size(in)+1}
+
def insert1(l: List, v: Int) = (
Cons(v, l)
) ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l))