我将 z3 用作 C++ 库。 在我当前的编程项目中，我使用 z3 简化了 bool 方程。
为了在我的项目中使用简化方程，我需要左轴、右轴和简化方程的运算。
例如:表达式 (x==3)&&(x<5) 在 z3 中被简化为 (x==3)
(= x 3)
lhs 参数 -> x
expression.arg(0)
rhs 参数 -> 3
expression.arg(1)
如何获得操作(=)？
任何具有超过 1 个参数的 expr 都应该有操作权吗？
我现在查看 API 已经 3 个小时了，我就是想不通。
希望任何人都能为我指明正确的方向!
谢谢 脚趾
最佳答案
要将“顶层”运算符作为字符串获取，即对于原始的“and”和简化的“=”，您可以使用:
expression.decl().name().str()
关于c++ - z3 C++ API : get operation of expr，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/38323108/