is it possible to model associative arrays in z3?

181 views Asked by At

I am wondering if z3 supports associative arrays (aka maps)? If not is there a simple way to model such data structures using the current version of z3?

1

There are 1 answers

0
Christoph Wintersteiger On

Z3 has support for Arrays as defined by SMT-Lib and it also has support for datatypes, either of them should allow you to model maps. A detailed example of using datatypes is found in the answer to this question: a datatype contains a set in Z3. The Z3 Guide also contains sections on how to use arrays as well as datatypes.