Fix tests with new rules API

src/test/scala/leon/benchmark/SynthesisBenchmarks.scala

@@ -60,19 +60,19 @@ object SynthesisBenchmarks extends App {
 
     val (results, solver) = pipeline.run(ctx)(file.getPath :: Nil)
 
-    val sctx = SynthesisContext(solver, new SilentReporter)
+    val sctx = SynthesisContext(solver, new SilentReporter, new java.util.concurrent.atomic.AtomicBoolean)
 
 
     for ((f, ps) <- results; p <- ps) {
       val ts = System.currentTimeMillis
 
-      val rr = rules.CEGIS.attemptToApplyOn(sctx, p)
+      val rr = rules.CEGIS.instantiateOn(sctx, p)
       
-      val nAlt = rr.alternatives.size
+      val nAlt = rr.size
       var nSuccess, nInnap, nDecomp = 0
 
-      for (alt <- rr.alternatives) {
-        alt.apply() match {
+      for (alt <- rr) {
+        alt.apply(sctx) match {
           case RuleApplicationImpossible =>
             nInnap += 1
           case s: RuleDecomposed =>

src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala

@@ -104,22 +104,17 @@ class SynthesisSuite extends FunSuite {
     }
   }
 
-  def synthesisStep(s: Solver, r: Rule, p: Problem): RuleResult = {
-    val sctx = SynthesisContext(s, new SilentReporter)
-    r.attemptToApplyOn(sctx, p)
-  }
-
-  def assertRuleSuccess(rr: RuleResult) {
-    assert(rr.alternatives.isEmpty === false, "No rule alternative while the rule should have succeeded")
-    assert(rr.alternatives.exists(alt => alt.apply().isInstanceOf[RuleSuccess]) === true, "Rule did not succeed")
+  def assertRuleSuccess(sctx: SynthesisContext, rr: Traversable[RuleInstantiation]) {
+    assert(rr.isEmpty === false, "No rule alternative while the rule should have succeeded")
+    assert(rr.exists(alt => alt.apply(sctx).isInstanceOf[RuleSuccess]) === true, "Rule did not succeed")
   }
 
 
-  def assertFastEnough(rr: RuleResult, timeoutMs: Long) {
-    for (alt <- rr.alternatives) {
+  def assertFastEnough(sctx: SynthesisContext, rr: Traversable[RuleInstantiation], timeoutMs: Long) {
+    for (alt <- rr) {
       val ts = System.currentTimeMillis
 
-      val res = alt.apply()
+      val res = alt.apply(sctx)
 
       val t = System.currentTimeMillis - ts
 
@@ -130,7 +125,9 @@ class SynthesisSuite extends FunSuite {
 
   testFile("synthesis/Cegis1.scala") {
     case (solver, fd, p) => 
-      assertRuleSuccess(synthesisStep(solver, rules.CEGIS, p))
-      assertFastEnough(synthesisStep(solver, rules.CEGIS, p), 100)
+      val sctx = SynthesisContext(solver, new SilentReporter, new java.util.concurrent.atomic.AtomicBoolean)
+
+      assertRuleSuccess(sctx, rules.CEGIS.instantiateOn(sctx, p))
+      assertFastEnough(sctx, rules.CEGIS.instantiateOn(sctx, p), 100)
   }
 }