Skip to content
Snippets Groups Projects
Commit 882c3d70 authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

Fixed solverPool and Extractors unit tests

parent d462d349
Branches
Tags
No related merge requests found
addSbtPlugin("com.typesafe.sbt" % "sbt-site" % "0.8.1") addSbtPlugin("com.typesafe.sbt" % "sbt-site" % "0.8.1")
addSbtPlugin("info.hupel" % "sbt-libisabelle" % "0.1")
...@@ -19,9 +19,11 @@ import scala.reflect.runtime.universe._ ...@@ -19,9 +19,11 @@ import scala.reflect.runtime.universe._
trait SolverPoolFactory extends SolverFactory { self => trait SolverPoolFactory extends SolverFactory { self =>
val sf: SolverFactory { val program: self.program.type; type S = self.S } val factory: SolverFactory
val program: factory.program.type = factory.program
type S = factory.S
val name = "Pool(" + sf.name + ")" val name = "Pool(" + factory.name + ")"
var poolSize = 0 var poolSize = 0
val poolMaxSize = 5 val poolMaxSize = 5
...@@ -32,7 +34,7 @@ trait SolverPoolFactory extends SolverFactory { self => ...@@ -32,7 +34,7 @@ trait SolverPoolFactory extends SolverFactory { self =>
def getNewSolver(): S = { def getNewSolver(): S = {
if (availables.isEmpty) { if (availables.isEmpty) {
poolSize += 1 poolSize += 1
availables += sf.getNewSolver() availables += factory.getNewSolver()
} }
val s = availables.dequeue() val s = availables.dequeue()
...@@ -50,14 +52,14 @@ trait SolverPoolFactory extends SolverFactory { self => ...@@ -50,14 +52,14 @@ trait SolverPoolFactory extends SolverFactory { self =>
case _: CantResetException => case _: CantResetException =>
inUse -= s inUse -= s
s.free() s.free()
sf.reclaim(s) factory.reclaim(s)
availables += sf.getNewSolver() availables += factory.getNewSolver()
} }
} }
def init(): Unit = { def init(): Unit = {
for (i <- 1 to poolMaxSize) { for (i <- 1 to poolMaxSize) {
availables += sf.getNewSolver() availables += factory.getNewSolver()
} }
poolSize = poolMaxSize poolSize = poolMaxSize
...@@ -65,7 +67,7 @@ trait SolverPoolFactory extends SolverFactory { self => ...@@ -65,7 +67,7 @@ trait SolverPoolFactory extends SolverFactory { self =>
override def shutdown(): Unit = { override def shutdown(): Unit = {
for (s <- availables ++ inUse) { for (s <- availables ++ inUse) {
sf.reclaim(s) factory.reclaim(s)
} }
availables.clear() availables.clear()
...@@ -75,3 +77,11 @@ trait SolverPoolFactory extends SolverFactory { self => ...@@ -75,3 +77,11 @@ trait SolverPoolFactory extends SolverFactory { self =>
init() init()
} }
object SolverPoolFactory {
def apply(sf: SolverFactory): SolverPoolFactory {
val factory: sf.type
} = new {
val factory: sf.type = sf
} with SolverPoolFactory
}
...@@ -35,7 +35,7 @@ class SolverPoolSuite extends InoxTestSuite { ...@@ -35,7 +35,7 @@ class SolverPoolSuite extends InoxTestSuite {
test(s"SolverPool has at least $poolSize solvers") { implicit ctx => test(s"SolverPool has at least $poolSize solvers") { implicit ctx =>
val sp = new SolverPoolFactory(ctx, sfactory) val sp = SolverPoolFactory(sfactory)
var solvers = Set[Solver]() var solvers = Set[Solver]()
...@@ -48,7 +48,7 @@ class SolverPoolSuite extends InoxTestSuite { ...@@ -48,7 +48,7 @@ class SolverPoolSuite extends InoxTestSuite {
test("SolverPool reuses solvers") { implicit ctx => test("SolverPool reuses solvers") { implicit ctx =>
val sp = new SolverPoolFactory(ctx, sfactory) val sp = SolverPoolFactory(sfactory)
var solvers = Set[Solver]() var solvers = Set[Solver]()
...@@ -67,7 +67,7 @@ class SolverPoolSuite extends InoxTestSuite { ...@@ -67,7 +67,7 @@ class SolverPoolSuite extends InoxTestSuite {
test(s"SolverPool can grow") { implicit ctx => test(s"SolverPool can grow") { implicit ctx =>
val sp = new SolverPoolFactory(ctx, sfactory) val sp = SolverPoolFactory(sfactory)
var solvers = Set[Solver]() var solvers = Set[Solver]()
......
/* Copyright 2009-2016 EPFL, Lausanne */ /* Copyright 2009-2016 EPFL, Lausanne */
package leon.unit.purescala package inox.unit.trees
import org.scalatest._ import org.scalatest._
import leon.test.helpers.ExpressionsDSL class ExtractorsSuite extends FunSuite {
import leon.purescala.Common._ import inox.trees._
import leon.purescala.Expressions._
import leon.purescala.Extractors._
class ExtractorsSuite extends FunSuite with ExpressionsDSL {
test("Extractors do not simplify basic arithmetic") { test("Extractors do not simplify basic arithmetic") {
val e1 = BVPlus(1, 1) val e1 = Plus(IntLiteral(1), IntLiteral(1))
val e2 = e1 match { val e2 = e1 match {
case Operator(es, builder) => builder(es) case Operator(es, builder) => builder(es)
} }
assert(e1 === e2) assert(e1 === e2)
val e3 = Times(x, BigInt(1)) val e3 = Times(Variable(FreshIdentifier("x"), IntegerType), IntegerLiteral(1))
val e4 = e3 match { val e4 = e3 match {
case Operator(es, builder) => builder(es) case Operator(es, builder) => builder(es)
} }
...@@ -26,7 +22,7 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL { ...@@ -26,7 +22,7 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
} }
test("Extractors do not magically change the syntax") { test("Extractors do not magically change the syntax") {
val e1 = Equals(bi(1), bi(1)) val e1 = Equals(IntegerLiteral(1), IntegerLiteral(1))
val e2 = e1 match { val e2 = e1 match {
case Operator(es, builder) => builder(es) case Operator(es, builder) => builder(es)
} }
...@@ -38,7 +34,7 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL { ...@@ -38,7 +34,7 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
} }
assert(e3 === e4) assert(e3 === e4)
val e5 = TupleSelect(Tuple(Seq(bi(1), bi(2))), 2) val e5 = TupleSelect(Tuple(Seq(IntegerLiteral(1), IntegerLiteral(2))), 2)
val e6 = e5 match { val e6 = e5 match {
case Operator(es, builder) => builder(es) case Operator(es, builder) => builder(es)
} }
...@@ -46,24 +42,31 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL { ...@@ -46,24 +42,31 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
} }
test("Extractors of NonemptyArray with sparse elements") { test("Extractors of map operations") {
val a1 = NonemptyArray(Map(0 -> x, 3 -> y, 5 -> z), Some((BigInt(0), BigInt(10)))) val x = Variable(FreshIdentifier("x"), IntegerType)
val y = Variable(FreshIdentifier("y"), IntegerType)
val z = Variable(FreshIdentifier("z"), IntegerType)
val a1 = FiniteMap(
Seq(IntLiteral(0) -> x, IntLiteral(3) -> y, IntLiteral(5) -> z),
IntegerLiteral(10),
Int32Type)
val a2 = a1 match { val a2 = a1 match {
case Operator(es, builder) => { case Operator(es, builder) => {
assert(es === Seq(x, y, z, InfiniteIntegerLiteral(0), InfiniteIntegerLiteral(10))) assert(es === Seq(IntLiteral(0), x, IntLiteral(3), y, IntLiteral(5), z, IntegerLiteral(10)))
builder(es) builder(es)
} }
} }
assert(a2 === a1) assert(a2 === a1)
val a3 = NonemptyArray(Map(0 -> x, 1 -> y, 2 -> z), None) val app1 = MapApply(a1, IntLiteral(0))
val a4 = a3 match { val app2 = app1 match {
case Operator(es, builder) => { case Operator(es, builder) => {
assert(es === Seq(x, y, z)) assert(es === Seq(a1, IntLiteral(0)))
builder(es) builder(es)
} }
} }
assert(a3 === a4) assert(app1 === app2)
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment