Equality for constants in Z3 SMT solver
Question
I am using the Z3 SMT solver by Microsoft, and I am trying to define constants of a custom sort. It seems like such constants are not unequal by default. Suppose you have the following program:
(declare-sort S 0)
(declare-const x S)
(declare-const y S)
(assert (= x y))
(check-sat)
This will give "sat", because it is of course perfectly possible that two constants of the same sort are equal. Since I am making model in which constants have to be different from each other, this means that I would need to add an axiom of the form
(assert (not (= x y)))
for every pair of constants of the same sort. I was wondering if there is some way to do this generic, so that each constant of a sort is unique by default.
Solution
You can use datatypes to encode enumeration types found in many programming languages. In the following example, the sort S
has three elements and they are different from each other.
(declare-datatypes () ((S a b c)))
Here is a complete example: http://rise4fun.com/Z3/ncPc
(declare-datatypes () ((S a b c)))
(echo "a and b are different")
(simplify (= a b))
; x must be equal to a, b or c
(declare-const x S)
; since x != a, then it must be b or c
(assert (not (= x a)))
(check-sat)
(get-model)
; in the next check-sat x must be c
(assert (not (= x b)))
(check-sat)
(get-model)
Another possibility is to use distinct
.
(assert (distinct a b c d e))