1 /*----------------------------------------------------------------------- 2 3 File : che_to_precgen.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Routines for generating precedences for term orderings 10 11 Copyright 1998, 1999 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 Oct 16 17:01:23 MET DST 1998 20 New 21 22 -----------------------------------------------------------------------*/ 23 24 #ifndef CHE_TO_PRECGEN 25 26 #define CHE_TO_PRECGEN 27 28 #include <che_fcode_featurearrays.h> 29 30 /*---------------------------------------------------------------------*/ 31 /* Data type declarations */ 32 /*---------------------------------------------------------------------*/ 33 34 typedef enum 35 { 36 PInvalidEntry = -1, 37 PNoMethod = 0, /* Nothing */ 38 PUnaryFirst, /* My hack ;-) */ 39 PUnaryFirstFreq, /* My new hack ;-) */ 40 PArity, /* Sort by arity */ 41 PInvArity, /* Sort by inverse arity */ 42 PConstMax, /* Sort by arity, but constants first (Default 43 for SPASS) */ 44 PInvArConstMin, /* Sort by inverse arity, but make constants 45 minimal */ 46 PByFrequency, /* Make often occuring symbols big */ 47 PByInvFrequency, /* Make often occuring symbols small */ 48 PByInvConjFrequency, /* Make often occuring symbols small, 49 * conjecture symbols large */ 50 PByInvFreqConjMax, /* Make conjecture symbols maximal, otherwise 51 use invfreq */ 52 PByInvFreqConjMin, /* Make conjecture symbols mminimal, otherwise 53 use invfreq */ 54 PByInvFreqConstMin, /* Make rarely occuring symbols small, except for 55 constants */ 56 PByInvFreqHack, /* Make constants minimal, frequent unary 57 symbols maximal, otherwise as 58 PByInvFrequency */ 59 PArrayOpt, /* Special hack for theory of array with 60 conceptually typed symbols recognized by 61 name. */ 62 POrientAxioms, /* My (planned) hack */ 63 PMinMethod = PUnaryFirst, 64 PMaxMethod = POrientAxioms 65 }TOPrecGenMethod; 66 67 68 /*---------------------------------------------------------------------*/ 69 /* Exported Functions and Variables */ 70 /*---------------------------------------------------------------------*/ 71 72 #define FREQ_SEMI_INFTY 2000000 /* Bigger than any expected frequency, 73 * small enough to never cause over- 74 * or underflow */ 75 76 extern char* TOPrecGenNames[]; 77 78 #define TOGetPrecGenName(method) (TOPrecGenNames[(method)]) 79 80 TOPrecGenMethod TOTranslatePrecGenMethod(char* name); 81 82 #define TOGenerateDefaultPrecedence(ocb,axioms) \ 83 TOGeneratePrecedence((ocb), (axioms),NULL, PUnaryFirst) 84 85 void TOGeneratePrecedence(OCB_p ocb, ClauseSet_p axioms, 86 char* predefined, TOPrecGenMethod method); 87 88 89 #endif 90 91 /*---------------------------------------------------------------------*/ 92 /* End of File */ 93 /*---------------------------------------------------------------------*/ 94 95 96 97 98 99 100