1

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?

radrow
  • 6,419
  • 4
  • 26
  • 53

1 Answers1

2

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)))
alias
  • 28,120
  • 2
  • 23
  • 40