diff --git a/src/main/scala/leon/repair/RepairCostModel.scala b/src/main/scala/leon/repair/RepairCostModel.scala
index e9b1a8163f295f09111291b89536e08ec154bd15..8de1a98f50b13918b41c2a71ec88206774ee4538 100644
--- a/src/main/scala/leon/repair/RepairCostModel.scala
+++ b/src/main/scala/leon/repair/RepairCostModel.scala
@@ -4,6 +4,9 @@ package leon
package repair
import synthesis._
+import synthesis.rules._
+import repair.rules._
+
import purescala.Definitions._
import purescala.Trees._
import purescala.DefOps._
@@ -17,21 +20,24 @@ case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("
val h = cm.andNode(an, subs).minSize
Cost(an.ri.rule match {
- case rules.GuidedDecomp => h/2
- case rules.GuidedCloser => 0
- case rules.CEGLESS => 0
- case rules.TEGLESS => 1
+ case GuidedDecomp => 1
+ case GuidedCloser => 0
+ case CEGLESS => 0
+ case TEGLESS => 1
case _ => h+1
})
}
- def costOfGuide(p: Problem): Int = {
- val TopLevelAnds(clauses) = p.pc
+ override def rulesFor(sctx: SynthesisContext, on: OrNode) = {
+ val rs = cm.rulesFor(sctx, on)
- val guides = clauses.collect {
- case FunctionInvocation(TypedFunDef(fd, _), Seq(expr)) if fullName(fd) == "leon.lang.synthesis.guide" => expr
+ on.parent match {
+ case None =>
+ GuidedDecomp +: rs
+ case Some(an: AndNode) if an.ri.rule == GuidedDecomp =>
+ GuidedCloser +: rs
+ case _ =>
+ rs
}
-
- guides.map(formulaSize(_)).sum
}
}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 97fc1b86ecbaf391b490cd90ac5f8025cc148bae..e97cabe91c25089f08c53c6dd810b3b13b72cd31 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -109,11 +109,11 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
functionsToIgnore = soptions0.functionsToIgnore + fd,
costModel = RepairCostModel(soptions0.costModel),
rules = (soptions0.rules ++ Seq(
- GuidedDecomp,
- GuidedCloser,
- CEGLESS,
- TEGLESS
- )) diff Seq(ADTInduction)
+ //GuidedDecomp,
+ //GuidedCloser,
+ CEGLESS
+ //TEGLESS
+ )) diff Seq(ADTInduction, TEGIS)
);
// extract chooses from nfd
diff --git a/src/main/scala/leon/synthesis/rules/GuidedCloser.scala b/src/main/scala/leon/repair/rules/GuidedCloser.scala
similarity index 93%
rename from src/main/scala/leon/synthesis/rules/GuidedCloser.scala
rename to src/main/scala/leon/repair/rules/GuidedCloser.scala
index 0cc03942c364ec52da59e20cc0d1a9342bf59491..30062477cd20c94d8ceb01ea0e71392aafa861a8 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/repair/rules/GuidedCloser.scala
@@ -1,9 +1,11 @@
/* Copyright 2009-2014 EPFL, Lausanne */
package leon
-package synthesis
+package repair
package rules
+import synthesis._
+
import leon.utils.Simplifiers
import purescala.Trees._
import purescala.Definitions._
@@ -46,7 +48,8 @@ case object GuidedCloser extends NormalizingRule("Guided Closer") {
printer("== Unknown ==")
}
//None
- Some(Solution(BooleanLiteral(true), Set(), wrappedE, false))
+ //Some(Solution(BooleanLiteral(true), Set(), wrappedE, false))
+ None
case _ =>
sctx.reporter.ifDebug { printer =>
diff --git a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
similarity index 89%
rename from src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
rename to src/main/scala/leon/repair/rules/GuidedDecomp.scala
index 77ee3c002a01de67407837e90c2a33ff923f48a8..f200f69091146d9156b16f372ce5242d49a51fca 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
@@ -1,9 +1,11 @@
/* Copyright 2009-2014 EPFL, Lausanne */
package leon
-package synthesis
+package repair
package rules
+import synthesis._
+
import leon.utils.Simplifiers
import purescala.Trees._
@@ -42,7 +44,7 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess, "Guided If-Split on '"+c+"'"))
- case m @ MatchExpr(scrut0, cs) =>
+ case m @ MatchExpr(scrut0, _) =>
val scrut = scrut0 match {
case v : Variable => v
@@ -50,7 +52,15 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
}
var scrutCond: Expr = if (scrut == scrut0) BooleanLiteral(true) else Equals(scrut0, scrut)
- val subs = for ((c, cond) <- cs zip matchCasePathConditions(m, List(p.pc))) yield {
+ val fullMatch = if (isMatchExhaustive(m)) {
+ m
+ } else {
+ m.copy(cases = m.cases :+ MatchCase(WildcardPattern(None), None, Error(m.getType, "unreachable in original program")))
+ }
+
+ val cs = fullMatch.cases
+
+ val subs = for ((c, cond) <- cs zip matchCasePathConditions(fullMatch, List(p.pc))) yield {
val localScrut = c.pattern.binder.map(Variable) getOrElse scrut
val scrutConstraint = if (localScrut == scrut) BooleanLiteral(true) else Equals(localScrut, scrut)
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index 2e96db012e589f4d1fda94a8a067deeeef58040a..c08caa4107abaf2d28e3bdc3f7c0630792d5199b 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -16,6 +16,10 @@ abstract class CostModel(val name: String) {
def andNode(an: AndNode, subs: Option[Seq[Cost]]): Cost
def impossible: Cost
+
+ def rulesFor(sctx: SynthesisContext, on: OrNode): Seq[Rule] = {
+ sctx.rules
+ }
}
case class Cost(minSize: Int) extends Ordered[Cost] {
@@ -52,6 +56,8 @@ class WrappedCostModel(cm: CostModel, name: String) extends CostModel(name) {
def andNode(an: AndNode, subs: Option[Seq[Cost]]): Cost = cm.andNode(an, subs)
def impossible = cm.impossible
+
+ override def rulesFor(sctx: SynthesisContext, on: OrNode) = cm.rulesFor(sctx, on)
}
class SizeBasedCostModel(name: String) extends CostModel(name) {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index d616c3b933e2abfaab0e7720d1fab97b3250f1e4..5e6db134acc4e09d6a5f4103816ed54e8e6eee69 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -38,23 +38,6 @@ object Rules {
//AngelicHoles // @EK: Disabled now as it is explicit with withOracle { .. }
)
- def getInstantiations(sctx: SynthesisContext, problem: Problem): List[RuleInstantiation] = {
-
- val rulesPrio = sctx.rules.groupBy(_.priority).toSeq.sortBy(_._1)
-
- for ((_, rs) <- rulesPrio) {
- val results = rs.flatMap{ r =>
- sctx.context.timers.synthesis.instantiations.get(r.toString).timed {
- r.instantiateOn(sctx, problem)
- }
- }.toList
-
- if (results.nonEmpty) {
- return results;
- }
- }
- Nil
- }
}
abstract class SolutionBuilder(val arity: Int, val types: Seq[TypeTree]) {
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 7e07bca199f6095adca187583483e200765baae8..9e384d922e3ae976dcf929ee491d5edcef81fc68 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -164,14 +164,34 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
}
-class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(cm, parent) {
+class OrNode(cm: CostModel, val parent: Option[Node], val p: Problem) extends Node(cm, parent) {
override def toString = "\u2228 "+p;
+ def getInstantiations(sctx: SynthesisContext): List[RuleInstantiation] = {
+
+ val rules = cm.rulesFor(sctx, this)
+
+ val rulesPrio = rules.groupBy(_.priority).toSeq.sortBy(_._1)
+
+ for ((_, rs) <- rulesPrio) {
+ val results = rs.flatMap{ r =>
+ sctx.context.timers.synthesis.instantiations.get(r.toString).timed {
+ r.instantiateOn(sctx, p)
+ }
+ }.toList
+
+ if (results.nonEmpty) {
+ return results;
+ }
+ }
+ Nil
+ }
+
def expand(sctx: SynthesisContext): Unit = {
require(!isExpanded)
- val ris = Rules.getInstantiations(sctx, p)
+ val ris = getInstantiations(sctx)
descendents = ris.map(ri => new AndNode(cm, Some(this), ri))
selected = List()