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