From 0b2eb621c23c6ab17b734711fda38e7a114a57c5 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 14 Nov 2012 13:57:39 +0100
Subject: [PATCH] Implement EqualitySplit We should check whether we do not
always split on same variables
---
src/main/scala/leon/synthesis/Rules.scala | 24 +++++++++++++++++++++--
1 file changed, 22 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index b79ade73c..2ea3725c0 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -20,6 +20,7 @@ object Rules {
new UnusedInput(_),
new UnconstrainedOutput(_),
new OptimisticGround(_),
+ new EqualitySplit(_),
new CEGIS(_),
new Assert(_)
)
@@ -281,7 +282,7 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
}
}
-class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 50) {
+class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -457,7 +458,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 50) {
}
}
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) {
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 150) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -512,3 +513,22 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
}
}
}
+
+class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 10) {
+ def applyOn(task: Task): RuleResult = {
+ val p = task.problem
+
+ val asgroups = p.as.groupBy(_.getType).filter(_._2.size == 2).mapValues(_.toList)
+
+ val extraConds = for (List(a1, a2) <- asgroups.values) yield {
+ Or(Equals(Variable(a1), Variable(a2)), Not(Equals(Variable(a1), Variable(a2))))
+ }
+
+ if (!extraConds.isEmpty) {
+ val sub = p.copy(phi = And(And(extraConds.toSeq), p.phi))
+ RuleStep(List(sub), forward)
+ } else {
+ RuleInapplicable
+ }
+ }
+}
--
GitLab