如何在 Z3 Python 中使用内置三角函数？

Question

我想做一些类似的事情：

Exists y. 0<=cos(y)<=1.

，它可以返回模型，例如

y:=50

。这在Z3中可能吗？

我知道 SMT 求解器总体上对于非线性/超越运算 [1] 是有问题的，并且确实已经有一段时间没有实现了 [2,3]。然而，看起来至少对于三角函数有一些支持 [4,5]，而且，它看起来已经是内置的，就像 [6] 的函数

cos

中一样。

因此，我在Z3-PY中尝试了以下操作：

from z3 import *

x = Real('x')
solver = Solver()
solver.add(Exists([x],cos(x)<1))
solver.check()
model = solver.model()

...但看起来

cos

无法识别。你知道我该如何使用这个吗？我想到了一些不使用 Z3 的替代方法，但我想探索这种可能性，以便将所有内容都实现在同一个块中。

[1] SMT 求解器在实践中用于实闭域（例如，超越和无穷小）？ Z3、MetiTarski、dReal

[2] Z3可以处理正弦函数和指数函数吗

[3] Z3 支持非线性算术

[4] https://github.com/Z3Prover/z3/issues/680

[5] Z3 中支持三角函数（例如：cos、tan）

[6] Z3 中未记录的三角函数可以修复吗？

Answer 1

如果您坚持 SMTLib 接口，您可以在 z3 中使用三角函数：

(set-option :produce-models true)
(set-logic ALL)
(declare-fun x () Real)
(assert (< (cos x) 1.0))
(check-sat)

唉，这并不能让你走得太远。对于上述内容，z3 说：

unknown

对于使用三角函数的大多数问题来说都是这种情况。对它们的支持非常轻量级：它们或多或少被视为带有一些公理的未解释函数（如

sin^2 + cos^2 = 1

），可以处理一些简单的查询，但处理不多。

您似乎无法从 Python API 访问这些内容。并不是因为它无法完成，而是可能没有人担心，因为无论如何支持都相当薄弱。 （即，您可以在 Python 端自行将它们定义为具有多个公理的未解释函数，并且您几乎可以匹配 z3 SMTLib 对它们的支持。）

如果您对三角函数和自动定理证明感兴趣，那么您最好的选择是 MetiTarski (https://www.cl.cam.ac.uk/~lp15/papers/Arith/)。如果您想要更多按钮式的东西并且对增量可满足性感到满意，那么 dReal 是您应该考虑的另一个工具：https://dreal.github.io.