diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index e0557a3d82e4ad239c9e995e333237ef53ff3c04..d65eedf8199bae266604d3141f1e84db5bf41588 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -673,7 +673,7 @@ object TreeOps {
*
* will return, for the first pattern:
*
- * Seq(
+ * Map(
* e -> CaseClass(t, c),
* t -> (a, b2),
* b2 -> 42,
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
index 8b4ea7c175b99a6a2c78e949509cd4f44cdbe462..1a63edeb2fb2e749a558ec82f113ba491f851bf5 100644
--- a/src/main/scala/leon/refactor/Repairman.scala
+++ b/src/main/scala/leon/refactor/Repairman.scala
@@ -77,7 +77,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
// Synthesis from the ground up
val p = Problem(fd.params.map(_.id).toList, pc, spec, List(out))
- val soptions = SynthesisPhase.processOptions(ctx);
+ val soptions = SynthesisPhase.processOptions(ctx).copy(costModel = RepairCostModel(CostModel.default));
val synthesizer = new Synthesizer(ctx, fd, program, p, soptions)
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index b4cac6662ae50934b9231a8867910f2aaa6ec757..33529ccecbd7f9bf1c8d651ac5df5981357663ba 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -40,6 +40,18 @@ object CostModel {
)
}
+case class RepairCostModel(cm: CostModel) extends CostModel(cm.name) {
+ override def ruleAppCost(app: RuleInstantiation): Cost = {
+ app.rule match {
+ case rules.GuidedDecomp => 0
+ case _ => cm.ruleAppCost(app)
+ }
+ }
+ def solutionCost(s: Solution) = cm.solutionCost(s)
+ def problemCost(p: Problem) = cm.problemCost(p)
+}
+
+
case object NaiveCostModel extends CostModel("Naive") {
def solutionCost(s: Solution): Cost = {
val chooses = collectChooses(s.toExpr)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 160f3ec13e5a2c97783f5bed15f3179318600995..d109c73fb987417b4694094a27f1bb92c99470f6 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -415,6 +415,7 @@ case object CEGIS extends Rule("CEGIS") {
baseExampleInputs += p.as.map(a => model.getOrElse(a, simplestValue(a.getType)))
case Some(false) =>
+ sctx.reporter.debug("Path-condition seems UNSAT")
return RuleFailed()
case None =>
@@ -509,7 +510,7 @@ case object CEGIS extends Rule("CEGIS") {
try {
do {
- var needMoreUnrolling = false
+ var skipCESearch = false
var bssAssumptions = Set[Identifier]()
@@ -553,14 +554,12 @@ case object CEGIS extends Rule("CEGIS") {
val examples = allInputExamples()
while(valid && examples.hasNext) {
val e = examples.next()
- println("Running on "+e)
if (!ndProgram.testForProgram(p)(e)) {
failedTestsStats(e) += 1
wrongPrograms += p
prunedPrograms -= p
valid = false;
}
- println("Done")
}
if (wrongPrograms.size % 1000 == 0) {
@@ -573,11 +572,11 @@ case object CEGIS extends Rule("CEGIS") {
sctx.reporter.debug("#Programs passing tests: "+nPassing)
if (nPassing == 0) {
- needMoreUnrolling = true;
+ skipCESearch = true;
} else if (nPassing <= testUpTo) {
// Immediate Test
checkForPrograms(prunedPrograms) match {
- case rs: RuleClosed =>
+ case rs: RuleClosed if rs.solutions.nonEmpty =>
result = Some(rs)
case _ =>
wrongPrograms.foreach { p =>
@@ -614,7 +613,7 @@ case object CEGIS extends Rule("CEGIS") {
val bss = ndProgram.bss
- while (result.isEmpty && !needMoreUnrolling && !interruptManager.isInterrupted()) {
+ while (result.isEmpty && !skipCESearch && !interruptManager.isInterrupted()) {
solver1.checkAssumptions(bssAssumptions.map(id => Not(Variable(id)))) match {
case Some(true) =>
@@ -659,7 +658,7 @@ case object CEGIS extends Rule("CEGIS") {
// Retest whether the newly found C-E invalidates all programs
if (useCEPruning && ndProgram.canTest) {
if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
- needMoreUnrolling = true
+ skipCESearch = true
}
}
@@ -692,7 +691,7 @@ case object CEGIS extends Rule("CEGIS") {
}
if (unsatCore.isEmpty) {
- needMoreUnrolling = true
+ skipCESearch = true
} else {
solver1.assertCnstr(Not(And(unsatCore.toSeq)))
}
@@ -727,11 +726,11 @@ case object CEGIS extends Rule("CEGIS") {
}
}
- needMoreUnrolling = true
+ skipCESearch = true
case _ =>
// Last chance, we test first few programs
- return checkForPrograms(prunedPrograms.take(testUpTo))
+ result = Some(checkForPrograms(prunedPrograms.take(testUpTo)))
}
}
diff --git a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
index 260f238201ada1eaddbd765b3a48fec874c1b198..f2a26848ba3120dfc23b0d4cc18b68ed700721a0 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
@@ -4,6 +4,8 @@ package leon
package synthesis
package rules
+import leon.utils.Simplifiers
+
import purescala.Trees._
import purescala.Definitions._
import purescala.Common._
@@ -24,10 +26,16 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
}
- def doSubstitute(substs: Seq[(Expr, Expr)], e: Expr): Expr = {
- val m = substs.toMap
+ def simplify(e: Expr): Expr = {
+ Simplifiers.forPathConditions(sctx.context, sctx.program)(e)
+ }
- preMap({ case e => m.get(e) }, true)(e)
+ def doSubstitute(substs: Seq[(Expr, Expr)], e: Expr): Expr = {
+ var res = e
+ for (s <- substs) {
+ res = postMap(Map(s).lift)(res)
+ }
+ res
}
val alts = guides.collect {
@@ -45,14 +53,18 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess, "Guided If-Split on '"+c+"'"))
case m @ MatchExpr(scrut, cs) =>
+ var pcSoFar: Expr = BooleanLiteral(true)
val subs = for (c <- cs) yield {
val substs = patternSubstitutions(scrut, c.pattern)
+ val cond = conditionForPattern(scrut, c.pattern)
val g = c.theGuard.getOrElse(BooleanLiteral(true))
- val pc = doSubstitute(substs, And(g, replace(Map(m -> c.rhs), p.pc)))
+ val pc = simplify(doSubstitute(substs, And(Seq(pcSoFar, g, replace(Map(m -> c.rhs), p.pc)))))
val phi = doSubstitute(substs, p.phi)
val free = variablesOf(And(pc, phi)) -- p.xs
+ pcSoFar = And(pcSoFar, Not(cond))
+
val asPrefix = p.as.filter(free)
Problem(asPrefix ++ (free -- asPrefix), pc, phi, p.xs)
}
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index a9dc460ea5d5e2b08a9ab9d96d1672d1bdf53f5a..4791d5a07662a10e91f90bc86b0add4b6e2c2fb1 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -14,7 +14,7 @@ object Simplifiers {
val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))
val simplifiers = List[Expr => Expr](
- removeWitnesses(p)(_),
+ removeWitnesses(p) _,
simplifyTautologies(uninterpretedZ3)(_),
simplifyLets _,
decomposeIfs _,
@@ -39,6 +39,31 @@ object Simplifiers {
(new ScopeSimplifier).transform(s)
}
+ // Besteffort, but keep witnesses
+ def forPathConditions(ctx: LeonContext, p: Program)(e: Expr): Expr = {
+ val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))
+
+ val simplifiers = List[Expr => Expr](
+ simplifyTautologies(uninterpretedZ3)(_),
+ simplifyLets _,
+ decomposeIfs _,
+ matchToIfThenElse _,
+ simplifyPaths(uninterpretedZ3)(_),
+ patternMatchReconstruction _,
+ rewriteTuples _,
+ evalGround(ctx, p),
+ normalizeExpression _
+ )
+
+ val simple = { expr: Expr =>
+ simplifiers.foldLeft(expr){ case (x, sim) =>
+ sim(x)
+ }
+ }
+
+ fixpoint(simple, 5)(e)
+ }
+
def namePreservingBestEffort(ctx: LeonContext, p: Program)(e: Expr): Expr = {
val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))