Code explosion in mergeCalls about inox HOT 3 CLOSED

val (trec, tClauses) = mkExprClauses(newBool1, thenn, localSubst, pol)
val (erec, eClauses) = mkExprClauses(newBool2, elze, localSubst, pol)
builder ++= mergeCalls(pathVar, localSubst, tClauses, eClauses)

def mergeCalls(pathVar: Variable, condVar: Variable, substMap: Map[Variable, Encoded],
               thenClauses: TemplateClauses, elseClauses: TemplateClauses): TemplateClauses = {
  val builder = new Builder(pathVar, substMap)
  builder ++= thenClauses
  builder ++ elseClauses

  // Clear all guardedExprs in builder since we're going to transform them by merging calls.
  // The transformed guardedExprs will be added to builder at the end of the function.
  builder.guardedExprs = Map.empty

  def collectCalls(expr: Expr): Set[FunctionInvocation] =
    exprOps.collect { case fi: FunctionInvocation => Set(fi) case _ => Set.empty[FunctionInvocation] }(expr)
  def countCalls(expr: Expr): Int =
    exprOps.count { case fi: FunctionInvocation => 1 case _ => 0}(expr)
  def replaceCall(call: FunctionInvocation, newExpr: Expr)(e: Expr): Expr =
    exprOps.replace(Map(call, newExpr), e)

  def getCalls(guardedExprs: Map[Variable, Seq[Expr]]): Map[TypedFunDef, Seq[(FunctionInvocation, Set[Variable])]] =
    (for {(b, es) <- guardedExprs; e <- es; fi <- collectCalls(e)) yield (b -> fi))
    .groupBy(_._2)
    .mapValues(_.map(_._1).toSet)
    .toSeq
    .groupBy(_._1.tfd)
    .mapValues(_.toList.distinct.sortBy(p => countCalls(p._1)))  // place inner calls first
    .toMap

  var thenGuarded = thenClauses._4
  var elseGuarded = elseClauses._4

  val thenCalls = getCalls(thenGuarded)
  val elseCalls = getCalls(elseGuarded)

  // We sort common function calls in order to merge nested calls first.
  var toMerge = (thenCalls.keys() & elseCalls.keys())
    .flatMap(tfd => thenCalls(tfd) zip elseCalls(tfd))
    .toSeq
    .sortBy(p => countCalls(p._1._1) + countCalls(p._2._1))

  while (toMerge.nonEmpty) {
    val ((thenCall, thenBlockers), (elseCall, elseBlockers)) = toMerge.head
    toMerge = toMerge.tail

    val newExpr: Variable = Variable.fresh("call", thenCall.tfd.getType, true)
    builder.storeExpr(newExpr)

    val replaceThen = replaceCall(thenCall, newExpr) _
    val replaceElse = replaceCall(elseCall, newExpr) _

    thenGuarded = thenGuarded.mapValues(_.map(replaceThen)
    elseGuarded = elseGuarded.mapValues(_.map(replaceElse)
    toMerge = toMerge.map(p => (replaceThen(p._1), replaceElse(p._2))

    val newBlocker: Variable = Variable.fresh("bm", BooleanType(), true)
    // TODO: make this a method in Builder similar to storeCond
    builder.storeConds(thenBlockers ++ elseBlockers, newBlocker)
    builder.iff(orJoin((thenBlockers ++ elseBlockers).toSeq), newBlocker)

    val newArgs = (thenCall.args zip elseCall.args).map { case (thenArg, elseArg) =>
      val (newArg, argClauses) = mkExprClauses(newBlocker, IfExpr(condVar, thenArg, elseArg), builder.localSubst)
      builder ++= argClauses
      newArg
    }

    val newCall = thenCall.tfd.applied(newArgs)
    builder.storeGuarded(newBlocker, Equals(newExpr, newCall))
  }

  for ((b, es) <- thenGuarded; e <- es) builder.storeGuarded(b, e)
  for ((b, es) <- elseGuarded; e <- es) builder.storeGuarded(b, e)
  builder.result
}