From 15be6120b66c30d01436af330e98bb1b3889a6c9 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 5 Nov 2014 15:57:59 +0100
Subject: [PATCH] SimilarTo should not traverse exprs binding variables
---
src/main/scala/leon/synthesis/Rules.scala | 1 +
.../scala/leon/synthesis/rules/Cegis.scala | 25 ++++++++++++++++++-
.../synthesis/utils/ExpressionGrammar.scala | 22 ++++++++--------
src/main/scala/leon/utils/Simplifiers.scala | 1 -
4 files changed, 37 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 9623624af..efaca2093 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -28,6 +28,7 @@ object Rules {
TEGIS,
GuidedDecomp,
GuidedCloser,
+ CEGLESS,
rules.Assert,
DetupleOutput,
DetupleInput,
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 98ca2a4b2..33b583d39 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/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
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index be13325bd..3072a6999 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/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
}
}
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 4791d5a07..da10dd8f2 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -51,7 +51,6 @@ object Simplifiers {
simplifyPaths(uninterpretedZ3)(_),
patternMatchReconstruction _,
rewriteTuples _,
- evalGround(ctx, p),
normalizeExpression _
)
--
GitLab