Z3 Strings: Suche nach der API

Question

[1] Ich habe heruntergeladen und installiert Z3 4.5.0 von diesem GitHub-Repository:

https://github.com/Z3Prover/z3 

[2] Als nächstes ich diesen Befehl lautete:

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

[3] Wo example.txt ist:

(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] ich habe, was ich erwartet hatte:

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

[5] Allerdings kann ich die entsprechenden API Z3-String-Funktionen nicht finden, So kann ich inkrementell Formeln aus meiner C++ - Anwendung erstellen.

würde ich so etwas wie erwartet:

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

Aber ich kann nichts in der Nähe finden ...

Jede Hilfe sehr geschätzt, Dank!

Answer 1

Strings ist ein ziemlich neues Feature und es wird verbessert, da wir aus den aktuellen Ansätzen lernen. Sie werden viel besser mit dem neuesten nächtlichen Build sein. Dort enthält die C++ API Unterstützung für String-Operationen.