Module Theory.Mem

Sorts of memories.

A memory is an associative container of bitvectors indexed with bitvector keys.

type ('a, 'b) t
val define : 'a Bitv.t Value.sort -> 'b Bitv.t Value.sort -> ('a, 'b) t Value.sort

define ks vs a sort of memories with keys of type ks and data of type vs.

val refine : unit Value.sort -> ('a, 'b) t Value.sort option

refine s if s is a memory sort then restores its type.

val keys : ('a, 'b) t Value.sort -> 'a Bitv.t Value.sort

keys s returns the sort of keys.

val vals : ('a, 'b) t Value.sort -> 'b Bitv.t Value.sort

vals s returns the sort of values.