0
在Z3 python中是否有內置的方法將公式轉換爲DNF？我會想象應用一些策略或戰術來做到這一點。z3：將公式轉換爲dnf
而且，我怎麼「創造」的表達，例如，如果我有變量
op=Or, arg1=True, arg2=False
我想，以創建表達或（真，假）使用運算，ARG1，ARG2 。我可以做類似
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？ – Taylor
2L是Z3中int類型的標識符。 Z3中有一個文件告訴你這些標識符是什麼（例如2L對應於Z3_INT_SORT），我想知道文件的位置。 –