unique - 迭代地声明不同的变量

Question

这个问题与this和this question密切相关。

distinctZ3的功能

(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

f我们可以从Sto定义一个辅助fresh函数Int，然后断言

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

在这种方法中，我们只需要跟踪计数器。