Есть ли в SMT-Lib оператор неравенства?

Question

Я знаю, что могу утверждать неравенство с помощью простых (not (= a b)), но мне интересно, есть ли оператор, который делает это напрямую. Я перепробовал все, что приходило мне в голову, включая !=, <>, \= (это не разбирается), /=, =/=, neq и ни один из них не работает.

Есть ли для этого специальная функция или мне нужно составить равенство с отрицанием?

Answer 1

Да. Он называется, см. Раздел 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)))