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