From 6005d61f7074db2db67c928eae8912849f3a4a67 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 6 Dec 2012 18:55:59 +0100
Subject: [PATCH] Fix tests with new rules API
---
.../leon/benchmark/SynthesisBenchmarks.scala | 10 ++++----
.../test/synthesis/RuleApplicationSuite.scala | 23 ++++++++-----------
2 files changed, 15 insertions(+), 18 deletions(-)
diff --git a/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala b/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala
index 84bf363cd..f5f48403a 100644
--- a/src/test/scala/leon/benchmark/SynthesisBenchmarks.scala
+++ b/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 =>
diff --git a/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala b/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
index 91ea7f8d3..96a5e53a9 100644
--- a/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
+++ b/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)
}
}
--
GitLab