Подсчитать уникальные значения констант

Question

В моем проекте я определил следующие константы:

(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)
...

Теперь я хочу определить новый const с именем cost и назначить количество уникальных значений vi_g (в приведенном выше примере cost == 4 (то есть {0,2,8,10}). Как я могу добиться этого с помощью решателя z3?

Единственная идея, которая мне пришла в голову:

1. Зная максимальное значение (MAXVAL), которое может быть присвоено любому из vi_g, определите MAXVAL логические константы (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).. Наивным способом является осуществление подсчета с помощью линейного цикла, блокирующего одну модель за раз (или, возможно, несколько, если модель является частичной).