Significant array values in z3 SMT solver
I tried for a while to get a pretty simple requirement: I declared a new datatype
(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))
where key
should act as the primary key in the database i.e. each individual instance A
must have a different meaning key
. The container of various instances (functions) looks like this:
(declare-const A_instances (Array Int A))
So far so good. I tried to create a statement so that all instances in A_instances
have a different field key
. Therefore, for each index i
in the A_instances (key (select A_instances i))
should be distinguished. However, it returns unknown
.
Anyone have any suggestions?
source to share
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
source to share