diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala index b0de64ed05458d22cc113170dc850e2c1e2f6a3b..cef8eb560a45f48c917b776677af522f8484db82 100644 --- a/src/main/scala/leon/synthesis/rules/CEGIS.scala +++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala @@ -12,7 +12,7 @@ import purescala.Types.TypeTree case object NaiveCEGIS extends CEGISLike[TypeTree]("Naive CEGIS") { def getParams(sctx: SynthesisContext, p: Problem) = { CegisParams( - grammar = Grammars.typeDepthBound(Grammars.default(sctx, p), 2), // This limits type depth + grammar = Grammars.default(sctx, p), // This limits type depth rootLabel = {(tpe: TypeTree) => tpe }, optimizations = false ) diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala index 6f340554da971b0d833fe3c27998ab39540d21ee..a12f0ed34d48806927a0fa9f581b06027aee040d 100644 --- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala +++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala @@ -11,6 +11,7 @@ import purescala.Types._ import purescala.ExprOps._ import purescala.DefOps._ import purescala.Constructors._ +import purescala.TypeOps.typeDepth import solvers._ import grammars._ @@ -70,9 +71,14 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) { def unfolding = termSize - val grammar = SizeBoundedGrammar(params.grammar, params.optimizations) + private val targetType = tupleTypeWrap(p.xs.map(_.getType)) - def rootLabel = SizedNonTerm(params.rootLabel(tupleTypeWrap(p.xs.map(_.getType))), termSize) + val grammar = SizeBoundedGrammar( + Grammars.typeDepthBound(params.grammar, typeDepth(targetType)), + params.optimizations + ) + + def rootLabel = SizedNonTerm(params.rootLabel(targetType), termSize) def init(): Unit = { updateCTree()