Module MonadicSMemory_Base.CMapMemory

module Addition : sig ... end
type t = Addition.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type pred = BaseMemory.pred
val pred_from_str : string -> pred option
val pred_to_str : pred -> string
val empty : unit -> t
val compose : t -> t -> t Gillian.Monadic.Delayed.t
val is_exclusively_owned : t -> Gillian.Gil_syntax.Expr.t list -> bool Gillian.Monadic.Delayed.t
val is_empty : t -> bool
val is_concrete : t -> bool
val instantiate : Gillian.Gil_syntax.Expr.t list -> t * Gillian.Gil_syntax.Expr.t list
val assertions : t -> (pred * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list) list
val assertions_others : t -> Gillian.Gil_syntax.Asrt.atom list
val substitution_in_place : Gillian.Symbolic.Subst.t -> t -> t Gillian.Monadic.Delayed.t
val pp : Stdlib.Format.formatter -> t -> unit
val list_preds : unit -> (pred * string list * string list) list
type action =
  1. | BaseAct of BaseMemory.action
  2. | AddedAct of Addition.action
type err_t =
  1. | BaseErr of BaseMemory.err_t
  2. | AddedErr of Addition.err_t
val pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
val err_t_to_yojson : err_t -> Yojson.Safe.t
val err_t_of_yojson : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
val list_actions : unit -> (action * string list * string list) list
val action_from_str : string -> action option
val action_to_str : action -> string
val map_base_err : ('a, BaseMemory.err_t) Stdlib.result Gillian.Monadic.Delayed.t -> ('a, err_t) Stdlib.result Gillian.Monadic.Delayed.t
val map_added_err : ('a, Addition.err_t) Stdlib.result Gillian.Monadic.Delayed.t -> ('a, err_t) Stdlib.result Gillian.Monadic.Delayed.t
val can_fix : err_t -> bool
val get_fixes : err_t -> BaseMemory.pred States.MyAsrt.t list list
val execute_action : action -> BaseMemory.t -> Gillian.Gil_syntax.Expr.t list -> (BaseMemory.t * Gillian.Gil_syntax.Expr.t list, err_t) Stdlib.result Monadic__Delayed.t