From 9a05ae052faa79d2085c3a8f458b6063493bc8d0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 19 Nov 2012 14:19:40 +0100
Subject: [PATCH] Make RuleInapplicable a RuleAlternatives with no alternative
---
src/main/scala/leon/synthesis/Rules.scala | 7 +++++--
src/main/scala/leon/synthesis/Task.scala | 8 +++++---
.../leon/synthesis/heuristics/ADTInduction.scala | 4 ++--
.../leon/synthesis/heuristics/IntInduction.scala | 2 +-
.../synthesis/heuristics/OptimisticInjection.scala | 2 +-
.../synthesis/heuristics/SelectiveInlining.scala | 2 +-
src/main/scala/leon/synthesis/rules/ADTDual.scala | 2 +-
src/main/scala/leon/synthesis/rules/ADTSplit.scala | 14 ++++++++------
src/main/scala/leon/synthesis/rules/Assert.scala | 4 ++--
.../scala/leon/synthesis/rules/CaseSplit.scala | 4 ++--
src/main/scala/leon/synthesis/rules/Cegis.scala | 2 +-
.../scala/leon/synthesis/rules/EqualitySplit.scala | 14 ++++++++------
src/main/scala/leon/synthesis/rules/Ground.scala | 4 ++--
.../leon/synthesis/rules/IntegerEquation.scala | 2 +-
.../leon/synthesis/rules/IntegerInequalities.scala | 2 +-
src/main/scala/leon/synthesis/rules/OnePoint.scala | 2 +-
.../leon/synthesis/rules/OptimisticGround.scala | 10 +++++-----
.../leon/synthesis/rules/UnconstrainedOutput.scala | 2 +-
.../scala/leon/synthesis/rules/Unification.scala | 4 ++--
.../scala/leon/synthesis/rules/UnusedInput.scala | 2 +-
20 files changed, 51 insertions(+), 42 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index f6b957d1d..ea4271b45 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -27,14 +27,17 @@ object Rules {
}
sealed abstract class RuleResult
-case object RuleInapplicable extends RuleResult
case class RuleSuccess(solution: Solution) extends RuleResult
-case class RuleAlternatives(steps: Set[RuleMultiSteps]) extends RuleResult
+case class RuleAlternatives(steps: Traversable[RuleMultiSteps]) extends RuleResult
case class RuleMultiSteps(subProblems: List[Problem],
interSteps: List[List[Solution] => List[Problem]],
onSuccess: List[Solution] => (Solution, Boolean))
+object RuleInapplicable {
+ def apply() = RuleAlternatives(Seq())
+}
+
object RuleStep {
def apply(subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
RuleMultiSteps(subProblems, Nil, onSuccess.andThen((_, true)))
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 2e565bbad..260745880 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -27,7 +27,7 @@ class Task(synth: Synthesizer,
var solution: Option[Solution] = None
var solver: Option[RuleApplication] = None
- var alternatives = Set[RuleApplication]()
+ var alternatives = Traversable[RuleApplication]()
var minComplexity: AbsSolComplexity = new FixedSolComplexity(0)
@@ -109,12 +109,14 @@ class Task(synth: Synthesizer,
Nil
+ case RuleAlternatives(xs) if xs.isEmpty =>
+ // Inapplicable
+ Nil
+
case RuleAlternatives(steps) =>
this.alternatives = steps.map( step => new RuleApplication(step.subProblems, step.interSteps, step.onSuccess) )
this.alternatives.flatMap(_.initProblems).toList
- case RuleInapplicable =>
- Nil
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 064163d0b..90b4ebd22 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -100,10 +100,10 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
HeuristicOneStep(synth, p, subProblemsInfo.map(_._1).toList, onSuccess)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index c1000f824..a82eae8f7 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -58,7 +58,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50)
HeuristicOneStep(synth, p, List(subBase, subGT, subLT), onSuccess)
case _ =>
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index cb6682fcc..8f3e65195 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -40,7 +40,7 @@ class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", syn
HeuristicOneStep(synth, p, List(sub), forward)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 60c066e5f..6ee4935f5 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -40,7 +40,7 @@ class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth,
HeuristicOneStep(synth, p, List(sub), forward)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 37d6cf63f..1cf0a71f1 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -28,7 +28,7 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
RuleOneStep(List(sub), forward)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 6d43a4a52..41236da02 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -13,7 +13,7 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
- val candidate = p.as.collect {
+ val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
val optCases = for (dcd <- cd.knownDescendents) yield dcd match {
@@ -44,8 +44,8 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
}
- candidate.find(_.isDefined) match {
- case Some(Some((id, cases))) =>
+ val steps = candidates.collect{ _ match {
+ case Some((id, cases)) =>
val oas = p.as.filter(_ != id)
val subInfo = for(ccd <- cases) yield {
@@ -72,9 +72,11 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
}
- RuleOneStep(subInfo.map(_._2).toList, onSuccess)
+ Some(RuleStep(subInfo.map(_._2).toList, onSuccess))
case _ =>
- RuleInapplicable
- }
+ None
+ }}.flatten
+
+ RuleAlternatives(steps)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 814632bce..29514b2b3 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -25,10 +25,10 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
RuleOneStep(List(sub), forward)
}
} else {
- RuleInapplicable
+ RuleInapplicable()
}
case _ =>
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index dcd7e6835..42d7e5095 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -10,7 +10,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
p.phi match {
- case Or(Seq(o1, o2)) =>
+ case Or(o1 :: o2 :: _) =>
val sub1 = Problem(p.as, p.c, o1, p.xs)
val sub2 = Problem(p.as, p.c, o2, p.xs)
@@ -21,7 +21,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
RuleOneStep(List(sub1, sub2), onSuccess)
case _ =>
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 307840d69..14bf62a17 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -213,6 +213,6 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
unrolings += 1
} while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && synth.continue)
- result.getOrElse(RuleInapplicable)
+ result.getOrElse(RuleInapplicable())
}
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index fe0214362..8cd63ef80 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -12,7 +12,7 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
- val candidate = p.as.groupBy(_.getType).map(_._2.toList).find {
+ val candidates = p.as.groupBy(_.getType).map(_._2.toList).filter {
case List(a1, a2) =>
val toValEQ = Implies(p.c, Equals(Variable(a1), Variable(a2)))
@@ -37,8 +37,8 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
}
- candidate match {
- case Some(List(a1, a2)) =>
+ val steps = candidates.map(_ match {
+ case List(a1, a2) =>
val sub1 = p.copy(c = And(Equals(Variable(a1), Variable(a2)), p.c))
val sub2 = p.copy(c = And(Not(Equals(Variable(a1), Variable(a2))), p.c))
@@ -50,9 +50,11 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
Solution.none
}
- RuleOneStep(List(sub1, sub2), onSuccess)
+ Some(RuleStep(List(sub1, sub2), onSuccess))
case _ =>
- RuleInapplicable
- }
+ None
+ }).flatten
+
+ RuleAlternatives(steps)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 122829442..ddb4c7b6d 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -21,10 +21,10 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
case (Some(false), model) =>
RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
case _ =>
- RuleInapplicable
+ RuleInapplicable()
}
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index bb2005f9d..a8af1d203 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -43,7 +43,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
allOthers = allOthers ++ candidates
optionNormalizedEq match {
- case None => RuleInapplicable
+ case None => RuleInapplicable()
case Some(normalizedEq0) => {
val eqas = problem.as.toSet.intersect(vars)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 760891e0c..80b340595 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -31,7 +31,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
val ineqVars = lhsSides.foldLeft(Set[Identifier]())((acc, lhs) => acc ++ variablesOf(lhs))
val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains(_))
- if(candidateVars.isEmpty) RuleInapplicable else {
+ if(candidateVars.isEmpty) RuleInapplicable() else {
val processedVar = candidateVars.head
val otherVars: List[Identifier] = problem.xs.filterNot(_ == processedVar)
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 1ee39b2d1..40f7da864 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -40,7 +40,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
RuleOneStep(List(newProblem), onSuccess)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 193380720..390f41c39 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -42,25 +42,25 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
case _ =>
- result = Some(RuleInapplicable)
+ result = Some(RuleInapplicable())
}
case (Some(false), _) =>
if (predicates.isEmpty) {
result = Some(RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
- result = Some(RuleInapplicable)
+ result = Some(RuleInapplicable())
}
case _ =>
- result = Some(RuleInapplicable)
+ result = Some(RuleInapplicable())
}
i += 1
}
- result.getOrElse(RuleInapplicable)
+ result.getOrElse(RuleInapplicable())
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index a804d9cfc..021a68204 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -23,7 +23,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
RuleOneStep(List(sub), onSuccess)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 90a5c8741..e1412874f 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -31,7 +31,7 @@ object Unification {
RuleOneStep(List(sub), forward)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
@@ -56,7 +56,7 @@ object Unification {
RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index e9e0c18d6..482d594a1 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -16,7 +16,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 100) {
RuleOneStep(List(sub), forward)
} else {
- RuleInapplicable
+ RuleInapplicable()
}
}
}
--
GitLab