Small improvements

src/main/scala/leon/grammars/DepthBoundedGrammar.scala

@@ -3,9 +3,6 @@
 package leon
 package grammars
 
-import purescala.Types._
-import purescala.Expressions._
-
 case class DepthBoundedGrammar[T](g: ExpressionGrammar[Label[T]], bound: Int) extends ExpressionGrammar[Label[T]] {
   def computeProductions(l: Label[T])(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(l).flatMap {
     case gen =>

src/main/scala/leon/grammars/Label.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package grammars
 

src/main/scala/leon/purescala/Definitions.scala

@@ -406,13 +406,13 @@ object Definitions {
     def subDefinitions = params ++ tparams ++ directlyNestedFuns.toList
 
     /** Duplication of this [[FunDef]].
-      * @note This will not replace recursive function calls
+      * @note This will not replace recursive function calls in [[fullBody]]
       */
     def duplicate(
-      id: Identifier = this.id.freshen,
-      tparams: Seq[TypeParameterDef] = this.tparams,
-      params: Seq[ValDef] = this.params,
-      returnType: TypeTree = this.returnType
+      id: Identifier                  = this.id.freshen,
+      tparams: Seq[TypeParameterDef]  = this.tparams,
+      params: Seq[ValDef]             = this.params,
+      returnType: TypeTree            = this.returnType
     ): FunDef = {
       val fd = new FunDef(id, tparams, params, returnType)
       fd.fullBody = this.fullBody

src/main/scala/leon/synthesis/graph/Graph.scala

@@ -28,11 +28,10 @@ sealed class Graph(val cm: CostModel, problem: Problem) {
 }
 
 sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
-  var parents: List[Node]     = parent.toList
-  var descendants: List[Node] = Nil
 
   def asString(implicit ctx: LeonContext): String
 
+  var descendants: List[Node] = Nil
   // indicates whether this particular node has already been expanded
   var isExpanded: Boolean = false
   def expand(hctx: SearchContext)
@@ -53,7 +52,7 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
     cm.isImpossible(cost)
   }
 
-  // For non-terminals, selected childs for solution
+  // For non-terminals, selected children for solution
   var selected: List[Node] = Nil
 
   def composeSolutions(sols: List[Stream[Solution]]): Stream[Solution]
@@ -94,7 +93,7 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
 
   def updateCost(): Unit = {
     cost = computeCost()
-    parents.foreach(_.updateCost())
+    parent.foreach(_.updateCost())
   }
 }
 
@@ -136,7 +135,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
           info(prefix+"Solved"+(if(sol.isTrusted) "" else " (untrusted)")+" with: "+sol.asString+"...")
         }
 
-        parents.foreach{ p =>
+        parent.foreach{ p =>
           p.updateCost()
           if (isSolved) {
             p.onSolved(this)
@@ -172,7 +171,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
     // Everything is solved correctly
     if (solveds.size == descendants.size) {
       isSolved = true
-      parents.foreach(_.onSolved(this))
+      parent.foreach(_.onSolved(this))
     }
   }
 
@@ -221,7 +220,7 @@ class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(c
   def onSolved(desc: Node): Unit = {
     isSolved = true
     selected = List(desc)
-    parents.foreach(_.onSolved(this))
+    parent.foreach(_.onSolved(this))
   }
 
   def composeSolutions(solss: List[Stream[Solution]]): Stream[Solution] = {

src/main/scala/leon/synthesis/rules/CEGISLike.scala

@@ -114,9 +114,9 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
         private var slots = Map[SizedLabel[T], Int]().withDefaultValue(0)
 
-        private def streamOf(t: SizedLabel[T]): Stream[Identifier] = {
-          FreshIdentifier(t.asString, t.getType, true) #:: streamOf(t)
-        }
+        private def streamOf(t: SizedLabel[T]): Stream[Identifier] = Stream.continually(
+          FreshIdentifier(t.asString, t.getType, true)
+        )
 
         def rewind(): Unit = {
           slots = Map[SizedLabel[T], Int]().withDefaultValue(0)
@@ -385,8 +385,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
         //println(programCTree.asString)
         //println(".. "*30)
 
-        //val evaluator  = new DualEvaluator(sctx.context, programCTree, CodeGenParams.default)
-        val evaluator  = new DefaultEvaluator(sctx.context, programCTree)
+        //val evaluator = new DualEvaluator(sctx.context, programCTree, CodeGenParams.default)
+        val evaluator = new DefaultEvaluator(sctx.context, programCTree)
 
         tester =
           { (ex: Example, bValues: Set[Identifier]) =>
@@ -679,7 +679,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           baseExampleInputs += InExample(p.as.map(a => simplestValue(a.getType)))
         } else {
           val solverf = sctx.solverFactory
-          val solver  = solverf.getNewSolver.setTimeout(exSolverTo)
+          val solver  = solverf.getNewSolver().setTimeout(exSolverTo)
 
           solver.assertCnstr(p.pc)
 
@@ -892,8 +892,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
                         } else {
                           result = Some(RuleFailed())
                         }
-                      }
                     }
+                  }
 
                 case Some(None) =>
                   skipCESearch = true