States.Fractional
module DR = Gillian.Monadic.Delayed_result
module Recovery_tactic = Gillian.General.Recovery_tactic
val _0 : Gillian.Gil_syntax.Expr.t
val _1 : Gillian.Gil_syntax.Expr.t
type t = (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option
Value * Fraction
val pp :
Ppx_deriving_runtime.Format.formatter ->
t ->
Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> 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
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 action_from_str : string -> action option
val action_to_str : action -> string
val list_actions : unit -> (action * string list * string list) list
val pred_from_str : string -> pred option
val pred_to_str : pred -> string
val list_preds : unit -> (pred * string list * string list) list
val empty : unit -> t
val execute_action :
action ->
t ->
Gillian.Gil_syntax.Expr.t list ->
((Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option
* Gillian.Gil_syntax.Expr.t list,
err_t)
Stdlib.result
Monadic.Delayed.t
val consume :
pred ->
('a * Gillian.Gil_syntax.Expr.t) option ->
Gillian.Gil_syntax.Expr.t list ->
(('a * Gillian.Gil_syntax.Expr.t) option * 'a list, err_t) Stdlib.result
Gillian.Monadic.Delayed.t
val produce :
pred ->
(Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option ->
Gillian.Gil_syntax.Expr.t list ->
(Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option
Gillian.Monadic.Delayed.t
val substitution_in_place :
Gillian.Symbolic.Subst.t ->
(Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option ->
(Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option
Gillian.Monadic.Delayed.t
val compose : t -> t -> t Gillian.Monadic.Delayed.t
val is_exclusively_owned :
('a * Gillian.Gil_syntax.Expr.t) option ->
'b ->
bool Gillian.Monadic.Delayed.t
val is_concrete :
(Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option ->
bool
val instantiate :
'a list ->
(Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option * 'b list
val lvars :
(Gillian.Gil_syntax.Expr.t * 'a) option ->
Gillian.Utils.Containers.SS.t
val alocs :
(Gillian.Gil_syntax.Expr.t * 'a) option ->
Gillian.Utils.Containers.SS.t
val assertions : ('a * 'b) option -> (pred * 'b list * 'a list) list
val get_recovery_tactic : 'a -> 'b Recovery_tactic.t