node_ptr
append_ns(
node_ptr x,
node_ptr y
)
- Constructs a new list by concatenating its arguments.
- Side Effects The modified list is returned. No side effects on
the returned list were performed.
- Defined in
node.c
node_ptr
append(
node_ptr x,
node_ptr y
)
- Constructs a new list by concatenating its arguments.
- Side Effects The modified list is returned. Side effects on
the returned list were performed. It is equivalent to the lisp NCONC
- Defined in
node.c
node_ptr
car(
node_ptr x
)
- Returns the left branch of a node.
- Side Effects None
- See Also
cdr
cons
- Defined in
node.c
node_ptr
cdr(
node_ptr x
)
- Returns the right branch of a node.
- Side Effects None
- See Also
car
cons
- Defined in
node.c
node_ptr
cons(
node_ptr x,
node_ptr y
)
- Conses two nodes.
- Side Effects None
- See Also
car
cdr
- Defined in
node.c
node_ptr
copy_list(
node_ptr list
)
- An invoker should free the returned list.
- Side Effects free_list
- Defined in
node.c
node_ptr
even_elements(
node_ptr l
)
- Extracts even elements of list L.
- Side Effects None
- See Also
odd_elements
- Defined in
node.c
node_ptr
find_atom(
node_ptr a
)
- Search the node hash for a given
node. If the node is not Nil, and the node is not stored in
the hash, the new node is created, stored in the hash and then returned.
- Side Effects The node hash may change.
- See Also
find_node
- Defined in
node.c
node_ptr
find_node(
int type,
node_ptr left,
node_ptr right
)
- A new node of type type and
left and right branch left and right respectively
is created. The returned node is stored in the node hash.
- Side Effects The node hash is modified.
- See Also
new_node
- Defined in
node.c
void
free_list(
node_ptr l
)
- Frees all the elements of the list for further use.
- Side Effects None
- See Also
car
- Defined in
node.c
void
free_node(
node_ptr node
)
- Free a node of the node manager. The
node is available for next node allocation.
- Side Effects None
- Defined in
node.c
int
in_list(
node_ptr n,
node_ptr list
)
- Checks list R to see if it contains the element N.
- Side Effects None
- See Also
node_subtract
- Defined in
node.c
node_ptr
insert_node(
node_ptr node
)
- Checks if node is in the cache, if it is the
case then the hashed value is returned, else a new one is created,
stored in the hash and returned.
- Side Effects None
- See Also
find_node
- Defined in
node.c
int
is_list_empty(
node_ptr list
)
- Returns 1 is the list is empty, 0 otherwise
- Side Effects None
- Defined in
node.c
node_ptr
last(
node_ptr x
)
- Returns the last cons in X.
- Side Effects None
- See Also
car
- Defined in
node.c
int
llength(
node_ptr r
)
- Returns the length of list r.
- Side Effects None
- Defined in
node.c
node_ptr
map2(
NPFNN fun,
node_ptr l1,
node_ptr l2
)
- Applies FUN to successive cars of LISTs and
returns the results as a list. l1 and l2 must have the same length
- Side Effects None
- See Also
map
walk
- Defined in
node.c
node_ptr
map(
NPFN fun,
node_ptr l
)
- Applies FUN to successive cars of LISTs and
returns the results as a list.
- Side Effects None
- See Also
map2
walk
- Defined in
node.c
node_ptr
new_lined_node(
int type,
node_ptr left,
node_ptr right,
int lineno
)
- The same as new_node except the line number
is explicitly proved. A new node of type type, with
left and right branch left and right respectively
and on the line number lineno is created.
The returned node is not stored in the node hash.
- Side Effects None
- See Also
new_node
find_node
- Defined in
node.c
node_ptr
new_list(
)
- Returns a new empty list
- Side Effects None
- Defined in
node.c
node_ptr
new_node(
int type,
node_ptr left,
node_ptr right
)
- A new node of type type and
left and right branch left and right respectively
is created. The returned node is not stored in the node hash.
- Side Effects None
- See Also
find_node
- Defined in
node.c
node_ptr
node_alloc(
)
- Allocates NODE_MEM_CHUNK records and stores them
in the free list of the node manager.
- Side Effects The free list of the node manager is
updated by appending the new allocated nodes.
- Defined in
node.c
unsigned
node_eq_fun(
node_ptr node1,
node_ptr node2
)
- Equality function for node hash.
- Side Effects None
- See Also
node_hash_fun
- Defined in
node.c
unsigned
node_hash_fun(
node_ptr node
)
- Hash function for nodes.
- Side Effects None
- See Also
node_eq_fun
- Defined in
node.c
void
node_init(
)
- The node manager is initialized.
- Side Effects None
- Defined in
node.c
inline int
node_is_failure(
node_ptr x
)
- Returns 0 if given node is not a FAILURE node
- Defined in
node.c
node_ptr
node_normalize(
node_ptr sexp
)
- Traverses the tree, and returns a possibly new tree that
is a normalized copy of the first. Use for constant-time comparison
of two trees
- Defined in
node.c
MasterPrinter_ptr
node_pkg_get_global_master_wff_printer(
)
- Returns the global master wff printer.
- Defined in
nodePkg.c
void
node_pkg_init(
)
- Creates master and printers, and initializes the node
structures
- See Also
node_pkg_quit
- Defined in
nodePkg.c
void
node_pkg_quit(
)
- Deinitializes the packages, finalizing all internal
structures
- See Also
node_pkg_init
- Defined in
nodePkg.c
void
node_quit(
)
- Quits the node manager. All the
memory allocated it's freed.
- Side Effects All the memory allocated by the node
manager are left to the operating system.
- Defined in
node.c
void
node_set_type(
node_ptr x,
int type
)
- Replaces the type of the node
- Side Effects Replaces the type of the node
- See Also
car
cdr
cons
setcar
node_get_type
- Defined in
node.c
node_ptr
node_subtract(
node_ptr set1,
node_ptr set2
)
- Deletes elements of list set1 from list set2
without doing side effect. The resulting list is returned.
- Side Effects None
- Defined in
node.c
node_ptr
odd_elements(
node_ptr l
)
- Extracts odd elements of list L.
- Side Effects None
- See Also
even_elements
- Defined in
node.c
int
print_node(
FILE * stream,
node_ptr n
)
- Pretty print a formula on a file
- Defined in
nodeWffPrint.c
void
print_sexp_custom(
FILE * file,
node_ptr node,
custom_print_sexp_t cps_fun
)
- In order to allow handling of unknown node types
(for example, to print expressions based on any SMV extension), one can
specify an external recursion function. On unknown node types
this external function is supposed to return true iff an exception
occurred on handling of external node types. In such cases an
un-handled message type is generated.
- See Also
print_sexp
- Defined in
nodePrint.c
node_ptr
reverse_ns(
node_ptr l
)
- reverses the list with no side-effect
Description [Returns a reversed version of the given list
- Side Effects None
- Defined in
node.c
node_ptr
reverse(
node_ptr x
)
- Returns a new sequence containing the same
elements as X but in reverse order.
- Side Effects None
- See Also
last
car
cons
append
- Defined in
node.c
void
setcar(
node_ptr x,
node_ptr y
)
- Replaces the car of X with Y
- Side Effects The car of X is replaced by Y.
- See Also
car
cdr
cons
setcdr
- Defined in
node.c
void
setcdr(
node_ptr x,
node_ptr y
)
- Replaces the cdr of X with Y
- Side Effects The cdr of X is replaced by Y.
- See Also
car
cdr
cons
setcar
- Defined in
node.c
char*
sprint_node(
node_ptr n
)
- Pretty print a formula into a string. The returned
string must be freed after using it.
- Defined in
nodeWffPrint.c
void
swap_nodes(
node_ptr * n1,
node_ptr * n2
)
- Swaps two nodes.
- Side Effects The two nodes are swapped.
- Defined in
node.c
void
walk(
VPFN fun,
node_ptr l
)
- Applies FUN to successive cars of LISTs.
- Side Effects None
- See Also
map
- Defined in
node.c
(
)
- Casts the given int to a node_ptr
- Defined in
node.h
(
)
- Casts the given node_ptr to an int
- Defined in
node.h
(
)
- Casts the given pointer to a node_ptr
- Defined in
node.h