diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index be50b59aadef480e27846f447fb45c0585710bf7..05b35b83f34f19f713898a1676da7eae6f849685 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 8db62a9149b14b45c3549a7f91f239722a7ae2ce..f6b957d1df716e33e349b96c2b535e92263d7010 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 f33ffe5c9f6edcdad631e70cbcf0f6f45a0c4cae..d88d3e8986950ab1be68c44e7d723ebbd224c638 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 a9d18d5b5d10aa90e16d623b674bdd75c88548a7..97b4a9b036b93b03372ab865eafe86b224b2ddec 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 d321a61db981784823d6a024d64547aa5554e9ba..064163d0b1ab085dbf722f46be15bdc23513ed6d 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 2bf690f8c7af7ba8efb6a5fe8987aa890433f307..c1000f82486286e42eb57f12df4087d24b6e5b5c 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 9c76475e4d8de3c0c972f3978b9a24efadae7bdf..cb6682fcc0c7b7be76b3117dbd2063fca4726f8d 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 04d38f5fe0431e4e752e83c3fcba29dfddf8b9f8..60c066e5f0366fa0d96efcc27d175d6177d3ddf2 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 5cf2bdb3b9f1647ffe9a0fed3d3919862e5bc78b..37d6cf63fbf52f77b688cec17a7c5e58b3f0bd32 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 f4a90086aba4f603215dbc2448e35794559a08e5..6d43a4a52d3edeb680eb26a08d70bd02e340fb64 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 cfd5f5a92a1be2e73e6f36c8be8e51cf6a71e9bf..814632bce81fc96aeb0009e753af5577aeefad44 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 a99b7a361dced3e19d8e79703d9cb90ba2483779..dcd7e6835b2c93abe6ed45f24f9c7aed87e3c80e 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 04d4f8bf70128a6c6aa8a95a1c43fa35ac9433a9..fe0214362caf0d3ccecf96692b0ce7c19b33d722 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 4ea9e93f579588cae5911f49ae6e0ccf2ef505a9..bb2005f9d359b219a22d467af059b24f91b744e5 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 e15291969b04171a1776856bd60889f28bde9b5b..760891e0cdd195a74d509749e7b71c40386846ea 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 af047f3cb4bf7952ef629bd530cc1c2c3e6830e1..1ee39b2d1c1b4fbd42d7d9b80de0a15b22f09dd6 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 0a24dff40cb757b288eea1fb4cb83b846c73507a..a804d9cfc4d8456b0bf14ed682cb6f26e993226f 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 7817d63d93bae7ff59bbdb00455ce9cc29aecc7c..90a5c8741887c9d764effe77d37d09e83ca7dc7c 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 cc9c35d6def0a11d37b5663642a7e19d411904f7..e9e0c18d6b780ac3f43153fe07b81d8e909eb361 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 02b4030fe4caa71f88260264e3376e7c04e9c417..7409a2745ce8375e20e32b9b63d1a32562208ba0 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
+ }
}