BOOL all_clauses_horn(Plist l);Is every clause in the Plist a Horn clause?
BOOL all_clauses_positive(Plist l);Is every clause in the Plist a unit clause?
BOOL all_clauses_unit(Plist l);Is every clause in the Plist a unit clause?
Topform clause_member_plist(Plist p, Topform c);Is a clause a member of a Plist? A deep identity check is done (clause_ident).
BOOL equality_in_clauses(Plist clauses);Does the Plist contain a clause with a positive equality literal?
Plist intersect_clauses(Plist a, Plist b);Intersect 2 Plists of clauses. The order of the result is determined by the order of the first list. A deep identity check is done (clause_ident).
int max_clause_symbol_count(Plist p);Given a Plist of clauses, return the symbol_count of a clause with most symbols.
int max_clause_weight(Plist p);Given a Plist of clauses, return the weight of the heaviest clause. The weight field of the clause is used.
int most_literals(Plist clauses);Given a Plist of clauses, what is the maximum number of literals in a clause.
int neg_nonunit_clauses(Plist l);How many negative nonunits are in a Plist of clauses?
int negative_clauses(Plist l);How many negative clauses are in a Plist of clauses?
Plist nonneg_clauses(Plist clauses);Given a Plist of clauses, return the subset of nonnegative clauses.
BOOL pos_equality_in_clauses(Plist clauses);Does the Plist contain a clause with a positive equality literal?