Z3文字列：APIを見つける

Question

[1]私はダウンロードして、このGitHubのリポジトリからZ3 4.5.0をインストールしている：

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

：[2]次に、私は、このコマンドを実行した

https://github.com/Z3Prover/z3 

[3]、EXAMPLE.SQLである場合：

(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には文字列操作のサポートが含まれています。