1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
/*-----------------------------------------------------------------------
File : che_varweights.h
Author: Stephan Schulz, schulz@eprover.org
Contents
Weight functions that play around a bit ;-)
Copyright 1998, 1999, 2005 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details..
Run "eprover -h" for contact information.
Changes
<1> Wed Jun 17 00:11:03 MET DST 1998
New
-----------------------------------------------------------------------*/
#ifndef CHE_VARWEIGHTS
#define CHE_VARWEIGHTS
#include <che_refinedweight.h>
#include <che_clausesetfeatures.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct varweightparamcell
{
OCB_p ocb;
double max_term_multiplier;
double max_literal_multiplier;
double pos_multiplier;
double conjecture_multiplier;
double hypothesis_multiplier;
double sig_size_multiplier;
double proof_size_multiplier;
double proof_depth_multiplier;
double term_weight_multiplier;
double term_depth_multiplier;
double weight_multiplier;
double app_var_mult;
long vlweight;
long vweight;
long fweight;
long nvweight;
long nfweight;
long cweight;
long pweight;
long stagger_limit;
}VarWeightParamCell, *VarWeightParam_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define VarWeightParamCellAlloc() (VarWeightParamCell*) \
SizeMalloc(sizeof(VarWeightParamCell))
#define VarWeightParamCellFree(junk) \
SizeFree(junk, sizeof(VarWeightParamCell))
WFCB_p TPTPTypeWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, OCB_p ocb, double
max_term_multiplier, double
max_literal_multiplier, double
pos_multiplier, double
conjecture_multiplier, double
hypothesis_multiplier, double app_var_mult);
WFCB_p TPTPTypeWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double TPTPTypeWeightCompute(void* data, Clause_p clause);
WFCB_p SigWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, OCB_p ocb, double
max_term_multiplier, double
max_literal_multiplier, double
pos_multiplier, double sig_size_multiplier,
double app_var_mult);
WFCB_p SigWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double SigWeightCompute(void* data, Clause_p clause);
WFCB_p ProofWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, OCB_p ocb, double
max_term_multiplier, double
max_literal_multiplier, double
pos_multiplier, double
proof_size_multiplier, double
proof_depth_multiplier, double
app_var_mult);
WFCB_p ProofWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double ProofWeightCompute(void* data, Clause_p clause);
WFCB_p DepthWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, OCB_p ocb, double
max_term_multiplier, double
max_literal_multiplier, double
pos_multiplier, double term_weight_multiplier,
double app_var_mult);
WFCB_p DepthWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double DepthWeightCompute(void* data, Clause_p clause);
WFCB_p WeightLessDepthInit(ClausePrioFun prio_fun, int fweight,
int vweight, OCB_p ocb, double
max_term_multiplier, double
max_literal_multiplier, double
pos_multiplier, double depth_weight_multiplier,
double app_var_mult);
WFCB_p WeightLessDepthParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double WeightLessDepthCompute(void* data, Clause_p clause);
WFCB_p NLWeightInit(ClausePrioFun prio_fun, int fweight,
int vlweight, int vweight, OCB_p ocb, double
max_term_multiplier, double
max_literal_multiplier, double
pos_multiplier, double app_var_mult);
WFCB_p NLWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double NLWeightCompute(void* data, Clause_p clause);
WFCB_p PNRefinedWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, int nfweight, int nvweight,
OCB_p ocb, double max_term_multiplier,
double max_literal_multiplier, double
pos_multiplier, double app_var_mult);
WFCB_p PNRefinedWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double PNRefinedWeightCompute(void* data, Clause_p clause);
WFCB_p SymTypeWeightInit(ClausePrioFun prio_fun, int fweight,
int vweight, int cweight, int pweight, OCB_p
ocb, double max_term_multiplier, double
max_literal_multiplier, double
pos_multiplier, double app_var_mult);
WFCB_p SymTypeWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double SymTypeWeightCompute(void* data, Clause_p clause);
WFCB_p ClauseWeightAgeInit(ClausePrioFun prio_fun, int fweight, int
vweight, double pos_multiplier,
double weight_multiplier, double app_var_mult);
WFCB_p ClauseWeightAgeParse(Scanner_p in, OCB_p ocb, ProofState_p state);
double ClauseWeightAgeCompute(void* data, Clause_p clause);
WFCB_p StaggeredWeightInit(ClausePrioFun prio_fun,
double stagger_factor, ClauseSet_p axioms);
WFCB_p StaggeredWeightParse(Scanner_p in, OCB_p ocb, ProofState_p
state);
double StaggeredWeightCompute(void* data, Clause_p clause);
void VarWeightExit(void* data);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
