From 6561e6c9dfb3cd87c947e792eae6dac7ffbd120c Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 11 Nov 2014 14:42:20 +0100
Subject: [PATCH] Make sure pattern binders are input variables in subproblems
---
.../scala/leon/synthesis/rules/GuidedDecomp.scala | 15 +++++++++++----
1 file changed, 11 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
index f2a26848b..878dd149c 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
@@ -55,12 +55,19 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
case m @ MatchExpr(scrut, cs) =>
var pcSoFar: Expr = BooleanLiteral(true)
val subs = for (c <- cs) yield {
- val substs = patternSubstitutions(scrut, c.pattern)
+ val s = scrut match {
+ case Variable(_) => scrut
+ case _ => Variable(FreshIdentifier("scrut", true).setType(scrut.getType))
+ }
+ val sConstr = scrut match {
+ case Variable(_) => BooleanLiteral(true)
+ case _ => Equals(s,scrut)
+ }
+ val substs = patternSubstitutions(s, c.pattern)
val cond = conditionForPattern(scrut, c.pattern)
-
val g = c.theGuard.getOrElse(BooleanLiteral(true))
- val pc = simplify(doSubstitute(substs, And(Seq(pcSoFar, g, replace(Map(m -> c.rhs), p.pc)))))
- val phi = doSubstitute(substs, p.phi)
+ val pc = simplify(doSubstitute(substs, And(Seq(pcSoFar, g, sConstr, replace(Map(m -> c.rhs), p.pc)))))
+ val phi = doSubstitute(substs, p.phi)
val free = variablesOf(And(pc, phi)) -- p.xs
pcSoFar = And(pcSoFar, Not(cond))
--
GitLab