From 049539251d4dc837d3a2f21a2d2616f9922725d9 Mon Sep 17 00:00:00 2001 From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch> Date: Wed, 7 Jan 2015 18:13:19 +0100 Subject: [PATCH] EquivalentInputs substitutes back during solution reconstruction --- src/main/scala/leon/synthesis/Rules.scala | 6 ++++++ .../scala/leon/synthesis/rules/EquivalentInputs.scala | 9 +++++++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala index f2df54b71..2ac45f4be 100644 --- a/src/main/scala/leon/synthesis/Rules.scala +++ b/src/main/scala/leon/synthesis/Rules.scala @@ -143,6 +143,12 @@ trait RuleDSL { def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replaceFromIDs(what, in) val forward: List[Solution] => Option[Solution] = { ss => ss.headOption } + + def forwardMap(f : Expr => Expr) : List[Solution] => Option[Solution] = { + _.headOption map { s => + Solution(f(s.pre), s.defs, f(s.term)) + } + } def decomp(sub: List[Problem], onSuccess: List[Solution] => Option[Solution], description: String) (implicit problem: Problem): RuleInstantiation = { diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala index b5c5744f6..35423e656 100644 --- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala +++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala @@ -19,7 +19,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") { case ccio @ CaseClassInstanceOf(cct, s) => ccio } - var clauses = allClauses.filterNot(instanceOfs.toSet) + val clauses = allClauses.filterNot(instanceOfs.toSet) val ccSubsts = for (CaseClassInstanceOf(cct, s) <- instanceOfs) yield { @@ -73,7 +73,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") { pc = simplifier(andJoin(replaceSeq(substs, p.pc) +: postsToInject)), phi = simplifier(replaceSeq(substs, p.phi))) - List(decomp(List(sub), forward, "Equivalent Inputs")) + val subst = replace( + substs.map{_.swap}.filter{ case (x,y) => formulaSize(x) > formulaSize(y) }.toMap, + _:Expr + ) + + List(decomp(List(sub), forwardMap(subst), "Equivalent Inputs")) } else { Nil } -- GitLab