diff --git a/project/plugins.sbt b/project/plugins.sbt
index fe91723924812684dbbbe5c04a401a120b339a0d..9a94578c3c5cb3741993e490723649b67eb71441 100644
--- a/project/plugins.sbt
+++ b/project/plugins.sbt
@@ -1,3 +1 @@
addSbtPlugin("com.typesafe.sbt" % "sbt-site" % "0.8.1")
-
-addSbtPlugin("info.hupel" % "sbt-libisabelle" % "0.1")
diff --git a/src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala b/src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala
index c82db1cdda97b74a1b134c529a4f06a7ab5787ae..ee9a9f7492568a3924302757c643ca8e00692695 100644
--- a/src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala
+++ b/src/main/scala/inox/solvers/combinators/SolverPoolFactory.scala
@@ -19,9 +19,11 @@ import scala.reflect.runtime.universe._
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
val poolMaxSize = 5
@@ -32,7 +34,7 @@ trait SolverPoolFactory extends SolverFactory { self =>
def getNewSolver(): S = {
if (availables.isEmpty) {
poolSize += 1
- availables += sf.getNewSolver()
+ availables += factory.getNewSolver()
}
val s = availables.dequeue()
@@ -50,14 +52,14 @@ trait SolverPoolFactory extends SolverFactory { self =>
case _: CantResetException =>
inUse -= s
s.free()
- sf.reclaim(s)
- availables += sf.getNewSolver()
+ factory.reclaim(s)
+ availables += factory.getNewSolver()
}
}
def init(): Unit = {
for (i <- 1 to poolMaxSize) {
- availables += sf.getNewSolver()
+ availables += factory.getNewSolver()
}
poolSize = poolMaxSize
@@ -65,7 +67,7 @@ trait SolverPoolFactory extends SolverFactory { self =>
override def shutdown(): Unit = {
for (s <- availables ++ inUse) {
- sf.reclaim(s)
+ factory.reclaim(s)
}
availables.clear()
@@ -75,3 +77,11 @@ trait SolverPoolFactory extends SolverFactory { self =>
init()
}
+
+object SolverPoolFactory {
+ def apply(sf: SolverFactory): SolverPoolFactory {
+ val factory: sf.type
+ } = new {
+ val factory: sf.type = sf
+ } with SolverPoolFactory
+}
diff --git a/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala b/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
index 390f0d33062c2ad57b0117a91bbfd98f506afc0b..518e6aa2e92ba7778eca3f30012f5b39fdc18277 100644
--- a/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
+++ b/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
@@ -35,7 +35,7 @@ class SolverPoolSuite extends InoxTestSuite {
test(s"SolverPool has at least $poolSize solvers") { implicit ctx =>
- val sp = new SolverPoolFactory(ctx, sfactory)
+ val sp = SolverPoolFactory(sfactory)
var solvers = Set[Solver]()
@@ -48,7 +48,7 @@ class SolverPoolSuite extends InoxTestSuite {
test("SolverPool reuses solvers") { implicit ctx =>
- val sp = new SolverPoolFactory(ctx, sfactory)
+ val sp = SolverPoolFactory(sfactory)
var solvers = Set[Solver]()
@@ -67,7 +67,7 @@ class SolverPoolSuite extends InoxTestSuite {
test(s"SolverPool can grow") { implicit ctx =>
- val sp = new SolverPoolFactory(ctx, sfactory)
+ val sp = SolverPoolFactory(sfactory)
var solvers = Set[Solver]()
diff --git a/src/test/scala/inox/unit/trees/ExtractorsSuite.scala b/src/test/scala/inox/unit/trees/ExtractorsSuite.scala
index 7873045207d50a0403df287729264dbe4446b110..89bbe833d4fe3a50015874f35f0ca43568599c4a 100644
--- a/src/test/scala/inox/unit/trees/ExtractorsSuite.scala
+++ b/src/test/scala/inox/unit/trees/ExtractorsSuite.scala
@@ -1,24 +1,20 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon.unit.purescala
+package inox.unit.trees
import org.scalatest._
-import leon.test.helpers.ExpressionsDSL
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Extractors._
-
-class ExtractorsSuite extends FunSuite with ExpressionsDSL {
+class ExtractorsSuite extends FunSuite {
+ import inox.trees._
test("Extractors do not simplify basic arithmetic") {
- val e1 = BVPlus(1, 1)
+ val e1 = Plus(IntLiteral(1), IntLiteral(1))
val e2 = e1 match {
case Operator(es, builder) => builder(es)
}
assert(e1 === e2)
- val e3 = Times(x, BigInt(1))
+ val e3 = Times(Variable(FreshIdentifier("x"), IntegerType), IntegerLiteral(1))
val e4 = e3 match {
case Operator(es, builder) => builder(es)
}
@@ -26,7 +22,7 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
}
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 {
case Operator(es, builder) => builder(es)
}
@@ -38,7 +34,7 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
}
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 {
case Operator(es, builder) => builder(es)
}
@@ -46,24 +42,31 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
}
- test("Extractors of NonemptyArray with sparse elements") {
- val a1 = NonemptyArray(Map(0 -> x, 3 -> y, 5 -> z), Some((BigInt(0), BigInt(10))))
+ test("Extractors of map operations") {
+ 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 {
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)
}
}
assert(a2 === a1)
- val a3 = NonemptyArray(Map(0 -> x, 1 -> y, 2 -> z), None)
- val a4 = a3 match {
+ val app1 = MapApply(a1, IntLiteral(0))
+ val app2 = app1 match {
case Operator(es, builder) => {
- assert(es === Seq(x, y, z))
+ assert(es === Seq(a1, IntLiteral(0)))
builder(es)
}
}
- assert(a3 === a4)
+ assert(app1 === app2)
}
}