From 7d8de42ac8047ffe87fa330e5d6c9443ea37db56 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 28 Apr 2016 14:36:45 +0200
Subject: [PATCH] Fix recomposition bugs in ADTSplit
---
.../scala/leon/synthesis/rules/ADTSplit.scala | 31 ++++++++-----------
1 file changed, 13 insertions(+), 18 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 56d28d01e..5b5070124 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -115,24 +115,19 @@ case object ADTSplit extends Rule("ADT Split.") {
cct.fieldsTypes.count { t => t == act }
}
- val onSuccess: List[Solution] => Option[Solution] = {
- case sols =>
- var globalPre = List[Expr]()
-
- val cases = for ((sol, (cct, problem, pattern)) <- sols zip subInfo) yield {
- if (sol.pre != BooleanLiteral(true)) {
- val substs = (for ((field,arg) <- cct.classDef.fields zip problem.as ) yield {
- (arg, caseClassSelector(cct, id.toVariable, field.id))
- }).toMap
- globalPre ::= and(IsInstanceOf(Variable(id), cct), replaceFromIDs(substs, sol.pre))
- } else {
- globalPre ::= BooleanLiteral(true)
- }
-
- SimpleCase(pattern, sol.term)
- }
-
- Some(Solution(orJoin(globalPre), sols.flatMap(_.defs).toSet, matchExpr(Variable(id), cases), sols.forall(_.isTrusted)))
+ val onSuccess: List[Solution] => Option[Solution] = { sols =>
+ val (cases, globalPres) = (for ((sol, (cct, problem, pattern)) <- sols zip subInfo) yield {
+ val retrievedArgs = pattern.subPatterns.collect{ case WildcardPattern(Some(id)) => id }
+ val substs = (for ((field,arg) <- cct.classDef.fields zip retrievedArgs ) yield {
+ (arg, caseClassSelector(cct, id.toVariable, field.id))
+ }).toMap
+ (
+ SimpleCase(pattern, sol.term),
+ and(IsInstanceOf(Variable(id), cct), replaceFromIDs(substs, sol.pre))
+ )
+ }).unzip
+
+ Some(Solution(orJoin(globalPres), sols.flatMap(_.defs).toSet, matchExpr(Variable(id), cases), sols.forall(_.isTrusted)))
}
decomp(subInfo.map(_._2).toList, onSuccess, s"ADT Split on '${id.asString}'")
--
GitLab