Rework the semantics of rules, their applications/instantiation, results

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

@@ -10,11 +10,11 @@ abstract class CostModel(val name: String) {
   def solutionCost(s: Solution): Cost
   def problemCost(p: Problem): Cost
 
-  def ruleAppCost(r: Rule, app: RuleApplication): Cost = new Cost {
-    val subSols = (1 to app.subProblemsCount).map {i => Solution.simplest }.toList
+  def ruleAppCost(r: Rule, app: RuleInstantiation): Cost = new Cost {
+    val subSols = (1 to app.onSuccess.arity).map {i => Solution.simplest }.toList
     val simpleSol = app.onSuccess(subSols)
 
-    val value = solutionCost(simpleSol).value
+    val value = simpleSol.map(solutionCost(_).value).getOrElse(0)
   }
 }
 

src/main/scala/leon/synthesis/Heuristics.scala

@@ -21,34 +21,31 @@ trait Heuristic {
 
 }
 
-object HeuristicStep {
-  def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Solution = {
-    //sctx here is unsafe to use in parallel. onSuccess should take a sctx for
-    //this to be possible
-
+object HeuristicInstantiation {
+  def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Option[Solution] = {
     //sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
     //  case (Some(true), model) =>
     //    sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
     //    sctx.reporter.warning(" - problem: "+problem)
     //    sctx.reporter.warning(" - precondition: "+s.pre)
-    //    s
+    //    None
     //  case _ =>
-    //    s
+    //    Some(s)
     //}
-    s
+
+    Some(s)
   }
 
-  def apply(sctx: SynthesisContext, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
-    new RuleApplication(subProblems.size, onSuccess.andThen(verifyPre(sctx, problem))) {
-      def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems, onSuccess)
+  def apply(problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+    val builder = new SolutionBuilder(subProblems.size) {
+      def apply(sols: List[Solution]) = {
+        Some(onSuccess(sols))
+      }
     }
-  }
-}
 
+    new RuleInstantiation(builder) {
+      def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems)
 
-object HeuristicFastStep {
-  def apply(sctx: SynthesisContext, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
-    RuleResult(List(HeuristicStep(sctx, problem, subProblems, onSuccess)))
+    }
   }
 }
-

src/main/scala/leon/synthesis/ParallelSearch.scala

@@ -34,7 +34,7 @@ class ParallelSearch(synth: Synthesizer,
         }
 
         ExpandSuccess(sol)
-      case RuleDecomposed(sub, onSuccess) =>
+      case RuleDecomposed(sub) =>
         synth.synchronized {
           info(prefix+"Got: "+t.problem)
           info(prefix+"Decomposed into:")
@@ -52,7 +52,7 @@ class ParallelSearch(synth: Synthesizer,
 
   def expandOrTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskTryRules) = {
     val sub = rules.flatMap { r => 
-      r.attemptToApplyOn(sctx, t.p).alternatives.map(TaskRunRule(t.p, r, _))
+      r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _))
     }
 
     if (!sub.isEmpty) {

src/main/scala/leon/synthesis/Rules.scala

@@ -27,54 +27,56 @@ object Rules {
   )
 }
 
-case class RuleResult(alternatives: Traversable[RuleApplication])
-object RuleInapplicable extends RuleResult(List())
+abstract class SolutionBuilder(val arity: Int) {
+  def apply(sols: List[Solution]): Option[Solution]
+}
 
-abstract class RuleApplication(val subProblemsCount: Int,
-                               val onSuccess: List[Solution] => Solution) {
+class SolutionCombiner(arity: Int, f: List[Solution] => Solution) extends SolutionBuilder(arity) {
+  def apply(sols: List[Solution]) = {
+    assert(sols.size == arity)
+    Some(f(sols))
+  }
+}
 
+object SolutionBuilder {
+  val none = new SolutionBuilder(0) {
+    def apply(sols: List[Solution]) = None
+  }
+}
+
+abstract class RuleInstantiation(val onSuccess: SolutionBuilder) {
   def apply(sctx: SynthesisContext): RuleApplicationResult
 }
 
-abstract class RuleImmediateApplication extends RuleApplication(0, s => Solution.simplest)
+//abstract class RuleApplication(val subProblemsCount: Int,
+//                               val onSuccess: List[Solution] => Solution) {
+//
+//  def apply(sctx: SynthesisContext): RuleApplicationResult
+//}
+//
+//abstract class RuleImmediateApplication extends RuleApplication(0, s => Solution.simplest)
 
 sealed abstract class RuleApplicationResult
-case class RuleSuccess(solution: Solution) extends RuleApplicationResult
-case class RuleDecomposed(sub: List[Problem], onSuccess: List[Solution] => Solution) extends RuleApplicationResult
-case object RuleApplicationImpossible extends RuleApplicationResult
+case class RuleSuccess(solution: Solution)    extends RuleApplicationResult
+case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
+case object RuleApplicationImpossible         extends RuleApplicationResult
 
-object RuleFastApplication {
-  def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
-    new RuleApplication(sub.size, onSuccess) {
-      def apply(sctx: SynthesisContext) = RuleDecomposed(sub, onSuccess)
+object RuleInstantiation {
+  def immediateDecomp(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
+    new RuleInstantiation(new SolutionCombiner(sub.size, onSuccess)) {
+      def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
     }
   }
-}
-
-object RuleFastInapplicable {
-  def apply() = {
-    RuleResult(List(new RuleApplication(0, ls => Solution.simplest) {
-      def apply(sctx: SynthesisContext) = RuleApplicationImpossible
-    }))
-  }
-}
 
-object RuleFastStep {
-  def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
-    RuleResult(List(RuleFastApplication(sub, onSuccess)))
-  }
-}
-
-object RuleFastSuccess {
-  def apply(solution: Solution) = {
-    RuleResult(List(new RuleApplication(0, ls => solution) {
+  def immediateSuccess(solution: Solution) = {
+    new RuleInstantiation(new SolutionCombiner(0, ls => solution)) {
       def apply(sctx: SynthesisContext) = RuleSuccess(solution)
-    }))
+    }
   }
 }
 
 abstract class Rule(val name: String, val priority: Priority) {
-  def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult
+  def instantiateOn(scrx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation]
 
   def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
   def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)

src/main/scala/leon/synthesis/SimpleSearch.scala

@@ -3,8 +3,8 @@ package synthesis
 
 import synthesis.search._
 
-case class TaskRunRule(problem: Problem, rule: Rule, app: RuleApplication) extends AOAndTask[Solution] {
-  def composeSolution(sols: List[Solution]): Solution = {
+case class TaskRunRule(problem: Problem, rule: Rule, app: RuleInstantiation) extends AOAndTask[Solution] {
+  def composeSolution(sols: List[Solution]): Option[Solution] = {
     app.onSuccess(sols)
   }
 
@@ -44,7 +44,7 @@ class SimpleSearch(synth: Synthesizer,
         info(prefix+"Solved with: "+sol)
 
         ExpandSuccess(sol)
-      case RuleDecomposed(sub, onSuccess) =>
+      case RuleDecomposed(sub) =>
         info(prefix+"Got: "+t.problem)
         info(prefix+"Decomposed into:")
         for(p <- sub) {
@@ -59,7 +59,7 @@ class SimpleSearch(synth: Synthesizer,
   }
 
   def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
-    val sub = rules.flatMap ( r => r.attemptToApplyOn(sctx, t.p).alternatives.map(TaskRunRule(t.p, r, _)) )
+    val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _)) )
 
     if (!sub.isEmpty) {
       Expanded(sub.toList)

src/main/scala/leon/synthesis/heuristics/ADTInduction.scala

@@ -10,7 +10,7 @@ import purescala.TypeTrees._
 import purescala.Definitions._
 
 case object ADTInduction extends Rule("ADT Induction", 80) with Heuristic {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val candidates = p.as.collect {
         case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
     }
@@ -97,12 +97,12 @@ case object ADTInduction extends Rule("ADT Induction", 80) with Heuristic {
             Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, p.as.map(Variable(_))))
         }
 
-        Some(HeuristicStep(sctx, p, subProblemsInfo.map(_._1).toList, onSuccess))
+        Some(HeuristicInstantiation(p, subProblemsInfo.map(_._1).toList, onSuccess))
       } else {
         None
       }
     }
 
-    RuleResult(steps.flatten)
+    steps.flatten
   }
 }

src/main/scala/leon/synthesis/heuristics/IntInduction.scala

@@ -10,7 +10,7 @@ import purescala.TypeTrees._
 import purescala.Definitions._
 
 case object IntInduction extends Rule("Int Induction", 50) with Heuristic {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.as match {
       case List(IsTyped(origId, Int32Type)) =>
         val tpe = TupleType(p.xs.map(_.getType))
@@ -54,9 +54,9 @@ case object IntInduction extends Rule("Int Induction", 50) with Heuristic {
             Solution.none
         }
 
-        HeuristicFastStep(sctx, p, List(subBase, subGT, subLT), onSuccess)
+        Some(HeuristicInstantiation(p, List(subBase, subGT, subLT), onSuccess))
       case _ =>
-        RuleInapplicable
+        None
     }
   }
 }

src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala

@@ -10,7 +10,7 @@ import purescala.TypeTrees._
 import purescala.Definitions._
 
 case object OptimisticInjection extends Rule("Opt. Injection", 50) with Heuristic {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = p.phi
 
     val eqfuncalls = exprs.collect{
@@ -36,9 +36,9 @@ case object OptimisticInjection extends Rule("Opt. Injection", 50) with Heuristi
 
       val sub = p.copy(phi = And(newExprs))
 
-      HeuristicFastStep(sctx, p, List(sub), forward)
+      Some(HeuristicInstantiation(p, List(sub), forward))
     } else {
-      RuleInapplicable
+      None
     }
   }
 }

src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala

@@ -10,7 +10,7 @@ import purescala.TypeTrees._
 import purescala.Definitions._
 
 case object SelectiveInlining extends Rule("Sel. Inlining", 20) with Heuristic {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = p.phi
 
     val eqfuncalls = exprs.collect{
@@ -36,9 +36,9 @@ case object SelectiveInlining extends Rule("Sel. Inlining", 20) with Heuristic {
 
       val sub = p.copy(phi = And(newExprs))
 
-      HeuristicFastStep(sctx, p, List(sub), forward)
+      Some(HeuristicInstantiation(p, List(sub), forward))
     } else {
-      RuleInapplicable
+      None
     }
   }
 }

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

@@ -7,7 +7,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 case object ADTDual extends Rule("ADTDual", 200) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val xs = p.xs.toSet
     val as = p.as.toSet
 
@@ -24,9 +24,9 @@ case object ADTDual extends Rule("ADTDual", 200) {
     if (!toRemove.isEmpty) {
       val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
 
-      RuleFastStep(List(sub), forward)
+      List(RuleInstantiation.immediateDecomp(List(sub), forward))
     } else {
-      RuleInapplicable
+      Nil
     }
   }
 }

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

@@ -10,7 +10,7 @@ import purescala.Extractors._
 import purescala.Definitions._
 
 case object ADTSplit extends Rule("ADT Split.", 70) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
     val candidates = p.as.collect {
       case IsTyped(id, AbstractClassType(cd)) =>
 
@@ -42,7 +42,7 @@ case object ADTSplit extends Rule("ADT Split.", 70) {
     }
 
 
-    val steps = candidates.collect{ _ match {
+    candidates.collect{ _ match {
       case Some((id, cases)) =>
         val oas = p.as.filter(_ != id)
 
@@ -70,11 +70,9 @@ case object ADTSplit extends Rule("ADT Split.", 70) {
             Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
         }
 
-        Some(RuleFastApplication(subInfo.map(_._2).toList, onSuccess))
+        Some(RuleInstantiation.immediateDecomp(subInfo.map(_._2).toList, onSuccess))
       case _ =>
         None
     }}.flatten
-
-    RuleResult(steps)
   }
 }

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

@@ -7,7 +7,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 case object Assert extends Rule("Assert", 200) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.phi match {
       case TopLevelAnds(exprs) =>
         val xsSet = p.xs.toSet
@@ -16,20 +16,20 @@ case object Assert extends Rule("Assert", 200) {
 
         if (!exprsA.isEmpty) {
           if (others.isEmpty) {
-            RuleFastSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
+            List(RuleInstantiation.immediateSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id)))))))
           } else {
             val sub = p.copy(pc = And(p.pc +: exprsA), phi = And(others))
 
-            RuleFastStep(List(sub), {
+            List(RuleInstantiation.immediateDecomp(List(sub), {
               case Solution(pre, defs, term) :: Nil => Solution(And(exprsA :+ pre), defs, term)
               case _ => Solution.none
-            })
+            }))
           }
         } else {
-          RuleInapplicable
+          Nil
         }
       case _ =>
