search

z3str / Z3-str

A Z3-Based String Constraint Solver
Other
87 stars 13 forks source link

Z3Str interface for C++ #14

Open Shirlies opened 8 years ago

Shirlies commented 8 years ago

Hi, Thanks to you for supporting us with the lib, and it is useful to us. I want to get the interface for c++, I hava read the "strTheory.h" file, but the file has no explanation for these functions. What is more, I do not know how to use it with C++. I am a fresher with Z3 and unfamiliar with the code for Z3Str. And I want to know how I could start to use it with C++ code.

Kind regards, Shirlies

z3str commented 8 years ago

Hi Shirlies,

Sorry for the delay. The API support in this version is not complete yet (There are some known issues about state maintenance if invoking the solver via APIs).

Would it be an option to dump the constraints to a temp file, invoke the solver and parse the results? We are porting Z3str2 to latest Z3 now and I think we would have better support in that version.

Thanks, -Yunhui

Shirlies commented 8 years ago

Hi Yunhui, Thank you for replying my question. What is more, the method which dump the constraints to a temp file is good for me and I have done it. Nevertheless, I have run into trouble. Details are as follows: When I run into line 6050 in strTheory.cpp with "Z3_lbool result = Z3_check_and_get_model(ctx, &m);",program exit without no error and no any hint. Content of the input file as follows: **(declare-const x String) (declare-const y1 String) (declare-const y2 String)

(declare-const cOnStStRx74_x65 String) (declare-const cOnStStRx73_x74 String)

(assert (= x ( Concat ( Concat cOnStStRx74_x65 y1 ) ( Concat cOnStStRx73_x74 y2 ) ) ) ) (check-sat) Above the content comes from a temp file which I use Z3-str.py to transform it to.And the content of the original file is: (declare-variable x String) (declare-variable y1 String) (declare-variable y2 String)

(assert (= x ( Concat ( Concat "te" y1 ) ( Concat "st" y2 ) ) ) )

(check-sat) (get-model)** How could I deal with the problem? We are looking forward to hearing from you soon, Thank you.

Kind regards, Shirlies