How to automatically check Z3 string by using Microsoft.z3.dll

May 13, 2015 at 12:34 PM
I have a smt2 string that is stored in a file *.smt2. I use z3.exe check it. The result is an exact answer. Now I want to use Microsoft.z3.dll integrated in my WindowsForm App with C#, but I don't know how to describe this string in Z3 API such that it works automatically. It means that, I give it a string SMT format intead of storing it in a file, It can answer "sat" or "unsat".
I have tried many examples internet, but is not successfully as I expected.

Who can suggest me to solve this problem or give me some links concern with this issue.
Thank alot,

Newfut
Coordinator
May 18, 2015 at 5:56 PM
Z3 has moved to github, see here:
https://github.com/Z3Prover/z3/

We are not using the Codeplex website anymore; please consider opening a new issue at github.

For this particular issue, the preferred way is to run the z3 binary ( z3.exe) on the SMT2 file, perhaps interfacing to it via a process pipe for incremental solving. There are functions to parse strings and files (Context.parse*) in the API, but they do not support all features, e.g., no SMT2 commands will be executed, and it will not provide any convenient features like a table of function declarations, they will only obtain the assertions of the SMT2 file.
May 22, 2015 at 9:45 AM
Thank you,
I will try.