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包含对字符串操作的支持。