diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index d65eedf8199bae266604d3141f1e84db5bf41588..a47f702c9ad0e6c6c1ac953eea24917e0245a4e8 100644 --- a/src/main/scala/leon/purescala/TreeOps.scala +++ b/src/main/scala/leon/purescala/TreeOps.scala @@ -318,6 +318,10 @@ object TreeOps { def collect[T](matcher: Expr => Set[T])(e: Expr): Set[T] = { foldRight[Set[T]]({ (e, subs) => matcher(e) ++ subs.foldLeft(Set[T]())(_ ++ _) } )(e) } + + def collectPreorder[T](matcher: Expr => Seq[T])(e: Expr): Seq[T] = { + foldRight[Seq[T]]({ (e, subs) => matcher(e) ++ subs.foldLeft(Set[T]())(_ ++ _) } )(e) + } def filter(matcher: Expr => Boolean)(e: Expr): Set[Expr] = { collect[Expr] { e => if (matcher(e)) Set(e) else Set() }(e) diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala index a9c606ab7fdb950ac453b8196bd3bf892f1e4394..be13325bdc41f410c154ea5a18997887e6431be5 100644 --- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala +++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala @@ -110,6 +110,44 @@ object ExpressionGrammars { } } + case class SimilarTo(e: Expr) extends ExpressionGrammar { + lazy val allSimilar = computeSimilar(e).groupBy(_._1).mapValues(_.map(_._2)) + + def computeProductions(t: TypeTree): Seq[Gen] = { + allSimilar.getOrElse(t, Nil) + } + + def computeSimilar(e : Expr) : Seq[(TypeTree, Gen)] = { + + def gen(tp : TypeTree, retType : TypeTree, f : Seq[Expr] => Expr) : (TypeTree, Gen) = + (retType, Generator[TypeTree, Expr](Seq(tp),f)) + + // A generator that always regenerates its input + def const(e: Expr) = ( e.getType, Generator[TypeTree, Expr](Seq(), _ => e) ) + + def rec(e : Expr) : Seq[(TypeTree, Gen)] = { + val tp = e.getType + const(e) +: (e match { + case t : Terminal => + Seq() + case UnaryOperator(sub, builder) => Seq( + gen( sub.getType, tp, { case Seq(ex) => builder(ex) } ) + ) + 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) } ) + ) + case NAryOperator(subs, builder) => + for ((sub,index) <- subs.zipWithIndex) yield { + gen( sub.getType, tp, { case Seq(ex) => builder(subs updated (index, ex) )} ) + } + }) + } + + collectPreorder(rec)(e).tail // Don't want the expression itself + } + } + case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[TypeTree]) extends ExpressionGrammar { def computeProductions(t: TypeTree): Seq[Gen] = {