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.

user_936310 · Answer

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.

user_491216 · Answer

Alternatively, have a look at Dafny's map axioms:

https://github.com/Microsoft/dafny/blob/master/Binaries/DafnyPrelude.bpl#L1113

Dafny is widely used (for a formal methods tool ;-)) and its axiomatisations are therefore fairly mature.

The map axioms are expressed in the Boogie language, but it is typically straight-forward to translate Boogie axiomatisations to SMT-LIB.