From 7378ba6f2446fa9e93649ccfbd5c695cf491b636 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 6 Dec 2012 17:02:18 +0100
Subject: [PATCH] Rework the semantics of rules, their
applications/instantiation, results
---
src/main/scala/leon/synthesis/CostModel.scala | 6 +-
.../scala/leon/synthesis/Heuristics.scala | 31 ++++-----
.../scala/leon/synthesis/ParallelSearch.scala | 4 +-
src/main/scala/leon/synthesis/Rules.scala | 66 ++++++++++---------
.../scala/leon/synthesis/SimpleSearch.scala | 8 +--
.../synthesis/heuristics/ADTInduction.scala | 6 +-
.../synthesis/heuristics/IntInduction.scala | 6 +-
.../heuristics/OptimisticInjection.scala | 6 +-
.../heuristics/SelectiveInlining.scala | 6 +-
.../scala/leon/synthesis/rules/ADTDual.scala | 6 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 8 +--
.../scala/leon/synthesis/rules/Assert.scala | 12 ++--
.../leon/synthesis/rules/CaseSplit.scala | 6 +-
.../scala/leon/synthesis/rules/Cegis.scala | 9 ++-
.../leon/synthesis/rules/Disunification.scala | 6 +-
.../leon/synthesis/rules/EqualitySplit.scala | 8 +--
.../scala/leon/synthesis/rules/Ground.scala | 12 ++--
.../synthesis/rules/IntegerEquation.scala | 10 ++-
.../synthesis/rules/IntegerInequalities.scala | 10 +--
.../scala/leon/synthesis/rules/OnePoint.scala | 6 +-
.../synthesis/rules/OptimisticGround.scala | 26 ++++----
.../synthesis/rules/UnconstrainedOutput.scala | 7 +-
.../leon/synthesis/rules/Unification.scala | 12 ++--
.../leon/synthesis/rules/UnusedInput.scala | 6 +-
.../leon/synthesis/search/AndOrGraph.scala | 4 +-
.../search/AndOrGraphPartialSolution.scala | 2 +-
26 files changed, 144 insertions(+), 145 deletions(-)
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index 447da1fb9..e997d9976 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -10,11 +10,11 @@ abstract class CostModel(val name: String) {
def solutionCost(s: Solution): Cost
def problemCost(p: Problem): Cost
- def ruleAppCost(r: Rule, app: RuleApplication): Cost = new Cost {
- val subSols = (1 to app.subProblemsCount).map {i => Solution.simplest }.toList
+ def ruleAppCost(r: Rule, app: RuleInstantiation): Cost = new Cost {
+ val subSols = (1 to app.onSuccess.arity).map {i => Solution.simplest }.toList
val simpleSol = app.onSuccess(subSols)
- val value = solutionCost(simpleSol).value
+ val value = simpleSol.map(solutionCost(_).value).getOrElse(0)
}
}
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index f8dc04423..706ed0f6c 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -21,34 +21,31 @@ trait Heuristic {
}
-object HeuristicStep {
- def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Solution = {
- //sctx here is unsafe to use in parallel. onSuccess should take a sctx for
- //this to be possible
-
+object HeuristicInstantiation {
+ def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Option[Solution] = {
//sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
// case (Some(true), model) =>
// sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
// sctx.reporter.warning(" - problem: "+problem)
// sctx.reporter.warning(" - precondition: "+s.pre)
- // s
+ // None
// case _ =>
- // s
+ // Some(s)
//}
- s
+
+ Some(s)
}
- def apply(sctx: SynthesisContext, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- new RuleApplication(subProblems.size, onSuccess.andThen(verifyPre(sctx, problem))) {
- def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems, onSuccess)
+ def apply(problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ val builder = new SolutionBuilder(subProblems.size) {
+ def apply(sols: List[Solution]) = {
+ Some(onSuccess(sols))
+ }
}
- }
-}
+ new RuleInstantiation(builder) {
+ def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems)
-object HeuristicFastStep {
- def apply(sctx: SynthesisContext, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleResult(List(HeuristicStep(sctx, problem, subProblems, onSuccess)))
+ }
}
}
-
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index 31ddf1fbb..0c48bd42a 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -34,7 +34,7 @@ class ParallelSearch(synth: Synthesizer,
}
ExpandSuccess(sol)
- case RuleDecomposed(sub, onSuccess) =>
+ case RuleDecomposed(sub) =>
synth.synchronized {
info(prefix+"Got: "+t.problem)
info(prefix+"Decomposed into:")
@@ -52,7 +52,7 @@ class ParallelSearch(synth: Synthesizer,
def expandOrTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskTryRules) = {
val sub = rules.flatMap { r =>
- r.attemptToApplyOn(sctx, t.p).alternatives.map(TaskRunRule(t.p, r, _))
+ r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _))
}
if (!sub.isEmpty) {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 3d2836c89..af348baf8 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -27,54 +27,56 @@ object Rules {
)
}
-case class RuleResult(alternatives: Traversable[RuleApplication])
-object RuleInapplicable extends RuleResult(List())
+abstract class SolutionBuilder(val arity: Int) {
+ def apply(sols: List[Solution]): Option[Solution]
+}
-abstract class RuleApplication(val subProblemsCount: Int,
- val onSuccess: List[Solution] => Solution) {
+class SolutionCombiner(arity: Int, f: List[Solution] => Solution) extends SolutionBuilder(arity) {
+ def apply(sols: List[Solution]) = {
+ assert(sols.size == arity)
+ Some(f(sols))
+ }
+}
+object SolutionBuilder {
+ val none = new SolutionBuilder(0) {
+ def apply(sols: List[Solution]) = None
+ }
+}
+
+abstract class RuleInstantiation(val onSuccess: SolutionBuilder) {
def apply(sctx: SynthesisContext): RuleApplicationResult
}
-abstract class RuleImmediateApplication extends RuleApplication(0, s => Solution.simplest)
+//abstract class RuleApplication(val subProblemsCount: Int,
+// val onSuccess: List[Solution] => Solution) {
+//
+// def apply(sctx: SynthesisContext): RuleApplicationResult
+//}
+//
+//abstract class RuleImmediateApplication extends RuleApplication(0, s => Solution.simplest)
sealed abstract class RuleApplicationResult
-case class RuleSuccess(solution: Solution) extends RuleApplicationResult
-case class RuleDecomposed(sub: List[Problem], onSuccess: List[Solution] => Solution) extends RuleApplicationResult
-case object RuleApplicationImpossible extends RuleApplicationResult
+case class RuleSuccess(solution: Solution) extends RuleApplicationResult
+case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
+case object RuleApplicationImpossible extends RuleApplicationResult
-object RuleFastApplication {
- def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
- new RuleApplication(sub.size, onSuccess) {
- def apply(sctx: SynthesisContext) = RuleDecomposed(sub, onSuccess)
+object RuleInstantiation {
+ def immediateDecomp(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
+ new RuleInstantiation(new SolutionCombiner(sub.size, onSuccess)) {
+ def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
}
}
-}
-
-object RuleFastInapplicable {
- def apply() = {
- RuleResult(List(new RuleApplication(0, ls => Solution.simplest) {
- def apply(sctx: SynthesisContext) = RuleApplicationImpossible
- }))
- }
-}
-object RuleFastStep {
- def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleResult(List(RuleFastApplication(sub, onSuccess)))
- }
-}
-
-object RuleFastSuccess {
- def apply(solution: Solution) = {
- RuleResult(List(new RuleApplication(0, ls => solution) {
+ def immediateSuccess(solution: Solution) = {
+ new RuleInstantiation(new SolutionCombiner(0, ls => solution)) {
def apply(sctx: SynthesisContext) = RuleSuccess(solution)
- }))
+ }
}
}
abstract class Rule(val name: String, val priority: Priority) {
- def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult
+ 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)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index d92de1d1e..bc254e2fa 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -3,8 +3,8 @@ package synthesis
import synthesis.search._
-case class TaskRunRule(problem: Problem, rule: Rule, app: RuleApplication) extends AOAndTask[Solution] {
- def composeSolution(sols: List[Solution]): Solution = {
+case class TaskRunRule(problem: Problem, rule: Rule, app: RuleInstantiation) extends AOAndTask[Solution] {
+ def composeSolution(sols: List[Solution]): Option[Solution] = {
app.onSuccess(sols)
}
@@ -44,7 +44,7 @@ class SimpleSearch(synth: Synthesizer,
info(prefix+"Solved with: "+sol)
ExpandSuccess(sol)
- case RuleDecomposed(sub, onSuccess) =>
+ case RuleDecomposed(sub) =>
info(prefix+"Got: "+t.problem)
info(prefix+"Decomposed into:")
for(p <- sub) {
@@ -59,7 +59,7 @@ class SimpleSearch(synth: Synthesizer,
}
def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
- val sub = rules.flatMap ( r => r.attemptToApplyOn(sctx, t.p).alternatives.map(TaskRunRule(t.p, r, _)) )
+ val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _)) )
if (!sub.isEmpty) {
Expanded(sub.toList)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index aec4b610b..02bff49b4 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -10,7 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
case object ADTInduction extends Rule("ADT Induction", 80) with Heuristic {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val candidates = p.as.collect {
case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
}
@@ -97,12 +97,12 @@ case object ADTInduction extends Rule("ADT Induction", 80) with Heuristic {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, p.as.map(Variable(_))))
}
- Some(HeuristicStep(sctx, p, subProblemsInfo.map(_._1).toList, onSuccess))
+ Some(HeuristicInstantiation(p, subProblemsInfo.map(_._1).toList, onSuccess))
} else {
None
}
}
- RuleResult(steps.flatten)
+ steps.flatten
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index 9d708689a..a4c7f9cf2 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -10,7 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
case object IntInduction extends Rule("Int Induction", 50) with Heuristic {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.as match {
case List(IsTyped(origId, Int32Type)) =>
val tpe = TupleType(p.xs.map(_.getType))
@@ -54,9 +54,9 @@ case object IntInduction extends Rule("Int Induction", 50) with Heuristic {
Solution.none
}
- HeuristicFastStep(sctx, p, List(subBase, subGT, subLT), onSuccess)
+ Some(HeuristicInstantiation(p, List(subBase, subGT, subLT), onSuccess))
case _ =>
- RuleInapplicable
+ None
}
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index 1378649d4..494e0979a 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -10,7 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
case object OptimisticInjection extends Rule("Opt. Injection", 50) with Heuristic {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
val eqfuncalls = exprs.collect{
@@ -36,9 +36,9 @@ case object OptimisticInjection extends Rule("Opt. Injection", 50) with Heuristi
val sub = p.copy(phi = And(newExprs))
- HeuristicFastStep(sctx, p, List(sub), forward)
+ Some(HeuristicInstantiation(p, List(sub), forward))
} else {
- RuleInapplicable
+ None
}
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 5961d6777..44ceb7879 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -10,7 +10,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
case object SelectiveInlining extends Rule("Sel. Inlining", 20) with Heuristic {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
val eqfuncalls = exprs.collect{
@@ -36,9 +36,9 @@ case object SelectiveInlining extends Rule("Sel. Inlining", 20) with Heuristic {
val sub = p.copy(phi = And(newExprs))
- HeuristicFastStep(sctx, p, List(sub), forward)
+ Some(HeuristicInstantiation(p, List(sub), forward))
} else {
- RuleInapplicable
+ None
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 0660f87a8..78573c819 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -7,7 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
case object ADTDual extends Rule("ADTDual", 200) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val xs = p.xs.toSet
val as = p.as.toSet
@@ -24,9 +24,9 @@ case object ADTDual extends Rule("ADTDual", 200) {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- RuleFastStep(List(sub), forward)
+ List(RuleInstantiation.immediateDecomp(List(sub), forward))
} else {
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 6a4d88c7a..631fe979a 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -10,7 +10,7 @@ import purescala.Extractors._
import purescala.Definitions._
case object ADTSplit extends Rule("ADT Split.", 70) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
@@ -42,7 +42,7 @@ case object ADTSplit extends Rule("ADT Split.", 70) {
}
- val steps = candidates.collect{ _ match {
+ candidates.collect{ _ match {
case Some((id, cases)) =>
val oas = p.as.filter(_ != id)
@@ -70,11 +70,9 @@ case object ADTSplit extends Rule("ADT Split.", 70) {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
}
- Some(RuleFastApplication(subInfo.map(_._2).toList, onSuccess))
+ Some(RuleInstantiation.immediateDecomp(subInfo.map(_._2).toList, onSuccess))
case _ =>
None
}}.flatten
-
- RuleResult(steps)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 04459435e..962e090ae 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -7,7 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
case object Assert extends Rule("Assert", 200) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.phi match {
case TopLevelAnds(exprs) =>
val xsSet = p.xs.toSet
@@ -16,20 +16,20 @@ case object Assert extends Rule("Assert", 200) {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- RuleFastSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
+ List(RuleInstantiation.immediateSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id)))))))
} else {
val sub = p.copy(pc = And(p.pc +: exprsA), phi = And(others))
- RuleFastStep(List(sub), {
+ List(RuleInstantiation.immediateDecomp(List(sub), {
case Solution(pre, defs, term) :: Nil => Solution(And(exprsA :+ pre), defs, term)
case _ => Solution.none
- })
+ }))
}
} else {
- RuleInapplicable
+ Nil
}
case _ =>
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 50b769c70..a2627256b 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -7,7 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
case object CaseSplit extends Rule("Case-Split", 200) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.phi match {
case Or(o1 :: o2 :: _) =>
val sub1 = Problem(p.as, p.pc, o1, p.xs)
@@ -18,9 +18,9 @@ case object CaseSplit extends Rule("Case-Split", 200) {
case _ => Solution.none
}
- RuleFastStep(List(sub1, sub2), onSuccess)
+ List(RuleInstantiation.immediateDecomp(List(sub1, sub2), onSuccess))
case _ =>
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index d3665ef42..c1029c5db 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -12,7 +12,7 @@ import purescala.Extractors._
import solvers.z3.FairZ3Solver
case object CEGIS extends Rule("CEGIS", 150) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
var generators = Map[TypeTree, Generator]()
@@ -122,7 +122,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
val (exprsA, others) = ands.partition(e => (variablesOf(e) & xsSet).isEmpty)
if (exprsA.isEmpty) {
- val res = new RuleImmediateApplication {
+ val res = new RuleInstantiation(SolutionBuilder.none) {
def apply(sctx: SynthesisContext) = {
var result: Option[RuleApplicationResult] = None
@@ -272,12 +272,11 @@ case object CEGIS extends Rule("CEGIS", 150) {
e.printStackTrace
RuleApplicationImpossible
}
-
}
}
- RuleResult(List(res))
+ List(res)
} else {
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 7bce9d378..53963b502 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -9,7 +9,7 @@ import purescala.Extractors._
object Disunification {
case object Decomp extends Rule("Disunif. Decomp.", 200) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
val (toRemove, toAdd) = exprs.collect {
@@ -26,9 +26,9 @@ object Disunification {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = Or((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- RuleFastStep(List(sub), forward)
+ List(RuleInstantiation.immediateDecomp(List(sub), forward))
} else {
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index f74c9fc55..eebab17e9 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
import purescala.Extractors._
case object EqualitySplit extends Rule("Eq. Split.", 90) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val candidates = p.as.groupBy(_.getType).map(_._2.toList).filter {
case List(a1, a2) =>
val toValEQ = Implies(p.pc, Equals(Variable(a1), Variable(a2)))
@@ -35,7 +35,7 @@ case object EqualitySplit extends Rule("Eq. Split.", 90) {
}
- val steps = candidates.map(_ match {
+ candidates.map(_ match {
case List(a1, a2) =>
val sub1 = p.copy(pc = And(Equals(Variable(a1), Variable(a2)), p.pc))
@@ -48,11 +48,9 @@ case object EqualitySplit extends Rule("Eq. Split.", 90) {
Solution.none
}
- Some(RuleFastApplication(List(sub1, sub2), onSuccess))
+ Some(RuleInstantiation.immediateDecomp(List(sub1, sub2), onSuccess))
case _ =>
None
}).flatten
-
- RuleResult(steps)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index f79af5afb..97c0c8366 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -8,21 +8,23 @@ import purescala.TreeOps._
import purescala.Extractors._
case object Ground extends Rule("Ground", 500) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
val tpe = TupleType(p.xs.map(_.getType))
sctx.solver.solveSAT(p.phi) match {
case (Some(true), model) =>
- RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
+ val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
+ Some(RuleInstantiation.immediateSuccess(sol))
case (Some(false), model) =>
- RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
+ val sol = Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))
+ Some(RuleInstantiation.immediateSuccess(sol))
case _ =>
- RuleInapplicable
+ None
}
} else {
- RuleInapplicable
+ None
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 9fc9be76c..00d21c604 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -12,7 +12,7 @@ import purescala.Definitions._
import LinearEquations.elimVariable
case object IntegerEquation extends Rule("Integer Equation", 600) {
- def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult = if(!problem.xs.exists(_.getType == Int32Type)) RuleInapplicable else {
+ def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = if(!problem.xs.exists(_.getType == Int32Type)) Nil else {
val TopLevelAnds(exprs) = problem.phi
@@ -41,7 +41,7 @@ case object IntegerEquation extends Rule("Integer Equation", 600) {
allOthers = allOthers ++ candidates
optionNormalizedEq match {
- case None => RuleInapplicable
+ case None => Nil
case Some(normalizedEq0) => {
val eqas = problem.as.toSet.intersect(vars)
@@ -60,7 +60,7 @@ case object IntegerEquation extends Rule("Integer Equation", 600) {
case _ => Solution.none
}
- RuleFastStep(List(newProblem), onSuccess)
+ List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
} else {
val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
@@ -103,10 +103,8 @@ case object IntegerEquation extends Rule("Integer Equation", 600) {
case _ => Solution.none
}
- RuleFastStep(List(newProblem), onSuccess)
+ List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
}
-
-
}
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 6d29637b2..7cb6b28cb 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -13,7 +13,7 @@ import LinearEquations.elimVariable
import leon.synthesis.Algebra.lcm
case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
- def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = problem.phi
//assume that we only have inequalities
@@ -32,7 +32,9 @@ case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
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) {
+ Nil
+ } else {
val processedVar: Identifier = candidateVars.map(v => {
val normalizedLhs: List[List[Expr]] = lhsSides.map(linearArithmeticForm(_, Array(v)).toList)
if(normalizedLhs.isEmpty)
@@ -129,7 +131,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
val constraints: List[Expr] = for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds)
yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc)))
val pre = And(exprNotUsed ++ constraints)
- RuleFastSuccess(Solution(pre, Set(), witness))
+ List(RuleInstantiation.immediateSuccess(Solution(pre, Set(), witness)))
} else {
val involvedVariables = (upperBounds++lowerBounds).foldLeft(Set[Identifier]())((acc, t) => {
@@ -198,7 +200,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
case _ => Solution.none
}
- RuleFastStep(List(subProblem), onSuccess)
+ List(RuleInstantiation.immediateDecomp(List(subProblem), onSuccess))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 412796a98..76aedbdc5 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -7,7 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
case object OnePoint extends Rule("One-point", 300) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
val candidates = exprs.collect {
@@ -35,9 +35,9 @@ case object OnePoint extends Rule("One-point", 300) {
case _ => Solution.none
}
- RuleFastStep(List(newProblem), onSuccess)
+ List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
} else {
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 57e179ef3..0ddce7824 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -8,7 +8,7 @@ import purescala.TreeOps._
import purescala.Extractors._
case object OptimisticGround extends Rule("Optimistic Ground", 150) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (!p.as.isEmpty && !p.xs.isEmpty) {
val xss = p.xs.toSet
val ass = p.as.toSet
@@ -18,10 +18,11 @@ case object OptimisticGround extends Rule("Optimistic Ground", 150) {
var i = 0;
var maxTries = 3;
- var result: Option[RuleResult] = None
- var predicates: Seq[Expr] = Seq()
+ var result: Option[RuleInstantiation] = None
+ var continue = true
+ var predicates: Seq[Expr] = Seq()
- while (result.isEmpty && i < maxTries) {
+ while (result.isEmpty && i < maxTries && continue) {
val phi = And(p.pc +: p.phi +: predicates)
//println("SOLVING " + phi + " ...")
sctx.solver.solveSAT(phi) match {
@@ -37,28 +38,31 @@ case object OptimisticGround extends Rule("Optimistic Ground", 150) {
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
case (Some(false), _) =>
- result = Some(RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+ result = Some(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
case _ =>
- result = Some(RuleFastInapplicable())
+ continue = false
+ result = None
}
case (Some(false), _) =>
if (predicates.isEmpty) {
- result = Some(RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
+ result = Some(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
- result = Some(RuleFastInapplicable())
+ continue = false
+ result = None
}
case _ =>
- result = Some(RuleFastInapplicable())
+ continue = false
+ result = None
}
i += 1
}
- result.getOrElse(RuleFastInapplicable())
+ result
} else {
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 8adc96ba1..808a76dd8 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -7,7 +7,7 @@ import purescala.TreeOps._
import purescala.Extractors._
case object UnconstrainedOutput extends Rule("Unconstr.Output", 100) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val unconstr = p.xs.toSet -- variablesOf(p.phi)
if (!unconstr.isEmpty) {
@@ -20,11 +20,10 @@ case object UnconstrainedOutput extends Rule("Unconstr.Output", 100) {
Solution.none
}
- RuleFastStep(List(sub), onSuccess)
+ List(RuleInstantiation.immediateDecomp(List(sub), onSuccess))
} else {
- RuleInapplicable
+ Nil
}
-
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index c5ee4c320..fd278ff24 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -9,7 +9,7 @@ import purescala.Extractors._
object Unification {
case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.", 200) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
val (toRemove, toAdd) = exprs.collect {
@@ -27,9 +27,9 @@ object Unification {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- RuleFastStep(List(sub), forward)
+ List(RuleInstantiation.immediateDecomp(List(sub), forward))
} else {
- RuleInapplicable
+ Nil
}
}
}
@@ -37,7 +37,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) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
val isImpossible = exprs.exists {
@@ -52,9 +52,9 @@ object Unification {
if (isImpossible) {
val tpe = TupleType(p.xs.map(_.getType))
- RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
+ List(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 03f8aeef8..d9b26efed 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -7,15 +7,15 @@ import purescala.TreeOps._
import purescala.Extractors._
case object UnusedInput extends Rule("UnusedInput", 100) {
- def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc)
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
- RuleFastStep(List(sub), forward)
+ List(RuleInstantiation.immediateDecomp(List(sub), forward))
} else {
- RuleInapplicable
+ Nil
}
}
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 2ac6881a2..5a61217a0 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -4,7 +4,7 @@ trait AOTask[S] {
}
trait AOAndTask[S] extends AOTask[S] {
- def composeSolution(sols: List[S]): S
+ def composeSolution(sols: List[S]): Option[S]
}
trait AOOrTask[S] extends AOTask[S] {
@@ -88,7 +88,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
subSolutions += sub.task -> sol
if (subSolutions.size == subProblems.size) {
- solution = Some(task.composeSolution(subTasks.map(subSolutions)))
+ solution = task.composeSolution(subTasks.map(subSolutions))
updateMin()
notifyParent(solution.get)
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
index 2406bc1ca..d4d38dd77 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
@@ -17,7 +17,7 @@ class AndOrGraphPartialSolution[AT <: AOAndTask[S],
case l: g.AndLeaf =>
missing(t.task)
case n: g.AndNode =>
- n.task.composeSolution(n.subProblems.values.map(solveOr(_)).toList)
+ n.task.composeSolution(n.subProblems.values.map(solveOr(_)).toList).getOrElse(missing(t.task))
}
}
}
--
GitLab