# #include "clist.h"

This page has information from files clist.h and clist.c.

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File clist.c

#### Index

clauses_in_clist | clist_length | clist_zap | neg_clauses_in_clist
clist_append | clist_member | copy_clist_to_plist_shallow | neg_nonunit_in_clist
clist_append_all | clist_move_clauses | equality_in_clist | p_clist
clist_append_plist | clist_number_of_weight | fprint_clause_clist | p_clist_mem
clist_check | clist_prepend | fprint_clist | plist_to_clist
clist_empty | clist_remove | fprint_clist_mem | pos_in_clist
clist_free | clist_remove_all | horn_clist | prepend_clist_to_plist
clist_init | clist_remove_all_clauses | max_wt_in_clist | sort_clist_by_id
clist_insert_after | clist_reverse | move_clist_to_plist | unit_clist
clist_insert_before | clist_swap | name_clist |

#### Details

    Plist clauses_in_clist(Plist p, Clist l);

Return the intersection of Plist p of clauses and Clist c of clauses.

    void clist_append(Topform c, Clist l);

This routine appends a Topform to a Clist.

    void clist_append_all(Clist l1, Clist l2);

Append each member of l2 to l1, then zap l2. Do not refer to l2 after the call.

    void clist_append_plist(Clist lst, Plist clauses);

    void clist_check(Clist l);

This routine checks the integrity of a Clist. If any errors are found, a message is sent to stdout. This is used for debugging.

    BOOL clist_empty(Clist lst);

This function checks if a (non-NULL) Clist is empty.

    void clist_free(Clist p);

This routine frees an empty Clist. If the Clist is not empty, nothing happens.

    Clist clist_init(char *name);

This routine allocates and returns an empty Clist, which is a doubly-linked list of pointers to clauses. You give it a string (any length, which is copied), representing the name of the list. If don't wish to name the list, send NULL. (You can name the list later with name_clist().)

    void clist_insert_after(Topform c, Clist_pos pos);

This routine inserts a Topform after a given position in a Clist.

    void clist_insert_before(Topform c, Clist_pos pos);

This routine inserts a Topform before a given position in a Clist.

    int clist_length(Clist l);

    int clist_member(Topform c, Clist l);

This Boolean routine checks if a Topform is a member of a Clist.

    void clist_move_clauses(Clist a, Clist b);

Move all clauses from a to the end of b.

    int clist_number_of_weight(Clist lst, int weight);

    void clist_prepend(Topform c, Clist l);

This routine inserts a Topform as the first member of a Clist.

    void clist_remove(Topform c, Clist l);

This routine removes a clause from a Clist. If the Topform occurs more than once in the Clist, the most recently inserted occurrence is removed. A fatal error occurs if the Topform is not in the Clist.

    int clist_remove_all(Topform c);

This routine removes a clause from all lists in which it occurs. The number of lists from which it was removed is returned.

    void clist_remove_all_clauses(Clist l);

This routine removes all clauses from a clist. The clauses are NOT deleted, even if they occur nowhere else.

    void clist_reverse(Clist l);

Reverse a Clist.

    void clist_swap(Topform a, Topform b);

Every clause occurs in a set (maybe empty) of Clists. Given clauses A and B, this routine puts A into the lists in which B occurs and vice versa.

    void clist_zap(Clist l);

For each Topform (occurrence) in a Clist, remove it, and if it occurs in no other Clist, call zap_topform() to delete the clause. Then, free the Clist.

    Plist copy_clist_to_plist_shallow(Clist a);

    BOOL equality_in_clist(Clist l);

Does the list contain a clause with a positive equality literal?

    void fprint_clause_clist(FILE *fp, Clist lst);

This routine prints (to FILE *fp) a Clist of clauses in standard prefix form.

    void fprint_clist(FILE *fp, Clist l);

This routine prints (to FILE *fp) each clause in a Clist. If the Clist has a non-empty name, say "usable", the string "list(usable).\n" is printed first. The string "end_of_list.\n" is always printed at the end.

    void fprint_clist_mem(FILE *fp, BOOL heading);

This routine prints (to FILE *fp) memory usage statistics for data types associated with the clist package. The Boolean argument heading tells whether to print a heading on the table.

    BOOL horn_clist(Clist l);

Is every clause in the list a Horn clause?

    int max_wt_in_clist(Clist l);

Scan a Clist, and return the maximum clause weight seen.

    Plist move_clist_to_plist(Clist a);

    void name_clist(Clist p, char *name);

This routine names or renames a Clist. The string you supply can be any length and is copied.

    Plist neg_clauses_in_clist(Clist a);

    BOOL neg_nonunit_in_clist(Clist l);

Does the list contain a negative nonunit clause ?

    void p_clist(Clist l);

This routine prints (to stdout) each clause in a Clist. See fprint_clist().

    void p_clist_mem();

This routine prints (to stdout) memory usage statistics for data types associated with the clist package.

    Clist plist_to_clist(Plist p, char *name);

    Clist_pos pos_in_clist(Clist lst, Topform c);

Return the Clist_pos of a Topform in a Clist.

    Plist prepend_clist_to_plist(Plist p, Clist c);

    void sort_clist_by_id(Clist lst);

    BOOL unit_clist(Clist l);

Is every clause in the list a unit clause?

## Public Definitions in File clist.h

    typedef struct clist_pos * Clist_pos;
    typedef struct clist * Clist;

    struct clist {
      char       *name;
      Clist_pos  first, last;
      int        length;
    };

    struct clist_pos {
      Clist_pos  prev, next;  /* previous and next member of Clist */
      Clist_pos  nocc;        /* next member of containment list */
      Clist      list;        /* the head of the list */
      Topform     c;          /* pointer to the clause */
    };

## Introduction

This package handles Clists, which are doubly-linked lists of (pointers to) clauses. This is the "official" way of building lists of clauses. (If you need a temporary, singly linked list, you can use Plist instead.)

An important property of Clists is that each clause knows what Clists it is on. In particular, each clause has a (singly linked) list of containing Clists, constructed from the same nodes as the ordinary Clist (see the definition of struct clist_pos).