diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 95ac39a13d8d8d55d295ff7c1edd8655495226dc..cb18ef781aec214808b3d9275b03c992deef524b 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -7,7 +7,7 @@ import purescala.TypeTrees.TupleType
import heuristics._
object Heuristics {
- def all = Set[Rule](
+ def all = List[Rule](
IntInduction,
InnerCaseSplit,
//new OptimisticInjection(_),
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index fb3f824c820c5b4f493d75ff85917feecf5d45e9..efe05182e1d329af67f7d744b7fa10348b941244 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -8,7 +8,7 @@ import solvers.TrivialSolver
class ParallelSearch(synth: Synthesizer,
problem: Problem,
- rules: Set[Rule],
+ rules: Seq[Rule],
costModel: CostModel,
nWorkers: Int) extends AndOrGraphParallelSearch[SynthesisContext, TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel)), nWorkers) {
@@ -69,14 +69,22 @@ class ParallelSearch(synth: Synthesizer,
}
def expandOrTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskTryRules) = {
- val sub = rules.flatMap { r =>
- r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
- }
+ val (normRules, otherRules) = rules.partition(_.isInstanceOf[NormalizingRule])
+
+ val normApplications = normRules.flatMap(_.instantiateOn(sctx, t.p))
- if (!sub.isEmpty) {
- Expanded(sub.toList)
+ if (!normApplications.isEmpty) {
+ Expanded(List(TaskRunRule(normApplications.head)))
} else {
- ExpandFailure()
+ val sub = otherRules.flatMap { r =>
+ r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
+ }
+
+ if (!sub.isEmpty) {
+ Expanded(sub.toList)
+ } else {
+ ExpandFailure()
+ }
}
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 27eba7ac6fc8b78b22fc8b6bef17cbbb483118df..7926efd69ac916f6678ec00b6a97fbddb7171864 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -8,7 +8,7 @@ import purescala.TreeOps._
import rules._
object Rules {
- def all = Set[Rule](
+ def all = List[Rule](
Unification.DecompTrivialClash,
Unification.OccursCheck, // probably useless
Disunification.Decomp,
@@ -89,3 +89,10 @@ abstract class Rule(val name: String) {
override def toString = "R: "+name
}
+
+// Note: Rules that extend NormalizingRule should all be commutative, The will
+// be applied before others in a deterministic order and their application
+// should never fail!
+abstract class NormalizingRule(name: String) extends Rule(name) {
+ override def toString = "N: "+name
+}
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 2b329ef705977bda1f12b15da05ebf207976edce..32258cedda16cbb3da45c077b89f68d8e0cd074c 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -32,7 +32,7 @@ case class SearchCostModel(cm: CostModel) extends AOCostModel[TaskRunRule, TaskT
class SimpleSearch(synth: Synthesizer,
problem: Problem,
- rules: Set[Rule],
+ rules: Seq[Rule],
costModel: CostModel) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel))) {
import synth.reporter._
@@ -64,12 +64,22 @@ class SimpleSearch(synth: Synthesizer,
}
def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
- val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(_)) )
+ val (normRules, otherRules) = rules.partition(_.isInstanceOf[NormalizingRule])
- if (!sub.isEmpty) {
- Expanded(sub.toList)
+ val normApplications = normRules.flatMap(_.instantiateOn(sctx, t.p))
+
+ if (!normApplications.isEmpty) {
+ Expanded(List(TaskRunRule(normApplications.head)))
} else {
- ExpandFailure()
+ val sub = otherRules.flatMap { r =>
+ r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
+ }
+
+ if (!sub.isEmpty) {
+ Expanded(sub.toList)
+ } else {
+ ExpandFailure()
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 0a402e5db9cbfce350bdd69302479f6aa9b636df..624b6a178e01c71090cb94823b56364900743676 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -22,7 +22,7 @@ class Synthesizer(val context : LeonContext,
val solver: Solver,
val program: Program,
val problem: Problem,
- val rules: Set[Rule],
+ val rules: Seq[Rule],
val options: SynthesizerOptions) {
protected[synthesis] val reporter = context.reporter
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 898f1ea05fa8eb74f949dc6093bbce51df2e7147..cab8ea72c20094db0018dd2ad97f74c982a2c5a9 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") {
+case object Assert extends NormalizingRule("Assert") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.phi match {
case TopLevelAnds(exprs) =>
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 42c931f5996bbd8d31c40b6bcb0be4e82f6ad0c7..d245e7bb2ee45030442ff0bf41beae33c066a28e 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") {
+case object OnePoint extends NormalizingRule("One-point") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index c5ddd02ef6845ef46c2b60af41e4444b4fc2133c..2ae957da30dc98e0b5e5903c331a08a9ac089cd7 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") {
+case object UnconstrainedOutput extends NormalizingRule("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/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index b44ad3411529237a12f1dc3acc53db19a5dd3954..b97ff9033b44c7e926c86362ace2fb6497399e65 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") {
+case object UnusedInput extends NormalizingRule("UnusedInput") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc)