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 回答