From b986717b60e6a713b5842ec6d50e924505c53065 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 3 Jan 2013 18:29:42 +0100
Subject: [PATCH] Handle problem of costs=0 in case of missing SolutionBuilder,
requires passing more info to RuleInstantiation, but it is useful anyway
---
src/main/scala/leon/synthesis/CostModel.scala | 9 +++++++--
src/main/scala/leon/synthesis/Heuristics.scala | 4 ++--
src/main/scala/leon/synthesis/ParallelSearch.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 10 +++++-----
src/main/scala/leon/synthesis/SimpleSearch.scala | 10 +++++++---
.../scala/leon/synthesis/heuristics/ADTInduction.scala | 2 +-
.../scala/leon/synthesis/heuristics/IntInduction.scala | 2 +-
.../synthesis/heuristics/OptimisticInjection.scala | 2 +-
.../leon/synthesis/heuristics/SelectiveInlining.scala | 2 +-
src/main/scala/leon/synthesis/rules/ADTDual.scala | 2 +-
src/main/scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
src/main/scala/leon/synthesis/rules/Assert.scala | 4 ++--
src/main/scala/leon/synthesis/rules/CaseSplit.scala | 2 +-
src/main/scala/leon/synthesis/rules/Cegis.scala | 2 +-
.../scala/leon/synthesis/rules/Disunification.scala | 2 +-
.../scala/leon/synthesis/rules/EqualitySplit.scala | 2 +-
src/main/scala/leon/synthesis/rules/Ground.scala | 4 ++--
.../scala/leon/synthesis/rules/IntegerEquation.scala | 4 ++--
.../leon/synthesis/rules/IntegerInequalities.scala | 4 ++--
src/main/scala/leon/synthesis/rules/OnePoint.scala | 2 +-
.../scala/leon/synthesis/rules/OptimisticGround.scala | 4 ++--
.../leon/synthesis/rules/UnconstrainedOutput.scala | 2 +-
src/main/scala/leon/synthesis/rules/Unification.scala | 4 ++--
src/main/scala/leon/synthesis/rules/UnusedInput.scala | 2 +-
24 files changed, 47 insertions(+), 38 deletions(-)
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index 11d035724..04892e750 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -11,11 +11,16 @@ abstract class CostModel(val name: String) {
def solutionCost(s: Solution): Cost
def problemCost(p: Problem): Cost
- def ruleAppCost(r: Rule, app: RuleInstantiation): Cost = new Cost {
+ def ruleAppCost(app: RuleInstantiation): Cost = new Cost {
val subSols = (1 to app.onSuccess.arity).map {i => Solution.simplest }.toList
val simpleSol = app.onSuccess(subSols)
- val value = simpleSol.map(solutionCost(_).value).getOrElse(0)
+ val value = simpleSol match {
+ case Some(sol) =>
+ solutionCost(sol).value
+ case None =>
+ problemCost(app.problem).value
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index cc313e629..a80831ec4 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -37,14 +37,14 @@ object HeuristicInstantiation {
Some(s)
}
- def apply(problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
val builder = new SolutionBuilder(subProblems.size) {
def apply(sols: List[Solution]) = {
Some(onSuccess(sols))
}
}
- new RuleInstantiation(builder) {
+ new RuleInstantiation(problem, rule, builder) {
def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems)
}
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index f85917212..5ec24b47e 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -70,7 +70,7 @@ class ParallelSearch(synth: Synthesizer,
def expandOrTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskTryRules) = {
val sub = rules.flatMap { r =>
- r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _))
+ r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
}
if (!sub.isEmpty) {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 3d24a3c2d..0ea37eac2 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -44,7 +44,7 @@ object SolutionBuilder {
}
}
-abstract class RuleInstantiation(val onSuccess: SolutionBuilder) {
+abstract class RuleInstantiation(val problem: Problem, val rule: Rule, val onSuccess: SolutionBuilder) {
def apply(sctx: SynthesisContext): RuleApplicationResult
}
@@ -62,14 +62,14 @@ case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
case object RuleApplicationImpossible extends RuleApplicationResult
object RuleInstantiation {
- def immediateDecomp(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
- new RuleInstantiation(new SolutionCombiner(sub.size, onSuccess)) {
+ def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Solution) = {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, onSuccess)) {
def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
}
}
- def immediateSuccess(solution: Solution) = {
- new RuleInstantiation(new SolutionCombiner(0, ls => solution)) {
+ def immediateSuccess(problem: Problem, rule: Rule, solution: Solution) = {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(0, ls => solution)) {
def apply(sctx: SynthesisContext) = RuleSuccess(solution)
}
}
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index d2b658bb2..393177e77 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -3,7 +3,11 @@ package synthesis
import synthesis.search._
-case class TaskRunRule(problem: Problem, rule: Rule, app: RuleInstantiation) extends AOAndTask[Solution] {
+case class TaskRunRule(app: RuleInstantiation) extends AOAndTask[Solution] {
+
+ val problem = app.problem
+ val rule = app.rule
+
def composeSolution(sols: List[Solution]): Option[Solution] = {
app.onSuccess(sols)
}
@@ -18,7 +22,7 @@ case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
case class SearchCostModel(cm: CostModel) extends AOCostModel[TaskRunRule, TaskTryRules, Solution] {
def taskCost(t: AOTask[Solution]) = t match {
case ttr: TaskRunRule =>
- cm.ruleAppCost(ttr.rule, ttr.app)
+ cm.ruleAppCost(ttr.app)
case trr: TaskTryRules =>
cm.problemCost(trr.p)
}
@@ -59,7 +63,7 @@ class SimpleSearch(synth: Synthesizer,
}
def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
- val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _)) )
+ val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(_)) )
if (!sub.isEmpty) {
Expanded(sub.toList)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index adcbb72a2..4cb8f2285 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -97,7 +97,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, Variable(origId) :: oas.map(Variable(_))))
}
- Some(HeuristicInstantiation(p, subProblemsInfo.map(_._1).toList, onSuccess))
+ Some(HeuristicInstantiation(p, this, subProblemsInfo.map(_._1).toList, onSuccess))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index fdcc626c4..a882fe32b 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -54,7 +54,7 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
Solution.none
}
- Some(HeuristicInstantiation(p, List(subBase, subGT, subLT), onSuccess))
+ Some(HeuristicInstantiation(p, this, List(subBase, subGT, subLT), onSuccess))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index a3ecedd72..1a957e402 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -36,7 +36,7 @@ case object OptimisticInjection extends Rule("Opt. Injection") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, List(sub), forward))
+ Some(HeuristicInstantiation(p, this, List(sub), forward))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 8e91394f0..488df7355 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -36,7 +36,7 @@ case object SelectiveInlining extends Rule("Sel. Inlining") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, List(sub), forward))
+ Some(HeuristicInstantiation(p, this, List(sub), forward))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 6b6dac90f..f1811f073 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -24,7 +24,7 @@ case object ADTDual extends Rule("ADTDual") {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index e94abd7f1..4680ca40b 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -70,7 +70,7 @@ case object ADTSplit extends Rule("ADT Split.") {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
}
- Some(RuleInstantiation.immediateDecomp(subInfo.map(_._2).toList, onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, subInfo.map(_._2).toList, onSuccess))
case _ =>
None
}}.flatten
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 4522067b8..d45d08903 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -16,11 +16,11 @@ case object Assert extends Rule("Assert") {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- List(RuleInstantiation.immediateSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id)))))))
+ List(RuleInstantiation.immediateSuccess(p, this, Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id)))))))
} else {
val sub = p.copy(pc = And(p.pc +: exprsA), phi = And(others))
- List(RuleInstantiation.immediateDecomp(List(sub), {
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), {
case Solution(pre, defs, term) :: Nil => Solution(And(exprsA :+ pre), defs, term)
case _ => Solution.none
}))
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 3850b1d74..9b3e56315 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -34,7 +34,7 @@ case object CaseSplit extends Rule("Case-Split") {
Solution.none
}
- RuleInstantiation.immediateDecomp(subs, onSuccess)
+ RuleInstantiation.immediateDecomp(p, this, subs, onSuccess)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 8eafd160f..c7f84e483 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -124,7 +124,7 @@ case object CEGIS extends Rule("CEGIS") {
val (exprsA, others) = ands.partition(e => (variablesOf(e) & xsSet).isEmpty)
if (exprsA.isEmpty) {
- val res = new RuleInstantiation(SolutionBuilder.none) {
+ val res = new RuleInstantiation(p, this, SolutionBuilder.none) {
def apply(sctx: SynthesisContext) = {
var result: Option[RuleApplicationResult] = None
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 9ca48a9f6..4925f6000 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -26,7 +26,7 @@ object Disunification {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = Or((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index bad8bc4c4..603a48a08 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -48,7 +48,7 @@ case object EqualitySplit extends Rule("Eq. Split.") {
Solution.none
}
- Some(RuleInstantiation.immediateDecomp(List(sub1, sub2), onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess))
case _ =>
None
}).flatten
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 6aefe88a8..953ad5b56 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -16,10 +16,10 @@ case object Ground extends Rule("Ground") {
sctx.solver.solveSAT(p.phi) match {
case (Some(true), model) =>
val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
- Some(RuleInstantiation.immediateSuccess(sol))
+ Some(RuleInstantiation.immediateSuccess(p, this, sol))
case (Some(false), model) =>
val sol = Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))
- Some(RuleInstantiation.immediateSuccess(sol))
+ Some(RuleInstantiation.immediateSuccess(p, this, sol))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index eabbfce2e..f74e4478e 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -60,7 +60,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
} else {
val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
@@ -103,7 +103,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 21f9dced1..7fbc67fd6 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -131,7 +131,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val constraints: List[Expr] = for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds)
yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc)))
val pre = And(exprNotUsed ++ constraints)
- List(RuleInstantiation.immediateSuccess(Solution(pre, Set(), witness)))
+ List(RuleInstantiation.immediateSuccess(problem, this, Solution(pre, Set(), witness)))
} else {
val involvedVariables = (upperBounds++lowerBounds).foldLeft(Set[Identifier]())((acc, t) => {
@@ -200,7 +200,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(subProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(subProblem), onSuccess))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 24eee3336..7f4fae9da 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -35,7 +35,7 @@ case object OnePoint extends Rule("One-point") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(p, this, List(newProblem), onSuccess))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 460a83fe4..953afc7b2 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -38,7 +38,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
case (Some(false), _) =>
- result = Some(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+ result = Some(RuleInstantiation.immediateSuccess(p, this, Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
case _ =>
continue = false
@@ -47,7 +47,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
case (Some(false), _) =>
if (predicates.isEmpty) {
- result = Some(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
+ result = Some(RuleInstantiation.immediateSuccess(p, this, Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
continue = false
result = None
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 7c8d2de15..381f73f6b 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -20,7 +20,7 @@ case object UnconstrainedOutput extends Rule("Unconstr.Output") {
Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(sub), onSuccess))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 5c8151619..9b7ea4230 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -27,7 +27,7 @@ object Unification {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}
@@ -52,7 +52,7 @@ object Unification {
if (isImpossible) {
val tpe = TupleType(p.xs.map(_.getType))
- List(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
+ List(RuleInstantiation.immediateSuccess(p, this, Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 13ba585ab..b44ad3411 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -13,7 +13,7 @@ case object UnusedInput extends Rule("UnusedInput") {
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}
--
GitLab