Z3唯一作業

我有一個未解釋的函數，稱爲uniqueFunc。現在，我想的唯一編號1分配到17，每個索引0到16 所以我對相同的代碼是 -Z3唯一作業

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

是否有這樣做的更好的辦法？

謝謝， Pranav

來源

2012-09-13 Raj

是，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-13 13:57:10 Taylor

是否有可能使用該使用C-API？例如，我必須使每個元素的AST（uniqueFunc x）'成爲AST，然後在其上聲明'Z3_mk_distinct（）'？ – Raj

是的，它適用於'Z3_mk_distinct（）' – Raj

如果你剛剛開始使用API，我可能會推薦使用Z3Py，因爲我發現它更容易處理大多數事情（但這取決於你想要的東西現有代碼等）：http://rise4fun.com/Z3Py/tutorial/guide – Taylor

回答

相關問題