#include "clist.h"

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

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.)