MP (gillian.Engine.MP)

type outs = (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) list

val outs_pp : outs Fmt.t

type step = Gillian.Gil_syntax.Asrt.atom * outs

The step type represents a matching plan step, consisting of an assertion together with the possible learned outs

val step_to_yojson : step -> Yojson.Safe.t

val step_of_yojson : Yojson.Safe.t -> step Ppx_deriving_yojson_runtime.error_or

type label = string * Utils.Containers.SS.t

val label_to_yojson : label -> Yojson.Safe.t

val label_of_yojson : 
  Yojson.Safe.t ->
  label Ppx_deriving_yojson_runtime.error_or

type post = Gillian.Gil_syntax.Flag.t * Gillian.Gil_syntax.Asrt.t list

val post_to_yojson : post -> Yojson.Safe.t

val post_of_yojson : Yojson.Safe.t -> post Ppx_deriving_yojson_runtime.error_or

val pp_step : step Fmt.t

type t =

| Choice of t * t
| ConsumeStep of step * t
| LabelStep of label * t
(*
Labels provide additional existentials to be bound manually by the user
*)
| Finished of post option
(*
The optional assertion corresponds to some post-condition that may be produced after successfuly matching. For example, a matching plan corresponding to a set of specifications will contain leaves that are respectively anntated with the corresponding post.
*)

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

type pred = {

pred : Gillian.Gil_syntax.Pred.t;
def_mp : t;
guard_mp : t option;

}

type 'a with_mp = {

mp : t;
data : 'a;

}

type spec = Gillian.Gil_syntax.Spec.t with_mp

type lemma = Gillian.Gil_syntax.Lemma.t with_mp

type 'annot prog = {

preds : (string, pred) Utils.Prelude.Hashtbl.t;
specs : (string, spec) Utils.Prelude.Hashtbl.t;
lemmas : (string, lemma) Utils.Prelude.Hashtbl.t;
coverage : (string * int, int) Utils.Prelude.Hashtbl.t;
prog : ('annot, int) Gillian.Gil_syntax.Prog.t;

}

type preds_tbl_t = (string, pred) Utils.Prelude.Hashtbl.t

type err_ =

| MPSpec of string * Gillian.Gil_syntax.Asrt.t list
| MPPred of string * Gillian.Gil_syntax.Asrt.t list
| MPLemma of string * Gillian.Gil_syntax.Asrt.t list
| MPAssert of Gillian.Gil_syntax.Asrt.t * Gillian.Gil_syntax.Asrt.t list
| MPInvariant of Gillian.Gil_syntax.Asrt.t * Gillian.Gil_syntax.Asrt.t list

val pp_err_ : 
  Ppx_deriving_runtime.Format.formatter ->
  err_ ->
  Ppx_deriving_runtime.unit

val show_err_ : err_ -> Ppx_deriving_runtime.string

type err = err_ Gillian.Utils.Location.located

val pp_err : 
  Ppx_deriving_runtime.Format.formatter ->
  err ->
  Ppx_deriving_runtime.unit

val show_err : err -> Ppx_deriving_runtime.string

module KB = Gillian.Gil_syntax.Expr.Set

val learn_expr : 
  ?top_level:bool ->
  KB.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  outs

val ins_outs_expr : 
  KB.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  (KB.t * outs) list

val simplify_asrts : 
  ?sorted:bool ->
  Gillian.Gil_syntax.Asrt.t ->
  Gillian.Gil_syntax.Asrt.t

val s_init_atoms : 
  preds:(string, int list) Utils.Prelude.Hashtbl.t ->
  KB.t ->
  Gillian.Gil_syntax.Asrt.t ->
  (step list, Gillian.Gil_syntax.Asrt.t) Stdlib.result

val of_step_list : ?post:post -> ?label:label -> step list -> t

val init : 
  ?use_params:bool ->
  KB.t ->
  KB.t ->
  (string, int list) Utils.Prelude.Hashtbl.t ->
  (Gillian.Gil_syntax.Asrt.t
   * ((string * Utils.Containers.SS.t) option
      * (Gillian.Gil_syntax.Flag.t * Gillian.Gil_syntax.Asrt.t list) option))
    list ->
  (t, Gillian.Gil_syntax.Asrt.t list) Stdlib.result

val init_prog : 
  ?preds_tbl:(string, pred) Utils.Prelude.Hashtbl.t ->
  ('a, int) Gillian.Gil_syntax.Prog.t ->
  'a prog

val init_preds : 
  (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t ->
  ((string, pred) Utils.Prelude.Hashtbl.t, err) Stdlib.result

val pp : Stdlib.Format.formatter -> t -> unit

val get_pred_def : preds_tbl_t -> string -> pred

val init_pred_defs : unit -> preds_tbl_t

val pp_pred_defs : Stdlib.Format.formatter -> preds_tbl_t -> unit

val get_procs : 'a prog -> ('a, int) Gillian.Gil_syntax.Proc.t list

val get_bispecs : 'a prog -> Gillian.Gil_syntax.BiSpec.t list

val pp_asrt : 
  ?preds_printer:
    (Stdlib.Format.formatter ->
      (string * Gillian.Gil_syntax.Expr.t list) ->
      unit) ->
  preds:preds_tbl_t ->
  Stdlib.Format.formatter ->
  Gillian.Gil_syntax.Asrt.t ->
  unit

val pp_spec : 
  ?preds_printer:
    (Stdlib.Format.formatter ->
      (string * Gillian.Gil_syntax.Expr.t list) ->
      unit) ->
  preds:preds_tbl_t ->
  Stdlib.Format.formatter ->
  Gillian.Gil_syntax.Spec.t ->
  unit

val pp_normal_spec : 
  ?preds_printer:
    (Stdlib.Format.formatter ->
      (string * Gillian.Gil_syntax.Expr.t list) ->
      unit) ->
  preds:preds_tbl_t ->
  Stdlib.Format.formatter ->
  Gillian.Gil_syntax.Spec.t ->
  unit

val add_spec : 'a prog -> Gillian.Gil_syntax.Spec.t -> unit

val remove_spec : 'a prog -> string -> unit

val get_lemma : 'a prog -> string -> (lemma, unit) Stdlib.result

val update_coverage : 'a prog -> string -> int -> unit

val first_time_running : 'a prog -> string -> int -> bool