Op overload parser (#1162)

* Update parser for operator overloading.

* Improvements

* Updates

* Add assert

5 files changed, 42 insertions, 2 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 5000be7a2..43c7ae3b1 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -70,9 +70,13 @@ SMT2_TESTS = \
 	hung13sdk_output2.smt2 \
 	declare-funs.smt2 \
 	declare-fun-is-match.smt2 \
+	issue1063-overloading-dt-cons.smt2 \
+	issue1063-overloading-dt-sel.smt2 \
+	issue1063-overloading-dt-fun.smt2 \
 	non-fatal-errors.smt2 \
 	sqrt2-sort-inf-unk.smt2
 
+
 # Regression tests for PL inputs
 CVC_TESTS = \
 	boolean.cvc \
diff --git a/test/regress/regress0/datatypes/error.cvc b/test/regress/regress0/datatypes/error.cvc
index 66fa17e02..23e658e6c 100644
--- a/test/regress/regress0/datatypes/error.cvc
+++ b/test/regress/regress0/datatypes/error.cvc
@@ -1,7 +1,7 @@
 % EXPECT-ERROR: CVC4 Error:
-% EXPECT-ERROR: Parse Error: foo already declared
+% EXPECT-ERROR: Parse Error: foo already declared in this datatype
 % EXIT: 1
 
-DATATYPE single_ctor = foo(bar:REAL) END;
+DATATYPE single_ctor = foo(bar:REAL) | foo(bar2:REAL) END;
 DATATYPE double_ctor = foo(bar:REAL) END;
 
diff --git a/test/regress/regress0/issue1063-overloading-dt-cons.smt2 b/test/regress/regress0/issue1063-overloading-dt-cons.smt2
new file mode 100644
index 000000000..f8ca2a9e5
--- /dev/null
+++ b/test/regress/regress0/issue1063-overloading-dt-cons.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((Enum0 (In_Air) (On_Ground) (None))))
+(declare-datatypes () ((Enum1 (True) (False) (None))))
+(declare-fun var_0 (Int) Enum0)
+(declare-fun var_1 (Int) Enum1)
+(assert (= (var_0 0) (as None Enum0)))
+(assert (= (var_1 1) (as None Enum1)))
+(assert (not (is-In_Air (var_0 0))))
+(declare-fun var_2 () Enum1)
+(assert (is-None var_2))
+(check-sat)
diff --git a/test/regress/regress0/issue1063-overloading-dt-fun.smt2 b/test/regress/regress0/issue1063-overloading-dt-fun.smt2
new file mode 100644
index 000000000..9cae20647
--- /dev/null
+++ b/test/regress/regress0/issue1063-overloading-dt-fun.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((Enum (cons (val Int)) (On_Ground) (None))))
+(declare-fun cons (Int Int) Int)
+(declare-fun cons (Enum) Bool)
+(declare-fun cons (Bool) Int)
+(assert (cons (cons 0)))
+(assert (= (cons (cons true) (cons false)) 4))
+(check-sat)
diff --git a/test/regress/regress0/issue1063-overloading-dt-sel.smt2 b/test/regress/regress0/issue1063-overloading-dt-sel.smt2
new file mode 100644
index 000000000..b3316d373
--- /dev/null
+++ b/test/regress/regress0/issue1063-overloading-dt-sel.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((Enum0 (cons (data Int)) (None))))
+(declare-datatypes () ((Enum1 (cons (data Bool)) (None))))
+(declare-fun var_0 () Enum0)
+(declare-fun var_1 () Enum1)
+(assert (= (data var_0) 5))
+(assert (data var_1))
+(check-sat)