-        RuleInapplicable
+        Nil
     }
   }
 }

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

@@ -7,7 +7,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 case object CaseSplit extends Rule("Case-Split", 200) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.phi match {
       case Or(o1 :: o2 :: _) =>
         val sub1 = Problem(p.as, p.pc, o1, p.xs)
@@ -18,9 +18,9 @@ case object CaseSplit extends Rule("Case-Split", 200) {
           case _ => Solution.none
         }
 
-        RuleFastStep(List(sub1, sub2), onSuccess)
+        List(RuleInstantiation.immediateDecomp(List(sub1, sub2), onSuccess))
       case _ =>
-        RuleInapplicable
+        Nil
     }
   }
 }

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

@@ -12,7 +12,7 @@ import purescala.Extractors._
 import solvers.z3.FairZ3Solver
 
 case object CEGIS extends Rule("CEGIS", 150) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
 
     var generators = Map[TypeTree, Generator]()
@@ -122,7 +122,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
 
     val (exprsA, others) = ands.partition(e => (variablesOf(e) & xsSet).isEmpty)
     if (exprsA.isEmpty) {
-      val res = new RuleImmediateApplication {
+      val res = new RuleInstantiation(SolutionBuilder.none) {
         def apply(sctx: SynthesisContext) = {
           var result: Option[RuleApplicationResult]   = None
 
@@ -272,12 +272,11 @@ case object CEGIS extends Rule("CEGIS", 150) {
               e.printStackTrace
               RuleApplicationImpossible
           }
-
         }
       }
-      RuleResult(List(res))
+      List(res)
     } else {
-      RuleInapplicable
+      Nil
     }
   }
 }

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

