Introduce ProductionRules costs to fix SafeFunctionCall cost

src/main/scala/leon/grammars/ExpressionGrammar.scala

@@ -22,13 +22,13 @@ abstract class ExpressionGrammar[T <: Typed] {
   private[this] val cache = new MutableMap[T, Seq[Prod]]()
 
   /** Generates a [[ProductionRule]] without nonterminal symbols */
-  def terminal(builder: => Expr, tag: Tags.Tag = Tags.Top) = {
-    ProductionRule[T, Expr](Nil, { (subs: Seq[Expr]) => builder }, tag)
+  def terminal(builder: => Expr, tag: Tags.Tag = Tags.Top, cost: Int = 1) = {
+    ProductionRule[T, Expr](Nil, { (subs: Seq[Expr]) => builder }, tag, cost)
   }
 
   /** Generates a [[ProductionRule]] with nonterminal symbols */
-  def nonTerminal(subs: Seq[T], builder: (Seq[Expr] => Expr), tag: Tags.Tag = Tags.Top): ProductionRule[T, Expr] = {
-    ProductionRule[T, Expr](subs, builder, tag)
+  def nonTerminal(subs: Seq[T], builder: (Seq[Expr] => Expr), tag: Tags.Tag = Tags.Top, cost: Int = 1): ProductionRule[T, Expr] = {
+    ProductionRule[T, Expr](subs, builder, tag, cost)
   }
 
   /** The list of production rules for this grammar for a given nonterminal.

src/main/scala/leon/grammars/ProductionRule.scala

@@ -14,5 +14,5 @@ import bonsai.Generator
  *  @tparam T The type of nonterminal symbols of the grammar
  *  @tparam R The type of syntax trees of the grammar
  */
-case class ProductionRule[T, R](override val subTrees: Seq[T], override val builder: Seq[R] => R, tag: Tags.Tag)
+case class ProductionRule[T, R](override val subTrees: Seq[T], override val builder: Seq[R] => R, tag: Tags.Tag, cost: Int = 1)
   extends Generator[T,R](subTrees, builder)

src/main/scala/leon/grammars/SafeRecursiveCalls.scala

@@ -25,7 +25,8 @@ case class SafeRecursiveCalls(prog: Program, ws: Expr, pc: Expr) extends Express
         nonTerminal(
           freeSeq.map(_.getType),
           { sub => replaceFromIDs(freeSeq.zip(sub).toMap, fi) },
-          Tags.tagOf(fi.tfd.fd, isSafe = true)
+          Tags.tagOf(fi.tfd.fd, isSafe = true),
+          2
         )
     }
   }

src/main/scala/leon/grammars/transformers/SizeBoundedGrammar.scala

@@ -43,9 +43,9 @@ case class SizeBoundedGrammar[T <: Typed](g: ExpressionGrammar[T], optimizeCommu
         // Optimization: When we have a commutative operation and all the labels are the same,
         // we can skew the expression to always be right-heavy
         val sizes = if(optimizeCommut && Tags.isCommut(gen.tag) && gen.subTrees.map(characteristic).toSet.size == 1) {
-          sumToOrdered(sl.size-1, gen.arity)
+          sumToOrdered(sl.size-gen.cost, gen.arity)
         } else {
-          sumTo(sl.size-1, gen.arity)
+          sumTo(sl.size-gen.cost, gen.arity)
         }
 
         for (ss <- sizes) yield {

src/main/scala/leon/utils/SeqUtils.scala

@@ -34,7 +34,10 @@ object SeqUtils {
   }
 
   def sumTo(sum: Int, arity: Int): Seq[Seq[Int]] = {
-    if (arity == 1) {
+    require(arity >= 1)
+    if (sum < arity) {
+      Nil
+    } else if (arity == 1) {
       Seq(Seq(sum))
     } else {
       (1 until sum).flatMap{ n =>