module Node:`sig`

..`end`

Node of the search graph

Node of the search graph

type`t =`

`Ast.node_cube`

the type of nodes constructed during the search

`val variables : ``t -> Variable.t list`

returns the variables of the associated cube

`val array : ``t -> Types.ArrayAtom.t`

returns the conjunction in array form of the associated cube

`val litterals : ``t -> Types.SAtom.t`

returns the conjunction of litterals of the associated cube

`val dim : ``t -> int`

returns the dimension of the associated cube (see

`Cube.dim`

)`val size : ``t -> int`

returns the size of the associated cube (see

`Cube.size`

)`val create : ``?kind:Ast.kind -> ?from:Ast.trace_step option -> Cube.t -> t`

given a cube creates a node with a given kind, and a history

`val compare_by_breadth : ``t -> t -> int`

compare two nodes with a heuristic to find the most general one. Gives
priority to nodes that have smaller depth in the search graph

`val compare_by_depth : ``t -> t -> int`

compare two nodes with a heuristic to find the most general one. Gives
priority to nodes that have bigger depth in the search graph

`val origin : ``t -> t`

returns the origin of the node, i.e. its further ancestor

`val has_deleted_ancestor : ``t -> bool`

returns

`true`

if one of the ancestor has been set to deleted`val ancestor_of : ``t -> t -> bool`

`ancestor_of a b`

returns `true`

if `a`

is an ancestor of `b`

`val subset : ``t -> t -> bool`

returns true if the set of litterals of the cube associated with the first
arguement is a subset of the second argument

`val print : ``Format.formatter -> t -> unit`

prints the cube of a node

`val print_history : ``Format.formatter -> t -> unit`

prints the trace corresponding to the history of a node