Handle subtypes in sets. Bug fixes for tuples with subtypes.

15 files changed, 108 insertions, 3 deletions

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index d9db39b40..caf1fc61c 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -79,7 +79,8 @@ TESTS =	\
 	dt-sel-2.6.smt2 \
 	dt-param-2.6.smt2 \
 	dt-color-2.6.smt2 \
-	dt-match-pat-param-2.6.smt2
+	dt-match-pat-param-2.6.smt2 \
+	tuple-no-clash.cvc
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc b/test/regress/regress0/datatypes/tuple-no-clash.cvc
new file mode 100644
index 000000000..4d7345a54
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc
@@ -0,0 +1,11 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+
+x : [ REAL, REAL ];
+y : REAL;
+z : REAL;
+
+ASSERT x = (y, z) OR x = (z, y);
+ASSERT x = (0,0) OR x = (1,1);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/atom_univ2.cvc b/test/regress/regress0/rels/atom_univ2.cvc
index 9901ce630..e01d99dee 100644
--- a/test/regress/regress0/rels/atom_univ2.cvc
+++ b/test/regress/regress0/rels/atom_univ2.cvc
@@ -1,4 +1,5 @@
 % EXPECT: unsat

+OPTION "sets-ext";

 OPTION "logic" "ALL_SUPPORTED";

 Atom: TYPE;

 

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 9413dfba3..5ff24f1ff 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -81,7 +81,12 @@ TESTS =	\
   complement3.cvc \
   sharing-simp.smt2 \
   pre-proc-univ.smt2 \
-  nonvar-univ.smt2
+  nonvar-univ.smt2 \
+  sets-poly-int-real.smt2 \
+  sets-poly-nonint.smt2 \
+  int-real-univ.smt2 \
+  int-real-univ-unsat.smt2 \
+  sets-tuple-poly.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc
index 73eeb2cbd..91388a56c 100644
--- a/test/regress/regress0/sets/complement.cvc
+++ b/test/regress/regress0/sets/complement.cvc
@@ -1,4 +1,5 @@
 % EXPECT: sat
+OPTION "sets-ext";
 OPTION "logic" "ALL_SUPPORTED";
 Atom: TYPE;
 a : SET OF [Atom];
diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc
index 22dde0338..b8100bf5f 100644
--- a/test/regress/regress0/sets/complement2.cvc
+++ b/test/regress/regress0/sets/complement2.cvc
@@ -1,4 +1,5 @@
 % EXPECT: unsat

+OPTION "sets-ext";

 OPTION "logic" "ALL_SUPPORTED";

 Atom: TYPE;

 a : SET OF Atom;

diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc
index ff527a9b3..fa0a31e40 100644
--- a/test/regress/regress0/sets/complement3.cvc
+++ b/test/regress/regress0/sets/complement3.cvc
@@ -1,4 +1,5 @@
 % EXPECT: sat
+OPTION "sets-ext";
 OPTION "logic" "ALL_SUPPORTED";
 Atom : TYPE;
 C32 : SET OF [Atom];
@@ -11,4 +12,4 @@ ASSERT TUPLE(V1) IS_IN ~(C32);
 ASSERT ATOM_UNIV = UNIVERSE :: SET OF [Atom];
 ASSERT TUPLE(V1) IS_IN ATOM_UNIV;
 ASSERT TUPLE(V1) IS_IN ~(C2);
-CHECKSAT;
\ No newline at end of file
+CHECKSAT;
diff --git a/test/regress/regress0/sets/int-real-univ-unsat.smt2 b/test/regress/regress0/sets/int-real-univ-unsat.smt2
new file mode 100644
index 000000000..56f7e8c5e
--- /dev/null
+++ b/test/regress/regress0/sets/int-real-univ-unsat.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun a () (Set Real))
+
+(declare-fun x () Real)
+
+(assert (= (as univset (Set Real)) (as univset (Set Int))))
+
+(assert (member x a))
+
+(assert (and (<= 5.5 x) (< x 5.8)))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/int-real-univ.smt2 b/test/regress/regress0/sets/int-real-univ.smt2
new file mode 100644
index 000000000..afe20b92f
--- /dev/null
+++ b/test/regress/regress0/sets/int-real-univ.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun a () (Set Real))
+
+(declare-fun x () Real)
+
+(assert (= (as univset (Set Real)) (as univset (Set Int))))
+
+(assert (member x a))
+
+(assert (and (<= 5.5 x) (< x 6.1)))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/nonvar-univ.smt2 b/test/regress/regress0/sets/nonvar-univ.smt2
index c71c984a2..5c3bc567c 100644
--- a/test/regress/regress0/sets/nonvar-univ.smt2
+++ b/test/regress/regress0/sets/nonvar-univ.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () (Set Int))
diff --git a/test/regress/regress0/sets/pre-proc-univ.smt2 b/test/regress/regress0/sets/pre-proc-univ.smt2
index 1b4bf8b41..f184ebf92 100644
--- a/test/regress/regress0/sets/pre-proc-univ.smt2
+++ b/test/regress/regress0/sets/pre-proc-univ.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () (Set Int))
diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2
new file mode 100644
index 000000000..407e95d3c
--- /dev/null
+++ b/test/regress/regress0/sets/sets-poly-int-real.smt2
@@ -0,0 +1,17 @@
+(set-logic QF_UFLIRAFS)
+(set-info :status sat)
+(declare-fun s () (Set Real))
+(declare-fun t1 () (Set Real))
+(declare-fun t2 () (Set Real))
+(declare-fun t3 () (Set Real))
+(declare-fun r1 () (Set Int))
+(declare-fun r2 () (Set Int))
+(declare-fun r3 () (Set Int))
+(assert (and (member 1.5 s) (member 0 s)))
+(assert (= t1 (union s (singleton 2.5))))
+(assert (= t2 (union s (singleton 2))))
+(assert (= t3 (union r3 (singleton 2.5))))
+(assert (= (intersection r1 r2) (intersection s (singleton 0))))
+(assert (not (= r1 (as emptyset (Set Real)))))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2
new file mode 100644
index 000000000..441716dcf
--- /dev/null
+++ b/test/regress/regress0/sets/sets-poly-nonint.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UFLIRAFS)
+(set-info :status unsat)
+(declare-fun s () (Set Int))
+(declare-fun t () (Set Real))
+(declare-fun r () (Set Real))
+(declare-fun u () (Set Real))
+(assert (member 1.5 t))
+(assert (member 2.5 r))
+(assert (member 3.5 u))
+(assert (or (member 4.5 s) (= s t) (= s r) (= s u) (= s (singleton 6.5))))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc
new file mode 100644
index 000000000..8d87345f6
--- /dev/null
+++ b/test/regress/regress0/sets/sets-tuple-poly.cvc
@@ -0,0 +1,18 @@
+% EXPECT: sat
+OPTION "sets-ext";
+OPTION "logic" "ALL_SUPPORTED";
+
+a : SET OF [REAL, INT];
+b : SET OF [INT, REAL];
+
+x : [ REAL, REAL ];
+
+
+ASSERT NOT x = (0,0);
+
+ASSERT x IS_IN a;
+ASSERT x IS_IN b;
+
+ASSERT NOT x.0 = x.1;
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2
index ec9750776..a8875cc41 100644
--- a/test/regress/regress0/sets/univset-simp.smt2
+++ b/test/regress/regress0/sets/univset-simp.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)