z3smtsmt-lib

Is there an operator for inequality in SMT-Lib?

I know I can assert inequality with simple (not (= a b)), but I wonder if there is a operator that does this directly. I have tried everything that came to my mind including !=, <>, \= (this doesn't parse), /=, =/=, neq and none of them works.

Is there a dedicated function for it or do I need to compose equality with negation?

Solution

  • Yes. It is called distinct, See section 3.7.1 of https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

    Note that distinct can take an arbitrary number of arguments. For instance:

    (assert (distinct x y z))

    means:

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