From fa25dd45bf1649bd67cbc13d6012e4d859fa6789 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 9 Nov 2012 16:52:03 +0100
Subject: [PATCH] By convention, we reserve priorities 1-99 to heuristics
---
.../scala/leon/synthesis/Heuristics.scala | 39 +++++++++++++++++--
src/main/scala/leon/synthesis/Rules.scala | 18 ++++-----
2 files changed, 45 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 4d32f4738..b9adc1fbe 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -22,7 +22,7 @@ trait Heuristic {
override def toString = "H: "+name
}
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 9) with Heuristic {
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) with Heuristic {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -79,7 +79,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
}
-class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8) with Heuristic {
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) with Heuristic {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -124,7 +124,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8) w
}
}
-class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", synth, 5) with Heuristic {
+class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", synth, 50) with Heuristic {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -148,9 +148,42 @@ class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", syn
val args = argss(0) zip argss(1)
newExprs ++= args.map{ case (l, r) => Equals(l, r) }
+ newExprs = newExprs.filterNot(toRemove)
+ }
+
+ val sub = p.copy(phi = And(newExprs))
+
+ RuleDecomposed(List(sub), forward)
+ } else {
+ RuleInapplicable
+ }
+ }
+}
+
+class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth, 20) with Heuristic {
+ def applyOn(task: Task): RuleResult = {
+ val p = task.problem
+
+ val TopLevelAnds(exprs) = p.phi
+ val eqfuncalls = exprs.collect{
+ case eq @ Equals(FunctionInvocation(fd, args), e) =>
+ ((fd, e), args, eq : Expr)
+ case eq @ Equals(e, FunctionInvocation(fd, args)) =>
+ ((fd, e), args, eq : Expr)
+ }
+
+ val candidates = eqfuncalls.groupBy(_._1).filter(_._2.size > 1)
+ if (!candidates.isEmpty) {
+ var newExprs = exprs
+ for (cands <- candidates.values) {
+ val cand = cands.take(2)
+ val toRemove = cand.map(_._3).toSet
+ val argss = cand.map(_._2)
+ val args = argss(0) zip argss(1)
+ newExprs ++= args.map{ case (l, r) => Equals(l, r) }
newExprs = newExprs.filterNot(toRemove)
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index ed3836e2e..bef01caf4 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -42,7 +42,7 @@ abstract class Rule(val name: String, val synth: Synthesizer, val priority: Prio
override def toString = "R: "+name
}
-class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 30) {
+class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -81,7 +81,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 30) {
}
}
-class Ground(synth: Synthesizer) extends Rule("Ground", synth, 50) {
+class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -103,7 +103,7 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 50) {
}
}
-class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 20) {
+class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
p.phi match {
@@ -123,7 +123,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 20) {
}
}
-class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
+class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -159,7 +159,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
}
}
-class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 10) {
+class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 100) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
val unused = p.as.toSet -- variablesOf(p.phi)
@@ -174,7 +174,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 10) {
}
}
-class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 10) {
+class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 100) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
val unconstr = p.xs.toSet -- variablesOf(p.phi)
@@ -198,7 +198,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
}
object Unification {
- class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 20) {
+ class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 200) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -226,7 +226,7 @@ object Unification {
}
}
- class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 20) {
+ class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 200) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -253,7 +253,7 @@ object Unification {
}
-class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20) {
+class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
--
GitLab