# #include "clauses.h"

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

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File clauses.c

#### Index

all_clauses_horn | equality_in_clauses | most_literals | pos_equality_in_clauses
all_clauses_positive | intersect_clauses | neg_nonunit_clauses |
all_clauses_unit | max_clause_symbol_count | negative_clauses |
clause_member_plist | max_clause_weight | nonneg_clauses |

#### Details

    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?

## Public Definitions in File clauses.h

## Introduction

This package contains various functions on Plists of clauses.