From 28eaf0ed81552740044aa320d915d1b6848d4ba6 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 22 Oct 2012 18:24:51 +0200
Subject: [PATCH] Generate a proper error in ground rule
---
src/main/scala/leon/synthesis/Rules.scala | 8 ++++++--
testcases/Choose.scala | 1 +
2 files changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index e56157940..da031c5e7 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -3,6 +3,7 @@ package synthesis
import purescala.Common._
import purescala.Trees._
+import purescala.TypeTrees._
object Rules {
def all(synth: Synthesizer) = List(
@@ -65,16 +66,19 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
def isApplicable(p: Problem, parent: Task): List[Task] = {
if (p.as.isEmpty) {
+
+ val tpe = TupleType(p.xs.map(_.getType))
+
synth.solveSAT(p.phi) match {
case (Some(true), model) =>
val onSuccess: List[Solution] => Solution = {
- case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)))
+ case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe))
}
List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
case (Some(false), model) =>
val onSuccess: List[Solution] => Solution = {
- case Nil => Solution(BooleanLiteral(false), BooleanLiteral(false))
+ case Nil => Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))
}
List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
diff --git a/testcases/Choose.scala b/testcases/Choose.scala
index 3d7740348..336299a0f 100644
--- a/testcases/Choose.scala
+++ b/testcases/Choose.scala
@@ -3,6 +3,7 @@ import leon.Utils._
object ChooseTest {
def c0(): Int = choose{ (x1: Int) => x1 > 13 }
+ def b0(): Int = choose{ (x1: Int) => x1 > 13 && x1 < 2 }
def c1(a: Int): Int = choose{ (x1: Int) => x1 > a }
def c2(a: Int): (Int, Int) = choose{ (x1: Int, x2: Int) => x1 > a && x2 > a }
--
GitLab