diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-03 19:00:40 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-03 17:00:40 -0700 |
commit | 4873b5e515d8b3e5e70c42c50e8f680b26ba2331 (patch) | |
tree | 0472c0e4dc6e4de4a1b1fba8cd08dff10c06111a /test/regress/regress0/sets | |
parent | 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 (diff) |
Sets subtypes (#1095)
Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.
Diffstat (limited to 'test/regress/regress0/sets')
-rw-r--r-- | test/regress/regress0/sets/sets-of-sets-subtypes.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 new file mode 100644 index 000000000..86a1d93b4 --- /dev/null +++ b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_LIRAFS) +(set-info :status unsat) + +(declare-fun s () (Set (Set Real))) +(declare-fun t () (Set (Set Int))) + +(declare-fun x () (Set Int)) +(declare-fun y () (Set Real)) + +(assert (member 0.5 y)) +(assert (member y s)) +(assert (or (= s t) (= s (singleton (singleton 1.0))) (= s (singleton (singleton 0.0))))) + +(check-sat) |