diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/Cegless.scala index c4789c8a05a914072037cbb23722e0d06f50bbe2..b2c35de16c6fe3a822ecef487d55266743288972 100644 --- a/src/main/scala/leon/synthesis/rules/Cegless.scala +++ b/src/main/scala/leon/synthesis/rules/Cegless.scala @@ -26,7 +26,7 @@ case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") { val inputs = p.as.map(_.toVariable) - val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, Set(sctx.functionContext))).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _) + val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _) CegisParams( grammar = guidedGrammar, diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala index 58eb0f5827450cde0038f9567cc02e3b9cf27fad..8e422986bf633d073b52f3a8c2326d7cfb1f0188 100644 --- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala +++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala @@ -167,7 +167,7 @@ object ExpressionGrammars { override def toString = t.toString+"@"+l } - case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), excludeFCalls: Set[FunDef] = Set()) extends ExpressionGrammar[Label[String]] { + case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[Label[String]] { type L = Label[String] @@ -195,6 +195,14 @@ object ExpressionGrammars { case _ => false } + val normalGrammar = EmbededGrammar( + ExpressionGrammars.default(sctx, p), + { (t: TypeTree) => Label(t, "B")}, + { (l: Label[String]) => l.getType } + ) + + val excludeFCalls = Set(sctx.functionContext) + def rec(e: Expr, el: L, gl: L): Seq[(L, Gen)] = { def gens(e: Expr, el: L, gl: L, subs: Seq[Expr], builder: (Seq[Expr] => Expr)): Seq[(L, Gen)] = { @@ -227,7 +235,14 @@ object ExpressionGrammars { Nil } - allSubs ++ exact ++ injectG ++ swaps + // if e is a terminal, we also rely on standard CEGIS + val fallback = if (subs.size == 0) { + normalGrammar.getProductions(gl).map(gl -> _) + } else { + Nil + } + + allSubs ++ exact ++ injectG ++ swaps ++ fallback } val subs: Seq[(L, Gen)] = e match { @@ -333,6 +348,14 @@ object ExpressionGrammars { } } + case class EmbededGrammar[Ti <% Typed, To <% Typed](g: ExpressionGrammar[Ti], iToo: Ti => To, oToi: To => Ti) extends ExpressionGrammar[To] { + + def computeProductions(t: To): Seq[Gen] = g.computeProductions(oToi(t)).map { + case g : Generator[Ti, Expr] => + Generator(g.subTrees.map(iToo), g.builder) + } + } + case class SafeRecCalls(prog: Program, ws: Expr, pc: Expr) extends ExpressionGrammar[TypeTree] { def computeProductions(t: TypeTree): Seq[Gen] = { val calls = terminatingCalls(prog, t, ws, pc)