From 978df2d3c071c10f3882234ea08cdfa4c3f5d22b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 7 Mar 2016 16:03:32 +0100
Subject: [PATCH] Simplify SimilarTo
Use Grammars.default
Remove SafeRecursiveCalls
---
src/main/scala/leon/grammars/Grammars.scala | 4 ++--
src/main/scala/leon/grammars/SimilarTo.scala | 19 +++++++------------
.../scala/leon/synthesis/rules/CEGLESS.scala | 4 +---
.../scala/leon/synthesis/rules/TEGLESS.scala | 4 +---
4 files changed, 11 insertions(+), 20 deletions(-)
diff --git a/src/main/scala/leon/grammars/Grammars.scala b/src/main/scala/leon/grammars/Grammars.scala
index 762ea5325..fcbc628c4 100644
--- a/src/main/scala/leon/grammars/Grammars.scala
+++ b/src/main/scala/leon/grammars/Grammars.scala
@@ -24,10 +24,10 @@ object Grammars {
FunctionCalls(prog, currentFunction, inputs.map(_.getType), exclude)
}
- def default(sctx: SynthesisContext, p: Problem): ExpressionGrammar[TypeTree] = {
+ def default(sctx: SynthesisContext, p: Problem, extraHints: Seq[Expr] = Seq()): ExpressionGrammar[TypeTree] = {
val TopLevelAnds(ws) = p.ws
val hints = ws.collect{ case Hint(e) if formulaSize(e) >= 4 => e }
- default(sctx.program, p.as.map(_.toVariable) ++ hints, sctx.functionContext, sctx.settings.functionsToIgnore)
+ default(sctx.program, p.as.map(_.toVariable) ++ hints ++ extraHints, sctx.functionContext, sctx.settings.functionsToIgnore)
}
def typeDepthBound[T <: Typed](g: ExpressionGrammar[T], b: Int) = {
diff --git a/src/main/scala/leon/grammars/SimilarTo.scala b/src/main/scala/leon/grammars/SimilarTo.scala
index 4d2ee3f45..6b2f3f538 100644
--- a/src/main/scala/leon/grammars/SimilarTo.scala
+++ b/src/main/scala/leon/grammars/SimilarTo.scala
@@ -14,20 +14,15 @@ import synthesis._
/** A grammar that generates expressions by inserting small variations in [[e]]
* @param e The [[Expr]] to which small variations will be inserted
- * @param terminals A set of [[Expr]]s that may be inserted into [[e]] as small variations
*/
-case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[NonTerminal[String]] {
+case class SimilarTo(e: Expr, sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[NonTerminal[String]] {
val excludeFCalls = sctx.settings.functionsToIgnore
val normalGrammar: ExpressionGrammar[NonTerminal[String]] = DepthBoundedGrammar(EmbeddedGrammar(
- BaseGrammar ||
- EqualityGrammar(Set(IntegerType, Int32Type, BooleanType) ++ terminals.map { _.getType }) ||
- OneOf(terminals.toSeq :+ e) ||
- FunctionCalls(sctx.program, sctx.functionContext, p.as.map(_.getType), excludeFCalls) ||
- SafeRecursiveCalls(sctx.program, p.ws, p.pc),
- { (t: TypeTree) => NonTerminal(t, "B", None)},
- { (l: NonTerminal[String]) => l.getType }
+ Grammars.default(sctx, p, Seq(e)),
+ (t: TypeTree) => NonTerminal(t, "B", None),
+ (l: NonTerminal[String]) => l.getType
), 1)
type L = NonTerminal[String]
@@ -148,9 +143,9 @@ case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisConte
gens(e, gl, subs, { case ss => builder(ss) })
}
- val terminalsMatching = terminals.collect {
- case IsTyped(term, tpe) if tpe == gl.getType && term != e =>
- gl -> terminal(term)
+ val terminalsMatching = p.as.collect {
+ case IsTyped(term, tpe) if tpe == gl.getType && Variable(term) != e =>
+ gl -> terminal(Variable(term))
}
val variations = e.getType match {
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index 52d6af00f..d59e99011 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -19,8 +19,6 @@ case object CEGLESS extends CEGISLike[NonTerminal[String]]("CEGLESS") {
case Guide(e) => e
}
- val inputs = p.as.map(_.toVariable)
-
sctx.reporter.ifDebug { printer =>
printer("Guides available:")
for (g <- guides) {
@@ -28,7 +26,7 @@ case object CEGLESS extends CEGISLike[NonTerminal[String]]("CEGLESS") {
}
}
- val guidedGrammar = Union(guides.map(SimilarTo(_, inputs.toSet, sctx, p)))
+ val guidedGrammar = Union(guides.map(SimilarTo(_, sctx, p)))
CegisParams(
grammar = guidedGrammar,
diff --git a/src/main/scala/leon/synthesis/rules/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
index dfc38ed16..f87968ea3 100644
--- a/src/main/scala/leon/synthesis/rules/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
@@ -19,8 +19,6 @@ case object TEGLESS extends TEGISLike[NonTerminal[String]]("TEGLESS") {
case Guide(expr) => expr
}
- val inputs = p.as.map(_.toVariable)
-
sctx.reporter.ifDebug { printer =>
printer("Guides available:")
for (g <- guides) {
@@ -28,7 +26,7 @@ case object TEGLESS extends TEGISLike[NonTerminal[String]]("TEGLESS") {
}
}
- val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[NonTerminal[String]]](Empty())(_ || _)
+ val guidedGrammar = guides.map(SimilarTo(_, sctx, p)).foldLeft[ExpressionGrammar[NonTerminal[String]]](Empty())(_ || _)
TegisParams(
grammar = guidedGrammar,
--
GitLab