From 12032a9a858de434fe3917654b3b4e5e555136e2 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 10 Feb 2015 13:17:02 +0100
Subject: [PATCH] Unit test for default evaluator
---
.../evaluators/DefaultEvaluatorTests.scala | 106 ++++++++++++++++++
1 file changed, 106 insertions(+)
create mode 100644 src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
new file mode 100644
index 000000000..8b0946d8b
--- /dev/null
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -0,0 +1,106 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.test.evaluators
+
+import leon._
+import leon.evaluators._
+
+import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
+import leon.frontends.scalac.ExtractionPhase
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.DefOps._
+import leon.purescala.TypeTrees._
+
+
+class DefaultEvaluatorTests 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())
+ }
+
+ test("eval of simple arithmetic expressions") {
+ expectSuccessful(
+ defaultEvaluator.eval(Plus(IntLiteral(3), IntLiteral(5))), IntLiteral(8))
+ expectSuccessful(
+ defaultEvaluator.eval(Minus(IntLiteral(7), IntLiteral(2))), IntLiteral(5))
+ expectSuccessful(
+ defaultEvaluator.eval(UMinus(IntLiteral(7))), IntLiteral(-7))
+ expectSuccessful(
+ defaultEvaluator.eval(Times(IntLiteral(2), IntLiteral(3))), IntLiteral(6))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(IntLiteral(10), 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 simple variable") {
+ val id = FreshIdentifier("id").setType(Int32Type)
+ expectSuccessful(
+ defaultEvaluator.eval(Variable(id), Map(id -> IntLiteral(23))),
+ IntLiteral(23))
+ }
+
+ test("eval with unbound variable should return EvaluatorError") {
+ val id = FreshIdentifier("id").setType(Int32Type)
+ val foo = FreshIdentifier("foo").setType(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))
+ }
+}
--
GitLab