diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index a17968b4196e692473cf41d269f80f3d18f31ab5..301d9fa3a9d354b089bd4259533fadc5a3d026bd 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -108,4 +108,118 @@ trait ExprOps extends GenTreeOps {
val Deconstructor(es, _) = e
es foreach rec
}
+
+ /** Simple, local optimization on string */
+ def simplifyString(expr: Expr): Expr = {
+ def simplify0(expr: Expr): Expr = (expr match {
+ case StringConcat(StringLiteral(""), b) => b
+ case StringConcat(b, StringLiteral("")) => b
+ case StringConcat(StringLiteral(a), StringLiteral(b)) => StringLiteral(a + b)
+ case StringLength(StringLiteral(a)) => IntLiteral(a.length)
+ case SubString(StringLiteral(a), IntLiteral(start), IntLiteral(end)) =>
+ StringLiteral(a.substring(start.toInt, end.toInt))
+ case _ => expr
+ }).copiedFrom(expr)
+
+ utils.fixpoint(simplePostTransform(simplify0))(expr)
+ }
+
+ /** Simple, local simplification on arithmetic
+ *
+ * You should not assume anything smarter than some constant folding and
+ * simple cancellation. To avoid infinite cycle we only apply simplification
+ * that reduce the size of the tree. The only guarantee from this function is
+ * to not augment the size of the expression and to be sound.
+ */
+ def simplifyArithmetic(expr: Expr): Expr = {
+ def simplify0(expr: Expr): Expr = (expr match {
+ case Plus(IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 + i2)
+ case Plus(IntegerLiteral(zero), e) if zero == BigInt(0) => e
+ case Plus(e, IntegerLiteral(zero)) if zero == BigInt(0) => e
+ case Plus(e1, UMinus(e2)) => Minus(e1, e2)
+ case Plus(Plus(e, IntegerLiteral(i1)), IntegerLiteral(i2)) => Plus(e, IntegerLiteral(i1+i2))
+ case Plus(Plus(IntegerLiteral(i1), e), IntegerLiteral(i2)) => Plus(IntegerLiteral(i1+i2), e)
+
+ case Minus(e, IntegerLiteral(zero)) if zero == BigInt(0) => e
+ case Minus(IntegerLiteral(zero), e) if zero == BigInt(0) => UMinus(e)
+ case Minus(IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 - i2)
+ case Minus(e1, UMinus(e2)) => Plus(e1, e2)
+ case Minus(e1, Minus(UMinus(e2), e3)) => Plus(e1, Plus(e2, e3))
+
+ case UMinus(IntegerLiteral(x)) => IntegerLiteral(-x)
+ case UMinus(UMinus(x)) => x
+ case UMinus(Plus(UMinus(e1), e2)) => Plus(e1, UMinus(e2))
+ case UMinus(Minus(e1, e2)) => Minus(e2, e1)
+
+ case Times(IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 * i2)
+ case Times(IntegerLiteral(one), e) if one == BigInt(1) => e
+ case Times(IntegerLiteral(mone), e) if mone == BigInt(-1) => UMinus(e)
+ case Times(e, IntegerLiteral(one)) if one == BigInt(1) => e
+ case Times(IntegerLiteral(zero), _) if zero == BigInt(0) => IntegerLiteral(0)
+ case Times(_, IntegerLiteral(zero)) if zero == BigInt(0) => IntegerLiteral(0)
+ case Times(IntegerLiteral(i1), Times(IntegerLiteral(i2), t)) => Times(IntegerLiteral(i1*i2), t)
+ case Times(IntegerLiteral(i1), Times(t, IntegerLiteral(i2))) => Times(IntegerLiteral(i1*i2), t)
+ case Times(IntegerLiteral(i), UMinus(e)) => Times(IntegerLiteral(-i), e)
+ case Times(UMinus(e), IntegerLiteral(i)) => Times(e, IntegerLiteral(-i))
+ case Times(IntegerLiteral(i1), Division(e, IntegerLiteral(i2))) if i2 != BigInt(0) && i1 % i2 == BigInt(0) =>
+ Times(IntegerLiteral(i1/i2), e)
+
+ case Division(IntegerLiteral(i1), IntegerLiteral(i2)) if i2 != BigInt(0) => IntegerLiteral(i1 / i2)
+ case Division(e, IntegerLiteral(one)) if one == BigInt(1) => e
+
+ //here we put more expensive rules
+ //btw, I know those are not the most general rules, but they lead to good optimizations :)
+ case Plus(UMinus(Plus(e1, e2)), e3) if e1 == e3 => UMinus(e2)
+ case Plus(UMinus(Plus(e1, e2)), e3) if e2 == e3 => UMinus(e1)
+ case Minus(e1, e2) if e1 == e2 => IntegerLiteral(0)
+ case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => IntegerLiteral(0)
+ case Minus(Plus(e1, e2), Plus(Plus(e3, e4), e5)) if e1 == e4 && e2 == e3 => UMinus(e5)
+
+ case StringConcat(StringLiteral(""), a) => a
+ case StringConcat(a, StringLiteral("")) => a
+ case StringConcat(StringLiteral(a), StringLiteral(b)) => StringLiteral(a+b)
+ case StringConcat(StringLiteral(a), StringConcat(StringLiteral(b), c)) => StringConcat(StringLiteral(a+b), c)
+ case StringConcat(StringConcat(c, StringLiteral(a)), StringLiteral(b)) => StringConcat(c, StringLiteral(a+b))
+ case StringConcat(a, StringConcat(b, c)) => StringConcat(StringConcat(a, b), c)
+ //default
+ case e => e
+ }).copiedFrom(expr)
+
+ utils.fixpoint(simplePostTransform(simplify0))(expr)
+ }
+
+ /**
+ * Some helper methods for FractionLiterals
+ */
+ def normalizeFraction(fl: FractionLiteral) = {
+ val FractionLiteral(num, denom) = fl
+ val modNum = if (num < 0) -num else num
+ val modDenom = if (denom < 0) -denom else denom
+ val divisor = modNum.gcd(modDenom)
+ val simpNum = num / divisor
+ val simpDenom = denom / divisor
+ if (simpDenom < 0)
+ FractionLiteral(-simpNum, -simpDenom)
+ else
+ FractionLiteral(simpNum, simpDenom)
+ }
+
+ val realzero = FractionLiteral(0, 1)
+ def floor(fl: FractionLiteral): FractionLiteral = {
+ val FractionLiteral(n, d) = normalizeFraction(fl)
+ if (d == 0) throw new IllegalStateException("denominator zero")
+ if (n == 0) realzero
+ else if (n > 0) {
+ //perform integer division
+ FractionLiteral(n / d, 1)
+ } else {
+ //here the number is negative
+ if (n % d == 0)
+ FractionLiteral(n / d, 1)
+ else {
+ //perform integer division and subtract 1
+ FractionLiteral(n / d - 1, 1)
+ }
+ }
+ }
}
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 2fa81b40f4d32a9d10a260313b14a0f2677a4edd..2c101cfce8fe18e092aec0fb53b8e5fb3702d77e 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -448,118 +448,6 @@ trait SymbolOps { self: TypeOps =>
replace(vars.map(vd => vd.toVariable -> valuator(vd)).toMap, expr)
}
- /** Simple, local optimization on string */
- def simplifyString(expr: Expr): Expr = {
- def simplify0(expr: Expr): Expr = (expr match {
- case StringConcat(StringLiteral(""), b) => b
- case StringConcat(b, StringLiteral("")) => b
- case StringConcat(StringLiteral(a), StringLiteral(b)) => StringLiteral(a + b)
- case StringLength(StringLiteral(a)) => IntLiteral(a.length)
- case SubString(StringLiteral(a), IntLiteral(start), IntLiteral(end)) => StringLiteral(a.substring(start.toInt, end.toInt))
- case _ => expr
- }).copiedFrom(expr)
- simplify0(expr)
- fixpoint(simplePostTransform(simplify0))(expr)
- }
-
- /** Simple, local simplification on arithmetic
- *
- * You should not assume anything smarter than some constant folding and
- * simple cancellation. To avoid infinite cycle we only apply simplification
- * that reduce the size of the tree. The only guarantee from this function is
- * to not augment the size of the expression and to be sound.
- */
- def simplifyArithmetic(expr: Expr): Expr = {
- def simplify0(expr: Expr): Expr = (expr match {
- case Plus(IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 + i2)
- case Plus(IntegerLiteral(zero), e) if zero == BigInt(0) => e
- case Plus(e, IntegerLiteral(zero)) if zero == BigInt(0) => e
- case Plus(e1, UMinus(e2)) => Minus(e1, e2)
- case Plus(Plus(e, IntegerLiteral(i1)), IntegerLiteral(i2)) => Plus(e, IntegerLiteral(i1+i2))
- case Plus(Plus(IntegerLiteral(i1), e), IntegerLiteral(i2)) => Plus(IntegerLiteral(i1+i2), e)
-
- case Minus(e, IntegerLiteral(zero)) if zero == BigInt(0) => e
- case Minus(IntegerLiteral(zero), e) if zero == BigInt(0) => UMinus(e)
- case Minus(IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 - i2)
- case Minus(e1, UMinus(e2)) => Plus(e1, e2)
- case Minus(e1, Minus(UMinus(e2), e3)) => Plus(e1, Plus(e2, e3))
-
- case UMinus(IntegerLiteral(x)) => IntegerLiteral(-x)
- case UMinus(UMinus(x)) => x
- case UMinus(Plus(UMinus(e1), e2)) => Plus(e1, UMinus(e2))
- case UMinus(Minus(e1, e2)) => Minus(e2, e1)
-
- case Times(IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 * i2)
- case Times(IntegerLiteral(one), e) if one == BigInt(1) => e
- case Times(IntegerLiteral(mone), e) if mone == BigInt(-1) => UMinus(e)
- case Times(e, IntegerLiteral(one)) if one == BigInt(1) => e
- case Times(IntegerLiteral(zero), _) if zero == BigInt(0) => IntegerLiteral(0)
- case Times(_, IntegerLiteral(zero)) if zero == BigInt(0) => IntegerLiteral(0)
- case Times(IntegerLiteral(i1), Times(IntegerLiteral(i2), t)) => Times(IntegerLiteral(i1*i2), t)
- case Times(IntegerLiteral(i1), Times(t, IntegerLiteral(i2))) => Times(IntegerLiteral(i1*i2), t)
- case Times(IntegerLiteral(i), UMinus(e)) => Times(IntegerLiteral(-i), e)
- case Times(UMinus(e), IntegerLiteral(i)) => Times(e, IntegerLiteral(-i))
- case Times(IntegerLiteral(i1), Division(e, IntegerLiteral(i2))) if i2 != BigInt(0) && i1 % i2 == BigInt(0) => Times(IntegerLiteral(i1/i2), e)
-
- case Division(IntegerLiteral(i1), IntegerLiteral(i2)) if i2 != BigInt(0) => IntegerLiteral(i1 / i2)
- case Division(e, IntegerLiteral(one)) if one == BigInt(1) => e
-
- //here we put more expensive rules
- //btw, I know those are not the most general rules, but they lead to good optimizations :)
- case Plus(UMinus(Plus(e1, e2)), e3) if e1 == e3 => UMinus(e2)
- case Plus(UMinus(Plus(e1, e2)), e3) if e2 == e3 => UMinus(e1)
- case Minus(e1, e2) if e1 == e2 => IntegerLiteral(0)
- case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => IntegerLiteral(0)
- case Minus(Plus(e1, e2), Plus(Plus(e3, e4), e5)) if e1 == e4 && e2 == e3 => UMinus(e5)
-
- case StringConcat(StringLiteral(""), a) => a
- case StringConcat(a, StringLiteral("")) => a
- case StringConcat(StringLiteral(a), StringLiteral(b)) => StringLiteral(a+b)
- case StringConcat(StringLiteral(a), StringConcat(StringLiteral(b), c)) => StringConcat(StringLiteral(a+b), c)
- case StringConcat(StringConcat(c, StringLiteral(a)), StringLiteral(b)) => StringConcat(c, StringLiteral(a+b))
- case StringConcat(a, StringConcat(b, c)) => StringConcat(StringConcat(a, b), c)
- //default
- case e => e
- }).copiedFrom(expr)
-
- fixpoint(simplePostTransform(simplify0))(expr)
- }
-
- /**
- * Some helper methods for FractionLiterals
- */
- def normalizeFraction(fl: FractionLiteral) = {
- val FractionLiteral(num, denom) = fl
- val modNum = if (num < 0) -num else num
- val modDenom = if (denom < 0) -denom else denom
- val divisor = modNum.gcd(modDenom)
- val simpNum = num / divisor
- val simpDenom = denom / divisor
- if (simpDenom < 0)
- FractionLiteral(-simpNum, -simpDenom)
- else
- FractionLiteral(simpNum, simpDenom)
- }
-
- val realzero = FractionLiteral(0, 1)
- def floor(fl: FractionLiteral): FractionLiteral = {
- val FractionLiteral(n, d) = normalizeFraction(fl)
- if (d == 0) throw new IllegalStateException("denominator zero")
- if (n == 0) realzero
- else if (n > 0) {
- //perform integer division
- FractionLiteral(n / d, 1)
- } else {
- //here the number is negative
- if (n % d == 0)
- FractionLiteral(n / d, 1)
- else {
- //perform integer division and subtract 1
- FractionLiteral(n / d - 1, 1)
- }
- }
- }
-
object InvocationExtractor {
private def flatInvocation(expr: Expr): Option[(Identifier, Seq[Type], Seq[Expr])] = expr match {
case fi @ FunctionInvocation(id, tps, args) => Some((id, tps, args))
diff --git a/src/test/scala/inox/InoxTestSuite.scala b/src/test/scala/inox/InoxTestSuite.scala
index 1e80c083b7546ff3027e9e6a509dfda0a840b12d..4ca956cf14fe275609357255dc7cc8053b8e3aa8 100644
--- a/src/test/scala/inox/InoxTestSuite.scala
+++ b/src/test/scala/inox/InoxTestSuite.scala
@@ -5,12 +5,14 @@ package inox
import org.scalatest._
import org.scalatest.concurrent._
-trait InoxTestSuite extends FunSuite with Timeouts {
+import utils._
+
+trait InoxTestSuite extends FunSuite with Matchers with Timeouts {
type FixtureParam = InoxContext
val configurations: Seq[Seq[InoxOption[Any]]] = Seq(Seq.empty)
- protected def test(name: String, tags: Tag*)(test: InoxContext => Outcome): Unit = {
+ protected def test(name: String, tags: Tag*)(test: InoxContext => Unit): Unit = {
for (config <- configurations) {
val reporter = new TestSilentReporter
val ctx = InoxContext(reporter, new InterruptManager(reporter), InoxOptions(config))
@@ -18,8 +20,8 @@ trait InoxTestSuite extends FunSuite with Timeouts {
test(ctx)
} catch {
case err: FatalError =>
- reporter.lastErrors ++= err.msg
- Failed(new exceptions.TestFailedException(reporter.lastErrors.mkString("\n"), err, 5))
+ reporter.lastErrors :+= err.msg
+ throw new exceptions.TestFailedException(reporter.lastErrors.mkString("\n"), err, 5)
}
}
}
diff --git a/src/test/scala/inox/SolvingTestSuite.scala b/src/test/scala/inox/SolvingTestSuite.scala
index bcc837762636b561e0d7c0827dc1addab68b2408..a522214ef896964737ff111e69bd58c255a84027 100644
--- a/src/test/scala/inox/SolvingTestSuite.scala
+++ b/src/test/scala/inox/SolvingTestSuite.scala
@@ -6,15 +6,15 @@ trait SolvingTestSuite extends InoxTestSuite {
import solvers._
override val configurations = for {
- solverName <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4")
- checkModels <- Seq(true, false)
- feelingLucky <- Seq(true, false)
- unrollCores <- Seq(true, false)
+ solverName <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4")
+ checkModels <- Seq(true, false)
+ feelingLucky <- Seq(true, false)
+ unrollAssumptions <- Seq(true, false)
} yield Seq(
- InoxOption(InoxOptions.optSelectedSolver)(Set(solverName)),
+ InoxOption(InoxOptions.optSelectedSolvers)(Set(solverName)),
InoxOption(optCheckModels)(checkModels),
InoxOption(unrolling.optFeelingLucky)(feelingLucky),
- InoxOption(unrolling.optUnrollCores)(unrollCores),
+ InoxOption(unrolling.optUnrollAssumptions)(unrollAssumptions),
InoxOption(InoxOptions.optTimeout)(300)
)
}
diff --git a/src/test/scala/inox/TestSilentReporter.scala b/src/test/scala/inox/TestSilentReporter.scala
index 6ecd70be9dfd086160a85a82fe01e6ac598535ea..a42ec27a4736bcd699afdbe5a3654a519d8ef09d 100644
--- a/src/test/scala/inox/TestSilentReporter.scala
+++ b/src/test/scala/inox/TestSilentReporter.scala
@@ -2,8 +2,6 @@
package inox
-import DefaultReporter
-
class TestSilentReporter extends DefaultReporter(Set()) {
var lastErrors: List[String] = Nil
diff --git a/src/test/scala/inox/regression/SimpleQuantifiersSuite.scala b/src/test/scala/inox/regression/SimpleQuantifiersSuite.scala
index 026c325342420b4f8ed8d3850a9f3db8fec0c131..db43db66a36a1fc6f51b3fe37fe0f4d440bab9a8 100644
--- a/src/test/scala/inox/regression/SimpleQuantifiersSuite.scala
+++ b/src/test/scala/inox/regression/SimpleQuantifiersSuite.scala
@@ -3,29 +3,31 @@
package inox
package regression
+import solvers._
+
class SimpleQuantifiersSuite extends SolvingTestSuite {
import inox.trees._
import dsl._
val isAssociativeID = FreshIdentifier("isAssociative")
- val isAssociative = mkFunDef(isAssociativeID)("A") { case Seq(aT) =>
+ val isAssociative = mkFunDef(isAssociativeID)("A") { case Seq(aT) => (
Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
forall("x" :: aT, "y" :: aT, "z" :: aT)((x,y,z) => f(f(x,y),z) === f(x,f(y,z)))
- }
+ })
}
val isCommutativeID = FreshIdentifier("isCommutative")
- val isCommutative = mkFunDef(isCommutativeID)("A") { case Seq(aT) =>
+ val isCommutative = mkFunDef(isCommutativeID)("A") { case Seq(aT) => (
Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
forall("x" :: aT, "y" :: aT)((x,y) => f(x,y) === f(y,x))
- }
+ })
}
val isRotateID = FreshIdentifier("isRotate")
- val isRotate = mkFunDef(isRotateID)("A") { case Seq(aT) =>
+ val isRotate = mkFunDef(isRotateID)("A") { case Seq(aT) => (
Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
forall("x" :: aT, "y" :: aT, "z" :: aT)((x,y,z) => f(f(x,y),z) === f(f(y,z),x))
- }
+ })
}
val symbols = new Symbols(Map(
@@ -38,7 +40,7 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
val program = InoxProgram(ctx, symbols)
val (aT,bT) = (T("A"), T("B"))
- val Seq(f1,f2) = Seq("f1" :: (T(aT, aT) =>: aT), "f2" :: (T(bT, bT) =>: bT))
+ val Seq(f1,f2) = Seq("f1" :: (T(aT, aT) =>: aT), "f2" :: (T(bT, bT) =>: bT)).map(_.toVariable)
val clause = isAssociative(aT)(f1) && isAssociative(bT)(f2) && !isAssociative(T(aT,bT)) {
\("p1" :: T(aT,bT), "p2" :: T(aT, bT))((p1,p2) => E(f1(p1._1,p2._1), f2(p1._2,p2._2)))
}
@@ -52,7 +54,7 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
val program = InoxProgram(ctx, symbols)
val aT = T("A")
- val f = "f" :: (T(aT, aT) =>: aT)
+ val f = ("f" :: (T(aT, aT) =>: aT)).toVariable
val clause = isCommutative(aT)(f) && isRotate(aT)(f) && !isAssociative(aT)(f)
val sf = SolverFactory.default(program)
@@ -63,7 +65,7 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
test("Commutative and rotate ==> associative (integer type)") { ctx =>
val program = InoxProgram(ctx, symbols)
- val f = "f" :: (T(IntegerType, IntegerType) =>: IntegerType)
+ val f = ("f" :: (T(IntegerType, IntegerType) =>: IntegerType)).toVariable
val clause = isCommutative(IntegerType)(f) && isRotate(IntegerType)(f) && !isAssociative(IntegerType)(f)
val sf = SolverFactory.default(program)
@@ -75,7 +77,7 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
val program = InoxProgram(ctx, symbols)
val aT = T("A")
- val f = "f" :: (T(aT, aT) =>: aT)
+ val f = ("f" :: (T(aT, aT) =>: aT)).toVariable
val clause = isAssociative(aT)(f) && !isCommutative(aT)(f)
val sf = SolverFactory.default(program)
@@ -87,7 +89,7 @@ class SimpleQuantifiersSuite extends SolvingTestSuite {
val program = InoxProgram(ctx, symbols)
val aT = T("A")
- val f = "f" :: (T(aT, aT) =>: aT)
+ val f = ("f" :: (T(aT, aT) =>: aT)).toVariable
val clause = isCommutative(aT)(f) && !isAssociative(aT)(f)
val sf = SolverFactory.default(program)
diff --git a/src/test/scala/inox/unit/evaluators/EvaluatorSuite.scala b/src/test/scala/inox/unit/evaluators/EvaluatorSuite.scala
index e7c0f8d8f15eef2c5734218ec905c00a076486d9..80d6eced505d4a6b244f9c9b09518b152e73226f 100644
--- a/src/test/scala/inox/unit/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/inox/unit/evaluators/EvaluatorSuite.scala
@@ -1,267 +1,272 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon.unit.evaluators
+package inox.unit.evaluators
-import leon._
-import leon.test._
-import leon.evaluators._
+import inox._
+import inox.evaluators._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.Extractors._
-import leon.purescala.Constructors._
+class EvaluatorSuite extends InoxTestSuite {
+ import inox.trees._
-class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
-
- implicit val pgm = Program.empty
-
- def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
- List(
- new DefaultEvaluator(ctx, pgm),
- new AngelicEvaluator(new StreamEvaluator(ctx, pgm))
- )
- }
-
- def codegenEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
- List(
- new CodeGenEvaluator(ctx, pgm)
- )
+ val symbols = new Symbols(Map.empty, Map.empty)
+ def evaluator(ctx: InoxContext): DeterministicEvaluator { val program: InoxProgram } = {
+ val program = InoxProgram(ctx, symbols)
+ RecursiveEvaluator.default(program)
}
- def allEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
- normalEvaluators ++ codegenEvaluators
+ test("Literals") { ctx =>
+ val e = evaluator(ctx)
+
+ eval(e, BooleanLiteral(true)) === BooleanLiteral(true)
+ eval(e, BooleanLiteral(false)) === BooleanLiteral(false)
+ eval(e, IntLiteral(0)) === IntLiteral(0)
+ eval(e, IntLiteral(42)) === IntLiteral(42)
+ eval(e, UnitLiteral()) === UnitLiteral()
+ eval(e, IntegerLiteral(0)) === IntegerLiteral(0)
+ eval(e, IntegerLiteral(42)) === IntegerLiteral(42)
+ eval(e, FractionLiteral(0 ,1)) === FractionLiteral(0 ,1)
+ eval(e, FractionLiteral(42 ,1)) === FractionLiteral(42, 1)
+ eval(e, FractionLiteral(26, 3)) === FractionLiteral(26, 3)
}
+ test("BitVector Arithmetic") { ctx =>
+ val e = evaluator(ctx)
- test("Literals") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, BooleanLiteral(true)) === BooleanLiteral(true)
- eval(e, BooleanLiteral(false)) === BooleanLiteral(false)
- eval(e, IntLiteral(0)) === IntLiteral(0)
- eval(e, IntLiteral(42)) === IntLiteral(42)
- eval(e, UnitLiteral()) === UnitLiteral()
- eval(e, InfiniteIntegerLiteral(0)) === InfiniteIntegerLiteral(0)
- eval(e, InfiniteIntegerLiteral(42)) === InfiniteIntegerLiteral(42)
- eval(e, FractionalLiteral(0 ,1)) === FractionalLiteral(0 ,1)
- eval(e, FractionalLiteral(42 ,1)) === FractionalLiteral(42, 1)
- eval(e, FractionalLiteral(26, 3)) === FractionalLiteral(26, 3)
- }
+ eval(e, Plus(IntLiteral(3), IntLiteral(5))) === IntLiteral(8)
+ eval(e, Plus(IntLiteral(0), IntLiteral(5))) === IntLiteral(5)
+ eval(e, Times(IntLiteral(3), IntLiteral(3))) === IntLiteral(9)
}
- test("BitVector Arithmetic") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, BVPlus(IntLiteral(3), IntLiteral(5))) === IntLiteral(8)
- eval(e, BVPlus(IntLiteral(0), IntLiteral(5))) === IntLiteral(5)
- eval(e, BVTimes(IntLiteral(3), IntLiteral(3))) === IntLiteral(9)
- }
- }
+ test("eval bitwise operations") { ctx =>
+ val e = evaluator(ctx)
- test("eval bitwise operations") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, BVAnd(IntLiteral(3), IntLiteral(1))) === IntLiteral(1)
- eval(e, BVAnd(IntLiteral(3), IntLiteral(3))) === IntLiteral(3)
- eval(e, BVAnd(IntLiteral(5), IntLiteral(3))) === IntLiteral(1)
- eval(e, BVAnd(IntLiteral(5), IntLiteral(4))) === IntLiteral(4)
- eval(e, BVAnd(IntLiteral(5), IntLiteral(2))) === IntLiteral(0)
+ eval(e, BVAnd(IntLiteral(3), IntLiteral(1))) === IntLiteral(1)
+ eval(e, BVAnd(IntLiteral(3), IntLiteral(3))) === IntLiteral(3)
+ eval(e, BVAnd(IntLiteral(5), IntLiteral(3))) === IntLiteral(1)
+ eval(e, BVAnd(IntLiteral(5), IntLiteral(4))) === IntLiteral(4)
+ eval(e, BVAnd(IntLiteral(5), IntLiteral(2))) === IntLiteral(0)
- eval(e, BVOr(IntLiteral(3), IntLiteral(1))) === IntLiteral(3)
- eval(e, BVOr(IntLiteral(3), IntLiteral(3))) === IntLiteral(3)
- eval(e, BVOr(IntLiteral(5), IntLiteral(3))) === IntLiteral(7)
- eval(e, BVOr(IntLiteral(5), IntLiteral(4))) === IntLiteral(5)
- eval(e, BVOr(IntLiteral(5), IntLiteral(2))) === IntLiteral(7)
+ eval(e, BVOr(IntLiteral(3), IntLiteral(1))) === IntLiteral(3)
+ eval(e, BVOr(IntLiteral(3), IntLiteral(3))) === IntLiteral(3)
+ eval(e, BVOr(IntLiteral(5), IntLiteral(3))) === IntLiteral(7)
+ eval(e, BVOr(IntLiteral(5), IntLiteral(4))) === IntLiteral(5)
+ eval(e, BVOr(IntLiteral(5), IntLiteral(2))) === IntLiteral(7)
- eval(e, BVXOr(IntLiteral(3), IntLiteral(1))) === IntLiteral(2)
- eval(e, BVXOr(IntLiteral(3), IntLiteral(3))) === IntLiteral(0)
+ eval(e, BVXOr(IntLiteral(3), IntLiteral(1))) === IntLiteral(2)
+ eval(e, BVXOr(IntLiteral(3), IntLiteral(3))) === IntLiteral(0)
- eval(e, BVNot(IntLiteral(1))) === IntLiteral(-2)
+ eval(e, BVNot(IntLiteral(1))) === IntLiteral(-2)
- eval(e, BVShiftLeft(IntLiteral(3), IntLiteral(1))) === IntLiteral(6)
- eval(e, BVShiftLeft(IntLiteral(4), IntLiteral(2))) === IntLiteral(16)
+ eval(e, BVShiftLeft(IntLiteral(3), IntLiteral(1))) === IntLiteral(6)
+ eval(e, BVShiftLeft(IntLiteral(4), IntLiteral(2))) === IntLiteral(16)
- eval(e, BVLShiftRight(IntLiteral(8), IntLiteral(1))) === IntLiteral(4)
- eval(e, BVAShiftRight(IntLiteral(8), IntLiteral(1))) === IntLiteral(4)
- }
+ eval(e, BVLShiftRight(IntLiteral(8), IntLiteral(1))) === IntLiteral(4)
+ eval(e, BVAShiftRight(IntLiteral(8), IntLiteral(1))) === IntLiteral(4)
}
- test("Arithmetic") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(5))) === InfiniteIntegerLiteral(8)
- eval(e, Minus(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(2))) === InfiniteIntegerLiteral(5)
- eval(e, UMinus(InfiniteIntegerLiteral(7))) === InfiniteIntegerLiteral(-7)
- eval(e, Times(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3))) === InfiniteIntegerLiteral(6)
- }
+ test("Arithmetic") { ctx =>
+ val e = evaluator(ctx)
+
+ eval(e, Plus(IntegerLiteral(3), IntegerLiteral(5))) === IntegerLiteral(8)
+ eval(e, Minus(IntegerLiteral(7), IntegerLiteral(2))) === IntegerLiteral(5)
+ eval(e, UMinus(IntegerLiteral(7))) === IntegerLiteral(-7)
+ eval(e, Times(IntegerLiteral(2), IntegerLiteral(3))) === IntegerLiteral(6)
}
- test("BigInt Modulo and Remainder") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, Division(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))) === InfiniteIntegerLiteral(3)
- eval(e, Remainder(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))) === InfiniteIntegerLiteral(1)
- eval(e, Modulo(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))) === InfiniteIntegerLiteral(1)
+ test("BigInt Modulo and Remainder") { ctx =>
+ val e = evaluator(ctx)
- eval(e, Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))) === InfiniteIntegerLiteral(0)
- eval(e, Remainder(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))) === InfiniteIntegerLiteral(-1)
+ eval(e, Division(IntegerLiteral(10), IntegerLiteral(3))) === IntegerLiteral(3)
+ eval(e, Remainder(IntegerLiteral(10), IntegerLiteral(3))) === IntegerLiteral(1)
+ eval(e, Modulo(IntegerLiteral(10), IntegerLiteral(3))) === IntegerLiteral(1)
- eval(e, Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))) === InfiniteIntegerLiteral(2)
+ eval(e, Division(IntegerLiteral(-1), IntegerLiteral(3))) === IntegerLiteral(0)
+ eval(e, Remainder(IntegerLiteral(-1), IntegerLiteral(3))) === IntegerLiteral(-1)
- eval(e, Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))) === InfiniteIntegerLiteral(0)
- eval(e, Remainder(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))) === InfiniteIntegerLiteral(-1)
- eval(e, Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))) === InfiniteIntegerLiteral(2)
+ eval(e, Modulo(IntegerLiteral(-1), IntegerLiteral(3))) === IntegerLiteral(2)
- eval(e, Division(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))) === InfiniteIntegerLiteral(0)
- eval(e, Remainder(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))) === InfiniteIntegerLiteral(1)
- eval(e, Modulo(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))) === InfiniteIntegerLiteral(1)
- }
+ eval(e, Division(IntegerLiteral(-1), IntegerLiteral(-3))) === IntegerLiteral(0)
+ eval(e, Remainder(IntegerLiteral(-1), IntegerLiteral(-3))) === IntegerLiteral(-1)
+ eval(e, Modulo(IntegerLiteral(-1), IntegerLiteral(-3))) === IntegerLiteral(2)
+
+ eval(e, Division(IntegerLiteral(1), IntegerLiteral(-3))) === IntegerLiteral(0)
+ eval(e, Remainder(IntegerLiteral(1), IntegerLiteral(-3))) === IntegerLiteral(1)
+ eval(e, Modulo(IntegerLiteral(1), IntegerLiteral(-3))) === IntegerLiteral(1)
}
- test("Int Comparisons") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, GreaterEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))) === BooleanLiteral(true)
- eval(e, GreaterEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))) === BooleanLiteral(true)
- eval(e, GreaterEquals(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))) === BooleanLiteral(false)
+ test("Int Comparisons") { ctx =>
+ val e = evaluator(ctx)
- eval(e, GreaterThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))) === BooleanLiteral(true)
- eval(e, GreaterThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))) === BooleanLiteral(false)
- eval(e, GreaterThan(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))) === BooleanLiteral(false)
+ eval(e, GreaterEquals(IntegerLiteral(7), IntegerLiteral(4))) === BooleanLiteral(true)
+ eval(e, GreaterEquals(IntegerLiteral(7), IntegerLiteral(7))) === BooleanLiteral(true)
+ eval(e, GreaterEquals(IntegerLiteral(4), IntegerLiteral(7))) === BooleanLiteral(false)
- eval(e, LessEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))) === BooleanLiteral(false)
- eval(e, LessEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))) === BooleanLiteral(true)
- eval(e, LessEquals(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))) === BooleanLiteral(true)
+ eval(e, GreaterThan(IntegerLiteral(7), IntegerLiteral(4))) === BooleanLiteral(true)
+ eval(e, GreaterThan(IntegerLiteral(7), IntegerLiteral(7))) === BooleanLiteral(false)
+ eval(e, GreaterThan(IntegerLiteral(4), IntegerLiteral(7))) === BooleanLiteral(false)
- eval(e, LessThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))) === BooleanLiteral(false)
- eval(e, LessThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))) === BooleanLiteral(false)
- eval(e, LessThan(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))) === BooleanLiteral(true)
- }
+ eval(e, LessEquals(IntegerLiteral(7), IntegerLiteral(4))) === BooleanLiteral(false)
+ eval(e, LessEquals(IntegerLiteral(7), IntegerLiteral(7))) === BooleanLiteral(true)
+ eval(e, LessEquals(IntegerLiteral(4), IntegerLiteral(7))) === BooleanLiteral(true)
+
+ eval(e, LessThan(IntegerLiteral(7), IntegerLiteral(4))) === BooleanLiteral(false)
+ eval(e, LessThan(IntegerLiteral(7), IntegerLiteral(7))) === BooleanLiteral(false)
+ eval(e, LessThan(IntegerLiteral(4), IntegerLiteral(7))) === BooleanLiteral(true)
}
+ test("Int Modulo and Remainder") { ctx =>
+ val e = evaluator(ctx)
- test("Int Modulo and Remainder") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, BVDivision(IntLiteral(10), IntLiteral(3))) === IntLiteral(3)
- eval(e, BVRemainder(IntLiteral(10), IntLiteral(3))) === IntLiteral(1)
+ eval(e, Division(IntLiteral(10), IntLiteral(3))) === IntLiteral(3)
+ eval(e, Remainder(IntLiteral(10), IntLiteral(3))) === IntLiteral(1)
- eval(e, BVDivision(IntLiteral(-1), IntLiteral(3))) === IntLiteral(0)
- eval(e, BVRemainder(IntLiteral(-1), IntLiteral(3))) === IntLiteral(-1)
+ eval(e, Division(IntLiteral(-1), IntLiteral(3))) === IntLiteral(0)
+ eval(e, Remainder(IntLiteral(-1), IntLiteral(3))) === IntLiteral(-1)
- eval(e, BVDivision(IntLiteral(-1), IntLiteral(-3))) === IntLiteral(0)
- eval(e, BVRemainder(IntLiteral(-1), IntLiteral(-3))) === IntLiteral(-1)
+ eval(e, Division(IntLiteral(-1), IntLiteral(-3))) === IntLiteral(0)
+ eval(e, Remainder(IntLiteral(-1), IntLiteral(-3))) === IntLiteral(-1)
- eval(e, BVDivision(IntLiteral(1), IntLiteral(-3))) === IntLiteral(0)
- eval(e, BVRemainder(IntLiteral(1), IntLiteral(-3))) === IntLiteral(1)
- }
+ eval(e, Division(IntLiteral(1), IntLiteral(-3))) === IntLiteral(0)
+ eval(e, Remainder(IntLiteral(1), IntLiteral(-3))) === IntLiteral(1)
}
- test("Boolean Operations") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, And(BooleanLiteral(true), BooleanLiteral(true))) === BooleanLiteral(true)
- eval(e, And(BooleanLiteral(true), BooleanLiteral(false))) === BooleanLiteral(false)
- eval(e, And(BooleanLiteral(false), BooleanLiteral(false))) === BooleanLiteral(false)
- eval(e, And(BooleanLiteral(false), BooleanLiteral(true))) === BooleanLiteral(false)
- eval(e, Or(BooleanLiteral(true), BooleanLiteral(true))) === BooleanLiteral(true)
- eval(e, Or(BooleanLiteral(true), BooleanLiteral(false))) === BooleanLiteral(true)
- eval(e, Or(BooleanLiteral(false), BooleanLiteral(false))) === BooleanLiteral(false)
- eval(e, Or(BooleanLiteral(false), BooleanLiteral(true))) === BooleanLiteral(true)
- eval(e, Not(BooleanLiteral(false))) === BooleanLiteral(true)
- eval(e, Not(BooleanLiteral(true))) === BooleanLiteral(false)
- }
+ test("Boolean Operations") { ctx =>
+ val e = evaluator(ctx)
+
+ eval(e, And(BooleanLiteral(true), BooleanLiteral(true))) === BooleanLiteral(true)
+ eval(e, And(BooleanLiteral(true), BooleanLiteral(false))) === BooleanLiteral(false)
+ eval(e, And(BooleanLiteral(false), BooleanLiteral(false))) === BooleanLiteral(false)
+ eval(e, And(BooleanLiteral(false), BooleanLiteral(true))) === BooleanLiteral(false)
+ eval(e, Or(BooleanLiteral(true), BooleanLiteral(true))) === BooleanLiteral(true)
+ eval(e, Or(BooleanLiteral(true), BooleanLiteral(false))) === BooleanLiteral(true)
+ eval(e, Or(BooleanLiteral(false), BooleanLiteral(false))) === BooleanLiteral(false)
+ eval(e, Or(BooleanLiteral(false), BooleanLiteral(true))) === BooleanLiteral(true)
+ eval(e, Not(BooleanLiteral(false))) === BooleanLiteral(true)
+ eval(e, Not(BooleanLiteral(true))) === BooleanLiteral(false)
}
- test("Real Arightmetic") { implicit fix =>
- for (e <- allEvaluators) {
- eval(e, RealPlus(FractionalLiteral(2, 3), FractionalLiteral(1, 3))) === FractionalLiteral(1, 1)
- eval(e, RealMinus(FractionalLiteral(1, 1), FractionalLiteral(1, 4))) === FractionalLiteral(3, 4)
- eval(e, RealUMinus(FractionalLiteral(7, 1))) === FractionalLiteral(-7, 1)
- eval(e, RealTimes(FractionalLiteral(2, 3), FractionalLiteral(1, 3))) === FractionalLiteral(2, 9)
- }
- }
+ test("Real Arightmetic") { ctx =>
+ val e = evaluator(ctx)
- test("Real Comparisons") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, GreaterEquals(FractionalLiteral(7, 1), FractionalLiteral(4, 2))) === BooleanLiteral(true)
- eval(e, GreaterEquals(FractionalLiteral(7, 2), FractionalLiteral(49, 13))) === BooleanLiteral(false)
+ eval(e, Plus(FractionLiteral(2, 3), FractionLiteral(1, 3))) === FractionLiteral(1, 1)
+ eval(e, Minus(FractionLiteral(1, 1), FractionLiteral(1, 4))) === FractionLiteral(3, 4)
+ eval(e, UMinus(FractionLiteral(7, 1))) === FractionLiteral(-7, 1)
+ eval(e, Times(FractionLiteral(2, 3), FractionLiteral(1, 3))) === FractionLiteral(2, 9)
+ }
- eval(e, GreaterThan(FractionalLiteral(49, 13), FractionalLiteral(7, 2))) === BooleanLiteral(true)
- eval(e, GreaterThan(FractionalLiteral(49, 14), FractionalLiteral(7, 2))) === BooleanLiteral(false)
- eval(e, GreaterThan(FractionalLiteral(4, 2), FractionalLiteral(7, 1))) === BooleanLiteral(false)
+ test("Real Comparisons") { ctx =>
+ val e = evaluator(ctx)
- eval(e, LessEquals(FractionalLiteral(7, 1), FractionalLiteral(4, 2))) === BooleanLiteral(false)
- eval(e, LessEquals(FractionalLiteral(7, 2), FractionalLiteral(49, 13))) === BooleanLiteral(true)
+ eval(e, GreaterEquals(FractionLiteral(7, 1), FractionLiteral(4, 2))) === BooleanLiteral(true)
+ eval(e, GreaterEquals(FractionLiteral(7, 2), FractionLiteral(49, 13))) === BooleanLiteral(false)
- eval(e, LessThan(FractionalLiteral(49, 13), FractionalLiteral(7, 2))) === BooleanLiteral(false)
- eval(e, LessThan(FractionalLiteral(49, 14), FractionalLiteral(7, 2))) === BooleanLiteral(false)
- eval(e, LessThan(FractionalLiteral(4, 2), FractionalLiteral(7, 1))) === BooleanLiteral(true)
- }
- }
+ eval(e, GreaterThan(FractionLiteral(49, 13), FractionLiteral(7, 2))) === BooleanLiteral(true)
+ eval(e, GreaterThan(FractionLiteral(49, 14), FractionLiteral(7, 2))) === BooleanLiteral(false)
+ eval(e, GreaterThan(FractionLiteral(4, 2), FractionLiteral(7, 1))) === BooleanLiteral(false)
- test("Simple Variable") { implicit fix =>
- for(e <- allEvaluators) {
- val id = FreshIdentifier("id", Int32Type)
+ eval(e, LessEquals(FractionLiteral(7, 1), FractionLiteral(4, 2))) === BooleanLiteral(false)
+ eval(e, LessEquals(FractionLiteral(7, 2), FractionLiteral(49, 13))) === BooleanLiteral(true)
- eval(e, Variable(id), Map(id -> IntLiteral(23))) === IntLiteral(23)
- }
+ eval(e, LessThan(FractionLiteral(49, 13), FractionLiteral(7, 2))) === BooleanLiteral(false)
+ eval(e, LessThan(FractionLiteral(49, 14), FractionLiteral(7, 2))) === BooleanLiteral(false)
+ eval(e, LessThan(FractionLiteral(4, 2), FractionLiteral(7, 1))) === BooleanLiteral(true)
}
- test("Undefined Variable") { implicit fix =>
- for(e <- allEvaluators) {
- val id = FreshIdentifier("id", Int32Type)
- val foo = FreshIdentifier("foo", Int32Type)
+ test("Simple Variable") { ctx =>
+ val e = evaluator(ctx)
- eval(e, Variable(id), Map(foo -> IntLiteral(23))).failed
- }
- }
+ val v = Variable(FreshIdentifier("id"), Int32Type)
- test("Let") { implicit fix =>
- for(e <- normalEvaluators) {
- val id = FreshIdentifier("id")
- eval(e, Let(id, IntLiteral(42), Variable(id))) === IntLiteral(42)
- }
- }
-
- def eqArray(a1: Expr, a2: Expr) = (a1, a2) match {
- case (FiniteArray(es1, d1, IntLiteral(l1)), FiniteArray(es2, d2, IntLiteral(l2))) =>
- assert(l1 === l2)
- for (i <- 0 until l1) {
- val v1 = es1.get(i).orElse(d1)
- val v2 = es2.get(i).orElse(d2)
- assert(v1 === v2)
- }
- case (e, _) =>
- fail("Expected array, got "+e)
+ eval(e, v, Map(v.toVal -> IntLiteral(23))) === IntLiteral(23)
}
- test("Array Operations") { implicit fix =>
- for (e <- allEvaluators) {
- eqArray(eval(e, finiteArray(Map[Int,Expr](), Some(IntLiteral(12), IntLiteral(7)), Int32Type)).res,
- finiteArray(Map[Int,Expr](), Some(IntLiteral(12), IntLiteral(7)), Int32Type))
+ test("Undefined Variable") { ctx =>
+ val e = evaluator(ctx)
- eval(e, ArrayLength(finiteArray(Map[Int,Expr](), Some(IntLiteral(12), IntLiteral(7)), Int32Type))) ===
- IntLiteral(7)
+ val v1 = Variable(FreshIdentifier("id"), Int32Type)
+ val v2 = Variable(FreshIdentifier("foo"), Int32Type)
- eval(e, ArraySelect(finiteArray(Seq(IntLiteral(2), IntLiteral(4), IntLiteral(7))), IntLiteral(1))) ===
- IntLiteral(4)
+ eval(e, v1, Map(v2.toVal -> IntLiteral(23))).failed
+ }
- eqArray(eval(e, ArrayUpdated( finiteArray(Seq(IntLiteral(2), IntLiteral(4), IntLiteral(7))), IntLiteral(1), IntLiteral(42))).res,
- finiteArray(Seq(IntLiteral(2), IntLiteral(42), IntLiteral(7))))
+ test("Let") { ctx =>
+ val e = evaluator(ctx)
- }
+ val v = Variable(FreshIdentifier("id"), IntegerType)
+ eval(e, Let(v.toVal, IntLiteral(42), v)) === IntLiteral(42)
}
- test("Array with variable length") { implicit fix =>
- // This does not work with CodegenEvaluator
- for (e <- normalEvaluators) {
- val len = FreshIdentifier("len", Int32Type)
- eval(e, ArrayLength(finiteArray(Map[Int, Expr](), Some(IntLiteral(12), Variable(len)), Int32Type)), Map(len -> IntLiteral(27))) ===
- IntLiteral(27)
- }
+ test("Map Operations") { ctx =>
+ val e = evaluator(ctx)
+
+ eval(e, Equals(
+ FiniteMap(Seq.empty, IntLiteral(12), Int32Type),
+ FiniteMap(Seq.empty, IntLiteral(12), Int32Type))
+ ) === BooleanLiteral(true)
+
+ eval(e, Equals(
+ FiniteMap(Seq.empty, IntLiteral(9), Int32Type),
+ FiniteMap(Seq.empty, IntLiteral(12), Int32Type))
+ ) === BooleanLiteral(false)
+
+ eval(e, Equals(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(3)), IntLiteral(9), Int32Type),
+ FiniteMap(Seq(IntLiteral(2) -> IntLiteral(3), IntLiteral(1) -> IntLiteral(2)), IntLiteral(9), Int32Type))
+ ) === BooleanLiteral(true)
+
+ eval(e, Equals(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(1) -> IntLiteral(3)), IntLiteral(9), Int32Type),
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(3), IntLiteral(1) -> IntLiteral(2)), IntLiteral(9), Int32Type))
+ ) === BooleanLiteral(false)
+
+ eval(e, Equals(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(1) -> IntLiteral(3)), IntLiteral(9), Int32Type),
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(3)), IntLiteral(9), Int32Type))
+ ) === BooleanLiteral(true)
+
+ eval(e, MapApply(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type),
+ IntLiteral(1))
+ ) === IntLiteral(4)
+
+ eval(e, MapApply(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type),
+ IntLiteral(3))
+ ) === IntLiteral(6)
+
+ eval(e, MapApply(
+ MapUpdated(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type),
+ IntLiteral(1), IntLiteral(3)),
+ IntLiteral(1))
+ ) === IntLiteral(3)
}
- test("Array Default Value") { implicit fix =>
- for (e <- allEvaluators) {
- val id = FreshIdentifier("id", Int32Type)
- eqArray(eval(e, finiteArray(Map[Int, Expr](), Some(Variable(id), IntLiteral(7)), Int32Type), Map(id -> IntLiteral(27))).res,
- finiteArray(Map[Int, Expr](), Some(IntLiteral(27), IntLiteral(7)), Int32Type))
- }
+ test("Map with variables") { ctx =>
+ val e = evaluator(ctx)
+
+ val v1 = Variable(FreshIdentifier("v1"), Int32Type)
+ val v2 = Variable(FreshIdentifier("v2"), Int32Type)
+ val v3 = Variable(FreshIdentifier("v3"), Int32Type)
+
+ eval(e, Equals(
+ FiniteMap(Seq(v1 -> IntLiteral(2), v2 -> IntLiteral(4)), v3, Int32Type),
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type)),
+ Map(v1.toVal -> IntLiteral(1), v2.toVal -> IntLiteral(2), v3.toVal -> IntLiteral(6))
+ ) === BooleanLiteral(true)
+
+ eval(e, MapApply(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type),
+ v1),
+ Map(v1.toVal -> IntLiteral(3))
+ ) === IntLiteral(6)
+
+ eval(e, MapApply(
+ MapUpdated(
+ FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type),
+ v1, v2), v3),
+ Map(v1.toVal -> IntLiteral(1), v2.toVal -> IntLiteral(3), v3.toVal -> IntLiteral(1))
+ ) === IntLiteral(3)
}
abstract class EvalDSL {
@@ -271,7 +276,7 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
def success: Expr = res
}
- case class Success(expr: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator, res: Expr) extends EvalDSL {
+ case class Success(expr: Expr, env: Map[ValDef, Expr], evaluator: DeterministicEvaluator, res: Expr) extends EvalDSL {
override def failed = {
fail(s"Evaluation of '$expr' with '$evaluator' (and env $env) should have failed")
}
@@ -281,7 +286,7 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
}
}
- case class Failed(expr: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator, err: String) extends EvalDSL {
+ case class Failed(expr: Expr, env: Map[ValDef, Expr], evaluator: DeterministicEvaluator, err: String) extends EvalDSL {
override def success = {
fail(s"Evaluation of '$expr' with '$evaluator' (and env $env) should have succeeded but failed with $err")
}
@@ -291,7 +296,11 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
def ===(res: Expr) = success
}
- def eval(e: DeterministicEvaluator, toEval: Expr, env: Map[Identifier, Expr] = Map()): EvalDSL = {
+ def eval(
+ e: DeterministicEvaluator { val program: InoxProgram },
+ toEval: Expr,
+ env: Map[ValDef, Expr] = Map()
+ ): EvalDSL = {
e.eval(toEval, env) match {
case EvaluationResults.Successful(res) => Success(toEval, env, e, res)
case EvaluationResults.RuntimeError(err) => Failed(toEval, env, e, err)
diff --git a/src/test/scala/inox/unit/orb/OrbUnitTestSuite.scala b/src/test/scala/inox/unit/orb/OrbUnitTestSuite.scala
deleted file mode 100644
index ac6a65f71602e8c73769bd3e9c81c350eabfc243..0000000000000000000000000000000000000000
--- a/src/test/scala/inox/unit/orb/OrbUnitTestSuite.scala
+++ /dev/null
@@ -1,82 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.unit.orb
-
-import leon._
-import leon.test._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.Common._
-import leon.purescala.ExprOps._
-import leon.invariant.util.LetTupleSimplification
-import scala.math.BigInt.int2bigInt
-import leon.purescala.Definitions._
-import leon.invariant.engine._
-import leon.transformations._
-import java.io.File
-import leon.purescala.Types.TupleType
-import leon.utils._
-import invariant.structure.LinearConstraintUtil._
-import leon.invariant.util.ExpressionTransformer._
-import invariant.structure._
-import invariant.util._
-import ProgramUtil._
-import Util.zero
-
-class OrbUnitTestSuite extends LeonTestSuite {
- val a = FreshIdentifier("a", IntegerType).toVariable
- val b = FreshIdentifier("b", IntegerType).toVariable
- val c = FreshIdentifier("c", IntegerType).toVariable
- val d = FreshIdentifier("d", IntegerType).toVariable
- val l42 = InfiniteIntegerLiteral(42)
- val l43 = InfiniteIntegerLiteral(43)
- val mtwo = InfiniteIntegerLiteral(-2)
-
- test("Pull lets to top with tuples and tuple select") { ctx =>
- val in = TupleSelect(Tuple(Seq(a, b)), 1)
- val exp = in
- val out = LetTupleSimplification.removeLetsFromLetValues(in)
- assert(out === exp)
- }
-
- test("TestElimination") {ctx =>
- val exprs = Seq(Equals(a, b), Equals(c, Plus(a, b)), GreaterEquals(Plus(c, d), zero))
- //println("Exprs: "+exprs)
- val retainVars = Set(d).map(_.id)
- val ctrs = exprs map ConstraintUtil.createConstriant
- val nctrs = apply1PRuleOnDisjunct(ctrs.collect{ case c: LinearConstraint => c }, retainVars, None)
- //println("Constraints after elimination: "+nctrs)
- assert(nctrs.size == 1)
- }
-
- test("TestElimination2") {ctx =>
- val exprs = Seq(Equals(zero, Plus(a, b)), Equals(a, zero), GreaterEquals(Plus(b, c), zero))
- //println("Exprs: "+exprs)
- val retainVars = Set(c).map(_.id)
- val ctrs = exprs map ConstraintUtil.createConstriant
- val nctrs = apply1PRuleOnDisjunct(ctrs.collect{ case c: LinearConstraint => c }, retainVars, None)
- //println("Constraints after elimination: "+nctrs)
- assert(nctrs.size == 1)
- }
-
- def createLeonContext(opts: String*): LeonContext = {
- val reporter = new TestSilentReporter
- Main.processOptions(opts.toList).copy(reporter = reporter, interruptManager = new InterruptManager(reporter))
- }
-
- def scalaExprToTree(scalaExpr: String): Expr = {
- val ctx = createLeonContext()
- val testFilename = toTempFile(s"""
- import leon.annotation._
- object Test { def test() = { $scalaExpr } }""")
- val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
- new leon.utils.PreprocessingPhase
- val (_, program) = beginPipe.run(ctx, testFilename)
- //println("Program: "+program)
- functionByName("test", program).get.body.get
- }
-
- def toTempFile(content: String): List[String] = {
- TemporaryInputPhase.run(createLeonContext(), (List(content), Nil))._2
- }
-}
diff --git a/src/test/scala/inox/unit/purescala/DependencyFinderSuite.scala b/src/test/scala/inox/unit/purescala/DependencyFinderSuite.scala
deleted file mode 100644
index a699d69e5b19e2869e759e505bdba00240cd1773..0000000000000000000000000000000000000000
--- a/src/test/scala/inox/unit/purescala/DependencyFinderSuite.scala
+++ /dev/null
@@ -1,132 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.unit.purescala
-
-import org.scalatest._
-
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.Definitions._
-import leon.purescala.DependencyFinder
-
-class DependencyFinderSuite extends FunSuite with helpers.ExpressionsDSL {
-
- private val fd1 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd1.body = Some(x)
-
- private val fd2 = new FunDef(FreshIdentifier("f2"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd2.body = Some(FunctionInvocation(fd1.typed, List(bi(1))))
-
- private val rec1 = new FunDef(FreshIdentifier("rec1"), Seq(), Seq(ValDef(x.id)), IntegerType)
- rec1.body = Some(FunctionInvocation(rec1.typed, List(x)))
-
- test("Direct fun def dependencies with function invocation in body") {
- val deps = new DependencyFinder
- assert(deps(fd1) === Set())
- assert(deps(fd2) === Set(fd1))
- assert(deps(rec1) === Set(rec1))
- }
-
- test("transitive fun def dependencies with function invocation in body") {
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd.body = Some(FunctionInvocation(fd2.typed, List(bi(1))))
- val deps = new DependencyFinder
- assert(deps(fd) === Set(fd1, fd2))
- assert(deps(fd1) === Set())
- assert(deps(fd2) === Set(fd1))
- }
-
- private val classA = new CaseClassDef(FreshIdentifier("A"), Seq(), None, false)
- private val classAField = FreshIdentifier("x", IntegerType)
- classA.setFields(Seq(ValDef(classAField)))
- private val classB = new CaseClassDef(FreshIdentifier("B"), Seq(), None, false)
- private val classBField = FreshIdentifier("a", classA.typed)
- classB.setFields(Seq(ValDef(classBField)))
-
- test("Direct class def dependencies via fields") {
- val deps = new DependencyFinder
- assert(deps(classB) === Set(classA))
- }
-
- test("Direct fun def dependencies with case class selectors in body") {
- val a = FreshIdentifier("a", classA.typed)
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(a)), classAField.getType)
- fd.body = Some(CaseClassSelector(classA.typed, a.toVariable, classAField))
- val deps = new DependencyFinder
- assert(deps(fd) === Set(classA))
- }
-
- test("Transitive fun def dependencies with case class selectors in body") {
- val b = FreshIdentifier("b", classB.typed)
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(b)), classBField.getType)
- fd.body = Some(CaseClassSelector(classB.typed, b.toVariable, classBField))
- val deps = new DependencyFinder
- assert(deps(fd) === Set(classB, classA))
- }
-
-
- test("Class depends on its invariant") {
- val classC = new CaseClassDef(FreshIdentifier("C"), Seq(), None, false)
- val classCField = FreshIdentifier("x", IntegerType)
- classC.setFields(Seq(ValDef(classCField)))
-
- val thisId = FreshIdentifier("this", classC.typed)
-
- val inv = new FunDef(FreshIdentifier("inv"), Seq(), Seq(ValDef(thisId)), BooleanType)
- inv.body = Some(BooleanLiteral(true))
- classC.setInvariant(inv)
-
- val deps = new DependencyFinder
- assert(deps(classC) === Set(inv, classC))
- }
-
- test("Class depends on invariant of its dependencies") {
- val classC = new CaseClassDef(FreshIdentifier("C"), Seq(), None, false)
- val classCField = FreshIdentifier("x", IntegerType)
- classC.setFields(Seq(ValDef(classCField)))
- val classD = new CaseClassDef(FreshIdentifier("D"), Seq(), None, false)
- val classDField = FreshIdentifier("c", classC.typed)
- classD.setFields(Seq(ValDef(classDField)))
-
- val thisId = FreshIdentifier("this", classC.typed)
-
- val inv = new FunDef(FreshIdentifier("inv"), Seq(), Seq(ValDef(thisId)), BooleanType)
- inv.body = Some(BooleanLiteral(true))
- classC.setInvariant(inv)
-
- val deps = new DependencyFinder
- assert(deps(classD) === Set(inv, classC))
- assert(deps(classC) === Set(inv, classC))
- }
-
- test("Class depends on invariant and transitive deps") {
- val classC = new CaseClassDef(FreshIdentifier("C"), Seq(), None, false)
- val classCField = FreshIdentifier("x", IntegerType)
- classC.setFields(Seq(ValDef(classCField)))
- val classD = new CaseClassDef(FreshIdentifier("D"), Seq(), None, false)
- val classDField = FreshIdentifier("c", classC.typed)
- classD.setFields(Seq(ValDef(classDField)))
-
- val thisId = FreshIdentifier("this", classC.typed)
-
- val inv = new FunDef(FreshIdentifier("inv"), Seq(), Seq(ValDef(thisId)), BooleanType)
- inv.body = Some(FunctionInvocation(fd2.typed, Seq(bi(10))))
- classC.setInvariant(inv)
-
- val deps = new DependencyFinder
- assert(deps(classD) === Set(inv, classC, fd2, fd1))
- }
-
- test("Dependencies of mutually recursive functions") {
- val rec1 = new FunDef(FreshIdentifier("rec1"), Seq(), Seq(ValDef(x.id)), IntegerType)
- val rec2 = new FunDef(FreshIdentifier("rec2"), Seq(), Seq(ValDef(x.id)), IntegerType)
- rec1.body = Some(FunctionInvocation(rec2.typed, List(bi(1))))
- rec2.body = Some(FunctionInvocation(rec1.typed, List(bi(1))))
-
- val deps = new DependencyFinder
- assert(deps(rec1) === Set(rec1, rec2))
- assert(deps(rec2) === Set(rec1, rec2))
- }
-}
diff --git a/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala b/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
index 09f9fc603a5e7d15da443d65caf632bcba781915..390f0d33062c2ad57b0117a91bbfd98f506afc0b 100644
--- a/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
+++ b/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
@@ -1,18 +1,15 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon.unit.solvers
+package inox.unit.solvers
-import leon._
-import leon.test._
-import leon.solvers._
-import leon.solvers.combinators._
+import inox._
+import inox.solvers._
+import inox.solvers.combinators._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
+class SolverPoolSuite extends InoxTestSuite {
+ import inox.trees._
-class SolverPoolSuite extends LeonTestSuite {
-
- private class DummySolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
+ private trait DummySolver extends Solver {
val name = "Dummy"
val description = "dummy"
@@ -27,8 +24,11 @@ class SolverPoolSuite extends LeonTestSuite {
def recoverInterrupt() {}
}
- def sfactory(implicit ctx: LeonContext): SolverFactory[Solver] = {
- SolverFactory("dummy", () => new DummySolver(ctx.toSctx, Program.empty))
+ def sfactory(implicit ctx: InoxContext): SolverFactory { val program: InoxProgram } = {
+ val p = InoxProgram(ctx, new Symbols(Map.empty, Map.empty))
+ SolverFactory.create(p)("dummy", () => new DummySolver {
+ val program: p.type = p
+ })
}
val poolSize = 5;
diff --git a/src/test/scala/inox/unit/synthesis/AlgebraSuite.scala b/src/test/scala/inox/unit/synthesis/AlgebraSuite.scala
deleted file mode 100644
index b185454d9e2ed246a618172acd17bf6d24db2b0a..0000000000000000000000000000000000000000
--- a/src/test/scala/inox/unit/synthesis/AlgebraSuite.scala
+++ /dev/null
@@ -1,204 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.unit.synthesis
-import leon.test._
-
-import leon.synthesis.Algebra._
-
-class AlgebraSuite extends LeonTestSuite {
-
- test("remainder") { ctx =>
- assert(remainder(1,1) === 0)
- assert(remainder(2,2) === 0)
- assert(remainder(2,1) === 0)
- assert(remainder(0,1) === 0)
- assert(remainder(0,4) === 0)
- assert(remainder(1,3) === 1)
- assert(remainder(1,8) === 1)
- assert(remainder(4,2) === 0)
- assert(remainder(17,3) === 2)
- assert(remainder(25,5) === 0)
- assert(remainder(26,5) === 1)
- assert(remainder(29,5) === 4)
-
- assert(remainder(1,-1) === 0)
- assert(remainder(-1,1) === 0)
- assert(remainder(2,-2) === 0)
- assert(remainder(-2,-2) === 0)
- assert(remainder(-2,1) === 0)
- assert(remainder(0,-1) === 0)
- assert(remainder(1,-2) === 1)
- assert(remainder(-1,2) === 1)
- assert(remainder(-1,3) === 2)
- assert(remainder(-1,-3) === 2)
- assert(remainder(1,-3) === 1)
- assert(remainder(17,-3) === 2)
- assert(remainder(-25,5) === 0)
- }
-
- test("divide") { ctx =>
- assert(divide(1,1) === (1, 0))
- assert(divide(2,2) === (1, 0))
- assert(divide(2,1) === (2, 0))
- assert(divide(0,1) === (0, 0))
- assert(divide(0,4) === (0, 0))
- assert(divide(1,3) === (0, 1))
- assert(divide(1,8) === (0, 1))
- assert(divide(4,2) === (2, 0))
- assert(divide(17,3) === (5, 2))
- assert(divide(25,5) === (5, 0))
- assert(divide(26,5) === (5, 1))
- assert(divide(29,5) === (5, 4))
-
- assert(divide(1,-1) === (-1, 0))
- assert(divide(-1,1) === (-1, 0))
- assert(divide(2,-2) === (-1, 0))
- assert(divide(-2,-2) === (1, 0))
- assert(divide(-2,1) === (-2, 0))
- assert(divide(0,-1) === (0, 0))
- assert(divide(1,-2) === (0, 1))
- assert(divide(-1,2) === (-1, 1))
- assert(divide(-1,3) === (-1, 2))
- assert(divide(-1,-3) === (1, 2))
- assert(divide(1,-3) === (0, 1))
- assert(divide(17,-3) === (-5, 2))
- assert(divide(-25,5) === (-5, 0))
- }
-
- test("binary gcd") { ctx =>
- assert(gcd(1,1) === 1)
- assert(gcd(1,3) === 1)
- assert(gcd(3,1) === 1)
- assert(gcd(3,3) === 3)
- assert(gcd(4,3) === 1)
- assert(gcd(5,3) === 1)
- assert(gcd(6,3) === 3)
- assert(gcd(2,12) === 2)
- assert(gcd(4,10) === 2)
- assert(gcd(10,4) === 2)
- assert(gcd(12,8) === 4)
- assert(gcd(23,41) === 1)
- assert(gcd(0,41) === 41)
- assert(gcd(4,0) === 4)
-
- assert(gcd(-4,0) === 4)
- assert(gcd(-23,41) === 1)
- assert(gcd(23,-41) === 1)
- assert(gcd(-23,-41) === 1)
- assert(gcd(2,-12) === 2)
- assert(gcd(-4,10) === 2)
- assert(gcd(-4,-8) === 4)
- }
-
- test("n-ary gcd") { ctx =>
- assert(gcd(1,1,1) === 1)
- assert(gcd(1,3,5) === 1)
- assert(gcd(3,1,2) === 1)
- assert(gcd(3,3,3) === 3)
- assert(gcd(4,3,8,6) === 1)
- assert(gcd(5,3,2) === 1)
- assert(gcd(6,3,9) === 3)
- assert(gcd(6,3,8) === 1)
- assert(gcd(2,12,16,4) === 2)
- assert(gcd(4,10,8,22) === 2)
- assert(gcd(10,4,20) === 2)
- assert(gcd(12,8,4) === 4)
- assert(gcd(12,8,2) === 2)
- assert(gcd(12,8,6) === 2)
- assert(gcd(23,41,11) === 1)
- assert(gcd(2,4,8,12,16,4) === 2)
- assert(gcd(2,4,8,11,16,4) === 1)
- assert(gcd(6,3,8, 0) === 1)
- assert(gcd(2,12, 0,16,4) === 2)
-
- assert(gcd(-12,8,6) === 2)
- assert(gcd(23,-41,11) === 1)
- assert(gcd(23,-41, 0,11) === 1)
- assert(gcd(2,4,-8,-12,16,4) === 2)
- assert(gcd(-2,-4,-8,-11,-16,-4) === 1)
- }
-
- test("seq gcd") { ctx =>
- assert(gcd(Seq(1)) === 1)
- assert(gcd(Seq(4)) === 4)
- assert(gcd(Seq(7)) === 7)
- assert(gcd(Seq(1,1,1)) === 1)
- assert(gcd(Seq(1,3,5)) === 1)
- assert(gcd(Seq(3,1,2)) === 1)
- assert(gcd(Seq(3,3,3)) === 3)
- assert(gcd(Seq(4,3,8,6)) === 1)
- assert(gcd(Seq(5,3,2)) === 1)
- assert(gcd(Seq(6,3,9)) === 3)
- assert(gcd(Seq(6,3,8)) === 1)
- assert(gcd(Seq(2,12,16,4)) === 2)
- assert(gcd(Seq(4,10,8,22)) === 2)
- assert(gcd(Seq(10,4,20)) === 2)
- assert(gcd(Seq(12,8,4)) === 4)
- assert(gcd(Seq(12,8,2)) === 2)
- assert(gcd(Seq(12,8,6)) === 2)
- assert(gcd(Seq(23,41,11)) === 1)
- assert(gcd(Seq(2,4,8,12,16,4)) === 2)
- assert(gcd(Seq(2,4,8,11,16,4)) === 1)
- assert(gcd(Seq(6,3,8, 0)) === 1)
- assert(gcd(Seq(2,12, 0,16,4)) === 2)
-
- assert(gcd(Seq(-1)) === 1)
- assert(gcd(Seq(-7)) === 7)
- assert(gcd(Seq(-12,8,6)) === 2)
- assert(gcd(Seq(23,-41,11)) === 1)
- assert(gcd(Seq(23,-41, 0,11)) === 1)
- assert(gcd(Seq(2,4,-8,-12,16,4)) === 2)
- assert(gcd(Seq(-2,-4,-8,-11,-16,-4)) === 1)
- }
-
- test("binary lcm") { ctx =>
- assert(lcm(1,3) === 3)
- assert(lcm(1,1) === 1)
- assert(lcm(0,1) === 0)
- assert(lcm(2,3) === 6)
- assert(lcm(4,3) === 12)
- assert(lcm(4,6) === 12)
- assert(lcm(8,6) === 24)
- }
- test("n-ary lcm") { ctx =>
- assert(lcm(1,2,3) === 6)
- assert(lcm(1,2,3,4) === 12)
- assert(lcm(5,2,3,4) === 60)
- }
- test("seq lcm") { ctx =>
- assert(lcm(Seq(1,2,3)) === 6)
- assert(lcm(Seq(1,2,3,4)) === 12)
- assert(lcm(Seq(5,2,3,4)) === 60)
- }
-
- def checkExtendedEuclid(a: Int, b: Int) {
- val (x, y) = extendedEuclid(a, b)
- assert(x*a + y*b === gcd(a, b))
- }
-
- test("extendedEuclid") { ctx =>
- checkExtendedEuclid(1, 1)
- checkExtendedEuclid(3, 1)
- checkExtendedEuclid(1, 2)
- checkExtendedEuclid(1, 15)
- checkExtendedEuclid(4, 1)
- checkExtendedEuclid(4, 3)
- checkExtendedEuclid(12, 23)
- checkExtendedEuclid(11, 10)
- checkExtendedEuclid(10, 15)
-
- checkExtendedEuclid(-1, 1)
- checkExtendedEuclid(-1, -1)
- checkExtendedEuclid(3, -1)
- checkExtendedEuclid(-3, -1)
- checkExtendedEuclid(-3, 1)
- checkExtendedEuclid(1, -2)
- checkExtendedEuclid(-1, 2)
- checkExtendedEuclid(-1, -2)
- checkExtendedEuclid(12, -23)
- checkExtendedEuclid(-11, 10)
- checkExtendedEuclid(10, -15)
- }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/scala/inox/unit/synthesis/LinearEquationsSuite.scala b/src/test/scala/inox/unit/synthesis/LinearEquationsSuite.scala
deleted file mode 100644
index da62193665b761c5777ef2ae814c96dcaa0e176d..0000000000000000000000000000000000000000
--- a/src/test/scala/inox/unit/synthesis/LinearEquationsSuite.scala
+++ /dev/null
@@ -1,246 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.unit.synthesis
-import leon.test._
-
-import leon.LeonContext
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.ExprOps._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.evaluators._
-
-import leon.synthesis.LinearEquations._
-
-class LinearEquationsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.ExpressionsDSL {
-
- val aa = FreshIdentifier("aa", IntegerType).toVariable
- val bb = FreshIdentifier("bb", IntegerType).toVariable
-
- //use some random values to check that any vector in the basis is a valid solution to
- //the equation
- def checkVectorSpace(basis: Array[Array[Int]], equation: Array[Int]): Unit =
- checkVectorSpace(basis.map(_.map(i => BigInt(i))), equation.map(i => BigInt(i)))
-
- def checkVectorSpace(basis: Array[Array[BigInt]], equation: Array[BigInt]): Unit = {
- require(basis.length == basis(0).length + 1 && basis.length == equation.length)
- val n = basis(0).length
- val min: BigInt = -5
- val max: BigInt = 5
- val components = Array.fill(n)(min)
- var counter = 0
-
- while(counter < n) {
- val sol = mult(basis, components) //one linear combination of the basis
- assert(eval(sol, equation) === 0)
-
- //next components
- if(components(counter) < max)
- components(counter) += 1
- else {
- while(counter < n && components(counter) >= max) {
- components(counter) = min
- counter += 1
- }
- if(counter < n) {
- components(counter) += 1
- counter = 0
- }
- }
- }
- }
-
- def checkSameExpr(e1: Expr, e2: Expr, pre: Expr, vs: Map[Identifier, Expr] = Map())(implicit ctx: LeonContext): Unit = {
- checkLikelyEq(ctx)(e1, e2, Some(pre), vs)
- }
-
- //val that the sol vector with the term in the equation
- def eval(sol: Array[BigInt], equation: Array[BigInt]): BigInt = {
- require(sol.length == equation.length)
- sol.zip(equation).foldLeft(BigInt(0))((acc, p) => acc + p._1 * p._2)
- }
-
- //multiply the matrix by the vector: [M1 M2 .. Mn] * [v1 .. vn] = v1*M1 + ... + vn*Mn]
- def mult(matrix: Array[Array[BigInt]], vector: Array[BigInt]): Array[BigInt] = {
- require(vector.length == matrix(0).length && vector.length > 0)
- val tmat = matrix.transpose
- var tmp: Array[BigInt] = null
- tmp = mult(vector(0), tmat(0))
- var i = 1
- while(i < vector.length) {
- tmp = add(tmp, mult(vector(i), tmat(i)))
- i += 1
- }
- tmp
- }
-
- def mult(c: BigInt, v: Array[BigInt]): Array[BigInt] = v.map(_ * c)
- def add(v1: Array[BigInt], v2: Array[BigInt]): Array[BigInt] = {
- require(v1.length == v2.length)
- v1.zip(v2).map(p => p._1 + p._2)
- }
-
- test("checkVectorSpace") { implicit ctx =>
- checkVectorSpace(Array(Array(1), Array(2)), Array(-2, 1))
- checkVectorSpace(Array(Array(4, 0), Array(-3, 2), Array(0, -1)), Array(3, 4, 8))
- }
-
-
- test("particularSolution basecase") { implicit ctx =>
- def toExpr(es: Array[Expr]): Expr = {
- val vars: Array[Expr] = Array[Expr](bi(1)) ++ Array[Expr](x, y)
- es.zip(vars).foldLeft[Expr](bi(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
- }
-
- val t1: Expr = Plus(aa, bb)
- val c1: Expr = bi(4)
- val d1: Expr = bi(22)
- val e1: Array[Expr] = Array(t1, c1, d1)
- val (pre1, (w1, w2)) = particularSolution(Set(aa.id, bb.id), t1, c1, d1)
- checkSameExpr(toExpr(e1), bi(0), pre1, Map(x.id -> w1, y.id -> w2))
-
- val t2: Expr = bi(-1)
- val c2: Expr = bi(1)
- val d2: Expr = bi(-1)
- val e2: Array[Expr] = Array(t2, c2, d2)
- val (pre2, (w3, w4)) = particularSolution(Set(), t2, c2, d2)
- checkSameExpr(toExpr(e2), bi(0), pre2, Map(x.id -> w3, y.id -> w4))
- }
-
- test("particularSolution preprocess") { implicit ctx =>
- def toExpr(es: Array[Expr], vs: Array[Expr]): Expr = {
- val vars: Array[Expr] = Array[Expr](bi(1)) ++ vs
- es.zip(vars).foldLeft[Expr](bi(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
- }
-
- val t1: Expr = Plus(aa, bb)
- val c1: Expr = bi(4)
- val d1: Expr = bi(22)
- val e1: Array[Expr] = Array(t1, c1, d1)
- val (pre1, s1) = particularSolution(Set(aa.id, bb.id), e1.toList)
- checkSameExpr(toExpr(e1, Array(x, y)), bi(0), pre1, Array(x.id, y.id).zip(s1).toMap)
-
- val t2: Expr = Plus(aa, bb)
- val c2: Expr = bi(4)
- val d2: Expr = bi(22)
- val f2: Expr = bi(10)
- val e2: Array[Expr] = Array(t2, c2, d2, f2)
- val (pre2, s2) = particularSolution(Set(aa.id, bb.id), e2.toList)
- checkSameExpr(toExpr(e2, Array(x, y, z)), bi(0), pre2, Array(x.id, y.id, z.id).zip(s2).toMap)
-
- val t3: Expr = Plus(aa, Times(bi(2), bb))
- val c3: Expr = bi(6)
- val d3: Expr = bi(24)
- val f3: Expr = bi(9)
- val e3: Array[Expr] = Array(t3, c3, d3, f3)
- val (pre3, s3) = particularSolution(Set(aa.id, bb.id), e3.toList)
- checkSameExpr(toExpr(e3, Array(x, y, z)), bi(0), pre3, Array(x.id, y.id, z.id).zip(s3).toMap)
-
- val t4: Expr = Plus(aa, bb)
- val c4: Expr = bi(4)
- val e4: Array[Expr] = Array(t4, c4)
- val (pre4, s4) = particularSolution(Set(aa.id, bb.id), e4.toList)
- checkSameExpr(toExpr(e4, Array(x)), bi(0), pre4, Array(x.id).zip(s4).toMap)
- }
-
-
- test("linearSet") { implicit ctx =>
- val as = Set[Identifier]()
-
- val evaluator = new DefaultEvaluator(ctx, Program.empty)
-
- val eq1 = Array[BigInt](3, 4, 8)
- val basis1 = linearSet(evaluator, as, eq1)
- checkVectorSpace(basis1, eq1)
-
- val eq2 = Array[BigInt](1, 2, 3)
- val basis2 = linearSet(evaluator, as, eq2)
- checkVectorSpace(basis2, eq2)
-
- val eq3 = Array[BigInt](1, 1)
- val basis3 = linearSet(evaluator, as, eq3)
- checkVectorSpace(basis3, eq3)
-
- val eq4 = Array[BigInt](1, 1, 2, 7)
- val basis4 = linearSet(evaluator, as, eq4)
- checkVectorSpace(basis4, eq4)
-
- val eq5 = Array[BigInt](1, -1)
- val basis5 = linearSet(evaluator, as, eq5)
- checkVectorSpace(basis5, eq5)
-
- val eq6 = Array[BigInt](1, -6, 3)
- val basis6 = linearSet(evaluator, as, eq6)
- checkVectorSpace(basis6, eq6)
- }
-
-
- def enumerate(nbValues: Int, app: (Array[Int] => Unit)) {
- val min = -5
- val max = 5
- val counters: Array[Int] = (1 to nbValues).map(_ => min).toArray
- var i = 0
-
- while(i < counters.length) {
- app(counters)
- if(counters(i) < max)
- counters(i) += 1
- else {
- while(i < counters.length && counters(i) >= max) {
- counters(i) = min
- i += 1
- }
- if(i < counters.length) {
- counters(i) += 1
- i = 0
- }
- }
- }
-
- }
-
- //TODO: automatic check result
- // and make faster to have into unit tests
- ignore("elimVariable") { implicit ctx =>
- val as = Set[Identifier](aa.id, bb.id)
-
- val evaluator = new DefaultEvaluator(ctx, Program.empty)
-
- def check(t: Expr, c: List[Expr], prec: Expr, witnesses: List[Expr], freshVars: List[Identifier]) {
- enumerate(freshVars.size, (vals: Array[Int]) => {
- val mapping: Map[Expr, Expr] = freshVars.zip(vals.toList).map(t => (Variable(t._1), bi(t._2))).toMap
- val cWithVars: Expr = c.zip(witnesses).foldLeft[Expr](bi(0)){ case (acc, (coef, wit)) => Plus(acc, Times(coef, replace(mapping, wit))) }
- checkSameExpr(Plus(t, cWithVars), bi(0), prec)
- })
- }
-
- val t1 = Minus(Times(bi(2), aa), bb)
- val c1 = List(bi(3), bi(4), bi(8))
- val (pre1, wit1, f1) = elimVariable(evaluator, as, t1::c1)
- check(t1, c1, pre1, wit1, f1)
-
- val t2 = Plus(Plus(bi(0), bi(2)), Times(bi(-1), bi(3)))
- val c2 = List(bi(1), bi(-1))
- val (pre2, wit2, f2) = elimVariable(evaluator, Set(), t2::c2)
- check(t2, c2, pre2, wit2, f2)
-
-
- val t3 = Minus(Times(bi(2), aa), bi(3))
- val c3 = List(bi(2))
- val (pre3, wit3, f3) = elimVariable(evaluator, Set(aa.id), t3::c3)
- check(t3, c3, pre3, wit3, f3)
-
- val t4 = Times(bi(2), aa)
- val c4 = List(bi(2), bi(4))
- val (pre4, wit4, f4) = elimVariable(evaluator, Set(aa.id), t4::c4)
- check(t4, c4, pre4, wit4, f4)
-
- val t5 = Minus(aa, bb)
- val c5 = List(bi(-60), bi(-3600))
- val (pre5, wit5, f5) = elimVariable(evaluator, Set(aa.id, bb.id), t5::c5)
- check(t5, c5, pre5, wit5, f5)
-
- }
-
-}
diff --git a/src/test/scala/inox/unit/purescala/DefinitionTransformerSuite.scala b/src/test/scala/inox/unit/trees/DefinitionTransformerSuite.scala
similarity index 100%
rename from src/test/scala/inox/unit/purescala/DefinitionTransformerSuite.scala
rename to src/test/scala/inox/unit/trees/DefinitionTransformerSuite.scala
diff --git a/src/test/scala/inox/unit/purescala/ExprOpsSuite.scala b/src/test/scala/inox/unit/trees/ExprOpsSuite.scala
similarity index 59%
rename from src/test/scala/inox/unit/purescala/ExprOpsSuite.scala
rename to src/test/scala/inox/unit/trees/ExprOpsSuite.scala
index 8d40aa5ce6672fe8fa6bb2e001ecb8797da68272..0755370e2c2d5ee7f6f9cac30436c27c112ef6ff 100644
--- a/src/test/scala/inox/unit/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/inox/unit/trees/ExprOpsSuite.scala
@@ -1,26 +1,33 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon.unit.purescala
+package inox.unit.trees
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.TypeOps.isSubtypeOf
-import leon.purescala.Definitions._
-import leon.purescala.ExprOps._
+import inox._
-class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.ExpressionsDSL {
+class ExprOpsSuite extends InoxTestSuite {
+ import inox.trees._
+ import inox.trees.exprOps._
private def foldConcatNames(e: Expr, subNames: Seq[String]): String = e match {
- case Variable(id) => subNames.mkString + id.name
+ case Variable(id, _) => subNames.mkString + id.name
case _ => subNames.mkString
}
+
private def foldCountVariables(e: Expr, subCounts: Seq[Int]): Int = e match {
- case Variable(_) => subCounts.sum + 1
+ case Variable(_, _) => subCounts.sum + 1
case _ => subCounts.sum
}
+ val a = Variable(FreshIdentifier("a"), Int32Type)
+ val b = Variable(FreshIdentifier("b"), Int32Type)
+
+ val x = Variable(FreshIdentifier("x"), IntegerType)
+ val y = Variable(FreshIdentifier("y"), IntegerType)
+
+ val p = Variable(FreshIdentifier("p"), BooleanType)
+ val q = Variable(FreshIdentifier("q"), BooleanType)
+ val r = Variable(FreshIdentifier("r"), BooleanType)
+
test("foldRight works on single variable expression") { ctx =>
assert(fold(foldConcatNames)(x) === x.id.name)
assert(fold(foldConcatNames)(y) === y.id.name)
@@ -64,7 +71,7 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
var names: List[String] = List()
preTraversal({
- case Variable(id) => names ::= id.name
+ case Variable(id, _) => names ::= id.name
case _ => ()
})(x)
assert(names === List(x.id.name))
@@ -84,7 +91,7 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
test("preTraversal visits children from left to right") { ctx =>
var names: List[String] = List()
preTraversal({
- case Variable(id) => names ::= id.name
+ case Variable(id, _) => names ::= id.name
case _ => ()
})(And(List(p, q, r)))
assert(names === List(r.id.name, q.id.name, p.id.name))
@@ -113,7 +120,7 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
var names: List[String] = List()
postTraversal({
- case Variable(id) => names ::= id.name
+ case Variable(id, _) => names ::= id.name
case _ => ()
})(x)
assert(names === List(x.id.name))
@@ -133,7 +140,7 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
test("postTraversal visits children from left to right") { ctx =>
var names: List[String] = List()
postTraversal({
- case Variable(id) => names ::= id.name
+ case Variable(id, _) => names ::= id.name
case _ => ()
})(And(List(p, q, r)))
assert(names === List(r.id.name, q.id.name, p.id.name))
@@ -168,40 +175,29 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
case e => (None, e)
}
+ def checkEq(ctx: InoxContext)(e1: Expr, e2: Expr): Unit = {
+ val e = evaluators.RecursiveEvaluator.default(InoxProgram(ctx, new Symbols(Map.empty, Map.empty)))
+ val r1 = e.eval(e1)
+ val r2 = e.eval(e2)
-
- test("simplifyArithmetic") { ctx =>
- val e1 = Plus(bi(3), bi(2))
- checkLikelyEq(ctx)(e1, simplifyArithmetic(e1))
- val e2 = Plus(x, Plus(bi(3), bi(2)))
- checkLikelyEq(ctx)(e2, simplifyArithmetic(e2))
-
- val e3 = Minus(bi(3), bi(2))
- checkLikelyEq(ctx)(e3, simplifyArithmetic(e3))
- val e4 = Plus(x, Minus(bi(3), bi(2)))
- checkLikelyEq(ctx)(e4, simplifyArithmetic(e4))
- val e5 = Plus(x, Minus(x, bi(2)))
- checkLikelyEq(ctx)(e5, simplifyArithmetic(e5))
-
- val e6 = Times(bi(9), Plus(Division(x, bi(3)), Division(x, bi(6))))
- checkLikelyEq(ctx)(e6, simplifyArithmetic(e6))
+ assert(r1 === r2, s"'$e1' != '$e2' ('$r1' != '$r2')")
}
- test("expandAndSimplifyArithmetic") { ctx =>
- val e1 = Plus(bi(3), bi(2))
- checkLikelyEq(ctx)(e1, expandAndSimplifyArithmetic(e1))
- val e2 = Plus(x, Plus(bi(3), bi(2)))
- checkLikelyEq(ctx)(e2, expandAndSimplifyArithmetic(e2))
-
- val e3 = Minus(bi(3), bi(2))
- checkLikelyEq(ctx)(e3, expandAndSimplifyArithmetic(e3))
- val e4 = Plus(x, Minus(bi(3), bi(2)))
- checkLikelyEq(ctx)(e4, expandAndSimplifyArithmetic(e4))
- val e5 = Plus(x, Minus(x, bi(2)))
- checkLikelyEq(ctx)(e5, expandAndSimplifyArithmetic(e5))
-
- val e6 = Times(bi(9), Plus(Division(x, bi(3)), Division(x, bi(6))))
- checkLikelyEq(ctx)(e6, expandAndSimplifyArithmetic(e6))
+ test("simplifyArithmetic") { ctx =>
+ val e1 = Plus(IntegerLiteral(3), IntegerLiteral(2))
+ checkEq(ctx)(e1, simplifyArithmetic(e1))
+ val e2 = Plus(x, Plus(IntegerLiteral(3), IntegerLiteral(2)))
+ checkEq(ctx)(e2, simplifyArithmetic(e2))
+
+ val e3 = Minus(IntegerLiteral(3), IntegerLiteral(2))
+ checkEq(ctx)(e3, simplifyArithmetic(e3))
+ val e4 = Plus(x, Minus(IntegerLiteral(3), IntegerLiteral(2)))
+ checkEq(ctx)(e4, simplifyArithmetic(e4))
+ val e5 = Plus(x, Minus(x, IntegerLiteral(2)))
+ checkEq(ctx)(e5, simplifyArithmetic(e5))
+
+ val e6 = Times(IntegerLiteral(9), Plus(Division(x, IntegerLiteral(3)), Division(x, IntegerLiteral(6))))
+ checkEq(ctx)(e6, simplifyArithmetic(e6))
}
test("extractEquals") { ctx =>
@@ -233,10 +229,10 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
}
test("pre and post traversal") { ctx =>
- val expr = Plus(bi(1), Minus(bi(2), bi(3)))
+ val expr = Plus(IntegerLiteral(1), Minus(IntegerLiteral(2), IntegerLiteral(3)))
var res = ""
def f(e: Expr): Unit = e match {
- case InfiniteIntegerLiteral(i) => res += i
+ case IntegerLiteral(i) => res += i
case _ : Plus => res += "P"
case _ : Minus => res += "M"
}
@@ -250,22 +246,25 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
}
test("pre- and postMap") { ctx =>
- val expr = Plus(bi(1), Minus(bi(2), bi(3)))
+ val expr = Plus(IntegerLiteral(1), Minus(IntegerLiteral(2), IntegerLiteral(3)))
def op(e : Expr ) = e match {
- case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => Some(bi(2))
- case InfiniteIntegerLiteral(one) if one == BigInt(1) => Some(bi(2))
- case InfiniteIntegerLiteral(two) if two == BigInt(2) => Some(bi(42))
+ case Minus(IntegerLiteral(two), e2) if two == BigInt(2) => Some(IntegerLiteral(2))
+ case IntegerLiteral(one) if one == BigInt(1) => Some(IntegerLiteral(2))
+ case IntegerLiteral(two) if two == BigInt(2) => Some(IntegerLiteral(42))
case _ => None
}
- assert( preMap(op, false)(expr) == Plus(bi(2), bi(2)) )
- assert( preMap(op, true )(expr) == Plus(bi(42), bi(42)) )
- assert( postMap(op, false)(expr) == Plus(bi(2), Minus(bi(42), bi(3))) )
- assert( postMap(op, true)(expr) == Plus(bi(42), Minus(bi(42), bi(3))) )
+ assert( preMap(op, false)(expr) == Plus(IntegerLiteral(2), IntegerLiteral(2)) )
+ assert( preMap(op, true )(expr) == Plus(IntegerLiteral(42), IntegerLiteral(42)) )
+ assert( postMap(op, false)(expr) == Plus(IntegerLiteral(2), Minus(IntegerLiteral(42), IntegerLiteral(3))) )
+ assert( postMap(op, true)(expr) == Plus(IntegerLiteral(42), Minus(IntegerLiteral(42), IntegerLiteral(3))) )
}
test("simplestValue") { ctx =>
+ val symbols = new Symbols(Map.empty, Map.empty)
+ import symbols._
+
val types = Seq(BooleanType,
Int32Type,
IntegerType,
@@ -273,6 +272,7 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
TupleType(Seq(BooleanType, BooleanType)),
MapType(Int32Type, BooleanType))
+
for (t <- types) {
val v = simplestValue(t)
assert(isSubtypeOf(v.getType, t), "SimplestValue of "+t+": "+v+":"+v.getType)
@@ -281,42 +281,44 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
}
test("preMapWithContext") { ctx =>
- val expr = Plus(bi(1), Minus(bi(2), bi(3)))
+ val expr = Plus(IntegerLiteral(1), Minus(IntegerLiteral(2), IntegerLiteral(3)))
def op(e : Expr, set: Set[Int]): (Option[Expr], Set[Int]) = e match {
- case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => (Some(bi(2)), set)
- case InfiniteIntegerLiteral(one) if one == BigInt(1) => (Some(bi(2)), set)
- case InfiniteIntegerLiteral(two) if two == BigInt(2) => (Some(bi(42)), set)
+ case Minus(IntegerLiteral(two), e2) if two == BigInt(2) => (Some(IntegerLiteral(2)), set)
+ case IntegerLiteral(one) if one == BigInt(1) => (Some(IntegerLiteral(2)), set)
+ case IntegerLiteral(two) if two == BigInt(2) => (Some(IntegerLiteral(42)), set)
case _ => (None, set)
}
- assert(preMapWithContext(op, false)(expr, Set()) === Plus(bi(2), bi(2)))
- assert(preMapWithContext(op, true)(expr, Set()) === Plus(bi(42), bi(42)))
+ assert(preMapWithContext(op, false)(expr, Set()) === Plus(IntegerLiteral(2), IntegerLiteral(2)))
+ assert(preMapWithContext(op, true)(expr, Set()) === Plus(IntegerLiteral(42), IntegerLiteral(42)))
- val expr2 = Let(x.id, bi(1), Let(y.id, bi(2), Plus(x, y)))
- def op2(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
- case Let(id, InfiniteIntegerLiteral(v), body) => (None, bindings + (id -> v))
- case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ val expr2 = Let(x.toVal, IntegerLiteral(1), Let(y.toVal, IntegerLiteral(2), Plus(x, y)))
+ def op2(e: Expr, bindings: Map[Variable, BigInt]): (Option[Expr], Map[Variable, BigInt]) = e match {
+ case Let(vd, IntegerLiteral(v), body) => (None, bindings + (vd.toVariable -> v))
+ case v: Variable => (bindings.get(v).map(value => IntegerLiteral(value)), bindings)
case _ => (None, bindings)
}
- assert(preMapWithContext(op2, false)(expr2, Map()) === Let(x.id, bi(1), Let(y.id, bi(2), Plus(bi(1), bi(2)))))
+ assert(preMapWithContext(op2, false)(expr2, Map()) === Let(
+ x.toVal, IntegerLiteral(1), Let(y.toVal, IntegerLiteral(2), Plus(IntegerLiteral(1), IntegerLiteral(2)))))
- def op3(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
- case Let(id, InfiniteIntegerLiteral(v), body) => (Some(body), bindings + (id -> v))
- case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ def op3(e: Expr, bindings: Map[Variable, BigInt]): (Option[Expr], Map[Variable, BigInt]) = e match {
+ case Let(vd, IntegerLiteral(v), body) => (Some(body), bindings + (vd.toVariable -> v))
+ case v: Variable => (bindings.get(v).map(v => IntegerLiteral(v)), bindings)
case _ => (None, bindings)
}
- assert(preMapWithContext(op3, true)(expr2, Map()) === Plus(bi(1), bi(2)))
+ assert(preMapWithContext(op3, true)(expr2, Map()) === Plus(IntegerLiteral(1), IntegerLiteral(2)))
- val expr4 = Plus(Let(y.id, bi(2), y),
- Let(y.id, bi(4), y))
- def op4(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
- case Let(id, InfiniteIntegerLiteral(v), body) => (Some(body), if(bindings.contains(id)) bindings else (bindings + (id -> v)))
- case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ val expr4 = Plus(Let(y.toVal, IntegerLiteral(2), y),
+ Let(y.toVal, IntegerLiteral(4), y))
+ def op4(e: Expr, bindings: Map[Variable, BigInt]): (Option[Expr], Map[Variable, BigInt]) = e match {
+ case Let(vd, IntegerLiteral(v), body) =>
+ (Some(body), if (bindings.contains(vd.toVariable)) bindings else (bindings + (vd.toVariable -> v)))
+ case v: Variable => (bindings.get(v).map(v => IntegerLiteral(v)), bindings)
case _ => (None, bindings)
}
- assert(preMapWithContext(op4, true)(expr4, Map()) === Plus(bi(2), bi(4)))
+ assert(preMapWithContext(op4, true)(expr4, Map()) === Plus(IntegerLiteral(2), IntegerLiteral(4)))
}
}
diff --git a/src/test/scala/inox/unit/purescala/ExtractorsSuite.scala b/src/test/scala/inox/unit/trees/ExtractorsSuite.scala
similarity index 100%
rename from src/test/scala/inox/unit/purescala/ExtractorsSuite.scala
rename to src/test/scala/inox/unit/trees/ExtractorsSuite.scala
diff --git a/src/test/scala/inox/unit/purescala/SimplifyLetsSuite.scala b/src/test/scala/inox/unit/trees/SimplifyLetsSuite.scala
similarity index 100%
rename from src/test/scala/inox/unit/purescala/SimplifyLetsSuite.scala
rename to src/test/scala/inox/unit/trees/SimplifyLetsSuite.scala
diff --git a/src/test/scala/inox/unit/purescala/TreeNormalizationsSuite.scala b/src/test/scala/inox/unit/trees/TreeNormalizationsSuite.scala
similarity index 100%
rename from src/test/scala/inox/unit/purescala/TreeNormalizationsSuite.scala
rename to src/test/scala/inox/unit/trees/TreeNormalizationsSuite.scala
diff --git a/src/test/scala/inox/unit/purescala/TreeTestsSuite.scala b/src/test/scala/inox/unit/trees/TreeTestsSuite.scala
similarity index 100%
rename from src/test/scala/inox/unit/purescala/TreeTestsSuite.scala
rename to src/test/scala/inox/unit/trees/TreeTestsSuite.scala
diff --git a/src/test/scala/inox/unit/purescala/TypeOpsSuite.scala b/src/test/scala/inox/unit/trees/TypeOpsSuite.scala
similarity index 100%
rename from src/test/scala/inox/unit/purescala/TypeOpsSuite.scala
rename to src/test/scala/inox/unit/trees/TypeOpsSuite.scala
diff --git a/src/test/scala/inox/unit/utils/FunctionClosureSuite.scala b/src/test/scala/inox/unit/utils/FunctionClosureSuite.scala
deleted file mode 100644
index 54f7844d5838b6431614dcf278df0f75e83bd446..0000000000000000000000000000000000000000
--- a/src/test/scala/inox/unit/utils/FunctionClosureSuite.scala
+++ /dev/null
@@ -1,299 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package unit.utils
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.ExprOps._
-import purescala.Expressions._
-import purescala.FunctionClosure
-import purescala.Types._
-import test._
-import org.scalatest._
-
-class FunctionClosureSuite extends FunSuite with helpers.ExpressionsDSL {
-
- val fd1 = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd1.body = Some(x)
-
- test("close does not modify a function without nested functions") {
- val cfd1 = FunctionClosure.close(fd1)
- assert(cfd1.size === 1)
- assert(fd1 === cfd1.head)
- assert(fd1.body === cfd1.head.body)
- }
-
- test("close does not capture param from parent if not needed") {
- val nested = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested.body = Some(y)
-
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd.body = Some(LetDef(Seq(nested), x))
-
- val cfds = FunctionClosure.close(fd)
- assert(cfds.size === 2)
-
- cfds.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd.returnType)
- assert(cfd.params.size === fd.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested.returnType)
- assert(cfd.params.size === nested.params.size)
- assert(freeVars(cfd).isEmpty)
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
-
-
- val nested2 = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested2.body = Some(y)
-
- val fd2 = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd2.body = Some(Let(z.id, Plus(x, bi(1)), LetDef(Seq(nested2), x)))
-
- val cfds2 = FunctionClosure.close(fd2)
- assert(cfds2.size === 2)
-
- cfds2.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd2.returnType)
- assert(cfd.params.size === fd2.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested2.returnType)
- assert(cfd.params.size === nested2.params.size)
- assert(freeVars(cfd).isEmpty)
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
- }
-
- test("close does not capture enclosing require if not needed") {
- val nested = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested.body = Some(y)
-
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd.body = Some(Require(GreaterEquals(x, bi(0)), Let(z.id, Plus(x, bi(1)), LetDef(Seq(nested), x))))
-
- val cfds = FunctionClosure.close(fd)
- assert(cfds.size === 2)
-
- cfds.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd.returnType)
- assert(cfd.params.size === fd.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested.returnType)
- assert(cfd.params.size === nested.params.size)
- assert(freeVars(cfd).isEmpty)
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
-
-
- val deeplyNested2 = new FunDef(FreshIdentifier("deeplyNested"), Seq(), Seq(ValDef(z.id)), IntegerType)
- deeplyNested2.body = Some(Require(GreaterEquals(x, bi(0)), z))
-
- val nested2 = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested2.body = Some(LetDef(Seq(deeplyNested2), FunctionInvocation(deeplyNested2.typed, Seq(y))))
-
- val fd2 = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd2.body = Some(Require(GreaterEquals(x, bi(0)),
- LetDef(Seq(nested2), FunctionInvocation(nested2.typed, Seq(x)))))
-
- val cfds2 = FunctionClosure.close(fd2)
- assert(cfds2.size === 3)
-
- cfds2.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd2.returnType)
- assert(cfd.params.size === fd2.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested2.returnType)
- assert(cfd.params.size === 2)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "deeplyNested") {
- assert(cfd.returnType === deeplyNested2.returnType)
- assert(cfd.params.size === 2)
- assert(freeVars(cfd).isEmpty)
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
- }
-
- test("close captures enclosing require if needed") {
- val nested = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested.body = Some(Plus(x, y))
-
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd.body = Some(Require(GreaterEquals(x, bi(0)), LetDef(Seq(nested), x)))
-
- val cfds = FunctionClosure.close(fd)
- assert(cfds.size === 2)
-
- cfds.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd.returnType)
- assert(cfd.params.size === fd.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested.returnType)
- assert(cfd.params.size === 2)
- assert(freeVars(cfd).isEmpty)
- assert(cfd.precondition != None)
- //next assert is assuming that the function closures always adds paramters at the end of the parameter list
- cfd.precondition.foreach(pre => assert(pre == GreaterEquals(cfd.params.last.toVariable, bi(0))))
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
- }
-
- test("close captures transitive dependencies within path") {
- val x2 = FreshIdentifier("x2", IntegerType).toVariable
- val x3 = FreshIdentifier("x3", IntegerType).toVariable
-
- val nested = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested.body = Some(Plus(y, x3))
-
-
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd.body = Some(
- Let(x2.id, Plus(x, bi(1)),
- Let(x3.id, Plus(x2, bi(1)),
- LetDef(Seq(nested), x)))
- )
-
- val cfds = FunctionClosure.close(fd)
- assert(cfds.size === 2)
-
- cfds.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd.returnType)
- assert(cfd.params.size === fd.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested.returnType)
- assert(cfd.params.size === 2)
- assert(freeVars(cfd).isEmpty)
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
- }
-
- test("close captures transitive dependencies within path but not too many") {
- val x2 = FreshIdentifier("x2", IntegerType).toVariable
- val x3 = FreshIdentifier("x3", IntegerType).toVariable
- val x4 = FreshIdentifier("x4", IntegerType).toVariable
-
- val nested = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested.body = Some(Plus(y, x4))
-
-
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id), ValDef(z.id)), IntegerType)
- fd.body = Some(
- Let(x2.id, Plus(x, bi(1)),
- Let(x3.id, Plus(z, bi(1)),
- Let(x4.id, Plus(x2, bi(1)),
- LetDef(Seq(nested), x))))
- )
-
- val cfds = FunctionClosure.close(fd)
- assert(cfds.size === 2)
-
- cfds.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd.returnType)
- assert(cfd.params.size === fd.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested.returnType)
- assert(cfd.params.size === 2)
- assert(freeVars(cfd).isEmpty)
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
- }
-
- test("close captures enclosing require of callee functions") {
- val callee = new FunDef(FreshIdentifier("callee"), Seq(), Seq(), IntegerType)
- callee.body = Some(x)
-
- val caller = new FunDef(FreshIdentifier("caller"), Seq(), Seq(), IntegerType)
- caller.body = Some(FunctionInvocation(callee.typed, Seq()))
-
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd.body = Some(Require(GreaterEquals(x, bi(0)), LetDef(Seq(callee, caller), x)))
-
- val cfds = FunctionClosure.close(fd)
- assert(cfds.size === 3)
-
- cfds.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd.returnType)
- assert(cfd.params.size === fd.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "callee") {
- assert(cfd.returnType === callee.returnType)
- assert(cfd.params.size === 1)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "caller") {
- assert(cfd.returnType === caller.returnType)
- assert(cfd.params.size === 1)
- assert(freeVars(cfd).isEmpty)
- assert(cfd.precondition != None)
- //next assert is assuming that the function closures always adds paramters at the end of the parameter list
- cfd.precondition.foreach(pre => assert(pre == GreaterEquals(cfd.params.last.toVariable, bi(0))))
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
-
-
- val deeplyNested2 = new FunDef(FreshIdentifier("deeplyNested"), Seq(), Seq(ValDef(z.id)), IntegerType)
- deeplyNested2.body = Some(Require(GreaterEquals(x, bi(0)), z))
-
- val nested2 = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
- nested2.body = Some(LetDef(Seq(deeplyNested2), FunctionInvocation(deeplyNested2.typed, Seq(y))))
-
- val fd2 = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd2.body = Some(Require(GreaterEquals(x, bi(0)),
- LetDef(Seq(nested2), FunctionInvocation(nested2.typed, Seq(x)))))
-
- val cfds2 = FunctionClosure.close(fd2)
- assert(cfds2.size === 3)
-
- cfds2.foreach(cfd => {
- if(cfd.id.name == "f") {
- assert(cfd.returnType === fd2.returnType)
- assert(cfd.params.size === fd2.params.size)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "nested") {
- assert(cfd.returnType === nested2.returnType)
- assert(cfd.params.size === 2)
- assert(freeVars(cfd).isEmpty)
- } else if(cfd.id.name == "deeplyNested") {
- assert(cfd.returnType === deeplyNested2.returnType)
- assert(cfd.params.size === 2)
- assert(freeVars(cfd).isEmpty)
- } else {
- fail("Unexpected fun def: " + cfd)
- }
- })
- }
-
-
- private def freeVars(fd: FunDef): Set[Identifier] = variablesOf(fd.fullBody) -- fd.paramIds
-
-}
diff --git a/src/test/scala/inox/unit/xlang/EffectsAnalysisSuite.scala b/src/test/scala/inox/unit/xlang/EffectsAnalysisSuite.scala
deleted file mode 100644
index b8d8442193cd11e6ba1162d85b691bed4ec358f2..0000000000000000000000000000000000000000
--- a/src/test/scala/inox/unit/xlang/EffectsAnalysisSuite.scala
+++ /dev/null
@@ -1,157 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.unit.xlang
-
-import org.scalatest._
-
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.TypeOps.isSubtypeOf
-import leon.purescala.Definitions._
-import leon.xlang.EffectsAnalysis
-import leon.xlang.Expressions._
-import leon.xlang.ExprOps._
-
-class EffectsAnalysisSuite extends FunSuite with helpers.ExpressionsDSL {
-
- private val fd1 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd1.body = Some(x)
-
- private val fd2 = new FunDef(FreshIdentifier("f2"), Seq(), Seq(ValDef(x.id)), IntegerType)
- fd2.body = Some(FunctionInvocation(fd1.typed, List(bi(1))))
-
- private val rec1 = new FunDef(FreshIdentifier("rec1"), Seq(), Seq(ValDef(x.id)), IntegerType)
- rec1.body = Some(FunctionInvocation(rec1.typed, List(x)))
-
- def simplePgm(defs: List[Definition]): Program =
- Program(List(UnitDef(FreshIdentifier("pgm"),
- List("leon", "test"),
- Seq(),
- Seq(ModuleDef(
- FreshIdentifier("Test"),
- defs,
- true
- )),
- true)))
-
- test("Pure functions have no effects") {
- val effects = new EffectsAnalysis
- assert(effects(fd1) === Set())
- assert(effects(fd2) === Set())
- assert(effects(rec1) === Set())
- }
-
-
- private val classA = new CaseClassDef(FreshIdentifier("A"), Seq(), None, false)
- private val classAField = FreshIdentifier("x", IntegerType)
- classA.setFields(Seq(ValDef(classAField).setIsVar(true)))
- private val classAInstanceId = FreshIdentifier("a", classA.typed)
- private val classAInstance = classAInstanceId.toVariable
-
- private val mfd1 = new FunDef(FreshIdentifier("mf1"), Seq(), Seq(ValDef(classAInstanceId)), UnitType)
- mfd1.body = Some(FieldAssignment(classAInstance, classAField, bi(15)))
-
- test("Simple function that mutates its param has an effect") {
- val effects = new EffectsAnalysis
- assert(effects(mfd1) === Set(0))
- assert(effects(fd1) === Set())
- }
-
- test("Function that with immutable param has right effect") {
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id), ValDef(classAInstanceId)), UnitType)
- fd.body = Some(FieldAssignment(classAInstance, classAField, bi(15)))
-
- val effects = new EffectsAnalysis
- assert(effects(fd) === Set(1))
- }
-
- test("Function that takes a mutable param but does not mutate it has no effect") {
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(classAInstanceId)), UnitType)
- fd.body = Some(UnitLiteral())
-
- val effects = new EffectsAnalysis
- assert(effects(fd) === Set())
- }
-
-
- test("Function that mutates param via transitive call has effects") {
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(classAInstanceId)), UnitType)
- fd.body = Some(FunctionInvocation(mfd1.typed, Seq(classAInstance)))
-
- val effects = new EffectsAnalysis
- assert(effects(fd) === Set(0))
- assert(effects(mfd1) === Set(0))
- assert(effects(fd1) === Set())
- }
- test("Function that mutates param via multiple transitive call has effects") {
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(classAInstanceId)), UnitType)
- fd.body = Some(FunctionInvocation(mfd1.typed, Seq(classAInstance)))
- val nfd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(classAInstanceId)), UnitType)
- nfd.body = Some(FunctionInvocation(fd.typed, Seq(classAInstance)))
-
- val effects = new EffectsAnalysis
- assert(effects(nfd) === Set(0))
- assert(effects(fd) === Set(0))
- assert(effects(mfd1) === Set(0))
- }
-
- private val classB = new CaseClassDef(FreshIdentifier("B"), Seq(), None, false)
- private val classBField = FreshIdentifier("y", IntegerType)
- classB.setFields(Seq(ValDef(classBField).setIsVar(true)))
- private val classBInstanceId = FreshIdentifier("b", classB.typed)
- private val classBInstance = classBInstanceId.toVariable
-
- test("Function that with mutate only one param detects right effect") {
- val fd = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(classBInstanceId), ValDef(classAInstanceId)), UnitType)
- fd.body = Some(FieldAssignment(classAInstance, classAField, bi(15)))
-
- val effects = new EffectsAnalysis
- assert(effects(fd) === Set(1))
- }
-
- test("Mutually recursives functions without effects are pure") {
- val rfd1 = new FunDef(FreshIdentifier("rf1"), Seq(), Seq(ValDef(classAInstanceId), ValDef(classBInstanceId)), UnitType)
- val rfd2 = new FunDef(FreshIdentifier("rf2"), Seq(), Seq(ValDef(classAInstanceId), ValDef(classBInstanceId)), UnitType)
- rfd1.body = Some(FunctionInvocation(rfd2.typed, Seq(classAInstance, classBInstance)))
- rfd2.body = Some(FunctionInvocation(rfd1.typed, Seq(classAInstance, classBInstance)))
-
- val effects = new EffectsAnalysis
- assert(effects(rfd1) === Set())
- assert(effects(rfd2) === Set())
- }
-
- test("Mutually recursives functions with effects are transitively detected") {
- val rfd1 = new FunDef(FreshIdentifier("rf1"), Seq(), Seq(ValDef(classAInstanceId), ValDef(classBInstanceId)), UnitType)
- val rfd2 = new FunDef(FreshIdentifier("rf2"), Seq(), Seq(ValDef(classAInstanceId), ValDef(classBInstanceId)), UnitType)
- rfd1.body = Some(Block(Seq(FieldAssignment(classAInstance, classAField, bi(10))), FunctionInvocation(rfd2.typed, Seq(classAInstance, classBInstance))))
- rfd2.body = Some(FunctionInvocation(rfd1.typed, Seq(classAInstance, classBInstance)))
-
- val effects = new EffectsAnalysis
- assert(effects(rfd1) === Set(0))
- assert(effects(rfd2) === Set(0))
- }
-
- test("Mutually recursives functions with multiple effects are transitively detected") {
- val rfd1 = new FunDef(FreshIdentifier("rf1"), Seq(), Seq(ValDef(classAInstanceId), ValDef(classBInstanceId)), UnitType)
- val rfd2 = new FunDef(FreshIdentifier("rf2"), Seq(), Seq(ValDef(classAInstanceId), ValDef(classBInstanceId)), UnitType)
- rfd1.body = Some(Block(Seq(FieldAssignment(classAInstance, classAField, bi(10))), FunctionInvocation(rfd2.typed, Seq(classAInstance, classBInstance))))
- rfd2.body = Some(Block(Seq(FieldAssignment(classBInstance, classBField, bi(12))), FunctionInvocation(rfd1.typed, Seq(classAInstance, classBInstance))))
-
- val effects = new EffectsAnalysis
- assert(effects(rfd1) === Set(0,1))
- assert(effects(rfd2) === Set(0,1))
- }
-
-
- private val lambdaId = FreshIdentifier("lambda", FunctionType(Seq(classA.typed), UnitType))
- private val mfd2 = new FunDef(FreshIdentifier("mf2"), Seq(), Seq(ValDef(classAInstanceId), ValDef(lambdaId)), UnitType)
- mfd2.body = Some(Application(lambdaId.toVariable, Seq(classAInstance)))
-
-
- test("Function that takes higher-order function applied to a mutable param has effects") {
- val effects = new EffectsAnalysis
- assert(effects(mfd2) === Set(0))
- }
-}
diff --git a/src/test/scala/inox/unit/xlang/ExprOpsSuite.scala b/src/test/scala/inox/unit/xlang/ExprOpsSuite.scala
deleted file mode 100644
index df9b8022582c5922133a262ade700ef9a629f2b5..0000000000000000000000000000000000000000
--- a/src/test/scala/inox/unit/xlang/ExprOpsSuite.scala
+++ /dev/null
@@ -1,52 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.unit.xlang
-
-import org.scalatest._
-
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.TypeOps.isSubtypeOf
-import leon.purescala.Definitions._
-import leon.xlang.Expressions._
-import leon.xlang.ExprOps._
-
-class ExprOpsSuite extends FunSuite with helpers.ExpressionsDSL {
-
- test("flattenBlocks does not change a simple block") {
- assert(flattenBlocks(Block(Seq(y), x)) === Block(Seq(y), x))
- assert(flattenBlocks(Block(Seq(y, z), x)) === Block(Seq(y, z), x))
- }
-
- test("flattenBlocks of a single statement removes the block") {
- assert(flattenBlocks(Block(Seq(), x)) === x)
- assert(flattenBlocks(Block(Seq(), y)) === y)
- }
-
- test("flattenBlocks of a one nested block flatten everything") {
- assert(flattenBlocks(Block(Seq(Block(Seq(y), z)), x)) === Block(Seq(y, z), x))
- assert(flattenBlocks(Block(Seq(y, Block(Seq(), z)), x)) === Block(Seq(y, z), x))
- }
-
- test("flattenBlocks of a several nested blocks flatten everything") {
- assert(flattenBlocks(Block(Seq(Block(Seq(), y), Block(Seq(), z)), x)) === Block(Seq(y, z), x))
- }
-
- test("flattenBlocks of a nested block in last expr should flatten") {
- assert(flattenBlocks(Block(Seq(Block(Seq(), y)), Block(Seq(z), x))) === Block(Seq(y, z), x))
- }
-
- test("flattenBlocks should eliminate intermediate UnitLiteral") {
- assert(flattenBlocks(Block(Seq(UnitLiteral(), y, z), x)) === Block(Seq(y, z), x))
- assert(flattenBlocks(Block(Seq(y, UnitLiteral(), z), x)) === Block(Seq(y, z), x))
- assert(flattenBlocks(Block(Seq(UnitLiteral(), UnitLiteral(), z), x)) === Block(Seq(z), x))
- assert(flattenBlocks(Block(Seq(UnitLiteral()), x)) === x)
- }
-
- test("flattenBlocks should not eliminate trailing UnitLiteral") {
- assert(flattenBlocks(Block(Seq(x), UnitLiteral())) === Block(Seq(x), UnitLiteral()))
- }
-
-}