From 9c8b6e54a05d58dfd6c3e4e6d85d2d806ae2c2e4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 19 Nov 2012 13:49:08 +0100
Subject: [PATCH] Rules can (and should) have multiple application alternatives
---
.../scala/leon/synthesis/Heuristics.scala | 11 +-
src/main/scala/leon/synthesis/Rules.scala | 17 ++-
.../scala/leon/synthesis/Synthesizer.scala | 2 +-
src/main/scala/leon/synthesis/Task.scala | 116 +++++++++---------
.../synthesis/heuristics/ADTInduction.scala | 6 +-
.../synthesis/heuristics/IntInduction.scala | 2 +-
.../heuristics/OptimisticInjection.scala | 2 +-
.../heuristics/SelectiveInlining.scala | 2 +-
.../scala/leon/synthesis/rules/ADTDual.scala | 2 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
.../scala/leon/synthesis/rules/Assert.scala | 2 +-
.../leon/synthesis/rules/CaseSplit.scala | 2 +-
.../leon/synthesis/rules/EqualitySplit.scala | 2 +-
.../synthesis/rules/IntegerEquation.scala | 4 +-
.../synthesis/rules/IntegerInequalities.scala | 2 +-
.../scala/leon/synthesis/rules/OnePoint.scala | 2 +-
.../synthesis/rules/UnconstrainedOutput.scala | 2 +-
.../leon/synthesis/rules/Unification.scala | 2 +-
.../leon/synthesis/rules/UnusedInput.scala | 2 +-
testcases/synthesis/BinaryTree.scala | 8 ++
20 files changed, 105 insertions(+), 85 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index be50b59aa..05b35b83f 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(_)
)
}
@@ -40,6 +40,9 @@ object HeuristicStep {
}
-
-
+object HeuristicOneStep {
+ def apply(synth: Synthesizer, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ RuleAlternatives(Set(HeuristicStep(synth, problem, subProblems, onSuccess)))
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 8db62a914..f6b957d1d 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -20,17 +20,20 @@ object Rules {
new EqualitySplit(_),
new CEGIS(_),
new Assert(_),
-// new ADTSplit(_),
- new IntegerEquation(_)
+ new ADTSplit(_),
+ new IntegerEquation(_),
+ new IntegerInequalities(_)
)
}
sealed abstract class RuleResult
case object RuleInapplicable extends RuleResult
case class RuleSuccess(solution: Solution) extends RuleResult
+case class RuleAlternatives(steps: Set[RuleMultiSteps]) extends RuleResult
+
case class RuleMultiSteps(subProblems: List[Problem],
- steps: List[List[Solution] => List[Problem]],
- onSuccess: List[Solution] => (Solution, Boolean)) extends RuleResult
+ interSteps: List[List[Solution] => List[Problem]],
+ onSuccess: List[Solution] => (Solution, Boolean))
object RuleStep {
def apply(subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
@@ -38,6 +41,12 @@ object RuleStep {
}
}
+object RuleOneStep {
+ def apply(subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ RuleAlternatives(Set(RuleStep(subProblems, onSuccess)))
+ }
+}
+
abstract class Rule(val name: String, val synth: Synthesizer, val priority: Priority) {
def applyOn(task: Task): RuleResult
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index f33ffe5c9..d88d3e898 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -70,7 +70,7 @@ class Synthesizer(val reporter: Reporter,
val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root"))
- if (!(firstOnly && (task.parent ne null) && task.parent.isSolved(task.problem))) {
+ if (!(firstOnly && (task.parent ne null) && task.parent.isSolvedFor(task.problem))) {
val subProblems = task.run()
if (task.minComplexity <= bestSolutionSoFar.complexity) {
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index a9d18d5b5..97b4a9b03 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -24,8 +24,9 @@ class Task(synth: Synthesizer,
}
}
-
var solution: Option[Solution] = None
+ var alternatives = Set[RuleApplication]()
+
var minComplexity: AbsSolComplexity = new FixedSolComplexity(0)
class TaskStep(val subProblems: List[Problem]) {
@@ -34,52 +35,64 @@ class Task(synth: Synthesizer,
var failures = Set[Rule]()
}
- var steps: List[TaskStep] = Nil
- var nextSteps: List[List[Solution] => List[Problem]] = Nil
- var onSuccess: List[Solution] => (Solution, Boolean) = _
-
- def currentStep = steps.head
-
- def isSolved(problem: Problem): Boolean = parent.isSolved(this.problem) || (currentStep.subSolutions contains problem)
-
- def partlySolvedBy(t: Task, s: Solution) {
- if (isBetterSolutionThan(s, currentStep.subSolutions.get(t.problem))) {
- currentStep.subSolutions += t.problem -> s
- currentStep.subSolvers += t.problem -> t
-
- if (currentStep.subSolutions.size == currentStep.subProblems.size) {
- val solutions = currentStep.subProblems map currentStep.subSolutions
-
- if (!nextSteps.isEmpty) {
- val newProblems = nextSteps.head.apply(solutions)
- nextSteps = nextSteps.tail
-
- synth.addProblems(this, newProblems)
-
- steps = new TaskStep(newProblems) :: steps
- } else {
- onSuccess(solutions) match {
- case (s, true) =>
- solution = Some(s)
-
- parent.partlySolvedBy(this, solution.get)
- case _ =>
- // solution is there, but it is incomplete (precondition not strongest)
- //parent.partlySolvedBy(this, Solution.choose(problem))
+ class RuleApplication(
+ val initProblems: List[Problem],
+ val allNextSteps: List[List[Solution] => List[Problem]],
+ val onSuccess: List[Solution] => (Solution, Boolean)) {
+
+ var allSteps = List(new TaskStep(initProblems))
+ var nextSteps = allNextSteps
+ def currentStep = allSteps.head
+
+ def isSolvedFor(p: Problem) = allSteps.exists(_.subSolutions contains p)
+
+ def partlySolvedBy(t: Task, s: Solution) {
+ if (currentStep.subProblems.contains(t.problem)) {
+ if (isBetterSolutionThan(s, currentStep.subSolutions.get(t.problem))) {
+ currentStep.subSolutions += t.problem -> s
+ currentStep.subSolvers += t.problem -> t
+
+ if (currentStep.subSolutions.size == currentStep.subProblems.size) {
+ val solutions = currentStep.subProblems map currentStep.subSolutions
+
+ if (!nextSteps.isEmpty) {
+ // Advance to the next step
+ val newProblems = nextSteps.head.apply(solutions)
+ nextSteps = nextSteps.tail
+
+ synth.addProblems(Task.this, newProblems)
+
+ allSteps = new TaskStep(newProblems) :: allSteps
+ } else {
+ onSuccess(solutions) match {
+ case (s, true) =>
+ solution = Some(s)
+
+ parent.partlySolvedBy(Task.this, solution.get)
+ case _ =>
+ // solution is there, but it is incomplete (precondition not strongest)
+ //parent.partlySolvedBy(this, Solution.choose(problem))
+ }
+ }
}
}
}
}
+
+ val minComplexity: AbsSolComplexity = {
+ val simplestSubSolutions = allNextSteps.foldLeft(initProblems.map(Solution.basic(_))){
+ (sols, step) => step(sols).map(Solution.basic(_))
+ }
+ val simplestSolution = onSuccess(simplestSubSolutions)._1
+ new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
+ }
}
- def unsolvedBy(t: Task) {
- currentStep.failures += t.rule
+ // Is this subproblem already fixed?
+ def isSolvedFor(problem: Problem): Boolean = parent.isSolvedFor(this.problem) || (alternatives.exists(_.isSolvedFor(problem)))
- if (currentStep.failures.size == synth.rules.size) {
- // We might want to report unsolved instead of solvedByChoose, depending
- // on the cases
- //parent.partlySolvedBy(this, Solution.choose(problem))
- }
+ def partlySolvedBy(t: Task, s: Solution) {
+ alternatives.foreach(_.partlySolvedBy(t, s))
}
def run(): List[Problem] = {
@@ -91,22 +104,11 @@ class Task(synth: Synthesizer,
Nil
- case RuleMultiSteps(subProblems, interSteps, onSuccess) =>
- this.steps = new TaskStep(subProblems) :: Nil
- this.nextSteps = interSteps
- this.onSuccess = onSuccess
-
- // Compute simplest solution possible to evaluate whether this rule is worth it
- // To each problem we assign the most basic solution, fold on all inner
- // steps, and then reconstruct final solution
- val simplestSubSolutions = interSteps.foldLeft(subProblems.map(Solution.basic(_))){ (sols, step) => step(sols).map(Solution.basic(_)) }
- val simplestSolution = onSuccess(simplestSubSolutions)._1
- minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
-
- subProblems
+ case RuleAlternatives(steps) =>
+ this.alternatives = steps.map( step => new RuleApplication(step.subProblems, step.interSteps, step.onSuccess) )
+ this.alternatives.flatMap(_.initProblems).toList
case RuleInapplicable =>
- parent.unsolvedBy(this)
Nil
}
}
@@ -121,7 +123,7 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
List(problem)
}
- override def isSolved(problem: Problem) = solver.isDefined
+ override def isSolvedFor(problem: Problem) = solver.isDefined
override def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, solution)) {
@@ -129,8 +131,4 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
solver = Some(t)
}
}
-
- override def unsolvedBy(t: Task) {
- }
-
}
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index d321a61db..064163d0b 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -41,6 +41,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
val newFun = new FunDef(FreshIdentifier("rec", true), resType, VarDecl(inductOn, inductOn.getType) +: residualArgDefs)
val innerPhi = substAll(residualMap + (origId -> Variable(inductOn)), p.phi)
+ val innerPC = substAll(residualMap + (origId -> Variable(inductOn)), p.c)
val subProblemsInfo = for (dcd <- cd.knownDescendents) yield dcd match {
case ccd : CaseClassDef =>
@@ -64,10 +65,11 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
}).flatten
val subPhi = substAll(Map(inductOn -> CaseClass(ccd, newIds.map(Variable(_)))), innerPhi)
+ val subPC = substAll(Map(inductOn -> CaseClass(ccd, newIds.map(Variable(_)))), innerPC)
val subPre = CaseClassInstanceOf(ccd, Variable(origId))
- val subProblem = Problem(inputs ::: residualArgs, And(p.c :: postFs), subPhi, p.xs)
+ val subProblem = Problem(inputs ::: residualArgs, And(subPC :: postFs), subPhi, p.xs)
(subProblem, subPre, ccd, newIds, recCalls)
case _ =>
@@ -96,7 +98,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, p.as.map(Variable(_))))
}
- HeuristicStep(synth, p, subProblemsInfo.map(_._1).toList, onSuccess)
+ HeuristicOneStep(synth, p, subProblemsInfo.map(_._1).toList, onSuccess)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index 2bf690f8c..c1000f824 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -56,7 +56,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50)
Solution.none
}
- HeuristicStep(synth, p, List(subBase, subGT, subLT), onSuccess)
+ HeuristicOneStep(synth, p, List(subBase, subGT, subLT), onSuccess)
case _ =>
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index 9c76475e4..cb6682fcc 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -38,7 +38,7 @@ class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", syn
val sub = p.copy(phi = And(newExprs))
- HeuristicStep(synth, p, List(sub), forward)
+ HeuristicOneStep(synth, p, List(sub), forward)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 04d38f5fe..60c066e5f 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -38,7 +38,7 @@ class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth,
val sub = p.copy(phi = And(newExprs))
- HeuristicStep(synth, p, List(sub), forward)
+ HeuristicOneStep(synth, p, List(sub), forward)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 5cf2bdb3b..37d6cf63f 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -26,7 +26,7 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- RuleStep(List(sub), forward)
+ RuleOneStep(List(sub), forward)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index f4a90086a..6d43a4a52 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -72,7 +72,7 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
}
- HeuristicStep(synth, p, subInfo.map(_._2).toList, onSuccess)
+ RuleOneStep(subInfo.map(_._2).toList, onSuccess)
case _ =>
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index cfd5f5a92..814632bce 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -22,7 +22,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
} else {
val sub = p.copy(c = And(p.c +: exprsA), phi = And(others))
- RuleStep(List(sub), forward)
+ RuleOneStep(List(sub), forward)
}
} else {
RuleInapplicable
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index a99b7a361..dcd7e6835 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -19,7 +19,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
case _ => Solution.none
}
- RuleStep(List(sub1, sub2), onSuccess)
+ RuleOneStep(List(sub1, sub2), onSuccess)
case _ =>
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 04d4f8bf7..fe0214362 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -50,7 +50,7 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
Solution.none
}
- RuleStep(List(sub1, sub2), onSuccess)
+ RuleOneStep(List(sub1, sub2), onSuccess)
case _ =>
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 4ea9e93f5..bb2005f9d 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -62,7 +62,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
case _ => Solution.none
}
- RuleStep(List(newProblem), onSuccess)
+ RuleOneStep(List(newProblem), onSuccess)
} else {
val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
@@ -105,7 +105,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
case _ => Solution.none
}
- RuleStep(List(newProblem), onSuccess)
+ RuleOneStep(List(newProblem), onSuccess)
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index e15291969..760891e0c 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -161,7 +161,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
case _ => Solution.none
}
- RuleStep(List(subProblem), onSuccess)
+ RuleOneStep(List(subProblem), onSuccess)
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index af047f3cb..1ee39b2d1 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -38,7 +38,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
case _ => Solution.none
}
- RuleStep(List(newProblem), onSuccess)
+ RuleOneStep(List(newProblem), onSuccess)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 0a24dff40..a804d9cfc 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -21,7 +21,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
Solution.none
}
- RuleStep(List(sub), onSuccess)
+ RuleOneStep(List(sub), onSuccess)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 7817d63d9..90a5c8741 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -29,7 +29,7 @@ object Unification {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- RuleStep(List(sub), forward)
+ RuleOneStep(List(sub), forward)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index cc9c35d6d..e9e0c18d6 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -14,7 +14,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 100) {
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
- RuleStep(List(sub), forward)
+ RuleOneStep(List(sub), forward)
} else {
RuleInapplicable
}
diff --git a/testcases/synthesis/BinaryTree.scala b/testcases/synthesis/BinaryTree.scala
index 02b4030fe..7409a2745 100644
--- a/testcases/synthesis/BinaryTree.scala
+++ b/testcases/synthesis/BinaryTree.scala
@@ -15,4 +15,12 @@ object BinaryTree {
def delete(in : Tree, v : Int) = choose { (out : Tree) =>
content(out) == (content(in) -- Set(v))
}
+
+ def deleteSubProblem(left : Tree, leftR: Tree, value: Int, rightRleft: Tree, rightRvalue: Int, rightRright: Tree, rightR: Tree, right: Tree, toRemove : Int) = choose { (out : Tree) =>
+ content(out) == (content(Node(left, value, right)) -- Set(toRemove)) && content(leftR) == (content(left) -- Set(toRemove)) && rightR == Node(rightRleft, rightRvalue, rightRright) && content(Node(rightRleft, rightRvalue, rightRright)) == (content(right) -- Set(toRemove)) && value == toRemove
+ }
+
+ def deleteSubProblem2(left : Tree, leftR: Tree, value: Int, rightRleft: Tree, rightRvalue: Int, rightRright: Tree, right: Tree, toRemove : Int) = choose { (out : Tree) =>
+ content(out) == (content(Node(left, value, right)) -- Set(toRemove)) && content(leftR) == (content(left) -- Set(toRemove)) && content(Node(rightRleft, rightRvalue, rightRright)) == (content(right) -- Set(toRemove)) && value == toRemove
+ }
}
--
GitLab