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 的编程前端之一。例如，这里是如何使用 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))