/usr/include/ladr/mindex.h is in libladr-dev 0.0.200911a-2.1build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 | /* Copyright (C) 2006, 2007 William McCune
This file is part of the LADR Deduction Library.
The LADR Deduction Library is free software; you can redistribute it
and/or modify it under the terms of the GNU General Public License,
version 2.
The LADR Deduction Library is distributed in the hope that it will be
useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with the LADR Deduction Library; if not, write to the Free Software
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
*/
#ifndef TP_MINDEX_H
#define TP_MINDEX_H
#include "fpa.h"
#include "discrimb.h"
#include "discrimw.h"
#include "btu.h"
#include "btm.h"
/* INTRODUCTION
This is an indexing/unification package to store terms and to
retrieve unifiable terms.
(It is really just an interface to the various indexing and
unification packages.)
Several types of indexing and unification are supported.
When you allocate an index (with mindex_init()), you specify the
type of index and the type of unification.
<P>
Types of Retrieval
<P>
<TT>UNIFY, INSTANCE, GENERALIZATION, VARIANT, IDENTICAL</TT>.
<P>
Types of Unification
<P>
Associative-commutative (AC) and commutative/symmetric (C) symbols
are supported in most cases. If you have any AC or C symbols,
you must use backtrack unification, which handles more than one
unifier for a pair of terms; otherwise, you can use ordinary unification,
which assumes at most one unifier for a pair of terms.
(For the empty theory, ordinary unification is a bit
faster than backtrack unification.)
<P>
Types of Indexing
<UL>
<LI><TT>LINEAR :</TT> This is indexing without an index.
The terms you insert are put on a list, and each is tested in turn.
This supports AC and C symbols.
<LI><TT>FPA :</TT> This is FPA/Path indexing.
Supports AC symbols (in a primitive way, by treating them
as constants) and C symbols.
<LI><TT>DISCRIM_WILD :</TT> Discrimination indexing,
where matching is separate from unidexing.
This supports AC symbols and C symbols.
With C symbols, you can get duplicate answers.
Supports <TT>GENERALIZATION</TT> retrieval only.
<LI><TT>DISCRIM_BIND :</TT> Discrimination indexing, where matching
occurs during indexing. This supports C symbols, <I>but not AC symbols</I>.
Supports <TT>GENERALIZATION</TT> retrieval only.
</UL>
*/
/* Public definitions */
/* types of index */
typedef enum { LINEAR,
FPA,
DISCRIM_WILD,
DISCRIM_BIND
} Mindextype;
/* types of unification */
typedef enum { ORDINARY_UNIF,
BACKTRACK_UNIF
} Uniftype;
typedef struct mindex * Mindex;
typedef struct mindex_pos * Mindex_pos;
struct mindex {
Mindextype index_type;
Uniftype unif_type;
/* FPA */
Fpa_index fpa;
/* LINEAR */
Plist linear_first;
Plist linear_last;
/* DISCRIM_WILD and DISCRIM_BIND */
Discrim discrim_tree;
Mindex next; /* for avail list */
};
/* End of public definitions */
/* Public function prototypes from mindex.c */
void fprint_mindex_mem(FILE *fp, BOOL heading);
void p_mindex_mem();
Mindex mindex_init(Mindextype mtype, Uniftype utype, int fpa_depth);
BOOL mindex_empty(Mindex mdx);
void mindex_free(Mindex mdx);
void mindex_destroy(Mindex mdx);
void mindex_update(Mindex mdx, Term t, Indexop op);
Term mindex_retrieve_first(Term t, Mindex mdx, Querytype qtype,
Context query_subst, Context found_subst,
BOOL partial_match,
Mindex_pos *ppos);
Term mindex_retrieve_next(Mindex_pos pos);
void mindex_retrieve_cancel(Mindex_pos pos);
void fprint_mindex(FILE *fp, Mindex mdx);
#endif /* conditional compilation of whole file */
|