From 53d41d0253b33399af0b8314a8aed0f36c61d6c4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 16 Mar 2015 12:51:40 +0100
Subject: [PATCH] ExpressionGrammars should ignore synthetic functions
---
src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 23cd164dd..f44f23717 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -300,6 +300,7 @@ object ExpressionGrammars {
}
}
+ val funFilter = (fd: FunDef) => fd.isSynthetic || (excludeFCalls contains fd)
val subs: Seq[(L, Gen)] = (e match {
case _: Terminal | _: Let | _: LetDef | _: MatchExpr =>
@@ -308,7 +309,7 @@ object ExpressionGrammars {
case cc @ CaseClass(cct, exprs) =>
gens(e, gl, exprs, { case ss => CaseClass(cct, ss) }) ++ ccVariations(gl, cc)
- case FunctionInvocation(TypedFunDef(fd, _), _) if excludeFCalls contains fd =>
+ case FunctionInvocation(TypedFunDef(fd, _), _) if funFilter(fd) =>
// We allow only exact call, and/or cegis extensions
/*Seq(el -> Generator[L, Expr](Nil, { _ => e })) ++*/ cegis(gl)
@@ -401,7 +402,8 @@ object ExpressionGrammars {
}
}
- val funcs = functionsAvailable(prog).toSeq.flatMap(getCandidates).filterNot( tfd => exclude contains tfd.fd)
+ val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || (exclude contains tfd.fd)
+ val funcs = functionsAvailable(prog).toSeq.flatMap(getCandidates).filterNot(filter)
funcs.map{ tfd =>
Generator[TypeTree, Expr](tfd.params.map(_.getType), { sub => FunctionInvocation(tfd, sub) })
--
GitLab