如何解决SMT-Lib 中是否有不等式运算符?
我知道我可以用简单的 (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)))
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。