diff --git a/src/main/scala/leon/grammars/FunctionCalls.scala b/src/main/scala/leon/grammars/FunctionCalls.scala
index c8110a0208d5c893b2b56bb33751586436fe8ca8..00b0ef2be3f0612119e3dda4ae965444be5bbfaa 100644
--- a/src/main/scala/leon/grammars/FunctionCalls.scala
+++ b/src/main/scala/leon/grammars/FunctionCalls.scala
@@ -19,66 +19,67 @@ import purescala.Expressions._
case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[TypeTree], exclude: Set[FunDef]) extends SimpleExpressionGrammar {
def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Prod] = {
- def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
- // Prevents recursive calls
- val cfd = currentFunction
+ def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
+ // Prevents recursive calls
+ val cfd = currentFunction
- val isRecursiveCall = (prog.callGraph.transitiveCallers(cfd) + cfd) contains fd
+ val isRecursiveCall = (prog.callGraph.transitiveCallers(cfd) + cfd) contains fd
- val isDet = fd.body.exists(isDeterministic)
+ val isDet = fd.body.exists(isDeterministic)
- if (!isRecursiveCall && isDet) {
- val free = fd.tparams.map(_.tp)
+ if (!isRecursiveCall && isDet) {
+ val free = fd.tparams.map(_.tp)
- canBeSubtypeOf(fd.returnType, free, t, rhsFixed = true) match {
- case Some(tpsMap) =>
- val tfd = fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp)))
+ canBeSubtypeOf(fd.returnType, free, t, rhsFixed = true) match {
+ case Some(tpsMap) =>
+ val tfd = fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp)))
- if (tpsMap.size < free.size) {
- /* Some type params remain free, we want to assign them:
- *
- * List[T] => Int, for instance, will be found when
- * requesting Int, but we need to assign T to viable
- * types. For that we use list of input types as heuristic,
- * and look for instantiations of T such that input <?:
- * List[T].
- */
- types.distinct.flatMap { (atpe: TypeTree) =>
- var finalFree = free.toSet -- tpsMap.keySet
- var finalMap = tpsMap
+ if (tpsMap.size < free.size) {
+ /* Some type params remain free, we want to assign them:
+ *
+ * List[T] => Int, for instance, will be found when
+ * requesting Int, but we need to assign T to viable
+ * types. For that we use list of input types as heuristic,
+ * and look for instantiations of T such that input <?:
+ * List[T].
+ */
+ types.distinct.flatMap { (atpe: TypeTree) =>
+ var finalFree = free.toSet -- tpsMap.keySet
+ var finalMap = tpsMap
- for (ptpe <- tfd.params.map(_.getType).distinct) {
- canBeSubtypeOf(atpe, finalFree.toSeq, ptpe) match {
- case Some(ntpsMap) =>
- finalFree --= ntpsMap.keySet
- finalMap ++= ntpsMap
- case _ =>
- }
- }
+ for (ptpe <- tfd.params.map(_.getType).distinct) {
+ canBeSubtypeOf(atpe, finalFree.toSeq, ptpe) match {
+ case Some(ntpsMap) =>
+ finalFree --= ntpsMap.keySet
+ finalMap ++= ntpsMap
+ case _ =>
+ }
+ }
- if (finalFree.isEmpty) {
- List(fd.typed(free.map(tp => finalMap.getOrElse(tp, tp))))
- } else {
- Nil
- }
- }
- } else {
- // All type parameters that used to be free are assigned
- List(tfd)
- }
- case None =>
- Nil
- }
- } else {
- Nil
- }
- }
+ if (finalFree.isEmpty) {
+ List(fd.typed(free.map(tp => finalMap.getOrElse(tp, tp))))
+ } else {
+ Nil
+ }
+ }
+ } else {
+ // All type parameters that used to be free are assigned
+ List(tfd)
+ }
+ case None =>
+ Nil
+ }
+ } else {
+ Nil
+ }
+ }
- val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || tfd.fd.isInner || (exclude contains tfd.fd)
- val funcs = visibleFunDefsFromMain(prog).toSeq.sortBy(_.id).flatMap(getCandidates).filterNot(filter)
+ val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || tfd.fd.isInner || (exclude contains tfd.fd)
- funcs.map{ tfd =>
- nonTerminal(tfd.params.map(_.getType), FunctionInvocation(tfd, _), Tags.tagOf(tfd.fd, isSafe = false))
- }
- }
+ val funcs = visibleFunDefsFromMain(prog).toSeq.sortBy(_.id).flatMap(getCandidates).filterNot(filter)
+
+ funcs.map{ tfd =>
+ nonTerminal(tfd.params.map(_.getType), FunctionInvocation(tfd, _), Tags.tagOf(tfd.fd, isSafe = false))
+ }
}
+}
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 690ba4b87868cb14e109a56732b8aaddd53f26d3..ed22fa0ec21d19c27a083c8bf93f48e22973df7d 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -167,7 +167,9 @@ object ExamplesBank {
* allows us to evaluate expressions. */
case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb: ExamplesBank)(implicit hctx: SearchContext) {
- lazy val evaluator = new DefaultEvaluator(hctx, hctx.program).setEvaluationFailOnChoose(true)
+ // TODO: This might be slightly conservative. We might want something closer to a partial evaluator,
+ // to conserve things like (e: A).isInstanceOf[A] even when evaluation of e leads to choose
+ private lazy val evaluator = new DefaultEvaluator(hctx, hctx.program).setEvaluationFailOnChoose(true)
def removeOuts(toRemove: Set[Identifier]): QualifiedExamplesBank = {
val nxs = xs.filterNot(toRemove)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 4a9a277b6851b25d6999436a61e0237e1be56129..41e82c459b70fa61da686a89a1041433f6a599e4 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -441,7 +441,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
// This program contains a simplifiable expression,
// which means it is equivalent to a simpler one
- // Deactivated for now, since it doesnot seem to help
+ // Deactivated for now, since it does not seem to help
if (redundancyCheck && params.optimizations && exists(redundant)(outerSol)) {
excludeProgram(bs, true)
return Some(false)