From 54d6ebe258cfbaac75f863e212664b71494494f2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 18:12:40 +0200
Subject: [PATCH] Keep precondition inside formula, print precondition
---
src/main/scala/leon/synthesis/Rules.scala | 17 +++++------------
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
2 files changed, 6 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 1c045aabb..b2792da85 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -256,24 +256,17 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth) {
val TopLevelAnds(exprs) = p.phi
- val (toRemove, toAdd, toPre) = exprs.collect {
+ val (toRemove, toAdd) = exprs.collect {
case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
- (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) )
+ (eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } )
case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
- (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) )
- }.unzip3
+ (eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } )
+ }.unzip
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- val onSuccess: List[Solution] => Solution = {
- case List(s) =>
- Solution(And(s.pre +: toPre), s.term)
- case _ =>
- Solution.none
- }
-
- List(task.decompose(this, List(sub), onSuccess, 80))
+ List(task.decompose(this, List(sub), forward, 80))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 2b927cad0..9361e2c92 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -95,7 +95,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
val sol = synthesize(Problem(as, phi, xs), rules)
info("Scala code:")
- info(ScalaPrinter(sol.term))
+ info(ScalaPrinter(IfExpr(sol.pre, sol.term, Error("Precondition failed").setType(sol.term.getType))))
a
case _ =>
--
GitLab