z3 - Z3 式に対する集合演算

Question

set, intersection, union, membersZ3 式に対するセット操作を定義する関数はあります か? また、数式がまたはであるかどうかを確認する関数はありますcnfかdnf?

そうでない場合は、z3utils ファイルに実装してみます。

Answer 1

Python セットを使用して、式のセットをエンコードできます。唯一の問題は、__eq__式が等しいかどうかを比較する代わりに、Z3Py 式の演算子が新しい式を作成することです。これを修正するには、正しい比較 Z3 式を呼び出すラッパーを使用できます。サンプルを次に示します ( rise4funでオンラインで入手できます)。

class AstRefKey:
    def __init__(self, n):
        self.n = n
    def __hash__(self):
        return self.n.hash()
    def __eq__(self, other):
        return self.n.eq(other.n)
    def __repr__(self):
        return str(self.n)

def askey(n):
    assert isinstance(n, AstRef)
    return AstRefKey(n)

x = Int('x')
s = set()
s.add(askey(x+1))
s.add(askey(x))
print s
print askey(x + 1) in s
s2 = set()
s2.add(askey(x+2))
s2.add(askey(x))
print s2
print s.union(s2)

唯一の不便は、 を使い続けなければならないことaskeyです。ASTSet呼び出した Pythonsetオブジェクトをラップするクラスを定義することで、この不都合を回避できますaskey。

に関して、dnfおよびcnf認識者。この機能は、外部 API では公開されていません。