From 6522fc500b9785e5b3487e5b8057da71ceff0abe Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Oct 2012 19:41:49 +0200
Subject: [PATCH] Ands get decomposed into sub-ands
---
src/main/scala/leon/synthesis/Rules.scala | 8 +++++++-
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
src/main/scala/leon/synthesis/Task.scala | 11 ++++++++---
3 files changed, 16 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 408b2395e..635ea6834 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -22,7 +22,13 @@ object OnePoint extends Rule("One-point") {
def isApplicable(p: Problem, parent: Task): List[Task] = {
p.phi match {
- case And(exprs) =>
+ case a : And =>
+ def collectAnds(e: Expr): List[Expr] = e match {
+ case And(exs) => exs.toList.flatMap(collectAnds)
+ case e => List(e)
+ }
+
+ val exprs = collectAnds(a)
val candidates = exprs.collect {
case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
(x, e, eq)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 94fa516d5..3258b1062 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -67,7 +67,7 @@ class Synthesizer(rules: List[Rule]) {
val x = Variable(FreshIdentifier("x").setType(Int32Type))
val y = Variable(FreshIdentifier("y").setType(Int32Type))
- val p = Problem(Nil, And(GreaterThan(x, y), Equals(x, IntLiteral(3))), List(x.id, y.id))
+ val p = Problem(Nil, And(List(GreaterThan(x, y), Equals(y, IntLiteral(2)), Equals(x, IntLiteral(3)))), List(x.id, y.id))
synthesize(p)
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 2b8d6ad88..04689589a 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -17,7 +17,12 @@ class Task(
def succeeded() {
assert(isSuccess)
- notifyParent(onSuccess(Nil))
+
+ val solution = onSuccess(Nil)
+
+ println("Found solution: "+problem+" ⊢ "+solution)
+
+ notifyParent(solution)
}
def subSucceeded(p: Problem, s: Solution) {
@@ -30,7 +35,7 @@ class Task(
val solution = onSuccess(subProblems map subSolutions)
- println("Found solution to: "+problem+" ⊢ "+solution)
+ println("Found solution: "+problem+" ⊢ "+solution)
notifyParent(solution)
}
@@ -43,6 +48,6 @@ class Task(
class RootTask(p: Problem) extends Task(null, p, List(p), xs => xs.head, 0) {
override def notifyParent(solution: Solution) {
- sys.error("You need to extend this!")
+ sys.error("You need to override this!")
}
}
--
GitLab