blob: 6e4a846727fe6e3b4fd09e0bb178b8a8b2318d8f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(set-logic AUFLIA)
(set-info :source | mySet theory. |)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort mySet 0)
(declare-sort Elem 0)
(declare-fun member (Elem mySet) Bool)
(declare-fun subset (mySet mySet) Bool)
(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2))))
(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2)))))))
(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2))))
(declare-fun seteq (mySet mySet) Bool)
(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (= ?s1 ?s2))))
(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))
(declare-fun myunion (mySet mySet) mySet)
(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myunion ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2)))))
(declare-fun myintersection (mySet mySet) mySet)
(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myintersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2)))))
(declare-fun difference (mySet mySet) mySet)
(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2))))))
(declare-fun a () mySet)
(declare-fun b () mySet)
(assert (not (seteq (myintersection a b) (myintersection b a))))
(check-sat)
(exit)
|
