我是 z3 求解器的新手。我想实现通用量词，我在https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html 中发现 context.mkForAll() 可能会有所帮助，但该文档很难理解，因为有很多参数而没有示例。
例如，我应该如何实现检查以下语句：对于{2、4、6、8}中的任何y，存在整数x where x > y？
这是我第一次在这里提问，所以请告诉我如何改进我的问题。
【问题讨论】：
Z3 附带的 Java 示例中有许多量词示例：https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java#L597-L767
通读它们可以给你一个想法。
如果您是 z3 和编程新手，我强烈建议您不要使用 Java 或 C++ API。它们相当繁琐，充满了很多细节，作为一个新手，你既不需要也不关心。相反，看看你是否可以使用它的 Python 界面，它更轻量级且易于使用。例如，您的示例可以像这样简洁地编码：
from z3 import *
s = Solver()
x, y = Ints('x y')
s.add(Not(ForAll([y], Implies(Or([y == 2, y == 4, y == 6, y == 8]), Exists([x], x > y)))))
print(s.sexpr())
print(s.check())
（请注意，在 SMT 中，就像在解析定理证明中一样，您断言要证明的内容是否定的，并检查结果是否为 unsat。如果是，您已经证明了您的断言。因此包装了 @987654326 @在上面的例子中。）
当我运行它时，我得到：
(assert (let ((a!1 (forall ((y Int))
(=> (or (= y 2) (= y 4) (= y 6) (= y 8))
(exists ((x Int)) (> x y))))))
(not a!1)))
unsat
它还向您展示了如何在 SMTLib 中编写相同的代码。
我还应该指出，SMT 求解器通常不适合使用量词进行推理。上面的例子很简单，z3 可以轻松处理它，但 SMT 求解器的亮点通常是算术、位向量、布尔值以及未解释的值和函数的无量词组合。这是一个很好的教程，可以帮助您入门：https://ericpony.github.io/z3py-tutorial/guide-examples.htm
【讨论】：
let binders 的信息：smtlib.cs.uiowa.edu/papers/…