Z3位向量操作

Question

如何使用'repeat'和'rotate_left'位向量操作？

更一般地說，我可以在哪裏找到Z3使用的SMT2腳本格式的位向量操作的詳細文檔？

的一切，我覺得好像只是去教程，或者斷開鏈接：
https://github.com/Z3Prover/z3/wiki/Documentation
http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html

試圖瞭解 「重複」， 「ROTATE_LEFT」 和 「ROTATE_RIGHT」 的猜測一直frustating。我無法弄清楚如何使用它們。例如

(display (repeat #b01)) 
(display (repeat #b01 3)) 
(display (repeat 3)) 
(display (rotate_left #b0001 2)) 

給

"repeat expects one non-zero integer parameter" 
"repeat expects one argument" 
"operator is applied to arguments of the wrong sort" 
"rotate left expects one argument" 

文檔位於何處？希望他們沒有解釋，因爲所有這些都是標準的，我也看了smt-lib.org，但是沒有列出這些細節。太令人沮喪了。

Answer 1

除了dejvuth的回答是：

的SMT語言是有據可查（見smt-lib.org），對於此問題的FixedSizeBitVectors theory和QF_BV logic定義是相關的。後者包含重複的定義：

((_ repeat i) (_ BitVec m) (_ BitVec i*m)) 
- ((_ repeat i) x) means concatenate i copies of x 

除了那些，大衛Cok寫了一個很好的SMT2 tutorial。

Z3 API中的函數名與語法允許的SMT2中的函數名相同，在這種情況下，前綴Z3_mk_指示它們是構造Z3表達式的函數。

Answer 2

對於你的榜樣，你應該寫這樣的事情

(declare-const a (_ BitVec 2)) 
(declare-const b (_ BitVec 6)) 
(assert (= a #b01)) 
(assert (= b ((_ repeat 3) a))) 

(declare-const c (_ BitVec 4)) 
(declare-const d (_ BitVec 4)) 
(assert (= C#b0001)) 
(assert (= d ((_ rotate_left 2) c))) 

(check-sat) 
(get-model) 

你會得到

sat 
(model 
    (define-fun d() (_ BitVec 4) 
    #x4) 
    (define-fun c() (_ BitVec 4) 
    #x1) 
    (define-fun b() (_ BitVec 6) 
    #b010101) 
    (define-fun a() (_ BitVec 2) 
    #b01) 
) 

，我通常使用的是它的API好的文件。