Map data structure in Z3

Question

I need to prove some properties about the map data structure (such as emptiness, domain, update, etc). Is there support for maps in Z3?

I found a proposal: https://www.kroening.com/smt-lib-lsm.pdf and its associated SMT theory http://www.philipp.ruemmer.org/smt-lsm/SMT-LIB.tar.gz. This proposal treats maps as arrays with corresponding axioms. However, I cannot find an off-the-shelf implementation in a theorem prover.

Any suggestion of where to start if I'd like to have support for maps in Z3?

My best bet is that i need to add a new theory in Z3, which assumes good knowledge of Z3's implementation - assumption which doesn't hold in my case.

Answer 1

Z3 doesn't have native support for maps. Your best bet is to use arrays of records (algebraic data types) to simulate them, for the time being.

Adding a theory to an SMT solver is a significant undertaking. I'd recommend exploring arrays and records first before going down that path.