diff --git a/build.sbt b/build.sbt
index de14da5952368a72ed5f88fd42c10af7599f5b63..4b8234b849d852eaa8db6a7a9073dcb9bd530307 100644
--- a/build.sbt
+++ b/build.sbt
@@ -110,10 +110,16 @@ sourcesInBase in Compile := false
lazy val PerfTest = config("perf") extend(Test)
+lazy val UnitTest = config("unit-test") extend(Test)
+
scalaSource in PerfTest := baseDirectory.value / "src/test/scala/"
+scalaSource in UnitTest := baseDirectory.value / "src/unit-test/scala/"
+
parallelExecution in PerfTest := false
+parallelExecution in UnitTest := true
+
testOptions in (PerfTest, test) := Seq(Tests.Filter(s => s.endsWith("PerfTest")))
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
@@ -124,6 +130,8 @@ lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "6b74
lazy val root = (project in file(".")).
configs(PerfTest).
+ configs(UnitTest).
dependsOn(bonsai, scalaSmtLib).
- settings(inConfig(PerfTest)(Defaults.testSettings): _*)
+ settings(inConfig(PerfTest)(Defaults.testSettings): _*).
+ settings(inConfig(UnitTest)(Defaults.testSettings): _*)
diff --git a/src/unit-test/scala/leon/LeonTestSuite.scala b/src/unit-test/scala/leon/LeonTestSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..050ddf976980986b46084e681f3da06ae8a84d84
--- /dev/null
+++ b/src/unit-test/scala/leon/LeonTestSuite.scala
@@ -0,0 +1,105 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import utils._
+
+import org.scalatest._
+import org.scalatest.exceptions.TestFailedException
+
+trait LeonTestSuite extends FunSuite {
+
+ def createLeonContext(opts: String*): LeonContext = {
+ val reporter = new TestSilentReporter
+
+ Main.processOptions(opts.toList).copy(reporter = reporter, interruptManager = new InterruptManager(reporter))
+ }
+
+ //var testContext: LeonContext = null
+
+ //override def beforeEach() = {
+ // testContext = createLeonContext()
+ // super.beforeEach()
+ //}
+
+ //def testIdentifier(name: String): String = {
+ // def sanitize(s: String) = s.replaceAll("[^0-9a-zA-Z-]", "")
+
+ // sanitize(this.getClass.getName)+"/"+sanitize(name)
+ //}
+
+ //def bookKeepingFile(id: String) = {
+ // import java.io.File
+
+ // val f = new File(System.getProperty("user.dir")+"/.test-history/"+id+".log")
+
+ // f.getParentFile.mkdirs()
+
+ // f
+ //}
+
+ //def getStats(id: String): Statistics = {
+ // val f = bookKeepingFile(id)
+
+ // if (f.canRead) {
+ // Statistics(Source.fromFile(f).getLines().flatMap{ line =>
+ // val l = line.trim
+ // if (l.length > 0) {
+ // Some(line.toLong)
+ // } else {
+ // None
+ // }
+ // }.toList)
+ // } else {
+ // Statistics(Nil)
+ // }
+ //}
+
+ //def storeStats(id: String, stats: Statistics) {
+ // import java.io.FileWriter
+
+ // val f = bookKeepingFile(id)
+
+ // val fw = new FileWriter(f, true)
+ // fw.write(stats.values.head+"\n")
+ // fw.close()
+ //}
+
+ //override implicit val defaultInterruptor = new Interruptor {
+ // def apply(t: Thread) {
+ // testContext.interruptManager.interrupt()
+ // }
+ //}
+
+ //def testWithTimeout(name: String, timeout: Span)(body: => Unit) {
+ // super.test(name) {
+ // val id = testIdentifier(name)
+
+ // val ts = now()
+
+ // failAfter(timeout) {
+ // try {
+ // body
+ // } catch {
+ // case fe: LeonFatalError =>
+ // testContext.reporter match {
+ // case sr: TestSilentReporter =>
+ // sr.lastErrors ++= fe.msg
+ // throw new TestFailedException(sr.lastErrors.mkString("\n"), fe, 5)
+ // }
+ // }
+ // }
+
+ // val total = now()-ts
+
+ // val stats = getStats(id)
+
+ // if (!stats.accountsFor(total)) {
+ // info(Console.YELLOW+"[warning] Test took too long to run: "+total+"ms (avg: "+stats.avg+", stddev: "+stats.stddev+")")
+ // }
+
+ // storeStats(id, stats.withValue(total))
+ // }
+ //}
+
+}
diff --git a/src/unit-test/scala/leon/TestSilentReporter.scala b/src/unit-test/scala/leon/TestSilentReporter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9802995c66f505e0820842898045d4a8fcfc74a9
--- /dev/null
+++ b/src/unit-test/scala/leon/TestSilentReporter.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+class TestSilentReporter extends DefaultReporter(Set()) {
+ var lastErrors: List[String] = Nil
+
+ override def emit(msg: Message): Unit = msg match {
+ case Message(this.ERROR, _, msg) => lastErrors ++= List(msg.toString)
+ case Message(this.FATAL, _, msg) => lastErrors ++= List(msg.toString)
+ case _ =>
+ }
+}
diff --git a/src/unit-test/scala/leon/evaluators/DefaultEvaluatorSuite.scala b/src/unit-test/scala/leon/evaluators/DefaultEvaluatorSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8ac29542fc1a2ee0f78a2bae5bdb9e5eedc47022
--- /dev/null
+++ b/src/unit-test/scala/leon/evaluators/DefaultEvaluatorSuite.scala
@@ -0,0 +1,359 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import leon._
+import leon.evaluators._
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.purescala.Constructors._
+
+class DefaultEvaluatorSuite extends leon.test.LeonTestSuite {
+
+ private implicit lazy val leonContext: LeonContext = createLeonContext()
+ private val emptyProgram = Program.empty
+
+ private val defaultEvaluator = new DefaultEvaluator(leonContext, emptyProgram)
+
+ def expectSuccessful(res: EvaluationResults.Result, expected: Expr): Unit = {
+ res match {
+ case EvaluationResults.Successful(value) => assert(value === expected)
+ case _ => assert(false)
+ }
+ }
+
+ test("eval correctly evaluates literals") {
+ expectSuccessful(defaultEvaluator.eval(BooleanLiteral(true)), BooleanLiteral(true))
+ expectSuccessful(defaultEvaluator.eval(BooleanLiteral(false)), BooleanLiteral(false))
+ expectSuccessful(defaultEvaluator.eval(IntLiteral(0)), IntLiteral(0))
+ expectSuccessful(defaultEvaluator.eval(IntLiteral(42)), IntLiteral(42))
+ expectSuccessful(defaultEvaluator.eval(UnitLiteral()), UnitLiteral())
+ expectSuccessful(defaultEvaluator.eval(InfiniteIntegerLiteral(0)), InfiniteIntegerLiteral(0))
+ expectSuccessful(defaultEvaluator.eval(InfiniteIntegerLiteral(42)), InfiniteIntegerLiteral(42))
+ expectSuccessful(defaultEvaluator.eval(RealLiteral(0)), RealLiteral(0))
+ expectSuccessful(defaultEvaluator.eval(RealLiteral(42)), RealLiteral(42))
+ expectSuccessful(defaultEvaluator.eval(RealLiteral(13.255)), RealLiteral(13.255))
+ }
+
+ test("eval of simple bit vector arithmetic expressions") {
+ expectSuccessful(defaultEvaluator.eval(BVPlus(IntLiteral(3), IntLiteral(5))), IntLiteral(8))
+ expectSuccessful(defaultEvaluator.eval(BVPlus(IntLiteral(0), IntLiteral(5))), IntLiteral(5))
+ expectSuccessful(defaultEvaluator.eval(BVTimes(IntLiteral(3), IntLiteral(3))), IntLiteral(9))
+ }
+
+ test("eval bitwise operations") {
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(3), IntLiteral(1))), IntLiteral(1))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(3), IntLiteral(3))), IntLiteral(3))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(5), IntLiteral(3))), IntLiteral(1))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(5), IntLiteral(4))), IntLiteral(4))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(5), IntLiteral(2))), IntLiteral(0))
+
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(3), IntLiteral(1))), IntLiteral(3))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(3), IntLiteral(3))), IntLiteral(3))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(5), IntLiteral(3))), IntLiteral(7))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(5), IntLiteral(4))), IntLiteral(5))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(5), IntLiteral(2))), IntLiteral(7))
+
+ expectSuccessful(defaultEvaluator.eval(BVXOr(IntLiteral(3), IntLiteral(1))), IntLiteral(2))
+ expectSuccessful(defaultEvaluator.eval(BVXOr(IntLiteral(3), IntLiteral(3))), IntLiteral(0))
+
+ expectSuccessful(defaultEvaluator.eval(BVNot(IntLiteral(1))), IntLiteral(-2))
+
+ expectSuccessful(defaultEvaluator.eval(BVShiftLeft(IntLiteral(3), IntLiteral(1))), IntLiteral(6))
+ expectSuccessful(defaultEvaluator.eval(BVShiftLeft(IntLiteral(4), IntLiteral(2))), IntLiteral(16))
+
+ expectSuccessful(defaultEvaluator.eval(BVLShiftRight(IntLiteral(8), IntLiteral(1))), IntLiteral(4))
+ expectSuccessful(defaultEvaluator.eval(BVAShiftRight(IntLiteral(8), IntLiteral(1))), IntLiteral(4))
+ }
+
+ test("eval of simple arithmetic expressions") {
+ expectSuccessful(
+ defaultEvaluator.eval(Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(5))),
+ InfiniteIntegerLiteral(8))
+ expectSuccessful(
+ defaultEvaluator.eval(Minus(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(2))),
+ InfiniteIntegerLiteral(5))
+ expectSuccessful(
+ defaultEvaluator.eval(UMinus(InfiniteIntegerLiteral(7))),
+ InfiniteIntegerLiteral(-7))
+ expectSuccessful(
+ defaultEvaluator.eval(Times(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(6))
+ }
+
+ test("Eval of division, remainder and modulo semantics for BigInt") {
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(3))
+ expectSuccessful(
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(1))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(-1))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(2))
+
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(-1))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(2))
+
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(1))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(1))
+ }
+
+ test("eval of simple arithmetic comparisons over integers") {
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+ }
+
+
+ test("Eval of division and remainder semantics for bit vectors") {
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(10), IntLiteral(3))),
+ IntLiteral(3))
+ expectSuccessful(
+ defaultEvaluator.eval(BVRemainder(IntLiteral(10), IntLiteral(3))),
+ IntLiteral(1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(-1), IntLiteral(3))),
+ IntLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(BVRemainder(IntLiteral(-1), IntLiteral(3))),
+ IntLiteral(-1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(-1), IntLiteral(-3))),
+ IntLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(BVRemainder(IntLiteral(-1), IntLiteral(-3))),
+ IntLiteral(-1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(1), IntLiteral(-3))),
+ IntLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(BVRemainder(IntLiteral(1), IntLiteral(-3))),
+ IntLiteral(1))
+ }
+
+ test("Eval of simple boolean operations") {
+ expectSuccessful(
+ defaultEvaluator.eval(And(BooleanLiteral(true), BooleanLiteral(true))),
+ BooleanLiteral(true))
+ expectSuccessful(
+ defaultEvaluator.eval(And(BooleanLiteral(true), BooleanLiteral(false))),
+ BooleanLiteral(false))
+ expectSuccessful(
+ defaultEvaluator.eval(And(BooleanLiteral(false), BooleanLiteral(false))),
+ BooleanLiteral(false))
+ expectSuccessful(
+ defaultEvaluator.eval(And(BooleanLiteral(false), BooleanLiteral(true))),
+ BooleanLiteral(false))
+ expectSuccessful(
+ defaultEvaluator.eval(Or(BooleanLiteral(true), BooleanLiteral(true))),
+ BooleanLiteral(true))
+ expectSuccessful(
+ defaultEvaluator.eval(Or(BooleanLiteral(true), BooleanLiteral(false))),
+ BooleanLiteral(true))
+ expectSuccessful(
+ defaultEvaluator.eval(Or(BooleanLiteral(false), BooleanLiteral(false))),
+ BooleanLiteral(false))
+ expectSuccessful(
+ defaultEvaluator.eval(Or(BooleanLiteral(false), BooleanLiteral(true))),
+ BooleanLiteral(true))
+ expectSuccessful(
+ defaultEvaluator.eval(Not(BooleanLiteral(false))),
+ BooleanLiteral(true))
+ expectSuccessful(
+ defaultEvaluator.eval(Not(BooleanLiteral(true))),
+ BooleanLiteral(false))
+ }
+
+ test("eval of simple arithmetic expressions over real") {
+ expectSuccessful(
+ defaultEvaluator.eval(RealPlus(RealLiteral(3), RealLiteral(5))),
+ RealLiteral(8))
+ expectSuccessful(
+ defaultEvaluator.eval(RealMinus(RealLiteral(7), RealLiteral(2))),
+ RealLiteral(5))
+ expectSuccessful(
+ defaultEvaluator.eval(RealUMinus(RealLiteral(7))),
+ RealLiteral(-7))
+ expectSuccessful(
+ defaultEvaluator.eval(RealTimes(RealLiteral(2), RealLiteral(3))),
+ RealLiteral(6))
+
+ expectSuccessful(
+ defaultEvaluator.eval(RealPlus(RealLiteral(2.5), RealLiteral(3.5))),
+ RealLiteral(6))
+ }
+
+ test("eval of simple arithmetic comparisons over real") {
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(RealLiteral(7), RealLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(RealLiteral(7), RealLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(RealLiteral(4), RealLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(RealLiteral(7), RealLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(RealLiteral(7), RealLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(RealLiteral(4), RealLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(RealLiteral(7), RealLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(RealLiteral(7), RealLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(RealLiteral(4), RealLiteral(7))), BooleanLiteral(true)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(RealLiteral(7), RealLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(RealLiteral(7), RealLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(RealLiteral(4), RealLiteral(7))), BooleanLiteral(true)
+ )
+ }
+
+ test("eval simple variable") {
+ val id = FreshIdentifier("id", Int32Type)
+ expectSuccessful(
+ defaultEvaluator.eval(Variable(id), Map(id -> IntLiteral(23))),
+ IntLiteral(23))
+ }
+
+ test("eval with unbound variable should return EvaluatorError") {
+ val id = FreshIdentifier("id", Int32Type)
+ val foo = FreshIdentifier("foo", Int32Type)
+ val res = defaultEvaluator.eval(Variable(id), Map(foo -> IntLiteral(23)))
+ assert(res.isInstanceOf[EvaluationResults.EvaluatorError])
+ }
+
+ test("eval let expression") {
+ val id = FreshIdentifier("id")
+ expectSuccessful(
+ defaultEvaluator.eval(Let(id, IntLiteral(42), Variable(id))),
+ IntLiteral(42))
+ }
+
+
+ test("eval literal array ops") {
+ expectSuccessful(
+ defaultEvaluator.eval(finiteArray(Map[Int,Expr](), Some(IntLiteral(12), IntLiteral(7)), Int32Type)),
+ finiteArray(Map[Int,Expr](), Some(IntLiteral(12), IntLiteral(7)), Int32Type))
+ expectSuccessful(
+ defaultEvaluator.eval(
+ ArrayLength(finiteArray(Map[Int,Expr](), Some(IntLiteral(12), IntLiteral(7)), Int32Type))),
+ IntLiteral(7))
+ expectSuccessful(
+ defaultEvaluator.eval(ArraySelect(
+ finiteArray(Seq(IntLiteral(2), IntLiteral(4), IntLiteral(7))),
+ IntLiteral(1))),
+ IntLiteral(4))
+ expectSuccessful(
+ defaultEvaluator.eval(
+ ArrayUpdated(
+ finiteArray(Seq(IntLiteral(2), IntLiteral(4), IntLiteral(7))),
+ IntLiteral(1),
+ IntLiteral(42))),
+ finiteArray(Seq(IntLiteral(2), IntLiteral(42), IntLiteral(7))))
+ }
+
+ test("eval variable length of array") {
+ val id = FreshIdentifier("id", Int32Type)
+ expectSuccessful(
+ defaultEvaluator.eval(
+ ArrayLength(
+ finiteArray(Map[Int, Expr](), Some(IntLiteral(12), Variable(id)), Int32Type)),
+ Map(id -> IntLiteral(27))),
+ IntLiteral(27))
+ }
+
+ test("eval variable default value of array") {
+ val id = FreshIdentifier("id", Int32Type)
+ expectSuccessful(
+ defaultEvaluator.eval(
+ finiteArray(Map[Int, Expr](), Some(Variable(id), IntLiteral(7)), Int32Type),
+ Map(id -> IntLiteral(27))),
+ finiteArray(Map[Int, Expr](), Some(IntLiteral(27), IntLiteral(7)), Int32Type))
+ }
+
+}
diff --git a/src/unit-test/scala/leon/purescala/LikelyEqSuite.scala b/src/unit-test/scala/leon/purescala/LikelyEqSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..71115fac6993239883da8773f95ba1c09979c7bc
--- /dev/null
+++ b/src/unit-test/scala/leon/purescala/LikelyEqSuite.scala
@@ -0,0 +1,48 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon.test._
+import leon.purescala.Common._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+
+class LikelyEqSuite extends LeonTestSuite with WithLikelyEq {
+ def i(x: Int) = InfiniteIntegerLiteral(x)
+
+ val xId = FreshIdentifier("x", IntegerType)
+ val x = Variable(xId)
+ val yId = FreshIdentifier("y", IntegerType)
+ val y = Variable(yId)
+ val zId = FreshIdentifier("z", IntegerType)
+ val z = Variable(zId)
+
+ test("apply") {
+ assert(LikelyEq(Plus(x, x), Times(i(2), x), Set(xId)))
+ assert(LikelyEq(Plus(x, x), Times(x, i(2)), Set(xId)))
+
+ assert(LikelyEq(Plus(x, y), Plus(y, x), Set(xId, yId)))
+ assert(LikelyEq(Plus(Plus(x, y), y), Plus(x, Times(i(2), y)), Set(xId, yId)))
+
+ def defaultCompare(e1: Expr, e2: Expr) = e1 == e2
+
+ assert(LikelyEq(
+ Plus(i(2), Plus(x, y)),
+ Plus(i(3), Plus(x, z)),
+ Set(xId),
+ BooleanLiteral(true),
+ defaultCompare,
+ Map(yId -> i(2), zId -> i(1)))
+ )
+
+
+ assert(LikelyEq(
+ Plus(x, Times(i(2), Division(y, i(2))))
+ , Plus(x, y)
+ , Set(xId, yId)
+ , Equals(Modulo(y, i(2)), i(0))
+ ))
+
+ }
+
+}
diff --git a/src/unit-test/scala/leon/purescala/TreeNormalizationsSuite.scala b/src/unit-test/scala/leon/purescala/TreeNormalizationsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fc11c8a0911d937e3c81195bbca99490eb31ee39
--- /dev/null
+++ b/src/unit-test/scala/leon/purescala/TreeNormalizationsSuite.scala
@@ -0,0 +1,84 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon.test._
+
+import leon.purescala.Common._
+import leon.purescala.Types._
+import leon.purescala.Expressions._
+import leon.purescala.TreeNormalizations._
+
+class TreeNormalizationsSuite extends LeonTestSuite with WithLikelyEq {
+ def i(x: Int) = InfiniteIntegerLiteral(x)
+
+ val xId = FreshIdentifier("x", IntegerType)
+ val x = Variable(xId)
+ val yId = FreshIdentifier("y", IntegerType)
+ val y = Variable(yId)
+ val xs = Set(xId, yId)
+
+ val aId = FreshIdentifier("a", IntegerType)
+ val a = Variable(aId)
+ val bId = FreshIdentifier("b", IntegerType)
+ val b = Variable(bId)
+ val as = Set(aId, bId)
+
+
+ def checkSameExpr(e1: Expr, e2: Expr, vs: Set[Identifier]) {
+ assert( //this outer assert should not be needed because of the nested one
+ LikelyEq(e1, e2, vs, BooleanLiteral(true), (e1, e2) => {assert(e1 === e2); true})
+ )
+ }
+
+ def toSum(es: Seq[Expr]) = es.reduceLeft(Plus)
+ def coefToSum(es: Array[Expr], vs: Array[Expr]) = es.zip(Array[Expr](InfiniteIntegerLiteral(1)) ++ vs).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
+
+ test("checkSameExpr") {
+ checkSameExpr(Plus(x, y), Plus(y, x), xs)
+ checkSameExpr(Plus(x, x), Times(x, i(2)), xs)
+ checkSameExpr(Plus(x, Plus(x, x)), Times(x, i(3)), xs)
+ }
+
+ test("multiply") {
+ val lhs = Seq(x, i(2))
+ val rhs = Seq(y, i(1))
+ checkSameExpr(Times(toSum(lhs), toSum(rhs)), toSum(multiply(lhs, rhs)), xs)
+ checkSameExpr(Times(toSum(rhs), toSum(lhs)), toSum(multiply(rhs, lhs)), xs)
+
+ val lhs2 = Seq(x, y, i(2))
+ val rhs2 = Seq(y, i(1), Times(i(2), x))
+ checkSameExpr(Times(toSum(lhs2), toSum(rhs2)), toSum(multiply(lhs2, rhs2)), xs)
+ }
+
+ test("expandedForm") {
+ val e1 = Times(Plus(x, i(2)), Plus(y, i(1)))
+ checkSameExpr(toSum(expandedForm(e1)), e1, xs)
+
+ val e2 = Times(Plus(x, Times(i(2), y)), Plus(Plus(x, y), i(1)))
+ checkSameExpr(toSum(expandedForm(e2)), e2, xs)
+
+ val e3 = Minus(Plus(x, Times(i(2), y)), Plus(Plus(x, y), i(1)))
+ checkSameExpr(toSum(expandedForm(e3)), e3, xs)
+
+ val e4 = UMinus(Plus(x, Times(i(2), y)))
+ checkSameExpr(toSum(expandedForm(e4)), e4, xs)
+ }
+
+ test("linearArithmeticForm") {
+ val xsOrder = Array(xId, yId)
+
+ val e1 = Plus(Times(Plus(x, i(2)), i(3)), Times(i(4), y))
+ checkSameExpr(coefToSum(linearArithmeticForm(e1, xsOrder), Array(x, y)), e1, xs)
+
+ val e2 = Plus(Times(Plus(x, i(2)), i(3)), Plus(Plus(a, Times(i(5), b)), Times(i(4), y)))
+ checkSameExpr(coefToSum(linearArithmeticForm(e2, xsOrder), Array(x, y)), e2, xs ++ as)
+
+ val e3 = Minus(Plus(x, i(3)), Plus(y, i(2)))
+ checkSameExpr(coefToSum(linearArithmeticForm(e3, xsOrder), Array(x, y)), e3, xs)
+
+ val e4 = Plus(Plus(i(0), i(2)), Times(i(-1), i(3)))
+ assert(linearArithmeticForm(e4, Array()) === Array(i(-1)))
+
+ }
+}
diff --git a/src/unit-test/scala/leon/purescala/TreeOpsSuite.scala b/src/unit-test/scala/leon/purescala/TreeOpsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b73eec580ce50ed4dbde963b3ddeffe6db50d2d7
--- /dev/null
+++ b/src/unit-test/scala/leon/purescala/TreeOpsSuite.scala
@@ -0,0 +1,152 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon.test._
+import leon.purescala.Common._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
+
+class TreeOpsSuite extends LeonTestSuite with WithLikelyEq {
+
+ test("Path-aware simplifications") {
+ // TODO actually testing something here would be better, sorry
+ // PS
+
+ assert(true)
+ }
+
+ /**
+ * If the formula consist of some top level AND, find a top level
+ * Equals and extract it, return the remaining formula as well
+ */
+ def extractEquals(expr: Expr): (Option[Equals], Expr) = expr match {
+ case And(es) =>
+ // OK now I'm just messing with you.
+ val (r, nes) = es.foldLeft[(Option[Equals],Seq[Expr])]((None, Seq())) {
+ case ((None, nes), eq @ Equals(_,_)) => (Some(eq), nes)
+ case ((o, nes), e) => (o, e +: nes)
+ }
+ (r, And(nes.reverse))
+
+ case e => (None, e)
+ }
+
+
+ def i(x: Int) = InfiniteIntegerLiteral(x)
+
+ val xId = FreshIdentifier("x", IntegerType)
+ val x = Variable(xId)
+ val yId = FreshIdentifier("y", IntegerType)
+ val y = Variable(yId)
+ val xs = Set(xId, yId)
+
+ val aId = FreshIdentifier("a", IntegerType)
+ val a = Variable(aId)
+ val bId = FreshIdentifier("b", IntegerType)
+ val b = Variable(bId)
+ val as = Set(aId, bId)
+
+ def checkSameExpr(e1: Expr, e2: Expr, vs: Set[Identifier]) {
+ assert( //this outer assert should not be needed because of the nested one
+ LikelyEq(e1, e2, vs, BooleanLiteral(true), (e1, e2) => {assert(e1 === e2); true})
+ )
+ }
+
+ test("simplifyArithmetic") {
+ val e1 = Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ checkSameExpr(e1, simplifyArithmetic(e1), Set())
+ val e2 = Plus(x, Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
+ checkSameExpr(e2, simplifyArithmetic(e2), Set(xId))
+
+ val e3 = Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ checkSameExpr(e3, simplifyArithmetic(e3), Set())
+ val e4 = Plus(x, Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
+ checkSameExpr(e4, simplifyArithmetic(e4), Set(xId))
+ val e5 = Plus(x, Minus(x, InfiniteIntegerLiteral(2)))
+ checkSameExpr(e5, simplifyArithmetic(e5), Set(xId))
+
+ val e6 = Times(InfiniteIntegerLiteral(9), Plus(Division(x, InfiniteIntegerLiteral(3)), Division(x, InfiniteIntegerLiteral(6))))
+ checkSameExpr(e6, simplifyArithmetic(e6), Set(xId))
+ }
+
+ test("expandAndSimplifyArithmetic") {
+ val e1 = Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ checkSameExpr(e1, expandAndSimplifyArithmetic(e1), Set())
+ val e2 = Plus(x, Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
+ checkSameExpr(e2, expandAndSimplifyArithmetic(e2), Set(xId))
+
+ val e3 = Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ checkSameExpr(e3, expandAndSimplifyArithmetic(e3), Set())
+ val e4 = Plus(x, Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
+ checkSameExpr(e4, expandAndSimplifyArithmetic(e4), Set(xId))
+ val e5 = Plus(x, Minus(x, InfiniteIntegerLiteral(2)))
+ checkSameExpr(e5, expandAndSimplifyArithmetic(e5), Set(xId))
+
+ val e6 = Times(InfiniteIntegerLiteral(9), Plus(Division(x, InfiniteIntegerLiteral(3)), Division(x, InfiniteIntegerLiteral(6))))
+ checkSameExpr(e6, expandAndSimplifyArithmetic(e6), Set(xId))
+ }
+
+ test("extractEquals") {
+ val eq = Equals(a, b)
+ val lt1 = LessThan(a, b)
+ val lt2 = LessThan(b, a)
+ val lt3 = LessThan(x, y)
+
+ val f1 = And(Seq(eq, lt1, lt2, lt3))
+ val (eq1, r1) = extractEquals(f1)
+ assert(eq1 != None)
+ assert(eq1.get === eq)
+ assert(extractEquals(r1)._1 === None)
+
+ val f2 = And(Seq(lt1, lt2, eq, lt3))
+ val (eq2, r2) = extractEquals(f2)
+ assert(eq2 != None)
+ assert(eq2.get === eq)
+ assert(extractEquals(r2)._1 === None)
+
+ val f3 = And(Seq(lt1, eq, lt2, lt3, eq))
+ val (eq3, r3) = extractEquals(f3)
+ assert(eq3 != None)
+ assert(eq3.get === eq)
+ val (eq4, r4) = extractEquals(r3)
+ assert(eq4 != None)
+ assert(eq4.get === eq)
+ assert(extractEquals(r4)._1 === None)
+ }
+
+ test("pre and post traversal") {
+ val expr = Plus(InfiniteIntegerLiteral(1), Minus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3)))
+ var res = ""
+ def f(e: Expr): Unit = e match {
+ case InfiniteIntegerLiteral(i) => res += i
+ case _ : Plus => res += "P"
+ case _ : Minus => res += "M"
+ }
+
+ preTraversal(f)(expr)
+ assert(res === "P1M23")
+
+ res = ""
+ postTraversal(f)(expr)
+ assert(res === "123MP")
+ }
+
+ test("pre- and postMap") {
+ val expr = Plus(InfiniteIntegerLiteral(1), Minus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3)))
+ def op(e : Expr ) = e match {
+ case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => Some(InfiniteIntegerLiteral(2))
+ case InfiniteIntegerLiteral(one) if one == BigInt(1) => Some(InfiniteIntegerLiteral(2))
+ case InfiniteIntegerLiteral(two) if two == BigInt(2) => Some(InfiniteIntegerLiteral(42))
+ case _ => None
+ }
+
+ assert( preMap(op, false)(expr) == Plus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(2)) )
+ assert( preMap(op, true )(expr) == Plus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(42)) )
+ assert( postMap(op, false)(expr) == Plus(InfiniteIntegerLiteral(2), Minus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(3))) )
+ assert( postMap(op, true)(expr) == Plus(InfiniteIntegerLiteral(42), Minus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(3))) )
+
+ }
+
+}
diff --git a/src/unit-test/scala/leon/purescala/TreeTestsSuite.scala b/src/unit-test/scala/leon/purescala/TreeTestsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..933ba02dc4397850965c14d5dbf22ee8f5fe3f97
--- /dev/null
+++ b/src/unit-test/scala/leon/purescala/TreeTestsSuite.scala
@@ -0,0 +1,38 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon.test._
+
+import leon.purescala.Common._
+import leon.purescala.Constructors._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+
+class TreeTestsSuite extends LeonTestSuite {
+
+ test("And- and Or- simplifications") {
+ val x = Variable(FreshIdentifier("x", BooleanType))
+ val t = BooleanLiteral(true)
+ val f = BooleanLiteral(false)
+
+ def and(es : Expr*) : Expr = andJoin(es)
+ def or(es : Expr*) : Expr = orJoin(es)
+
+ assert(and(x, and(x, x), x) === and(x, x, x, x))
+ assert(and(x, t, x, t) === and(x, x))
+ assert(and(x, t, f, x) === and(x, f))
+ assert(and(x) === x)
+ assert(and() === t)
+ assert(and(t, t) === t)
+ assert(and(f) === f)
+
+ assert(or(x, or(x, x), x) === or(x, x, x, x))
+ assert(or(x, f, x, f) === or(x, x))
+ assert(or(x, f, t, x) === or(x, t))
+ assert(or(x) === x)
+ assert(or() === f)
+ assert(or(f, f) === f)
+ assert(or(t) === t)
+ }
+}
diff --git a/src/unit-test/scala/leon/purescala/WithLikelyEq.scala b/src/unit-test/scala/leon/purescala/WithLikelyEq.scala
new file mode 100644
index 0000000000000000000000000000000000000000..705f2ba403fd60ac500641d9d5c13559788d2354
--- /dev/null
+++ b/src/unit-test/scala/leon/purescala/WithLikelyEq.scala
@@ -0,0 +1,87 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package purescala
+
+import leon.evaluators._
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.ExprOps.replace
+import leon.purescala.Expressions._
+
+/*
+ * Determine if two expressions over arithmetic variables are likely to be equal.
+ *
+ * This is a probabilistic based approach, it does not rely on any external solver and can
+ * only prove the non equality of two expressions.
+ */
+trait WithLikelyEq {
+ this: LeonTestSuite =>
+
+ object LikelyEq {
+ private val min = -5
+ private val max = 5
+
+ /*
+ * compare e1 and e2, using a list of assignment of integer to the variables in vs.
+ * Pre is a boolean expression precondition over the same variables that must be evaluated to true
+ * before testing equality.
+ * Add a default mapping for some set parameters
+ * Note that the default map could contain a mapping for variables to other parameters
+ * It is thus necessary to first select values for those parameters and then substitute
+ * into the default map !
+ */
+ def apply(e1: Expr, e2: Expr, vs: Set[Identifier], pre: Expr = BooleanLiteral(true),
+ compare: (Expr, Expr) => Boolean = (e1, e2) => e1 == e2,
+ defaultMap: Map[Identifier, Expr] = Map()): Boolean = {
+ val evaluator = new DefaultEvaluator(createLeonContext(), Program.empty)
+ if(vs.isEmpty) {
+ val ndm = defaultMap.map { case (id, expr) => (id, evaluator.eval(expr).asInstanceOf[EvaluationResults.Successful].value) } //TODO: not quite sure why I need to do this...
+ (evaluator.eval(e1, ndm), evaluator.eval(e2, defaultMap)) match {
+ case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => compare(v1, v2)
+ case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
+ }
+ } else {
+ var isEq = true
+ val vsOrder = vs.toArray
+ val counters: Array[Int] = vsOrder.map(_ => min)
+ var i = 0
+
+ while(i < counters.length && isEq) {
+ val m: Map[Expr, Expr] = vsOrder.zip(counters).map{case (v, c) => (Variable(v), InfiniteIntegerLiteral(c))}.toMap
+ val ne1 = replace(m, e1)
+ val ne2 = replace(m, e2)
+ val npre = replace(m, pre)
+ val ndm = defaultMap.map{ case (id, expr) => (id, evaluator.eval(expr, m.map{case (Variable(id), t) => (id, t)}).asInstanceOf[EvaluationResults.Successful].value) }
+ evaluator.eval(npre, ndm) match {
+ case EvaluationResults.Successful(BooleanLiteral(false)) =>
+ case EvaluationResults.Successful(BooleanLiteral(true)) =>
+ val ev1 = evaluator.eval(ne1, ndm)
+ val ev2 = evaluator.eval(ne2, ndm)
+ (ev1, ev2) match {
+ case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => if(!compare(v1, v2)) isEq = false
+ case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
+ }
+ case err => sys.error("evaluation of precondition could not complete, got: " + err)
+ }
+
+ 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
+ }
+ }
+ }
+ isEq
+ }
+ }
+
+ }
+
+}
diff --git a/src/unit-test/scala/leon/synthesis/AlgebraSuite.scala b/src/unit-test/scala/leon/synthesis/AlgebraSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cb0eed3dd924512507e89bcfee95c4e00c64539f
--- /dev/null
+++ b/src/unit-test/scala/leon/synthesis/AlgebraSuite.scala
@@ -0,0 +1,204 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+import Algebra._
+
+class AlgebraSuite extends LeonTestSuite {
+
+ test("remainder") {
+ 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") {
+ 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") {
+ 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") {
+ 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") {
+ 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") {
+ 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") {
+ assert(lcm(1,2,3) === 6)
+ assert(lcm(1,2,3,4) === 12)
+ assert(lcm(5,2,3,4) === 60)
+ }
+ test("seq lcm") {
+ 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") {
+ 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/unit-test/scala/leon/synthesis/LinearEquationsSuite.scala b/src/unit-test/scala/leon/synthesis/LinearEquationsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9506b271326f35c33c0ff53b36178b0c74ad47d0
--- /dev/null
+++ b/src/unit-test/scala/leon/synthesis/LinearEquationsSuite.scala
@@ -0,0 +1,260 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+import leon.purescala.WithLikelyEq
+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 WithLikelyEq {
+
+ def i(x: Int) = InfiniteIntegerLiteral(x)
+
+ val xId = FreshIdentifier("x", IntegerType)
+ val x = Variable(xId)
+ val yId = FreshIdentifier("y", IntegerType)
+ val y = Variable(yId)
+ val zId = FreshIdentifier("z", IntegerType)
+ val z = Variable(zId)
+
+ val aId = FreshIdentifier("a", IntegerType)
+ val a = Variable(aId)
+ val bId = FreshIdentifier("b", IntegerType)
+ val b = Variable(bId)
+
+ def toSum(es: Seq[Expr]) = es.reduceLeft(Plus)
+
+ def checkSameExpr(e1: Expr, e2: Expr, vs: Set[Identifier], prec: Expr, defaultMap: Map[Identifier, Expr] = Map()) {
+ assert( //this outer assert should not be needed because of the nested one
+ LikelyEq(e1, e2, vs, prec, (e1, e2) => {assert(e1 === e2); true}, defaultMap)
+ )
+ }
+
+
+ //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
+ }
+ }
+ }
+ }
+
+ //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") {
+ 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") {
+ def toExpr(es: Array[Expr]): Expr = {
+ val vars: Array[Expr] = Array[Expr](i(1)) ++ Array[Expr](x, y)
+ es.zip(vars).foldLeft[Expr](i(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
+ }
+
+ val t1: Expr = Plus(a, b)
+ val c1: Expr = i(4)
+ val d1: Expr = i(22)
+ val e1: Array[Expr] = Array(t1, c1, d1)
+ val (pre1, (w1, w2)) = particularSolution(Set(aId, bId), t1, c1, d1)
+ checkSameExpr(toExpr(e1), i(0), Set(aId, bId), pre1, Map(xId -> w1, yId -> w2))
+
+ val t2: Expr = i(-1)
+ val c2: Expr = i(1)
+ val d2: Expr = i(-1)
+ val e2: Array[Expr] = Array(t2, c2, d2)
+ val (pre2, (w3, w4)) = particularSolution(Set(), t2, c2, d2)
+ checkSameExpr(toExpr(e2), i(0), Set(), pre2, Map(xId -> w3, yId -> w4))
+ }
+
+ test("particularSolution preprocess") {
+ def toExpr(es: Array[Expr], vs: Array[Expr]): Expr = {
+ val vars: Array[Expr] = Array[Expr](i(1)) ++ vs
+ es.zip(vars).foldLeft[Expr](i(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
+ }
+
+ val t1: Expr = Plus(a, b)
+ val c1: Expr = i(4)
+ val d1: Expr = i(22)
+ val e1: Array[Expr] = Array(t1, c1, d1)
+ val (pre1, s1) = particularSolution(Set(aId, bId), e1.toList)
+ checkSameExpr(toExpr(e1, Array(x, y)), i(0), Set(aId, bId), pre1, Array(xId, yId).zip(s1).toMap)
+
+ val t2: Expr = Plus(a, b)
+ val c2: Expr = i(4)
+ val d2: Expr = i(22)
+ val f2: Expr = i(10)
+ val e2: Array[Expr] = Array(t2, c2, d2, f2)
+ val (pre2, s2) = particularSolution(Set(aId, bId), e2.toList)
+ checkSameExpr(toExpr(e2, Array(x, y, z)), i(0), Set(aId, bId), pre2, Array(xId, yId, zId).zip(s2).toMap)
+
+ val t3: Expr = Plus(a, Times(i(2), b))
+ val c3: Expr = i(6)
+ val d3: Expr = i(24)
+ val f3: Expr = i(9)
+ val e3: Array[Expr] = Array(t3, c3, d3, f3)
+ val (pre3, s3) = particularSolution(Set(aId, bId), e3.toList)
+ checkSameExpr(toExpr(e3, Array(x, y, z)), i(0), Set(aId, bId), pre3, Array(xId, yId, zId).zip(s3).toMap)
+
+ val t4: Expr = Plus(a, b)
+ val c4: Expr = i(4)
+ val e4: Array[Expr] = Array(t4, c4)
+ val (pre4, s4) = particularSolution(Set(aId, bId), e4.toList)
+ checkSameExpr(toExpr(e4, Array(x)), i(0), Set(aId, bId), pre4, Array(xId).zip(s4).toMap)
+ }
+
+
+ test("linearSet") {
+ val as = Set[Identifier]()
+
+ val evaluator = new DefaultEvaluator(createLeonContext(), 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
+ test("elimVariable") {
+ val as = Set[Identifier](aId, bId)
+
+ val evaluator = new DefaultEvaluator(createLeonContext(), 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), i(t._2))).toMap
+ val cWithVars: Expr = c.zip(witnesses).foldLeft[Expr](i(0)){ case (acc, (coef, wit)) => Plus(acc, Times(coef, replace(mapping, wit))) }
+ checkSameExpr(Plus(t, cWithVars), i(0), as, prec)
+ })
+ }
+
+ val t1 = Minus(Times(i(2), a), b)
+ val c1 = List(i(3), i(4), i(8))
+ val (pre1, wit1, f1) = elimVariable(evaluator, as, t1::c1)
+ check(t1, c1, pre1, wit1, f1)
+
+ val t2 = Plus(Plus(i(0), i(2)), Times(i(-1), i(3)))
+ val c2 = List(i(1), i(-1))
+ val (pre2, wit2, f2) = elimVariable(evaluator, Set(), t2::c2)
+ check(t2, c2, pre2, wit2, f2)
+
+
+ val t3 = Minus(Times(i(2), a), i(3))
+ val c3 = List(i(2))
+ val (pre3, wit3, f3) = elimVariable(evaluator, Set(aId), t3::c3)
+ check(t3, c3, pre3, wit3, f3)
+
+ val t4 = Times(i(2), a)
+ val c4 = List(i(2), i(4))
+ val (pre4, wit4, f4) = elimVariable(evaluator, Set(aId), t4::c4)
+ check(t4, c4, pre4, wit4, f4)
+
+ val t5 = Minus(a, b)
+ val c5 = List(i(-60), i(-3600))
+ val (pre5, wit5, f5) = elimVariable(evaluator, Set(aId, bId), t5::c5)
+ check(t5, c5, pre5, wit5, f5)
+
+ }
+
+}
diff --git a/src/unit-test/scala/leon/utils/StreamsSuite.scala b/src/unit-test/scala/leon/utils/StreamsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ee87d8ea3eb4b711114ed788193a35d376ba6e11
--- /dev/null
+++ b/src/unit-test/scala/leon/utils/StreamsSuite.scala
@@ -0,0 +1,66 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package utils
+
+import purescala.Common._
+import utils.StreamUtils._
+
+class StreamsSuite extends LeonTestSuite {
+ test("Cartesian Product 1") {
+ val s1 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty
+
+ val s2 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty
+
+ val ss = cartesianProduct(List(s1, s2))
+
+ assert(ss.size === s1.size * s2.size)
+
+
+ }
+
+ test("Cartesian Product 2") {
+ val s1 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty
+
+ val s2 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty
+
+ val tmp1 = s1.mkString
+ val tmp2 = s2.mkString
+
+ val ss = cartesianProduct(List(s1, s2))
+
+ assert(ss.size === s1.size * s2.size)
+ }
+
+
+ test("Cartesian Product 3") {
+ val s1 = 1 #::
+ 2 #::
+ 3 #::
+ 4 #:: Stream.empty
+
+ val s2 = 5 #::
+ 6 #::
+ 7 #::
+ 8 #:: Stream.empty
+
+ val tmp1 = s1.mkString
+ val tmp2 = s2.mkString
+
+ val ss = cartesianProduct(List(s1, s2))
+
+ assert(ss.size === s1.size * s2.size)
+ }
+}