python - z3 python API で Implies および if boolean コマンドを使用する方法

Question

if-then-else一次式の結合の一部として Z3 python API を使用して実装する方法は? 例えば

s.add( F, H, (if then else)).

関連する質問は次のとおりです。この目的のためにZ3 pythonオンラインガイドで指定されたブール「Implies」または「if」コマンドを使用する方法は?

score 2 · Accepted Answer

if(A, B, C)を使用して Z3 Python API でエンコードされた式If(A, B, C)。次に例を示します。

F, H, A, B, C = Bools('F H A B C')
s = Solver()
s.add(F, H, If(A, B, C))
print s

「暗黙」を使用した別の例を次に示します。

F, H, A, B, C = Bools('F H A B C')
s = Solver()
s.add(F, H, Implies(A, B))
print s

1 に答える 1