CODEWITHSUNDEEP
encodingz3
Raj
Raj

Reputation: 3462

Z3 Unique Assignment

I have an uninterpreted function called as uniqueFunc. Now, I want to assign a unique number 1 to 17, to each of the index of 0 to 16. So my code for the same is - 

(declare-fun uniqueFunc (Int) Int)

(assert (and (> (uniqueFunc 0) 0) (< (uniqueFunc 0) 18)))
(assert (and (> (uniqueFunc 1) 0) (< (uniqueFunc 1) 18)))
(assert (and (> (uniqueFunc 2) 0) (< (uniqueFunc 2) 18)))
(assert (and (> (uniqueFunc 3) 0) (< (uniqueFunc 3) 18)))
(assert (and (> (uniqueFunc 4) 0) (< (uniqueFunc 4) 18)))
(assert (and (> (uniqueFunc 5) 0) (< (uniqueFunc 5) 18)))
(assert (and (> (uniqueFunc 6) 0) (< (uniqueFunc 6) 18)))
(assert (and (> (uniqueFunc 7) 0) (< (uniqueFunc 7) 18)))
(assert (and (> (uniqueFunc 8) 0) (< (uniqueFunc 8) 18)))
(assert (and (> (uniqueFunc 9) 0) (< (uniqueFunc 9) 18)))
(assert (and (> (uniqueFunc 10) 0) (< (uniqueFunc 10) 18)))
(assert (and (> (uniqueFunc 11) 0) (< (uniqueFunc 11) 18)))
(assert (and (> (uniqueFunc 12) 0) (< (uniqueFunc 12) 18)))
(assert (and (> (uniqueFunc 13) 0) (< (uniqueFunc 13) 18)))
(assert (and (> (uniqueFunc 14) 0) (< (uniqueFunc 14) 18)))
(assert (and (> (uniqueFunc 15) 0) (< (uniqueFunc 15) 18)))
(assert (and (> (uniqueFunc 16) 0) (< (uniqueFunc 16) 18)))

