1 /* 2 * cos.h -- preprocessor definitions of indices for arrays of 3 * flags, parameters, statistics, clocks, and internal flags. 4 * 5 */ 6 7 /************* 8 * 9 * Flags are boolean valued options. To install a new flag, append 10 * a new name and index to the end of this list, then insert code to 11 * initialize it in the routine `init_options'. 12 * Example access: if (Flags[PARA_FROM_LEFT].val) { 13 * See routine `init_options' for defaults. 14 * 15 *************/ 16 17 #define MAX_FLAGS 200 /* This must hold the following list! */ 18 19 enum { 20 SOS_QUEUE, /* pick first clause on sos as given clause */ 21 SOS_STACK, /* pick last sos clause as given clause */ 22 INPUT_SOS_FIRST, /* use input sos before generated sos */ 23 INTERACTIVE_GIVEN, /* user selects given clause interactively */ 24 PRINT_GIVEN, /* print given clauses */ 25 PRINT_LISTS_AT_END, /* print clause lists at end of run */ 26 27 BINARY_RES, /* binary resolution */ 28 HYPER_RES, /* hyperresolution */ 29 NEG_HYPER_RES, /* negatve hyperresolution inference rule */ 30 UR_RES, /* UR-resolution */ 31 PARA_INTO, /* `into' paramodulation inference rule */ 32 PARA_FROM, /* `from' paramodulation inference rule */ 33 DEMOD_INF, /* apply demodulation as an inference rule */ 34 35 ORDER_HYPER, /* ordered hyperresolution (satellites) */ 36 UNIT_RES, /* Unit resolution restriction */ 37 UR_LAST, /* restrict UR: target literal is last */ 38 39 PARA_FROM_LEFT, /* allow paramodulation from left sides */ 40 PARA_FROM_RIGHT, /* allow paramodulation from right sides */ 41 PARA_INTO_LEFT, /* allow paramodulation into left args of = */ 42 PARA_INTO_RIGHT, /* allow paramodulation into right args of = */ 43 PARA_FROM_VARS, /* allow paramodulation from variables */ 44 PARA_INTO_VARS, /* allow paramodulation into variables */ 45 PARA_FROM_UNITS_ONLY, /* from clause must be unit */ 46 PARA_INTO_UNITS_ONLY, /* into clause must be unit */ 47 PARA_SKIP_SKOLEM, /* Skolem function restriction strategy */ 48 PARA_ONES_RULE, /* paramod only into first args of terms */ 49 PARA_ALL, /* paramodulate all occurrences of into term */ 50 51 DETAILED_HISTORY, /* store literal numbers and position vectors */ 52 ORDER_HISTORY, /* Nucleus number first for hyper, UR. */ 53 UNIT_DELETION, /* unit deletion processing */ 54 BACK_UNIT_DELETION, /* like back demodulation, but for literals */ 55 DELETE_IDENTICAL_NESTED_SKOLEM, /* delete clauses containing */ 56 SORT_LITERALS, /* sort literals in pre_process */ 57 FOR_SUB, /* forward subsumption */ 58 BACK_SUB, /* back subsumption */ 59 FACTOR, /* factor during post_process */ 60 61 DEMOD_HISTORY, /* build history in demodulation */ 62 ORDER_EQ, /* flip equalities (+ and -) if right arg heavier */ 63 EQ_UNITS_BOTH_WAYS, /* nonoriented eq units both ways */ 64 DEMOD_LINEAR, /* use linear search instead of index tree */ 65 DEMOD_OUT_IN, /* demodulate outside-in, (leftmost) */ 66 DYNAMIC_DEMOD, /* dynamic addition of demodulators */ 67 DYNAMIC_DEMOD_ALL, /* try to make all equalities into demodulators */ 68 DYNAMIC_DEMOD_LEX_DEP, /* allow lex-dep dynamic demodulators */ 69 BACK_DEMOD, /* back demodulation */ 70 ANL_EQ, /* meta-option for standard equational strategy */ 71 KNUTH_BENDIX, /* Alias for ANL_EQ */ 72 LRPO, /* lexicographic recursive path ordering */ 73 LEX_ORDER_VARS, /* consider variables when lex_checking terms */ 74 SYMBOL_ELIM, /* orient equalities to eliminate symbols */ 75 REWRITER, /* meta-option for demodulation only */ 76 77 CHECK_ARITY, /* require symbols to have fixed arities */ 78 PROLOG_STYLE_VARIABLES, /* vars start with A-Z */ 79 ECHO_INCLUDED_FILES, /* echo input from included files */ 80 SIMPLIFY_FOL, /* attempt to simplify during cnf translation */ 81 PROCESS_INPUT, /* process input usable and sos */ 82 TPTP_EQ, /* for TPTP: "equal" is the one and only equality */ 83 84 VERY_VERBOSE, /* print generated clauses */ 85 PRINT_KEPT, /* print kept clauses */ 86 PRINT_PROOFS, /* print all proofs found */ 87 BUILD_PROOF_OBJECT, /* alias to build_proof_object_1 */ 88 BUILD_PROOF_OBJECT_1, /* build proof to be checked elsewhere */ 89 BUILD_PROOF_OBJECT_2, /* build new kind of proof object */ 90 PRINT_NEW_DEMOD, /* print new demodultors */ 91 PRINT_BACK_DEMOD, /* print back demodulated clauses */ 92 PRINT_BACK_SUB, /* print back subsumed clauses */ 93 DISPLAY_TERMS, /* print terms in internal format */ 94 PRETTY_PRINT, /* Pretty print requested by Boyle */ 95 BIRD_PRINT, /* output a(_,_) terms in combinatory logic notation */ 96 97 INDEX_FOR_BACK_DEMOD, /* index (FPA) all terms for back demod */ 98 FOR_SUB_FPA, /* forward subsump with FPA, not discrim. tree */ 99 NO_FAPL, /* don't FPA index all positive literals */ 100 NO_FANL, /* don't FPA index all negative literals */ 101 102 /* misc 1 */ 103 104 CONTROL_MEMORY, /* automatically adjust max_weight */ 105 PROPOSITIONAL, /* some propositional optimizations */ 106 REALLY_DELETE_CLAUSES, /* delete back demod and back_subed cls */ 107 ATOM_WT_MAX_ARGS, /* weight of atom is max of weights of arguments */ 108 TERM_WT_MAX_ARGS, /* weight of term is max of weights of arguments */ 109 FREE_ALL_MEM, /* free all memory to avail lists at end of run */ 110 111 /*********************** Fringe ******************************/ 112 113 KEEP_HINT_SUBSUMERS, /* do not delete if it subsumes a hint */ 114 KEEP_HINT_EQUIVALENTS, /* see hint_keep_test() */ 115 PRINT_PROOF_AS_HINTS, /* constructd from proof object */ 116 DEGRADE_HINTS2, /* Bob's Hint degradation */ 117 118 INPUT_SEQUENT, /* input clauses in sequent notation */ 119 OUTPUT_SEQUENT, /* output clauses in sequent notation */ 120 SIGINT_INTERACT, /* interact on SIGINT */ 121 ANCESTOR_SUBSUME, /* ancestor subsumption */ 122 123 AUTO, /* select the current AUTO mode (see AUTO*) (sets auto1) */ 124 AUTO1, /* original AUTO mode (3.0.4) */ 125 AUTO2, /* revised AUTO mode (3.0.5) */ 126 127 GEOMETRIC_RULE, /* RP's inference rule, with unification */ 128 GEOMETRIC_REWRITE_BEFORE, /* RP's inference rule as a rewrite */ 129 GEOMETRIC_REWRITE_AFTER, /* RP's inference rule as a rewrite */ 130 GL_DEMOD, /* Delay demodulation. */ 131 132 SPLIT_CLAUSE, /* case splitting with fork */ 133 SPLIT_WHEN_GIVEN, /* Split clauses when given */ 134 SPLIT_ATOM, /* Split on atoms instead of clauses */ 135 SPLIT_POS, /* Split on positive clauses only */ 136 SPLIT_NEG, /* Split on negatvie clauses only */ 137 SPLIT_NONHORN, /* Split on negatvie clauses only */ 138 SPLIT_MIN_MAX, /* Split on clause with min max-literal */ 139 SPLIT_POPULAR, /* Split on most popular atoms */ 140 141 LINKED_UR_RES, /* linked UR resolution inference rule */ 142 LINKED_UR_TRACE, /* trace linked UR res inference rule */ 143 LINKED_SUB_UNIT_USABLE, /* use Usable list to subsume subsumable */ 144 LINKED_SUB_UNIT_SOS, /* use Sos list to subsume subsumable */ 145 LINKED_UNIT_DEL, /* use Unit Deletion during linked UR resolution. */ 146 LINKED_TARGET_ALL, /* If set, all literals are targets. */ 147 LINKED_HYPER_RES, /* Linked hyper inference rule */ 148 149 /* not documented */ 150 151 FOR_SUB_EQUIVALENTS_ONLY, /* forward subsumption iff equivalent */ 152 PROOF_WEIGHT, /* Calculate proof weight (ancestor bag). */ 153 FORMULA_HISTORY, /* Make input clauses point at formula parent */ 154 BELL, /* Ring the bell for important events? */ 155 156 DISCARD_COMMUTATIVITY_CONSEQUENCES, /* experimental */ 157 LITERALS_WEIGH_ONE, 158 HYPER_SYMMETRY_KLUDGE, /* secret flag */ 159 DISCARD_NON_ORIENTABLE_EQ, /* secret flag */ 160 DISCARD_XX_RESOLVABLE, /* secret flag */ 161 162 LOG_FOR_X_SHOW, /* log some events for X display */ 163 164 PICK_DIFF_SIM, /* selection of given clause */ 165 PICK_RANDOM_LIGHTEST, /* selection of given clause */ 166 PICK_LAST_LIGHTEST, /* selection of given clause */ 167 PICK_MID_LIGHTEST, /* selection of given clause */ 168 169 MULTI_JUST, /* for proof-shortening experiment */ 170 MULTI_JUST_LESS, /* for proof-shortening experiment */ 171 MULTI_JUST_SHORTER, /* for proof-shortening experiment */ 172 173 PROG_SYNTHESIS, /* program synthesis mode */ 174 175 CLOCKS /* detailed timing */ 176 }; 177 178 /* end of Flags */ 179 180 /************* 181 * 182 * Parms are integer valued options. To install a new parm, append 183 * a new name and index to the end of this list, then insert code to 184 * initialize it in the routine `init_options'. 185 * Example access: if (Parms[FPA_LITERALS].val == 4) { 186 * See routine `init_options' for defaults. 187 * 188 *************/ 189 190 #define MAX_PARMS 100 /* This must hold the following list! */ 191 192 enum { 193 REPORT, /* output stats and times every n seconds */ 194 195 MAX_SECONDS, /* stop search after this many seconds */ 196 MAX_GEN, /* stop search after this many generated clauses */ 197 MAX_KEPT, /* stop search after this many kept clauses */ 198 MAX_GIVEN, /* stop search after this many given clauses */ 199 MAX_LEVELS, /* with sos_queue, stop after this many levels */ 200 MAX_MEM, /* stop search after this many K bytes allocated */ 201 202 MAX_LITERALS, /* max # of lits in kept clause (0 -> no limit) */ 203 MAX_WEIGHT, /* maximum weight of kept clauses */ 204 MAX_DISTINCT_VARS, /* max # of variables in kept clause */ 205 MAX_ANSWERS, /* maximum number of answer literals */ 206 207 FPA_LITERALS, /* FPA indexing depth for literals */ 208 FPA_TERMS, /* FPA indexing depth for terms */ 209 210 PICK_GIVEN_RATIO, /* pick lightest n times, then pick first */ 211 AGE_FACTOR, /* to adjust the pick-given weight */ 212 DISTINCT_VARS_FACTOR, /* to adjust the pick-given weight */ 213 INTERRUPT_GIVEN, /* call interact after this many given cls */ 214 DEMOD_LIMIT, /* Limit on number of rewrites per clause */ 215 MAX_PROOFS, /* stop search after this many empty clauses */ 216 MIN_BIT_WIDTH, /* minimum field for bit strings */ 217 NEG_WEIGHT, /* add this value to wight of negative literals */ 218 PRETTY_PRINT_INDENT, /* indent for pretty print */ 219 STATS_LEVEL, /* higher stats_level -> output more statistics */ 220 DYNAMIC_DEMOD_DEPTH, /* deciding dynamic demoulators (ad hoc) */ 221 DYNAMIC_DEMOD_RHS, /* deciding dynamic demoulators (ad hoc) */ 222 223 FSUB_HINT_ADD_WT, /* add to pick-given wt */ 224 BSUB_HINT_ADD_WT, /* add to pick-given wt */ 225 EQUIV_HINT_ADD_WT, /* add to pick-given wt */ 226 FSUB_HINT_WT, /* pick-given wt */ 227 BSUB_HINT_WT, /* pick-given wt */ 228 EQUIV_HINT_WT, /* pick-given wt */ 229 230 /* fringe */ 231 232 CHANGE_LIMIT_AFTER, /* replace reduce_weight_limit */ 233 NEW_MAX_WEIGHT, /* replace reduce_weight_limit */ 234 235 GEO_GIVEN_RATIO, /* like pick_given_ratio, for geo children */ 236 237 DEBUG_FIRST, /* turn debugging on */ 238 DEBUG_LAST, /* turn debugging off */ 239 VERBOSE_DEMOD_SKIP, /* debugging option */ 240 241 HEAT, /* maximum heat level */ 242 DYNAMIC_HEAT_WEIGHT, /* max weigth of dynamic hot clause */ 243 244 MAX_UR_DEPTH, /* max depth for linked UR (normal depth = 0) */ 245 MAX_UR_DEDUCTION_SIZE, /* max resolutions in a single linked UR */ 246 247 SPLIT_SECONDS, /* time to search before splitting */ 248 SPLIT_GIVEN, /* given clauses before splitting */ 249 SPLIT_DEPTH, /* maximum splitting depth */ 250 251 /* not documented */ 252 253 NEW_SYMBOL_LEX_POSITION, 254 255 WARN_MEM, /* reset max_weight at this memory usage */ 256 WARN_MEM_MAX_WEIGHT, /* new max_weight */ 257 258 PICK_DIFF, /* selection of given clause */ 259 PICK_DIFF_RANGE, /* selection of given clause */ 260 261 MULTI_JUST_MAX /* for proof-shortening experiment */ 262 }; 263 264 /* end of Parms */ 265 266 /************* 267 * 268 * Statistics. To install a new statistic, append a new name and index 269 * to the end of this list, then insert the code to output it in the 270 * routine `print_stats'. 271 * Example access: Stats[INPUT_ERRORS]++; 272 * 273 *************/ 274 275 #define MAX_STATS 50 /* This must hold the following list! */ 276 277 enum { 278 INPUT_ERRORS, 279 CL_INPUT, 280 CL_GENERATED, 281 CL_KEPT, 282 CL_FOR_SUB, 283 CL_BACK_SUB, 284 CL_TAUTOLOGY, 285 CL_GIVEN, 286 CL_WT_DELETE, 287 REWRITES, 288 UNIT_DELETES, 289 EMPTY_CLAUSES, 290 FPA_OVERLOADS, /* not output if 0 */ 291 FPA_UNDERLOADS, /* not output if 0 */ 292 CL_VAR_DELETES, /* not output if 0 */ 293 FOR_SUB_SOS, 294 NEW_DEMODS, 295 CL_BACK_DEMOD, 296 LINKED_UR_DEPTH_HITS, 297 LINKED_UR_DED_HITS, 298 SOS_SIZE, 299 K_MALLOCED, 300 CL_NOT_ANC_SUBSUMED, 301 USABLE_SIZE, 302 DEMODULATORS_SIZE, 303 DEMOD_LIMITS, /* not output if 0 */ 304 INIT_WALL_SECONDS, 305 BINARY_RES_GEN, 306 HYPER_RES_GEN, 307 NEG_HYPER_RES_GEN, 308 UR_RES_GEN, 309 PARA_INTO_GEN, 310 PARA_FROM_GEN, 311 LINKED_UR_RES_GEN, 312 GEO_GEN, 313 DEMOD_INF_GEN, 314 FACTOR_GEN, 315 HOT_GENERATED, 316 HOT_KEPT, 317 FACTOR_SIMPLIFICATIONS, 318 HOT_SIZE, 319 PASSIVE_SIZE, 320 BACK_UNIT_DEL_GEN 321 }; 322 323 /* end of Stats */ 324 325 /************* 326 * 327 * Clocks. To install a new clock, append a new name and index 328 * to the end of this list, then insert the code to output it in the 329 * routine `print_times'. Example of use: CLOCK_START(INPUT_TIME), 330 * CLOCK_STOP(INPUT_TIME), micro_sec = clock_val(INPUT_TIME);. 331 * See files macros.h and clocks.c. 332 * 333 *************/ 334 335 #define MAX_CLOCKS 50 /* This must hold the following list! */ 336 337 enum { 338 INPUT_TIME, 339 CLAUSIFY_TIME, 340 PROCESS_INPUT_TIME, 341 342 BINARY_TIME, 343 HYPER_TIME, 344 NEG_HYPER_TIME, 345 UR_TIME, 346 PARA_INTO_TIME, 347 PARA_FROM_TIME, 348 LINKED_UR_TIME, 349 350 PRE_PROC_TIME, 351 RENUMBER_TIME, 352 DEMOD_TIME, 353 ORDER_EQ_TIME, 354 UNIT_DEL_TIME, 355 WEIGH_CL_TIME, 356 SORT_LITS_TIME, 357 FOR_SUB_TIME, 358 DEL_CL_TIME, 359 KEEP_CL_TIME, 360 PRINT_CL_TIME, 361 CONFLICT_TIME, 362 NEW_DEMOD_TIME, 363 364 POST_PROC_TIME, 365 BACK_DEMOD_TIME, 366 BACK_SUB_TIME, 367 FACTOR_TIME, 368 369 UN_INDEX_TIME, 370 HOT_TIME, 371 FACTOR_SIMP_TIME, 372 373 HINTS_TIME, 374 HINTS_KEEP_TIME, 375 376 BACK_UNIT_DEL_TIME, 377 PICK_GIVEN_TIME 378 }; 379 380 /* end of Clocks */ 381 382 /************* 383 * 384 * internal flags--invisible to users 385 * 386 *************/ 387 388 #define MAX_INTERNAL_FLAGS 10 /* This must hold the following list! */ 389 390 enum { 391 SPECIAL_UNARY_PRESENT, 392 DOLLAR_PRESENT, 393 LEX_VALS_SET, 394 REALLY_CHECK_ARITY, 395 FOREACH_SOS, 396 HINTS_PRESENT, 397 HINTS2_PRESENT 398 }; 399 400 /************* 401 * 402 * clause attributes 403 * 404 *************/ 405 406 /* attribute types */ 407 408 enum { 409 INT_ATTR, 410 BOOL_ATTR, 411 DOUBLE_ATTR, 412 STRING_ATTR, 413 TERM_ATTR 414 }; 415 416 /* attributes */ 417 418 #define MAX_ATTRIBUTES 20 /* This must hold the following list! */ 419 420 enum { 421 BSUB_HINT_WT_ATTR, 422 FSUB_HINT_WT_ATTR, 423 EQUIV_HINT_WT_ATTR, 424 BSUB_HINT_ADD_WT_ATTR, 425 FSUB_HINT_ADD_WT_ATTR, 426 EQUIV_HINT_ADD_WT_ATTR, 427 LABEL_ATTR 428 }; 429 430