CODEWITHSUNDEEP
z3
Heyji
Heyji

Reputation: 1211

Reading a Z3 file

My program creates a log of all z3 interactions with Z3_open_log(). Then in another program, I read it back with Z3_parse_z3_file(). It gives me the conjuction of all asserts made on the input. Let say I have two asserts: a1 and a2. Then by parsing the z3 file, I get (and a1 a2).

I would like to test (and (not a1) a2). How can I do that provided that I only get the conjuction of the two asserts, not a pair of asserts ? I could not find any function in the API that allows me to navigate into an AST, see if it is a conjunction and iterate over it.

If it is not the way I should go, what way would you recommand?

Thanks in advance,

AG.

Upvotes: 1

Views: 883

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

As Pad already described in the comment above, you can use the API to traverse Z3 ASTs. That being said, I have a couple of comments.

The logging is meant for debugging purposes. They are mainly used to report problematic traces. We have a new logging mechanism in Z3 4.0. It records all APIs, and allow us to have a faithful reproduction of the interaction between the host application and Z3.

The Z3 low level and Simplify formats are deprecated in Z3 4.0. Z3 still have some limited support for them.

Z3 4.0 has new C, C++, .NET and Python APIs. The C API is backward compatible, but I marked several procedures as deprecated. It is much easier to traverse and manipulate ASTs using the new APIs. Python API is already available online. Here is one example:

http://rise4fun.com/Z3Py/Cp

Here is another example that builds (and a1 a2), extract each children, and builds (and (not a1) a2).

http://rise4fun.com/Z3Py/8h

The following tutorial covers the new Z3 API:

http://rise4fun.com/Z3Py/tutorial/guide

Z3 4.0 will be released soon.

Upvotes: 1

Related Questions