From 8f6204930a3f4194482cbcdfd573d4bff8542bc8 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 4 Jan 2013 16:39:25 +0100
Subject: [PATCH] Improve search by making it more deterministic
---
.../scala/leon/synthesis/SimpleSearch.scala | 5 ++--
.../synthesis/heuristics/ADTInduction.scala | 2 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
.../leon/synthesis/search/AndOrGraph.scala | 23 ++++++++-----------
.../synthesis/search/AndOrGraphSearch.scala | 2 +-
5 files changed, 15 insertions(+), 19 deletions(-)
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 393177e77..2b329ef70 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -42,14 +42,13 @@ class SimpleSearch(synth: Synthesizer,
def expandAndTask(t: TaskRunRule): ExpandResult[TaskTryRules] = {
val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
+ info(prefix+"Got: "+t.problem)
t.app.apply(sctx) match {
case RuleSuccess(sol) =>
- info(prefix+"Got: "+t.problem)
info(prefix+"Solved with: "+sol)
ExpandSuccess(sol)
case RuleDecomposed(sub) =>
- info(prefix+"Got: "+t.problem)
info(prefix+"Decomposed into:")
for(p <- sub) {
info(prefix+" - "+p)
@@ -58,6 +57,8 @@ class SimpleSearch(synth: Synthesizer,
Expanded(sub.map(TaskTryRules(_)))
case RuleApplicationImpossible =>
+ info(prefix+"Failed")
+
ExpandFailure()
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 1c50c18c8..c9e5af133 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -40,7 +40,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
val innerPhi = substAll(residualMap + (origId -> Variable(inductOn)), p.phi)
val innerPC = substAll(residualMap + (origId -> Variable(inductOn)), p.pc)
- val subProblemsInfo = for (dcd <- cd.knownDescendents) yield dcd match {
+ val subProblemsInfo = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
case ccd : CaseClassDef =>
var recCalls = Map[List[Identifier], List[Expr]]()
var postFs = List[Expr]()
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 4680ca40b..61d3a9768 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -14,7 +14,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
- val optCases = for (dcd <- cd.knownDescendents) yield dcd match {
+ val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
case ccd : CaseClassDef =>
val toSat = And(p.pc, Not(CaseClassInstanceOf(ccd, Variable(id))))
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 48f38675a..251734160 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -77,11 +77,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
}
def expandLeaf(l: OrLeaf, succ: List[AT]) {
- val n = new OrNode(this, Map(), l.task)
- n.alternatives = succ.map(t => t -> new AndLeaf(n, t)).toMap
- n.updateMin()
-
- subProblems += l.task -> n
+ subProblems += l.task -> new OrNode(this, succ, l.task)
}
def notifySolution(sub: OrTree, sol: S) {
@@ -106,11 +102,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
object RootNode extends OrLeaf(null, root) {
override def expandWith(succ: List[AT]) {
- val n = new OrNode(null, Map(), root)
- n.alternatives = succ.map(t => t -> new AndLeaf(n, t)).toMap
- n.updateMin()
-
- tree = n
+ tree = new OrNode(null, succ, root)
}
}
@@ -122,10 +114,13 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
}
- class OrNode(val parent: AndNode, var alternatives: Map[AT, AndTree], val task: OT) extends OrTree with Node[AndTree] {
- var triedAlternatives = Map[AT, AndTree]()
- var minAlternative: AndTree = _
- var minCost = costModel.taskCost(task)
+ class OrNode(val parent: AndNode, val altTasks: List[AT], val task: OT) extends OrTree with Node[AndTree] {
+ var alternatives: Map[AT, AndTree] = altTasks.map(t => t -> new AndLeaf(this, t)).toMap
+ var triedAlternatives = Map[AT, AndTree]()
+ var minAlternative: AndTree = _
+ var minCost = costModel.taskCost(task)
+
+ updateMin()
def updateMin() {
if (!alternatives.isEmpty) {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index e8d402b4f..79e70aecf 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -20,7 +20,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
case l: g.Leaf =>
collectLeaf(WL(l, newCosts.reverse))
case a: g.AndNode =>
- for (o <- (a.subProblems -- a.subSolutions.keySet).values) {
+ for (o <- a.subTasks.filterNot(a.subSolutions.keySet).map(a.subProblems)) {
collectFromOr(o, newCosts)
}
}
--
GitLab