search

z3str / Z3-str

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

Compatibility with latest z3 version #6

Closed yannicnoller closed 8 years ago

yannicnoller commented 8 years ago

Hi all,

I'm trying to use your z3-string plugin with the latest z3 4.4.1 version in order to use the Java API. Do you know whether it is possible to apply your patch the latest version? Or is it possible to generate a Java API with your referenced version 4.1.1?

Cheers, Yannic

z3str commented 8 years ago

Hi Yannic,

Unfortunately, this theory plug-in based version won't work with the latest Z3, Z3 changed its internal logic significantly and has the retired the theory plug-in interface. But we are working on a new version of Z3str. The goal is to directly implement the string part in Z3.

We don't have a chance to try Java API yet. Any chance you could let us know more about how these APIs are generated and used in your scenario?

Thanks, -Yunhui

yannicnoller commented 8 years ago

Hi Yunhui,

okay. The Java API for the latest Z3 version can be generated by configuring Z3 with the --java option to scripts/mk_make.py. Then you can use the class Solver and the SMT functions push, pop, getModel, etc.

Is there a chance to generate the python API for your Z3str? So far I only build the binary file "str" (using cygwin on windows 7).

Cheers, Yannic

yannicnoller commented 8 years ago

clarified in issue #9