z3 API C++: получить команду expr

Question

Я использую z3 в качестве библиотеки C++. В моем текущем проекте программирования у меня есть логические уравнения, которые я упрощаю с помощью z3.

Для использования упрощенных уравнений в рамках моего проекта мне нужны lhs, rhs и операция упрощенного уравнения.

Eg: выражение (х == 3) & & (х < 5) упрощается до (х == 3) в z3

(= x 3) 

LHS аргумент -> х

expression.arg(0) 

аргумент аргумента -> 3

expression.arg(1) 

Как получить операцию (=)?

Любое выражение с более чем 1 аргументом должно иметь операцию справа?

Я смотрю API на 3 часа сейчас, и я просто не могу понять это.

Надеюсь, каждый может указать мне в правильном направлении!

Благодаря Toebs

Answer 1

Чтобы получить «верхний» оператор уровня в качестве строки, то есть для оригинала «и», а для упрощенного «=» вы можете использовать:

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

Answer 2

функции приложения в Z3 представлены в виде вектора аргументов и объявлении функции. Например, предположим, что функция f применяется к аргументам x и y. В API C++ это принимает форму объекта с expre, который имеет e.num_args() аргументов, x, y являются e.arg(0), e.arg(1) и применяются к тем аргументам.

(Очевидно, что это также работает для 0 аргументов, которые часто называют const в различных частях API, потому что они являются приложением постоянных функций.)