@@ -9,7 +9,7 @@ import purescala.Extractors._
 
 object Disunification {
   case object Decomp extends Rule("Disunif. Decomp.", 200) {
-    def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+    def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
       val TopLevelAnds(exprs) = p.phi
 
       val (toRemove, toAdd) = exprs.collect {
@@ -26,9 +26,9 @@ object Disunification {
       if (!toRemove.isEmpty) {
         val sub = p.copy(phi = Or((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
 
-        RuleFastStep(List(sub), forward)
+        List(RuleInstantiation.immediateDecomp(List(sub), forward))
       } else {
-        RuleInapplicable
+        Nil
       }
     }
   }

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

@@ -9,7 +9,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 case object EqualitySplit extends Rule("Eq. Split.", 90) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val candidates = p.as.groupBy(_.getType).map(_._2.toList).filter {
       case List(a1, a2) =>
         val toValEQ = Implies(p.pc, Equals(Variable(a1), Variable(a2)))
@@ -35,7 +35,7 @@ case object EqualitySplit extends Rule("Eq. Split.", 90) {
     }
 
 
-    val steps = candidates.map(_ match {
+    candidates.map(_ match {
       case List(a1, a2) =>
 
         val sub1 = p.copy(pc = And(Equals(Variable(a1), Variable(a2)), p.pc))
@@ -48,11 +48,9 @@ case object EqualitySplit extends Rule("Eq. Split.", 90) {
             Solution.none
         }
 
-        Some(RuleFastApplication(List(sub1, sub2), onSuccess))
+        Some(RuleInstantiation.immediateDecomp(List(sub1, sub2), onSuccess))
       case _ =>
         None
     }).flatten
-
-    RuleResult(steps)
   }
 }

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

@@ -8,21 +8,23 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 case object Ground extends Rule("Ground", 500) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     if (p.as.isEmpty) {
 
       val tpe = TupleType(p.xs.map(_.getType))
 
       sctx.solver.solveSAT(p.phi) match {
         case (Some(true), model) =>
-          RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
+          val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
+          Some(RuleInstantiation.immediateSuccess(sol))
         case (Some(false), model) =>
-          RuleFastSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
+          val sol = Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))
+          Some(RuleInstantiation.immediateSuccess(sol))
         case _ =>
-          RuleInapplicable
+          None
       }
     } else {
-      RuleInapplicable
+      None
     }
   }
 }

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

@@ -12,7 +12,7 @@ import purescala.Definitions._
 import LinearEquations.elimVariable
 
 case object IntegerEquation extends Rule("Integer Equation", 600) {
-  def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult = if(!problem.xs.exists(_.getType == Int32Type)) RuleInapplicable else {
+  def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = if(!problem.xs.exists(_.getType == Int32Type)) Nil else {
 
     val TopLevelAnds(exprs) = problem.phi
 
@@ -41,7 +41,7 @@ case object IntegerEquation extends Rule("Integer Equation", 600) {
     allOthers = allOthers ++ candidates
 
     optionNormalizedEq match {
-      case None => RuleInapplicable
+      case None => Nil
       case Some(normalizedEq0) => {
 
         val eqas = problem.as.toSet.intersect(vars)
@@ -60,7 +60,7 @@ case object IntegerEquation extends Rule("Integer Equation", 600) {
             case _ => Solution.none
           }
 
-          RuleFastStep(List(newProblem), onSuccess)
+          List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
 
         } else {
           val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
@@ -103,10 +103,8 @@ case object IntegerEquation extends Rule("Integer Equation", 600) {
             case _ => Solution.none
           }
 
-          RuleFastStep(List(newProblem), onSuccess)
+          List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
         }
-
-
       }
     }
 

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

@@ -13,7 +13,7 @@ import LinearEquations.elimVariable
 import leon.synthesis.Algebra.lcm
 
 case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
-  def attemptToApplyOn(sctx: SynthesisContext, problem: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = problem.phi
 
     //assume that we only have inequalities
@@ -32,7 +32,9 @@ case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
     val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
     val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains(_))
 
-    if(candidateVars.isEmpty) RuleInapplicable else {
+    if (candidateVars.isEmpty) {
+      Nil
+    } else {
       val processedVar: Identifier = candidateVars.map(v => {
         val normalizedLhs: List[List[Expr]] = lhsSides.map(linearArithmeticForm(_, Array(v)).toList)
         if(normalizedLhs.isEmpty)
@@ -129,7 +131,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
         val constraints: List[Expr] = for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds) 
                                         yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc)))
         val pre = And(exprNotUsed ++ constraints)
-        RuleFastSuccess(Solution(pre, Set(), witness))
+        List(RuleInstantiation.immediateSuccess(Solution(pre, Set(), witness)))
       } else {
 
         val involvedVariables = (upperBounds++lowerBounds).foldLeft(Set[Identifier]())((acc, t) => {
@@ -198,7 +200,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
           case _ => Solution.none
         }
 
-        RuleFastStep(List(subProblem), onSuccess)
+        List(RuleInstantiation.immediateDecomp(List(subProblem), onSuccess))
       }
     }
   }

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

@@ -7,7 +7,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 case object OnePoint extends Rule("One-point", 300) {
-  def attemptToApplyOn(sctx: SynthesisContext, p: Problem): RuleResult = {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = p.phi
 
     val candidates = exprs.collect {
@@ -35,9 +35,9 @@ case object OnePoint extends Rule("One-point", 300) {
         case _ => Solution.none
       }
 
-      RuleFastStep(List(newProblem), onSuccess)
+      List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
     } else {
-      RuleInapplicable
+      Nil
     }
   }
 }