| clist_copy | copy_clauses_to_clist | delete_clist | move_clauses_to_clist |
| copy_clause_ija | delete_clause | input_clauses | |
| copy_clauses_ija | delete_clauses | make_clause_basic |
Clist clist_copy(Clist a, BOOL assign_ids);Copy a clist of clauses. Justificatons and attributes are copied, and the clauses get new IDs.
Topform copy_clause_ija(Topform c);Copy a clause, including ID, justification, attributes, and termflags. Clauses constructed with this routine should be deallocated with delete_clause().
Plist copy_clauses_ija(Plist p);Copy a Plist of clauses. Clauses are coped with copy_clause_ija(), which copies ID, justification, attributes, and termflags.
Clist copy_clauses_to_clist(Plist clauses, char *name, BOOL assign_ids);
void delete_clause(Topform c);This routine frees a clause and all of its subterms. If the clause has an ID, it is unassigned. If the clause has a justification list, it is freed.
This routine is not in the clause package, because (at this time) the clause package doesn't know about just.h or clauseid.h.
void delete_clauses(Plist p);Delete (deep) a Pist of clauses.
void delete_clist(Clist l);For each Topform in the Clist, remove it from the Clist; if it occurs in no other Clists, call delete_clause(). Finally, free the Clist.
This routine is not in the clist package, because (at this time) the clist package doesn't know about just.h or clauseid.h.
Plist input_clauses(Plist a);Given a Plist of clauses, return the Plist of input clauses (in the same order).
void make_clause_basic(Topform c);This routine clears all of the "nonbasic" marks in a clause.
Clist move_clauses_to_clist(Plist clauses, char *name, BOOL assign_ids);