module Node:sig..end
Node of the search graph
typet =Ast.node_cube
the type of nodes constructed during the search
val variables : t -> Variable.t listreturns the variables of the associated cube
val array : t -> Types.ArrayAtom.treturns the conjunction in array form of the associated cube
val litterals : t -> Types.SAtom.treturns the conjunction of litterals of the associated cube
val dim : t -> intreturns the dimension of the associated cube (see Cube.dim)
val size : t -> intreturns the size of the associated cube (see Cube.size)
val create : ?kind:Ast.kind -> ?from:Ast.trace_step option -> Cube.t -> tgiven a cube creates a node with a given kind, and a history
val compare_by_breadth : t -> t -> intcompare 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 -> intcompare 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 -> treturns the origin of the node, i.e. its further ancestor
val has_deleted_ancestor : t -> boolreturns true if one of the ancestor has been set to deleted
val ancestor_of : t -> t -> boolancestor_of a b returns true if a is an ancestor of b
val subset : t -> t -> boolreturns 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 -> unitprints the cube of a node
val print_history : Format.formatter -> t -> unitprints the trace corresponding to the history of a node