diff --git a/src/main/scala/leon/synthesis/Cost.scala b/src/main/scala/leon/synthesis/Cost.scala
index e3cb213d35d758fef1dc60a2521e5de60015e5a1..7d989b3476c18edd1ed6a0d16a948dc8da585aa6 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 a9a7f17351a9696217cb7cecb56867f535e91d7b..aaf3054ae57bcad27a322003311fad84d208ce03 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 96eccf1d1a1ac7984305a6db21cdbeb2dfbd42ef..ae3717d3cb1cfbc721a63bdc560e236426f1429b 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 0f3fd8607da4a14bcd57bb7bc3583f94124d3655..ac005a3803fa02b6e0992e7c1dd1b296e8b6a509 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 74659050bc917b8a36f3bbbcc3e933a3217d95e5..75913701ce175c2d2da747b04ad09047b2127f13 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 0dbf5d73d507e33e2df5d60fb1c25abddc6b5652..04059da77e6be06e7a1309a8ce4046223559818f 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 =>