Module Make_Concrete.State

val vt_to_yojson : vt -> Yojson.Safe.t
val vt_of_yojson : Yojson.Safe.t -> vt Ppx_deriving_yojson_runtime.error_or
val pp_vt : Ppx_deriving_runtime.Format.formatter -> vt -> Ppx_deriving_runtime.unit
val show_vt : vt -> Ppx_deriving_runtime.string
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type store_t = Engine.CStore.t
val m_err_t_to_yojson : m_err_t -> Yojson.Safe.t
val m_err_t_of_yojson : Yojson.Safe.t -> m_err_t Ppx_deriving_yojson_runtime.error_or
type err_t = (m_err_t, vt) Engine.StateErr.t
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 pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
exception Internal_State_Error of err_t list * t
type action_ret = (t * vt list, err_t) Engine.Res_list.t
type variants_t = (string, Gillian.Gil_syntax.Expr.t option) Utils.Prelude.Hashtbl.t
val variants_t_to_yojson : variants_t -> Yojson.Safe.t
val variants_t_of_yojson : Yojson.Safe.t -> variants_t Ppx_deriving_yojson_runtime.error_or
val execute_action : string -> t -> vt list -> action_ret
val is_overlapping_asrt : string -> bool
val eval_expr : t -> Gillian.Gil_syntax.Expr.t -> vt
val get_store : t -> store_t
val set_store : t -> store_t -> t
val assume : ?unfold:bool -> t -> vt -> t list
val assume_a : ?matching:bool -> ?production:bool -> ?time:string -> t -> Gillian.Gil_syntax.Formula.t list -> t option
val assume_t : t -> vt -> Gillian.Gil_syntax.Type.t -> t option
val sat_check : t -> vt -> bool
val sat_check_f : t -> Gillian.Gil_syntax.Formula.t list -> st option
val assert_a : t -> Gillian.Gil_syntax.Formula.t list -> bool
val equals : t -> vt -> vt -> bool
val get_type : t -> vt -> Gillian.Gil_syntax.Type.t option
val simplify : ?save:bool -> ?kill_new_lvars:bool -> ?matching:bool -> t -> st * t list
val simplify_val : t -> vt -> vt
val fresh_loc : ?loc:vt -> t -> vt
val pp : Stdlib.Format.formatter -> t -> unit
val pp_by_need : Utils.Containers.SS.t -> Utils.Containers.SS.t -> Utils.Containers.SS.t -> Stdlib.Format.formatter -> t -> unit
val pp_err : Stdlib.Format.formatter -> err_t -> unit
val get_recovery_tactic : t -> err_t list -> vt Engine.Recovery_tactic.t
val copy : t -> t
val add_spec_vars : t -> Gillian.Gil_syntax.Var.Set.t -> t
val get_spec_vars : t -> Gillian.Gil_syntax.Var.Set.t
val get_lvars : t -> Gillian.Gil_syntax.Var.Set.t
val to_assertions : ?to_keep:Utils.Containers.SS.t -> t -> Gillian.Gil_syntax.Asrt.t list
val match_invariant : 'a Engine.MP.prog -> bool -> t -> Gillian.Gil_syntax.Asrt.t -> string list -> (t * t, err_t) Engine.Res_list.t
val frame_on : t -> (string * t) list -> string list -> (t, err_t) Engine.Res_list.t
val run_spec : Engine.MP.spec -> t -> string -> vt list -> (string * (string * vt) list) option -> (t * Gillian.Gil_syntax.Flag.t, err_t) Engine.Res_list.t
val sure_is_nonempty : t -> bool
val unfolding_vals : t -> Gillian.Gil_syntax.Formula.t list -> vt list
val try_recovering : t -> vt Engine.Recovery_tactic.t -> (t list, string) Stdlib.result
val substitution_in_place : ?subst_all:bool -> st -> t -> t list
val clean_up : ?keep:Gil_syntax.Expr.Set.t -> t -> unit
val match_assertion : t -> st -> Engine.MP.step -> (t, err_t) Engine.Res_list.t
val produce_posts : t -> st -> Gillian.Gil_syntax.Asrt.t list -> t list
val update_subst : t -> st -> unit
val mem_constraints : t -> Gillian.Gil_syntax.Formula.t list
val can_fix : err_t -> bool
val get_failing_constraint : err_t -> Gillian.Gil_syntax.Formula.t
val get_fixes : err_t -> Gillian.Gil_syntax.Asrt.t list list
val get_equal_values : t -> vt list -> vt list
val get_heap : t -> heap_t
val init : init_data -> t