1 /*----------------------------------------------------------------------- 2 3 File : ccl_pdtrees.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Perfect discrimination trees for optimized rewriting and 10 subsumption. PDTrees are machines and have a state - each new search 11 must initialize a tree to a consistent state, and only one search 12 may be conducted at any given time. 13 14 Copyright 1998, 1999 by the author. 15 This code is released under the GNU General Public Licence and 16 the GNU Lesser General Public License. 17 See the file COPYING in the main E directory for details.. 18 Run "eprover -h" for contact information. 19 20 Changes 21 22 <1> Mon Jun 22 17:04:32 MET DST 1998 23 New 24 <2> Fri Mar 2 16:06:12 CET 2001 25 Completely rewritten 26 27 -----------------------------------------------------------------------*/ 28 29 #ifndef CCL_PDTREES 30 31 #define CCL_PDTREES 32 33 #include <clb_intmap.h> 34 #include <ccl_clausepos.h> 35 #include <clb_simple_stuff.h> 36 37 /*---------------------------------------------------------------------*/ 38 /* Data type declarations */ 39 /*---------------------------------------------------------------------*/ 40 41 42 /* A node in the perfect discrimination tree... */ 43 44 typedef struct pdt_node_cell 45 { 46 IntMap_p f_alternatives; /* Function symbols */ 47 PDArray_p v_alternatives; /* Variables */ 48 FunCode max_var; /* Largest variable... */ 49 long size_constr; /* Only terms that have at 50 least this weight are 51 indexed at or beyond this 52 node */ 53 SysDate age_constr; /* Only clauses that are older 54 than this date are indexed 55 at or beyond this node */ 56 struct pdt_node_cell *parent; /* Back-pointer to next node 57 towards the root */ 58 long ref_count; /* How many entries share this 59 node? */ 60 PTree_p entries; /* Clauses that are indexed 61 - this should be NULL at 62 all but leaf nodes. */ 63 Term_p variable; /* If this node corresponds 64 to a variable, point to it 65 (so that we can bind it 66 while searching for 67 matches) */ 68 bool bound; /* Did we bind a variable (in 69 fact, the one above...) to 70 reach this node? I.e. do we 71 need to backtrack this 72 binding if we backtrack 73 over this node? */ 74 FunCode trav_count; /* For traversing during 75 matching. Both 0 and 76 node->max_var+1 represent 77 the (maximal one) function 78 symbol alternative, i is 79 variable i. */ 80 }PDTNodeCell, *PDTNode_p; 81 82 /* A PDTreeCell is an object encapsulating a PDTree and the necessary 83 data structures to efficiently seach it */ 84 85 typedef struct pd_tree_cell 86 { 87 PDTNode_p tree; 88 PStack_p term_stack; /* For flattening the term */ 89 PStack_p term_proc; /* Store traversed terms for backtracking */ 90 PDTNode_p tree_pos; /* For traversing the tree */ 91 PStack_p store_stack; /* For traversing entries in leaves */ 92 Term_p term; /* ...used as a key during search */ 93 SysDate term_date; /* Temporarily bound during matching */ 94 long term_weight; /* Ditto */ 95 int prefer_general; /* Ditto */ 96 long node_count; /* How many tree nodes? */ 97 long clause_count; /* How many clauses? */ 98 long arr_storage_est;/* How much memory used by arrays? */ 99 unsigned long match_count; /* How often has the index been 100 searched? */ 101 unsigned long visited_count; /* How many nodes in the index have 102 been visited? */ 103 }PDTreeCell, *PDTree_p; 104 105 /*---------------------------------------------------------------------*/ 106 /* Exported Functions and Variables */ 107 /*---------------------------------------------------------------------*/ 108 109 #ifdef PDT_COUNT_NODES 110 #define PDT_COUNT_INC(x) ((x)++) 111 extern unsigned long PDTNodeCounter; 112 #else 113 #define PDT_COUNT_INC(x) 114 #endif 115 116 117 #define PDNODE_FUN_INIT_ALT 8 118 #define PDNODE_FUN_GROW_ALT 6 119 #define PDNODE_VAR_INIT_ALT 4 120 #define PDNODE_VAR_GROW_ALT 4 121 122 #define PDTREE_IGNORE_TERM_WEIGHT LONG_MAX 123 #define PDTREE_IGNORE_NF_DATE SysDateCreationTime() 124 #define PDT_NODE_INIT_VAL(tree) ((tree)->prefer_general) 125 #define PDT_NODE_CLOSED(tree,node) ((tree)->prefer_general?\ 126 (((node)->max_var)+2):(((node)->max_var)+1)) 127 128 #define PDTreeCellAlloc() (PDTreeCell*)SizeMalloc(sizeof(PDTreeCell)) 129 #define PDTreeCellFree(junk) SizeFree(junk, sizeof(PDTreeCell)) 130 131 #ifdef CONSTANT_MEM_ESTIMATE 132 #define PDTREE_CELL_MEM 16 133 #else 134 #define PDTREE_CELL_MEM MEMSIZE(PDTreeCell) 135 #endif 136 137 PDTree_p PDTreeAlloc(void); 138 void PDTreeFree(PDTree_p tree); 139 140 #ifdef CONSTANT_MEM_ESTIMATE 141 #define PDTNODE_MEM 52 142 #else 143 #define PDTNODE_MEM MEMSIZE(PDTNodeCell) 144 #endif 145 146 #define PDTreeStorage(tree) \ 147 ((tree)\ 148 ?\ 149 ((tree)->node_count*PDTNODE_MEM\ 150 +(tree)->arr_storage_est\ 151 +(tree)->clause_count*(PDTREE_CELL_MEM+CLAUSEPOSCELL_MEM))\ 152 :\ 153 0) 154 155 extern bool PDTreeUseAgeConstraints; 156 extern bool PDTreeUseSizeConstraints; 157 158 #define PDTNodeGetSizeConstraint(node) ((node)->size_constr != -1 ? (node)->size_constr : pdt_compute_size_constraint((node))) 159 #define PDTNodeGetAgeConstraint(node) (!SysDateIsInvalid((node)->age_constr))? (node)->age_constr: pdt_compute_age_constraint((node)) 160 161 #define PDTNodeCellAlloc() (PDTNodeCell*)SizeMalloc(sizeof(PDTNodeCell)) 162 #define PDTNodeCellFree(junk) SizeFree(junk, sizeof(PDTNodeCell)) 163 PDTNode_p PDTNodeAlloc(void); 164 void PDTNodeFree(PDTNode_p tree); 165 166 void TermLRTraverseInit(PStack_p stack, Term_p term); 167 Term_p TermLRTraverseNext(PStack_p stack); 168 Term_p TermLRTraversePrev(PStack_p stack, Term_p term); 169 170 void PDTreeInsert(PDTree_p tree, ClausePos_p demod_side); 171 long PDTreeDelete(PDTree_p tree, Term_p term, Clause_p clause); 172 173 void PDTreeSearchInit(PDTree_p tree, Term_p term, SysDate 174 age_constr, bool prefer_general); 175 void PDTreeSearchExit(PDTree_p tree); 176 177 PDTNode_p PDTreeFindNextIndexedLeaf(PDTree_p tree, Subst_p subst); 178 179 ClausePos_p PDTreeFindNextDemodulator(PDTree_p tree, Subst_p subst); 180 181 void PDTreePrint(FILE* out, PDTree_p tree); 182 183 #endif 184 185 /*---------------------------------------------------------------------*/ 186 /* End of File */ 187 /*---------------------------------------------------------------------*/ 188 189 190 191 192 193 194