我现在用的是Z3 SMT求解器由微软，我试图定义一个自定义排序的常数。 这似乎是这样的常量是默认情况下不相等。 假设你有以下程序：
(declare-sort S 0)
(declare-const x S)
(declare-const y S)
(assert (= x y))
(check-sat)
这将使“坐”，因为这是当然的完全可能是同一类的两个常数是相等的。 因为我在做其中的常量必须是彼此不同的模式，这意味着我需要补充形式的公理
(assert (not (= x y)))
每对同一种类的常量。 我想知道是否有某种方式来做到这一点的通用，这样一种对每一恒定在默认情况下是唯一的。
您可以使用的数据类型编码在许多编程语言中枚举类型。 在以下示例中，排序S具有三个元件和它们彼此不同。
(declare-datatypes () ((S a b c)))
下面是一个完整的例子： 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)
另一种可能性是使用distinct 。
(assert (distinct a b c d e))
