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
|
/*-----------------------------------------------------------------------
File : cte_idx_fp.h
Author: Stephan Schulz (schulz@eprover.org)
Contents
Compute a fingerprint of a term suitable for fingerprint indexing. A
fingerprint is a vector of individual samples for positions p, where
the result is t|p->f_code if p is a position in t, BELOW_VAR
(=LONG_MIN) if p<=q, t|q=Xn, 0 otherwise.
Copyright 2010 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details..
Run "eprover -h" for contact information.
Changes
<1> Sat Feb 20 19:19:23 EET 2010
New
-----------------------------------------------------------------------*/
#ifndef CTE_IDX_FP
#define CTE_IDX_FP
#include <stdarg.h>
#include <cte_termtypes.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/* Fingerprints of n elements are FunCode (long) arrays, with the
* first element containing the lenghts (inclusive), the others the
* results of the sampling */
typedef FunCode *IndexFP_p;
typedef IndexFP_p (*FPIndexFunction)(Term_p t);
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
extern char* FPIndexNames[];
#define MAX_PM_INDEX_NAME_LEN 20
#define BELOW_VAR -2
#define ANY_VAR -1
#define NOT_IN_TERM 0
FunCode TermFPSampleFO(Term_p term, va_list ap);
FunCode TermFPFlexSampleFO(Term_p term, IntOrP* *seq);
FunCode TermFPSample(Term_p term, ...);
#ifdef ENABLE_LFHO
FunCode TermFPSampleHO(Term_p term, va_list ap);
FunCode TermFPFlexSampleHO(Term_p term, IntOrP* *seq);
FunCode TermFPFlexSample(Term_p term, IntOrP* *seq);
#else
#define TermFPFlexSample(term, seq) (TermFPFlexSampleFO(term, seq))
#endif
IndexFP_p IndexFP0Create(Term_p t);
IndexFP_p IndexFPfpCreate(Term_p t);
IndexFP_p IndexFP1Create(Term_p t);
IndexFP_p IndexFP2Create(Term_p t);
IndexFP_p IndexFP3DCreate(Term_p t);
IndexFP_p IndexFP3WCreate(Term_p t);
IndexFP_p IndexFP4DCreate(Term_p t);
IndexFP_p IndexFP4WCreate(Term_p t);
IndexFP_p IndexFP4MCreate(Term_p t);
IndexFP_p IndexFP5MCreate(Term_p t);
IndexFP_p IndexFP6MCreate(Term_p t);
IndexFP_p IndexFP7Create(Term_p t);
IndexFP_p IndexFP7MCreate(Term_p t);
IndexFP_p IndexFP4X2_2Create(Term_p t);
IndexFP_p IndexFPFlexCreate(Term_p t, PStack_p pos, int len);
IndexFP_p IndexFP3DFlexCreate(Term_p t);
IndexFP_p IndexDTCreate(Term_p t);
void IndexFPFree(IndexFP_p junk);
FPIndexFunction GetFPIndexFunction(char* name);
void IndexFPPrint(FILE* out, IndexFP_p fp);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
