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
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
|
/*-----------------------------------------------------------------------
File : che_clausesetfeatures.h
Author: Stephan Schulz
Contents
Functions for determining various features of clause sets.
Copyright 1998, 1999 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> Mon Sep 28 19:17:50 MET DST 1998
New
-----------------------------------------------------------------------*/
#ifndef CHE_CLAUSESETFEATURES
#define CHE_CLAUSESETFEATURES
#include <che_clausefeatures.h>
#include <ccl_proofstate.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef enum
{
SpecUnit,
SpecHorn,
SpecGeneral,
SpecNoEq,
SpecSomeEq,
SpecPureEq,
SpecFewPosNonGroundUnits,
SpecSomePosNonGroundUnits,
SpecManyPosNonGroundUnits,
SpecFewPosGround,
SpecSomePosGround,
SpecManyPosGround,
SpecFewAxioms,
SpecSomeAxioms,
SpecManyAxioms,
SpecFewLiterals,
SpecSomeLiterals,
SpecManyLiterals,
SpecSmallTerms,
SpecMediumTerms,
SpecLargeTerms,
SpecArity0,
SpecArity1,
SpecArity2,
SpecArity3Plus,
SpecAritySumSmall,
SpecAritySumMedium,
SpecAritySumLarge,
SpecDepthShallow,
SpecDepthMedium,
SpecDepthDeep,
}SpecFeatures;
/* Limits for designating feature-based classes. They will be set in
SpecFeatureCells based on these values. */
typedef struct spec_limits_cell
{
bool ngu_absolute;
double ngu_few_limit;
double ngu_many_limit;
bool gpc_absolute;
double gpc_few_limit;
double gpc_many_limit;
long ax_some_limit;
long ax_many_limit;
long lit_some_limit;
long lit_many_limit;
long term_medium_limit;
long term_large_limit;
long far_sum_medium_limit;
long far_sum_large_limit;
long depth_medium_limit;
long depth_deep_limit;
int symbols_medium_limit;
int symbols_large_limit;
int predc_medium_limit;
int predc_large_limit;
int pred_medium_limit;
int pred_large_limit;
int func_medium_limit;
int func_large_limit;
int fun_medium_limit;
int fun_large_limit;
}SpecLimitsCell, *SpecLimits_p;
/* Stores all the precomputed feature values (including, after a call
to SpecFeaturesAddEval, the classifications */
typedef struct spec_feature_cell
{
SpecFeatures axiomtypes;
SpecFeatures goaltypes;
SpecFeatures eq_content;
SpecFeatures ng_unit_content;
SpecFeatures ground_positive_content;
bool goals_are_ground;
SpecFeatures set_clause_size;
SpecFeatures set_literal_size;
SpecFeatures set_termcell_size;
SpecFeatures max_fun_ar_class; /* Arity of _real_ function symbols,
0,1,2,>2 */
SpecFeatures avg_fun_ar_class;
SpecFeatures sum_fun_ar_class;
SpecFeatures max_depth_class;
long clauses;
long goals;
long axioms;
long literals;
long term_cells;
long clause_max_depth;
long clause_avg_depth;
long unit;
long unitgoals;
long unitaxioms;
long horn;
long horngoals;
long hornaxioms;
long eq_clauses;
long peq_clauses;
long groundunitaxioms;
long positiveaxioms;
long groundpositiveaxioms;
long groundgoals;
double ng_unit_axioms_part;
double ground_positive_axioms_part;
int max_fun_arity;
int avg_fun_arity;
int sum_fun_arity;
int max_pred_arity;
int avg_pred_arity;
int sum_pred_arity;
int fun_const_count;
int fun_nonconst_count;
int pred_nonconst_count;
}SpecFeatureCell, *SpecFeature_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define NGU_ABSOLUTE true
#define NGU_FEW_DEFAULT 0.25
#define NGU_MANY_DEFAULT 0.75
#define NGU_FEW_ABSDEFAULT 1
#define NGU_MANY_ABSDEFAULT 3
#define GPC_ABSOLUTE true
#define GPC_FEW_DEFAULT 0.25
#define GPC_MANY_DEFAULT 0.75
#define GPC_FEW_ABSDEFAULT 1
#define GPC_MANY_ABSDEFAULT 3
#define AX_1_DEFAULT 10
#define AX_4_DEFAULT 15
#define AX_SOME_DEFAULT 20
#define AX_MANY_DEFAULT 100
#define LIT_SOME_DEFAULT 15
#define LIT_MANY_DEFAULT 100
#define TERM_MED_DEFAULT 60
#define TERM_LARGE_DEFAULT 1000
#define FAR_SUM_MED_DEFAULT 5
#define FAR_SUM_LARGE_DEFAULT 24
#define DEPTH_MEDIUM_DEFAULT 0 /* Partitioning two ways turns out
to be nearly as good as 3 way on
the test set */
#define DEPTH_DEEP_DEFAULT 6
#define SYMBOLS_MEDIUM_DEFAULT 100
#define SYMBOLS_LARGE_DEFAULT 1000
#define PREDC_MEDIUM_DEFAULT 0
#define PREDC_LARGE_DEFAULT 2
#define PRED_MEDIUM_DEFAULT 1225
#define PRED_LARGE_DEFAULT 4000
#define FUNC_MEDIUM_DEFAULT 8
#define FUNC_LARGE_DEFAULT 110
#define FUN_MEDIUM_DEFAULT 360
#define FUN_LARGE_DEFAULT 400
#define DEFAULT_OUTPUT_DESCRIPTOR "eigEIG"
#define DEFAULT_CLASS_MASK "aaaaaaaaaaaaa"
#define SpecLimitsCellAlloc() \
(SpecLimitsCell*)SizeMalloc(sizeof(SpecLimitsCell))
#define SpecLimitsCellFree(junk) \
SizeFree(junk, sizeof(SpecLimitsCell))
SpecLimits_p SpecLimitsAlloc(void);
#define SpecFeatureCellAlloc() \
(SpecFeatureCell*)SizeMalloc(sizeof(SpecFeatureCell))
#define SpecFeatureCellFree(junk) \
SizeFree(junk, sizeof(SpecFeatureCell))
#define Spec(spec) (true) /* For auto-generated code */
#define SpecIsFO(spec) (true)
#define SpecAxiomsAreUnit(spec) ((spec)->axioms == (spec)->unitaxioms)
#define SpecAxiomsAreHorn(spec) ((spec)->axioms == (spec)->hornaxioms)
#define SpecAxiomsAreNonUnitHorn(spec) (SpecAxiomsAreHorn(spec)&&\
!(SpecAxiomsAreUnit(spec)))
#define SpecAxiomsAreGeneral(spec) ((spec)->axioms > (spec)->hornaxioms)
#define SpecGoalsAreUnit(spec) ((spec)->goals == (spec)->unitgoals)
#define SpecGoalsAreHorn(spec) (!SpecGoalsAreUnit(spec))
#define SpecGoalsAreGround(spec) ((spec)->goals_are_ground)
#define SpecGoalsHaveVars(spec) (!SpecGoalsAreGround(spec))
#define SpecPureEq(spec) ((spec)->clauses==(spec)->peq_clauses)
#define SpecSomeEq(spec) ((spec)->eq_clauses && !SpecPureEq(spec))
#define SpecNoEq(spec) (!(spec)->eq_clauses)
#define SpecFewNGPosUnits(spec) \
((spec)->ng_unit_content == SpecFewPosNonGroundUnits)
#define SpecSomeNGPosUnits(spec) \
((spec)->ng_unit_content == SpecSomePosNonGroundUnits)
#define SpecManyNGPosUnits(spec) \
((spec)->ng_unit_content == SpecManyPosNonGroundUnits)
#define SpecFewGroundPos(spec) \
((spec)->ground_positive_content == SpecFewPosGround)
#define SpecSomeGroundPos(spec) \
((spec)->ground_positive_content == SpecSomePosGround)
#define SpecManyGroundPos(spec) \
((spec)->ground_positive_content == SpecManyPosGround)
#define SpecFewAxioms(spec) \
((spec)->set_clause_size == SpecFewAxioms)
#define SpecSomeAxioms(spec) \
((spec)->set_clause_size == SpecSomeAxioms)
#define SpecManyAxioms(spec) \
((spec)->set_clause_size == SpecManyAxioms)
#define SpecFewLiterals(spec) \
((spec)->set_literal_size == SpecFewLiterals)
#define SpecSomeLiterals(spec) \
((spec)->set_literal_size == SpecSomeLiterals)
#define SpecManyLiterals(spec) \
((spec)->set_literal_size == SpecManyLiterals)
#define SpecSmallTerms(spec) \
((spec)->set_termcell_size == SpecSmallTerms)
#define SpecMediumTerms(spec) \
((spec)->set_termcell_size == SpecMediumTerms)
#define SpecLargeTerms(spec) \
((spec)->set_termcell_size == SpecLargeTerms)
#define SpecMaxFArity0(spec) \
((spec)->max_fun_ar_class == SpecArity0)
#define SpecMaxFArity1(spec) \
((spec)->max_fun_ar_class == SpecArity1)
#define SpecMaxFArity2(spec) \
((spec)->max_fun_ar_class == SpecArity2)
#define SpecMaxFArity3Plus(spec) \
((spec)->max_fun_ar_class ==SpecArity3Plus)
#define SpecAvgFArity0(spec) \
((spec)->avg_fun_ar_class == SpecArity0)
#define SpecAvgFArity1(spec) \
((spec)->avg_fun_ar_class == SpecArity1)
#define SpecAvgFArity2(spec) \
((spec)->avg_fun_ar_class == SpecArity2)
#define SpecAvgFArity3Plus(spec) \
((spec)->avg_fun_ar_class ==SpecArity3Plus)
#define SpecSmallFArSum(spec) \
((spec)->sum_fun_ar_class == SpecAritySumSmall)
#define SpecMediumFArSum(spec) \
((spec)->sum_fun_ar_class == SpecAritySumMedium)
#define SpecLargeFArSum(spec) \
((spec)->sum_fun_ar_class == SpecAritySumLarge)
#define SpecShallowMaxDepth(spec) \
((spec)->max_depth_class == SpecDepthShallow)
#define SpecMediumMaxDepth(spec) \
((spec)->max_depth_class == SpecDepthMedium)
#define SpecDeepMaxDepth(spec) \
((spec)->max_depth_class == SpecDepthDeep)
long ClauseSetCountGoals(ClauseSet_p set);
#define ClauseSetCountAxioms(set)\
((set)->members-ClauseSetCountGoals(set))
long ClauseSetCountUnit(ClauseSet_p set);
long ClauseSetCountUnitGoals(ClauseSet_p set);
#define ClauseSetCountUnitAxioms(set)\
(ClauseSetCountUnit(set)-ClauseSetCountUnitGoals(set))
#define ClauseSetIsUnitSet(set) \
((set)->members == ClauseSetCountUnit(set))
#define ClauseSetAxiomsAreUnit(set) \
(ClauseSetCountUnitAxioms(set) == ClauseSetCountAxioms(set))
#define ClauseSetGoalsAreUnit(set) \
(ClauseSetCountUnitGoals(set) == ClauseSetCountGoals(set))
long ClauseSetCountHorn(ClauseSet_p set);
long ClauseSetCountHornGoals(ClauseSet_p set);
#define ClauseSetCountHornAxioms(set) \
(ClauseSetCountHorn(set)-ClauseSetCountHornGoals(set))
#define ClauseSetIsHornSet(set) \
((set)->members == ClauseSetCountHorn(set))
#define ClauseSetAxiomsAreHorn(set) \
(ClauseSetCountHornAxioms(set) == ClauseSetCountAxioms(set))
#define ClauseSetGoalsAreHorn(set) \
(ClauseSetCountHornGoals(set) == ClauseSetCountGoals(set))
long ClauseSetCountEquational(ClauseSet_p set);
/* Are all clauses equational? */
#define ClauseSetIsEquationalSet(set) \
((set)->members == ClauseSetCountEquational(set))
/* Is there equality in the clause set? */
#define ClauseSetIsEquational(set) \
(ClauseSetCountEquational(set)>=1)
long ClauseSetCountPureEquational(ClauseSet_p set);
#define ClauseSetIsPureEquationalSet(set) \
((set)->members == ClauseSetCountPureEquational(set))
long ClauseSetCountGroundGoals(ClauseSet_p set);
#define ClauseSetGoalsAreGround(set) \
(ClauseSetCountGoals(set)==ClauseSetCountGroundGoals(set))
long ClauseSetCountGround(ClauseSet_p set);
#define ClauseSetIsGround(set)\
(ClauseSetCountGround(set)==(set)->members)
long ClauseSetCountGroundPositiveAxioms(ClauseSet_p set);
long ClauseSetCountPositiveAxioms(ClauseSet_p set);
long ClauseSetCountGroundUnitAxioms(ClauseSet_p set);
#define ClauseSetCountNonGroundUnitAxioms(set) \
(ClauseSetCountUnitAxioms(set)-ClauseSetCountGroundUnitAxioms(set))
long ClauseSetCountRangeRestricted(ClauseSet_p set);
double ClauseSetNonGoundAxiomPart(ClauseSet_p set);
long ClauseSetCollectArityInformation(ClauseSet_p set,
Sig_p sig,
int *max_fun_arity,
int *avg_fun_arity,
int *sum_fun_arity,
int *max_pred_arity,
int *avg_pred_arity,
int *sum_pred_arity,
int *non_const_funs,
int *non_const_preds);
long ClauseSetCountMaximalTerms(ClauseSet_p set);
long ClauseSetCountMaximalLiterals(ClauseSet_p set);
long ClauseSetCountUnorientableLiterals(ClauseSet_p set);
long ClauseSetCountEqnLiterals(ClauseSet_p set);
long ClauseSetMaxStandardWeight(ClauseSet_p set);
long ClauseSetTermCells(ClauseSet_p set);
long ClauseSetMaxLiteralNumber(ClauseSet_p set);
long ClauseSetCountVariables(ClauseSet_p set);
long ClauseSetCountSingletons(ClauseSet_p set);
long ClauseSetTPTPDepthInfoAdd(ClauseSet_p set, long* depthmax,
long* depthsum, long* count);
void SpecFeaturesCompute(SpecFeature_p features, ClauseSet_p set,
Sig_p sig);
void SpecFeaturesAddEval(SpecFeature_p features, SpecLimits_p limits);
void SpecFeaturesPrint(FILE* out, SpecFeature_p features);
void SpecFeaturesParse(Scanner_p in, SpecFeature_p features);
void SpecTypePrint(FILE* out, SpecFeature_p features, char* mask);
void ClauseSetPrintPosUnits(FILE* out, ClauseSet_p set, bool
printinfo);
void ClauseSetPrintNegUnits(FILE* out, ClauseSet_p set, bool
printinfo);
void ClauseSetPrintNonUnits(FILE* out, ClauseSet_p set, bool
printinfo);
void ProofStatePrintSelective(FILE* out, ProofState_p state, char*
descriptor, bool printinfo);
SpecLimits_p CreateDefaultSpecLimits(void);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
