迭代聲明不同的變量

Question

這個問題與this和this有很大關係。

Z3

的 distinct功能

(declare-const a S) 
(declare-const b S) 
(assert (distinct a b)) 

允許約束組變量（這裏a和b），使得在該組的所有變量必須採取不同的值。

我的問題是：是否也可以強制一個變量採取一個獨特的值，而不明確提及它應該是不同的變量集？類似於

(declare-unique-const a S) 
(declare-unique-const b S) 
(declare-unique-const c S) 

在迭代過程中聲明新變量的情況下（例如在程序驗證過程中），這將會很不錯。

如果這是不可能的，我想我們必須跟蹤所有不同的變量，並使用該集合發出適當的distinct (newvar, oldvar1, ..., oldvarn))約束。

Answer 1

我們可以從S限定輔助功能新鮮到fInt，並斷言

f(a_1) = 1 
f(a_1) = 2 
f(a_3) = 3 
... 
f(a_n) = n 

然後，a_1，...，a_n必須彼此不同。 如果我們想說b也不同於所有a_i s。我們只是斷言

f(b) = n+1 

在這種方法中，我們只需要跟蹤計數器。