z3 C++ API: Operation von expr

Question

Ich benutze z3 als C++ - Bibliothek. In meinem aktuellen Programmierprojekt habe ich boolesche Gleichungen, die ich mit z3 vereinfache.

Um die vereinfachten Gleichungen in meinem Projekt zu verwenden, brauche ich die Lhs, rhs und die Operation der vereinfachten Gleichung.

eG: Ausdruck (x == 3) & & (x < 5) wird vereinfacht zu (x == 3) in z3

(= x 3) 

lhs Argument -> x

expression.arg(0) 

rhs Argument -> 3

expression.arg(1) 

Wie erhalte ich die Operation (=)?

Jeder Ausdruck mit mehr als 1 Argument sollte eine Operation richtig haben?

Ich schaue die API für 3hrs jetzt an und ich kann es einfach nicht herausfinden.

Hoffentlich kann mir jeder in die richtige Richtung zeigen!

Dank Toebs

Answer 1

Um den „top“ Level Operator zu erhalten als String, dh für die original „und“, und für die vereinfachte „=“ können Sie verwenden:

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

Answer 2

Funktionsanwendungen in Z3 als Vektor von Argumenten und einer Funktionsdeklaration dargestellt. Angenommen, die Funktion f wird auf die Argumente x und y angewendet. In der C++ API nimmt dies die Form eines Objekts expre die e.num_args() Argumente hat, x, y sind e.arg(0), e.arg(1) und auf diese Argumente angewendet wird.

(Natürlich funktioniert das auch für 0 Argumente, die oft als const in verschiedenen Teilen der API bezeichnet wird, da sie Anwendungen von konstanten Funktionen.)