diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index f6b957d1df716e33e349b96c2b535e92263d7010..ea4271b458582be52b34e7e0e8f9ce0009074390 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 2e565bbadf9207bb3f6b9f71e8745bbb12b7fb4e..26074588029dc3486fc3aa2e55585fb01a10fd0f 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 064163d0b1ab085dbf722f46be15bdc23513ed6d..90b4ebd227f0eb13976e0c7663ebf8c5a2c9a212 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 c1000f82486286e42eb57f12df4087d24b6e5b5c..a82eae8f74153c04370f747354319f4eb4a0afee 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 cb6682fcc0c7b7be76b3117dbd2063fca4726f8d..8f3e6519514522dfe76302b61d3ecbbf9d2b8559 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 60c066e5f0366fa0d96efcc27d175d6177d3ddf2..6ee4935f5f8eabb5510aafbd586e075d79a67368 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 37d6cf63fbf52f77b688cec17a7c5e58b3f0bd32..1cf0a71f17b2a786d7405c4591439d087ab85962 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 6d43a4a52d3edeb680eb26a08d70bd02e340fb64..41236da021169d69342f2926970caab68bc46c1f 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 814632bce81fc96aeb0009e753af5577aeefad44..29514b2b37dfda88b580d2b67c01ca70182bc1c2 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 dcd7e6835b2c93abe6ed45f24f9c7aed87e3c80e..42d7e509506e2d472604fada4821837a17a80cf3 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 307840d69bd3589781bb1dbd168a056f8e27e26a..14bf62a1725d3f3e283ca6d64f3de09003379fb8 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 fe0214362caf0d3ccecf96692b0ce7c19b33d722..8cd63ef801d5bcd24f467dc152fc79324c0fb7d3 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 122829442033c802a5fd0ec82647a0b86f0c1f05..ddb4c7b6df965311a7eb3ac02165d063ff4cd9a5 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 bb2005f9d359b219a22d467af059b24f91b744e5..a8af1d203c72cf275d1f5a3031b576d4fa4f8415 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 760891e0cdd195a74d509749e7b71c40386846ea..80b340595f1528caf21860548f54b2a0e450ad5a 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 1ee39b2d1c1b4fbd42d7d9b80de0a15b22f09dd6..40f7da86443a8d2bea369cac6351b58837b5517f 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 1933807202ab826e82ea1e3407d54b6b9b2c9ac8..390f41c39e1d761c62c2c8c888be588f28b17980 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 a804d9cfc4d8456b0bf14ed682cb6f26e993226f..021a6820437d4fa1f87fa91139f1d22d4e3bba79 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 90a5c8741887c9d764effe77d37d09e83ca7dc7c..e1412874f3d27504d1076186980d49b7cd68c8e1 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 e9e0c18d6b780ac3f43153fe07b81d8e909eb361..482d594a1ab010d4513a0b2d75da51635dac342b 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()
}
}
}