From: Tim King <taking@cs.nyu.edu>
Date: Tue, 14 Sep 2010 19:37:31 +0000 (+0000)
Subject: * added test/regress/regress0/arith for easy arithmetic regress tests.
X-Git-Tag: cvc5-1.0.0~8866
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ed3bc77005060a5745696519da31babd745181a7;p=cvc5.git

* added test/regress/regress0/arith for easy arithmetic regress tests.
---

diff --git a/test/Makefile.am b/test/Makefile.am
index 045599bc1..a257b96d9 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   blu=''; \
   std=''; \
 }
-subdirs_to_check = unit system regress/regress0 regress/regress0/uf regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
 check-recursive: check-pre
 .PHONY: check-pre
 check-pre:
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 7f732b17f..c376be91b 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . precedence uf
+SUBDIRS = . arith precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
new file mode 100644
index 000000000..e4fc110b4
--- /dev/null
+++ b/test/regress/regress0/arith/Makefile.am
@@ -0,0 +1,28 @@
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	arith.01.cvc \
+	arith.02.cvc 
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc
new file mode 100644
index 000000000..5b4a33bed
--- /dev/null
+++ b/test/regress/regress0/arith/arith.01.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+x : REAL;
+y : REAL;
+
+QUERY (x * y ) = (y * x);
+% EXIT: 20
diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc
new file mode 100644
index 000000000..a2c93da46
--- /dev/null
+++ b/test/regress/regress0/arith/arith.02.cvc
@@ -0,0 +1,7 @@
+% EXPECT: VALID
+x : REAL;
+y : REAL;
+z : REAL;
+
+QUERY x*(y*z) = (x*y)*z;
+% EXIT: 20
diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc
new file mode 100644
index 000000000..96af458f0
--- /dev/null
+++ b/test/regress/regress0/arith/arith.03.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+x : REAL;
+y : REAL;
+
+QUERY (x + y)*(x + y) = x*x + 2*x*y + y*y;
+% EXIT: 20