#include "pindex.h"

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

Public Routines
Public Definitions
Introduction

Public Routines in File pindex.c

Index

delete_pair_index	insert_pair_index	pairs_exhausted
fprint_pindex_mem	p_pindex_mem	retrieve_pair
init_pair_index	pair_already_used	zap_pair_index

Details

void delete_pair_index(Topform c, int wt, Pair_index p);

This routine removes a clause from a Pair_index. The parameter wt must be the same as when the clause was inserted. A fatal error may occur if the clause was not previously inserted or if it was inserted with a different weight.

void fprint_pindex_mem(FILE *fp, BOOL heading);

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

Pair_index init_pair_index(int n);

This routine allocates and initializes a Pair_index. Parameter n specifies the range 0 .. n-1 of weights that will be used. If a clause is inserted with weight outside of that range, the effective weight for pair indexing will be set to 0 or n-1.

void insert_pair_index(Topform c, int wt, Pair_index p);

This routine inserts a clause into a Pair_index. If the given weight is out of range [0 ... n-1] (where n is the parameter given to init_pair_index()), weight 0 or n-1 will be used instead.

void p_pindex_mem();

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

int pair_already_used(Topform c1, int weight1,
		      Topform c2, int weight2,
		      Pair_index p);

This Boolean routine checks if a pair of clauses (with corresponding weights) has already been retrieved.

int pairs_exhausted(Pair_index p);

This routine is TRUE if the previous call to retrieve_pair() returned nothing and no more pairs have been inserted since then. (Also, TRUE is returned if no pairs were ever inserted.)

Note that FALSE may be returned when there really no pairs available.

void retrieve_pair(Pair_index p, Topform *cp1, Topform *cp2);

This routine retrieves the next pair from a Pair_index. The caller gives addresses of clauses which are filled in with the answer. If no pair is available, NULLs are filled in.

void zap_pair_index(Pair_index p);

This routine frees a pair index. It need not be empty.

Public Definitions in File pindex.h

typedef struct pair_index * Pair_index;

Introduction

This package has code for indexing clauses that are to be retrieved in pairs. When a clause is inserted, its weight is given. Retrieval is by sum of the weights of the pair -- lowest first. Say we have clauses with weights 0--4. Then pairs will be returned in this order:

(0,0)
(0,1)
(1,1)  (0,2)
(1,2)  (0,3)
(2,2)  (1,3)  (0,4)
(2,3)  (1,4)
(3,3)  (2,4)
(3,4)
(4,4)

Clauses can be inserted or deleted after retrieval has begun; the smallest available pair will always be returned. When the index is initialized, the caller supplies a parameter N, and the actual weight range for indexing will be 0...N-1. If an inserted clause has weight outside of this range, the weight will be changed to 0 or N-1.