From d8f70e729d8597c17ab030b9bd61f3c97aaa4503 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Wed, 7 Jan 2015 17:19:52 +0100
Subject: [PATCH] Make sure ADTSplit substitutes away introduced variables
---
.../scala/leon/synthesis/rules/ADTSplit.scala | 17 +++++++++++------
1 file changed, 11 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 482f40564..d5b03204d 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -48,7 +48,7 @@ case object ADTSplit extends Rule("ADT Split.") {
}
}
- candidates.collect{ _ match {
+ candidates.collect {
case Some((id, act, cases)) =>
val oas = p.as.filter(_ != id)
@@ -72,7 +72,14 @@ case object ADTSplit extends Rule("ADT Split.") {
var globalPre = List[Expr]()
val cases = for ((sol, (cct, problem, pattern)) <- (sols zip subInfo)) yield {
- globalPre ::= and(CaseClassInstanceOf(cct, Variable(id)), sol.pre)
+ if (sol.pre != BooleanLiteral(true)) {
+ val substs = (for ((field,arg) <- cct.fields zip problem.as ) yield {
+ (arg, CaseClassSelector(cct, id.toVariable, field.id))
+ }).toMap
+ globalPre ::= and(CaseClassInstanceOf(cct, Variable(id)), replaceFromIDs(substs, sol.pre))
+ } else {
+ globalPre ::= BooleanLiteral(true)
+ }
SimpleCase(pattern, sol.term)
}
@@ -80,9 +87,7 @@ case object ADTSplit extends Rule("ADT Split.") {
Some(Solution(orJoin(globalPre), sols.flatMap(_.defs).toSet, matchExpr(Variable(id), cases), sols.forall(_.isTrusted)))
}
- Some(decomp(subInfo.map(_._2).toList, onSuccess, s"ADT Split on '$id'"))
- case _ =>
- None
- }}.flatten
+ decomp(subInfo.map(_._2).toList, onSuccess, s"ADT Split on '$id'")
+ }
}
}
--
GitLab