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)
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
y. In the C++ API this takes the shape of an
e which has
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.)