(assert (and (not (= (uniqueFunc 0) (uniqueFunc 1)))
     (not (= (uniqueFunc 0) (uniqueFunc 2)))
     (not (= (uniqueFunc 0) (uniqueFunc 3)))
     (not (= (uniqueFunc 0) (uniqueFunc 4)))
     (not (= (uniqueFunc 0) (uniqueFunc 5)))
     (not (= (uniqueFunc 0) (uniqueFunc 6)))
     (not (= (uniqueFunc 0) (uniqueFunc 7)))
     (not (= (uniqueFunc 0) (uniqueFunc 8)))
     (not (= (uniqueFunc 0) (uniqueFunc 9)))
     (not (= (uniqueFunc 0) (uniqueFunc 10)))
     (not (= (uniqueFunc 0) (uniqueFunc 11)))
     (not (= (uniqueFunc 0) (uniqueFunc 12)))
     (not (= (uniqueFunc 0) (uniqueFunc 13)))
     (not (= (uniqueFunc 0) (uniqueFunc 14)))
     (not (= (uniqueFunc 0) (uniqueFunc 15)))
     (not (= (uniqueFunc 0) (uniqueFunc 16)))
     (not (= (uniqueFunc 1) (uniqueFunc 2)))
     (not (= (uniqueFunc 1) (uniqueFunc 3)))
     (not (= (uniqueFunc 1) (uniqueFunc 4)))
     (not (= (uniqueFunc 1) (uniqueFunc 5)))
     (not (= (uniqueFunc 1) (uniqueFunc 6)))
     (not (= (uniqueFunc 1) (uniqueFunc 7)))
     (not (= (uniqueFunc 1) (uniqueFunc 8)))
     (not (= (uniqueFunc 1) (uniqueFunc 9)))
     (not (= (uniqueFunc 1) (uniqueFunc 10)))
     (not (= (uniqueFunc 1) (uniqueFunc 11)))
     (not (= (uniqueFunc 1) (uniqueFunc 12)))
     (not (= (uniqueFunc 1) (uniqueFunc 13)))
     (not (= (uniqueFunc 1) (uniqueFunc 14)))
     (not (= (uniqueFunc 1) (uniqueFunc 15)))
     (not (= (uniqueFunc 1) (uniqueFunc 16)))
     (not (= (uniqueFunc 2) (uniqueFunc 3)))
     (not (= (uniqueFunc 2) (uniqueFunc 4)))
     (not (= (uniqueFunc 2) (uniqueFunc 5)))
     (not (= (uniqueFunc 2) (uniqueFunc 6)))
     (not (= (uniqueFunc 2) (uniqueFunc 7)))
     (not (= (uniqueFunc 2) (uniqueFunc 8)))
     (not (= (uniqueFunc 2) (uniqueFunc 9)))
     (not (= (uniqueFunc 2) (uniqueFunc 10)))
     (not (= (uniqueFunc 2) (uniqueFunc 11)))
     (not (= (uniqueFunc 2) (uniqueFunc 12)))
     (not (= (uniqueFunc 2) (uniqueFunc 13)))
     (not (= (uniqueFunc 2) (uniqueFunc 14)))
     (not (= (uniqueFunc 2) (uniqueFunc 15)))
     (not (= (uniqueFunc 2) (uniqueFunc 16)))
     (not (= (uniqueFunc 3) (uniqueFunc 4)))
     (not (= (uniqueFunc 3) (uniqueFunc 5)))
     (not (= (uniqueFunc 3) (uniqueFunc 6)))
     (not (= (uniqueFunc 3) (uniqueFunc 7)))
     (not (= (uniqueFunc 3) (uniqueFunc 8)))
     (not (= (uniqueFunc 3) (uniqueFunc 9)))
     (not (= (uniqueFunc 3) (uniqueFunc 10)))
     (not (= (uniqueFunc 3) (uniqueFunc 11)))
     (not (= (uniqueFunc 3) (uniqueFunc 12)))
     (not (= (uniqueFunc 3) (uniqueFunc 13)))
     (not (= (uniqueFunc 3) (uniqueFunc 14)))
     (not (= (uniqueFunc 3) (uniqueFunc 15)))
     (not (= (uniqueFunc 3) (uniqueFunc 16)))
     (not (= (uniqueFunc 4) (uniqueFunc 5)))
     (not (= (uniqueFunc 4) (uniqueFunc 6)))
     (not (= (uniqueFunc 4) (uniqueFunc 7)))
     (not (= (uniqueFunc 4) (uniqueFunc 8)))
     (not (= (uniqueFunc 4) (uniqueFunc 9)))
     (not (= (uniqueFunc 4) (uniqueFunc 10)))
     (not (= (uniqueFunc 4) (uniqueFunc 11)))
     (not (= (uniqueFunc 4) (uniqueFunc 12)))
     (not (= (uniqueFunc 4) (uniqueFunc 13)))
     (not (= (uniqueFunc 4) (uniqueFunc 14)))
     (not (= (uniqueFunc 4) (uniqueFunc 15)))
     (not (= (uniqueFunc 4) (uniqueFunc 16)))
     (not (= (uniqueFunc 5) (uniqueFunc 6)))
     (not (= (uniqueFunc 5) (uniqueFunc 7)))
     (not (= (uniqueFunc 5) (uniqueFunc 8)))
     (not (= (uniqueFunc 5) (uniqueFunc 9)))
     (not (= (uniqueFunc 5) (uniqueFunc 10)))
     (not (= (uniqueFunc 5) (uniqueFunc 11)))
     (not (= (uniqueFunc 5) (uniqueFunc 12)))
     (not (= (uniqueFunc 5) (uniqueFunc 13)))
     (not (= (uniqueFunc 5) (uniqueFunc 14)))
     (not (= (uniqueFunc 5) (uniqueFunc 15)))
     (not (= (uniqueFunc 5) (uniqueFunc 16)))
     (not (= (uniqueFunc 6) (uniqueFunc 7)))
     (not (= (uniqueFunc 6) (uniqueFunc 8)))
     (not (= (uniqueFunc 6) (uniqueFunc 9)))
     (not (= (uniqueFunc 6) (uniqueFunc 10)))
     (not (= (uniqueFunc 6) (uniqueFunc 11)))
     (not (= (uniqueFunc 6) (uniqueFunc 12)))
     (not (= (uniqueFunc 6) (uniqueFunc 13)))
     (not (= (uniqueFunc 6) (uniqueFunc 14)))
     (not (= (uniqueFunc 6) (uniqueFunc 15)))
     (not (= (uniqueFunc 6) (uniqueFunc 16)))
     (not (= (uniqueFunc 7) (uniqueFunc 8)))
     (not (= (uniqueFunc 7) (uniqueFunc 9)))
     (not (= (uniqueFunc 7) (uniqueFunc 10)))
     (not (= (uniqueFunc 7) (uniqueFunc 11)))
     (not (= (uniqueFunc 7) (uniqueFunc 12)))
     (not (= (uniqueFunc 7) (uniqueFunc 13)))
     (not (= (uniqueFunc 7) (uniqueFunc 14)))
     (not (= (uniqueFunc 7) (uniqueFunc 15)))
     (not (= (uniqueFunc 7) (uniqueFunc 16)))
     (not (= (uniqueFunc 8) (uniqueFunc 9)))
     (not (= (uniqueFunc 8) (uniqueFunc 10)))
     (not (= (uniqueFunc 8) (uniqueFunc 11)))
     (not (= (uniqueFunc 8) (uniqueFunc 12)))
     (not (= (uniqueFunc 8) (uniqueFunc 13)))
     (not (= (uniqueFunc 8) (uniqueFunc 14)))
     (not (= (uniqueFunc 8) (uniqueFunc 15)))
     (not (= (uniqueFunc 8) (uniqueFunc 16)))
     (not (= (uniqueFunc 9) (uniqueFunc 10)))
     (not (= (uniqueFunc 9) (uniqueFunc 11)))
     (not (= (uniqueFunc 9) (uniqueFunc 12)))
     (not (= (uniqueFunc 9) (uniqueFunc 13)))
     (not (= (uniqueFunc 9) (uniqueFunc 14)))
     (not (= (uniqueFunc 9) (uniqueFunc 15)))
     (not (= (uniqueFunc 9) (uniqueFunc 16)))
     (not (= (uniqueFunc 10) (uniqueFunc 11)))
     (not (= (uniqueFunc 10) (uniqueFunc 12)))
     (not (= (uniqueFunc 10) (uniqueFunc 13)))
     (not (= (uniqueFunc 10) (uniqueFunc 14)))
     (not (= (uniqueFunc 10) (uniqueFunc 15)))
     (not (= (uniqueFunc 10) (uniqueFunc 16)))
     (not (= (uniqueFunc 11) (uniqueFunc 12)))
     (not (= (uniqueFunc 11) (uniqueFunc 13)))
     (not (= (uniqueFunc 11) (uniqueFunc 14)))
     (not (= (uniqueFunc 11) (uniqueFunc 15)))
     (not (= (uniqueFunc 11) (uniqueFunc 16)))
     (not (= (uniqueFunc 12) (uniqueFunc 13)))
     (not (= (uniqueFunc 12) (uniqueFunc 14)))
     (not (= (uniqueFunc 12) (uniqueFunc 15)))
     (not (= (uniqueFunc 12) (uniqueFunc 16)))
     (not (= (uniqueFunc 13) (uniqueFunc 14)))
     (not (= (uniqueFunc 13) (uniqueFunc 15)))
     (not (= (uniqueFunc 13) (uniqueFunc 16)))
     (not (= (uniqueFunc 14) (uniqueFunc 15)))
     (not (= (uniqueFunc 14) (uniqueFunc 16)))
     (not (= (uniqueFunc 15) (uniqueFunc 16)))))

Is there a better way of doing it?

Thanks, Pranav

Upvotes: 0

Views: 364

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

Yes, Z3 has a distinct expression. This will do all the not-equal permutations for you. Here's the API description:

http://research.microsoft.com/en-us/um/redmond/projects/z3/ml/z3.html#VALmk_distinct

For your example:

(assert (distinct (uniqueFunc 0) (uniqueFunc 1) (uniqueFunc 2) (uniqueFunc 3) (uniqueFunc 4) (uniqueFunc 5) (uniqueFunc 6) (uniqueFunc 7) (uniqueFunc 8) (uniqueFunc 9) (uniqueFunc 10) (uniqueFunc 11) (uniqueFunc 12) (uniqueFunc 13) (uniqueFunc 14) (uniqueFunc 15) (uniqueFunc 16)))

Upvotes: 1

Related Questions