Z3字符串：找到API

Question

[1]我已經下載並從這個GitHub的倉庫安裝Z3 4.5.0：

https://github.com/Z3Prover/z3 

[2]接下來，我跑了這個命令：

./build/z3 smt.string_solver=z3str3 -smt2 example.txt 

[3] example.txt的地方是：

(declare-const s1 String) 
(declare-const s2 String) 
(declare-const s3 String) 
(declare-const s4 String) 

(assert (= (str.len s1) 1)) 
(assert (= (str.len s2) 2)) 
(assert (> (str.len s4) 4)) 
(assert (= (str.++ s1 s2) s3)) 
(assert (str.contains s4 s3)) 

(check-sat) 
(get-value (s1 s2 s3 s4)) 

[4]我得到了我的預期：

sat 
((s1 "d") 
(s2 "af") 
(s3 "daf") 
(s4 "bdafaaaI")) 

[5]然而，我找不到相應的API Z3字符串函數， 因此，我可以從我的C++應用程序逐步構建公式。

我希望是這樣的：

z3_mk_concat(...) 
z3_mk_str_contains(...) 
etc. 

但我找不到任何接近...

任何幫助非常感謝，謝謝！

Answer 1

字符串是一個相當新的功能，它正在改進，因爲我們從當前的方法中吸取教訓。使用最新的每晚構建將會更好。那裏的C++ API包含對字符串操作的支持。