Module BlockTree.Tree

type t = {
  1. node : Node.t;
  2. span : Range.t;
  3. children : (t * t) option;
}
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
module Lift : sig ... end
val is_concrete : t -> bool
val box_range_and_node : (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) -> Node.t -> PrintBox.t
val box_full : t -> PrintBox.t
val pp_full : Stdlib.Format.formatter -> t -> unit
val is_empty : t -> bool
val make : node:Node.t -> span:Range.t -> ?children:(t * t) -> unit -> t
val realign : t -> Gillian.Gil_syntax.Expr.t -> t
val with_children : t -> left:t -> right:t -> t Monadic.Delayed.t
val of_children_s : left:t -> right:t -> t Monadic__Delayed.t
val of_children : 'a -> left:t -> right:t -> t Monadic__Delayed.t
val update_parent_perm : t -> left:t -> right:t -> t Monadic.Delayed.t
val remove_node : t -> (t, 'a) Stdlib.result
val sval_leaf : low:Gillian.Gil_syntax.Expr.t -> perm:Perm.t -> value:SVal.t -> chunk:Chunk.t -> t
val sarr_leaf : low:Gillian.Gil_syntax.Expr.t -> perm:Perm.t -> size:Gillian.Gil_syntax.Expr.t -> array:SVArr.t -> chunk:Chunk.t -> t
val undefined : ?perm:Perm.t -> Range.t -> t
val create_root : Range.t -> t
val extend_if_needed : t -> (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) -> t Monadic__Delayed.t
val frame_range : t -> replace_node:(t -> (t, err) Stdlib.result) -> rebuild_parent:(t -> left:t -> right:t -> t Monadic.Delayed.t) -> Range.t -> (t * t, err) DR.t
val cons_node : t -> Range.t -> (Node.t * t, err) DR.t
val prod_node : t -> Range.t -> Node.t -> (t, err) DR.t
val cons_single : t -> Gillian.Gil_syntax.Expr.t -> Chunk.t -> (SVal.t * Perm.t option * t, err) DR.t
val prod_single : t -> Gillian.Gil_syntax.Expr.t -> Chunk.t -> SVal.t -> Perm.t -> (t, err) DR.t
val store : t -> Gillian.Gil_syntax.Expr.t -> Chunk.t -> SVal.t -> (t, err) DR.t
val get_perm_at : t -> Gillian.Gil_syntax.Expr.t -> (Perm.t, err) DR.t
val weak_valid_pointer : t -> Gillian.Gil_syntax.Expr.t -> (bool, err) DR.t
val lvars : t -> SS.t
val alocs : t -> SS.t
val assertions : t -> (LActions.ga * 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 : svarr_subst:(SVArr.t -> SVArr.t) -> sval_subst:(SVal.t -> SVal.t) -> le_subst:(Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) -> t -> t
val box : t -> PrintBox.t
val pp : Stdlib.Format.formatter -> t -> unit