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