From 6adbc58360d34d2420345510ed6a981fac95d077 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 18:42:44 +0200
Subject: [PATCH] Fix assert, Add example, add more debug output for last rule
---
src/main/scala/leon/purescala/Trees.scala | 2 ++
src/main/scala/leon/synthesis/Rules.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 1 +
testcases/synthesis/Spt.scala | 2 ++
4 files changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 04db1ab18..58e4f8162 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -1059,6 +1059,8 @@ object Trees {
None
}
}
+ case letTuple @ LetTuple(ids, e, body) =>
+ None
case _ => None
}
searchAndReplace(simplerLet)(expr)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index b2792da85..e1dab45ee 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -131,7 +131,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- List(task.solveUsing(this, Solution(And(exprsA), BooleanLiteral(true), 150), 150))
+ List(task.solveUsing(this, Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))), 150))
} else {
val onSuccess: List[Solution] => Solution = {
case List(s) => Solution(And(s.pre +: exprsA), s.term, 150)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 9361e2c92..a4ab6b46f 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -32,6 +32,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
alternatives.find(_.isSuccess) match {
case Some(ss) =>
+ info(" => "+ss.rule+" succeeded")
ss.succeeded()
case None =>
info(" => Possible Next Steps:")
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 551317142..3a797a9b1 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -13,6 +13,8 @@ object SynthesisProceduresToolkit {
def e5(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) => Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4)))
+ def e6(a: Nat, b: Nat): (Nat, NatList) = choose( (x: Nat, y: NatList) => a == Succ(b))
+
abstract class Nat
case class Z() extends Nat
case class Succ(n: Nat) extends Nat
--
GitLab