From 261ea138c174032e32c9d236a32bc29fc7dff88e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 21 Nov 2012 17:26:28 +0100
Subject: [PATCH] Fix Search, fix problem cost, re-introduce ADT Split
---
src/main/scala/leon/synthesis/Cost.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 10 +++++-
.../scala/leon/synthesis/Synthesizer.scala | 2 +-
.../synthesis/rules/OptimisticGround.scala | 8 ++---
.../leon/synthesis/search/AndOrGraph.scala | 4 +--
.../synthesis/search/AndOrGraphSearch.scala | 34 ++++++-------------
6 files changed, 27 insertions(+), 33 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Cost.scala b/src/main/scala/leon/synthesis/Cost.scala
index e3cb213d3..7d989b347 100644
--- a/src/main/scala/leon/synthesis/Cost.scala
+++ b/src/main/scala/leon/synthesis/Cost.scala
@@ -16,7 +16,7 @@ case class SolutionCost(s: Solution) extends Cost {
}
case class ProblemCost(p: Problem) extends Cost {
- val value = math.pow(2, p.xs.size).toInt + formulaSize(p.phi)
+ val value = p.xs.size
}
case class RuleApplicationCost(rule: Rule, app: RuleApplication) extends Cost {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index a9a7f1735..aaf3054ae 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -20,7 +20,7 @@ object Rules {
new EqualitySplit(_),
new CEGIS(_),
new Assert(_),
-// new ADTSplit(_),
+ new ADTSplit(_),
new IntegerEquation(_),
new IntegerInequalities(_)
)
@@ -50,6 +50,14 @@ object RuleFastApplication {
}
}
+object RuleFastInapplicable {
+ def apply() = {
+ RuleResult(List(new RuleApplication(0, ls => Solution.simplest) {
+ def apply() = RuleApplicationImpossible
+ }))
+ }
+}
+
object RuleFastStep {
def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
RuleResult(List(RuleFastApplication(sub, onSuccess)))
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 96eccf1d1..ae3717d3c 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -72,7 +72,7 @@ class Synthesizer(val reporter: Reporter,
}
case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
- val cost = Cost.zero
+ val cost = ProblemCost(p)
override def toString = p.toString
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 0f3fd8607..ac005a380 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -40,23 +40,23 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
result = Some(RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
case _ =>
- result = Some(RuleInapplicable)
+ result = Some(RuleFastInapplicable())
}
case (Some(false), _) =>
if (predicates.isEmpty) {
result = Some(RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
- result = Some(RuleInapplicable)
+ result = Some(RuleFastInapplicable())
}
case _ =>
- result = Some(RuleInapplicable)
+ result = Some(RuleFastInapplicable())
}
i += 1
}
- result.getOrElse(RuleInapplicable)
+ result.getOrElse(RuleFastInapplicable())
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 74659050b..75913701c 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -131,13 +131,13 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
if (!alternatives.isEmpty) {
minAlternative = alternatives.values.minBy(_.minCost)
val old = minCost
- minCost = minAlternative.minCost + task.cost
+ minCost = minAlternative.minCost
if (minCost != old) {
Option(parent).foreach(_.updateMin())
}
} else {
minAlternative = null
- minCost = task.cost
+ minCost = Cost.zero
}
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index 0dbf5d73d..04059da77 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -4,35 +4,21 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
OT <: AOOrTask[S],
S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
- def nextLeaf: Option[g.Leaf] = {
- import collection.mutable.PriorityQueue
-
- case class WT(t: g.Tree, prefixCost: Cost) extends Ordered[WT] {
- val cost = t.minCost + prefixCost
-
- def compare(that: WT) = that.cost.compare(this.cost) // DESC
- }
-
- val q = new PriorityQueue[WT]()
- q += WT(g.tree, Cost.zero)
+ def nextLeafSimple: Option[g.Leaf] = {
+ var c : g.Tree = g.tree
var res: Option[g.Leaf] = None
- while(res.isEmpty && !q.isEmpty) {
- q.dequeue() match {
- case WT(l: g.Leaf, c) =>
+ while(res.isEmpty) {
+ c match {
+ case l: g.Leaf =>
res = Some(l)
- case WT(an: g.AndNode, c) =>
- if (!an.isSolved) {
- q ++= (an.subProblems -- an.subSolutions.keySet).values.map(n => WT(n, c + an.minCost))
- }
-
- case WT(on: g.OrNode, c) =>
- if (!on.isSolved) {
- q ++= on.alternatives.values.map(n => WT(n, c + on.minCost))
- }
+ case an: g.AndNode =>
+ c = (an.subProblems -- an.subSolutions.keySet).values.minBy(_.minCost)
+ case on: g.OrNode =>
+ c = on.alternatives.values.minBy(_.minCost)
}
}
@@ -48,7 +34,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
def search(): Option[S] = {
while (!g.tree.isSolved && continue) {
- nextLeaf match {
+ nextLeafSimple match {
case Some(l) =>
l match {
case al: g.AndLeaf =>
--
GitLab