From 4d1ce245c0426d3c04b94b9d7ca9804bf32988e9 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 16 Dec 2014 11:05:47 +0100
Subject: [PATCH] Improve EquivalentInputs, use foo' to represent new function.
No BUTEGIS
---
src/main/scala/leon/repair/Repairman.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 2 +-
.../scala/leon/synthesis/rules/EquivalentInputs.scala | 9 ++++++++-
3 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index e5b257f07..72b20588b 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -95,7 +95,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
def getSynthesizer(passingTests: List[Example], failingTests: List[Example]): Synthesizer = {
// Create a fresh function
- val nid = FreshIdentifier(fd.id.name+"_repair").copiedFrom(fd.id)
+ val nid = FreshIdentifier(fd.id.name+"'").copiedFrom(fd.id)
val nfd = new FunDef(nid, fd.tparams, fd.returnType, fd.params, fd.defType)
nfd.copyContentFrom(fd)
nfd.copiedFrom(fd)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index e93aa7089..d616c3b93 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -27,7 +27,7 @@ object Rules {
InequalitySplit,
CEGIS,
TEGIS,
- BottomUpTEGIS,
+ //BottomUpTEGIS,
rules.Assert,
DetupleOutput,
DetupleInput,
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 3a0847389..6b936d66b 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -50,8 +50,15 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
}
- val substs = discoverEquivalences(clauses)
+ // We could discover one equivalence, which could allow us to discover
+ // other equivalences: We do a fixpoint with limit 5.
+ val substs = fixpoint({ (substs: Set[(Expr, Expr)]) =>
+ val newClauses = substs.map{ case(e,v) => Equals(v, e) } // clauses are directed: foo = obj.f
+ substs ++ discoverEquivalences(clauses ++ newClauses)
+ }, 5)(Set()).toSeq
+
+ // We are replacing foo(a) with b. We inject postcondition(foo)(a, b).
val postsToInject = substs.collect {
case (FunctionInvocation(tfd, args), e) if tfd.hasPostcondition =>
val Some((id, post)) = tfd.postcondition
--
GitLab