CODEWITHSUNDEEP
c++z3
toebs
toebs

Reputation: 409

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

Upvotes: 0

Views: 309

Answers (2)

Joakim
Joakim

Reputation: 36

To get the "top" level operator as a string, i.e., for the original "and", and for the simplified "=" you can use:

expression.decl().name().str()

Upvotes: 2

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

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

Upvotes: 1

Related Questions