main driver supports .smt2 input, added an smt2 regression (currently broken, so...

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 2ad34597e975a1f8e811da877e381446a30d0d73..a09da850dbef1a3b5213c816e7de3f4db5a187da 100644 (file)
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -41,9 +41,10 @@ namespace main {
 
 static const char lang_help[] = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
-  auto          attempt to automatically determine the input language\n\
-  pl | cvc4     CVC4 presentation language\n\
-  smt | smtlib  SMT-LIB format\n\
+  auto           attempt to automatically determine the input language\n\
+  pl | cvc4      CVC4 presentation language\n\
+  smt | smtlib   SMT-LIB format 1.2\n\
+  smt2 | smtlib2 SMT-LIB format 2.0\n\
 ";
 
 /**

diff --git a/src/main/main.cpp b/src/main/main.cpp
index bdf4f882b24ef215b8da5d9f8e60a45458bf6e86..a575426fd181b1c63d55c1b74a32327916c9adc3 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -117,7 +117,9 @@ int runCvc4(int argc, char* argv[]) {
   if(/*!inputFromStdin && */options.lang == parser::LANG_AUTO) {
     const char* filename = argv[firstArgIndex];
     unsigned len = strlen(filename);
-    if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+    if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
+      options.lang = parser::LANG_SMTLIB_V2;
+    } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
       options.lang = parser::LANG_SMTLIB;
     } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
               || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index fe95ed7aa9949a3530f955e64348818446108bc6..d87ff05411ac4dbd254bd677d2a527d0fb505db2 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -2,17 +2,17 @@ SUBDIRS = precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =        \
-    error.cvc \
-    boolean-prec.cvc \
-    distinct.smt \
-    flet.smt \
-    flet2.smt \
+       error.cvc \
+       boolean-prec.cvc \
+       distinct.smt \
+       flet.smt \
+       flet2.smt \
        let.smt \
        let2.smt \
        simple2.smt \
        simple.smt \
        simple-uf.smt \
-    bug32.cvc \
+       bug32.cvc \
        hole6.cvc \
        logops.01.cvc \
        logops.02.cvc \

diff --git a/test/regress/regress0/bignum_quant.smt2 b/test/regress/regress0/bignum_quant.smt2
new file mode 100644 (file)
index 0000000..d809e7e
--- /dev/null
+++ b/test/regress/regress0/bignum_quant.smt2
@@ -0,0 +1,13 @@
+(set-info :source | SMT-COMP'06 organizers |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(set-logic AUFLIA)
+(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.| )
+(set-info :difficulty 0.000)
+(declare-fun f (Int) Int)
+(assert (= (f 0) 1))
+(assert (forall (?x Int) (=> (> ?x 0) (= (f ?x) (* (- 1000) (f (- ?x 1)))))))
+(assert (< (f 20) 0))
+(check-sat)
+(exit)

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 439c8e6c940c520a0e3c52338711ed8d5bf6b9c7..9003479e75d8a56785be128304bda5cfe849abe1 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -5,7 +5,7 @@
 #
 # usage:
 #
-#     run_regression cvc4-binary [ benchmark.cvc | benchmark.smt ]
+#     run_regression cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
 #
 # Runs benchmark and checks for correct exit status and output.
 #
@@ -13,7 +13,7 @@
 prog=`basename "$0"`
 
 if [ $# != 2 ]; then
-  echo "usage: $prog cvc4-binary [ benchmark.cvc | benchmark.smt ]" >&2
+  echo "usage: $prog cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2
   exit 1
 fi
 
@@ -42,6 +42,16 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   else
     error "cannot determine status of \`$benchmark'"
   fi
+elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
+  if grep '^ *(set-info  *:status  *sat' "$benchmark" &>/dev/null; then
+    expected_output=SAT
+    expected_exit_status=10
+  elif grep '^ *(set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
+    expected_output=UNSAT
+    expected_exit_status=20
+  else
+    error "cannot determine status of \`$benchmark'"
+  fi
 elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
   expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
   expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
@@ -54,7 +64,7 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
     error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
   fi
 else
-  error "benchmark \`$benchmark' must be *.cvc or *.smt"
+  error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2"
 fi
 
 expoutfile=`mktemp -t cvc4_expect_stdout.XXXXXXXXXX`