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 0000000000000000000000000000000000000000..04d4d77237273cdd5c4bcdbf8e2e24dd0d523ace --- /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 + } +}