Simplify CostModels (and InputSplit)

src/main/scala/leon/repair/RepairCostModel.scala

@@ -8,9 +8,9 @@ import synthesis.rules._
 import repair.rules._
 
 case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("+cm.name+")") {
-  import graph._
 
-  override def andNode(an: AndNode, subs: Option[Seq[Cost]]) = {
+  // FIXME: Implement this in repair strategy
+  /*override def andNode(an: AndNode, subs: Option[Seq[Cost]]) = {
     val h = cm.andNode(an, subs).minSize
 
     Cost(an.ri.rule match {
@@ -19,5 +19,5 @@ case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("
       case TEGLESS      => 1
       case _            => h+1
     })
-  }
+  }*/
 }

src/main/scala/leon/synthesis/CostModel.scala

@@ -3,16 +3,12 @@
 package leon
 package synthesis
 
-import graph._
-
 import purescala.Expressions._
 import purescala.ExprOps._
 
 /** A named way of computing the cost of problem and solutions.*/
 abstract class CostModel(val name: String) {
   def solution(s: Solution): Cost
-  def problem(p: Problem): Cost
-  def andNode(an: AndNode, subs: Option[Seq[Cost]]): Cost
 
   def impossible: Cost
 
@@ -34,7 +30,7 @@ case class Cost(minSize: Int) extends AnyVal with Ordered[Cost] {
 
 /** Contains all and the default [CostModel] */
 object CostModels {
-  def default: CostModel = WeightedBranchesCostModel
+  def default: CostModel = NaiveCostModel
 
   def all: Set[CostModel] = Set(
     NaiveCostModel,
@@ -47,10 +43,6 @@ class WrappedCostModel(cm: CostModel, name: String) extends CostModel(name) {
 
   def solution(s: Solution): Cost = cm.solution(s)
 
-  def problem(p: Problem): Cost = cm.problem(p)
-
-  def andNode(an: AndNode, subs: Option[Seq[Cost]]): Cost = cm.andNode(an, subs)
-
   def impossible = cm.impossible
 }
 
@@ -58,34 +50,10 @@ class WrappedCostModel(cm: CostModel, name: String) extends CostModel(name) {
   * For problems, returns a cost of 1 */
 class SizeBasedCostModel(name: String) extends CostModel(name) {
   def solution(s: Solution) = {
-    Cost(formulaSize(s.toExpr)/10)
-  }
-
-  def problem(p: Problem) = {
-    Cost(1)
-  }
-
-  def andNode(an: AndNode, subs: Option[Seq[Cost]]) = {
-
-    subs match {
-      case Some(subs) if subs.isEmpty =>
-        impossible
-
-      case osubs =>
-        val app = an.ri
-
-        val subSols = app.onSuccess.types.map {t => Solution.simplest(t) }.toList
-        val selfCost = app.onSuccess(subSols) match {
-          case Some(sol) =>
-            solution(sol).minSize - subSols.size
-          case None =>
-            1
-        }
-        Cost(osubs.toList.flatten.foldLeft(selfCost)(_ + _.minSize))
-    }   
+    Cost(formulaSize(s.term))
   }
 
-  def impossible = Cost(200)
+  def impossible = Cost(1000)
 }
 
 case object NaiveCostModel extends SizeBasedCostModel("Naive")

src/main/scala/leon/synthesis/SynthesisPhase.scala

@@ -53,8 +53,7 @@ object SynthesisPhase extends TransformationPhase {
       timeoutMs = timeout map { _ * 1000 },
       generateDerivationTrees = ctx.findOptionOrDefault(optDerivTrees),
       costModel = costModel,
-      rules = Rules.all(ctx.findOptionOrDefault(optCEGISNaiveGrammar)) ++
-        (if(ms.isDefined) Seq(rules.AsChoose, rules.SygusCVC4) else Seq()),
+      rules = Rules.all(ctx.findOptionOrDefault(optCEGISNaiveGrammar)),
       manualSearch = ms,
       functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
       cegisUseOptTimeout = ctx.findOptionOrDefault(optCEGISOptTimeout),

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

@@ -31,8 +31,8 @@ case object InputSplit extends Rule("In. Split") {
 
       val onSuccess: List[Solution] => Option[Solution] = {
         case List(s1, s2) =>
-          Some(Solution(or(and(Equals(Variable(a), BooleanLiteral(true)), s1.pre),
-                           and(Equals(Variable(a), BooleanLiteral(false)), s2.pre)),
+          Some(Solution(or(and(    Variable(a) , s1.pre),
+                           and(Not(Variable(a)), s2.pre)),
                         s1.defs ++ s2.defs,
                         IfExpr(Variable(a), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
         case _ =>