Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.

5 files changed, 75 insertions, 2 deletions

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index fed65924b..90d6b4716 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -74,7 +74,10 @@ TESTS =	\
 	dt-param-card4-bool-sat.smt2 \
 	bug604.smt2 \
 	bug597-rbt.smt2 \
-	example-dailler-min.smt2
+	example-dailler-min.smt2 \
+	dt-2.6.smt2  \
+	dt-sel-2.6.smt2 \
+	dt-param-2.6.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/dt-2.6.smt2 b/test/regress/regress0/datatypes/dt-2.6.smt2
new file mode 100644
index 000000000..07dc0169e
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-2.6.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --lang=smt2.6
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((IntList 0)) (
+((empty) (insert ( head Int ) ( tail IntList ) ))
+))
+
+(declare-fun x () IntList)
+(declare-fun y () IntList)
+(declare-fun z () IntList)
+
+(assert (distinct x y z))
+
+(check-sat)
diff --git a/test/regress/regress0/datatypes/dt-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-param-2.6.smt2
new file mode 100644
index 000000000..a132ce8fc
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-param-2.6.smt2
@@ -0,0 +1,37 @@
+; COMMAND-LINE: --lang=smt2.6
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ( ( Tree 1) ( TreeList 1) ) (
+(par ( X ) ( ( node ( value X ) ( children ( TreeList X )) )))
+(par ( Y ) ( ( empty ) ( insert ( head ( Tree Y )) ( tail ( TreeList Y ))) ))
+))
+
+
+(declare-fun x () (Tree Int))
+(declare-fun y () (Tree Int))
+(declare-fun z () (Tree Int))
+
+
+(assert (distinct x y z))
+(assert (= (value x) 5))
+(assert ((_ is insert) (children y)))
+(assert (= (value (head (children y))) 7))
+
+(declare-sort U 0)
+(declare-fun a () (Tree U))
+(declare-fun b () (Tree U))
+(declare-fun c () (Tree U))
+
+(assert (distinct a b c))
+
+(assert ((_ is insert) (children a)))
+
+
+(declare-fun d () (Tree (Tree Int)))
+(declare-fun e () (Tree (Tree Int)))
+(declare-fun f () (Tree (Tree Int)))
+
+(assert (distinct d e f))
+
+(check-sat)
diff --git a/test/regress/regress0/datatypes/dt-sel-2.6.smt2 b/test/regress/regress0/datatypes/dt-sel-2.6.smt2
new file mode 100644
index 000000000..ae290a5ba
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-sel-2.6.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --lang=smt2.6
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((IntList 0)) (
+((empty) (insert ( head Int ) ( tail IntList ) ))
+))
+
+(declare-fun x () IntList)
+(declare-fun y () IntList)
+(declare-fun z () IntList)
+
+(assert (distinct x y z))
+
+(assert (not ((_ is insert) x)))
+(assert (not ((_ is insert) y)))
+
+(check-sat)
diff --git a/test/regress/run_regression b/test/regress/run_regression
index a04e488d8..5bc46d4f9 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -212,7 +212,7 @@ else
   error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p or *.sy"
 fi
 
-command_line="${command_line:+$command_line }--lang=$lang"
+command_line="--lang=$lang ${command_line:+$command_line }"
 
 gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX
 gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX