diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 9f373400770d59fa5019e516e3b5b1bcb4cb5fc4..e60d36f5310762d9e5aa56e3b9b55c13abc9ddc4 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -853,10 +853,10 @@ object TreeOps {
case LiteralPattern(Some(id), lit) => Map(id -> in)
}
- private def convertMatchToIfThenElse(expr: Expr) : Expr = {
+ private def convertMatchToIfThenElse(expr: Expr): Expr = {
- def rewritePM(e: Expr) : Option[Expr] = e match {
- case m @ MatchExpr(scrut, cases) => {
+ def rewritePM(e: Expr): Option[Expr] = e match {
+ case m @ MatchExpr(scrut, cases) =>
// println("Rewriting the following PM: " + e)
val condsAndRhs = for(cse <- cases) yield {
@@ -879,11 +879,19 @@ object TreeOps {
})
Some(bigIte)
- }
+
+ case p: Passes =>
+ // This introduces a MatchExpr
+ Some(p.asConstraint)
+
+ case g: Gives =>
+ // This introduces a MatchExpr
+ Some(g.asMatch)
+
case _ => None
}
- postMap(rewritePM)(expr)
+ preMap(rewritePM)(expr)
}
def matchCasePathConditions(m: MatchExpr, pathCond: List[Expr]) : Seq[List[Expr]] = {
@@ -1381,14 +1389,6 @@ object TreeOps {
new ChooseCollectorWithPaths().traverse(e).map(_._1).toList
}
- def containsChoose(e: Expr): Boolean = {
- preTraversal{
- case Choose(_, _, None) => return true
- case _ =>
- }(e)
- false
- }
-
def isDeterministic(e: Expr): Boolean = {
preTraversal{
case Choose(_, _, None) => return false
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 171d8cc04280aacd79832671ba2caec875549072..421d97600d994c5d513537c26714338fd4407104 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -192,10 +192,14 @@ object Trees {
}
case class Gives(scrutinee: Expr, cases : Seq[MatchCase]) extends MatchLike {
- def asIncompleteMatch = {
+ def asMatchWithHole = {
val theHole = SimpleCase(WildcardPattern(None), Hole(this.getType, Seq()))
MatchExpr(scrutinee, cases :+ theHole)
}
+
+ def asMatch = {
+ matchExpr(scrutinee, cases)
+ }
}
case class Passes(in: Expr, out : Expr, cases : Seq[MatchCase]) extends Expr {
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 09ce38e76a3637588753334a4c05e25de2a4846c..cdad71b8859c2dcb0e2be28f778f9234a3be3bf3 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -223,7 +223,9 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
val rb = rec(pathVar, replace(mapping.toMap, b))
rb
- case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
+ case m : MatchExpr => sys.error("'MatchExpr's should have been eliminated before generating templates.")
+ case p : Passes => sys.error("'Passes's should have been eliminated before generating templates.")
+ case g : Gives => sys.error("'Gives' should have been eliminated before generating templates.")
case i @ Implies(lhs, rhs) =>
implies(rec(pathVar, lhs), rec(pathVar, rhs))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index ac0719cd63ff41723c7ee4d0edd583ead42d0e39..51dc20d565bb58e70573a26cb744fec0cbd1cc5a 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -501,8 +501,8 @@ trait AbstractZ3Solver
case me @ MatchExpr(s, cs) =>
rec(matchToIfThenElse(me))
- case Gives(scrut, tests) =>
- rec(matchToIfThenElse(matchExpr(scrut, tests)))
+ case g @ Gives(scrut, tests) =>
+ rec(g.asMatch)
case tu @ Tuple(args) =>
typeToSort(tu.getType) // Make sure we generate sort & meta info
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 375b6dfe17a929ac4d6378f58d09360f3345526e..a7051f4930d1d587aee7affbab58cc43f0afdfa3 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -63,7 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
val withoutHoles = preMap {
case p : Gives if treatGives =>
- Some(p.asIncompleteMatch)
+ Some(p.asMatchWithHole)
case h : Hole =>
val (expr, ids) = toExpr(h)
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index 1e6cc3a0bcfb89405b3eb86639604959bac68d14..98d7b68cd7d3c9aca6ddfc5408b600d408de197b 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -42,9 +42,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
def getParams(sctx: SynthesisContext, p: Problem): CegisParams
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-
- def debugPrinter(t: Tree) = ScalaPrinter(t, PrinterOptions(printUniqueIds = true))
-
val exSolverTo = 2000L
val cexSolverTo = 2000L
@@ -59,7 +56,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val useOptTimeout = sctx.settings.cegisUseOptTimeout
val useVanuatoo = sctx.settings.cegisUseVanuatoo
val useCETests = sctx.settings.cegisUseCETests
- val useCEPruning = sctx.settings.cegisUseCEPruning
// Limits the number of programs CEGIS will specifically validate individually
val validateUpTo = 5
@@ -279,12 +275,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val affected = prog0.callGraph.transitiveCallers(chFd).toSet ++ Set(chFd, cTreeFd, phiFd) ++ fullSol.defs
- //println("Affected:")
- //for (fd <- affected) {
- // println(" - "+debugPrinter(fd.id))
- //}
-
-
cTreeFd.body = None
phiFd.body = Some(
letTuple(p.xs,
@@ -319,13 +309,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
case _ =>
None
})
- //println("FunDef Map:")
- //for ((f, t) <- fdMap2) {
- // println("- "+debugPrinter(f.id)+" -> "+debugPrinter(t.id))
- //}
-
- //println("Program:")
- //println(debugPrinter(prog2))
programCTree = prog2
cTreeFd = fdMap2(cTreeFd)
@@ -415,9 +398,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
hctx.ci.ch.impl = Some(fullSol.guardedTerm)
- //println("Validating Solution "+sol)
- //println(debugPrinter(prog))
-
val cnstr = and(p.pc, letTuple(p.xs, sol, Not(p.phi)))
//println("Solving for: "+cnstr)
@@ -428,6 +408,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
case Some(true) =>
excludeProgram(bs)
val model = solver.getModel
+ //println("Found counter example: ")
+ //for ((s, v) <- model) {
+ // println(" "+s.asString+" -> "+v.asString)
+ //}
+
+ //val evaluator = new DefaultEvaluator(ctx, prog)
+ //println(evaluator.eval(cnstr, model))
+
Some(p.as.map(a => model.getOrElse(a, simplestValue(a.getType))))
case Some(false) =>
@@ -830,20 +818,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
baseExampleInputs.iterator ++ cachedInputIterator
}
- // Keep track of collected cores to filter programs to test
- var collectedCores = Set[Set[Identifier]]()
-
- //val initExClause = and(pc, p.phi, Variable(initGuard))
- //val initCExClause = and(pc, not(p.phi), Variable(initGuard))
-
- //// solver1 is used for the initial SAT queries
- //var solver1 = sctx.newSolver.setTimeout(exSolverTo)
- //solver1.assertCnstr(initExClause)
-
- //// solver2 is used for validating a candidate program, or finding new inputs
- //var solver2 = sctx.newSolver.setTimeout(cexSolverTo)
- //solver2.assertCnstr(initCExClause)
-
val tpe = tupleTypeWrap(p.xs.map(_.getType))
try {
@@ -858,11 +832,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
// Compute all programs that have not been excluded yet
- var prunedPrograms: Set[Set[Identifier]] = if (useCEPruning) {
- ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p))).toSet
- } else {
- Set()
- }
+ var prunedPrograms: Set[Set[Identifier]] = ndProgram.allPrograms.toSet
val nInitial = prunedPrograms.size
sctx.reporter.debug("#Programs: "+nInitial)
@@ -881,7 +851,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
var wrongPrograms = Set[Set[Identifier]]();
// We further filter the set of working programs to remove those that fail on known examples
- if (useCEPruning && hasInputExamples()) {
+ if (hasInputExamples()) {
for (bs <- prunedPrograms if !interruptManager.isInterrupted()) {
var valid = true
val examples = allInputExamples()
@@ -967,10 +937,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
baseExampleInputs += inputsCE
// Retest whether the newly found C-E invalidates all programs
- if (useCEPruning) {
- if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(inputsCE))) {
- skipCESearch = true
- }
+ if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(inputsCE))) {
+ skipCESearch = true
}
case Some(None) =>