diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala index c1ad894153820f61064a7c86a1bc1cfb24c91d6b..f96ecacbfe88a6949eae7135c9742924fc56212c 100644 --- a/src/main/scala/leon/synthesis/Heuristics.scala +++ b/src/main/scala/leon/synthesis/Heuristics.scala @@ -72,7 +72,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn } -class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8, 50) { +class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8, 100) { def applyOn(task: Task): RuleResult = { val p = task.problem diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala index 7210ef271b7b656694e363f664a978abdfac4a12..51e1c02eabbb60055d14fa778eed6ad67d2000bb 100644 --- a/src/main/scala/leon/synthesis/Rules.scala +++ b/src/main/scala/leon/synthesis/Rules.scala @@ -17,8 +17,7 @@ object Rules { new CaseSplit(synth), new UnusedInput(synth), new UnconstrainedOutput(synth), - new Assert(synth), - new GiveUp(synth) + new Assert(synth) ) } @@ -276,9 +275,3 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20, 0) { } } -class GiveUp(synth: Synthesizer) extends Rule("GiveUp", synth, -100000, 100) { - def applyOn(task: Task): RuleResult = { - RuleSuccess(Solution.choose(task.problem)) - } -} - diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index d18bd0cb1c38a3684175f989258445e9e69a0519..0739733ea0cbdefbcd0769e8e693fc5a454575e3 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -28,16 +28,26 @@ class Synthesizer(val r: Reporter, val workList = new PriorityQueue[Task]() val rootTask = new RootTask(this, p) + val giveUpComplexity = new TaskComplexity(null) { + override def value = 100000 + } workList += rootTask while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) { val task = workList.dequeue() - val subProblems = task.run - - for (p <- subProblems; r <- rules) yield { - workList += new Task(this, task, p, r) + if (task.complexity > giveUpComplexity) { + // This task is too complicated, we give up with a choose solution + val solution = Solution.choose(task.problem) + task.solution = Some(solution) + task.parent.partlySolvedBy(task, solution) + } else { + val subProblems = task.run + + for (p <- subProblems; r <- rules) yield { + workList += new Task(this, task, p, r) + } } } diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala index fd4e8a2c90977b01ce05fe367d11b4baf30089b7..c1c5bdb694b6de1a3e78792b2ddeb5e3a01c4684 100644 --- a/src/main/scala/leon/synthesis/Task.scala +++ b/src/main/scala/leon/synthesis/Task.scala @@ -2,7 +2,7 @@ package leon package synthesis class Task(synth: Synthesizer, - parent: Task, + val parent: Task, val problem: Problem, val rule: Rule) extends Ordered[Task] { @@ -34,6 +34,17 @@ class Task(synth: Synthesizer, } } + var failures = Set[Rule]() + def unsolvedBy(t: Task) { + failures += t.rule + + if (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 run: List[Problem] = { rule.applyOn(this) match { case RuleSuccess(solution) => @@ -48,6 +59,7 @@ class Task(synth: Synthesizer, subProblems case RuleInapplicable => + parent.unsolvedBy(this) Nil } } @@ -62,13 +74,24 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p override lazy val minSolutionCost = 0 - override def partlySolvedBy(t: Task, s: Solution) = { + override def partlySolvedBy(t: Task, s: Solution) { if (isBetterSolutionThan(s, solution)) { solution = Some(s) solver = Some(t) } } + override def unsolvedBy(t: Task) { + failures += t.rule + + if (failures.size == synth.rules.size) { + // We might want to report unsolved instead of solvedByChoose, depending + // on the cases + solution = Some(Solution.choose(problem)) + solver = None + } + } + override def run: List[Problem] = { List(problem) }