1 /*-----------------------------------------------------------------------
2 
3 File  : ccl_global_indices.h
4 
5 Author: Stephan Schulz (schulz@eprover.org)
6 
7 Contents
8 
9   Code abstracting several (optional) indices into one structure.
10 
11   Copyright 2010 by the author.
12   This code is released under the GNU General Public Licence and
13   the GNU Lesser General Public License.
14   See the file COPYING in the main E directory for details..
15   Run "eprover -h" for contact information.
16 
17 Changes
18 
19 <1> Fri May  7 21:13:39 CEST 2010
20     New
21 
22 -----------------------------------------------------------------------*/
23 
24 #ifndef CCL_GLOBAL_INDICES
25 
26 #define CCL_GLOBAL_INDICES
27 
28 #include <ccl_subterm_index.h>
29 #include <ccl_overlap_index.h>
30 #include <ccl_clausesets.h>
31 
32 
33 /*---------------------------------------------------------------------*/
34 /*                    Data type declarations                           */
35 /*---------------------------------------------------------------------*/
36 
37 
38 typedef struct global_indices_cell
39 {
40    char              rw_bw_index_type[MAX_PM_INDEX_NAME_LEN];
41    char              pm_from_index_type[MAX_PM_INDEX_NAME_LEN];
42    char              pm_into_index_type[MAX_PM_INDEX_NAME_LEN];
43    char              pm_negp_index_type[MAX_PM_INDEX_NAME_LEN];
44    Sig_p             sig;
45    SubtermIndex_p    bw_rw_index;
46    OverlapIndex_p    pm_from_index;
47    OverlapIndex_p    pm_into_index;
48    OverlapIndex_p    pm_negp_index;
49 }GlobalIndices, *GlobalIndices_p;
50 
51 
52 /*---------------------------------------------------------------------*/
53 /*                Exported Functions and Variables                     */
54 /*---------------------------------------------------------------------*/
55 
56 PERF_CTR_DECL(PMIndexTimer);
57 PERF_CTR_DECL(BWRWIndexTimer);
58 
59 
60 void GlobalIndicesNull(GlobalIndices_p indices);
61 void GlobalIndicesInit(GlobalIndices_p indices,
62                        Sig_p sig,
63                        char* rw_bw_index_type,
64                        char* pm_from_index_type,
65                        char* pm_into_index_type);
66 
67 void GlobalIndicesFreeIndices(GlobalIndices_p indices);
68 void GlobalIndicesReset(GlobalIndices_p indices);
69 
70 
71 void GlobalIndicesInsertClause(GlobalIndices_p indices, Clause_p clause);
72 void GlobalIndicesDeleteClause(GlobalIndices_p indices, Clause_p clause);
73 void GlobalIndicesInsertClauseSet(GlobalIndices_p indices, ClauseSet_p set);
74 
75 
76 #endif
77 
78 /*---------------------------------------------------------------------*/
79 /*                        End of File                                  */
80 /*---------------------------------------------------------------------*/
81 
82 
83 
84 
85 
86