This changes mkTuple -> tuple and tupSel -> tuple_select.
This is in line with the most recent syntax for tuples in preparation for the theory of tables in smt2.
(assert
(= r1
(insert
- (mkTuple "a" 1)
- (mkTuple "b" 2)
- (mkTuple "c" 3)
- (singleton (mkTuple "d" 4)))))
+ (tuple "a" 1)
+ (tuple "b" 2)
+ (tuple "c" 3)
+ (singleton (tuple "d" 4)))))
(assert
(= r2
(insert
- (mkTuple 1 "1")
- (mkTuple 2 "2")
- (mkTuple 3 "3")
- (singleton (mkTuple 17 "17")))))
+ (tuple 1 "1")
+ (tuple 2 "2")
+ (tuple 3 "3")
+ (singleton (tuple 17 "17")))))
(assert (= r (join r1 r2)))
(assert (= s (transpose r)))
(assert (= t (product r1 r2)))
(=
lt1
(insert
- (mkTuple 1 2)
- (mkTuple 2 3)
- (mkTuple 3 4)
- (singleton (mkTuple 4 5)))))
+ (tuple 1 2)
+ (tuple 2 3)
+ (tuple 3 4)
+ (singleton (tuple 4 5)))))
(assert (= lt2 (tclosure lt1)))
(assert (= i (card t)))
EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
-TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
-TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
+TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple';
+TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select';
TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project';
HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
if (dt.isTuple())
{
stillNeedToPrintParams = false;
- out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
+ out << "tuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
}
break;
}
if (dt.isTuple())
{
stillNeedToPrintParams = false;
- out << "(_ tupSel " << DType::indexOf(op) << ") ";
+ out << "(_ tuple_select " << DType::indexOf(op) << ") ";
}
}
break;
(set-option :incremental false)
(declare-fun f (Int) (Tuple Int Bool))
(declare-fun a () Int)
-(assert (not (= (f a) (mkTuple 0 false))))
+(assert (not (= (f a) (tuple 0 false))))
(check-sat)
(set-logic ALL)
(set-info :status unsat)
(declare-fun a () Tuple)
-(assert (distinct a mkTuple))
+(assert (distinct a tuple))
(check-sat)
(set-option :incremental false)
(declare-fun test (Int) (Tuple Int Int))
-(assert (= (test 5) (mkTuple 2 3)))
-(assert (= (test 7) (mkTuple 3 4)))
+(assert (= (test 5) (tuple 2 3)))
+(assert (= (test 7) (tuple 3 4)))
(check-sat)
(set-logic ALL)
(set-option :incremental false)
(declare-fun x () (Tuple Int Bool))
-(assert (not (= x (mkTuple 0 false))))
+(assert (not (= x (tuple 0 false))))
(check-sat)
(declare-datatypes ((list 1)) ((par (T)((cons (car T) (care Bool) (cdr (list T))) (nil)))))
(declare-fun x () (list Real))
(declare-fun y () (Tuple Int Bool Int))
-(assert (= y (mkTuple 5 true 4)))
-(assert ((_ tupSel 1) y))
+(assert (= y (tuple 5 true 4)))
+(assert ((_ tuple_select 1) y))
(assert (= x ((as cons (list Real)) (/ 11 10) true (as nil (list Real)))))
(check-sat)
(set-logic ALL)
(set-option :incremental false)
(declare-fun x () (Tuple Int Int))
-(assert (= ((_ tupSel 0) x) 5))
+(assert (= ((_ tuple_select 0) x) 5))
(check-sat)
(declare-fun x () (Tuple Real Real))
(declare-fun y () Real)
(declare-fun z () Real)
-(assert (or (= x (mkTuple y z)) (= x (mkTuple z y))))
-(assert (let ((_let_1 1.0)) (let ((_let_2 0.0)) (or (= x (mkTuple _let_2 _let_2)) (= x (mkTuple _let_1 _let_1))))))
+(assert (or (= x (tuple y z)) (= x (tuple z y))))
+(assert (let ((_let_1 1.0)) (let ((_let_2 0.0)) (or (= x (tuple _let_2 _let_2)) (= x (tuple _let_1 _let_1))))))
(check-sat)
(declare-fun x () Int)
(define-fun foo ((x |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)) |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| ((_ update int) x (int x)))
(declare-fun m () |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)
-(define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (mkTuple (foo m) 0) (mkTuple m 0)))
-(check-sat-assuming ( (not (= ((_ tupSel 1) (ite (= x 0) (mkTuple (foo m) 0) (mkTuple m 0))) 1)) ))
+(define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (tuple (foo m) 0) (tuple m 0)))
+(check-sat-assuming ( (not (= ((_ tuple_select 1) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) 1)) ))
; EXPECT: unsat
(set-logic ALL)
(set-option :incremental false)
-(define-fun x () (Tuple Real Int Real) (mkTuple (/ 4 5) 9 (/ 11 9)))
-(define-fun first_elem () Real ((_ tupSel 0) (mkTuple (/ 4 5) 9 (/ 11 9))))
-(define-fun third_elem () Real ((_ tupSel 2) (mkTuple (/ 4 5) 9 (/ 11 9))))
+(define-fun x () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9)))
+(define-fun first_elem () Real ((_ tuple_select 0) (tuple (/ 4 5) 9 (/ 11 9))))
+(define-fun third_elem () Real ((_ tuple_select 2) (tuple (/ 4 5) 9 (/ 11 9))))
-(define-fun y () (Tuple Real Int Real) (mkTuple (/ 4 5) 9 (/ 11 9)))
-(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (mkTuple (/ 4 5) 9 (/ 11 9)) 3))
-(check-sat-assuming ( (not (let ((_let_1 (mkTuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tupSel 0) _let_1) ((_ tupSel 0) _let_2))) (= ((_ tupSel 2) _let_1) ((_ tupSel 2) _let_2))) (= ((_ tupSel 1) _let_2) 3))))) ))
+(define-fun y () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9)))
+(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (tuple (/ 4 5) 9 (/ 11 9)) 3))
+(check-sat-assuming ( (not (let ((_let_1 (tuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tuple_select 0) _let_1) ((_ tuple_select 0) _let_2))) (= ((_ tuple_select 2) _let_1) ((_ tuple_select 2) _let_2))) (= ((_ tuple_select 1) _let_2) 3))))) ))
(declare-fun t1 () (Tuple (Tuple Int Int) (Tuple Int String Int)))
(declare-fun t2 () (Tuple (Tuple Bool Int) String))
-(assert (= t1 (mkTuple (mkTuple 12 99) (mkTuple 5 "xyz" 17))))
-(assert (= t2 (mkTuple (mkTuple true 14) "abc")))
-(assert (= t mkTuple))
+(assert (= t1 (tuple (tuple 12 99) (tuple 5 "xyz" 17))))
+(assert (= t2 (tuple (tuple true 14) "abc")))
+(assert (= t tuple))
(check-sat)
(declare-fun t () (Tuple Int String))
(declare-fun i () String)
-(assert (= t (mkTuple 0 "0")))
-(assert (= i ((_ tupSel 1) t)))
+(assert (= t (tuple 0 "0")))
+(assert (= i ((_ tuple_select 1) t)))
(check-sat)
(assert (= REAL_UNIVERSE (as univset (Set (Tuple Real)))))
(assert (= ATOM_UNIVERSE (as univset (Set (Tuple Atom)))))
(declare-fun levelVal () (Set (Tuple Atom Real)))
-(assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (member (mkTuple s) ATOM_UNIVERSE) (member (mkTuple v1) REAL_UNIVERSE)) (member (mkTuple v2) REAL_UNIVERSE)) (=> (and (member (mkTuple s v1) levelVal) (member (mkTuple s v2) levelVal)) (= v1 v2)))))
+(assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (member (tuple s) ATOM_UNIVERSE) (member (tuple v1) REAL_UNIVERSE)) (member (tuple v2) REAL_UNIVERSE)) (=> (and (member (tuple s v1) levelVal) (member (tuple s v2) levelVal)) (= v1 v2)))))
(check-sat)
; EXPECT: sat
; EXPECT: (((a r) "active"))
-; EXPECT: ((((_ tupSel 1) y) 9))
+; EXPECT: ((((_ tuple_select 1) y) 9))
(set-logic ALL)
(set-option :incremental false)
(set-option :produce-models true)
(declare-fun r () __cvc5_record_a_String_b_String)
(declare-fun y () (Tuple Real Int Real))
(assert (= r (__cvc5_record_a_String_b_String_ctor "active" "who knows?")))
-(assert (= y (mkTuple (/ 4 5) 9 (/ 11 9))))
+(assert (= y (tuple (/ 4 5) 9 (/ 11 9))))
(check-sat-assuming ( (not (= (a r) "what?")) ))
(get-value ( (a r) ))
-(get-value ( ((_ tupSel 1) y) ))
+(get-value ( ((_ tuple_select 1) y) ))
(declare-fun addr () (Set (Tuple Atom Atom Atom)))
(declare-fun b1 () Atom)
(declare-fun b1_tup () (Tuple Atom))
-(assert (= b1_tup (mkTuple b1)))
+(assert (= b1_tup (tuple b1)))
(assert (member b1_tup Book))
(declare-fun b2 () Atom)
(declare-fun b2_tup () (Tuple Atom))
-(assert (= b2_tup (mkTuple b2)))
+(assert (= b2_tup (tuple b2)))
(assert (member b2_tup Book))
(declare-fun b3 () Atom)
(declare-fun b3_tup () (Tuple Atom))
-(assert (= b3_tup (mkTuple b3)))
+(assert (= b3_tup (tuple b3)))
(assert (member b3_tup Book))
(declare-fun n () Atom)
(declare-fun n_tup () (Tuple Atom))
-(assert (= n_tup (mkTuple n)))
+(assert (= n_tup (tuple n)))
(assert (member n_tup Name))
(declare-fun t () Atom)
(declare-fun t_tup () (Tuple Atom))
-(assert (= t_tup (mkTuple t)))
+(assert (= t_tup (tuple t)))
(assert (member t_tup Target))
(assert (subset (join (join Book addr) Target) Name))
(assert (subset (join Book names) Name))
(declare-fun x () Atom)
(declare-fun y () Atom)
(assert (not (= x y)))
-(assert (member (mkTuple y) a))
-(assert (member (mkTuple x y) b))
+(assert (member (tuple y) a))
+(assert (member (tuple x y) b))
(assert (= (as univset (Set (Tuple Atom Atom))) (product (as univset (Set (Tuple Atom))) (as univset (Set (Tuple Atom))))))
(declare-fun u () (Set (Tuple Atom Atom)))
(assert (= u (as univset (Set (Tuple Atom Atom)))))
-(assert (not (member (mkTuple x y) u)))
+(assert (not (member (tuple x y) u)))
(check-sat)
(declare-fun id () (Set (Tuple Int Int)))
(declare-fun t () (Set (Tuple Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1) t))
-(assert (member (mkTuple 2) t))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1) t))
+(assert (member (tuple 2) t))
(assert (member z x))
(assert (member zt x))
(assert (member v x))
(assert (member a x))
(assert (= id (iden t)))
-(assert (not (member (mkTuple 1 1) (intersection id x))))
+(assert (not (member (tuple 1 1) (intersection id x))))
(check-sat)
(declare-fun c () Atom)
(declare-fun d () Atom)
(assert (= univ (as univset (Set (Tuple Atom)))))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple c d) x))
+(assert (member (tuple a b) x))
+(assert (member (tuple c d) x))
(assert (not (= a b)))
(assert (= (iden (join x univ)) x))
(check-sat)
(declare-fun w () (Set (Tuple Int unit)))
(declare-fun z () (Set (Tuple unit Int)))
(assert (= (join x y) (join w z)))
-(assert (member (mkTuple 0 1) (join x y)))
-(assert (member (mkTuple 0 u) w))
+(assert (member (tuple 0 1) (join x y)))
+(assert (member (tuple 0 u) w))
(declare-fun t () Int)
(assert (and (> t 0) (< t 3)))
-(assert (not (member (mkTuple u t) z)))
+(assert (not (member (tuple u t) z)))
(check-sat)
(declare-fun w () (Set (Tuple Int unit)))
(declare-fun z () (Set (Tuple unit Int)))
(assert (= (join x y) (join w z)))
-(assert (member (mkTuple 0 1) (join x y)))
-(assert (member (mkTuple 0 u) w))
+(assert (member (tuple 0 1) (join x y)))
+(assert (member (tuple 0 u) w))
(declare-fun t () Int)
(assert (and (> t 0) (< t 2)))
-(assert (not (member (mkTuple u t) z)))
+(assert (not (member (tuple u t) z)))
(check-sat)
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun t () (Set (Tuple Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
(assert (member z x))
-(assert (member (mkTuple 7 5) y))
+(assert (member (tuple 7 5) y))
(assert (= t (join_image x 2)))
-(assert (member (mkTuple 3) (join_image x 2)))
-(assert (not (member (mkTuple 1) (join_image x 2))))
-(assert (member (mkTuple 4) (join_image x 2)))
-(assert (member (mkTuple 1) (join_image x 1)))
+(assert (member (tuple 3) (join_image x 2)))
+(assert (not (member (tuple 1) (join_image x 2))))
+(assert (member (tuple 4) (join_image x 2)))
+(assert (member (tuple 1) (join_image x 1)))
(check-sat)
(declare-fun c () Atom)
(declare-fun J ((Set (Tuple Atom)) (Set (Tuple Atom Atom))) (Set (Tuple Atom)))
(declare-fun T ((Set (Tuple Atom Atom))) (Set (Tuple Atom Atom)))
-(assert (let ((_let_1 (singleton (mkTuple a)))) (= (join _let_1 t) (J _let_1 t))))
-(assert (let ((_let_1 (singleton (mkTuple c)))) (not (= (join _let_1 (tclosure t)) _let_1))))
+(assert (let ((_let_1 (singleton (tuple a)))) (= (join _let_1 t) (J _let_1 t))))
+(assert (let ((_let_1 (singleton (tuple c)))) (not (= (join _let_1 (tclosure t)) _let_1))))
(check-sat)
(declare-fun y () (Set (Tuple Int)))
(declare-fun z () (Set (Tuple Int)))
(declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 2 1)))
+(assert (= b (tuple 2 1)))
(assert (member b x))
(declare-fun a () (Tuple Int))
-(assert (= a (mkTuple 1)))
+(assert (= a (tuple 1)))
(assert (member a y))
(declare-fun c () (Tuple Int))
-(assert (= c (mkTuple 2)))
+(assert (= c (tuple 2)))
(assert (= z (join x y)))
(assert (not (member c z)))
(check-sat)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 f)))
+(assert (= e (tuple 4 f)))
(assert (member e x))
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple g 3)))
+(assert (= d (tuple g 3)))
(assert (member d y))
(assert (= z (union (singleton f) (singleton g))))
(assert (= 0 (- f g)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 3)))
+(assert (= a (tuple 4 3)))
(assert (= r (join x y)))
(assert (not (member a r)))
(check-sat)
(declare-fun z () (Set (Tuple Int)))
(declare-fun r2 () (Set (Tuple Int Int)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 3 1)))
+(assert (= a (tuple 3 1)))
(assert (member a x))
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 1 3)))
+(assert (= d (tuple 1 3)))
(assert (member d y))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
(assert (= r (join x y)))
-(assert (member (mkTuple 1) w))
-(assert (member (mkTuple 2) z))
+(assert (member (tuple 1) w))
+(assert (member (tuple 2) z))
(assert (= r2 (product w z)))
(assert (not (member e r)))
(assert (subset r r2))
-(assert (not (member (mkTuple 3 3) r2)))
+(assert (not (member (tuple 3 3) r2)))
(check-sat)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 4)))
+(assert (= e (tuple 4 4)))
(assert (member e x))
-(assert (not (member (mkTuple 4 4) x)))
+(assert (not (member (tuple 4 4) x)))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 7 5) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 7 5) y))
(assert (member z x))
(assert (member zt y))
(assert (not (member a (join x y))))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 4 3) x))
-(assert (member (mkTuple 7 5) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 4 3) x))
+(assert (member (tuple 7 5) y))
(assert (member z x))
(assert (member zt y))
(assert (member a (join x y)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
(assert (member z x))
(assert (member zt y))
(assert (not (member a (join x y))))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
(assert (member z x))
(assert (member zt y))
(assert (= r (join x y)))
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 2 1 3)))
+(assert (= zt (tuple 2 1 3)))
(declare-fun a () (Tuple Int Int Int))
-(assert (= a (mkTuple 1 1 3)))
+(assert (= a (tuple 1 1 3)))
(assert (member z x))
(assert (member zt y))
(assert (not (member a (join x y))))
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 2 1 3)))
+(assert (= zt (tuple 2 1 3)))
(declare-fun a () (Tuple Int Int Int))
-(assert (= a (mkTuple 1 1 3)))
+(assert (= a (tuple 1 1 3)))
(assert (member z x))
(assert (member zt y))
(assert (member a (join x y)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
(assert (= r (join x y)))
(assert (member z x))
(assert (member zt y))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 7 5) y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 7 5) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
(assert (= r (join x y)))
(assert (member z x))
(assert (member zt y))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
+(assert (= a (tuple 1 5)))
(declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 7 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
+(assert (= b (tuple 7 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
(assert (member b y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
(assert (= r (join x y)))
(assert (member z x))
(assert (member zt y))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 4)))
+(assert (= a (tuple 1 4)))
(assert (= r (join (join (transpose x) y) z)))
(assert (not (member a r)))
(check-sat)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
-(assert (= x (union (singleton (mkTuple 1 2)) (singleton (mkTuple 3 4)))))
-(assert (= y (join x (union (singleton (mkTuple 2 1)) (singleton (mkTuple 4 3))))))
-(assert (not (member (mkTuple 1 1) y)))
+(assert (= x (union (singleton (tuple 1 2)) (singleton (tuple 3 4)))))
+(assert (= y (join x (union (singleton (tuple 2 1)) (singleton (tuple 4 3))))))
+(assert (not (member (tuple 1 1) y)))
(check-sat)
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun w () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 7 5) y))
+(assert (= a (tuple 1 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 7 5) y))
(assert (member z x))
(assert (member zt y))
(assert (= w (union r (join x y))))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int Int Int))
-(assert (= v (mkTuple 1 2 2 1)))
+(assert (= v (tuple 1 2 2 1)))
(assert (member z x))
(assert (member zt y))
(assert (not (member v (product x y))))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int Int Int))
-(assert (= v (mkTuple 1 2 2 1)))
+(assert (= v (tuple 1 2 2 1)))
(assert (member z x))
(assert (member zt y))
(assert (member v (product x y)))
(declare-fun y () (Set (Tuple Int Int Int)))
(declare-fun r () (Set (Tuple Int Int Int)))
(declare-fun z () (Tuple Int Int Int))
-(assert (= z (mkTuple 1 2 3)))
+(assert (= z (tuple 1 2 3)))
(declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 1)))
+(assert (= zt (tuple 3 2 1)))
(declare-fun v () (Tuple Int Int Int Int Int Int))
-(assert (= v (mkTuple 1 2 3 3 2 1)))
+(assert (= v (tuple 1 2 3 3 2 1)))
(assert (member z x))
(assert (member zt y))
(assert (not (member v (product x y))))
(declare-fun y () (Set (Tuple Int Int Int)))
(declare-fun r () (Set (Tuple Int Int Int Int Int Int)))
(declare-fun z () (Tuple Int Int Int))
-(assert (= z (mkTuple 1 2 3)))
+(assert (= z (tuple 1 2 3)))
(declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 1)))
+(assert (= zt (tuple 3 2 1)))
(assert (member z x))
(assert (member zt y))
-(assert (member (mkTuple 1 1 1 1 1 1) r))
+(assert (member (tuple 1 1 1 1 1 1) r))
(assert (= r (product x y)))
(check-sat)
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun f () Int)
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple f 3)))
+(assert (= d (tuple f 3)))
(assert (member d y))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 f)))
+(assert (= e (tuple 4 f)))
(assert (member e x))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 3)))
+(assert (= a (tuple 4 3)))
(assert (= r (join x y)))
(assert (not (member a r)))
(check-sat)
(declare-fun a () (Tuple Int Int))
(assert (member a x))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
(assert (= r (join x y)))
(assert (not (member e r)))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 1 3)))
-(assert (member (mkTuple 1 3) y))
+(assert (= d (tuple 1 3)))
+(assert (member (tuple 1 3) y))
(declare-fun a () (Tuple Int Int))
(assert (member a x))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
(assert (= r (join x y)))
(assert (not (member e r)))
(check-sat)
(declare-fun d () (Tuple Int Int))
(assert (member d y))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 f)))
+(assert (= e (tuple 4 f)))
(assert (member e x))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 3)))
+(assert (= a (tuple 4 3)))
(assert (= r (join x y)))
(assert (not (member a r)))
(check-sat)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int Int Int)))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 5 3) x))
-(assert (member (mkTuple 3 9) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 5 3) x))
+(assert (member (tuple 3 9) x))
(assert (= z (product x y)))
-(assert (member (mkTuple 1 2 3 4) z))
-(assert (not (member (mkTuple 5 9) x)))
-(assert (member (mkTuple 3 8) y))
+(assert (member (tuple 1 2 3 4) z))
+(assert (not (member (tuple 5 9) x)))
+(assert (member (tuple 3 8) y))
(assert (= y (tclosure x)))
-(assert (not (member (mkTuple 1 2) y)))
+(assert (not (member (tuple 1 2) y)))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun e () Int)
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 e)))
+(assert (= a (tuple 1 e)))
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple e 5)))
+(assert (= d (tuple e 5)))
(assert (member a x))
(assert (member d x))
-(assert (not (member (mkTuple 1 1) x)))
-(assert (not (member (mkTuple 1 2) x)))
-(assert (not (member (mkTuple 1 3) x)))
-(assert (not (member (mkTuple 1 4) x)))
-(assert (not (member (mkTuple 1 5) x)))
-(assert (not (member (mkTuple 1 6) x)))
-(assert (not (member (mkTuple 1 7) x)))
+(assert (not (member (tuple 1 1) x)))
+(assert (not (member (tuple 1 2) x)))
+(assert (not (member (tuple 1 3) x)))
+(assert (not (member (tuple 1 4) x)))
+(assert (not (member (tuple 1 5) x)))
+(assert (not (member (tuple 1 6) x)))
+(assert (not (member (tuple 1 7) x)))
(assert (= y (tclosure x)))
-(assert (member (mkTuple 1 5) y))
+(assert (member (tuple 1 5) y))
(check-sat)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
-(assert (member (mkTuple 1 a) x))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 1 d) x))
-(assert (member (mkTuple b 1) x))
+(assert (member (tuple 1 a) x))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 1 d) x))
+(assert (member (tuple b 1) x))
(assert (= b d))
(assert (> b (- d 1)))
(assert (< b (+ d 1)))
(assert (= y (tclosure x)))
-(assert (not (member (mkTuple 1 1) y)))
+(assert (not (member (tuple 1 1) y)))
(check-sat)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
-(assert (member (mkTuple 1 a) x))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 1 d) x))
-(assert (member (mkTuple b 1) x))
+(assert (member (tuple 1 a) x))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 1 d) x))
+(assert (member (tuple b 1) x))
(assert (= b d))
(assert (= y (tclosure x)))
(check-sat)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(assert (= y (join (tclosure x) x)))
-(assert (member (mkTuple 1 2) (join (join x x) x)))
+(assert (member (tuple 1 2) (join (join x x) x)))
(assert (not (subset y (tclosure x))))
(check-sat)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
-(assert (member (mkTuple 2 2) (tclosure x)))
+(assert (member (tuple 2 2) (tclosure x)))
(assert (= x (as emptyset (Set (Tuple Int Int)))))
(check-sat)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
-(assert (member (mkTuple 1 3) x))
-(assert (or (member (mkTuple 2 3) z) (member (mkTuple 2 1) z)))
+(assert (member (tuple 1 3) x))
+(assert (or (member (tuple 2 3) z) (member (tuple 2 1) z)))
(assert (= y (transpose x)))
-(assert (not (member (mkTuple 1 2) y)))
+(assert (not (member (tuple 1 2) y)))
(assert (= x z))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 5 1)))
+(assert (= a (tuple 5 1)))
(declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 7 5)))
-(assert (member (mkTuple 1 7) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 3 4) x))
+(assert (= b (tuple 7 5)))
+(assert (member (tuple 1 7) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 3 4) x))
(assert (member b y))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
(assert (= r (join x y)))
(assert (member z x))
(assert (member zt y))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun b () (Tuple Int Int))
-(assert (= b (mkTuple 1 7)))
+(assert (= b (tuple 1 7)))
(declare-fun c () (Tuple Int Int))
-(assert (= c (mkTuple 2 3)))
+(assert (= c (tuple 2 3)))
(assert (member b x))
(assert (member c x))
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 7 3)))
+(assert (= d (tuple 7 3)))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 7)))
+(assert (= e (tuple 4 7)))
(assert (member d y))
(assert (member e y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 3 4) z))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
(assert (= r (join (join x y) z)))
(assert (not (member a (transpose r))))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
(assert (= r (join (join (transpose x) y) z)))
(assert (not (member a (transpose r))))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
-(assert (member (mkTuple 3 3) w))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
+(assert (member (tuple 3 3) w))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
(assert (not (member a (transpose r))))
(declare-fun zz () (Set (Tuple Int Int)))
(assert (= zz (join (transpose x) y)))
-(assert (not (member (mkTuple 1 3) w)))
-(assert (not (member (mkTuple 1 3) (union w zz))))
+(assert (not (member (tuple 1 3) w)))
+(assert (not (member (tuple 1 3) (union w zz))))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
-(assert (= x (union (singleton (mkTuple 1 7)) (singleton (mkTuple 2 3)))))
+(assert (= x (union (singleton (tuple 1 7)) (singleton (tuple 2 3)))))
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 7 3)))
+(assert (= d (tuple 7 3)))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 7)))
+(assert (= e (tuple 4 7)))
(assert (member d y))
(assert (member e y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 3 4) z))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
(assert (= r (join (join x y) z)))
(assert (not (member a (transpose r))))
(check-sat)
(declare-fun u () Int)
(assert (and (< 4 t) (< t 6)))
(assert (and (< 4 u) (< u 6)))
-(assert (member (mkTuple 1 u) x))
-(assert (member (mkTuple t 3) y))
+(assert (member (tuple 1 u) x))
+(assert (member (tuple t 3) y))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 3)))
+(assert (= a (tuple 1 3)))
(assert (not (member a (join x y))))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int Int Int)))
-(assert (member (mkTuple 2 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 2 2) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 2 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 2 2) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
(declare-fun v () (Tuple Int Int Int Int))
-(assert (= v (mkTuple 4 3 2 1)))
+(assert (= v (tuple 4 3 2 1)))
(assert (= r (product (join (transpose x) y) z)))
(assert (not (member v (transpose r))))
(check-sat)
(declare-fun u () Int)
(assert (and (< 4 t) (< t 6)))
(assert (and (< 4 u) (< u 6)))
-(assert (member (mkTuple 1 t) x))
-(assert (member (mkTuple u 3) y))
+(assert (member (tuple 1 t) x))
+(assert (member (tuple u 3) y))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 3)))
+(assert (= a (tuple 1 3)))
(assert (not (member a (join x y))))
(declare-fun st () (Set Int))
(declare-fun su () (Set Int))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun a () Int)
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(assert (member z x))
(assert (not (member zt (transpose x))))
(assert (= y (transpose x)))
(declare-fun x () (Set (Tuple Int Int Int)))
(declare-fun y () (Set (Tuple Int Int Int)))
(declare-fun z () (Tuple Int Int Int))
-(assert (= z (mkTuple 1 2 3)))
+(assert (= z (tuple 1 2 3)))
(declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 1)))
+(assert (= zt (tuple 3 2 1)))
(assert (member z x))
(assert (not (member zt (transpose x))))
(check-sat)
(declare-fun y () (Set (Tuple Int Int Int)))
(declare-fun z () (Tuple Int Int Int))
(declare-fun a () Int)
-(assert (= z (mkTuple 1 2 a)))
+(assert (= z (tuple 1 2 a)))
(declare-fun zt () (Tuple Int Int Int))
-(assert (= zt (mkTuple 3 2 2)))
+(assert (= zt (tuple 3 2 2)))
(assert (member z x))
(assert (member zt (transpose x)))
(assert (= y (transpose x)))
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(assert (= x y))
(assert (member z x))
(assert (not (member zt (transpose y))))
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(assert (member z x))
-(assert (not (member (mkTuple 2 1) (transpose x))))
+(assert (not (member (tuple 2 1) (transpose x))))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(assert (member zt y))
(declare-fun w () (Tuple Int Int))
-(assert (= w (mkTuple 2 2)))
+(assert (= w (tuple 2 2)))
(assert (member w y))
(assert (member z x))
(assert (not (member zt (transpose (join x y)))))
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(assert (member z x))
-(assert (member (mkTuple 3 4) x))
-(assert (member (mkTuple 3 5) x))
-(assert (member (mkTuple 3 3) x))
+(assert (member (tuple 3 4) x))
+(assert (member (tuple 3 5) x))
+(assert (member (tuple 3 3) x))
(assert (= x (transpose y)))
(assert (not (member zt y)))
(assert (member z y))
(declare-fun lt2 () (Set (Tuple Int Int)))
(declare-fun i () Int)
-(assert (= r1 (insert (mkTuple "a" 1) (mkTuple "b" 2) (mkTuple "c" 3) (singleton (mkTuple "d" 4)))))
-(assert (= r2 (insert (mkTuple 1 "1") (mkTuple 2 "2") (mkTuple 3 "3") (singleton (mkTuple 17 "17")))))
+(assert (= r1 (insert (tuple "a" 1) (tuple "b" 2) (tuple "c" 3) (singleton (tuple "d" 4)))))
+(assert (= r2 (insert (tuple 1 "1") (tuple 2 "2") (tuple 3 "3") (singleton (tuple 17 "17")))))
(assert (= r (join r1 r2)))
(assert (= s (transpose r)))
(assert (= t (product r1 r2)))
-(assert (= lt1 (insert (mkTuple 1 2) (mkTuple 2 3) (mkTuple 3 4) (singleton (mkTuple 4 5)))))
+(assert (= lt1 (insert (tuple 1 2) (tuple 2 3) (tuple 3 4) (singleton (tuple 4 5)))))
(assert (= lt2 (tclosure lt1)))
(assert (= i (card t)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun x () Int)
(declare-fun y () Int)
-(assert (member (mkTuple 1 x) w))
-(assert (member (mkTuple y 2) z))
-(assert (not (member (mkTuple 1 2) (join w z))))
+(assert (member (tuple 1 x) w))
+(assert (member (tuple y 2) z))
+(assert (not (member (tuple 1 2) (join w z))))
(check-sat)
(declare-fun ATOM_UNIV () (Set (Tuple Atom)))
(declare-fun V1 () Atom)
(assert (= C32 (intersection (complement C2) (complement C4))))
-(assert (member (mkTuple V1) (complement C32)))
+(assert (member (tuple V1) (complement C32)))
(assert (= ATOM_UNIV (as univset (Set (Tuple Atom)))))
-(assert (member (mkTuple V1) ATOM_UNIV))
-(assert (member (mkTuple V1) (complement C2)))
+(assert (member (tuple V1) ATOM_UNIV))
+(assert (member (tuple V1) (complement C2)))
(check-sat)
(declare-fun u () (Tuple String String))
(declare-fun v () Tuple)
(declare-fun x () String)
-(assert (= t (mkTuple "a" "b" "c" "d")))
-(assert (= x ((_ tupSel 0) t)))
+(assert (= t (tuple "a" "b" "c" "d")))
+(assert (= x ((_ tuple_select 0) t)))
(assert (= u ((_ tuple_project 2 3) t)))
(assert (= v (tuple_project t)))
(check-sat)
\ No newline at end of file
(declare-fun ev_set () (Set |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|))
(assert (= ev_set (union (singleton ow1) (singleton or2))))
(declare-fun RF () (Set (Tuple |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE| |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)))
-(assert (forall ((r |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|) (w |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)) (=> (and (member r ev_set) (member w ev_set)) (= (member (mkTuple r w) RF) (and (= (O r) R) (= (O w) W))))))
+(assert (forall ((r |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|) (w |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)) (=> (and (member r ev_set) (member w ev_set)) (= (member (tuple r w) RF) (and (= (O r) R) (= (O w) W))))))
(check-sat)
(declare-fun addr () (Set (Tuple Atom Atom Atom)))
(declare-fun b1 () Atom)
(declare-fun b1_tup () (Tuple Atom))
-(assert (= b1_tup (mkTuple b1)))
+(assert (= b1_tup (tuple b1)))
(assert (member b1_tup Book))
(declare-fun b2 () Atom)
(declare-fun b2_tup () (Tuple Atom))
-(assert (= b2_tup (mkTuple b2)))
+(assert (= b2_tup (tuple b2)))
(assert (member b2_tup Book))
(declare-fun b3 () Atom)
(declare-fun b3_tup () (Tuple Atom))
-(assert (= b3_tup (mkTuple b3)))
+(assert (= b3_tup (tuple b3)))
(assert (member b3_tup Book))
(declare-fun m () Atom)
(declare-fun m_tup () (Tuple Atom))
-(assert (= m_tup (mkTuple m)))
+(assert (= m_tup (tuple m)))
(assert (member m_tup Name))
(declare-fun t () Atom)
(declare-fun t_tup () (Tuple Atom))
-(assert (= t_tup (mkTuple t)))
+(assert (= t_tup (tuple t)))
(assert (member t_tup Target))
(assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom)))))
-(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t)))))
-(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t)))))
+(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (tuple m t)))))
+(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (tuple m t)))))
(assert (not (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr))))
(check-sat)
(declare-fun addr () (Set (Tuple Atom Atom Atom)))
(declare-fun b1 () Atom)
(declare-fun b1_tup () (Tuple Atom))
-(assert (= b1_tup (mkTuple b1)))
+(assert (= b1_tup (tuple b1)))
(assert (member b1_tup Book))
(declare-fun b2 () Atom)
(declare-fun b2_tup () (Tuple Atom))
-(assert (= b2_tup (mkTuple b2)))
+(assert (= b2_tup (tuple b2)))
(assert (member b2_tup Book))
(declare-fun b3 () Atom)
(declare-fun b3_tup () (Tuple Atom))
-(assert (= b3_tup (mkTuple b3)))
+(assert (= b3_tup (tuple b3)))
(assert (member b3_tup Book))
(declare-fun m () Atom)
(declare-fun m_tup () (Tuple Atom))
-(assert (= m_tup (mkTuple m)))
+(assert (= m_tup (tuple m)))
(assert (member m_tup Name))
(declare-fun t () Atom)
(declare-fun t_tup () (Tuple Atom))
-(assert (= t_tup (mkTuple t)))
+(assert (= t_tup (tuple t)))
(assert (member t_tup Target))
(assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom)))))
-(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t)))))
-(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t)))))
+(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (tuple m t)))))
+(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (tuple m t)))))
(assert (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr)))
(check-sat)
(declare-fun d () (_ BitVec 1))
(declare-fun e () (_ BitVec 1))
(assert (not (= b c)))
-(assert (member (mkTuple a u b) x))
-(assert (member (mkTuple a u c) x))
-(assert (member (mkTuple d u a) y))
-(assert (not (member (mkTuple a u u a) (join x y))))
+(assert (member (tuple a u b) x))
+(assert (member (tuple a u c) x))
+(assert (member (tuple d u a) y))
+(assert (not (member (tuple a u u a) (join x y))))
(check-sat)
(declare-fun e () (_ BitVec 1))
(declare-fun u () unitb)
(assert (not (= b c)))
-(assert (member (mkTuple a u b) x))
-(assert (member (mkTuple a u c) x))
-(assert (member (mkTuple d u a) y))
-(assert (not (member (mkTuple a u u a) (join x y))))
+(assert (member (tuple a u b) x))
+(assert (member (tuple a u c) x))
+(assert (member (tuple d u a) y))
+(assert (not (member (tuple a u u a) (join x y))))
(check-sat)
(declare-fun d () (_ BitVec 1))
(declare-fun e () (_ BitVec 1))
(assert (not (= b c)))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple a c) x))
-(assert (member (mkTuple d a) y))
-(assert (not (member (mkTuple a a) (join x y))))
+(assert (member (tuple a b) x))
+(assert (member (tuple a c) x))
+(assert (member (tuple d a) y))
+(assert (not (member (tuple a a) (join x y))))
(check-sat)
(declare-fun d () (_ BitVec 2))
(declare-fun e () (_ BitVec 2))
(assert (not (= b c)))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple a c) x))
-(assert (member (mkTuple d a) y))
-(assert (not (member (mkTuple a a) (join x y))))
+(assert (member (tuple a b) x))
+(assert (member (tuple a c) x))
+(assert (member (tuple d a) y))
+(assert (not (member (tuple a a) (join x y))))
(check-sat)
(declare-fun s1 () H_TYPE)
(declare-fun s2 () H_TYPE)
(declare-fun s3 () H_TYPE)
-(assert (= h0 (singleton (mkTuple s0))))
-(assert (= h1 (singleton (mkTuple s1))))
-(assert (= h2 (singleton (mkTuple s2))))
-(assert (= h3 (singleton (mkTuple s3))))
+(assert (= h0 (singleton (tuple s0))))
+(assert (= h1 (singleton (tuple s1))))
+(assert (= h2 (singleton (tuple s2))))
+(assert (= h3 (singleton (tuple s3))))
(declare-fun ref () (Set (Tuple H_TYPE Obj Obj)))
(declare-fun mark () (Set (Tuple H_TYPE Obj)))
(declare-fun empty_obj_set () (Set (Tuple Obj)))
(declare-fun live () Obj)
(assert (= (join h1 mark) empty_obj_set))
(assert (subset (join h0 ref) (join h1 ref)))
-(assert (forall ((n Obj)) (=> (member (mkTuple root n) (tclosure (join h1 ref))) (member (mkTuple n) (join h2 mark)))))
+(assert (forall ((n Obj)) (=> (member (tuple root n) (tclosure (join h1 ref))) (member (tuple n) (join h2 mark)))))
(assert (subset (join h1 ref) (join h2 ref)))
-(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set)))))
-(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref))))))))
-(assert (member (mkTuple root live) (tclosure (join h0 ref))))
-(assert (let ((_let_1 (singleton (mkTuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref))))))
+(assert (forall ((n Obj)) (let ((_let_1 (tuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set)))))
+(assert (forall ((n Obj)) (let ((_let_1 (tuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref))))))))
+(assert (member (tuple root live) (tclosure (join h0 ref))))
+(assert (let ((_let_1 (singleton (tuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref))))))
(check-sat)
(assert (= univ (as univset (Set (Tuple Atom)))))
(assert (= univ2 (as univset (Set (Tuple Atom Atom)))))
(assert (= univ2 (product univ univ)))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple c d) x))
+(assert (member (tuple a b) x))
+(assert (member (tuple c d) x))
(assert (not (= a b)))
(assert (subset (iden univ) x))
(check-sat)
(declare-fun w () (Set (Tuple Int unit)))
(declare-fun z () (Set (Tuple unit Int)))
(assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (and (= _let_2 _let_1) (= _let_2 (transpose _let_1))))))
-(assert (member (mkTuple 0 1) (join x y)))
+(assert (member (tuple 0 1) (join x y)))
(declare-fun t () Int)
(assert (and (>= t 0) (<= t 1)))
(declare-fun s () Int)
(assert (and (>= s 0) (<= s 1)))
(assert (= (+ s t) 1))
-(assert (member (mkTuple s u) w))
-(assert (not (member (mkTuple u t) z)))
+(assert (member (tuple s u) w))
+(assert (not (member (tuple u t) z)))
(check-sat)
(declare-fun w () (Set (Tuple Int unit)))
(declare-fun z () (Set (Tuple unit Int)))
(assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (or (= _let_2 _let_1) (= _let_2 (transpose _let_1))))))
-(assert (member (mkTuple 0 1) (join x y)))
+(assert (member (tuple 0 1) (join x y)))
(declare-fun t () Int)
(assert (and (>= t 0) (<= t 1)))
(declare-fun s () Int)
(assert (and (>= s 0) (<= s 1)))
(assert (= (+ s t) 1))
-(assert (member (mkTuple s u) w))
-(assert (not (member (mkTuple u t) z)))
+(assert (member (tuple s u) w))
+(assert (not (member (tuple u t) z)))
(check-sat)
(declare-fun t () (Set (Tuple Int)))
(declare-fun u () (Set (Tuple Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun v () (Tuple Int Int))
-(assert (= v (mkTuple 1 1)))
+(assert (= v (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
+(assert (= a (tuple 1 5)))
(declare-fun b () Int)
-(assert (member (mkTuple 1 7) x))
+(assert (member (tuple 1 7) x))
(assert (member z x))
-(assert (member (mkTuple 7 5) y))
+(assert (member (tuple 7 5) y))
(assert (= t (join_image x 2)))
-(assert (member (mkTuple 3) (join_image x 2)))
+(assert (member (tuple 3) (join_image x 2)))
(assert (= u (join_image x 1)))
-(assert (member (mkTuple 4) (join_image x 2)))
-(assert (member (mkTuple b) (join_image x 1)))
+(assert (member (tuple 4) (join_image x 2)))
+(assert (member (tuple b) (join_image x 1)))
(check-sat)
(declare-fun u () (Set (Tuple Int)))
(declare-fun univ () (Set (Tuple Int)))
(declare-fun z () (Tuple Int Int))
-(assert (= z (mkTuple 1 2)))
+(assert (= z (tuple 1 2)))
(declare-fun zt () (Tuple Int Int))
-(assert (= zt (mkTuple 2 1)))
+(assert (= zt (tuple 2 1)))
(declare-fun s () (Tuple Int Int))
-(assert (= s (mkTuple 1 1)))
+(assert (= s (tuple 1 1)))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 1 5)))
+(assert (= a (tuple 1 5)))
(declare-fun b () Int)
-(assert (member (mkTuple 1 7) x))
+(assert (member (tuple 1 7) x))
(assert (member z x))
-(assert (member (mkTuple 7 5) y))
+(assert (member (tuple 7 5) y))
(assert (= t (join_image x 2)))
(assert (= univ (join_image x 0)))
-(assert (member (mkTuple 100) t))
-(assert (not (member (mkTuple 3) univ)))
+(assert (member (tuple 100) t))
+(assert (not (member (tuple 3) univ)))
(assert (= u (join_image x 1)))
-(assert (member (mkTuple 4) (join_image x 2)))
-(assert (member (mkTuple b) (join_image x 1)))
+(assert (member (tuple 4) (join_image x 2)))
+(assert (member (tuple b) (join_image x 1)))
(check-sat)
(declare-fun c () Atom)
(declare-fun d () Atom)
(declare-fun e () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
-(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
+(assert (member (tuple a) (join_image x 2)))
+(assert (= x (union (union (singleton (tuple b c)) (singleton (tuple d e))) (singleton (tuple c e)))))
(assert (not (= a b)))
(check-sat)
(declare-fun c () Atom)
(declare-fun d () Atom)
(declare-fun e () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
+(assert (member (tuple a) (join_image x 2)))
(assert (= t (join_image x 2)))
-(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
-(assert (member (mkTuple c) t))
+(assert (= x (union (union (singleton (tuple b c)) (singleton (tuple d e))) (singleton (tuple c e)))))
+(assert (member (tuple c) t))
(check-sat)
(declare-fun e () Atom)
(declare-fun f () Atom)
(declare-fun g () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
-(assert (member (mkTuple a) (join_image y 3)))
-(assert (= x (union (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))) (singleton (mkTuple f b)))))
-(assert (member (mkTuple a f) x))
-(assert (member (mkTuple a f) y))
+(assert (member (tuple a) (join_image x 2)))
+(assert (member (tuple a) (join_image y 3)))
+(assert (= x (union (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e))) (singleton (tuple f b)))))
+(assert (member (tuple a f) x))
+(assert (member (tuple a f) y))
(assert (= x y))
(assert (not (= a b)))
-(assert (not (member (mkTuple d) (join_image x 2))))
+(assert (not (member (tuple d) (join_image x 2))))
(assert (= f d))
(check-sat)
(declare-fun e () Atom)
(declare-fun f () Atom)
(declare-fun g () Atom)
-(assert (member (mkTuple a) (join_image x 2)))
-(assert (member (mkTuple a) (join_image y 1)))
-(assert (= y (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
-(assert (= x (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e)))))
+(assert (member (tuple a) (join_image x 2)))
+(assert (member (tuple a) (join_image y 1)))
+(assert (= y (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e)))))
+(assert (= x (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e)))))
(assert (or (not (= a b)) (not (= a f))))
(check-sat)
(declare-fun z2 () (Set (Tuple Int Int)))
(declare-fun w2 () (Set (Tuple Int Int)))
(assert (not (= z (product x y))))
-(assert (member (mkTuple 0 1 2 3) z))
-(assert (member (mkTuple 0 1) z1))
-(assert (member (mkTuple 0 1) z2))
-(assert (member (mkTuple 2 3) w1))
-(assert (member (mkTuple 2 3) w2))
+(assert (member (tuple 0 1 2 3) z))
+(assert (member (tuple 0 1) z1))
+(assert (member (tuple 0 1) z2))
+(assert (member (tuple 2 3) w1))
+(assert (member (tuple 2 3) w2))
(assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2))))
(check-sat)
(declare-fun P ((Set (Tuple Int Int Int Int))) Bool)
(assert (= z (product x y)))
(assert (P z))
-(assert (not (P (singleton (mkTuple 0 1 2 3)))))
-(assert (member (mkTuple 0 1) z1))
-(assert (member (mkTuple 0 1) z2))
-(assert (member (mkTuple 2 3) w1))
-(assert (member (mkTuple 2 3) w2))
+(assert (not (P (singleton (tuple 0 1 2 3)))))
+(assert (member (tuple 0 1) z1))
+(assert (member (tuple 0 1) z2))
+(assert (member (tuple 2 3) w1))
+(assert (member (tuple 2 3) w2))
(assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2))))
(check-sat)
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun w () (Set (Tuple Int Int)))
(declare-fun f () (Tuple Int Int))
-(assert (= f (mkTuple 3 1)))
+(assert (= f (tuple 3 1)))
(assert (member f x))
(declare-fun g () (Tuple Int Int))
-(assert (= g (mkTuple 1 3)))
+(assert (= g (tuple 1 3)))
(assert (member g y))
(declare-fun h () (Tuple Int Int))
-(assert (= h (mkTuple 3 5)))
+(assert (= h (tuple 3 5)))
(assert (member h x))
(assert (member h y))
(assert (= r (join x y)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun w () (Set (Tuple Int Int)))
(declare-fun f () (Tuple Int Int))
-(assert (= f (mkTuple 3 1)))
+(assert (= f (tuple 3 1)))
(assert (member f x))
(declare-fun g () (Tuple Int Int))
-(assert (= g (mkTuple 1 3)))
+(assert (= g (tuple 1 3)))
(assert (member g y))
(declare-fun h () (Tuple Int Int))
-(assert (= h (mkTuple 3 5)))
+(assert (= h (tuple 3 5)))
(assert (member h x))
(assert (member h y))
(assert (= r (join x y)))
(declare-fun a () Int)
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple a a)))
+(assert (= e (tuple a a)))
(assert (= w (singleton e)))
(assert (subset (transpose w) y))
(assert (not (member e r)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun w () (Set (Tuple Int Int)))
(declare-fun f () (Tuple Int Int))
-(assert (= f (mkTuple 3 1)))
+(assert (= f (tuple 3 1)))
(assert (member f x))
(declare-fun g () (Tuple Int Int))
-(assert (= g (mkTuple 1 3)))
+(assert (= g (tuple 1 3)))
(assert (member g y))
(declare-fun h () (Tuple Int Int))
-(assert (= h (mkTuple 3 5)))
+(assert (= h (tuple 3 5)))
(assert (member h x))
(assert (member h y))
(assert (= r (join x y)))
(declare-fun a () (Tuple Int))
-(assert (= a (mkTuple 1)))
+(assert (= a (tuple 1)))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 1 1)))
+(assert (= e (tuple 1 1)))
(assert (let ((_let_1 (singleton a))) (= w (product _let_1 _let_1))))
(assert (subset (transpose w) y))
(assert (not (member e r)))
(declare-fun z () (Set (Tuple Int)))
(declare-fun r2 () (Set (Tuple Int Int)))
(declare-fun d () (Tuple Int Int))
-(assert (= d (mkTuple 1 3)))
-(assert (member (mkTuple 1 3) y))
+(assert (= d (tuple 1 3)))
+(assert (member (tuple 1 3) y))
(declare-fun a () (Tuple Int Int))
(assert (member a x))
(declare-fun e () (Tuple Int Int))
-(assert (= e (mkTuple 4 3)))
+(assert (= e (tuple 4 3)))
(assert (= r (join x y)))
(assert (= r2 (product w z)))
(assert (not (member e r)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun a11 () (Tuple Int Int))
-(assert (= a11 (mkTuple 1 1)))
+(assert (= a11 (tuple 1 1)))
(assert (member a11 x))
(declare-fun a12 () (Tuple Int Int))
-(assert (= a12 (mkTuple 1 2)))
+(assert (= a12 (tuple 1 2)))
(assert (member a12 x))
(declare-fun a13 () (Tuple Int Int))
-(assert (= a13 (mkTuple 1 3)))
+(assert (= a13 (tuple 1 3)))
(assert (member a13 x))
(declare-fun a14 () (Tuple Int Int))
-(assert (= a14 (mkTuple 1 4)))
+(assert (= a14 (tuple 1 4)))
(assert (member a14 x))
(declare-fun a15 () (Tuple Int Int))
-(assert (= a15 (mkTuple 1 5)))
+(assert (= a15 (tuple 1 5)))
(assert (member a15 x))
(declare-fun a16 () (Tuple Int Int))
-(assert (= a16 (mkTuple 1 6)))
+(assert (= a16 (tuple 1 6)))
(assert (member a16 x))
(declare-fun a17 () (Tuple Int Int))
-(assert (= a17 (mkTuple 1 7)))
+(assert (= a17 (tuple 1 7)))
(assert (member a17 x))
(declare-fun a18 () (Tuple Int Int))
-(assert (= a18 (mkTuple 1 8)))
+(assert (= a18 (tuple 1 8)))
(assert (member a18 x))
(declare-fun a19 () (Tuple Int Int))
-(assert (= a19 (mkTuple 1 9)))
+(assert (= a19 (tuple 1 9)))
(assert (member a19 x))
(declare-fun a110 () (Tuple Int Int))
-(assert (= a110 (mkTuple 1 10)))
+(assert (= a110 (tuple 1 10)))
(assert (member a110 x))
(declare-fun a21 () (Tuple Int Int))
-(assert (= a21 (mkTuple 2 1)))
+(assert (= a21 (tuple 2 1)))
(assert (member a21 x))
(declare-fun a22 () (Tuple Int Int))
-(assert (= a22 (mkTuple 2 2)))
+(assert (= a22 (tuple 2 2)))
(assert (member a22 x))
(declare-fun a23 () (Tuple Int Int))
-(assert (= a23 (mkTuple 2 3)))
+(assert (= a23 (tuple 2 3)))
(assert (member a23 x))
(declare-fun a24 () (Tuple Int Int))
-(assert (= a24 (mkTuple 2 4)))
+(assert (= a24 (tuple 2 4)))
(assert (member a24 x))
(declare-fun a25 () (Tuple Int Int))
-(assert (= a25 (mkTuple 2 5)))
+(assert (= a25 (tuple 2 5)))
(assert (member a25 x))
(declare-fun a26 () (Tuple Int Int))
-(assert (= a26 (mkTuple 2 6)))
+(assert (= a26 (tuple 2 6)))
(assert (member a26 x))
(declare-fun a27 () (Tuple Int Int))
-(assert (= a27 (mkTuple 2 7)))
+(assert (= a27 (tuple 2 7)))
(assert (member a27 x))
(declare-fun a28 () (Tuple Int Int))
-(assert (= a28 (mkTuple 2 8)))
+(assert (= a28 (tuple 2 8)))
(assert (member a28 x))
(declare-fun a29 () (Tuple Int Int))
-(assert (= a29 (mkTuple 2 9)))
+(assert (= a29 (tuple 2 9)))
(assert (member a29 x))
(declare-fun a210 () (Tuple Int Int))
-(assert (= a210 (mkTuple 2 10)))
+(assert (= a210 (tuple 2 10)))
(assert (member a210 x))
(declare-fun a31 () (Tuple Int Int))
-(assert (= a31 (mkTuple 3 1)))
+(assert (= a31 (tuple 3 1)))
(assert (member a31 x))
(declare-fun a32 () (Tuple Int Int))
-(assert (= a32 (mkTuple 3 2)))
+(assert (= a32 (tuple 3 2)))
(assert (member a32 x))
(declare-fun a33 () (Tuple Int Int))
-(assert (= a33 (mkTuple 3 3)))
+(assert (= a33 (tuple 3 3)))
(assert (member a33 x))
(declare-fun a34 () (Tuple Int Int))
-(assert (= a34 (mkTuple 3 4)))
+(assert (= a34 (tuple 3 4)))
(assert (member a34 x))
(declare-fun a35 () (Tuple Int Int))
-(assert (= a35 (mkTuple 3 5)))
+(assert (= a35 (tuple 3 5)))
(assert (member a35 x))
(declare-fun a36 () (Tuple Int Int))
-(assert (= a36 (mkTuple 3 6)))
+(assert (= a36 (tuple 3 6)))
(assert (member a36 x))
(declare-fun a37 () (Tuple Int Int))
-(assert (= a37 (mkTuple 3 7)))
+(assert (= a37 (tuple 3 7)))
(assert (member a37 x))
(declare-fun a38 () (Tuple Int Int))
-(assert (= a38 (mkTuple 3 8)))
+(assert (= a38 (tuple 3 8)))
(assert (member a38 x))
(declare-fun a39 () (Tuple Int Int))
-(assert (= a39 (mkTuple 3 9)))
+(assert (= a39 (tuple 3 9)))
(assert (member a39 x))
(declare-fun a310 () (Tuple Int Int))
-(assert (= a310 (mkTuple 3 10)))
+(assert (= a310 (tuple 3 10)))
(assert (member a310 x))
(declare-fun a41 () (Tuple Int Int))
-(assert (= a41 (mkTuple 4 1)))
+(assert (= a41 (tuple 4 1)))
(assert (member a41 x))
(declare-fun a42 () (Tuple Int Int))
-(assert (= a42 (mkTuple 4 2)))
+(assert (= a42 (tuple 4 2)))
(assert (member a42 x))
(declare-fun a43 () (Tuple Int Int))
-(assert (= a43 (mkTuple 4 3)))
+(assert (= a43 (tuple 4 3)))
(assert (member a43 x))
(declare-fun a44 () (Tuple Int Int))
-(assert (= a44 (mkTuple 4 4)))
+(assert (= a44 (tuple 4 4)))
(assert (member a44 x))
(declare-fun a45 () (Tuple Int Int))
-(assert (= a45 (mkTuple 4 5)))
+(assert (= a45 (tuple 4 5)))
(assert (member a45 x))
(declare-fun a46 () (Tuple Int Int))
-(assert (= a46 (mkTuple 4 6)))
+(assert (= a46 (tuple 4 6)))
(assert (member a46 x))
(declare-fun a47 () (Tuple Int Int))
-(assert (= a47 (mkTuple 4 7)))
+(assert (= a47 (tuple 4 7)))
(assert (member a47 x))
(declare-fun a48 () (Tuple Int Int))
-(assert (= a48 (mkTuple 4 8)))
+(assert (= a48 (tuple 4 8)))
(assert (member a48 x))
(declare-fun a49 () (Tuple Int Int))
-(assert (= a49 (mkTuple 4 9)))
+(assert (= a49 (tuple 4 9)))
(assert (member a49 x))
(declare-fun a410 () (Tuple Int Int))
-(assert (= a410 (mkTuple 4 10)))
+(assert (= a410 (tuple 4 10)))
(assert (member a410 x))
(declare-fun a51 () (Tuple Int Int))
-(assert (= a51 (mkTuple 5 1)))
+(assert (= a51 (tuple 5 1)))
(assert (member a51 x))
(declare-fun a52 () (Tuple Int Int))
-(assert (= a52 (mkTuple 5 2)))
+(assert (= a52 (tuple 5 2)))
(assert (member a52 x))
(declare-fun a53 () (Tuple Int Int))
-(assert (= a53 (mkTuple 5 3)))
+(assert (= a53 (tuple 5 3)))
(assert (member a53 x))
(declare-fun a54 () (Tuple Int Int))
-(assert (= a54 (mkTuple 5 4)))
+(assert (= a54 (tuple 5 4)))
(assert (member a54 x))
(declare-fun a55 () (Tuple Int Int))
-(assert (= a55 (mkTuple 5 5)))
+(assert (= a55 (tuple 5 5)))
(assert (member a55 x))
(declare-fun a56 () (Tuple Int Int))
-(assert (= a56 (mkTuple 5 6)))
+(assert (= a56 (tuple 5 6)))
(assert (member a56 x))
(declare-fun a57 () (Tuple Int Int))
-(assert (= a57 (mkTuple 5 7)))
+(assert (= a57 (tuple 5 7)))
(assert (member a57 x))
(declare-fun a58 () (Tuple Int Int))
-(assert (= a58 (mkTuple 5 8)))
+(assert (= a58 (tuple 5 8)))
(assert (member a58 x))
(declare-fun a59 () (Tuple Int Int))
-(assert (= a59 (mkTuple 5 9)))
+(assert (= a59 (tuple 5 9)))
(assert (member a59 x))
(declare-fun a510 () (Tuple Int Int))
-(assert (= a510 (mkTuple 5 10)))
+(assert (= a510 (tuple 5 10)))
(assert (member a510 x))
(declare-fun a61 () (Tuple Int Int))
-(assert (= a61 (mkTuple 6 1)))
+(assert (= a61 (tuple 6 1)))
(assert (member a61 x))
(declare-fun a62 () (Tuple Int Int))
-(assert (= a62 (mkTuple 6 2)))
+(assert (= a62 (tuple 6 2)))
(assert (member a62 x))
(declare-fun a63 () (Tuple Int Int))
-(assert (= a63 (mkTuple 6 3)))
+(assert (= a63 (tuple 6 3)))
(assert (member a63 x))
(declare-fun a64 () (Tuple Int Int))
-(assert (= a64 (mkTuple 6 4)))
+(assert (= a64 (tuple 6 4)))
(assert (member a64 x))
(declare-fun a65 () (Tuple Int Int))
-(assert (= a65 (mkTuple 6 5)))
+(assert (= a65 (tuple 6 5)))
(assert (member a65 x))
(declare-fun a66 () (Tuple Int Int))
-(assert (= a66 (mkTuple 6 6)))
+(assert (= a66 (tuple 6 6)))
(assert (member a66 x))
(declare-fun a67 () (Tuple Int Int))
-(assert (= a67 (mkTuple 6 7)))
+(assert (= a67 (tuple 6 7)))
(assert (member a67 x))
(declare-fun a68 () (Tuple Int Int))
-(assert (= a68 (mkTuple 6 8)))
+(assert (= a68 (tuple 6 8)))
(assert (member a68 x))
(declare-fun a69 () (Tuple Int Int))
-(assert (= a69 (mkTuple 6 9)))
+(assert (= a69 (tuple 6 9)))
(assert (member a69 x))
(declare-fun a610 () (Tuple Int Int))
-(assert (= a610 (mkTuple 6 10)))
+(assert (= a610 (tuple 6 10)))
(assert (member a610 x))
(declare-fun a71 () (Tuple Int Int))
-(assert (= a71 (mkTuple 7 1)))
+(assert (= a71 (tuple 7 1)))
(assert (member a71 x))
(declare-fun a72 () (Tuple Int Int))
-(assert (= a72 (mkTuple 7 2)))
+(assert (= a72 (tuple 7 2)))
(assert (member a72 x))
(declare-fun a73 () (Tuple Int Int))
-(assert (= a73 (mkTuple 7 3)))
+(assert (= a73 (tuple 7 3)))
(assert (member a73 x))
(declare-fun a74 () (Tuple Int Int))
-(assert (= a74 (mkTuple 7 4)))
+(assert (= a74 (tuple 7 4)))
(assert (member a74 x))
(declare-fun a75 () (Tuple Int Int))
-(assert (= a75 (mkTuple 7 5)))
+(assert (= a75 (tuple 7 5)))
(assert (member a75 x))
(declare-fun a76 () (Tuple Int Int))
-(assert (= a76 (mkTuple 7 6)))
+(assert (= a76 (tuple 7 6)))
(assert (member a76 x))
(declare-fun a77 () (Tuple Int Int))
-(assert (= a77 (mkTuple 7 7)))
+(assert (= a77 (tuple 7 7)))
(assert (member a77 x))
(declare-fun a78 () (Tuple Int Int))
-(assert (= a78 (mkTuple 7 8)))
+(assert (= a78 (tuple 7 8)))
(assert (member a78 x))
(declare-fun a79 () (Tuple Int Int))
-(assert (= a79 (mkTuple 7 9)))
+(assert (= a79 (tuple 7 9)))
(assert (member a79 x))
(declare-fun a710 () (Tuple Int Int))
-(assert (= a710 (mkTuple 7 10)))
+(assert (= a710 (tuple 7 10)))
(assert (member a710 x))
(declare-fun a81 () (Tuple Int Int))
-(assert (= a81 (mkTuple 8 1)))
+(assert (= a81 (tuple 8 1)))
(assert (member a81 x))
(declare-fun a82 () (Tuple Int Int))
-(assert (= a82 (mkTuple 8 2)))
+(assert (= a82 (tuple 8 2)))
(assert (member a82 x))
(declare-fun a83 () (Tuple Int Int))
-(assert (= a83 (mkTuple 8 3)))
+(assert (= a83 (tuple 8 3)))
(assert (member a83 x))
(declare-fun a84 () (Tuple Int Int))
-(assert (= a84 (mkTuple 8 4)))
+(assert (= a84 (tuple 8 4)))
(assert (member a84 x))
(declare-fun a85 () (Tuple Int Int))
-(assert (= a85 (mkTuple 8 5)))
+(assert (= a85 (tuple 8 5)))
(assert (member a85 x))
(declare-fun a86 () (Tuple Int Int))
-(assert (= a86 (mkTuple 8 6)))
+(assert (= a86 (tuple 8 6)))
(assert (member a86 x))
(declare-fun a87 () (Tuple Int Int))
-(assert (= a87 (mkTuple 8 7)))
+(assert (= a87 (tuple 8 7)))
(assert (member a87 x))
(declare-fun a88 () (Tuple Int Int))
-(assert (= a88 (mkTuple 8 8)))
+(assert (= a88 (tuple 8 8)))
(assert (member a88 x))
(declare-fun a89 () (Tuple Int Int))
-(assert (= a89 (mkTuple 8 9)))
+(assert (= a89 (tuple 8 9)))
(assert (member a89 x))
(declare-fun a810 () (Tuple Int Int))
-(assert (= a810 (mkTuple 8 10)))
+(assert (= a810 (tuple 8 10)))
(assert (member a810 x))
(declare-fun a91 () (Tuple Int Int))
-(assert (= a91 (mkTuple 9 1)))
+(assert (= a91 (tuple 9 1)))
(assert (member a91 x))
(declare-fun a92 () (Tuple Int Int))
-(assert (= a92 (mkTuple 9 2)))
+(assert (= a92 (tuple 9 2)))
(assert (member a92 x))
(declare-fun a93 () (Tuple Int Int))
-(assert (= a93 (mkTuple 9 3)))
+(assert (= a93 (tuple 9 3)))
(assert (member a93 x))
(declare-fun a94 () (Tuple Int Int))
-(assert (= a94 (mkTuple 9 4)))
+(assert (= a94 (tuple 9 4)))
(assert (member a94 x))
(declare-fun a95 () (Tuple Int Int))
-(assert (= a95 (mkTuple 9 5)))
+(assert (= a95 (tuple 9 5)))
(assert (member a95 x))
(declare-fun a96 () (Tuple Int Int))
-(assert (= a96 (mkTuple 9 6)))
+(assert (= a96 (tuple 9 6)))
(assert (member a96 x))
(declare-fun a97 () (Tuple Int Int))
-(assert (= a97 (mkTuple 9 7)))
+(assert (= a97 (tuple 9 7)))
(assert (member a97 x))
(declare-fun a98 () (Tuple Int Int))
-(assert (= a98 (mkTuple 9 8)))
+(assert (= a98 (tuple 9 8)))
(assert (member a98 x))
(declare-fun a99 () (Tuple Int Int))
-(assert (= a99 (mkTuple 9 9)))
+(assert (= a99 (tuple 9 9)))
(assert (member a99 x))
(declare-fun a910 () (Tuple Int Int))
-(assert (= a910 (mkTuple 9 10)))
+(assert (= a910 (tuple 9 10)))
(assert (member a910 x))
(declare-fun a101 () (Tuple Int Int))
-(assert (= a101 (mkTuple 10 1)))
+(assert (= a101 (tuple 10 1)))
(assert (member a101 x))
(declare-fun a102 () (Tuple Int Int))
-(assert (= a102 (mkTuple 10 2)))
+(assert (= a102 (tuple 10 2)))
(assert (member a102 x))
(declare-fun a103 () (Tuple Int Int))
-(assert (= a103 (mkTuple 10 3)))
+(assert (= a103 (tuple 10 3)))
(assert (member a103 x))
(declare-fun a104 () (Tuple Int Int))
-(assert (= a104 (mkTuple 10 4)))
+(assert (= a104 (tuple 10 4)))
(assert (member a104 x))
(declare-fun a105 () (Tuple Int Int))
-(assert (= a105 (mkTuple 10 5)))
+(assert (= a105 (tuple 10 5)))
(assert (member a105 x))
(declare-fun a106 () (Tuple Int Int))
-(assert (= a106 (mkTuple 10 6)))
+(assert (= a106 (tuple 10 6)))
(assert (member a106 x))
(declare-fun a107 () (Tuple Int Int))
-(assert (= a107 (mkTuple 10 7)))
+(assert (= a107 (tuple 10 7)))
(assert (member a107 x))
(declare-fun a108 () (Tuple Int Int))
-(assert (= a108 (mkTuple 10 8)))
+(assert (= a108 (tuple 10 8)))
(assert (member a108 x))
(declare-fun a109 () (Tuple Int Int))
-(assert (= a109 (mkTuple 10 9)))
+(assert (= a109 (tuple 10 9)))
(assert (member a109 x))
(declare-fun a1010 () (Tuple Int Int))
-(assert (= a1010 (mkTuple 10 10)))
+(assert (= a1010 (tuple 10 10)))
(assert (member a1010 x))
(declare-fun b11 () (Tuple Int Int))
-(assert (= b11 (mkTuple 1 1)))
+(assert (= b11 (tuple 1 1)))
(assert (member b11 y))
(declare-fun b12 () (Tuple Int Int))
-(assert (= b12 (mkTuple 1 2)))
+(assert (= b12 (tuple 1 2)))
(assert (member b12 y))
(declare-fun b13 () (Tuple Int Int))
-(assert (= b13 (mkTuple 1 3)))
+(assert (= b13 (tuple 1 3)))
(assert (member b13 y))
(declare-fun b14 () (Tuple Int Int))
-(assert (= b14 (mkTuple 1 4)))
+(assert (= b14 (tuple 1 4)))
(assert (member b14 y))
(declare-fun b15 () (Tuple Int Int))
-(assert (= b15 (mkTuple 1 5)))
+(assert (= b15 (tuple 1 5)))
(assert (member b15 y))
(declare-fun b16 () (Tuple Int Int))
-(assert (= b16 (mkTuple 1 6)))
+(assert (= b16 (tuple 1 6)))
(assert (member b16 y))
(declare-fun b17 () (Tuple Int Int))
-(assert (= b17 (mkTuple 1 7)))
+(assert (= b17 (tuple 1 7)))
(assert (member b17 y))
(declare-fun b18 () (Tuple Int Int))
-(assert (= b18 (mkTuple 1 8)))
+(assert (= b18 (tuple 1 8)))
(assert (member b18 y))
(declare-fun b19 () (Tuple Int Int))
-(assert (= b19 (mkTuple 1 9)))
+(assert (= b19 (tuple 1 9)))
(assert (member b19 y))
(declare-fun b110 () (Tuple Int Int))
-(assert (= b110 (mkTuple 1 10)))
+(assert (= b110 (tuple 1 10)))
(assert (member b110 y))
(declare-fun b21 () (Tuple Int Int))
-(assert (= b21 (mkTuple 2 1)))
+(assert (= b21 (tuple 2 1)))
(assert (member b21 y))
(declare-fun b22 () (Tuple Int Int))
-(assert (= b22 (mkTuple 2 2)))
+(assert (= b22 (tuple 2 2)))
(assert (member b22 y))
(declare-fun b23 () (Tuple Int Int))
-(assert (= b23 (mkTuple 2 3)))
+(assert (= b23 (tuple 2 3)))
(assert (member b23 y))
(declare-fun b24 () (Tuple Int Int))
-(assert (= b24 (mkTuple 2 4)))
+(assert (= b24 (tuple 2 4)))
(assert (member b24 y))
(declare-fun b25 () (Tuple Int Int))
-(assert (= b25 (mkTuple 2 5)))
+(assert (= b25 (tuple 2 5)))
(assert (member b25 y))
(declare-fun b26 () (Tuple Int Int))
-(assert (= b26 (mkTuple 2 6)))
+(assert (= b26 (tuple 2 6)))
(assert (member b26 y))
(declare-fun b27 () (Tuple Int Int))
-(assert (= b27 (mkTuple 2 7)))
+(assert (= b27 (tuple 2 7)))
(assert (member b27 y))
(declare-fun b28 () (Tuple Int Int))
-(assert (= b28 (mkTuple 2 8)))
+(assert (= b28 (tuple 2 8)))
(assert (member b28 y))
(declare-fun b29 () (Tuple Int Int))
-(assert (= b29 (mkTuple 2 9)))
+(assert (= b29 (tuple 2 9)))
(assert (member b29 y))
(declare-fun b210 () (Tuple Int Int))
-(assert (= b210 (mkTuple 2 10)))
+(assert (= b210 (tuple 2 10)))
(assert (member b210 y))
(declare-fun b31 () (Tuple Int Int))
-(assert (= b31 (mkTuple 3 1)))
+(assert (= b31 (tuple 3 1)))
(assert (member b31 y))
(declare-fun b32 () (Tuple Int Int))
-(assert (= b32 (mkTuple 3 2)))
+(assert (= b32 (tuple 3 2)))
(assert (member b32 y))
(declare-fun b33 () (Tuple Int Int))
-(assert (= b33 (mkTuple 3 3)))
+(assert (= b33 (tuple 3 3)))
(assert (member b33 y))
(declare-fun b34 () (Tuple Int Int))
-(assert (= b34 (mkTuple 3 4)))
+(assert (= b34 (tuple 3 4)))
(assert (member b34 y))
(declare-fun b35 () (Tuple Int Int))
-(assert (= b35 (mkTuple 3 5)))
+(assert (= b35 (tuple 3 5)))
(assert (member b35 y))
(declare-fun b36 () (Tuple Int Int))
-(assert (= b36 (mkTuple 3 6)))
+(assert (= b36 (tuple 3 6)))
(assert (member b36 y))
(declare-fun b37 () (Tuple Int Int))
-(assert (= b37 (mkTuple 3 7)))
+(assert (= b37 (tuple 3 7)))
(assert (member b37 y))
(declare-fun b38 () (Tuple Int Int))
-(assert (= b38 (mkTuple 3 8)))
+(assert (= b38 (tuple 3 8)))
(assert (member b38 y))
(declare-fun b39 () (Tuple Int Int))
-(assert (= b39 (mkTuple 3 9)))
+(assert (= b39 (tuple 3 9)))
(assert (member b39 y))
(declare-fun b310 () (Tuple Int Int))
-(assert (= b310 (mkTuple 3 10)))
+(assert (= b310 (tuple 3 10)))
(assert (member b310 y))
(declare-fun b41 () (Tuple Int Int))
-(assert (= b41 (mkTuple 4 1)))
+(assert (= b41 (tuple 4 1)))
(assert (member b41 y))
(declare-fun b42 () (Tuple Int Int))
-(assert (= b42 (mkTuple 4 2)))
+(assert (= b42 (tuple 4 2)))
(assert (member b42 y))
(declare-fun b43 () (Tuple Int Int))
-(assert (= b43 (mkTuple 4 3)))
+(assert (= b43 (tuple 4 3)))
(assert (member b43 y))
(declare-fun b44 () (Tuple Int Int))
-(assert (= b44 (mkTuple 4 4)))
+(assert (= b44 (tuple 4 4)))
(assert (member b44 y))
(declare-fun b45 () (Tuple Int Int))
-(assert (= b45 (mkTuple 4 5)))
+(assert (= b45 (tuple 4 5)))
(assert (member b45 y))
(declare-fun b46 () (Tuple Int Int))
-(assert (= b46 (mkTuple 4 6)))
+(assert (= b46 (tuple 4 6)))
(assert (member b46 y))
(declare-fun b47 () (Tuple Int Int))
-(assert (= b47 (mkTuple 4 7)))
+(assert (= b47 (tuple 4 7)))
(assert (member b47 y))
(declare-fun b48 () (Tuple Int Int))
-(assert (= b48 (mkTuple 4 8)))
+(assert (= b48 (tuple 4 8)))
(assert (member b48 y))
(declare-fun b49 () (Tuple Int Int))
-(assert (= b49 (mkTuple 4 9)))
+(assert (= b49 (tuple 4 9)))
(assert (member b49 y))
(declare-fun b410 () (Tuple Int Int))
-(assert (= b410 (mkTuple 4 10)))
+(assert (= b410 (tuple 4 10)))
(assert (member b410 y))
(declare-fun b51 () (Tuple Int Int))
-(assert (= b51 (mkTuple 5 1)))
+(assert (= b51 (tuple 5 1)))
(assert (member b51 y))
(declare-fun b52 () (Tuple Int Int))
-(assert (= b52 (mkTuple 5 2)))
+(assert (= b52 (tuple 5 2)))
(assert (member b52 y))
(declare-fun b53 () (Tuple Int Int))
-(assert (= b53 (mkTuple 5 3)))
+(assert (= b53 (tuple 5 3)))
(assert (member b53 y))
(declare-fun b54 () (Tuple Int Int))
-(assert (= b54 (mkTuple 5 4)))
+(assert (= b54 (tuple 5 4)))
(assert (member b54 y))
(declare-fun b55 () (Tuple Int Int))
-(assert (= b55 (mkTuple 5 5)))
+(assert (= b55 (tuple 5 5)))
(assert (member b55 y))
(declare-fun b56 () (Tuple Int Int))
-(assert (= b56 (mkTuple 5 6)))
+(assert (= b56 (tuple 5 6)))
(assert (member b56 y))
(declare-fun b57 () (Tuple Int Int))
-(assert (= b57 (mkTuple 5 7)))
+(assert (= b57 (tuple 5 7)))
(assert (member b57 y))
(declare-fun b58 () (Tuple Int Int))
-(assert (= b58 (mkTuple 5 8)))
+(assert (= b58 (tuple 5 8)))
(assert (member b58 y))
(declare-fun b59 () (Tuple Int Int))
-(assert (= b59 (mkTuple 5 9)))
+(assert (= b59 (tuple 5 9)))
(assert (member b59 y))
(declare-fun b510 () (Tuple Int Int))
-(assert (= b510 (mkTuple 5 10)))
+(assert (= b510 (tuple 5 10)))
(assert (member b510 y))
(declare-fun b61 () (Tuple Int Int))
-(assert (= b61 (mkTuple 6 1)))
+(assert (= b61 (tuple 6 1)))
(assert (member b61 y))
(declare-fun b62 () (Tuple Int Int))
-(assert (= b62 (mkTuple 6 2)))
+(assert (= b62 (tuple 6 2)))
(assert (member b62 y))
(declare-fun b63 () (Tuple Int Int))
-(assert (= b63 (mkTuple 6 3)))
+(assert (= b63 (tuple 6 3)))
(assert (member b63 y))
(declare-fun b64 () (Tuple Int Int))
-(assert (= b64 (mkTuple 6 4)))
+(assert (= b64 (tuple 6 4)))
(assert (member b64 y))
(declare-fun b65 () (Tuple Int Int))
-(assert (= b65 (mkTuple 6 5)))
+(assert (= b65 (tuple 6 5)))
(assert (member b65 y))
(declare-fun b66 () (Tuple Int Int))
-(assert (= b66 (mkTuple 6 6)))
+(assert (= b66 (tuple 6 6)))
(assert (member b66 y))
(declare-fun b67 () (Tuple Int Int))
-(assert (= b67 (mkTuple 6 7)))
+(assert (= b67 (tuple 6 7)))
(assert (member b67 y))
(declare-fun b68 () (Tuple Int Int))
-(assert (= b68 (mkTuple 6 8)))
+(assert (= b68 (tuple 6 8)))
(assert (member b68 y))
(declare-fun b69 () (Tuple Int Int))
-(assert (= b69 (mkTuple 6 9)))
+(assert (= b69 (tuple 6 9)))
(assert (member b69 y))
(declare-fun b610 () (Tuple Int Int))
-(assert (= b610 (mkTuple 6 10)))
+(assert (= b610 (tuple 6 10)))
(assert (member b610 y))
(declare-fun b71 () (Tuple Int Int))
-(assert (= b71 (mkTuple 7 1)))
+(assert (= b71 (tuple 7 1)))
(assert (member b71 y))
(declare-fun b72 () (Tuple Int Int))
-(assert (= b72 (mkTuple 7 2)))
+(assert (= b72 (tuple 7 2)))
(assert (member b72 y))
(declare-fun b73 () (Tuple Int Int))
-(assert (= b73 (mkTuple 7 3)))
+(assert (= b73 (tuple 7 3)))
(assert (member b73 y))
(declare-fun b74 () (Tuple Int Int))
-(assert (= b74 (mkTuple 7 4)))
+(assert (= b74 (tuple 7 4)))
(assert (member b74 y))
(declare-fun b75 () (Tuple Int Int))
-(assert (= b75 (mkTuple 7 5)))
+(assert (= b75 (tuple 7 5)))
(assert (member b75 y))
(declare-fun b76 () (Tuple Int Int))
-(assert (= b76 (mkTuple 7 6)))
+(assert (= b76 (tuple 7 6)))
(assert (member b76 y))
(declare-fun b77 () (Tuple Int Int))
-(assert (= b77 (mkTuple 7 7)))
+(assert (= b77 (tuple 7 7)))
(assert (member b77 y))
(declare-fun b78 () (Tuple Int Int))
-(assert (= b78 (mkTuple 7 8)))
+(assert (= b78 (tuple 7 8)))
(assert (member b78 y))
(declare-fun b79 () (Tuple Int Int))
-(assert (= b79 (mkTuple 7 9)))
+(assert (= b79 (tuple 7 9)))
(assert (member b79 y))
(declare-fun b710 () (Tuple Int Int))
-(assert (= b710 (mkTuple 7 10)))
+(assert (= b710 (tuple 7 10)))
(assert (member b710 y))
(declare-fun b81 () (Tuple Int Int))
-(assert (= b81 (mkTuple 8 1)))
+(assert (= b81 (tuple 8 1)))
(assert (member b81 y))
(declare-fun b82 () (Tuple Int Int))
-(assert (= b82 (mkTuple 8 2)))
+(assert (= b82 (tuple 8 2)))
(assert (member b82 y))
(declare-fun b83 () (Tuple Int Int))
-(assert (= b83 (mkTuple 8 3)))
+(assert (= b83 (tuple 8 3)))
(assert (member b83 y))
(declare-fun b84 () (Tuple Int Int))
-(assert (= b84 (mkTuple 8 4)))
+(assert (= b84 (tuple 8 4)))
(assert (member b84 y))
(declare-fun b85 () (Tuple Int Int))
-(assert (= b85 (mkTuple 8 5)))
+(assert (= b85 (tuple 8 5)))
(assert (member b85 y))
(declare-fun b86 () (Tuple Int Int))
-(assert (= b86 (mkTuple 8 6)))
+(assert (= b86 (tuple 8 6)))
(assert (member b86 y))
(declare-fun b87 () (Tuple Int Int))
-(assert (= b87 (mkTuple 8 7)))
+(assert (= b87 (tuple 8 7)))
(assert (member b87 y))
(declare-fun b88 () (Tuple Int Int))
-(assert (= b88 (mkTuple 8 8)))
+(assert (= b88 (tuple 8 8)))
(assert (member b88 y))
(declare-fun b89 () (Tuple Int Int))
-(assert (= b89 (mkTuple 8 9)))
+(assert (= b89 (tuple 8 9)))
(assert (member b89 y))
(declare-fun b810 () (Tuple Int Int))
-(assert (= b810 (mkTuple 8 10)))
+(assert (= b810 (tuple 8 10)))
(assert (member b810 y))
(declare-fun b91 () (Tuple Int Int))
-(assert (= b91 (mkTuple 9 1)))
+(assert (= b91 (tuple 9 1)))
(assert (member b91 y))
(declare-fun b92 () (Tuple Int Int))
-(assert (= b92 (mkTuple 9 2)))
+(assert (= b92 (tuple 9 2)))
(assert (member b92 y))
(declare-fun b93 () (Tuple Int Int))
-(assert (= b93 (mkTuple 9 3)))
+(assert (= b93 (tuple 9 3)))
(assert (member b93 y))
(declare-fun b94 () (Tuple Int Int))
-(assert (= b94 (mkTuple 9 4)))
+(assert (= b94 (tuple 9 4)))
(assert (member b94 y))
(declare-fun b95 () (Tuple Int Int))
-(assert (= b95 (mkTuple 9 5)))
+(assert (= b95 (tuple 9 5)))
(assert (member b95 y))
(declare-fun b96 () (Tuple Int Int))
-(assert (= b96 (mkTuple 9 6)))
+(assert (= b96 (tuple 9 6)))
(assert (member b96 y))
(declare-fun b97 () (Tuple Int Int))
-(assert (= b97 (mkTuple 9 7)))
+(assert (= b97 (tuple 9 7)))
(assert (member b97 y))
(declare-fun b98 () (Tuple Int Int))
-(assert (= b98 (mkTuple 9 8)))
+(assert (= b98 (tuple 9 8)))
(assert (member b98 y))
(declare-fun b99 () (Tuple Int Int))
-(assert (= b99 (mkTuple 9 9)))
+(assert (= b99 (tuple 9 9)))
(assert (member b99 y))
(declare-fun b910 () (Tuple Int Int))
-(assert (= b910 (mkTuple 9 10)))
+(assert (= b910 (tuple 9 10)))
(assert (member b910 y))
(declare-fun b101 () (Tuple Int Int))
-(assert (= b101 (mkTuple 10 1)))
+(assert (= b101 (tuple 10 1)))
(assert (member b101 y))
(declare-fun b102 () (Tuple Int Int))
-(assert (= b102 (mkTuple 10 2)))
+(assert (= b102 (tuple 10 2)))
(assert (member b102 y))
(declare-fun b103 () (Tuple Int Int))
-(assert (= b103 (mkTuple 10 3)))
+(assert (= b103 (tuple 10 3)))
(assert (member b103 y))
(declare-fun b104 () (Tuple Int Int))
-(assert (= b104 (mkTuple 10 4)))
+(assert (= b104 (tuple 10 4)))
(assert (member b104 y))
(declare-fun b105 () (Tuple Int Int))
-(assert (= b105 (mkTuple 10 5)))
+(assert (= b105 (tuple 10 5)))
(assert (member b105 y))
(declare-fun b106 () (Tuple Int Int))
-(assert (= b106 (mkTuple 10 6)))
+(assert (= b106 (tuple 10 6)))
(assert (member b106 y))
(declare-fun b107 () (Tuple Int Int))
-(assert (= b107 (mkTuple 10 7)))
+(assert (= b107 (tuple 10 7)))
(assert (member b107 y))
(declare-fun b108 () (Tuple Int Int))
-(assert (= b108 (mkTuple 10 8)))
+(assert (= b108 (tuple 10 8)))
(assert (member b108 y))
(declare-fun b109 () (Tuple Int Int))
-(assert (= b109 (mkTuple 10 9)))
+(assert (= b109 (tuple 10 9)))
(assert (member b109 y))
(declare-fun b1010 () (Tuple Int Int))
-(assert (= b1010 (mkTuple 10 10)))
+(assert (= b1010 (tuple 10 10)))
(assert (member b1010 y))
-(assert (member (mkTuple 1 9) z))
+(assert (member (tuple 1 9) z))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 9 1)))
+(assert (= a (tuple 9 1)))
(assert (= r (join (join (transpose x) y) z)))
(assert (not (member a (transpose r))))
(check-sat)
(declare-fun d () Int)
(assert (= a c))
(assert (= a d))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 2 d) x))
-(assert (member (mkTuple a 5) y))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 2 d) x))
+(assert (member (tuple a 5) y))
(assert (= y (tclosure x)))
-(assert (member (mkTuple 2 5) y))
+(assert (member (tuple 2 5) y))
(check-sat)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
-(assert (member (mkTuple 1 a) x))
-(assert (member (mkTuple 1 c) x))
-(assert (member (mkTuple 1 d) x))
-(assert (member (mkTuple b 1) x))
+(assert (member (tuple 1 a) x))
+(assert (member (tuple 1 c) x))
+(assert (member (tuple 1 d) x))
+(assert (member (tuple b 1) x))
(assert (= b d))
-(assert (member (mkTuple 2 b) (join (join x x) x)))
-(assert (not (member (mkTuple 2 1) (tclosure x))))
+(assert (member (tuple 2 b) (join (join x x) x)))
+(assert (not (member (tuple 2 1) (tclosure x))))
(check-sat)
(declare-fun w () (Set (Tuple Int Int)))
(assert (= z (tclosure x)))
(assert (= w (join x y)))
-(assert (member (mkTuple 2 2) z))
-(assert (member (mkTuple 0 3) y))
-(assert (member (mkTuple (- 1) 3) y))
-(assert (member (mkTuple 1 3) y))
-(assert (member (mkTuple (- 2) 3) y))
-(assert (member (mkTuple 2 3) y))
-(assert (member (mkTuple 3 3) y))
-(assert (member (mkTuple 4 3) y))
-(assert (member (mkTuple 5 3) y))
-(assert (not (member (mkTuple 2 3) (join x y))))
-(assert (not (member (mkTuple 2 1) x)))
+(assert (member (tuple 2 2) z))
+(assert (member (tuple 0 3) y))
+(assert (member (tuple (- 1) 3) y))
+(assert (member (tuple 1 3) y))
+(assert (member (tuple (- 2) 3) y))
+(assert (member (tuple 2 3) y))
+(assert (member (tuple 3 3) y))
+(assert (member (tuple 4 3) y))
+(assert (member (tuple 5 3) y))
+(assert (not (member (tuple 2 3) (join x y))))
+(assert (not (member (tuple 2 1) x)))
(check-sat)
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
-(assert (member (mkTuple 7 1) x))
-(assert (member (mkTuple 2 3) x))
-(assert (member (mkTuple 7 3) y))
-(assert (member (mkTuple 4 7) y))
-(assert (member (mkTuple 3 4) z))
+(assert (member (tuple 7 1) x))
+(assert (member (tuple 2 3) x))
+(assert (member (tuple 7 3) y))
+(assert (member (tuple 4 7) y))
+(assert (member (tuple 3 4) z))
(declare-fun a () (Tuple Int Int))
-(assert (= a (mkTuple 4 1)))
+(assert (= a (tuple 4 1)))
(assert (= r (join (join (transpose x) y) z)))
(assert (member a (transpose r)))
(check-sat)
(assert (member a x))
(assert (member b y))
(assert (member b w))
-(assert (member (mkTuple x y) z))
-(assert (member (mkTuple w x) z))
-(assert (not (member (mkTuple x x) (join z z))))
-(assert (member (mkTuple x (singleton (mkTuple 0 0))) (join z z)))
+(assert (member (tuple x y) z))
+(assert (member (tuple w x) z))
+(assert (not (member (tuple x x) (join z z))))
+(assert (member (tuple x (singleton (tuple 0 0))) (join z z)))
(check-sat)
(assert (not (= a b)))
(assert (member a z))
(assert (member b z))
-(assert (member (mkTuple a b) x))
-(assert (member (mkTuple b a) x))
+(assert (member (tuple a b) x))
+(assert (member (tuple b a) x))
(assert (member c x))
-(assert (and (not (= c (mkTuple a b))) (not (= c (mkTuple b a)))))
+(assert (and (not (= c (tuple a b))) (not (= c (tuple b a)))))
(check-sat)
(declare-fun d () (Set (Tuple String String)))
(declare-fun f () (Set Int))
(declare-fun e () Int)
-(assert (= b (insert (mkTuple "" 1) (mkTuple "" 2) (singleton (mkTuple "" 4)))))
-(assert (= c (insert (mkTuple 1 "1") (mkTuple 2 "2") (singleton (mkTuple 7 "")))))
+(assert (= b (insert (tuple "" 1) (tuple "" 2) (singleton (tuple "" 4)))))
+(assert (= c (insert (tuple 1 "1") (tuple 2 "2") (singleton (tuple 7 "")))))
(assert (= d (join b c)))
(assert (= e (card f)))
(check-sat)
(declare-fun a () (Set (Tuple Real Int)))
(declare-fun b () (Set (Tuple Int Real)))
(declare-fun x () (Tuple Real Real))
-(assert (let ((_let_1 0.0)) (not (= x (mkTuple _let_1 _let_1)))))
-(assert (member (mkTuple ((_ tupSel 0) x) (to_int ((_ tupSel 1) x))) a))
-(assert (member (mkTuple (to_int ((_ tupSel 0) x)) ((_ tupSel 1) x)) b))
-(assert (not (= ((_ tupSel 0) x) ((_ tupSel 1) x))))
+(assert (let ((_let_1 0.0)) (not (= x (tuple _let_1 _let_1)))))
+(assert (member (tuple ((_ tuple_select 0) x) (to_int ((_ tuple_select 1) x))) a))
+(assert (member (tuple (to_int ((_ tuple_select 0) x)) ((_ tuple_select 1) x)) b))
+(assert (not (= ((_ tuple_select 0) x) ((_ tuple_select 1) x))))
(check-sat)
}
ASSERT_EQ(
- "((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton "
+ "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (singleton "
"\"Z\")))",
projection.toString());
}
projects / cvc5.git / commitdiff