diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index f3554752238134baa03b92572a750663d0396237..f69f3846e9d880aa73caa57606659a4cf1fe80c2 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -336,6 +336,14 @@ object TreeOps {
postMap(substs.lift)(expr)
}
+ def replaceSeq(substs: Seq[(Expr, Expr)], expr: Expr): Expr = {
+ var res = expr
+ for (s <- substs) {
+ res = replace(Map(s), res)
+ }
+ res
+ }
+
def replaceFromIDs(substs: Map[Identifier, Expr], expr: Expr) : Expr = {
postMap( {
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index f216eb33d6fd413c49af61fbe4d1a279a3c5f7bb..8afe7d70a23da52f70acd6b089e02b9ab5b9d146 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -58,9 +58,10 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val soptions = soptions0.copy(
costModel = RepairCostModel(soptions0.costModel),
rules = (soptions0.rules ++ Seq(
- GuidedDecomp,
- GuidedCloser,
- CEGLESS
+ //GuidedDecomp,
+ //GuidedCloser,
+ CEGLESS,
+ TEGLESS
)) diff Seq(ADTInduction)
);
@@ -149,23 +150,15 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
var res: Option[(Expr, Expr)] = None
// in case scrut is an non-variable expr, we simplify to a variable + inject in env
- val (sid, nenv) = scrut match {
- case Variable(id) =>
- (id, env)
- case expr =>
- val id = FreshIdentifier("scrut", true).copiedFrom(scrut)
- (id, env + (id -> scrut))
- }
-
for (c <- cases if res.isEmpty) {
- val cond = and(conditionForPattern(sid.toVariable, c.pattern, includeBinders = false),
+ val cond = and(conditionForPattern(scrut, c.pattern, includeBinders = false),
c.optGuard.getOrElse(BooleanLiteral(true)))
- val map = mapForPattern(sid.toVariable, c.pattern)
+ val map = mapForPattern(scrut, c.pattern)
- forAllTests(cond, nenv ++ map) match {
+ forAllTests(cond, env ++ map) match {
case Some(true) =>
- val (b, r) = focus(c.rhs, nenv ++ map)
+ val (b, r) = focus(c.rhs, env ++ map)
res = Some((MatchExpr(scrut, cases.map { c2 =>
if (c2 eq c) {
c2.copy(rhs = b)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index b36573bc719f4740e4b4127e5d02b2b9e0f2590b..330ba38c0c89ba20dee64b6824677d0052851444 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -20,6 +20,7 @@ object Rules {
CaseSplit,
IfSplit,
UnusedInput,
+ EquivalentInputs,
UnconstrainedOutput,
OptimisticGround,
EqualitySplit,
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index cec945313f378e5401fc62463c3e73bddf1fe872..da431e8c0c14bca7346be58d523395f6dbb30fde 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -600,6 +600,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val e = examples.next()
if (!ndProgram.testForProgram(bs)(e)) {
failedTestsStats(e) += 1
+ //sctx.reporter.debug(" Program: "+ndProgram.determinize(bs)+" failed on "+e)
wrongPrograms += bs
prunedPrograms -= bs
diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/Cegless.scala
index b2c35de16c6fe3a822ecef487d55266743288972..9c36964a24f028f49da927370ddf214a0ed14f76 100644
--- a/src/main/scala/leon/synthesis/rules/Cegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegless.scala
@@ -26,6 +26,13 @@ case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
val inputs = p.as.map(_.toVariable)
+ sctx.reporter.ifDebug { printer =>
+ printer("Guides available:")
+ for (g <- guides) {
+ printer(" - "+g)
+ }
+ }
+
val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
CegisParams(
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
new file mode 100644
index 0000000000000000000000000000000000000000..99057db0cf2f8934450f2f46a609037264f04535
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -0,0 +1,66 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.utils._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.Extractors._
+
+case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+ val TopLevelAnds(clauses) = p.pc
+
+ def discoverEquivalences(allClauses: Seq[Expr]): Seq[(Expr, Expr)] = {
+ val instanceOfs = allClauses.collect {
+ case ccio @ CaseClassInstanceOf(cct, s) => ccio
+ }
+
+ var clauses = allClauses.filterNot(instanceOfs.toSet)
+
+ val ccSubsts = for (CaseClassInstanceOf(cct, s) <- instanceOfs) yield {
+
+ val fieldsVals = (for (f <- cct.fields) yield {
+ val id = f.id
+
+ clauses.find {
+ case Equals(e, CaseClassSelector(`cct`, `s`, `id`)) => true
+ case _ => false
+ } match {
+ case Some(Equals(e, _)) =>
+ Some(e)
+ case _ =>
+ None
+ }
+
+ }).flatten
+
+
+ if (fieldsVals.size == cct.fields.size) {
+ Some((s, CaseClass(cct, fieldsVals)))
+ } else {
+ None
+ }
+ }
+
+ ccSubsts.flatten
+ }
+
+
+ val substs = discoverEquivalences(clauses)
+
+ if (substs.nonEmpty) {
+ val simplifier = Simplifiers.bestEffort(sctx.context, sctx.program) _
+
+ val sub = p.copy(ws = replaceSeq(substs, p.ws),
+ pc = simplifier(replaceSeq(substs, p.pc)),
+ phi = simplifier(replaceSeq(substs, p.phi)))
+
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward, this.name))
+ } else {
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
index a5a7418c218a87fa9e08acccedee547ebf5f4d9a..77ee3c002a01de67407837e90c2a33ff923f48a8 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
@@ -28,14 +28,6 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
val simplify = Simplifiers.bestEffort(sctx.context, sctx.program)_
- 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 {
case g @ IfExpr(c, thn, els) =>
val sub1 = p.copy(ws = replace(Map(g -> thn), p.ws), pc = and(c, replace(Map(g -> thn), p.pc)))
@@ -66,11 +58,11 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
val pc = simplify(and(
scrutCond,
- replace(Map(scrut0 -> scrut), doSubstitute(substs,scrutConstraint)),
+ replace(Map(scrut0 -> scrut), replaceSeq(substs,scrutConstraint)),
replace(Map(scrut0 -> scrut), replace(Map(m -> c.rhs), andJoin(cond)))
))
val ws = replace(Map(m -> c.rhs), p.ws)
- val phi = doSubstitute(substs, p.phi)
+ val phi = replaceSeq(substs, p.phi)
val free = variablesOf(and(pc, phi)) -- p.xs
val asPrefix = p.as.filter(free)
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index 736b7035380dda4bbd718a257278b7dcbbb9dcae..273e170ecbf8c30aeb84bbfe63bca216e916f37f 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -16,9 +16,10 @@ import datagen._
import utils._
case object TEGIS extends TEGISLike[TypeTree]("TEGIS") {
- def getGrammar(sctx: SynthesisContext, p: Problem) = {
- ExpressionGrammars.default(sctx, p)
+ def getParams(sctx: SynthesisContext, p: Problem) = {
+ TegisParams(
+ grammar = ExpressionGrammars.default(sctx, p),
+ rootLabel = {(tpe: TypeTree) => tpe }
+ )
}
-
- def getRootLabel(tpe: TypeTree): TypeTree = tpe
}
diff --git a/src/main/scala/leon/synthesis/rules/TegisLike.scala b/src/main/scala/leon/synthesis/rules/TegisLike.scala
index ed5003d47a27f4d9bb600496dd6ec4b6c14c19f3..3f55650e38646c654d788932cfcfbfae647744d3 100644
--- a/src/main/scala/leon/synthesis/rules/TegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TegisLike.scala
@@ -21,19 +21,22 @@ import bonsai._
import bonsai.enumerators._
abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
- def getGrammar(sctx: SynthesisContext, p: Problem): ExpressionGrammar[T]
+ case class TegisParams(
+ grammar: ExpressionGrammar[T],
+ rootLabel: TypeTree => T,
+ enumLimit: Int = 10000,
+ reorderInterval: Int = 50
+ );
- def getRootLabel(tpe: TypeTree): T
-
- val enumLimit = 10000;
- val testsReorderInterval = 50; // Every X test filterings, we reorder tests with most filtering first.
+ def getParams(sctx: SynthesisContext, p: Problem): TegisParams
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
def apply(sctx: SynthesisContext): RuleApplication = {
- val grammar = getGrammar(sctx, p)
+ val params = getParams(sctx, p)
+ val grammar = params.grammar
var tests = p.getTests(sctx).map(_.ins).distinct
if (tests.nonEmpty) {
@@ -53,7 +56,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
val timers = sctx.context.timers.synthesis.rules.tegis;
- val allExprs = enum.iterator(getRootLabel(targetType))
+ val allExprs = enum.iterator(params.rootLabel(targetType))
var failStat = Map[Seq[Expr], Int]().withDefaultValue(0)
@@ -63,7 +66,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
def findNext(): Option[Expr] = {
candidate = None
timers.generating.start()
- allExprs.take(enumLimit).takeWhile(e => candidate.isEmpty).foreach { e =>
+ allExprs.take(params.enumLimit).takeWhile(e => candidate.isEmpty).foreach { e =>
val exprToTest = if (!isWrapped) {
Let(p.xs.head, e, p.phi)
} else {
@@ -93,7 +96,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
}
timers.testing.stop()
- if (n % testsReorderInterval == 0) {
+ if (n % params.reorderInterval == 0) {
tests = tests.sortBy(t => -failStat(t))
}
n += 1
@@ -114,6 +117,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
RuleClosed(toStream())
} else {
+ sctx.reporter.debug("No test available")
RuleFailed()
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Tegless.scala b/src/main/scala/leon/synthesis/rules/Tegless.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cdef20a9bbcd3ae89aeee0b34c76bdadf41dda49
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/Tegless.scala
@@ -0,0 +1,46 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Extractors._
+import utils._
+import utils.ExpressionGrammars._
+
+case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
+ def getParams(sctx: SynthesisContext, p: Problem) = {
+
+ val TopLevelAnds(clauses) = p.ws
+
+ val guide = sctx.program.library.guide.get
+
+ val guides = clauses.collect {
+ case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+ }
+
+ val inputs = p.as.map(_.toVariable)
+
+ sctx.reporter.ifDebug { printer =>
+ printer("Guides available:")
+ for (g <- guides) {
+ printer(" - "+g)
+ }
+ }
+
+ val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
+
+ TegisParams(
+ grammar = guidedGrammar,
+ rootLabel = { (tpe: TypeTree) => Label(tpe, "G0") }
+ )
+ }
+}
+
+
+
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index f87d9e6b58bfdfa4982bb411a625d81bb10c2227..565a6c2bc6856e3dfee5430c74fde3da1afef0d7 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -222,7 +222,7 @@ object ExpressionGrammars {
gl -> Generator(subEls.updated(i, sgl), builder)
}
- val swaps = if (subs.size > 1 || isCommutative(e)) {
+ val swaps = if (subs.size > 1 && !isCommutative(e)) {
(for (i <- 0 until subs.size;
j <- i+1 until subs.size) yield {