问题描述
我知道我可以用简单的 (not (= a b)) 来断言不等式，但我想知道是否有一个运算符可以直接执行此操作。我已经尝试了所有想到的方法，包括 !=、<>、\=（这不会解析）、/=、=/=、{{1 }} 并且它们都不起作用。
是否有专门的函数，或者我是否需要将相等与否定组合起来？
解决方法
是的。它被称为 distinct，见 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)))