toebs - 2 months ago 40

C++ Question

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*.)