From a0dff8f4a2d3251be6296212ba93da55f20c70a8 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Thu, 8 Jan 2015 17:06:53 +0100
Subject: [PATCH] DetupleInput recomposes inputs, if possible
---
.../leon/synthesis/rules/DetupleInput.scala | 42 ++++++++++++++-----
1 file changed, 31 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 06c5b5d18..1157a17ca 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -65,19 +65,39 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
val newAs = subAs.flatten
//sctx.reporter.warning("newOuts: " + newOuts.toString)
- val sub = Problem(newAs, subWs, subPc, subProblem, p.xs)
-
- val onSuccess: List[Solution] => Option[Solution] = {
- case List(sol) =>
- val newPre = substAll(reverseMap, sol.pre)
- val newTerm = substAll(reverseMap, sol.term)
- Some(Solution(newPre, sol.defs, newTerm, sol.isTrusted))
- case _ =>
- None
+ // Recompose CaseClasses and Tuples.
+ // E.g. Cons(l.head, l.tail) ~~> l
+ // (t._1, t._2, t._3) ~~> t
+ def recompose(e : Expr) : Expr = e match {
+ case CaseClass(ct, args) =>
+ val (cts, es) = args.zip(ct.fields).map {
+ case (CaseClassSelector(ct, e, id), field) if field.id == id => (ct, e)
+ case _ => return e
+ }.unzip
+
+ if (cts.distinct.size == 1 && es.distinct.size == 1) {
+ es.head
+ } else {
+ e
+ }
+ case Tuple(args) =>
+ val es = args.zipWithIndex.map {
+ case (TupleSelect(e, i), index) if i == index + 1 => e
+ case _ => return e
+ }
+ if (es.distinct.size == 1) {
+ es.head
+ } else {
+ e
+ }
+ case other => other
}
+
+ val sub = Problem(newAs, subWs, subPc, subProblem, p.xs)
-
- Some(decomp(List(sub), onSuccess, s"Detuple ${reverseMap.keySet.mkString(", ")}"))
+ val s = {substAll(reverseMap, _:Expr)} andThen { simplePostTransform(recompose) }
+
+ Some(decomp(List(sub), forwardMap(s), s"Detuple ${reverseMap.keySet.mkString(", ")}"))
} else {
None
}
--
GitLab