Z3 SMT求解器中的常數相等

Question

我正在使用Microsoft的Z3 SMT解算器，並試圖定義自定義排序的常量。似乎這樣的常量默認情況下不是不相等的。假設你有下面的程序：

(declare-sort S 0) 

(declare-const x S) 
(declare-const y S) 

(assert (= x y)) 
(check-sat) 

這將給「坐」，因爲這是當然的完全可能是同一類的兩個常數是相等的。因爲我在做其中的常量必須是彼此不同的模式，這意味着我需要補充的形式

(assert (not (= x y))) 

的公理每對同一種類的常量。我想知道是否有一些方法來做這個泛型，以便默認情況下每種常量都是唯一的。

Answer 1

您可以使用數據類型對許多編程語言中找到的枚舉類型進行編碼。在下面的例子中，排序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))