From 0efd7d952b51fe1a537c44d545db98d8159e5972 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 13 Nov 2012 17:50:49 +0100
Subject: [PATCH] tests for integer synthesis
---
.../synthesis/IntegerSynthesisSuite.scala | 39 +++++++++++++++++++
1 file changed, 39 insertions(+)
create mode 100644 src/test/scala/leon/test/synthesis/IntegerSynthesisSuite.scala
diff --git a/src/test/scala/leon/test/synthesis/IntegerSynthesisSuite.scala b/src/test/scala/leon/test/synthesis/IntegerSynthesisSuite.scala
new file mode 100644
index 000000000..4052ed825
--- /dev/null
+++ b/src/test/scala/leon/test/synthesis/IntegerSynthesisSuite.scala
@@ -0,0 +1,39 @@
+package leon.test.synthesis
+
+import org.scalatest.FunSuite
+
+import leon.Evaluator
+import leon.purescala.Trees._
+import leon.purescala.Common._
+
+import leon.synthesis.ArithmeticNormalization._
+import leon.synthesis.LikelyEq
+import leon.synthesis.IntegerSynthesis.apply
+
+class IntegerSynthesisSuite extends FunSuite {
+
+ def i(x: Int) = IntLiteral(x)
+
+ val xId = FreshIdentifier("x")
+ val x = Variable(xId)
+ val yId = FreshIdentifier("y")
+ val y = Variable(yId)
+ val xs = Set(xId, yId)
+
+ val aId = FreshIdentifier("a")
+ val a = Variable(aId)
+ val bId = FreshIdentifier("b")
+ val b = Variable(bId)
+ val as = Set(aId, bId)
+
+ test("apply") {
+
+ val f1 = And(
+ Equals(Plus(x, IntLiteral(2)), Plus(y, IntLiteral(3))),
+ Equals(Minus(x, IntLiteral(1)), Plus(y, IntLiteral(2)))
+ )
+
+ //apply(as, xs, f1)
+ }
+
+}
--
GitLab