diff --git a/src/main/scala/leon/grammars/ExpressionGrammar.scala b/src/main/scala/leon/grammars/ExpressionGrammar.scala
index 186729fce32c11b956cd51912941922f3954f9f0..a1309669896a9754b0f6309f2575ed2990a1b9c4 100644
--- a/src/main/scala/leon/grammars/ExpressionGrammar.scala
+++ b/src/main/scala/leon/grammars/ExpressionGrammar.scala
@@ -18,7 +18,7 @@ abstract class ExpressionGrammar {
* @param lab The nonterminal for which production rules will be generated
* @note This is the cached version of [[computeProductions]]. Clients should use this method.
*/
- def getProductions(lab: Label)(implicit ctx: LeonContext) = {
+ final def getProductions(lab: Label)(implicit ctx: LeonContext) = {
cache.getOrElse(lab, {
val res = applyAspects(lab, computeProductions(lab))
cache += lab -> res
@@ -33,7 +33,7 @@ abstract class ExpressionGrammar {
*/
def computeProductions(lab: Label)(implicit ctx: LeonContext): Seq[ProductionRule[Label, Expr]]
- def applyAspects(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
+ protected def applyAspects(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
lab.aspects.foldLeft(ps) {
case (ps, a) => a.applyTo(lab, ps)
}
diff --git a/src/main/scala/leon/grammars/Grammars.scala b/src/main/scala/leon/grammars/Grammars.scala
index 2f60d59a48463391d9dce50add99acd19da51de1..56d63a4387460163cfcbfe8146761bff6093689e 100644
--- a/src/main/scala/leon/grammars/Grammars.scala
+++ b/src/main/scala/leon/grammars/Grammars.scala
@@ -29,5 +29,8 @@ object Grammars {
val hints = ws.collect{ case Hint(e) if formulaSize(e) >= 4 => e }
default(sctx.program, p.as.map(_.toVariable) ++ hints ++ extraHints, sctx.functionContext, sctx.settings.functionsToIgnore)
}
+
+ def similarTo(e: Expr, base: ExpressionGrammar) = {
+ }
}
diff --git a/src/main/scala/leon/grammars/SimilarTo.scala b/src/main/scala/leon/grammars/SimilarTo.scala
deleted file mode 100644
index 295f18311213ff6b93316477c09926957f777527..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/grammars/SimilarTo.scala
+++ /dev/null
@@ -1,172 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package grammars
-
-import purescala.Types._
-import purescala.TypeOps._
-import purescala.Extractors._
-import purescala.Definitions._
-import purescala.Expressions._
-
-import synthesis._
-
-/** A grammar that generates expressions by inserting small variations in [[e]]
- * @param e The [[Expr]] to which small variations will be inserted
- */
-case class SimilarTo(e: Expr, sctx: SynthesisContext, p: Problem) extends ExpressionGrammar {
-
- def computeProductions(l: Label)(implicit ctx: LeonContext) = Nil
-// val excludeFCalls = sctx.settings.functionsToIgnore
-//
-// val normalGrammar: ExpressionGrammar[NonTerminal[String]] = DepthBoundedGrammar(EmbeddedGrammar(
-// Grammars.default(sctx, p, Seq(e)),
-// (t: TypeTree) => NonTerminal(t, "B", None),
-// (l: NonTerminal[String]) => l.getType
-// ), 1)
-//
-// type L = NonTerminal[String]
-//
-// val getNext: () => Int = {
-// var counter = -1
-// () => {
-// counter += 1
-// counter
-// }
-// }
-//
-// private[this] var similarCache: Option[Map[L, Seq[Prod]]] = None
-//
-// def computeProductions(t: L)(implicit ctx: LeonContext): Seq[Prod] = {
-// t match {
-// case NonTerminal(_, "B", _) => normalGrammar.computeProductions(t)
-// case _ =>
-//
-// val allSimilar = similarCache.getOrElse {
-// val res = computeSimilar(e).groupBy(_._1).mapValues(_.map(_._2))
-// similarCache = Some(res)
-// res
-// }
-//
-// allSimilar.getOrElse(t, Nil)
-// }
-// }
-//
-// def computeSimilar(e : Expr)(implicit ctx: LeonContext): Seq[(L, Prod)] = {
-//
-// def getLabel(t: TypeTree) = {
-// val tpe = bestRealType(t)
-// val c = getNext()
-// NonTerminal(tpe, "G"+c)
-// }
-//
-// def isCommutative(e: Expr) = e match {
-// case _: Plus | _: Times => true
-// case _ => false
-// }
-//
-// def rec(e: Expr, gl: L): Seq[(L, Prod)] = {
-//
-// def gens(e: Expr, gl: L, subs: Seq[Expr], builder: (Seq[Expr] => Expr)): Seq[(L, Prod)] = {
-// val subGls = subs.map { s => getLabel(s.getType) }
-//
-// // All the subproductions for sub gl
-// val allSubs = (subs zip subGls).flatMap { case (e, gl) => rec(e, gl) }
-//
-// // Inject fix at one place
-// val injectG = for ((sgl, i) <- subGls.zipWithIndex) yield {
-// gl -> nonTerminal(Seq(sgl), { case Seq(ge) => builder(subs.updated(i, ge)) } )
-// }
-//
-// val swaps = if (subs.size > 1 && !isCommutative(e)) {
-// (for (i <- subs.indices;
-// j <- i+1 until subs.size) yield {
-//
-// if (subs(i).getType == subs(j).getType) {
-// val swapSubs = subs.updated(i, subs(j)).updated(j, subs(i))
-// Some(gl -> terminal(builder(swapSubs)))
-// } else {
-// None
-// }
-// }).flatten
-// } else {
-// Nil
-// }
-//
-// allSubs ++ injectG ++ swaps
-// }
-//
-// def cegis(gl: L): Seq[(L, Prod)] = {
-// normalGrammar.getProductions(gl).map(gl -> _)
-// }
-//
-// def int32Variations(gl: L, e : Expr): Seq[(L, Prod)] = {
-// Seq(
-// gl -> terminal(BVMinus(e, IntLiteral(1))),
-// gl -> terminal(BVPlus (e, IntLiteral(1)))
-// )
-// }
-//
-// def intVariations(gl: L, e : Expr): Seq[(L, Prod)] = {
-// Seq(
-// gl -> terminal(Minus(e, InfiniteIntegerLiteral(1))),
-// gl -> terminal(Plus (e, InfiniteIntegerLiteral(1)))
-// )
-// }
-//
-// // Find neighbor case classes that are compatible with the arguments:
-// // Turns And(e1, e2) into Or(e1, e2)...
-// def ccVariations(gl: L, cc: CaseClass): Seq[(L, Prod)] = {
-// val CaseClass(cct, args) = cc
-//
-// val neighbors = cct.root.knownCCDescendants diff Seq(cct)
-//
-// for (scct <- neighbors if scct.fieldsTypes == cct.fieldsTypes) yield {
-// gl -> terminal(CaseClass(scct, args))
-// }
-// }
-//
-// val funFilter = (fd: FunDef) => fd.isSynthetic || (excludeFCalls contains fd)
-// val subs: Seq[(L, Prod)] = e match {
-//
-// case _: Terminal | _: Let | _: LetDef | _: MatchExpr =>
-// gens(e, gl, Nil, { _ => e }) ++ cegis(gl)
-//
-// case cc @ CaseClass(cct, exprs) =>
-// gens(e, gl, exprs, { case ss => CaseClass(cct, ss) }) ++ ccVariations(gl, cc)
-//
-// case FunctionInvocation(TypedFunDef(fd, _), _) if funFilter(fd) =>
-// // We allow only exact call, and/or cegis extensions
-// /*Seq(el -> Generator[L, Expr](Nil, { _ => e })) ++*/ cegis(gl)
-//
-// case Operator(subs, builder) =>
-// gens(e, gl, subs, { case ss => builder(ss) })
-// }
-//
-// val terminalsMatching = p.as.collect {
-// case IsTyped(term, tpe) if tpe == gl.getType && Variable(term) != e =>
-// gl -> terminal(Variable(term))
-// }
-//
-// val variations = e.getType match {
-// case IntegerType => intVariations(gl, e)
-// case Int32Type => int32Variations(gl, e)
-// case _ => Nil
-// }
-//
-// subs ++ terminalsMatching ++ variations
-// }
-//
-// val gl = getLabel(e.getType)
-//
-// val res = rec(e, gl)
-//
-// //for ((t, g) <- res) {
-// // val subs = g.subTrees.map { t => FreshIdentifier(t.asString, t.getType).toVariable}
-// // val gen = g.builder(subs)
-//
-// // println(f"$t%30s ::= "+gen)
-// //}
-// res
-// }
-}
diff --git a/src/main/scala/leon/grammars/aspects/SimilarTo.scala b/src/main/scala/leon/grammars/aspects/SimilarTo.scala
index cd27a058311f9ab6527ae3d35c414c94ef5760b6..fc500814826f8cf33f79f17f639a56069d82f43b 100644
--- a/src/main/scala/leon/grammars/aspects/SimilarTo.scala
+++ b/src/main/scala/leon/grammars/aspects/SimilarTo.scala
@@ -11,13 +11,13 @@ import purescala.Constructors._
import purescala.Extractors._
import utils.SeqUtils._
-/** Generates expressions similar to a given expression
- * @param e The expression for which similar ones will be generated
+/** Generates expressions similar to a [[Seq]] of given expressions
+ * @param es The expressions for which similar ones will be generated
*/
-case class SimilarTo(e: Expr) extends Aspect {
+case class SimilarTo(es: Seq[Expr]) extends Aspect {
type Prods = Seq[ProductionRule[Label, Expr]]
- def asString(implicit ctx: LeonContext) = "~"+e.asString+"~"
+ def asString(implicit ctx: LeonContext) = es.mkString("~", "~", "~")
def term(e: Expr, tag: Tags.Tag = Tags.Top, cost: Int = 1): ProductionRule[Label, Expr] = {
ProductionRule(Nil, { case Seq() => e }, tag, cost)
@@ -34,7 +34,7 @@ case class SimilarTo(e: Expr) extends Aspect {
case _ => false
}
- val similarProds: Prods = if (isSubtypeOf(e.getType, lab.getType)) {
+ val similarProds: Prods = es.filter(e => isSubtypeOf(e.getType, lab.getType)).flatMap { e =>
val swaps: Prods = e match {
case Operator(as, b) if as.nonEmpty && !isCommutative(e) =>
val ast = as.zipWithIndex.groupBy(_._1.getType).mapValues(_.map(_._2).toList)
@@ -66,7 +66,7 @@ case class SimilarTo(e: Expr) extends Aspect {
case Operator(as, b) if as.nonEmpty =>
for ((a, i) <- as.zipWithIndex) yield {
ProductionRule[Label, Expr](
- List(Label(a.getType).withAspect(SimilarTo(a))),
+ List(Label(a.getType).withAspect(SimilarTo(Seq(a)))),
{ case Seq(e) =>
b(as.updated(i, e))
},
@@ -127,8 +127,6 @@ case class SimilarTo(e: Expr) extends Aspect {
}
swaps ++ subs ++ typeVariations ++ ccVariations
- } else {
- Nil
}
ps ++ similarProds
diff --git a/src/main/scala/leon/grammars/aspects/TypeDepthBound.scala b/src/main/scala/leon/grammars/aspects/TypeDepthBound.scala
new file mode 100644
index 0000000000000000000000000000000000000000..177c6bfd979c39597a5c5ff94ebaa0121ba78fac
--- /dev/null
+++ b/src/main/scala/leon/grammars/aspects/TypeDepthBound.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package grammars
+package aspects
+
+import purescala.TypeOps.depth
+
+case class TypeDepthBound(bound: Int) extends PersistentAspect {
+ override def asString(implicit ctx: LeonContext): String = s"TD$bound"
+
+ override def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: LeonContext) = {
+ if (depth(lab.getType) > bound) Nil
+ else super.applyTo(lab, ps)
+ }
+
+}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index ab6a848df444a3d1d7a39550febfd8a9feac02b9..95045094272c99865089b8ebf845ce8adb9dc7a5 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -190,11 +190,6 @@ object ExprOps extends { val Deconstructor = Operator } with GenTreeOps[Expr] {
}(expr)
}
- /** Computes the depth of the expression's tree */
- def depth(e: Expr): Int = {
- fold[Int]{ (_, sub) => 1 + (0 +: sub).max }(e)
- }
-
/** Applies the function to the I/O constraint and simplifies the resulting constraint */
def applyAsMatches(p : Passes, f : Expr => Expr) = {
f(p.asConstraint) match {
diff --git a/src/main/scala/leon/purescala/GenTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
index bcf6002d156a8bb854bda077e17c5375b6cfaf50..66a7829737898b2bcda91cd93c2e49f11cfb7c54 100644
--- a/src/main/scala/leon/purescala/GenTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -333,4 +333,10 @@ trait GenTreeOps[SubTree <: Tree] {
res
}
+ /** Computes the depth of the expression's tree */
+ def depth(e: SubTree): Int = {
+ fold[Int]{ (_, sub) => 1 + (0 +: sub).max }(e)
+ }
+
+
}
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index e0ba119b7a8299e45d32251fc794b53e3c07a4a8..34db65c8a16e2849f173be77fda04da6aa90aea9 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -14,10 +14,6 @@ object TypeOps extends GenTreeOps[TypeTree] {
val Deconstructor = NAryType
- def typeDepth(t: TypeTree): Int = t match {
- case NAryType(tps, builder) => 1 + (0 +: (tps map typeDepth)).max
- }
-
def typeParamsOf(expr: Expr): Set[TypeParameter] = {
ExprOps.collect(e => typeParamsOf(e.getType))(expr)
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
index 2ec177fc947e42b4810b4c4d16fb9407b592248d..7d15ba8f48934e6b33e966f9aed806f175a1dcba 100644
--- a/src/main/scala/leon/synthesis/rules/CEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala
@@ -13,9 +13,7 @@ import purescala.Types.TypeTree
case object NaiveCEGIS extends CEGISLike("Naive CEGIS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
CegisParams(
- //grammar = Grammars.typeDepthBound(Grammars.default(sctx, p), 2), // This limits type depth
- //rootLabel = {(tpe: TypeTree) => tpe },
- grammar = Grammars.default(sctx, p), // This limits type depth
+ grammar = Grammars.default(sctx, p),
rootLabel = Label(_),
optimizations = false
)
@@ -28,9 +26,7 @@ case object NaiveCEGIS extends CEGISLike("Naive CEGIS") {
case object CEGIS extends CEGISLike("CEGIS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
CegisParams(
- //grammar = TaggedGrammar(base),
- //rootLabel = TaggedNonTerm(_, Tags.Top, 0, None),
- grammar = NaiveCEGIS.getParams(sctx,p).grammar,
+ grammar = Grammars.default(sctx, p),
rootLabel = Label(_).withAspect(Tagged(Tags.Top, 0, None)),
optimizations = true
)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index cdd7d433354334eacbd77e56e9ee39895d21ace8..74bf7133daae772f51182465419dd466222b1c12 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -9,9 +9,9 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Types._
import purescala.ExprOps._
+import purescala.TypeOps.depth
import purescala.DefOps._
import purescala.Constructors._
-import purescala.TypeOps.typeDepth
import solvers._
import grammars._
@@ -77,8 +77,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
val grammar = params.grammar
- //def rootLabel = SizedNonTerm(params.rootLabel(tupleTypeWrap(p.xs.map(_.getType))), termSize)
- def rootLabel = params.rootLabel(targetType).withAspect(Sized(termSize))
+ def rootLabel = params.rootLabel(targetType).withAspect(TypeDepthBound(depth(targetType) + 1)).withAspect(Sized(termSize))
def init(): Unit = {
updateCTree()
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index e29c6d2bc2ceb6a1d01d1c56f42381427be90386..c1c89f6c2935b33cae0fd0014773991c6e45bfe5 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -8,6 +8,7 @@ import purescala.ExprOps._
import purescala.Types._
import purescala.Extractors._
import grammars._
+import grammars.aspects._
import Witnesses._
case object CEGLESS extends CEGISLike("CEGLESS") {
@@ -25,12 +26,9 @@ case object CEGLESS extends CEGISLike("CEGLESS") {
}
}
- val guidedGrammar = Union(guides.map(SimilarTo(_, sctx, p)))
-
CegisParams(
- grammar = guidedGrammar,
- //rootLabel = { (tpe: TypeTree) => NonTerminal(tpe, "G0") },
- rootLabel = { (tpe: TypeTree) => Label(tpe) },
+ grammar = Grammars.default(sctx, p),
+ rootLabel = (tpe: TypeTree) => Label(tpe).withAspect(DepthBound(2)).withAspect(SimilarTo(guides)),
optimizations = false,
maxSize = Some((0 +: guides.map(depth(_) + 1)).max)
)
diff --git a/src/main/scala/leon/synthesis/rules/unused/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/unused/TEGLESS.scala
index 924e9567b04ba53c8eaf56da16bed8e6fba3cc0b..4526148dab62e3f4b7484f0d6f51d6c77c69738c 100644
--- a/src/main/scala/leon/synthesis/rules/unused/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/TEGLESS.scala
@@ -8,6 +8,7 @@ import purescala.Types._
import purescala.Extractors._
import Witnesses._
import grammars._
+import grammars.aspects.{SimilarTo, DepthBound}
case object TEGLESS extends TEGISLike("TEGLESS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
@@ -25,15 +26,9 @@ case object TEGLESS extends TEGISLike("TEGLESS") {
}
}
- val guidedGrammar = guides.map(SimilarTo(_, sctx, p)).foldLeft[ExpressionGrammar](Empty())(_ || _)
-
TegisParams(
- grammar = guidedGrammar,
- //rootLabel = { (tpe: TypeTree) => NonTerminal(tpe, "G0") }
- rootLabel = { (tpe: TypeTree) => Label(tpe) }
+ grammar = Grammars.default(sctx, p),
+ rootLabel = { (tpe: TypeTree) => Label(tpe).withAspect(DepthBound(2)).withAspect(SimilarTo(guides)) }
)
}
}
-
-
-
diff --git a/src/test/scala/leon/integration/grammars/GrammarsSuite.scala b/src/test/scala/leon/integration/grammars/SimilarToSuite.scala
similarity index 95%
rename from src/test/scala/leon/integration/grammars/GrammarsSuite.scala
rename to src/test/scala/leon/integration/grammars/SimilarToSuite.scala
index 71fc0cb55fe92f37123d7c51be9f7984b29119ab..b61d6cb942348b8b6821c0a915e8e3415ee3b987 100644
--- a/src/test/scala/leon/integration/grammars/GrammarsSuite.scala
+++ b/src/test/scala/leon/integration/grammars/SimilarToSuite.scala
@@ -138,19 +138,13 @@ class SimilarToSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
for ((vs, from, exp) <- tests) {
// SimilarTo(<from>) should produce <exp>
- val sctx = new SynthesisContext(fix._1, SynthesisSettings(), ofd.getOrElse(fix._2.definedFunctions.head), fix._2)
- val p = Problem(vs.map(_.id), BooleanLiteral(true), BooleanLiteral(true), BooleanLiteral(true), Nil, ExamplesBank.empty)
-
val g = OneOf(vs)
val enum = new MemoizedEnumerator[Label, Expr, ProductionRule[Label, Expr]](g.getProductions)
- val exprs = enum.iterator(Label(exp.getType).withAspect(SimilarTo(from)))
+ val exprs = enum.iterator(Label(exp.getType).withAspect(SimilarTo(Seq(from))))
//println(s"SimilarTo(${from.asString}):")
- if (!(exprs.exists { e =>
- //println(s" - ${e.asString}")
- e == exp
- })) {
+ if (!exprs.contains(exp)) {
info("Productions: ")
g.printProductions(info(_))