z3 - SMT-Lib 中是否存在不等式运算符？

Question

我知道我可以用 simple 断言不等式(not (= a b))，但我想知道是否有直接执行此操作的运算符。我已经尝试了所有想到的东西，包括!=, <>, \=（这不会解析），/=, =/=，neq但它们都不起作用。

是否有专门的功能，或者我需要用否定组成相等吗？

Answer 1

是的。它被称为distinct，见第 3.7.1 节https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

请注意，distinct可以采用任意数量的参数。例如：

(assert (distinct x y z))

方法：

(assert (and (distinct x y) (distinct x z) (distinct y z)))