【发布时间】：2012-10-23 14:24:24
【问题描述】：
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，它的名字是什么？
【问题讨论】：
-
我想出了创建表达式部分，我可以简单地调用 op(arg1,arg2) ..
-
您可能需要一个成熟的解析器，这取决于您想要完成的任务，而不是打开操作名称。我没看懂最后一部分：“我记得 Z3 中有一个文件列出了排序代码，例如 2L 是 Z3_INT_SORT，它的名称是什么？”什么是2L？
-
2L 是 Z3 中 int 排序的标识符。 Z3 中有一个文件告诉你这些标识符是什么（例如 2L 对应于 Z3_INT_SORT），我想知道那个文件在哪里。
-
好的，看一下 python 文档的底部（在“数据”部分下）：research.microsoft.com/en-us/um/redmond/projects/z3/z3.html 你可以看到 Z3_INT_SORT 声明为 2 那里。您还可以查看此源文件 (z3consts.py)：z3.codeplex.com/SourceControl/changeset/view/…
标签： z3