Module Verifier.SMatcher

type err_t
type state_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
type t = {
  1. state : state_t;
  2. preds : Engine.Preds.t;
  3. wands : Engine.Wands.t;
  4. pred_defs : Engine.MP.preds_tbl_t;
  5. variants : variants_t;
}
type post_res = (Gillian.Gil_syntax.Flag.t * Gillian.Gil_syntax.Asrt.t list) option
type search_state = (t * Gillian.Symbolic.Subst.t * Engine.MP.t) list * err_t list
module Logging : sig ... end
type unfold_info_t = (string * string) list
val produce_posts : t -> Gillian.Symbolic.Subst.t -> Gillian.Gil_syntax.Asrt.t list -> t list
val unfold : ?additional_bindings:unfold_info_t -> t -> string -> Gillian.Gil_syntax.Expr.t list -> (Gillian.Symbolic.Subst.t * t, err_t) Engine.Res_list.t

unfold state name args unfold_info returns a list of pairs (subst, state), resulting from unfolding the predicate name(..args..) from the given state. unfold_info contains information about how to bind new variables.

val rec_unfold : ?fuel:int -> t -> string -> Gillian.Gil_syntax.Expr.t list -> (t, err_t) Engine.Res_list.t
val unfold_all : t -> string -> (t, err_t) Engine.Res_list.t
val try_recovering : t -> Gillian.Gil_syntax.Expr.t Engine.Recovery_tactic.t -> (t list, string) Stdlib.result

Tries recovering from an error using the provided recovery tactic.

val unfold_with_vals : auto_level:[ `High | `Low ] -> t -> Gillian.Gil_syntax.Expr.t list -> (Gillian.Symbolic.Subst.t * t) list option

Tries to unfold the given predicate in the state. If it manages, it returns the new set of states and corresponding substitutions, otherwise, it returns None.

val unfold_concrete_preds : t -> (Gillian.Symbolic.Subst.t option * t) option

Unfolds 1 predicate for which all arguments are concrete.

  • If it finds one:
  • if it succeeds to unfold, it returns Some (Some subst, new_state )
  • if it fails to unfold it returns None
  • If it doesn't find one, it returns Some (None, input_state)
val match_assertion : ?no_auto_fold:bool -> t -> Gillian.Symbolic.Subst.t -> Engine.MP.step -> (t, err_t) Engine.Res_list.t
val match_ : ?in_matching:bool -> t -> Gillian.Symbolic.Subst.t -> Engine.MP.t -> Engine.Matcher.match_kind -> (t * Gillian.Symbolic.Subst.t * post_res, err_t) Engine.Res_list.t
val fold : ?in_matching:bool -> ?additional_bindings: (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) list -> match_kind:Engine.Matcher.match_kind -> state:t -> Engine.MP.pred -> Gillian.Gil_syntax.Expr.t list -> (t, err_t) Engine.Res_list.t

Folds a predicate in the state, consuming its definition and producing the folded predicate. If the predicate has a guard, the guard is produced.

val consume_pred : ?in_matching:bool -> ?fold_outs_info: (Gillian.Symbolic.Subst.t * Engine.MP.step * Gillian.Gil_syntax.Expr.t list) -> ?no_auto_fold:bool -> t -> string -> Gillian.Gil_syntax.Expr.t option list -> (t * Gillian.Gil_syntax.Expr.t list, err_t) Engine.Res_list.t

Consumes a predicate from the state. If the predicate is not "verbatim" in our set of preds, and it is not abstract and we are not in manual mode, we attempt to fold it.

val package_wand : t -> Engine.Wands.wand -> (t, err_t) Gillian.Utils.List_res.t