From fbc59990c6bb07c0472112e4563dc59d1cb0c90c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 6 Aug 2015 15:05:54 +0200
Subject: [PATCH] Add unit-test for solver pools
---
.../leon/test/solvers/SolverPoolSuite.scala | 76 +++++++++++++++++++
1 file changed, 76 insertions(+)
create mode 100644 src/test/scala/leon/test/solvers/SolverPoolSuite.scala
diff --git a/src/test/scala/leon/test/solvers/SolverPoolSuite.scala b/src/test/scala/leon/test/solvers/SolverPoolSuite.scala
new file mode 100644
index 000000000..04d4d7723
--- /dev/null
+++ b/src/test/scala/leon/test/solvers/SolverPoolSuite.scala
@@ -0,0 +1,76 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.solvers
+
+import leon._
+import leon.test._
+import leon.solvers._
+import leon.solvers.combinators._
+
+import leon.purescala.Definitions._
+import leon.purescala.Expressions._
+
+class SolverPoolSuite extends LeonTestSuite {
+
+ private class DummySolver(val context : LeonContext, val program: Program) extends Solver {
+ val name = "Dummy"
+ val description = "dummy"
+
+ def check: Option[Boolean] = None
+ def assertCnstr(e: Expr) = {}
+ def free() {}
+ def reset() {}
+ def getModel = ???
+ }
+
+ def sfactory(implicit ctx: LeonContext): SolverFactory[Solver] = {
+ SolverFactory(() => new DummySolver(ctx, Program.empty))
+ }
+
+ val poolSize = 5;
+
+ test(s"SolverPool has at least $poolSize solvers") { implicit ctx =>
+
+ val sp = new SolverPoolFactory(ctx, sfactory)
+
+ var solvers = Set[Solver]()
+
+ for (i <- 1 to poolSize) {
+ solvers += sp.getNewSolver()
+ }
+
+ solvers.size === poolSize
+ }
+
+ test("SolverPool reuses solvers") { implicit ctx =>
+
+ val sp = new SolverPoolFactory(ctx, sfactory)
+
+ var solvers = Set[Solver]()
+
+ for (i <- 1 to poolSize) {
+ val s = sp.getNewSolver()
+ solvers += s
+ sp.reclaim(s)
+ }
+
+ for (i <- 1 to poolSize) {
+ val s = sp.getNewSolver()
+ assert(solvers contains s, "Solver not reused?")
+ sp.reclaim(s)
+ }
+ }
+
+ test(s"SolverPool can grow") { implicit ctx =>
+
+ val sp = new SolverPoolFactory(ctx, sfactory)
+
+ var solvers = Set[Solver]()
+
+ for (i <- 1 to poolSize+3) {
+ solvers += sp.getNewSolver()
+ }
+
+ solvers.size === poolSize+3
+ }
+}
--
GitLab