在SMT-Lib中是否有不等式的算子？

Question

我知道我可以用简单的(not (= a b))断言不等式，但我想知道是否有一个运算符可以直接这样做。我试过了所有出现在我脑海中的东西，包括!=、<>、\= (这不能解析)、/=、=/=、neq，但它们都不起作用。

有没有专门的函数来处理它，或者我需要把相等和否定组合起来？

Answer 1

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

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

(assert (distinct x y z))

意思是：

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