1
/* Copyright (C) 2006, 2007 William McCune
3
This file is part of the LADR Deduction Library.
5
The LADR Deduction Library is free software; you can redistribute it
6
and/or modify it under the terms of the GNU General Public License,
9
The LADR Deduction Library is distributed in the hope that it will be
10
useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12
GNU General Public License for more details.
14
You should have received a copy of the GNU General Public License
15
along with the LADR Deduction Library; if not, write to the Free Software
16
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
25
This package has code for indexing clauses that are to be retrieved in
26
pairs. When a clause is inserted, its weight is given. Retrieval
27
is by sum of the weights of the pair -- lowest first. Say we have
28
clauses with weights 0--4. Then pairs will be returned in this order:
40
Clauses can be inserted or deleted after retrieval has begun; the smallest
41
available pair will always be returned. When the index is
42
initialized, the caller supplies a parameter N, and the actual
43
weight range for indexing will be 0...N-1. If an inserted clause has
44
weight outside of this range, the weight will be changed to 0 or N-1.
46
This is intended to be used for binary inference rules such as
47
paramodulation and resolution.
48
It is similar to the method in ``A Theorem-Proving Language
49
for Experimentation'' by Henschen, Overbeek, Wos, CACM 17(6), 1974.
52
/* Public definitions */
54
typedef struct pair_index * Pair_index;
56
/* End of public definitions */
58
/* Public function prototypes from pindex.c */
60
void fprint_pindex_mem(FILE *fp, BOOL heading);
64
Pair_index init_pair_index(int n);
66
void zap_pair_index(Pair_index p);
68
int pairs_exhausted(Pair_index p);
70
void insert_pair_index(Topform c, int wt, Pair_index p);
72
void delete_pair_index(Topform c, int wt, Pair_index p);
74
void retrieve_pair(Pair_index p, Topform *cp1, Topform *cp2);
76
int pair_already_used(Topform c1, int weight1,
77
Topform c2, int weight2,
80
#endif /* conditional compilation of whole file */