1

式をDNFに変換するためのZ3 pythonの組み込みメソッドはありますか? そうするために何らかの戦略や戦術を適用することを想像します。

また、変数がある場合など、式を「作成」するにはどうすればよいですか

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 です。その名前は何ですか?

4

1 に答える 1

0

DNFに変換する方法については、この回答を参照してください。数式を選言標準形に変換する方法は？

関連する注記として、CNFに変換する方法については、次の回答を参照してください。数式をCNFに変換する

これらの例はSMT形式であり、ここではz3pyにあります：http：//rise4fun.com/Z3Py/ik4

于 2012-10-23T16:13:04.953 に答える