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

Moved extractorSuite test

parent b29c5b71
No related branches found
No related tags found
No related merge requests found
...@@ -71,62 +71,3 @@ class ExtractorsSuite extends FunSuite { ...@@ -71,62 +71,3 @@ class ExtractorsSuite extends FunSuite {
} }
} }
//class ExtractorsSuite extends FunSuite with ExpressionsDSL {
//
// test("Extractors do not simplify basic arithmetic") {
// val e1 = BVPlus(1, 1)
// val e2 = e1 match {
// case Operator(es, builder) => builder(es)
// }
// assert(e1 === e2)
//
// val e3 = Times(x, BigInt(1))
// val e4 = e3 match {
// case Operator(es, builder) => builder(es)
// }
// assert(e3 === e4)
// }
//
// test("Extractors do not magically change the syntax") {
// val e1 = Equals(bi(1), bi(1))
// val e2 = e1 match {
// case Operator(es, builder) => builder(es)
// }
// assert(e1 === e2)
//
// val e3 = Equals(BooleanLiteral(true), BooleanLiteral(false))
// val e4 = e3 match {
// case Operator(es, builder) => builder(es)
// }
// assert(e3 === e4)
//
// val e5 = TupleSelect(Tuple(Seq(bi(1), bi(2))), 2)
// val e6 = e5 match {
// case Operator(es, builder) => builder(es)
// }
// assert(e5 === e6)
// }
//
//
// test("Extractors of NonemptyArray with sparse elements") {
// val a1 = NonemptyArray(Map(0 -> x, 3 -> y, 5 -> z), Some((BigInt(0), BigInt(10))))
// val a2 = a1 match {
// case Operator(es, builder) => {
// assert(es === Seq(x, y, z, InfiniteIntegerLiteral(0), InfiniteIntegerLiteral(10)))
// builder(es)
// }
// }
// assert(a2 === a1)
//
// val a3 = NonemptyArray(Map(0 -> x, 1 -> y, 2 -> z), None)
// val a4 = a3 match {
// case Operator(es, builder) => {
// assert(es === Seq(x, y, z))
// builder(es)
// }
// }
// assert(a3 === a4)
// }
//
//}
/* Copyright 2009-2016 EPFL, Lausanne */
package inox.unit.trees
import org.scalatest._
class ExtractorsSuite extends FunSuite {
import inox.trees._
test("Extractors do not simplify basic arithmetic") {
val e1 = Plus(IntLiteral(1), IntLiteral(1))
val e2 = e1 match {
case Operator(es, builder) => builder(es)
}
assert(e1 === e2)
val e3 = Times(Variable(FreshIdentifier("x"), IntegerType), IntegerLiteral(1))
val e4 = e3 match {
case Operator(es, builder) => builder(es)
}
assert(e3 === e4)
}
test("Extractors do not magically change the syntax") {
val e1 = Equals(IntegerLiteral(1), IntegerLiteral(1))
val e2 = e1 match {
case Operator(es, builder) => builder(es)
}
assert(e1 === e2)
val e3 = Equals(BooleanLiteral(true), BooleanLiteral(false))
val e4 = e3 match {
case Operator(es, builder) => builder(es)
}
assert(e3 === e4)
val e5 = TupleSelect(Tuple(Seq(IntegerLiteral(1), IntegerLiteral(2))), 2)
val e6 = e5 match {
case Operator(es, builder) => builder(es)
}
assert(e5 === e6)
}
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(IntLiteral(0), x, IntLiteral(3), y, IntLiteral(5), z, IntegerLiteral(10)))
builder(es)
}
}
assert(a2 === a1)
val app1 = MapApply(a1, IntLiteral(0))
val app2 = app1 match {
case Operator(es, builder) => {
assert(es === Seq(a1, IntLiteral(0)))
builder(es)
}
}
assert(app1 === app2)
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment