(set-logic QF_UFLIA) ; min/max on Int (define (min (x Int) (y Int)) (ite (< x y) x y)) (define (max (x Int) (y Int)) (ite (> x y) x y)) ;;;BEGIN GENERATED SET (declare-fun count (Int Int) Int) (declare-fun item (Int) Int) (declare-fun empty () Int) (declare-fun e0 () Int) (declare-fun e1 () Int) (declare-fun e2 () Int) (declare-fun e3 () Int) (declare-fun e4 () Int) (declare-fun e5 () Int) (declare-fun e6 () Int) (declare-fun e7 () Int) (assert (= (count empty e0) 0)) (assert (= (count empty e1) 0)) (assert (= (count empty e2) 0)) (assert (= (count empty e3) 0)) (assert (= (count empty e4) 0)) (assert (= (count empty e5) 0)) (assert (= (count empty e6) 0)) (assert (= (count empty e7) 0)) (assert (= (count (item e0) e0) (ite (= e0 e0) 1 0))) (assert (= (count (item e0) e1) (ite (= e0 e1) 1 0))) (assert (= (count (item e0) e2) (ite (= e0 e2) 1 0))) (assert (= (count (item e0) e3) (ite (= e0 e3) 1 0))) (assert (= (count (item e0) e4) (ite (= e0 e4) 1 0))) (assert (= (count (item e0) e5) (ite (= e0 e5) 1 0))) (assert (= (count (item e0) e6) (ite (= e0 e6) 1 0))) (assert (= (count (item e0) e7) (ite (= e0 e7) 1 0))) (assert (= (count (item e1) e0) (ite (= e1 e0) 1 0))) (assert (= (count (item e1) e1) (ite (= e1 e1) 1 0))) (assert (= (count (item e1) e2) (ite (= e1 e2) 1 0))) (assert (= (count (item e1) e3) (ite (= e1 e3) 1 0))) (assert (= (count (item e1) e4) (ite (= e1 e4) 1 0))) (assert (= (count (item e1) e5) (ite (= e1 e5) 1 0))) (assert (= (count (item e1) e6) (ite (= e1 e6) 1 0))) (assert (= (count (item e1) e7) (ite (= e1 e7) 1 0))) (assert (= (count (item e2) e0) (ite (= e2 e0) 1 0))) (assert (= (count (item e2) e1) (ite (= e2 e1) 1 0))) (assert (= (count (item e2) e2) (ite (= e2 e2) 1 0))) (assert (= (count (item e2) e3) (ite (= e2 e3) 1 0))) (assert (= (count (item e2) e4) (ite (= e2 e4) 1 0))) (assert (= (count (item e2) e5) (ite (= e2 e5) 1 0))) (assert (= (count (item e2) e6) (ite (= e2 e6) 1 0))) (assert (= (count (item e2) e7) (ite (= e2 e7) 1 0))) (assert (= (count (item e3) e0) (ite (= e3 e0) 1 0))) (assert (= (count (item e3) e1) (ite (= e3 e1) 1 0))) (assert (= (count (item e3) e2) (ite (= e3 e2) 1 0))) (assert (= (count (item e3) e3) (ite (= e3 e3) 1 0))) (assert (= (count (item e3) e4) (ite (= e3 e4) 1 0))) (assert (= (count (item e3) e5) (ite (= e3 e5) 1 0))) (assert (= (count (item e3) e6) (ite (= e3 e6) 1 0))) (assert (= (count (item e3) e7) (ite (= e3 e7) 1 0))) (assert (= (count (item e4) e0) (ite (= e4 e0) 1 0))) (assert (= (count (item e4) e1) (ite (= e4 e1) 1 0))) (assert (= (count (item e4) e2) (ite (= e4 e2) 1 0))) (assert (= (count (item e4) e3) (ite (= e4 e3) 1 0))) (assert (= (count (item e4) e4) (ite (= e4 e4) 1 0))) (assert (= (count (item e4) e5) (ite (= e4 e5) 1 0))) (assert (= (count (item e4) e6) (ite (= e4 e6) 1 0))) (assert (= (count (item e4) e7) (ite (= e4 e7) 1 0))) (assert (= (count (item e5) e0) (ite (= e5 e0) 1 0))) (assert (= (count (item e5) e1) (ite (= e5 e1) 1 0))) (assert (= (count (item e5) e2) (ite (= e5 e2) 1 0))) (assert (= (count (item e5) e3) (ite (= e5 e3) 1 0))) (assert (= (count (item e5) e4) (ite (= e5 e4) 1 0))) (assert (= (count (item e5) e5) (ite (= e5 e5) 1 0))) (assert (= (count (item e5) e6) (ite (= e5 e6) 1 0))) (assert (= (count (item e5) e7) (ite (= e5 e7) 1 0))) (assert (= (count (item e6) e0) (ite (= e6 e0) 1 0))) (assert (= (count (item e6) e1) (ite (= e6 e1) 1 0))) (assert (= (count (item e6) e2) (ite (= e6 e2) 1 0))) (assert (= (count (item e6) e3) (ite (= e6 e3) 1 0))) (assert (= (count (item e6) e4) (ite (= e6 e4) 1 0))) (assert (= (count (item e6) e5) (ite (= e6 e5) 1 0))) (assert (= (count (item e6) e6) (ite (= e6 e6) 1 0))) (assert (= (count (item e6) e7) (ite (= e6 e7) 1 0))) (assert (= (count (item e7) e0) (ite (= e7 e0) 1 0))) (assert (= (count (item e7) e1) (ite (= e7 e1) 1 0))) (assert (= (count (item e7) e2) (ite (= e7 e2) 1 0))) (assert (= (count (item e7) e3) (ite (= e7 e3) 1 0))) (assert (= (count (item e7) e4) (ite (= e7 e4) 1 0))) (assert (= (count (item e7) e5) (ite (= e7 e5) 1 0))) (assert (= (count (item e7) e6) (ite (= e7 e6) 1 0))) (assert (= (count (item e7) e7) (ite (= e7 e7) 1 0))) (define (mset-well-formed (s Int)) (and (>= (count s e0) 0) (>= (count s e1) 0) (>= (count s e2) 0) (>= (count s e3) 0) (>= (count s e4) 0) (>= (count s e5) 0) (>= (count s e6) 0) (>= (count s e7) 0) )) (define (eq (s Int) (t Int)) (and (= (count s e0) (count t e0)) (= (count s e1) (count t e1)) (= (count s e2) (count t e2)) (= (count s e3) (count t e3)) (= (count s e4) (count t e4)) (= (count s e5) (count t e5)) (= (count s e6) (count t e6)) (= (count s e7) (count t e7)) )) (define (in (e Int) (s Int)) (and (> (count s e0) 0) (> (count s e1) 0) (> (count s e2) 0) (> (count s e3) 0) (> (count s e4) 0) (> (count s e5) 0) (> (count s e6) 0) (> (count s e7) 0) )) (define (union (u Int) (v Int) (s Int)) (and (= (count s e0) (+ (count u e0) (count v e0))) (= (count s e1) (+ (count u e1) (count v e1))) (= (count s e2) (+ (count u e2) (count v e2))) (= (count s e3) (+ (count u e3) (count v e3))) (= (count s e4) (+ (count u e4) (count v e4))) (= (count s e5) (+ (count u e5) (count v e5))) (= (count s e6) (+ (count u e6) (count v e6))) (= (count s e7) (+ (count u e7) (count v e7))) )) (define (union3 (t Int) (u Int) (v Int) (s Int)) (and (= (count s e0) (+ (count t e0) (count u e0) (count v e0))) (= (count s e1) (+ (count t e1) (count u e1) (count v e1))) (= (count s e2) (+ (count t e2) (count u e2) (count v e2))) (= (count s e3) (+ (count t e3) (count u e3) (count v e3))) (= (count s e4) (+ (count t e4) (count u e4) (count v e4))) (= (count s e5) (+ (count t e5) (count u e5) (count v e5))) (= (count s e6) (+ (count t e6) (count u e6) (count v e6))) (= (count s e7) (+ (count t e7) (count u e7) (count v e7))) )) (define (diff (u Int) (v Int) (s Int)) (and (= (count s e0) (ite (> (count u e0) (count v e0)) (- (count u e0) (count v e0)) 0)) (= (count s e1) (ite (> (count u e1) (count v e1)) (- (count u e1) (count v e1)) 0)) (= (count s e2) (ite (> (count u e2) (count v e2)) (- (count u e2) (count v e2)) 0)) (= (count s e3) (ite (> (count u e3) (count v e3)) (- (count u e3) (count v e3)) 0)) (= (count s e4) (ite (> (count u e4) (count v e4)) (- (count u e4) (count v e4)) 0)) (= (count s e5) (ite (> (count u e5) (count v e5)) (- (count u e5) (count v e5)) 0)) (= (count s e6) (ite (> (count u e6) (count v e6)) (- (count u e6) (count v e6)) 0)) (= (count s e7) (ite (> (count u e7) (count v e7)) (- (count u e7) (count v e7)) 0)) )) (define (leq (s Int) (t Int)) (and (or (= (count s e0) 0) (= (count t e1) 0) (<= e0 e1)) (or (= (count s e0) 0) (= (count t e2) 0) (<= e0 e2)) (or (= (count s e0) 0) (= (count t e3) 0) (<= e0 e3)) (or (= (count s e0) 0) (= (count t e4) 0) (<= e0 e4)) (or (= (count s e0) 0) (= (count t e5) 0) (<= e0 e5)) (or (= (count s e0) 0) (= (count t e6) 0) (<= e0 e6)) (or (= (count s e0) 0) (= (count t e7) 0) (<= e0 e7)) (or (= (count s e1) 0) (= (count t e0) 0) (<= e1 e0)) (or (= (count s e1) 0) (= (count t e2) 0) (<= e1 e2)) (or (= (count s e1) 0) (= (count t e3) 0) (<= e1 e3)) (or (= (count s e1) 0) (= (count t e4) 0) (<= e1 e4)) (or (= (count s e1) 0) (= (count t e5) 0) (<= e1 e5)) (or (= (count s e1) 0) (= (count t e6) 0) (<= e1 e6)) (or (= (count s e1) 0) (= (count t e7) 0) (<= e1 e7)) (or (= (count s e2) 0) (= (count t e0) 0) (<= e2 e0)) (or (= (count s e2) 0) (= (count t e1) 0) (<= e2 e1)) (or (= (count s e2) 0) (= (count t e3) 0) (<= e2 e3)) (or (= (count s e2) 0) (= (count t e4) 0) (<= e2 e4)) (or (= (count s e2) 0) (= (count t e5) 0) (<= e2 e5)) (or (= (count s e2) 0) (= (count t e6) 0) (<= e2 e6)) (or (= (count s e2) 0) (= (count t e7) 0) (<= e2 e7)) (or (= (count s e3) 0) (= (count t e0) 0) (<= e3 e0)) (or (= (count s e3) 0) (= (count t e1) 0) (<= e3 e1)) (or (= (count s e3) 0) (= (count t e2) 0) (<= e3 e2)) (or (= (count s e3) 0) (= (count t e4) 0) (<= e3 e4)) (or (= (count s e3) 0) (= (count t e5) 0) (<= e3 e5)) (or (= (count s e3) 0) (= (count t e6) 0) (<= e3 e6)) (or (= (count s e3) 0) (= (count t e7) 0) (<= e3 e7)) (or (= (count s e4) 0) (= (count t e0) 0) (<= e4 e0)) (or (= (count s e4) 0) (= (count t e1) 0) (<= e4 e1)) (or (= (count s e4) 0) (= (count t e2) 0) (<= e4 e2)) (or (= (count s e4) 0) (= (count t e3) 0) (<= e4 e3)) (or (= (count s e4) 0) (= (count t e5) 0) (<= e4 e5)) (or (= (count s e4) 0) (= (count t e6) 0) (<= e4 e6)) (or (= (count s e4) 0) (= (count t e7) 0) (<= e4 e7)) (or (= (count s e5) 0) (= (count t e0) 0) (<= e5 e0)) (or (= (count s e5) 0) (= (count t e1) 0) (<= e5 e1)) (or (= (count s e5) 0) (= (count t e2) 0) (<= e5 e2)) (or (= (count s e5) 0) (= (count t e3) 0) (<= e5 e3)) (or (= (count s e5) 0) (= (count t e4) 0) (<= e5 e4)) (or (= (count s e5) 0) (= (count t e6) 0) (<= e5 e6)) (or (= (count s e5) 0) (= (count t e7) 0) (<= e5 e7)) (or (= (count s e6) 0) (= (count t e0) 0) (<= e6 e0)) (or (= (count s e6) 0) (= (count t e1) 0) (<= e6 e1)) (or (= (count s e6) 0) (= (count t e2) 0) (<= e6 e2)) (or (= (count s e6) 0) (= (count t e3) 0) (<= e6 e3)) (or (= (count s e6) 0) (= (count t e4) 0) (<= e6 e4)) (or (= (count s e6) 0) (= (count t e5) 0) (<= e6 e5)) (or (= (count s e6) 0) (= (count t e7) 0) (<= e6 e7)) (or (= (count s e7) 0) (= (count t e0) 0) (<= e7 e0)) (or (= (count s e7) 0) (= (count t e1) 0) (<= e7 e1)) (or (= (count s e7) 0) (= (count t e2) 0) (<= e7 e2)) (or (= (count s e7) 0) (= (count t e3) 0) (<= e7 e3)) (or (= (count s e7) 0) (= (count t e4) 0) (<= e7 e4)) (or (= (count s e7) 0) (= (count t e5) 0) (<= e7 e5)) (or (= (count s e7) 0) (= (count t e6) 0) (<= e7 e6)) )) (define (lt (s Int) (t Int)) (and (or (= (count s e0) 0) (= (count t e1) 0) (< e0 e1)) (or (= (count s e0) 0) (= (count t e2) 0) (< e0 e2)) (or (= (count s e0) 0) (= (count t e3) 0) (< e0 e3)) (or (= (count s e0) 0) (= (count t e4) 0) (< e0 e4)) (or (= (count s e0) 0) (= (count t e5) 0) (< e0 e5)) (or (= (count s e0) 0) (= (count t e6) 0) (< e0 e6)) (or (= (count s e0) 0) (= (count t e7) 0) (< e0 e7)) (or (= (count s e1) 0) (= (count t e0) 0) (< e1 e0)) (or (= (count s e1) 0) (= (count t e2) 0) (< e1 e2)) (or (= (count s e1) 0) (= (count t e3) 0) (< e1 e3)) (or (= (count s e1) 0) (= (count t e4) 0) (< e1 e4)) (or (= (count s e1) 0) (= (count t e5) 0) (< e1 e5)) (or (= (count s e1) 0) (= (count t e6) 0) (< e1 e6)) (or (= (count s e1) 0) (= (count t e7) 0) (< e1 e7)) (or (= (count s e2) 0) (= (count t e0) 0) (< e2 e0)) (or (= (count s e2) 0) (= (count t e1) 0) (< e2 e1)) (or (= (count s e2) 0) (= (count t e3) 0) (< e2 e3)) (or (= (count s e2) 0) (= (count t e4) 0) (< e2 e4)) (or (= (count s e2) 0) (= (count t e5) 0) (< e2 e5)) (or (= (count s e2) 0) (= (count t e6) 0) (< e2 e6)) (or (= (count s e2) 0) (= (count t e7) 0) (< e2 e7)) (or (= (count s e3) 0) (= (count t e0) 0) (< e3 e0)) (or (= (count s e3) 0) (= (count t e1) 0) (< e3 e1)) (or (= (count s e3) 0) (= (count t e2) 0) (< e3 e2)) (or (= (count s e3) 0) (= (count t e4) 0) (< e3 e4)) (or (= (count s e3) 0) (= (count t e5) 0) (< e3 e5)) (or (= (count s e3) 0) (= (count t e6) 0) (< e3 e6)) (or (= (count s e3) 0) (= (count t e7) 0) (< e3 e7)) (or (= (count s e4) 0) (= (count t e0) 0) (< e4 e0)) (or (= (count s e4) 0) (= (count t e1) 0) (< e4 e1)) (or (= (count s e4) 0) (= (count t e2) 0) (< e4 e2)) (or (= (count s e4) 0) (= (count t e3) 0) (< e4 e3)) (or (= (count s e4) 0) (= (count t e5) 0) (< e4 e5)) (or (= (count s e4) 0) (= (count t e6) 0) (< e4 e6)) (or (= (count s e4) 0) (= (count t e7) 0) (< e4 e7)) (or (= (count s e5) 0) (= (count t e0) 0) (< e5 e0)) (or (= (count s e5) 0) (= (count t e1) 0) (< e5 e1)) (or (= (count s e5) 0) (= (count t e2) 0) (< e5 e2)) (or (= (count s e5) 0) (= (count t e3) 0) (< e5 e3)) (or (= (count s e5) 0) (= (count t e4) 0) (< e5 e4)) (or (= (count s e5) 0) (= (count t e6) 0) (< e5 e6)) (or (= (count s e5) 0) (= (count t e7) 0) (< e5 e7)) (or (= (count s e6) 0) (= (count t e0) 0) (< e6 e0)) (or (= (count s e6) 0) (= (count t e1) 0) (< e6 e1)) (or (= (count s e6) 0) (= (count t e2) 0) (< e6 e2)) (or (= (count s e6) 0) (= (count t e3) 0) (< e6 e3)) (or (= (count s e6) 0) (= (count t e4) 0) (< e6 e4)) (or (= (count s e6) 0) (= (count t e5) 0) (< e6 e5)) (or (= (count s e6) 0) (= (count t e7) 0) (< e6 e7)) (or (= (count s e7) 0) (= (count t e0) 0) (< e7 e0)) (or (= (count s e7) 0) (= (count t e1) 0) (< e7 e1)) (or (= (count s e7) 0) (= (count t e2) 0) (< e7 e2)) (or (= (count s e7) 0) (= (count t e3) 0) (< e7 e3)) (or (= (count s e7) 0) (= (count t e4) 0) (< e7 e4)) (or (= (count s e7) 0) (= (count t e5) 0) (< e7 e5)) (or (= (count s e7) 0) (= (count t e6) 0) (< e7 e6)) )) ;;;END GENERATED SET ; Trees (declare-sort Int) (declare-fun nil () Int) (declare-fun left (Int Int) Int) (declare-fun right (Int Int) Int) (declare-fun value (Int Int) Int) (declare-fun height (Int Int) Int) (declare-fun color (Int Int) Bool) ; BST (declare-fun bst (Int Int) Bool) (declare-fun keys (Int Int) Int) ; RBT (declare-fun rbt (Int Int) Bool) (declare-fun srbt (Int Int) Bool) (declare-fun c (Int Int) Bool) (declare-fun bh (Int Int) Int) (define (red) true) (define (black) false) ; RBT (define (unroll-keys (t Int) (vi Int) (li Int) (ri Int) (ki Int) (lki Int) (rki Int)) (or (and (= t nil) (= (keys ki t) empty) ) (and (not (= t nil)) (union3 (keys lki (left li t)) (item (value vi t)) (keys rki (right ri t)) (keys ki t)) ; axiom (mset-well-formed (keys lki (left li t))) ; axiom (mset-well-formed (keys rki (right ri t))) ) )) (define (unroll-c (t Int) (cfi Int) (ci Int)) (or (and (= t nil) (= (c ci t) black) ) (and (not (= t nil)) (= (c ci t) (color cfi t)) ) )) (define (unroll-bh (t Int) (cfi Int) (li Int) (bhi Int) (lbhi Int)) (or (and (= t nil) (= (bh bhi t) 0) ) (and (not (= t nil)) (= (bh bhi t) (+ (ite (= (color cfi t) black) 1 0) (bh lbhi (left li t)))) ; axiom (>= (bh lbhi (left li t)) 0) ) )) (define (unroll-srbt-funs (t Int) (vi Int) (cfi Int) (li Int) (ri Int) (ki Int) (lki Int) (rki Int) (ci Int) (lci Int) (rci Int) (bhi Int) (lbhi Int) (rbhi Int)) (and (unroll-keys t vi li ri ki lki rki) (unroll-c t cfi ci) (unroll-bh t cfi li bhi lbhi) )) (define (unroll-srbt-cons (t Int) (vi Int) (cfi Int) (li Int) (ri Int) (ki Int) (lki Int) (rki Int) (ci Int) (lci Int) (rci Int) (bhi Int) (lbhi Int) (rbhi Int)) (ite (= t nil) true (and (leq (keys lki (left li t)) (item (value vi t))) (leq (item (value vi t)) (keys rki (right ri t))) (= (bh lbhi (left li t)) (bh rbhi (right ri t))) (or (= (c ci t) black) (and (= (c lci (left li t)) black) (= (c rci (right ri t)) black)) ) ) ) ) (define (unroll-srbt (t Int) (vi Int) (cfi Int) (li Int) (ri Int) (srbti Int) (lsrbti Int) (rsrbti Int) (ki Int) (lki Int) (rki Int) (ci Int) (lci Int) (rci Int) (bhi Int) (lbhi Int) (rbhi Int)) (and (=> (srbt srbti t) (and (unroll-srbt-cons t vi cfi li ri ki lki rki ci lci rci bhi lbhi rbhi) (srbt lsrbti (left li t)) (srbt rsrbti (right ri t)) ) ) (unroll-srbt-funs t vi cfi li ri ki lki rki ci lci rci bhi lbhi rbhi) )) (define (insert2-pre (t Int) (srbti Int) (ki Int)) (and (srbt srbti t) (mset-well-formed (keys ki t)) ) ) (define (insert2-post-assert (t1 Int) (ki1 Int) (ci1 Int) (bhi1 Int) (v Int) (t2 Int) (vi2 Int) (cfi2 Int) (li2 Int) (ri2 Int) (ki2 Int) (lki2 Int) (rki2 Int) (ci2 Int) (lci2 Int) (rci2 Int) (bhi2 Int) (lbhi2 Int) (rbhi2 Int)) (and (not (= t2 nil)) (leq (keys lki2 (left li2 t2)) (item (value vi2 t2))) (leq (item (value vi2 t2)) (keys rki2 (right ri2 t2))) (= (bh lbhi2 (left li2 t2)) (bh rbhi2 (right ri2 t2))) (or (= (c ci2 t2) black) (and (= (c lci2 (left li2 t2)) black) (= (c rci2 (right ri2 t2)) black)) (and (= (c ci1 t1) red) (or (= (c lci2 (left li2 t2)) black)(= (c rci2 (right ri2 t2)) black)) ) ) (union (keys ki1 t1) (item v) (keys ki2 t2)) (= (bh bhi1 t1) (bh bhi2 t2)) ) ) (define (insert2-post-assume (t1 Int) (ki1 Int) (ci1 Int) (bhi1 Int) (v Int) (t2 Int) (vi2 Int) (cfi2 Int) (li2 Int) (ri2 Int) (srbti Int) (lsrbti2 Int) (rsrbti2 Int) (ki2 Int) (lki2 Int) (rki2 Int) (ci2 Int) (lci2 Int) (rci2 Int) (bhi2 Int) (lbhi2 Int) (rbhi2 Int)) (and (insert2-post-assert t1 ki1 ci1 bhi1 v t2 vi2 cfi2 li2 ri2 ki2 lki2 rki2 ci2 lci2 rci2 bhi2 lbhi2 rbhi2) (unroll-srbt-funs t2 vi2 cfi2 li2 ri2 ki2 lki2 rki2 ci2 lci2 rci2 bhi2 lbhi2 rbhi2) (srbt lsrbti2 (left li2 t2)) (srbt rsrbti2 (right ri2 t2)) ) ) (define (delete2-pre (t Int) (srbti Int) (ki Int) (bhi Int)) (and (srbt srbti t) (mset-well-formed (keys ki t)) (>= (bh bhi t) 0) ) ) (define (delete2-post-assert (t1 Int) (ki1 Int) (ci1 Int) (bhi1 Int) (v Int) (t2 Int) (ki2 Int) (ci2 Int) (bhi2 Int) (fixed Bool)) (and (diff (keys ki1 t1) (item v) (keys ki2 t2)) (or (= (c ci2 t2) (c ci1 t1)) (= (c ci2 t2) black)) (or (and (= (bh bhi2 t2) (bh bhi1 t1)) fixed) (and (= (bh bhi2 t2) (- (bh bhi1 t1) 1)) (= (c ci2 t2) black) (not fixed) ) ) (>= (bh bhi2 t2) 0) ) ) (define (delete2-post-assume (t1 Int) (ki1 Int) (ci1 Int) (bhi1 Int) (v Int) (t2 Int) (srbti2 Int) (ki2 Int) (ci2 Int) (bhi2 Int) (fixed Bool)) (and (delete2-post-assert t1 ki1 ci1 bhi1 v t2 ki2 ci2 bhi2 fixed) (srbt srbti2 t2) ) ) (define (left-delete-fixup-pre (t Int) (vi Int) (cfi Int) (li Int) (ri Int) (srbti Int) (lsrbti Int) (rsrbti Int) (ki Int) (lki Int) (rki Int) (ci Int) (lci Int) (rci Int) (bhi Int) (lbhi Int) (rbhi Int) (fixed Bool)) (and (not fixed) (not (= t nil)) (leq (keys lki (left li t)) (item (value vi t))) (leq (item (value vi t)) (keys rki (right ri t))) (or (= (c ci t) black) (and (= (c lci (left li t)) black) (= (c rci (right ri t)) black)) ) (= (c lci (left li t)) black) (= (bh lbhi (left li t)) (- (bh rbhi (right ri t)) 1)) (srbt lsrbti (left li t)) (srbt rsrbti (right ri t)) ) ) (define (left-delete-fixup-post-assert (t1 Int) (ki1 Int) (ci1 Int) (li1 Int) (lbhi1 Int) (t2 Int) (ki2 Int) (ci2 Int) (bhi2 Int) (fixed Bool)) (and (eq (keys ki2 t2) (keys ki1 t1)) (or (= (c ci2 t2) (c ci1 t1)) (= (c ci2 t2) black)) (or (and (= (bh bhi2 t2) (+ (bh lbhi1 (left li1 t1)) (ite (= (c ci1 t1) black) 1 0) 1)) fixed ) (and (= (bh bhi2 t2) (+ (bh lbhi1 (left li1 t1)) (ite (= (c ci1 t1) black) 1 0))) (= (c ci1 t1) black) (= (c ci2 t2) black) (not fixed) ) ) (>= (bh bhi2 t2) 0) ) ) (define (left-delete-fixup-post-assume (t1 Int) (ki1 Int) (ci1 Int) (li1 Int) (lbhi1 Int) (t2 Int) (srbti2 Int) (ki2 Int) (ci2 Int) (bhi2 Int) (fixed Bool)) (and (left-delete-fixup-post-assert t1 ki1 ci1 li1 lbhi1 t2 ki2 ci2 bhi2 fixed) (srbt srbti2 t2) ) ) (define (right-delete-fixup-pre (t Int) (vi Int) (cfi Int) (li Int) (ri Int) (srbti Int) (lsrbti Int) (rsrbti Int) (ki Int) (lki Int) (rki Int) (ci Int) (lci Int) (rci Int) (bhi Int) (lbhi Int) (rbhi Int) (fixed Bool)) (and (not fixed) (not (= t nil)) (leq (keys lki (left li t)) (item (value vi t))) (leq (item (value vi t)) (keys rki (right ri t))) (or (= (c ci t) black) (and (= (c lci (left li t)) black) (= (c rci (right ri t)) black)) ) (= (c rci (right ri t)) black) (= (bh rbhi (right ri t)) (- (bh lbhi (left li t)) 1)) (srbt lsrbti (left li t)) (srbt rsrbti (right ri t)) ) ) (define (right-delete-fixup-post-assert (t1 Int) (ki1 Int) (ci1 Int) (ri1 Int) (rbhi1 Int) (t2 Int) (ki2 Int) (ci2 Int) (bhi2 Int) (fixed Bool)) (and (eq (keys ki2 t2) (keys ki1 t1)) (or (= (c ci2 t2) (c ci1 t1)) (= (c ci2 t2) black)) (or (and (= (bh bhi2 t2) (+ (bh rbhi1 (right ri1 t1)) (ite (= (c ci1 t1) black) 1 0) 1)) fixed ) (and (= (bh bhi2 t2) (+ (bh rbhi1 (right ri1 t1)) (ite (= (c ci1 t1) black) 1 0))) (= (c ci1 t1) black) (= (c ci2 t2) black) (not fixed) ) ) (>= (bh bhi2 t2) 0) ) ) (define (right-delete-fixup-post-assume (t1 Int) (ki1 Int) (ci1 Int) (ri1 Int) (rbhi1 Int) (t2 Int) (srbti2 Int) (ki2 Int) (ci2 Int) (bhi2 Int) (fixed Bool)) (and (right-delete-fixup-post-assert t1 ki1 ci1 ri1 rbhi1 t2 ki2 ci2 bhi2 fixed) (srbt srbti2 t2) ) ) ; extra states (declare-fun v0 () Int) (declare-fun v1 () Int) (declare-fun t0 () Int) (declare-fun t1 () Int) (declare-fun t2 () Int) (declare-fun t3 () Int) (declare-fun fixed0 () Bool) (declare-fun fixed1 () Bool) ; declare multiset elements ;(assert (= e1 v0)) ;(assert (= e2 (value 0 t0))) ;(assert (= e3 (value 0 (left 1 t0)))) ;(assert (= e4 (value 0 (right 0 (left 1 t0))))) ;(assert (= e5 (value 0 (right 1 t0)))) ;(assert (= e6 (value 0 (left 0 (right 1 t0))))) ;(assert (= e7 (value 1 t0))) ;(assert (= e8 (value 1 (left 0 t0)))) ;(assert (= e9 (value 1 (right 1 (left 0 t0))))) ;(assert (= e10 (value 0 (left 0 t0)))) ;(assert (= e11 (value 0 (right 1 (left 0 t0))))) ;(assert (= e12 (value 0 (right 0 t0)))) ;(assert (= e13 (value 0 (left 1 (right 0 t0))))) ;;;;;;;;;;;;;; ; RBT insert ; ;;;;;;;;;;;;;; ; path 0 (define trail0 (and (= t0 nil) (unroll-srbt t0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) ; (not (= t1 nil)) (= (value 0 t1) v0) (= (color 0 t1) red) (= (left 0 t1) nil) (= (right 0 t1) nil) )) ; VC0 (define vc0 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail0 (unroll-srbt-funs t1 0 0 0 0 0 0 0 0 0 0 0 0 0) (unroll-srbt-funs (left 0 t1) 0 0 0 0 0 0 0 0 0 0 0 0 0) (unroll-srbt-funs (right 0 t1) 0 0 0 0 0 0 0 0 0 0 0 0 0) ) (and (insert2-post-assert t0 0 0 0 v0 t1 0 0 0 0 0 0 0 0 0 0 0 0 0) (unroll-srbt-cons (left 0 t1) 0 0 0 0 0 0 0 0 0 0 0 0 0) (unroll-srbt-cons (right 0 t1) 0 0 0 0 0 0 0 0 0 0 0 0 0) ) ))) ; path 1 (define trail1 (and (not (= t0 nil)) ; (unroll-srbt t0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e1 (value 0 t0)) ; register mset element (< v0 (value 0 t0)) )) ; VC1 (define vc1 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail1 ) (and (insert2-pre (left 0 t0) 0 0) ) ))) ; path 2 (define trail2 (and trail1 ; (insert2-post-assume (left 0 t0) 0 0 0 v0 (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e2 (value 0 (left 1 t0))) ; register mset element ; (= (c 0 (left 1 t0)) red) ; (= (c 0 (right 0 t0)) red) ; (or (= (c 0 (left 1 (left 1 t0))) red) (= (c 0 (right 0 (left 1 t0))) red)) ; (unroll-srbt (right 0 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e3 (value 0 (right 0 t0))) ; register mset element (= (color 1 t0) red) (= (color 1 (left 1 t0)) black) (= (color 1 (right 0 t0)) black) )) ; VC2 (define vc2 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail2 (unroll-srbt-funs t0 0 1 1 0 1 0 0 1 1 1 1 1 1) (unroll-srbt-funs (left 1 t0) 0 1 1 0 0 0 0 1 0 0 1 0 0) (unroll-srbt-funs (right 0 t0) 0 1 1 0 0 0 0 1 0 0 1 0 0) ) (and (insert2-post-assert t0 0 0 0 v0 t0 0 1 1 0 1 0 0 1 1 1 1 1 1) (unroll-srbt-cons (left 1 t0) 0 1 1 0 0 0 0 1 0 0 1 0 0) (unroll-srbt-cons (right 0 t0) 0 1 1 0 0 0 0 1 0 0 1 0 0) (srbt 0 (left 1 (left 1 t0))) (srbt 0 (right 0 (left 1 t0))) (srbt 0 (left 1 (right 0 t0))) (srbt 0 (right 0 (right 0 t0))) ) ))) ; path 3 (define trail3 (and trail1 ; (insert2-post-assume (left 0 t0) 0 0 0 v0 (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e2 (value 0 (left 1 t0))) ; register mset element ; (= (c 0 (left 1 t0)) red) ; (= (c 0 (right 0 t0)) red) ; (not (or (= (c 0 (left 1 (left 1 t0))) red) (= (c 0 (right 0 (left 1 t0))) red) )) )) ; VC3 (define vc3 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail3 (unroll-srbt-funs t0 0 0 1 0 1 0 0 1 1 0 1 1 0) (unroll-srbt-funs (left 1 t0) 0 0 1 0 0 0 0 1 0 0 1 0 0) ) (and (insert2-post-assert t0 0 0 0 v0 t0 0 0 1 0 1 0 0 1 1 0 1 1 0) (unroll-srbt-cons (left 1 t0) 0 0 1 0 0 0 0 1 0 0 1 0 0) (srbt 0 (left 1 (left 1 t0))) (srbt 0 (right 0 (left 1 t0))) (srbt 0 (right 0 t0)) ) ))) ; path 4 (define trail4 (and trail1 ; (insert2-post-assume (left 0 t0) 0 0 0 v0 (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e2 (value 0 (left 1 t0))) ; register mset element ; (= (c 0 (left 1 t0)) red) ; (not (= (c 0 (right 0 t0)) red)) ; (= (c 0 (right 0 (left 1 t0))) red) ; (unroll-srbt (right 0 (left 1 t0)) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e3 (value 0 (right 0 (left 1 t0)))) ; register mset element (= (left 2 t0) (right 0 (left 1 t0))) (= (left 2 (left 2 t0)) (left 1 t0)) (= (right 1 (left 2 t0)) (right 0 (right 0 (left 1 t0)))) (= (left 2 (left 2 (left 2 t0))) (left 1 (left 1 t0))) (= (right 1 (left 2 (left 2 t0))) (left 1 (right 0 (left 1 t0)))) (= (right 1 t0) (right 0 t0)) ; (= (c 0 (left 2 (left 2 t0))) red) ; (= t1 (left 2 t0)) (= (left 3 t1) (left 2 (left 2 t0))) (= (left 3 (left 3 t1)) (left 2 (left 2 (left 2 t0)))) (= (right 2 (left 3 t1)) (right 1 (left 2 (left 2 t0)))) (= (right 2 t1) t0) (= (left 3 (right 2 t1)) (right 1 (left 2 t0))) (= (right 2 (right 2 t1)) (right 1 t0)) (= (color 1 t1) black) (= (color 1 (left 3 t1)) (color 0 (left 3 t1))) (= (color 1 (right 2 t1)) red) )) ; VC4 (define vc4 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail4 (unroll-srbt-funs t1 0 1 3 2 1 1 1 1 1 1 1 1 1) (unroll-srbt-funs (left 3 t1) 0 1 3 2 1 0 0 1 0 0 1 0 0) (unroll-srbt-funs (right 2 t1) 0 1 3 2 1 0 0 1 0 0 1 0 0) ) (and (insert2-post-assert t0 0 0 0 v0 t1 0 1 3 2 1 1 1 1 1 1 1 1 1) (unroll-srbt-cons (left 3 t1) 0 1 3 2 1 0 0 1 0 0 1 0 0) (unroll-srbt-cons (right 2 t1) 0 1 3 2 1 0 0 1 0 0 1 0 0) (srbt 0 (left 3 (left 3 t1))) (srbt 0 (right 2 (left 3 t1))) (srbt 0 (left 3 (right 2 t1))) (srbt 0 (right 2 (right 2 t1))) ) ))) ; path 5 (define trail5 (and trail1 ; (insert2-post-assume (left 0 t0) 0 0 0 v0 (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e2 (value 0 (left 1 t0))) ; register mset element ; (= (c 0 (left 1 t0)) red) ; (not (= (c 0 (right 0 t0)) red)) ; (= (c 0 (right 0 (left 1 t0))) red) ; (unroll-srbt (right 0 (left 1 t0)) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e3 (value 0 (right 0 (left 1 t0)))) ; register mset element (= (left 2 t0) (right 0 (left 1 t0))) (= (left 2 (left 2 t0)) (left 1 t0)) (= (right 1 (left 2 t0)) (right 0 (right 0 (left 1 t0)))) (= (left 2 (left 2 (left 2 t0))) (left 1 (left 1 t0))) (= (right 1 (left 2 (left 2 t0))) (left 1 (right 0 (left 1 t0)))) (= (right 1 t0) (right 0 t0)) ; (not (= (c 0 (left 2 (left 2 t0))) red)) )) ; VC5 (define vc5 (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail5 ) ) ; path 6 (define trail6 (and trail1 ; (insert2-post-assume (left 0 t0) 0 0 0 v0 (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e2 (value 0 (left 1 t0))) ; register mset element ; (= (c 0 (left 1 t0)) red) ; (not (= (c 0 (right 0 t0)) red)) ; (not (= (c 0 (right 0 (left 1 t0))) red)) ; (= (c 0 (left 1 (left 1 t0))) red) ; (= t1 (left 1 t0)) (= (left 2 t1) (left 1 (left 1 t0))) (= (right 1 t1) t0) (= (left 2 (right 1 t1)) (right 0 (left 1 t0))) (= (right 1 (right 1 t1)) (right 0 t0)) (= (color 1 t1) black) (= (color 1 (right 1 t1)) red) )) ; VC6 (define vc6 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail6 (unroll-srbt-funs t1 0 1 2 1 1 0 1 1 0 1 1 0 1) (unroll-srbt-funs (right 1 t1) 0 1 2 1 1 0 0 1 0 0 1 0 0) ) (and (insert2-post-assert t0 0 0 0 v0 t1 0 1 2 1 1 0 1 1 0 1 1 0 1) (unroll-srbt-cons (right 1 t1) 0 1 2 1 1 0 0 1 0 0 1 0 0) (srbt 0 (left 2 t1)) (srbt 0 (left 2 (right 1 t1))) (srbt 0 (right 1 (right 1 t1))) ) ))) ; path 7 (define trail7 (and trail1 ; (insert2-post-assume (left 0 t0) 0 0 0 v0 (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e2 (value 0 (left 1 t0))) ; register mset element ; (= (c 0 (left 1 t0)) red) ; (not (= (c 0 (right 0 t0)) red)) ; (not (= (c 0 (right 0 (left 1 t0))) red)) ; (not (= (c 0 (left 1 (left 1 t0))) red)) )) ; VC7 (define vc7 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail7 (unroll-srbt-funs t0 0 0 1 0 1 0 0 1 0 0 1 0 0) ) (and (insert2-post-assert t0 0 0 0 v0 t0 0 0 1 0 1 0 0 1 0 0 1 0 0) (unroll-srbt-cons (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0) (srbt 0 (left 1 (left 1 t0))) (srbt 0 (right 0 (left 1 t0))) (srbt 0 (right 0 t0)) ) ))) ; path 8 (define trail8 (and trail1 ; (insert2-post-assume (left 0 t0) 0 0 0 v0 (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0) (= e2 (value 0 (left 1 t0))) ; register mset element ; (not (= (c 0 (left 1 t0)) red)) )) ; VC8 (define vc8 (not (=> (and (insert2-pre t0 0 0) (= e0 v0) ; register mset element trail8 (unroll-srbt-funs t0 0 0 1 0 1 0 0 1 0 0 1 0 0) ) (and (insert2-post-assert t0 0 0 0 v0 t0 0 0 1 0 1 0 0 1 0 0 1 0 0) (unroll-srbt-cons (left 1 t0) 0 0 1 0 0 0 0 0 0 0 0 0 0) (srbt 0 (left 1 (left 1 t0))) (srbt 0 (right 0 (left 1 t0))) (srbt 0 (right 0 t0)) ) ))) (assert (or vc0 vc1 vc2 vc3 vc4 vc5 vc6 vc7 vc8 )) (check-sat)(exit) (get-value (e0 (count (keys 0 t0) e0))) (get-value (e1 (count (keys 0 t0) e1))) (get-value (e2 (count (keys 0 t0) e2))) (get-value (e3 (count (keys 0 t0) e3))) (get-value (e4 (count (keys 0 t0) e4))) (get-value (e5 (count (keys 0 t0) e5))) (get-value (e6 (count (keys 0 t0) e6))) (get-value (e7 (count (keys 0 t0) e7))) (get-value (v0)) (get-value (e0 (count (keys 2 t1) e0))) (get-value (e1 (count (keys 2 t1) e1))) (get-value (e2 (count (keys 2 t1) e2))) (get-value (e3 (count (keys 2 t1) e3))) (get-value (e4 (count (keys 2 t1) e4))) (get-value (e5 (count (keys 2 t1) e5))) (get-value (e6 (count (keys 2 t1) e6))) (get-value (e7 (count (keys 2 t1) e7))) (exit)