From 40ed136d8019e10e73b8dff63d60218ab8e9e061 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 1 Nov 2012 16:01:59 +0100
Subject: [PATCH] Some organization
---
.../scala/leon/synthesis/Heuristics.scala | 88 +++++++++++++++++++
src/main/scala/leon/synthesis/Rules.scala | 77 +---------------
.../scala/leon/synthesis/Synthesizer.scala | 4 +-
src/main/scala/leon/synthesis/Task.scala | 2 +-
testcases/synthesis/SortedList.scala | 3 +
5 files changed, 95 insertions(+), 79 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/Heuristics.scala
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
new file mode 100644
index 000000000..2e4a3946a
--- /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 8b78e8429..7fb8a3c8e 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 7fc3fa884..918b6584a 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 3584447e2..ee579b1a1 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 2e5a42ff9..09f664a12 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))
--
GitLab