diff options
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/set8.smt2 | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/test/regress/regress0/quantifiers/set8.smt2 b/test/regress/regress0/quantifiers/set8.smt2 index 6e4a84672..684d94b7a 100644 --- a/test/regress/regress0/quantifiers/set8.smt2 +++ b/test/regress/regress0/quantifiers/set8.smt2 @@ -1,26 +1,26 @@ (set-logic AUFLIA) -(set-info :source | mySet theory. |) +(set-info :source | Set theory. |) (set-info :smt-lib-version 2.0) (set-info :category "crafted") (set-info :status unsat) -(declare-sort mySet 0) +(declare-sort Set 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)))) +(declare-fun member (Elem Set) Bool) +(declare-fun subset (Set Set) Bool) +(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2)))) +(assert (forall ((?s1 Set) (?s2 Set)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2))))))) +(assert (forall ((?s1 Set) (?s2 Set)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2)))) +(declare-fun seteq (Set Set) Bool) +(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (= ?s1 ?s2)))) +(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1))))) +(declare-fun union (Set Set) Set) +(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (union ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2))))) +(declare-fun intersection (Set Set) Set) +(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (intersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2))))) +(declare-fun difference (Set Set) Set) +(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2)))))) +(declare-fun a () Set) +(declare-fun b () Set) +(assert (not (seteq (intersection a b) (intersection b a)))) (check-sat) (exit) |