z3 C++ API：获取expr的操作答案

【问题标题】：z3 C++ API: get operation of exprz3 C++ API：获取expr的操作
【发布时间】：2016-07-12 07:59:46
【问题描述】：

我将 z3 用作 C++ 库。在我当前的编程项目中，我使用 z3 简化了布尔方程。

为了在我的项目中使用简化方程，我需要 lhs、rhs 和简化方程的运算。

例如：表达式 (x==3)&&(x

(= x 3)

lhs 参数 -> x

expression.arg(0)

rhs 参数 -> 3

expression.arg(1)

如何获得操作（=）？

任何具有超过 1 个参数的 expr 都应该有一个操作吗？

我正在研究 API 3 小时，但我就是想不通。

希望任何人都可以为我指明正确的方向！

谢谢脚趾

【问题讨论】：

“获取公式”是什么意思？（数学）方程总是有一个==。
我更新了问题以澄清我的意思！

标签： c++ z3

【解决方案1】：

要将“顶级”运算符作为字符串获取，即对于原始的“and”和简化的“=”，您可以使用：

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

【讨论】：

好答案！谢谢

【解决方案2】：

Z3 中的函数应用程序表示为参数向量和函数声明。例如，假设函数f 应用于参数x 和y。在 C++ API 中，它采用 expr 对象 e 的形式，它具有 e.num_args() 参数，x、y 是 e.arg(0)、e.arg(1) 和 e.decl() 应用于这些参数。

（显然这也适用于 0 参数，在 API 的各个部分中通常称为const，因为它们是常量函数的应用。）

【讨论】：