From 76e4a4a50af5d17a80a4ce64e24b4c4716570876 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Sat, 3 Nov 2012 02:12:38 +0100
Subject: [PATCH] Kill Assert as we know it for now. Keep the trivial base
case.
Assert may not be helping at all. It is trimming crucial information
from the formula, i.e.
[[ a,b ; a = size(x) AND a+1 = size(b); x ]].
Applying assert will remove 'a+1 = size(b)' from phi and push it as
precondition when reconstructing a solution. The subproblem will become:
[[ a,b ; a = size(x) ; x]]
The input 'b' is then removed by applying Unused-Input.
---
src/main/scala/leon/synthesis/Rules.scala | 4 ++++
src/main/scala/leon/synthesis/Synthesizer.scala | 8 ++++----
2 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index ca8b32d86..ba7be35c7 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -137,6 +137,8 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
if (others.isEmpty) {
RuleSuccess(Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
} else {
+ /*
+ * Disable for now, it is not that useful anyway
val onSuccess: List[Solution] => Solution = {
case List(s) => Solution(And(s.pre +: exprsA), s.term)
case _ => Solution.none
@@ -145,6 +147,8 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
val sub = p.copy(phi = And(others))
RuleDecomposed(List(sub), onSuccess)
+ */
+ RuleInapplicable
}
} else {
RuleInapplicable
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 5020c5220..f8f9f5686 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -55,11 +55,11 @@ class Synthesizer(val r: Reporter,
// current solution
if (task.minComplexity < bestSolutionSoFar().complexity) {
if (!subProblems.isEmpty) {
- val name = Option(task.rule).map(_.name).getOrElse("root")
- println("["+name+"] Got: "+task.problem)
- println("["+name+"] Decomposed into:")
+ val prefix = "[%-20s] ".format(Option(task.rule).map(_.name).getOrElse("root"))
+ println(prefix+"Got: "+task.problem)
+ println(prefix+"Decomposed into:")
for(p <- subProblems) {
- println("["+name+"] - "+p)
+ println(prefix+" - "+p)
}
}
--
GitLab