#include "clauses.h"

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

Contents


Public Routines in File clauses.c

Index

all_clauses_hornequality_in_clausesmost_literalspos_equality_in_clauses
all_clauses_positiveintersect_clausesneg_nonunit_clauses
all_clauses_unitmax_clause_symbol_countnegative_clauses
clause_member_plistmax_clause_weightnonneg_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.