From ce6ef073f149a3adb4cae27953c59980bdfddcf4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 3 Jan 2013 16:41:59 +0100
Subject: [PATCH] Remove obsolete concept of Rule priorities. This is now
implicitly handled by the search.
---
src/main/scala/leon/synthesis/Rules.scala | 2 +-
src/main/scala/leon/synthesis/heuristics/ADTInduction.scala | 2 +-
src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala | 2 +-
src/main/scala/leon/synthesis/heuristics/IntInduction.scala | 2 +-
.../scala/leon/synthesis/heuristics/OptimisticInjection.scala | 2 +-
.../scala/leon/synthesis/heuristics/SelectiveInlining.scala | 2 +-
src/main/scala/leon/synthesis/rules/ADTDual.scala | 2 +-
src/main/scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
src/main/scala/leon/synthesis/rules/Assert.scala | 2 +-
src/main/scala/leon/synthesis/rules/CaseSplit.scala | 2 +-
src/main/scala/leon/synthesis/rules/Cegis.scala | 2 +-
src/main/scala/leon/synthesis/rules/Disunification.scala | 2 +-
src/main/scala/leon/synthesis/rules/EqualitySplit.scala | 2 +-
src/main/scala/leon/synthesis/rules/Ground.scala | 2 +-
src/main/scala/leon/synthesis/rules/IntegerEquation.scala | 2 +-
src/main/scala/leon/synthesis/rules/IntegerInequalities.scala | 2 +-
src/main/scala/leon/synthesis/rules/OnePoint.scala | 2 +-
src/main/scala/leon/synthesis/rules/OptimisticGround.scala | 2 +-
src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala | 2 +-
src/main/scala/leon/synthesis/rules/Unification.scala | 4 ++--
src/main/scala/leon/synthesis/rules/UnusedInput.scala | 2 +-
21 files changed, 22 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index af348baf8..3d24a3c2d 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -75,7 +75,7 @@ object RuleInstantiation {
}
}
-abstract class Rule(val name: String, val priority: Priority) {
+abstract class Rule(val name: String) {
def instantiateOn(scrx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation]
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index bd8695540..adcbb72a2 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-case object ADTInduction extends Rule("ADT Induction", 80) with Heuristic {
+case object ADTInduction extends Rule("ADT Induction") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val candidates = p.as.collect {
case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
diff --git a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
index 5b50ac758..b2782c5dc 100644
--- a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object InnerCaseSplit extends Rule("Inner-Case-Split", 200) with Heuristic {
+case object InnerCaseSplit extends Rule("Inner-Case-Split") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.phi match {
case Or(_) =>
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index a4c7f9cf2..fdcc626c4 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-case object IntInduction extends Rule("Int Induction", 50) with Heuristic {
+case object IntInduction extends Rule("Int Induction") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.as match {
case List(IsTyped(origId, Int32Type)) =>
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index 494e0979a..a3ecedd72 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-case object OptimisticInjection extends Rule("Opt. Injection", 50) with Heuristic {
+case object OptimisticInjection extends Rule("Opt. Injection") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 44ceb7879..8e91394f0 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-case object SelectiveInlining extends Rule("Sel. Inlining", 20) with Heuristic {
+case object SelectiveInlining extends Rule("Sel. Inlining") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 78573c819..6b6dac90f 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object ADTDual extends Rule("ADTDual", 200) {
+case object ADTDual extends Rule("ADTDual") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val xs = p.xs.toSet
val as = p.as.toSet
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 631fe979a..e94abd7f1 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
import purescala.Extractors._
import purescala.Definitions._
-case object ADTSplit extends Rule("ADT Split.", 70) {
+case object ADTSplit extends Rule("ADT Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 962e090ae..4522067b8 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object Assert extends Rule("Assert", 200) {
+case object Assert extends Rule("Assert") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.phi match {
case TopLevelAnds(exprs) =>
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 2375f3375..3850b1d74 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object CaseSplit extends Rule("Case-Split", 200) {
+case object CaseSplit extends Rule("Case-Split") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.phi match {
case Or(os) =>
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index c2ab7c253..93898bcc8 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -11,7 +11,7 @@ import purescala.Extractors._
import solvers.z3.FairZ3Solver
-case object CEGIS extends Rule("CEGIS", 150) {
+case object CEGIS extends Rule("CEGIS") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 53963b502..9ca48a9f6 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -8,7 +8,7 @@ import purescala.TreeOps._
import purescala.Extractors._
object Disunification {
- case object Decomp extends Rule("Disunif. Decomp.", 200) {
+ case object Decomp extends Rule("Disunif. Decomp.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index eebab17e9..bad8bc4c4 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -8,7 +8,7 @@ import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-case object EqualitySplit extends Rule("Eq. Split.", 90) {
+case object EqualitySplit extends Rule("Eq. Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val candidates = p.as.groupBy(_.getType).map(_._2.toList).filter {
case List(a1, a2) =>
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 97c0c8366..6aefe88a8 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -7,7 +7,7 @@ import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-case object Ground extends Rule("Ground", 500) {
+case object Ground extends Rule("Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 00d21c604..eabbfce2e 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -11,7 +11,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
import LinearEquations.elimVariable
-case object IntegerEquation extends Rule("Integer Equation", 600) {
+case object IntegerEquation extends Rule("Integer Equation") {
def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = if(!problem.xs.exists(_.getType == Int32Type)) Nil else {
val TopLevelAnds(exprs) = problem.phi
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 7cb6b28cb..21f9dced1 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -12,7 +12,7 @@ import purescala.Definitions._
import LinearEquations.elimVariable
import leon.synthesis.Algebra.lcm
-case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
+case object IntegerInequalities extends Rule("Integer Inequalities") {
def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = problem.phi
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 76aedbdc5..24eee3336 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object OnePoint extends Rule("One-point", 300) {
+case object OnePoint extends Rule("One-point") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 0ddce7824..460a83fe4 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -7,7 +7,7 @@ import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-case object OptimisticGround extends Rule("Optimistic Ground", 150) {
+case object OptimisticGround extends Rule("Optimistic Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (!p.as.isEmpty && !p.xs.isEmpty) {
val xss = p.xs.toSet
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 808a76dd8..7c8d2de15 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object UnconstrainedOutput extends Rule("Unconstr.Output", 100) {
+case object UnconstrainedOutput extends Rule("Unconstr.Output") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val unconstr = p.xs.toSet -- variablesOf(p.phi)
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index fd278ff24..5c8151619 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -8,7 +8,7 @@ import purescala.TreeOps._
import purescala.Extractors._
object Unification {
- case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.", 200) {
+ case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
@@ -36,7 +36,7 @@ object Unification {
// This rule is probably useless; it never happens except in crafted
// examples, and will be found by OptimisticGround anyway.
- case object OccursCheck extends Rule("Unif OccursCheck", 200) {
+ case object OccursCheck extends Rule("Unif OccursCheck") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index d9b26efed..13ba585ab 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object UnusedInput extends Rule("UnusedInput", 100) {
+case object UnusedInput extends Rule("UnusedInput") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc)
--
GitLab