#include "literals.h"

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

Public Routines
Public Definitions
Introduction

Public Routines in File literals.c

Index

any_clause	false_term	lits_to_term	positive_literals
append_literal	first_literal_of_sign	mixed_clause	remove_null_literals
atom_number	fprint_literals_mem	neg_eq	symbol_occurrences_in_clause
clause_depth	free_literals	neg_eq_unit	tautology
clause_ident	free_lits_to_term	negative_clause	term_at_position
clause_symbol_count	get_literals	negative_literals	term_to_literals
constants_in_clause	greatest_variable_in_clause	new_literal	true_clause
contains_eq	ground_clause	number_of_literals	true_term
contains_pos_eq	horn_clause	number_of_variables	unit_clause
copy_literal	ith_literal	only_eq	varnums_in_clause
copy_literals	literal_number	p_literals_mem	vars_in_clause
copy_literals_with_flag	literal_to_term	pos_eq	zap_literal
copy_literals_with_flags	literals_depth	pos_eq_unit	zap_literals
definite_clause	literals_to_term	positive_clause

Details

BOOL any_clause(Literals lits);

This function is always TRUE. (It it intended to be used as an argument.)

Literals append_literal(Literals lits, Literals lit);

This routine appends a literal to a list of literals.

int atom_number(Literals lits, Term atom);

Given a clause and an atom, return the position of the atom (counting from 1) in the clause. The check is by pointer only. If the atom does not occur in the clause, 0 is returned.

int clause_depth(Literals lits);

Disjunction and negation signs are not included in the count. That is, return the depth of the deepest atomic formula.

BOOL clause_ident(Literals lits1, Literals lits2);

Identical clauses, including order of literals and variable numbering.

int clause_symbol_count(Literals lits);

Disjunction and negation signs are not included in the count.

Ilist constants_in_clause(Literals lits);

Given a clause, return the set of symnums for constants therein.

BOOL contains_eq(Literals lits);

This function checks if a clause contains an equality literal (positive or negative) for the purposes of paramodulation and demodulation.

BOOL contains_pos_eq(Literals lits);

This function checks if a clause contains a positive equality literal for the purposes of paramodulation and demodulation.

Literals copy_literal(Literals lit);

Literals copy_literals(Literals lits);

This routine builds and returns a copy of a clause. The container field of each nonvariable subterm points to the clause.

Literals copy_literals_with_flag(Literals lits, int flag);

This routine builds and returns a copy of a clause. The given termflag is copied for all subterms (including atoms, excluding variables).

Literals copy_literals_with_flags(Literals lits);

This routine builds and returns a copy of a clause. All termflags are copied for all subterms (including atoms, excluding variables).

BOOL definite_clause(Literals lits);

This Boolean function checks if a clause has exactly one positive literal.

BOOL false_term(Term t);

Literals first_literal_of_sign(Literals lits, BOOL sign);

void fprint_literals_mem(FILE *fp, int heading);

This routine prints (to FILE *fp) memory usage statistics for data types associated with the clause package. The Boolean argument heading tells whether to print a heading on the table.

void free_literals(Literals p);

void free_lits_to_term(Term t);

This routine is to be used with terms constructed by lits_to_term().

Literals get_literals(void);

int greatest_variable_in_clause(Literals lits);

This routine returns the greatest variable index in a clause. If the clause is ground, -1 is returned.

BOOL ground_clause(Literals lits);

BOOL horn_clause(Literals lits);

This function checks if a clause has at most one positive literal.

Literals ith_literal(Literals lits, int i);

Return the i-th literal of a clause, counting from 1. Return NULL if i is out of range.

int literal_number(Literals lits, Literals lit);

Given a clause and a literal, return the position of the literal (counting from 1) in the clause. The check is by pointer only. If the literal does not occur in the clause, 0 is returned.

Term literal_to_term(Literals l);

int literals_depth(Literals lits);

This function returns the maximum depth of a list of literals. Negation signs are not counted, and P(a) has depth 1.

Term literals_to_term(Literals l);

Term lits_to_term(Literals l);

This routine converts a nonempty list of literals into a term. This version does not copy atoms; it constructs new term nodes only for the NOT and OR structure at the top of the clause. Use free_lits_to_term() to free terms constructed with this routine.

BOOL mixed_clause(Literals lits);

This function checks if a clause has at least one positive and at least one negative literal.

BOOL neg_eq(Literals lit);

This function checks if a literal is a positive equality for the purposes of paramodulation and demodulation.

BOOL neg_eq_unit(Literals lits);

This function checks if a list of Literals is a negative equality unit.

BOOL negative_clause(Literals lits);

This function checks if all of the literals of a clause are negative.

int negative_literals(Literals lits);

This function returns the number of negative literals in a clause.

Literals new_literal(int sign, Term atom);

This routine takes a sign (Boolean) and a Term atom, and returns a literal. The atom is not copied.

int number_of_literals(Literals lits);

This function returns the number of literals in a clause.

int number_of_variables(Literals lits);

This routine returns number of (distinct) variables in a clause.

BOOL only_eq(Literals lits);

This function checks if a clause contains only equality literals (positive or negative).

void p_literals_mem();

This routine prints (to stdout) memory usage statistics for data types associated with the clause package.

BOOL pos_eq(Literals lit);

This function checks if a literal is a positive equality for the purposes of paramodulation and demodulation.

BOOL pos_eq_unit(Literals lits);

This function checks if a list of Literals is a positive equality unit for the purposes of paramodulation and demodulation.

BOOL positive_clause(Literals lits);

This function checks if all of the literals of a clause are positive.

int positive_literals(Literals lits);

This function returns the number of positive literals in a clause.

Literals remove_null_literals(Literals l);

int symbol_occurrences_in_clause(Literals lits, int symnum);

BOOL tautology(Literals lits);

This routine returns TRUE if the clause has complementary literals or if it has any literals of the form $T, -$F. This dos not check for x=x.

Term term_at_position(Literals lits, Ilist pos);

Literals term_to_literals(Term t, Literals lits);

BOOL true_clause(Literals lits);

Does the clause contain a literal $T? (This does not check for complementary literals, -$F, or x=x.)

BOOL true_term(Term t);

BOOL unit_clause(Literals lits);

This function checks if a clause has exactly one literal.

Ilist varnums_in_clause(Literals lits);

This routine returns the set of variable indexes (as an Ilist) in a clause.

Plist vars_in_clause(Literals lits);

This routine returns the set of variables (as a Plist) in a clause.

void zap_literal(Literals l);

This routine frees a literal.

void zap_literals(Literals l);

This routine frees a list of literals.

Public Definitions in File literals.h

typedef struct literals * Literals;

struct literals {
  BOOL      sign;
  Term      atom;
  Literals  next;
};

#include "literals.h"

Contents

Public Routines in File literals.c

Index

Details

Public Definitions in File literals.h

Introduction