CODEWITHSUNDEEP
uniquez3countingsmt
Qiu
Qiu

Reputation: 5761

Count unique values of consts

In my project I defined following 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)
...

In result, I got following values in my model:

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

Now I want to define new const called cost and assign the number of unique values of vi_g (in the example above cost == 4 (i.e. {0,2,8,10}). How can I achieve it using z3 solver?

The only idea I came up with is:

  1. Knowing the maximum value (MAXVAL) that can be assigned to any of vi_g, define MAXVAL boolean consts (ci),
  2. For each of this consts make an assert that e.g. c0 = (v0_g == 0) v (v1_g == 0) v ... v (vn_g == 0),
  3. Count how many ci const equals True.

However, it requires a lot of additional clauses if MAXVAL is large.

Upvotes: 1

Views: 294

Answers (1)

Nuno Lopes
Nuno Lopes

Reputation: 868

There's no easy way to count the number of models of a general formula. Either your specific formula allows some sort of simplification or it isn't easy. See e.g. literature for #SAT (https://en.wikipedia.org/wiki/Sharp-SAT). A naïve way is to implement the counting with a linear loop blocking one model at a time (or potentially several ones if the model is partial).

Upvotes: -1

Related Questions