Z3 python中是否有内置方法将公式转换为DNF？我会想象应用一些策略或策略来做到这一点。
另外，我如何“创建”一个表达式，例如，如果我有变量
op=Or, arg1=True, arg2=False
我想使用 op,arg1,arg2 创建表达式 Or(True,False)。我可以做类似的事情
if op.name == 'or': Or(arg1,arg2)
elif op.name == 'and': And(arg1,arg2)
...
但有更好的方法吗？
另外，我记得在 Z3 中有一个文件列出了排序代码，例如 2L 是 Z3_INT_SORT，它的名称是什么？