From e69cbc147a291ac3483f3bb025cdbf1843fdd83d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 19 Nov 2012 22:23:19 +0100
Subject: [PATCH] Some re-work based on and-or graphs
---
src/main/scala/leon/aographs/Graph.scala | 235 ++++++++++++++++++
src/main/scala/leon/synthesis/Cost.scala | 20 ++
.../scala/leon/synthesis/DerivationTree.scala | 2 +
.../scala/leon/synthesis/Heuristics.scala | 12 +-
src/main/scala/leon/synthesis/Rules.scala | 41 +--
src/main/scala/leon/synthesis/Solution.scala | 9 +-
.../scala/leon/synthesis/Synthesizer.scala | 136 +++++-----
src/main/scala/leon/synthesis/Task.scala | 2 +
.../synthesis/heuristics/ADTInduction.scala | 6 +-
.../synthesis/heuristics/IntInduction.scala | 8 +-
.../heuristics/OptimisticInjection.scala | 8 +-
.../heuristics/SelectiveInlining.scala | 8 +-
.../scala/leon/synthesis/rules/ADTDual.scala | 8 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 8 +-
.../scala/leon/synthesis/rules/Assert.scala | 12 +-
.../leon/synthesis/rules/CaseSplit.scala | 7 +-
.../scala/leon/synthesis/rules/Cegis.scala | 8 +-
.../leon/synthesis/rules/EqualitySplit.scala | 8 +-
.../scala/leon/synthesis/rules/Ground.scala | 12 +-
.../synthesis/rules/IntegerEquation.scala | 10 +-
.../synthesis/rules/IntegerInequalities.scala | 9 +-
.../scala/leon/synthesis/rules/OnePoint.scala | 9 +-
.../synthesis/rules/OptimisticGround.scala | 18 +-
.../synthesis/rules/UnconstrainedOutput.scala | 7 +-
.../leon/synthesis/rules/Unification.scala | 16 +-
.../leon/synthesis/rules/UnusedInput.scala | 7 +-
26 files changed, 428 insertions(+), 198 deletions(-)
create mode 100644 src/main/scala/leon/aographs/Graph.scala
create mode 100644 src/main/scala/leon/synthesis/Cost.scala
diff --git a/src/main/scala/leon/aographs/Graph.scala b/src/main/scala/leon/aographs/Graph.scala
new file mode 100644
index 000000000..6519fe3b5
--- /dev/null
+++ b/src/main/scala/leon/aographs/Graph.scala
@@ -0,0 +1,235 @@
+package leon.aographs
+
+trait AOCost extends Ordered[AOCost] {
+ def +(that: AOCost): AOCost = AOCostFixed(value + that.value)
+
+ def value: Int
+
+ def compare(that: AOCost) = this.value - that.value
+}
+
+case class AOCostFixed(value: Int) extends AOCost
+
+object AOCost {
+ val zero = new AOCostFixed(0)
+}
+
+trait AOTask[S <: AOSolution] {
+ def composeSolution(sols: List[S]): S
+ def cost: AOCost
+}
+
+trait AOSolution {
+ def cost: AOCost
+}
+
+
+class AndOrGraph[T <: AOTask[S], S <: AOSolution](val root: T) {
+ type C = AOCost
+
+ var tree: AndTree = RootNode
+
+ trait Tree {
+ val task : T
+ val parent: Node
+
+ def minCost: C
+
+ def isSolved: Boolean
+ }
+
+ abstract class AndTree extends Tree
+ abstract class OrTree extends Tree
+
+
+ trait Leaf extends Tree with Ordered[Leaf] {
+ val minCost: C = task.cost
+
+ def compare(that: Leaf) = this.minCost.compare(that.minCost)
+
+ def isSolved: Boolean = false
+ def expandWith(succ: List[T])
+ }
+
+ trait Node {
+ def expandLeaf(l: Leaf, succ: List[T])
+ def unsolvable(l: Tree)
+ def notifySolution(sub: Tree, sol: S)
+
+ var solution: Option[S] = None
+
+ def isSolved: Boolean = solution.isDefined
+ }
+
+ case class AndNode(parent: OrNode, subTasks: List[T], task: T) extends AndTree with Node {
+ var subProblems = Map[T, OrTree]()
+ var subSolutions = Map[T, S]()
+
+ def computeCost = {
+ solution match {
+ case Some(s) =>
+ s.cost
+ case _ =>
+ val subCosts = subProblems.map { case (t, ot) => subSolutions.get(t).map(_.cost).getOrElse(ot.minCost) }
+
+ subCosts.foldLeft(task.cost)(_ + _)
+ }
+ }
+
+ var minCost = computeCost
+
+ def unsolvable(l: Tree) {
+ parent.unsolvable(this)
+ }
+
+ def expandLeaf(l: Leaf, succ: List[T]) {
+ val n = OrNode(this, Map(), l.task)
+ n.alternatives = succ.map(t => t -> AndLeaf(n, t)).toMap
+ n.minAlternative = n.computeMin
+
+ subProblems += l.task -> n
+ }
+
+ def notifySolution(sub: Tree, sol: S) {
+ subSolutions += sub.task -> sol
+
+ if (subSolutions.size == subProblems.size) {
+ solution = Some(task.composeSolution(subTasks.map(subSolutions)))
+ minCost = computeCost
+
+ notifyParent(solution.get)
+ } else {
+ minCost = computeCost
+ }
+
+ }
+
+ def notifyParent(s: S) {
+ parent.notifySolution(this, s)
+ }
+ }
+
+ object RootNode extends AndLeaf(null, root) {
+ override def expandWith(succ: List[T]) {
+ val n = new AndNode(null, succ, task) {
+ override def unsolvable(l: Tree) {}
+ override def notifyParent(sol: S) {}
+ }
+
+ n.subProblems = succ.map(t => t -> OrLeaf(n, t)).toMap
+
+ tree = n
+ }
+ }
+
+ case class AndLeaf(parent: OrNode, task: T) extends AndTree with Leaf {
+ def expandWith(succ: List[T]) {
+ parent.expandLeaf(this, succ)
+ }
+
+ }
+
+
+ case class OrNode(parent: AndNode, var alternatives: Map[T, AndTree], task: T) extends OrTree with Node {
+ var minAlternative: Tree = _
+ def minCost: C = minAlternative.minCost
+
+ def computeMin = {
+ if (!alternatives.isEmpty) {
+ alternatives.values.minBy(_.minCost)
+ } else {
+ null
+ }
+ }
+
+ def unsolvable(l: Tree) {
+ alternatives -= l.task
+
+ if (alternatives.isEmpty) {
+ parent.unsolvable(this)
+ } else {
+ minAlternative = computeMin
+ }
+ }
+
+ def expandLeaf(l: Leaf, succ: List[T]) {
+ val n = AndNode(this, succ, l.task)
+ n.subProblems = succ.map(t => t -> OrLeaf(n, t)).toMap
+ n.minCost = n.computeCost
+
+ alternatives += l.task -> n
+ }
+
+ def notifySolution(sub: Tree, sol: S) {
+ solution match {
+ case Some(preSol) if (preSol.cost < sol.cost) =>
+ solution = Some(sol)
+ minAlternative = sub
+
+ parent.notifySolution(this, solution.get)
+ case None =>
+ solution = Some(sol)
+ minAlternative = sub
+
+ parent.notifySolution(this, solution.get)
+ }
+ }
+ }
+
+ case class OrLeaf(parent: AndNode, task: T) extends OrTree with Leaf {
+ def expandWith(succ: List[T]) {
+ parent.expandLeaf(this, succ)
+ }
+ }
+}
+
+abstract class AndOrGraphSearch[T <: AOTask[S], S <: AOSolution](val g: AndOrGraph[T, S]) {
+ import collection.mutable.PriorityQueue
+
+ def nextLeaf: Option[g.Leaf] = {
+ var c: g.Tree = g.tree
+ var res: Option[g.Leaf] = None
+
+ while(res.isEmpty) {
+ c match {
+ case l: g.Leaf =>
+ res = Some(l)
+
+ case an: g.AndNode =>
+ c = an.subProblems.values.minBy(_.minCost)
+
+ case on: g.OrNode =>
+ c = on.minAlternative
+ }
+ }
+
+ res
+ }
+
+ abstract class ExpandResult
+ case class Expanded(sub: List[T]) extends ExpandResult
+ case class ExpandSuccess(sol: S) extends ExpandResult
+ case object ExpandFailure extends ExpandResult
+
+ var continue = true
+
+ def search = {
+ while (!g.tree.isSolved && continue) {
+ nextLeaf match {
+ case Some(l) =>
+ processLeaf(l) match {
+ case r @ Expanded(ls) =>
+ l.expandWith(ls)
+ case r @ ExpandSuccess(sol) =>
+ l.parent.notifySolution(l, sol)
+ case r @ ExpandFailure =>
+ l.parent.unsolvable(l)
+ }
+ case None =>
+ continue = false
+ }
+ }
+ }
+
+ def processLeaf(l: g.Leaf): ExpandResult
+}
diff --git a/src/main/scala/leon/synthesis/Cost.scala b/src/main/scala/leon/synthesis/Cost.scala
new file mode 100644
index 000000000..bd479a489
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Cost.scala
@@ -0,0 +1,20 @@
+package leon
+package synthesis
+
+import purescala.Trees._
+import purescala.TreeOps._
+
+import aographs.AOCost
+
+case class SolutionCost(s: Solution) extends AOCost {
+ val value = {
+ val chooses = collectChooses(s.toExpr)
+ val chooseCost = chooses.foldLeft(0)((i, c) => i + (1000 * math.pow(2, c.vars.size).toInt + formulaSize(c.pred)))
+
+ formulaSize(s.toExpr) + chooseCost
+ }
+}
+
+case class ProblemCost(p: Problem) extends AOCost {
+ val value = math.pow(2, p.xs.size).toInt + formulaSize(p.phi)
+}
diff --git a/src/main/scala/leon/synthesis/DerivationTree.scala b/src/main/scala/leon/synthesis/DerivationTree.scala
index eae0104f4..0bf44b00e 100644
--- a/src/main/scala/leon/synthesis/DerivationTree.scala
+++ b/src/main/scala/leon/synthesis/DerivationTree.scala
@@ -1,6 +1,7 @@
package leon
package synthesis
+/*
class DerivationTree(root: RootTask) {
private[this] var _nextID = 0
@@ -60,3 +61,4 @@ class DerivationTree(root: RootTask) {
}
}
+*/
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 05b35b83f..928d7e31c 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -7,10 +7,10 @@ import heuristics._
object Heuristics {
def all = Set[Synthesizer => Rule](
- new IntInduction(_)
+ new IntInduction(_),
//new OptimisticInjection(_),
//new SelectiveInlining(_),
-// new ADTInduction(_)
+ new ADTInduction(_)
)
}
@@ -35,14 +35,16 @@ object HeuristicStep {
}
def apply(synth: Synthesizer, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleMultiSteps(subProblems, Nil, onSuccess.andThen(verifyPre(synth, problem)))
+ new RuleApplication(subProblems.size, onSuccess.andThen(verifyPre(synth, problem))) {
+ def apply() = RuleDecomposed(subProblems, onSuccess)
+ }
}
}
-object HeuristicOneStep {
+object HeuristicFastStep {
def apply(synth: Synthesizer, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleAlternatives(Set(HeuristicStep(synth, problem, subProblems, onSuccess)))
+ RuleResult(List(HeuristicStep(synth, problem, subProblems, onSuccess)))
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index ea4271b45..8602b74fb 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -26,32 +26,43 @@ object Rules {
)
}
-sealed abstract class RuleResult
-case class RuleSuccess(solution: Solution) extends RuleResult
-case class RuleAlternatives(steps: Traversable[RuleMultiSteps]) extends RuleResult
+case class RuleResult(alternatives: Traversable[RuleApplication])
+object RuleInapplicable extends RuleResult(List())
-case class RuleMultiSteps(subProblems: List[Problem],
- interSteps: List[List[Solution] => List[Problem]],
- onSuccess: List[Solution] => (Solution, Boolean))
+abstract class RuleApplication(val subProblemsCount: Int,
+ val onSuccess: List[Solution] => (Solution, Boolean)) {
-object RuleInapplicable {
- def apply() = RuleAlternatives(Seq())
+ def apply(): RuleApplicationResult
}
-object RuleStep {
- def apply(subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleMultiSteps(subProblems, Nil, onSuccess.andThen((_, true)))
+sealed abstract class RuleApplicationResult
+case class RuleSuccess(solution: Solution) extends RuleApplicationResult
+case class RuleDecomposed(sub: List[Problem], onSuccess: List[Solution] => (Solution, Boolean)) extends RuleApplicationResult
+
+object RuleFastApplication {
+ def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
+ new RuleApplication(sub.size, ls => (onSuccess(ls), true)) {
+ def apply() = RuleDecomposed(sub, onSuccess)
+ }
+ }
+}
+
+object RuleFastStep {
+ def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
+ RuleResult(List(RuleFastApplication(sub, onSuccess)))
}
}
-object RuleOneStep {
- def apply(subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleAlternatives(Set(RuleStep(subProblems, onSuccess)))
+object RuleFastSuccess {
+ def apply(solution: Solution) = {
+ RuleResult(List(new RuleApplication(0, ls => (solution, true)) {
+ def apply() = RuleSuccess(solution)
+ }))
}
}
abstract class Rule(val name: String, val synth: Synthesizer, val priority: Priority) {
- def applyOn(task: Task): RuleResult
+ def attemptToApplyOn(problem: Problem): RuleResult
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 309addbaf..255d7fd10 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -4,13 +4,14 @@ package synthesis
import leon.purescala.Trees._
import leon.purescala.Definitions._
import leon.purescala.TreeOps._
+import aographs._
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
-class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
+class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) extends AOSolution {
override def toString = "⟨ "+pre+" | "+defs.mkString(" ")+" "+term+" ⟩"
- lazy val complexity: AbsSolComplexity = new SolComplexity(this)
+ val cost: AOCost = null
def toExpr = {
val result = if (pre == BooleanLiteral(true)) {
@@ -47,6 +48,10 @@ object Solution {
new Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(id => simplestValue(id.getType))))
}
+ def simplest: Solution = {
+ new Solution(BooleanLiteral(true), Set(), BooleanLiteral(true))
+ }
+
def none: Solution = {
throw new Exception("Unexpected failure to construct solution")
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index d88d3e898..5b95fa9f5 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -25,105 +25,93 @@ class Synthesizer(val reporter: Reporter,
val rules = ruleConstructors.map(_.apply(this))
- var derivationCounter = 1;
-
- val rootTask: RootTask = new RootTask(this, problem)
-
- val workList = new PriorityQueue[Task]()
-
- def bestSolutionSoFar(): Solution = {
- rootTask.solution.getOrElse(worstSolution)
- }
-
- val worstSolution = Solution.choose(problem)
-
var continue = true
def synthesize(): Solution = {
- continue = true
- workList.clear()
- workList += rootTask
-
- val ts = System.currentTimeMillis
-
- def currentDurationMs = System.currentTimeMillis-ts
-
- def timeoutExpired(): Boolean = {
- timeoutMs match {
- case Some(t) if currentDurationMs/1000 > t => true
- case _ => false
- }
- }
val sigINT = new Signal("INT")
var oldHandler: SignalHandler = null
oldHandler = Signal.handle(sigINT, new SignalHandler {
def handle(sig: Signal) {
reporter.info("Aborting...")
- continue = false;
+ continue = false
Signal.handle(sigINT, oldHandler)
}
})
- while (!workList.isEmpty && continue) {
- val task = workList.dequeue()
+ /*
+ if (generateDerivationTrees) {
+ val deriv = new DerivationTree(rootTask)
+ deriv.toDotFile("derivation"+derivationCounter+".dot")
+ derivationCounter += 1
+ }
+ */
- val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root"))
+ val search = new AOSearch(problem, rules)
- if (!(firstOnly && (task.parent ne null) && task.parent.isSolvedFor(task.problem))) {
- val subProblems = task.run()
+ val res = search.search
- if (task.minComplexity <= bestSolutionSoFar.complexity) {
- if (task.solution.isDefined || !subProblems.isEmpty) {
- if (task.solution.isDefined) {
- info(prefix+"Got: "+task.problem)
- info(prefix+"Solved with: "+task.solution.get)
- } else {
- info(prefix+"Got: "+task.problem)
- info(prefix+"Decomposed into:")
- for(p <- subProblems) {
- info(prefix+" - "+p)
- }
- }
- }
- addProblems(task, subProblems)
- }
- }
+ println(res)
- if (timeoutExpired()) {
- warning("Timeout reached")
- continue = false
- }
- }
+ Solution.none
+ }
- if (!workList.isEmpty) {
- // We flush the worklist by solving everything with chooses, that should
- // rebuild a partial solution
- while (!workList.isEmpty) {
- val t = workList.dequeue()
- if (t.parent ne null) {
- t.parent.partlySolvedBy(t, Solution.choose(t.problem))
- }
- }
- }
+ import aographs._
- info("Finished in "+currentDurationMs+"ms")
+ abstract class Task extends AOTask[Solution]
+ case class TaskRunRule(problem: Problem, rule: Rule, app: RuleApplication) extends Task {
+ val subSols = (1 to app.subProblemsCount).map {i => Solution.simplest }.toList
+ val simpleSol = app.onSuccess(subSols)
- if (generateDerivationTrees) {
- val deriv = new DerivationTree(rootTask)
- deriv.toDotFile("derivation"+derivationCounter+".dot")
- derivationCounter += 1
+ def cost = SolutionCost(simpleSol._1)
+
+ def composeSolution(sols: List[Solution]): Solution = {
+ app.onSuccess(sols)._1
}
+ }
- bestSolutionSoFar()
+ case class TaskTryRules(p: Problem) extends Task {
+ def cost = ProblemCost(p)
+
+ def composeSolution(sols: List[Solution]): Solution = {
+ sys.error("Should not be called")
+ }
}
- def addProblems(task: Task, problems: Traversable[Problem]) {
- // Check if solving this task has the slightest chance of improving the
- // current solution
- for (p <- problems; rule <- rules) yield {
- workList += new Task(this, task, p, rule)
+ class AOSearch(problem: Problem, rules: Set[Rule]) extends AndOrGraphSearch[Task, Solution](new AndOrGraph(TaskTryRules(problem))) {
+ def processLeaf(l: g.Leaf) = {
+ l.task match {
+ case t: TaskTryRules =>
+ val sub = rules.flatMap ( r => r.attemptToApplyOn(t.p).alternatives.map(TaskRunRule(t.p, r, _)) )
+
+ if (!sub.isEmpty) {
+ Expanded(sub.toList)
+ } else {
+ ExpandFailure
+ }
+
+ case t: TaskRunRule=>
+ val prefix = "[%-20s] ".format(Option(t.rule))
+
+ t.app.apply() match {
+ case RuleSuccess(sol) =>
+ info(prefix+"Got: "+t.problem)
+ info(prefix+"Solved with: "+sol)
+
+ ExpandSuccess(sol)
+ case RuleDecomposed(sub, onSuccess) =>
+ info(prefix+"Got: "+t.problem)
+ info(prefix+"Decomposed into:")
+ for(p <- sub) {
+ info(prefix+" - "+p)
+ }
+
+ Expanded(sub.map(TaskTryRules(_)))
+ }
+ }
}
}
}
+
+
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 260745880..e2d8d65fc 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -1,6 +1,7 @@
package leon
package synthesis
+/*
class Task(synth: Synthesizer,
val parent: Task,
val problem: Problem,
@@ -139,3 +140,4 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
}
}
}
+*/
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 1c2769402..30cbe5bfd 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -10,9 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80) with Heuristic {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val candidates = p.as.collect {
case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
}
@@ -104,6 +102,6 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
}
}
- RuleAlternatives(steps.flatten)
+ RuleResult(steps.flatten)
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index a82eae8f7..f75e44e6d 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -10,9 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50) with Heuristic {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
p.as match {
case List(IsTyped(origId, Int32Type)) =>
val tpe = TupleType(p.xs.map(_.getType))
@@ -56,9 +54,9 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50)
Solution.none
}
- HeuristicOneStep(synth, p, List(subBase, subGT, subLT), onSuccess)
+ HeuristicFastStep(synth, p, List(subBase, subGT, subLT), onSuccess)
case _ =>
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index 8f3e65195..85d5f34cc 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -10,9 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", synth, 50) with Heuristic {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val eqfuncalls = exprs.collect{
@@ -38,9 +36,9 @@ class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", syn
val sub = p.copy(phi = And(newExprs))
- HeuristicOneStep(synth, p, List(sub), forward)
+ HeuristicFastStep(synth, p, List(sub), forward)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 6ee4935f5..4fe3f764d 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -10,9 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth, 20) with Heuristic {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val eqfuncalls = exprs.collect{
@@ -38,9 +36,9 @@ class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth,
val sub = p.copy(phi = And(newExprs))
- HeuristicOneStep(synth, p, List(sub), forward)
+ HeuristicFastStep(synth, p, List(sub), forward)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 1cf0a71f1..bb4753752 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -7,9 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val xs = p.xs.toSet
val as = p.as.toSet
@@ -26,9 +24,9 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- RuleOneStep(List(sub), forward)
+ RuleFastStep(List(sub), forward)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 41236da02..39e987c25 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -10,9 +10,7 @@ import purescala.Extractors._
import purescala.Definitions._
class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
@@ -72,11 +70,11 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
}
- Some(RuleStep(subInfo.map(_._2).toList, onSuccess))
+ Some(RuleFastApplication(subInfo.map(_._2).toList, onSuccess))
case _ =>
None
}}.flatten
- RuleAlternatives(steps)
+ RuleResult(steps)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 29514b2b3..62436e04d 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -7,9 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
p.phi match {
case TopLevelAnds(exprs) =>
val xsSet = p.xs.toSet
@@ -18,17 +16,17 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- RuleSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
+ RuleFastSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
} else {
val sub = p.copy(c = And(p.c +: exprsA), phi = And(others))
- RuleOneStep(List(sub), forward)
+ RuleFastStep(List(sub), forward)
}
} else {
- RuleInapplicable()
+ RuleInapplicable
}
case _ =>
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 42d7e5095..44f0b7bad 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -7,8 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
+ def attemptToApplyOn(p: Problem): RuleResult = {
p.phi match {
case Or(o1 :: o2 :: _) =>
val sub1 = Problem(p.as, p.c, o1, p.xs)
@@ -19,9 +18,9 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
case _ => Solution.none
}
- RuleOneStep(List(sub1, sub2), onSuccess)
+ RuleFastStep(List(sub1, sub2), onSuccess)
case _ =>
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 14bf62a17..80decb7fb 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -10,9 +10,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
var generators = Map[TypeTree, Generator]()
@@ -192,7 +190,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
mapping += c -> substAll(mapping, e)
}
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
+ result = Some(RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
case _ =>
synth.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
@@ -213,6 +211,6 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
unrolings += 1
} while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && synth.continue)
- result.getOrElse(RuleInapplicable())
+ result.getOrElse(RuleInapplicable)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 8cd63ef80..76330d820 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -9,9 +9,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val candidates = p.as.groupBy(_.getType).map(_._2.toList).filter {
case List(a1, a2) =>
val toValEQ = Implies(p.c, Equals(Variable(a1), Variable(a2)))
@@ -50,11 +48,11 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
Solution.none
}
- Some(RuleStep(List(sub1, sub2), onSuccess))
+ Some(RuleFastApplication(List(sub1, sub2), onSuccess))
case _ =>
None
}).flatten
- RuleAlternatives(steps)
+ RuleResult(steps)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index ddb4c7b6d..ae2284294 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -8,23 +8,21 @@ import purescala.TreeOps._
import purescala.Extractors._
class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
if (p.as.isEmpty) {
val tpe = TupleType(p.xs.map(_.getType))
synth.solver.solveSAT(p.phi) match {
case (Some(true), model) =>
- RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
+ RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
case (Some(false), model) =>
- RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
+ RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
case _ =>
- RuleInapplicable()
+ RuleInapplicable
}
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index a8af1d203..6b94025b6 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -12,9 +12,7 @@ import LinearEquations.elimVariable
import ArithmeticNormalization.simplify
class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth, 300) {
- def applyOn(task: Task): RuleResult = {
-
- val problem = task.problem
+ def attemptToApplyOn(problem: Problem): RuleResult = {
val TopLevelAnds(exprs) = problem.phi
@@ -43,7 +41,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
allOthers = allOthers ++ candidates
optionNormalizedEq match {
- case None => RuleInapplicable()
+ case None => RuleInapplicable
case Some(normalizedEq0) => {
val eqas = problem.as.toSet.intersect(vars)
@@ -62,7 +60,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
case _ => Solution.none
}
- RuleOneStep(List(newProblem), onSuccess)
+ RuleFastStep(List(newProblem), onSuccess)
} else {
val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
@@ -105,7 +103,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
case _ => Solution.none
}
- RuleOneStep(List(newProblem), onSuccess)
+ RuleFastStep(List(newProblem), onSuccess)
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 80b340595..5f70d9ac5 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -12,8 +12,7 @@ import LinearEquations.elimVariable
import ArithmeticNormalization.simplify
class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities", synth, 300) {
- def applyOn(task: Task): RuleResult = {
- val problem = task.problem
+ def attemptToApplyOn(problem: Problem): RuleResult = {
val TopLevelAnds(exprs) = problem.phi
//assume that we only have inequalities
@@ -31,7 +30,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
val ineqVars = lhsSides.foldLeft(Set[Identifier]())((acc, lhs) => acc ++ variablesOf(lhs))
val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains(_))
- if(candidateVars.isEmpty) RuleInapplicable() else {
+ if(candidateVars.isEmpty) RuleInapplicable else {
val processedVar = candidateVars.head
val otherVars: List[Identifier] = problem.xs.filterNot(_ == processedVar)
@@ -96,7 +95,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
val pre = And(
for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds)
yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc))))
- RuleSuccess(Solution(pre, Set(), witness))
+ RuleFastSuccess(Solution(pre, Set(), witness))
} else {
val L = GCD.lcm((upperBounds ::: lowerBounds).map(_._2))
val newUpperBounds: List[Expr] = upperBounds.map{case (bound, coef) => Times(IntLiteral(L/coef), bound)}
@@ -161,7 +160,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
case _ => Solution.none
}
- RuleOneStep(List(subProblem), onSuccess)
+ RuleFastStep(List(subProblem), onSuccess)
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 40f7da864..50b3aa9e6 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -7,10 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
- def applyOn(task: Task): RuleResult = {
-
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val candidates = exprs.collect {
@@ -38,9 +35,9 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
case _ => Solution.none
}
- RuleOneStep(List(newProblem), onSuccess)
+ RuleFastStep(List(newProblem), onSuccess)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 390f41c39..0f3fd8607 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -8,9 +8,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 150) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
if (!p.as.isEmpty && !p.xs.isEmpty) {
val xss = p.xs.toSet
val ass = p.as.toSet
@@ -39,28 +37,28 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
case (Some(false), _) =>
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+ result = Some(RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
case _ =>
- result = Some(RuleInapplicable())
+ result = Some(RuleInapplicable)
}
case (Some(false), _) =>
if (predicates.isEmpty) {
- result = Some(RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
+ result = Some(RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
- result = Some(RuleInapplicable())
+ result = Some(RuleInapplicable)
}
case _ =>
- result = Some(RuleInapplicable())
+ result = Some(RuleInapplicable)
}
i += 1
}
- result.getOrElse(RuleInapplicable())
+ result.getOrElse(RuleInapplicable)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 021a68204..3c0dc96b7 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -7,8 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 100) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
+ def attemptToApplyOn(p: Problem): RuleResult = {
val unconstr = p.xs.toSet -- variablesOf(p.phi)
if (!unconstr.isEmpty) {
@@ -21,9 +20,9 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
Solution.none
}
- RuleOneStep(List(sub), onSuccess)
+ RuleFastStep(List(sub), onSuccess)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index e1412874f..f7aec9959 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -9,9 +9,7 @@ import purescala.Extractors._
object Unification {
class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 200) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val (toRemove, toAdd) = exprs.collect {
@@ -29,17 +27,15 @@ object Unification {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- RuleOneStep(List(sub), forward)
+ RuleFastStep(List(sub), forward)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 200) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
+ def attemptToApplyOn(p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val isImpossible = exprs.exists {
@@ -54,9 +50,9 @@ object Unification {
if (isImpossible) {
val tpe = TupleType(p.xs.map(_.getType))
- RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
+ RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 482d594a1..18f633348 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -7,16 +7,15 @@ import purescala.TreeOps._
import purescala.Extractors._
class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 100) {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
+ def attemptToApplyOn(p: Problem): RuleResult = {
val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.c)
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
- RuleOneStep(List(sub), forward)
+ RuleFastStep(List(sub), forward)
} else {
- RuleInapplicable()
+ RuleInapplicable
}
}
}
--
GitLab