z3 - (eval (fxy)) の結果を単純化する方法は?

Question

解釈されていない関数を評価した結果として得られるブール式を単純化するにはどうすればよいですか? たとえば、例: http://rise4fun.com/Z3/G8sL、

(eval (f x y)) 

利回り (not (and (not x) (not y)))

代わりに式（またはxy）を取得したい。

(simplify (eval (f x y)) 

エラーを出します。

Answer 1

これは、SMT-LIB 2.0 フロントエンドではサポートされていません。Z3 のプログラマティック フロントエンドの 1 つを検討する必要があります。たとえば、Z3 Python フロントエンドを使用してそれを行う方法は次のとおりです (こちらからも入手できます)。

B = BoolSort()
f = Function('f', B, B, B)
x, y = Bools('x y')
b1, b2 = Bools('b1 b2')

s = Solver()
s.add(ForAll([b1, b2], Implies(Or(b1, b2), f(b1, b2))))
s.add(Exists([b1, b2], Not(f(b1, b2))))

print(s.check())
m = s.model()
print(m.evaluate(f(x, y)))
print(simplify(m.evaluate(f(x, y)), elim_and=True))