Array smtlib compliance tests

diff --git a/test/regress/README b/test/regress/README
index bef93b140b0ee25083e4eefa5e6a92676fdffe2f..58cd2f2e7dce9004c6fbd5c9141de5c591c1a767 100644 (file)
--- a/test/regress/README
+++ b/test/regress/README
@@ -39,6 +39,7 @@ QUERY TRUE;
 syntax error;
 % EXIT: 1
 
+[Outdated: please also see edit below as an addendum.]
 Use of % gestures in CVC format is natural, as these are comments and ignored
 by the CVC presentation language lexer.  In SMT and SMT2 formats, you can do the
 same, putting % gestures in the file.  However, the run_regression script
@@ -54,3 +55,9 @@ is left verbatim (and never processed to remove the % EXPECT: lines) by the
 run_regression script.
 
  -- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 01 Jul 2010 13:36:53 -0400
+
+[Edit 2014/03/14: No support for '%' in .smt2 files any
+longer. Please use ';' or create separate .expect files. Very few test
+were using this "feature" and was causing issues because temp file
+name changed the expected error output string. '%' works for .smt files
+--Kshitij]

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 067b5d381598d9b919a7c4d6dd3b1f77f0e475d6..e2d6664cdc5ec16391c8ba8ad63dd2585b7a5f44 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -46,6 +46,7 @@ SMT_TESTS = \
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = \
+       arrayinuf_declare.smt2 \
        chained-equality.smt2 \
        ite2.smt2 \
        ite3.smt2 \
@@ -164,12 +165,14 @@ EXTRA_DIST = $(TESTS) \
 if CVC4_BUILD_PROFILE_COMPETITION
 else
 TESTS += \
-       error.cvc
+       error.cvc \
+       arrayinuf_error.smt2
 endif
 
 # and make sure to distribute it
 EXTRA_DIST += \
        subranges.cvc \
+       arrayinuf_error.smt2 \
        error.cvc
 
 # synonyms for "check" in this directory

diff --git a/test/regress/regress0/arrayinuf_declare.smt2 b/test/regress/regress0/arrayinuf_declare.smt2
new file mode 100644 (file)
index 0000000..5b73f24
--- /dev/null
+++ b/test/regress/regress0/arrayinuf_declare.smt2
@@ -0,0 +1,4 @@
+; EXIT: 0
+(set-logic QF_UF)
+(declare-sort Array 1)
+(declare-fun a ((Array Bool) Bool Bool) Bool)

diff --git a/test/regress/regress0/arrayinuf_error.smt2 b/test/regress/regress0/arrayinuf_error.smt2
new file mode 100644 (file)
index 0000000..d029b2b
--- /dev/null
+++ b/test/regress/regress0/arrayinuf_error.smt2
@@ -0,0 +1,4 @@
+; EXPECT-ERROR: (error "Parse Error: arrayinuf_error.smt2:3.21: Symbol 'Array' not declared as a type")
+(set-logic QF_UF)
+(declare-fun a (Array Bool Bool))
+; EXIT: 1

diff --git a/test/regress/regress0/bug220.smt2 b/test/regress/regress0/bug220.smt2
index 117ee3be2983a05f0f17a92543b9df77ccc96865..1520bcde0e37aa98207ef26e06ffc9e833697b93 100644 (file)
--- a/test/regress/regress0/bug220.smt2
+++ b/test/regress/regress0/bug220.smt2
@@ -1,2 +1,2 @@
-% EXIT: 0
+; EXIT: 0
 (exit)

diff --git a/test/regress/regress0/bug398.smt2 b/test/regress/regress0/bug398.smt2
index 0423d11a45ddcad4121d5cf172a6c90b77ee0f5e..3e4a1faca73b10c61dcd3eb96b5836fa8b3a7469 100644 (file)
--- a/test/regress/regress0/bug398.smt2
+++ b/test/regress/regress0/bug398.smt2
@@ -1,3 +1,3 @@
-% EXIT: 0
+; EXIT: 0
 (set-logic QF_LRA)
 (define-fun x () Real (+ 4 1))

diff --git a/test/regress/run_regression b/test/regress/run_regression
index ef2bb9a351de357c7ee1451bbb3878482bbfc243..ec9e170578afa2c7c722fd9b3e1ecff5c05a3c15 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -114,19 +114,14 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       expected_exit_status=0
     fi
-  elif grep '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then
-    expected_output=`grep '^[%;] EXPECT: ' "$benchmark" | sed 's,^[%;] EXPECT: ,,'`
-    expected_error=`grep '^[%;] EXPECT-ERROR: ' "$benchmark" | sed 's,^[%;] EXPECT-ERROR: ,,'`
-    expected_exit_status=`grep -m 1 '^[%;] EXIT: ' "$benchmark" | perl -pe 's,^[%;] EXIT: ,,;s,\r,,'`
-    command_line=`grep '^[%;] COMMAND-LINE: ' "$benchmark" | sed 's,^[%;] COMMAND-LINE: ,,'`
-    # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
-    # this frustrates our auto-language-detection
-    gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX
-    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
+  elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then
+    expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'`
+    expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'`
+    expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'`
+    command_line=`grep '^; COMMAND-LINE: ' "$benchmark" | sed 's,^; COMMAND-LINE: ,,'`
     if [ -z "$expected_exit_status" ]; then
       expected_exit_status=0
     fi
-    benchmark=$tmpbenchmark
   elif grep '^ *( *set-info  *:status  *sat' "$benchmark" &>/dev/null; then
     expected_output=sat
     expected_exit_status=0