Module Node (.ml)

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