计算consts的唯一值

Question

在我的项目中，我定义了以下consts：

(declare-const v0_g Int)
(declare-const v1_g Int)
(declare-const v2_g Int)
(declare-const v3_g Int)
(declare-const v4_g Int)
...

结果，我在我的模型中得到以下值：

...    
(define-fun v4_g () Int
2)
(define-fun v3_g () Int
10)
(define-fun v2_g () Int
10)
(define-fun v1_g () Int
8)
(define-fun v0_g () Int
0)
...

现在我想定义一个名为cost的新const，并指定vi_g的唯一值的数量（在上面的例子中cost == 4（即{0,2,8,10}）。如何使用z3求解器实现它？

我想出的唯一想法是：

1. 知道可以分配给任何MAXVAL的最大值（vi_g），定义MAXVAL布尔consts（ci），
2. 对于这些争论中的每一个，都要断言，例如， c0 = (v0_g == 0) v (v1_g == 0) v ... v (vn_g == 0)，
3. 计算ci const等于True的数量。

但是，如果MAXVAL很大，它需要很多额外的条款。

Answer 1

没有简单的方法来计算通用公式的模型数量。您的特定公式可以允许某种简化，也不容易。参见例如#SAT（https://en.wikipedia.org/wiki/Sharp-SAT）的文献。一种天真的方法是使用线性循环一次阻塞一个模型来实现计数（或者如果模型是部分的，则可能是几个模型）。