From 147d699da5abba1890ca4d74b850d57f765a5604 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 15:55:57 +0200
Subject: [PATCH] Call z3 to get model satisfying no conditions
---
src/main/scala/leon/synthesis/Rules.scala | 11 ++++++++---
testcases/Choose.scala | 2 ++
2 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index cbc6f2974..986feb80b 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -164,8 +164,6 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
}
class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth) {
- def defaultValueFor(id: Identifier): Expr = IntLiteral(0)
-
def isApplicable(task: Task): List[DecomposedTask] = {
val p = task.problem
val unconstr = p.xs.toSet -- variablesOf(p.phi)
@@ -174,7 +172,14 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
val sub = p.copy(xs = p.xs.filterNot(unconstr))
val onSuccess: List[Solution] => Solution = {
- case List(s) => Solution(s.pre, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) defaultValueFor(id) else Variable(id) ))))
+ case List(s) =>
+ synth.solveSAT(And(unconstr.map(id => Equals(Variable(id), Variable(id))).toSeq)) match {
+ case (Some(true), model) =>
+ Solution(s.pre, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) model(id) else Variable(id)))))
+ case _ =>
+ Solution.none
+ }
+
case _ => Solution.none
}
diff --git a/testcases/Choose.scala b/testcases/Choose.scala
index 85b6225d7..bf9ef06fa 100644
--- a/testcases/Choose.scala
+++ b/testcases/Choose.scala
@@ -13,6 +13,8 @@ object ChooseTest {
def c4(a: Int): (Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int) => x1 > a && x2 > a }
def c5(a: Int): (Int, Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int, x5: Int) => x1 > a && x2 > a }
+ def z0(a: Int): (Int, Int, List) = choose{ (x1: Int, x2: Int, x3: List) => x1 > a && x2 > a }
+
sealed abstract class List
case class Nil() extends List
--
GitLab