From 76125021706e60a9b8ed8ef011ef086adb422ce0 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 14 Nov 2012 21:44:30 +0100
Subject: [PATCH] Chased the Set.empty[Int] vs. Set() subtelty.
---
src/main/scala/leon/synthesis/Rules.scala | 6 +++++-
testcases/synthesis/ADTInduction.scala | 14 ++++++++++++--
2 files changed, 17 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 78a8546a2..8fd86f53c 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -441,6 +441,8 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
case _ =>
+ reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ continue = false
}
case (Some(false), _) =>
@@ -479,12 +481,14 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
while (result.isEmpty && i < maxTries) {
val phi = And(p.phi +: predicates)
+ //println("SOLVING " + phi + " ...")
synth.solver.solveSAT(phi) match {
case (Some(true), satModel) =>
val satXsModel = satModel.filterKeys(xss)
val newPhi = valuateWithModelIn(phi, xss, satModel)
+ //println("REFUTING " + Not(newPhi) + "...")
synth.solver.solveSAT(Not(newPhi)) match {
case (Some(true), invalidModel) =>
// Found as such as the xs break, refine predicates
@@ -535,7 +539,7 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
)
}
- val candidate = p.as.groupBy(_.getType).map(_._2.toList).find{
+ val candidate = p.as.groupBy(_.getType).map(_._2.toList).find {
case List(a1, a2) => (pres & combinations(a1, a2)).isEmpty
case _ => false
}
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/ADTInduction.scala
index f30827fa3..23db0bb01 100644
--- a/testcases/synthesis/ADTInduction.scala
+++ b/testcases/synthesis/ADTInduction.scala
@@ -16,11 +16,21 @@ object SortedList {
//def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
def content(l: List): Set[Int] = l match {
- case Nil() => Set()
+ case Nil() => Set.empty[Int]
case Cons(i, t) => Set(i) ++ content(t)
}
- def deleteSynth(in: List, v: Int) = choose{ (out: List) => !(content(out) contains v) && size(out)+1 >= size(in) }
+ //def artifialSubcase(v : Int) = choose {
+ // (out : List) =>
+ // content(out) == (content(Nil()) -- Set(v))
+ //}
+
+ def deleteSynth(in: List, v: Int) = choose {
+ (out: List) =>
+ // This spec is too weak. Maybe use later as bad example?
+ //!(content(out) contains v) && size(out)+1 >= size(in)
+ (content(out) == (content(in) -- Set(v)))
+ }
def isSorted(l: List): Boolean = l match {
case Nil() => true
--
GitLab