Distinct Array values in z3 SMT solver

4
votes

I tried around a some time to get a rather simple requirement done: I declared a new datatype

(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))

where key should act like a primary key in a database, i.e., each different instance of A should have a different key value. The container of the different instances (functions) looks like the following:

(declare-const A_instances (Array Int A))

So far so good. I tried to create an assertion, such that all instances in A_instances have a different key field. Thus, for each index i in A_instances (key (select A_instances i)) should be distinct. However it returns unknown.

Someone has any suggestions?

1
z3smt

1 Answers

2
votes

One possible solution is

(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))
(declare-const A_instances (Array Int A))
(declare-fun j () Int)
(assert (forall ((i Int))  (implies (distinct i j) 
                           (distinct (key (select A_instances i))  
                                     (key (select A_instances j)))        )   ))
(check-sat)

and the corresponding output is

sat