diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-04 15:10:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-04 15:10:24 -0500 |
| commit | 13cf41801f8f2bac538cb45d53ae7427916041a7 (patch) | |
| tree | 78e82b56e92004991890943ba5da863e6af3538f /test/regress/regress0 | |
| parent | d662d3321a46aac61973f7a90341ea870c0b1171 (diff) | |
Remove subtyping for sets theory (#5179)
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/sets/sets-poly-int-real.smt2 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2 index 407e95d3c..df79a39b0 100644 --- a/test/regress/regress0/sets/sets-poly-int-real.smt2 +++ b/test/regress/regress0/sets/sets-poly-int-real.smt2 @@ -4,14 +4,14 @@ (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))) +(declare-fun r1 () (Set Real)) +(declare-fun r2 () (Set Real)) +(declare-fun r3 () (Set Real)) +(assert (and (member 1.5 s) (member 0.0 s))) (assert (= t1 (union s (singleton 2.5)))) -(assert (= t2 (union s (singleton 2)))) +(assert (= t2 (union s (singleton 2.0)))) (assert (= t3 (union r3 (singleton 2.5)))) -(assert (= (intersection r1 r2) (intersection s (singleton 0)))) +(assert (= (intersection r1 r2) (intersection s (singleton 0.0)))) (assert (not (= r1 (as emptyset (Set Real))))) (check-sat) |