~ubuntu-branches/ubuntu/saucy/ladr/saucy

« back to all changes in this revision

Viewing changes to ladr/pindex.h.bak

  • Committer: Package Import Robot
  • Author(s): Frank Lichtenheld
  • Date: 2013-05-25 11:43:32 UTC
  • mfrom: (5.1.5 sid)
  • Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.

Show diffs side-by-side

added added

removed removed

Lines of Context:
1
 
/*  Copyright (C) 2006, 2007 William McCune
2
 
 
3
 
    This file is part of the LADR Deduction Library.
4
 
 
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,
7
 
    version 2.
8
 
 
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.
13
 
 
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.
17
 
*/
18
 
 
19
 
#ifndef TP_PINDEX_H
20
 
#define TP_PINDEX_H
21
 
 
22
 
#include "clist.h"
23
 
 
24
 
/* INTRODUCTION
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:
29
 
<PRE>
30
 
(0,0)
31
 
(0,1)
32
 
(1,1)  (0,2)
33
 
(1,2)  (0,3)
34
 
(2,2)  (1,3)  (0,4)
35
 
(2,3)  (1,4)
36
 
(3,3)  (2,4)
37
 
(3,4)
38
 
(4,4)
39
 
</PRE>
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.
45
 
<P>
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.
50
 
*/
51
 
 
52
 
/* Public definitions */
53
 
 
54
 
typedef struct pair_index * Pair_index;
55
 
 
56
 
/* End of public definitions */
57
 
 
58
 
/* Public function prototypes from pindex.c */
59
 
 
60
 
void fprint_pindex_mem(FILE *fp, BOOL heading);
61
 
 
62
 
void p_pindex_mem();
63
 
 
64
 
Pair_index init_pair_index(int n);
65
 
 
66
 
void zap_pair_index(Pair_index p);
67
 
 
68
 
int pairs_exhausted(Pair_index p);
69
 
 
70
 
void insert_pair_index(Topform c, int wt, Pair_index p);
71
 
 
72
 
void delete_pair_index(Topform c, int wt, Pair_index p);
73
 
 
74
 
void retrieve_pair(Pair_index p, Topform *cp1, Topform *cp2);
75
 
 
76
 
int pair_already_used(Topform c1, int weight1,
77
 
                      Topform c2, int weight2,
78
 
                      Pair_index p);
79
 
 
80
 
#endif  /* conditional compilation of whole file */