【发布时间】：2021-07-17 11:46:49
【问题描述】：
我知道我可以用简单的(not (= a b)) 断言不等式，但我想知道是否有直接执行此操作的运算符。我已经尝试了所有想到的东西，包括!=、<>、\=（这不会解析）、/=、=/=、neq，但它们都不起作用。
是否有专门的功能，或者我需要用否定组成相等吗？
【问题讨论】：
【发布时间】：2021-07-17 11:46:49
【问题描述】：
是的。它被称为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)))
【讨论】：