0

as という未解釈の関数がありuniqueFuncます。ここで、0 から 16 のインデックスのそれぞれに、1 から 17 までの一意の番号を割り当てたいと思います。同じコードのコードは次のとおりです。

(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)))))

それを行うより良い方法はありますか？

ありがとう、プラナフ

4

1 に答える 1

1

はい、Z3にはdistinct表情があります。これにより、等しくない順列がすべて実行されます。API の説明は次のとおりです。

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

あなたの例：

(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)))

于 2012-09-13T13:57:10.783 に答える