1 /*----------------------------------------------------------------------- 2 3 File : che_to_weightgen.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Routines for generating weights 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 Sep 25 02:49:11 MET DST 1998 20 New 21 22 -----------------------------------------------------------------------*/ 23 24 #ifndef CHE_TO_WEIGHTGEN 25 26 #define CHE_TO_WEIGHTGEN 27 28 29 #include <che_fcode_featurearrays.h> 30 31 32 33 /*---------------------------------------------------------------------*/ 34 /* Data type declarations */ 35 /*---------------------------------------------------------------------*/ 36 37 typedef enum 38 { 39 WInvalidEntry = -1, 40 WNoMethod = 0, /* Nothing */ 41 WSelectMaximal, /* First maximal symbol in precedence gets 42 weight 0 */ 43 WArityWeight, /* Weight(f) = Arity(f)+1 */ 44 WArityMax0, /* Weight(f) = Arity(f)+1, 0 for first max*/ 45 WModArityWeight, /* Weight(f) = Arity(f)+W_TO_BASEWEIGHT */ 46 WModArityMax0, /* Weight(f) = Arity(f)+W_TO_BASEWEIGHT, 0 47 for first max*/ 48 WAritySqWeight, /* Weight(f) = Arity(f)^2+1) */ 49 WAritySqMax0, /* Weight(f) = Arity(f)^2+1), 0 for first 50 max */ 51 WInvArityWeight, /* Weight(f) = Maxarity+1-Arity(f) */ 52 WInvArityMax0, /* Weight(f) = Maxarity+1-Arity(f), 0 for 53 first max */ 54 WInvAritySqWeight, /* Weight(f) = Maxarity^2+1-Arity(f)^2 */ 55 WInvAritySqMax0, /* Weight(f) = Maxarity^2+1-Arity(f)^2, 0 56 for first max */ 57 WPrecedence, /* Weight(f) = |{g|g<f}| */ 58 WPrecedenceInv, /* Weight(f) = |{g|g>f}| */ 59 WPrecRank5, /* */ 60 WPrecRank10, /* */ 61 WPrecRank20, /* */ 62 WFrequency, /* Weight(f) = |Axioms|_f */ 63 WInvFrequency, /* Weight(f) = Maxfreq+1-|Axioms|_f */ 64 WFrequencyRank, /* Weight(f) = Rank in frequency-induced 65 quasi-ordering */ 66 WInvFrequencyRank, /* Weight(f) = Inverse rank in 67 frequency-induced * quasi-ordering */ 68 WInvConjFrequencyRank, /* Weight(f) = Inverse rank in 69 conjecture-frequency-induced 70 quasi-ordering */ 71 WFrequencyRankSq, /* As above, but squared */ 72 WInvFrequencyRankSq, /* Ditto */ 73 WInvModFreqRank, /* As WInvFrequencyRank, but difference 74 between ranks is cardinality of set of 75 symbols in rank */ 76 WInvModFreqRankMax0, /* As above, but first maximal unary is 0 */ 77 WConstantWeight, /* All weights 1 */ 78 WMinMethod = WSelectMaximal, 79 WMaxMethod = WConstantWeight /* Update as required! */ 80 }TOWeightGenMethod; 81 82 /* Think about goal-directedness, prefer symbols occuring in the goal */ 83 84 #define WConstNoSpecialWeight -1 85 #define WConstNoWeight 0 86 87 88 /* Used as base weight for ModArity */ 89 #define W_TO_BASEWEIGHT 4 90 91 92 /*---------------------------------------------------------------------*/ 93 /* Exported Functions and Variables */ 94 /*---------------------------------------------------------------------*/ 95 96 97 extern char* TOWeightGenNames[]; 98 99 #define TOGetWeightGenName(method) \ 100 (TOWeightGenNames[(method)]) 101 102 TOWeightGenMethod TOTranslateWeightGenMethod(char* name); 103 104 #define TOGenerateDefaultWeights(ocb) \ 105 TOGenerateWeights((ocb), NULL, WSelectMaximal, \ 106 W_DEFAULT_WEIGHT) 107 108 void TOGenerateWeights(OCB_p ocb, ClauseSet_p axioms, char *pre_weights, 109 TOWeightGenMethod method, long const_weight); 110 111 112 113 #endif 114 115 /*---------------------------------------------------------------------*/ 116 /* End of File */ 117 /*---------------------------------------------------------------------*/ 118 119 120 121 122 123 124