toebs toebs - 1 month ago 20
C++ Question

z3 C++ API: get operation of expr

I'm using z3 as a C++ library.
Within in my current programming project I have boolean equations I'm simplifying using z3.

In order to use the simplified equations within my project I need the lhs, rhs and the operation of the simplified equation.

e.G.: expression (x==3)&&(x<5) is simplified to (x==3) in z3

(= x 3)


lhs argument -> x

expression.arg(0)


rhs argument -> 3

expression.arg(1)


How do I get the operation(=) ?

Any expr with more than 1 argument should have a operation right?

I'm looking at the API for 3hrs now and I just can't figure it out.

Hopefully, anyone can point me in the right direction!

Thanks
Toebs

Answer

Function applications in Z3 are represented as a vector of arguments and a function declaration. For instance, suppose that function f is applied to the arguments x and y. In the C++ API this takes the shape of an expr object e which has e.num_args() arguments, x,y are e.arg(0), e.arg(1) and e.decl() is applied to those arguments.

(Obviously this also works for 0 arguments, which is often referred to as const in various parts of the API, because they are applications of constant functions.)