SimilarTo should not traverse exprs binding variables

src/main/scala/leon/synthesis/Rules.scala

@@ -28,6 +28,7 @@ object Rules {
     TEGIS,
     GuidedDecomp,
     GuidedCloser,
+    CEGLESS,
     rules.Assert,
     DetupleOutput,
     DetupleInput,

src/main/scala/leon/synthesis/rules/Cegis.scala

@@ -33,10 +33,33 @@ case object CEGIS extends CEGISLike("CEGIS") {
   }
 }
 
+case object CEGLESS extends CEGISLike("CEGLESS") {
+  override val maxUnrolings = 2;
+
+  def getGrammar(sctx: SynthesisContext, p: Problem) = {
+    import ExpressionGrammars._
+
+    val TopLevelAnds(clauses) = p.pc
+
+    val guide = sctx.program.library.guide.get
+
+    val guides = clauses.collect {
+      case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+    }
+
+    val guidedGrammar = guides.map(SimilarTo(_)).foldLeft[ExpressionGrammar](Empty)(_ || _)
+
+    guidedGrammar || OneOf(p.as.map(_.toVariable))
+  }
+}
+
 
 abstract class CEGISLike(name: String) extends Rule(name) {
+
   def getGrammar(sctx: SynthesisContext, p: Problem): ExpressionGrammar
 
+  val maxUnrolings = 3
+
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
 
     // CEGIS Flags to actiave or de-activate features
@@ -395,7 +418,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
 
         val ndProgram = new NonDeterministicProgram(p, initGuard)
         var unrolings = 1
-        val maxUnrolings = 3
+        val maxUnrolings = CEGISLike.this.maxUnrolings
 
         val exSolverTo  = 2000L
         val cexSolverTo = 2000L

src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala

@@ -34,7 +34,7 @@ abstract class ExpressionGrammar {
   def computeProductions(t: TypeTree): Seq[Gen]
 
   final def ||(that: ExpressionGrammar): ExpressionGrammar = {
-    ExpressionGrammar.Or(Seq(this, that))
+    ExpressionGrammars.Or(Seq(this, that))
   }
 
   final def printProductions(printer: String => Unit) {
@@ -47,7 +47,8 @@ abstract class ExpressionGrammar {
   }
 }
 
-object ExpressionGrammar {
+object ExpressionGrammars {
+
   case class Or(gs: Seq[ExpressionGrammar]) extends ExpressionGrammar {
     val subGrammars: Seq[ExpressionGrammar] = gs.flatMap {
       case o: Or => o.subGrammars
@@ -57,9 +58,10 @@ object ExpressionGrammar {
     def computeProductions(t: TypeTree): Seq[Gen] =
       subGrammars.flatMap(_.getProductions(t))
   }
-}
 
-object ExpressionGrammars {
+  case object Empty extends ExpressionGrammar {
+    def computeProductions(t: TypeTree): Seq[Gen] = Nil
+  }
 
   case object BaseGrammar extends ExpressionGrammar {
     def computeProductions(t: TypeTree): Seq[Gen] = t match {
@@ -128,23 +130,23 @@ object ExpressionGrammars {
       def rec(e : Expr) : Seq[(TypeTree, Gen)] = {
         val tp = e.getType
         const(e) +: (e match {
-          case t : Terminal =>
+          case _: Terminal | _: Let | _: LetTuple | _: LetDef | _: MatchExpr =>
             Seq()
           case UnaryOperator(sub, builder) => Seq(
             gen( sub.getType, tp, { case Seq(ex) => builder(ex) } )
-          )
+          ) ++ rec(sub)
           case BinaryOperator(sub1, sub2, builder) => Seq(
             gen( sub1.getType, tp, { case Seq(ex) => builder(ex, sub2) } ),
             gen( sub2.getType, tp, { case Seq(ex) => builder(sub1, ex) } )
-          )
+          ) ++ rec(sub1) ++ rec(sub2)
           case NAryOperator(subs, builder) => 
-            for ((sub,index) <- subs.zipWithIndex) yield {
+            (for ((sub,index) <- subs.zipWithIndex) yield {
               gen( sub.getType, tp, { case Seq(ex) => builder(subs updated (index, ex) )} )
-            }
+            }) ++ subs.flatMap(rec)
         })
       }
 
-      collectPreorder(rec)(e).tail // Don't want the expression itself
+      rec(e).tail // Don't want the expression itself
     }
   }
 

src/main/scala/leon/utils/Simplifiers.scala

@@ -51,7 +51,6 @@ object Simplifiers {
       simplifyPaths(uninterpretedZ3)(_),
       patternMatchReconstruction _,
       rewriteTuples _,
-      evalGround(ctx, p),
       normalizeExpression _
     )