From 5ccb8ebe0aeb76c117d21d3b031a0672c48f39fc Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 23 Nov 2012 16:49:52 +0100
Subject: [PATCH] Prepare ground for parallel search
---
.../scala/leon/synthesis/Complexity.scala | 34 -----------------
.../scala/leon/synthesis/Heuristics.scala | 24 ++++++------
src/main/scala/leon/synthesis/Problem.scala | 6 +--
src/main/scala/leon/synthesis/Rules.scala | 38 +++++++++----------
.../leon/synthesis/SynthesisContext.scala | 16 ++++++++
.../scala/leon/synthesis/Synthesizer.scala | 13 ++++---
.../synthesis/heuristics/ADTInduction.scala | 8 ++--
.../synthesis/heuristics/IntInduction.scala | 12 +++---
.../heuristics/OptimisticInjection.scala | 6 +--
.../heuristics/SelectiveInlining.scala | 6 +--
.../scala/leon/synthesis/rules/ADTDual.scala | 4 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 10 ++---
.../scala/leon/synthesis/rules/Assert.scala | 6 +--
.../leon/synthesis/rules/CaseSplit.scala | 8 ++--
.../scala/leon/synthesis/rules/Cegis.scala | 26 ++++++-------
.../leon/synthesis/rules/Disunification.scala | 4 +-
.../leon/synthesis/rules/EqualitySplit.scala | 16 ++++----
.../scala/leon/synthesis/rules/Ground.scala | 6 +--
.../synthesis/rules/IntegerEquation.scala | 8 ++--
.../synthesis/rules/IntegerInequalities.scala | 6 +--
.../scala/leon/synthesis/rules/OnePoint.scala | 6 +--
.../synthesis/rules/OptimisticGround.scala | 10 ++---
.../synthesis/rules/UnconstrainedOutput.scala | 4 +-
.../leon/synthesis/rules/Unification.scala | 8 ++--
.../leon/synthesis/rules/UnusedInput.scala | 6 +--
25 files changed, 136 insertions(+), 155 deletions(-)
delete mode 100644 src/main/scala/leon/synthesis/Complexity.scala
create mode 100644 src/main/scala/leon/synthesis/SynthesisContext.scala
diff --git a/src/main/scala/leon/synthesis/Complexity.scala b/src/main/scala/leon/synthesis/Complexity.scala
deleted file mode 100644
index 2f09637d4..000000000
--- a/src/main/scala/leon/synthesis/Complexity.scala
+++ /dev/null
@@ -1,34 +0,0 @@
-package leon
-package synthesis
-
-import purescala.Trees._
-import purescala.TreeOps._
-
-abstract class Complexity[T <: Complexity[T]] extends Ordered[T] {
- def compare(that: T) = this.value - that.value
-
- def value : Int
-}
-
-abstract class AbsSolComplexity extends Complexity[AbsSolComplexity] {
- def value: Int
-}
-
-case class SolComplexity(s: Solution) extends AbsSolComplexity {
- lazy val value = {
- val chooses = collectChooses(s.toExpr)
- val chooseCost = chooses.foldLeft(0)((i, c) => i + (1000 * math.pow(2, c.vars.size).toInt + formulaSize(c.pred)))
-
- formulaSize(s.toExpr) + chooseCost
- }
-}
-
-case class FixedSolComplexity(c: Int) extends AbsSolComplexity {
- val value = c
-}
-
-case class ProblemComplexity(p: Problem) extends Complexity[ProblemComplexity] {
- lazy val value = {
- math.pow(2, p.xs.size).toInt + formulaSize(p.phi)
- }
-}
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 6787da103..decfdeffb 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -6,11 +6,11 @@ import purescala.Trees._
import heuristics._
object Heuristics {
- def all = Set[Synthesizer => Rule](
- new IntInduction(_),
+ def all = Set[Rule](
+ IntInduction,
//new OptimisticInjection(_),
//new SelectiveInlining(_),
- new ADTInduction(_)
+ ADTInduction
)
}
@@ -22,20 +22,20 @@ trait Heuristic {
}
object HeuristicStep {
- def verifyPre(synth: Synthesizer, problem: Problem)(s: Solution): Solution = {
- synth.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
+ def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Solution = {
+ sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
case (Some(true), model) =>
- synth.reporter.warning("Heuristic failed to produce weakest precondition:")
- synth.reporter.warning(" - problem: "+problem)
- synth.reporter.warning(" - precondition: "+s.pre)
+ sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
+ sctx.reporter.warning(" - problem: "+problem)
+ sctx.reporter.warning(" - precondition: "+s.pre)
s
case _ =>
s
}
}
- def apply(synth: Synthesizer, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- new RuleApplication(subProblems.size, onSuccess.andThen(verifyPre(synth, problem))) {
+ def apply(sctx: SynthesisContext, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ new RuleApplication(subProblems.size, onSuccess.andThen(verifyPre(sctx, problem))) {
def apply() = RuleDecomposed(subProblems, onSuccess)
}
}
@@ -43,8 +43,8 @@ object HeuristicStep {
object HeuristicFastStep {
- def apply(synth: Synthesizer, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleResult(List(HeuristicStep(synth, problem, subProblems, onSuccess)))
+ 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/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 89b452873..0a43181e4 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -7,10 +7,8 @@ import leon.purescala.Common._
// Defines a synthesis triple of the form:
// ⟦ as ⟨ C | phi ⟩ xs ⟧
-case class Problem(as: List[Identifier], c: Expr, phi: Expr, xs: List[Identifier]) {
- override def toString = "⟦ "+as.mkString(";")+", "+c+" ᚒ ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
-
- val complexity: ProblemComplexity = ProblemComplexity(this)
+case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifier]) {
+ override def toString = "⟦ "+as.mkString(";")+", "+(if (pc != BooleanLiteral(true)) pc+" ᚒ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
}
object Problem {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 85d20e1d7..750171b1d 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -7,23 +7,23 @@ import purescala.TreeOps._
import rules._
object Rules {
- def all = Set[Synthesizer => Rule](
- new Unification.DecompTrivialClash(_),
- new Unification.OccursCheck(_), // probably useless
- new Disunification.Decomp(_),
- new ADTDual(_),
- new OnePoint(_),
- new Ground(_),
- new CaseSplit(_),
- new UnusedInput(_),
- new UnconstrainedOutput(_),
- new OptimisticGround(_),
- new EqualitySplit(_),
- new CEGIS(_),
- new Assert(_),
- new ADTSplit(_),
- new IntegerEquation(_),
- new IntegerInequalities(_)
+ def all = Set[Rule](
+ Unification.DecompTrivialClash,
+ Unification.OccursCheck, // probably useless
+ Disunification.Decomp,
+ ADTDual,
+ OnePoint,
+ Ground,
+ CaseSplit,
+ UnusedInput,
+ UnconstrainedOutput,
+ OptimisticGround,
+ EqualitySplit,
+ CEGIS,
+ Assert,
+ ADTSplit,
+ IntegerEquation,
+ IntegerInequalities
)
}
@@ -73,8 +73,8 @@ object RuleFastSuccess {
}
}
-abstract class Rule(val name: String, val synth: Synthesizer, val priority: Priority) {
- def attemptToApplyOn(problem: Problem): RuleResult
+abstract class Rule(val name: String, val priority: Priority) {
+ def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult
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/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
new file mode 100644
index 000000000..0f085f52c
--- /dev/null
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -0,0 +1,16 @@
+package leon
+package synthesis
+
+import solvers.Solver
+
+case class SynthesisContext(
+ synth: Synthesizer,
+ solver: Solver,
+ simpleSolver: Solver,
+ reporter: Reporter
+)
+
+object SynthesisContext {
+ def fromSynthesizer(synth: Synthesizer) = SynthesisContext(synth, synth.solver, synth.solver, synth.reporter)
+}
+
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index ae3717d3c..a708ecf06 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -18,20 +18,18 @@ import synthesis.search._
class Synthesizer(val reporter: Reporter,
val solver: Solver,
val problem: Problem,
- val ruleConstructors: Set[Synthesizer => Rule],
+ val rules: Set[Rule],
generateDerivationTrees: Boolean = false,
filterFuns: Option[Set[String]] = None,
firstOnly: Boolean = false,
timeoutMs: Option[Long] = None) {
import reporter.{error,warning,info,fatalError}
- val rules = ruleConstructors.map(_.apply(this))
-
var continue = true
def synthesize(): Solution = {
- val search = new AOSearch(problem, rules)
+ val search = new AOSearch(this, problem, rules)
val sigINT = new Signal("INT")
var oldHandler: SignalHandler = null
@@ -77,9 +75,12 @@ class Synthesizer(val reporter: Reporter,
override def toString = p.toString
}
- class AOSearch(problem: Problem,
+ class AOSearch(synth: Synthesizer,
+ problem: Problem,
rules: Set[Rule]) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem))) {
+ val sctx = SynthesisContext.fromSynthesizer(synth)
+
def processAndLeaf(t: TaskRunRule) = {
val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
@@ -104,7 +105,7 @@ class Synthesizer(val reporter: Reporter,
}
def processOrLeaf(t: TaskTryRules) = {
- val sub = rules.flatMap ( r => r.attemptToApplyOn(t.p).alternatives.map(TaskRunRule(t.p, r, _)) )
+ val sub = rules.flatMap ( r => r.attemptToApplyOn(sctx, t.p).alternatives.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 2117dc915..aec4b610b 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -9,8 +9,8 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80) with Heuristic {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object ADTInduction extends Rule("ADT Induction", 80) with Heuristic {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val candidates = p.as.collect {
case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
}
@@ -38,7 +38,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
if (isRecursive) {
val innerPhi = substAll(residualMap + (origId -> Variable(inductOn)), p.phi)
- val innerPC = substAll(residualMap + (origId -> Variable(inductOn)), p.c)
+ val innerPC = substAll(residualMap + (origId -> Variable(inductOn)), p.pc)
val subProblemsInfo = for (dcd <- cd.knownDescendents) yield dcd match {
case ccd : CaseClassDef =>
@@ -97,7 +97,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, p.as.map(Variable(_))))
}
- Some(HeuristicStep(synth, p, subProblemsInfo.map(_._1).toList, onSuccess))
+ Some(HeuristicStep(sctx, p, subProblemsInfo.map(_._1).toList, onSuccess))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index 28cb94845..9d708689a 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -9,8 +9,8 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50) with Heuristic {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object IntInduction extends Rule("Int Induction", 50) with Heuristic {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
p.as match {
case List(IsTyped(origId, Int32Type)) =>
val tpe = TupleType(p.xs.map(_.getType))
@@ -25,9 +25,9 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50)
val postCondGT = substAll(postXsMap + (origId -> Minus(Variable(inductOn), IntLiteral(1))), p.phi)
val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi)
- val subBase = Problem(List(), p.c, subst(origId -> IntLiteral(0), p.phi), p.xs)
- val subGT = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, p.c)), newPhi, p.xs)
- val subLT = Problem(inductOn :: postXs, And(Seq(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, p.c)), newPhi, p.xs)
+ val subBase = Problem(List(), p.pc, subst(origId -> IntLiteral(0), p.phi), p.xs)
+ val subGT = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, p.pc)), newPhi, p.xs)
+ val subLT = Problem(inductOn :: postXs, And(Seq(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, p.pc)), newPhi, p.xs)
val onSuccess: List[Solution] => Solution = {
case List(base, gt, lt) =>
@@ -54,7 +54,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50)
Solution.none
}
- HeuristicFastStep(synth, p, List(subBase, subGT, subLT), onSuccess)
+ HeuristicFastStep(sctx, p, List(subBase, subGT, subLT), onSuccess)
case _ =>
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index 85d5f34cc..1378649d4 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -9,8 +9,8 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", synth, 50) with Heuristic {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object OptimisticInjection extends Rule("Opt. Injection", 50) with Heuristic {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val eqfuncalls = exprs.collect{
@@ -36,7 +36,7 @@ class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", syn
val sub = p.copy(phi = And(newExprs))
- HeuristicFastStep(synth, p, List(sub), forward)
+ HeuristicFastStep(sctx, p, List(sub), forward)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 4fe3f764d..5961d6777 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -9,8 +9,8 @@ import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
-class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth, 20) with Heuristic {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object SelectiveInlining extends Rule("Sel. Inlining", 20) with Heuristic {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val eqfuncalls = exprs.collect{
@@ -36,7 +36,7 @@ class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth,
val sub = p.copy(phi = And(newExprs))
- HeuristicFastStep(synth, p, List(sub), forward)
+ HeuristicFastStep(sctx, p, List(sub), forward)
} else {
RuleInapplicable
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index bb4753752..0660f87a8 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -6,8 +6,8 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object ADTDual extends Rule("ADTDual", 200) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
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 39e987c25..6a4d88c7a 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -9,16 +9,16 @@ import purescala.TreeOps._
import purescala.Extractors._
import purescala.Definitions._
-class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object ADTSplit extends Rule("ADT Split.", 70) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
val optCases = for (dcd <- cd.knownDescendents) yield dcd match {
case ccd : CaseClassDef =>
- val toSat = And(p.c, Not(CaseClassInstanceOf(ccd, Variable(id))))
+ val toSat = And(p.pc, Not(CaseClassInstanceOf(ccd, Variable(id))))
- val isImplied = synth.solver.solveSAT(toSat) match {
+ val isImplied = sctx.solver.solveSAT(toSat) match {
case (Some(false), _) => true
case _ => false
}
@@ -50,7 +50,7 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
val args = ccd.fieldsIds.map(id => FreshIdentifier(id.name, true).setType(id.getType)).toList
val subPhi = subst(id -> CaseClass(ccd, args.map(Variable(_))), p.phi)
- val subProblem = Problem(args ::: oas, p.c, subPhi, p.xs)
+ val subProblem = Problem(args ::: oas, p.pc, subPhi, p.xs)
val subPattern = CaseClassPattern(None, ccd, args.map(id => WildcardPattern(Some(id))))
(ccd, subProblem, subPattern)
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index ab2e66d4b..04459435e 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -6,8 +6,8 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object Assert extends Rule("Assert", 200) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
p.phi match {
case TopLevelAnds(exprs) =>
val xsSet = p.xs.toSet
@@ -18,7 +18,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
if (others.isEmpty) {
RuleFastSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
} else {
- val sub = p.copy(c = And(p.c +: exprsA), phi = And(others))
+ val sub = p.copy(pc = And(p.pc +: exprsA), phi = And(others))
RuleFastStep(List(sub), {
case Solution(pre, defs, term) :: Nil => Solution(And(exprsA :+ pre), defs, term)
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 44f0b7bad..50b769c70 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -6,12 +6,12 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object CaseSplit extends Rule("Case-Split", 200) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
p.phi match {
case Or(o1 :: o2 :: _) =>
- val sub1 = Problem(p.as, p.c, o1, p.xs)
- val sub2 = Problem(p.as, p.c, o2, p.xs)
+ val sub1 = Problem(p.as, p.pc, o1, p.xs)
+ val sub2 = Problem(p.as, p.pc, o2, p.xs)
val onSuccess: List[Solution] => Solution = {
case List(Solution(p1, d1, t1), Solution(p2, d2, t2)) => Solution(Or(p1, p2), d1++d2, IfExpr(p1, t1, t2))
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 6b56bcc00..23d8bf2a9 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -9,8 +9,8 @@ import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object CEGIS extends Rule("CEGIS", 150) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
var generators = Map[TypeTree, Generator]()
@@ -40,7 +40,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
{ () =>
val alts: Seq[(Expr, Set[Identifier])] = cd.knownDescendents.flatMap(i => i match {
case acd: AbstractClassDef =>
- synth.reporter.error("Unnexpected abstract class in descendants!")
+ sctx.reporter.error("Unnexpected abstract class in descendants!")
None
case cd: CaseClassDef =>
val ids = cd.fieldsIds.map(i => FreshIdentifier("c", true).setType(i.getType))
@@ -50,7 +50,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
}
case _ =>
- synth.reporter.error("Can't construct generator. Unsupported type: "+t+"["+t.getClass+"]");
+ sctx.reporter.error("Can't construct generator. Unsupported type: "+t+"["+t.getClass+"]");
{ () => Nil }
}
val g = Generator(t, alternatives)
@@ -122,7 +122,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
var ass = p.as.toSet
var xss = p.xs.toSet
- var lastF = TentativeFormula(p.c, p.phi, BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
+ var lastF = TentativeFormula(p.pc, p.phi, BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
var currentF = lastF.unroll
var unrolings = 0
val maxUnrolings = 3
@@ -138,12 +138,12 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
var continue = true
- while (result.isEmpty && continue && synth.continue) {
+ while (result.isEmpty && continue && sctx.synth.continue) {
val basePhi = currentF.entireFormula
val constrainedPhi = And(basePhi +: predicates)
//println("-"*80)
//println("To satisfy: "+constrainedPhi)
- synth.solver.solveSAT(constrainedPhi) match {
+ sctx.solver.solveSAT(constrainedPhi) match {
case (Some(true), satModel) =>
//println("Found candidate!: "+satModel.filterKeys(bss))
@@ -154,7 +154,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
val counterPhi = And(Seq(currentF.pathcond, fixedBss, currentF.program, Not(currentF.phi)))
//println("Formula to validate: "+counterPhi)
- synth.solver.solveSAT(counterPhi) match {
+ sctx.solver.solveSAT(counterPhi) match {
case (Some(true), invalidModel) =>
val fixedAss = And(ass.map(a => Equals(Variable(a), invalidModel(a))).toSeq)
@@ -166,14 +166,14 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
case BooleanLiteral(false) => Not(Variable(b))
}}
- val unsatCore = synth.solver.solveSATWithCores(mustBeUnsat, bssAssumptions) match {
+ val unsatCore = sctx.solver.solveSATWithCores(mustBeUnsat, bssAssumptions) match {
case ((Some(false), _, core)) =>
//println("Formula: "+mustBeUnsat)
//println("Core: "+core)
//println(synth.solver.solveSAT(And(mustBeUnsat +: bssAssumptions.toSeq)))
//println("maxcore: "+bssAssumptions)
if (core.isEmpty) {
- synth.reporter.warning("Got empty core, must be unsat without assumptions!")
+ sctx.reporter.warning("Got empty core, must be unsat without assumptions!")
Set()
} else {
core
@@ -215,7 +215,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
case _ =>
- synth.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
continue = false
}
@@ -231,13 +231,13 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
lastF = currentF
currentF = currentF.unroll
unrolings += 1
- } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && synth.continue)
+ } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && sctx.synth.continue)
result.getOrElse(RuleApplicationImpossible)
} catch {
case e: Throwable =>
- synth.reporter.warning("CEGIS crashed: "+e.getMessage)
+ sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
RuleApplicationImpossible
}
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 9cf574acf..7bce9d378 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -8,8 +8,8 @@ import purescala.TreeOps._
import purescala.Extractors._
object Disunification {
- class Decomp(synth: Synthesizer) extends Rule("Disunif. Decomp.", synth, 200) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+ case object Decomp extends Rule("Disunif. Decomp.", 200) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val (toRemove, toAdd) = exprs.collect {
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 76330d820..f74c9fc55 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -8,21 +8,21 @@ import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object EqualitySplit extends Rule("Eq. Split.", 90) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val candidates = p.as.groupBy(_.getType).map(_._2.toList).filter {
case List(a1, a2) =>
- val toValEQ = Implies(p.c, Equals(Variable(a1), Variable(a2)))
+ val toValEQ = Implies(p.pc, Equals(Variable(a1), Variable(a2)))
- val impliesEQ = synth.solver.solveSAT(Not(toValEQ)) match {
+ val impliesEQ = sctx.solver.solveSAT(Not(toValEQ)) match {
case (Some(false), _) => true
case _ => false
}
if (!impliesEQ) {
- val toValNE = Implies(p.c, Not(Equals(Variable(a1), Variable(a2))))
+ val toValNE = Implies(p.pc, Not(Equals(Variable(a1), Variable(a2))))
- val impliesNE = synth.solver.solveSAT(Not(toValNE)) match {
+ val impliesNE = sctx.solver.solveSAT(Not(toValNE)) match {
case (Some(false), _) => true
case _ => false
}
@@ -38,8 +38,8 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
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))
+ val sub1 = p.copy(pc = And(Equals(Variable(a1), Variable(a2)), p.pc))
+ val sub2 = p.copy(pc = And(Not(Equals(Variable(a1), Variable(a2))), p.pc))
val onSuccess: List[Solution] => Solution = {
case List(s1, s2) =>
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index ae2284294..f79af5afb 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -7,13 +7,13 @@ import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object Ground extends Rule("Ground", 500) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
if (p.as.isEmpty) {
val tpe = TupleType(p.xs.map(_.getType))
- synth.solver.solveSAT(p.phi) match {
+ sctx.solver.solveSAT(p.phi) match {
case (Some(true), model) =>
RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
case (Some(false), model) =>
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 1561520d5..9fc9be76c 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -11,8 +11,8 @@ import purescala.TypeTrees._
import purescala.Definitions._
import LinearEquations.elimVariable
-class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth, 600) {
- def attemptToApplyOn(problem: Problem): RuleResult = if(!problem.xs.exists(_.getType == Int32Type)) RuleInapplicable else {
+case object IntegerEquation extends Rule("Integer Equation", 600) {
+ def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult = if(!problem.xs.exists(_.getType == Int32Type)) RuleInapplicable else {
val TopLevelAnds(exprs) = problem.phi
@@ -51,7 +51,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
if(normalizedEq.size == 1) {
val eqPre = Equals(normalizedEq.head, IntLiteral(0))
- val newProblem = Problem(problem.as, And(eqPre, problem.c), And(allOthers), problem.xs)
+ val newProblem = Problem(problem.as, And(eqPre, problem.pc), And(allOthers), problem.xs)
val onSuccess: List[Solution] => Solution = {
case List(Solution(pre, defs, term)) => {
@@ -88,7 +88,7 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
val ys: List[Identifier] = problem.xs.filterNot(neqxs.contains(_))
val subproblemxs: List[Identifier] = freshxs ++ ys
- val newProblem = Problem(problem.as ++ freshInputVariables, And(eqPre, problem.c), freshFormula, subproblemxs)
+ val newProblem = Problem(problem.as ++ freshInputVariables, And(eqPre, problem.pc), freshFormula, subproblemxs)
val onSuccess: List[Solution] => Solution = {
case List(Solution(pre, defs, term)) => {
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index d4cb134be..cf65cfffc 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -12,8 +12,8 @@ import purescala.Definitions._
import LinearEquations.elimVariable
import leon.synthesis.Algebra.lcm
-class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities", synth, 600) {
- def attemptToApplyOn(problem: Problem): RuleResult = {
+case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
+ def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult = {
val TopLevelAnds(exprs) = problem.phi
//assume that we only have inequalities
@@ -168,7 +168,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
newLowerBounds.map(lbound => LessEquals(Variable(k), Minus(b, lbound)))
} ++ exprNotUsed))
val subProblemxs: List[Identifier] = quotientIds ++ otherVars
- val subProblem = Problem(problem.as ++ remainderIds, problem.c, subProblemFormula, subProblemxs)
+ val subProblem = Problem(problem.as ++ remainderIds, problem.pc, subProblemFormula, subProblemxs)
def onSuccess(sols: List[Solution]): Solution = sols match {
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 50b3aa9e6..412796a98 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -6,8 +6,8 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object OnePoint extends Rule("One-point", 300) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val candidates = exprs.collect {
@@ -23,7 +23,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
val others = exprs.filter(_ != eq)
val oxs = p.xs.filter(_ != x)
- val newProblem = Problem(p.as, p.c, subst(x -> e, And(others)), oxs)
+ val newProblem = Problem(p.as, p.pc, subst(x -> e, And(others)), oxs)
val onSuccess: List[Solution] => Solution = {
case List(Solution(pre, defs, term)) =>
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 8225c7b6c..57e179ef3 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -7,8 +7,8 @@ import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 150) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object OptimisticGround extends Rule("Optimistic Ground", 150) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
if (!p.as.isEmpty && !p.xs.isEmpty) {
val xss = p.xs.toSet
val ass = p.as.toSet
@@ -22,16 +22,16 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
var predicates: Seq[Expr] = Seq()
while (result.isEmpty && i < maxTries) {
- val phi = And(p.c +: p.phi +: predicates)
+ val phi = And(p.pc +: p.phi +: predicates)
//println("SOLVING " + phi + " ...")
- synth.solver.solveSAT(phi) match {
+ sctx.solver.solveSAT(phi) match {
case (Some(true), satModel) =>
val satXsModel = satModel.filterKeys(xss)
val newPhi = valuateWithModelIn(phi, xss, satModel)
//println("REFUTING " + Not(newPhi) + "...")
- synth.solver.solveSAT(Not(newPhi)) match {
+ sctx.solver.solveSAT(Not(newPhi)) match {
case (Some(true), invalidModel) =>
// Found as such as the xs break, refine predicates
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 3c0dc96b7..8adc96ba1 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -6,8 +6,8 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 100) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+case object UnconstrainedOutput extends Rule("Unconstr.Output", 100) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val unconstr = p.xs.toSet -- variablesOf(p.phi)
if (!unconstr.isEmpty) {
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 5315eee03..c5ee4c320 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -8,8 +8,8 @@ import purescala.TreeOps._
import purescala.Extractors._
object Unification {
- class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 200) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+ case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.", 200) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val (toRemove, toAdd) = exprs.collect {
@@ -36,8 +36,8 @@ object Unification {
// This rule is probably useless; it never happens except in crafted
// examples, and will be found by OptimisticGround anyway.
- class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 200) {
- def attemptToApplyOn(p: Problem): RuleResult = {
+ case object OccursCheck extends Rule("Unif OccursCheck", 200) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
val TopLevelAnds(exprs) = p.phi
val isImpossible = exprs.exists {
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 18f633348..03f8aeef8 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -6,9 +6,9 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 100) {
- def attemptToApplyOn(p: Problem): RuleResult = {
- val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.c)
+case object UnusedInput extends Rule("UnusedInput", 100) {
+ def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+ val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc)
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
--
GitLab