1 /*-----------------------------------------------------------------------
2 
3 File  : che_clausesetfeatures.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   Functions for determining various features of clause sets.
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> Mon Sep 28 19:17:50 MET DST 1998
20     New
21 
22 -----------------------------------------------------------------------*/
23 
24 #ifndef CHE_CLAUSESETFEATURES
25 
26 #define CHE_CLAUSESETFEATURES
27 
28 #include <che_clausefeatures.h>
29 #include <ccl_proofstate.h>
30 
31 /*---------------------------------------------------------------------*/
32 /*                    Data type declarations                           */
33 /*---------------------------------------------------------------------*/
34 
35 typedef enum
36 {
37    SpecUnit,
38    SpecHorn,
39    SpecGeneral,
40    SpecNoEq,
41    SpecSomeEq,
42    SpecPureEq,
43    SpecFewPosNonGroundUnits,
44    SpecSomePosNonGroundUnits,
45    SpecManyPosNonGroundUnits,
46    SpecFewPosGround,
47    SpecSomePosGround,
48    SpecManyPosGround,
49    SpecFewAxioms,
50    SpecSomeAxioms,
51    SpecManyAxioms,
52    SpecFewLiterals,
53    SpecSomeLiterals,
54    SpecManyLiterals,
55    SpecSmallTerms,
56    SpecMediumTerms,
57    SpecLargeTerms,
58    SpecArity0,
59    SpecArity1,
60    SpecArity2,
61    SpecArity3Plus,
62    SpecAritySumSmall,
63    SpecAritySumMedium,
64    SpecAritySumLarge,
65    SpecDepthShallow,
66    SpecDepthMedium,
67    SpecDepthDeep,
68 }SpecFeatures;
69 
70 
71 
72 /* Limits for designating feature-based classes. They will be set in
73    SpecFeatureCells based on these values. */
74 
75 typedef struct spec_limits_cell
76 {
77    bool   ngu_absolute;
78    double ngu_few_limit;
79    double ngu_many_limit;
80    bool   gpc_absolute;
81    double gpc_few_limit;
82    double gpc_many_limit;
83    long   ax_some_limit;
84    long   ax_many_limit;
85    long   lit_some_limit;
86    long   lit_many_limit;
87    long   term_medium_limit;
88    long   term_large_limit;
89    long   far_sum_medium_limit;
90    long   far_sum_large_limit;
91    long   depth_medium_limit;
92    long   depth_deep_limit;
93    int    symbols_medium_limit;
94    int    symbols_large_limit;
95    int    predc_medium_limit;
96    int    predc_large_limit;
97    int    pred_medium_limit;
98    int    pred_large_limit;
99    int    func_medium_limit;
100    int    func_large_limit;
101    int    fun_medium_limit;
102    int    fun_large_limit;
103 }SpecLimitsCell, *SpecLimits_p;
104 
105 
106 /* Stores all the precomputed feature values (including, after a call
107    to SpecFeaturesAddEval, the classifications */
108 typedef struct spec_feature_cell
109 {
110    SpecFeatures axiomtypes;
111    SpecFeatures goaltypes;
112    SpecFeatures eq_content;
113    SpecFeatures ng_unit_content;
114    SpecFeatures ground_positive_content;
115    bool         goals_are_ground;
116    SpecFeatures set_clause_size;
117    SpecFeatures set_literal_size;
118    SpecFeatures set_termcell_size;
119    SpecFeatures max_fun_ar_class; /* Arity of _real_ function symbols,
120                0,1,2,>2 */
121    SpecFeatures avg_fun_ar_class;
122    SpecFeatures sum_fun_ar_class;
123    SpecFeatures max_depth_class;
124    long         clauses;
125    long         goals;
126    long         axioms;
127    long         literals;
128    long         term_cells;
129    long         clause_max_depth;
130    long         clause_avg_depth;
131    long         unit;
132    long         unitgoals;
133    long         unitaxioms;
134    long         horn;
135    long         horngoals;
136    long         hornaxioms;
137    long         eq_clauses;
138    long         peq_clauses;
139    long         groundunitaxioms;
140    long         positiveaxioms;
141    long         groundpositiveaxioms;
142    long         groundgoals;
143    double       ng_unit_axioms_part;
144    double       ground_positive_axioms_part;
145    int          max_fun_arity;
146    int          avg_fun_arity;
147    int          sum_fun_arity;
148    int          max_pred_arity;
149    int          avg_pred_arity;
150    int          sum_pred_arity;
151    int          fun_const_count;
152    int          fun_nonconst_count;
153    int          pred_nonconst_count;
154 }SpecFeatureCell, *SpecFeature_p;
155 
156 
157 /*---------------------------------------------------------------------*/
158 /*                Exported Functions and Variables                     */
159 /*---------------------------------------------------------------------*/
160 
161 #define NGU_ABSOLUTE           true
162 #define NGU_FEW_DEFAULT        0.25
163 #define NGU_MANY_DEFAULT       0.75
164 #define NGU_FEW_ABSDEFAULT        1
165 #define NGU_MANY_ABSDEFAULT       3
166 #define GPC_ABSOLUTE           true
167 #define GPC_FEW_DEFAULT        0.25
168 #define GPC_MANY_DEFAULT       0.75
169 #define GPC_FEW_ABSDEFAULT        1
170 #define GPC_MANY_ABSDEFAULT       3
171 #define AX_1_DEFAULT             10
172 #define AX_4_DEFAULT             15
173 #define AX_SOME_DEFAULT          20
174 #define AX_MANY_DEFAULT         100
175 #define LIT_SOME_DEFAULT         15
176 #define LIT_MANY_DEFAULT        100
177 #define TERM_MED_DEFAULT         60
178 #define TERM_LARGE_DEFAULT     1000
179 #define FAR_SUM_MED_DEFAULT      5
180 #define FAR_SUM_LARGE_DEFAULT   24
181 #define DEPTH_MEDIUM_DEFAULT     0 /* Partitioning two ways turns out
182                                       to be nearly as good as 3 way on
183                                       the test set */
184 #define DEPTH_DEEP_DEFAULT       6
185 #define SYMBOLS_MEDIUM_DEFAULT   100
186 #define SYMBOLS_LARGE_DEFAULT    1000
187 
188 #define PREDC_MEDIUM_DEFAULT     0
189 #define PREDC_LARGE_DEFAULT      2
190 #define PRED_MEDIUM_DEFAULT      1225
191 #define PRED_LARGE_DEFAULT       4000
192 #define FUNC_MEDIUM_DEFAULT      8
193 #define FUNC_LARGE_DEFAULT       110
194 #define FUN_MEDIUM_DEFAULT       360
195 #define FUN_LARGE_DEFAULT        400
196 
197 
198 
199 #define DEFAULT_OUTPUT_DESCRIPTOR "eigEIG"
200 #define DEFAULT_CLASS_MASK "aaaaaaaaaaaaa"
201 
202 
203 #define SpecLimitsCellAlloc() \
204         (SpecLimitsCell*)SizeMalloc(sizeof(SpecLimitsCell))
205 #define SpecLimitsCellFree(junk) \
206         SizeFree(junk, sizeof(SpecLimitsCell))
207 SpecLimits_p SpecLimitsAlloc(void);
208 
209 #define SpecFeatureCellAlloc() \
210         (SpecFeatureCell*)SizeMalloc(sizeof(SpecFeatureCell))
211 #define SpecFeatureCellFree(junk) \
212         SizeFree(junk, sizeof(SpecFeatureCell))
213 
214 #define Spec(spec) (true) /* For auto-generated code */
215 
216 #define SpecAxiomsAreUnit(spec) ((spec)->axioms == (spec)->unitaxioms)
217 #define SpecAxiomsAreHorn(spec) ((spec)->axioms == (spec)->hornaxioms)
218 #define SpecAxiomsAreNonUnitHorn(spec) (SpecAxiomsAreHorn(spec)&&\
219                                         !(SpecAxiomsAreUnit(spec)))
220 #define SpecAxiomsAreGeneral(spec) ((spec)->axioms >  (spec)->hornaxioms)
221 
222 #define SpecGoalsAreUnit(spec) ((spec)->goals == (spec)->unitgoals)
223 #define SpecGoalsAreHorn(spec) (!SpecGoalsAreUnit(spec))
224 #define SpecGoalsAreGround(spec) ((spec)->goals_are_ground)
225 #define SpecGoalsHaveVars(spec) (!SpecGoalsAreGround(spec))
226 
227 #define SpecPureEq(spec) ((spec)->clauses==(spec)->peq_clauses)
228 #define SpecSomeEq(spec) ((spec)->eq_clauses && !SpecPureEq(spec))
229 #define SpecNoEq(spec)   (!(spec)->eq_clauses)
230 
231 #define SpecFewNGPosUnits(spec) \
232         ((spec)->ng_unit_content == SpecFewPosNonGroundUnits)
233 #define SpecSomeNGPosUnits(spec) \
234         ((spec)->ng_unit_content == SpecSomePosNonGroundUnits)
235 #define SpecManyNGPosUnits(spec) \
236         ((spec)->ng_unit_content == SpecManyPosNonGroundUnits)
237 
238 #define SpecFewGroundPos(spec) \
239         ((spec)->ground_positive_content == SpecFewPosGround)
240 #define SpecSomeGroundPos(spec) \
241         ((spec)->ground_positive_content == SpecSomePosGround)
242 #define SpecManyGroundPos(spec) \
243         ((spec)->ground_positive_content == SpecManyPosGround)
244 
245 #define SpecFewAxioms(spec) \
246         ((spec)->set_clause_size == SpecFewAxioms)
247 #define SpecSomeAxioms(spec) \
248         ((spec)->set_clause_size == SpecSomeAxioms)
249 #define SpecManyAxioms(spec) \
250         ((spec)->set_clause_size == SpecManyAxioms)
251 
252 #define SpecFewLiterals(spec) \
253         ((spec)->set_literal_size == SpecFewLiterals)
254 #define SpecSomeLiterals(spec) \
255         ((spec)->set_literal_size == SpecSomeLiterals)
256 #define SpecManyLiterals(spec) \
257         ((spec)->set_literal_size == SpecManyLiterals)
258 
259 #define SpecSmallTerms(spec) \
260         ((spec)->set_termcell_size == SpecSmallTerms)
261 #define SpecMediumTerms(spec) \
262         ((spec)->set_termcell_size == SpecMediumTerms)
263 #define SpecLargeTerms(spec) \
264         ((spec)->set_termcell_size == SpecLargeTerms)
265 
266 #define SpecMaxFArity0(spec) \
267         ((spec)->max_fun_ar_class == SpecArity0)
268 #define SpecMaxFArity1(spec) \
269         ((spec)->max_fun_ar_class == SpecArity1)
270 #define SpecMaxFArity2(spec) \
271         ((spec)->max_fun_ar_class == SpecArity2)
272 #define SpecMaxFArity3Plus(spec) \
273         ((spec)->max_fun_ar_class ==SpecArity3Plus)
274 
275 #define SpecAvgFArity0(spec) \
276         ((spec)->avg_fun_ar_class == SpecArity0)
277 #define SpecAvgFArity1(spec) \
278         ((spec)->avg_fun_ar_class == SpecArity1)
279 #define SpecAvgFArity2(spec) \
280         ((spec)->avg_fun_ar_class == SpecArity2)
281 #define SpecAvgFArity3Plus(spec) \
282         ((spec)->avg_fun_ar_class ==SpecArity3Plus)
283 
284 #define SpecSmallFArSum(spec) \
285         ((spec)->sum_fun_ar_class == SpecAritySumSmall)
286 #define SpecMediumFArSum(spec) \
287         ((spec)->sum_fun_ar_class == SpecAritySumMedium)
288 #define SpecLargeFArSum(spec) \
289         ((spec)->sum_fun_ar_class == SpecAritySumLarge)
290 
291 #define SpecShallowMaxDepth(spec) \
292         ((spec)->max_depth_class == SpecDepthShallow)
293 #define SpecMediumMaxDepth(spec) \
294         ((spec)->max_depth_class == SpecDepthMedium)
295 #define SpecDeepMaxDepth(spec) \
296         ((spec)->max_depth_class == SpecDepthDeep)
297 
298 long    ClauseSetCountGoals(ClauseSet_p set);
299 #define ClauseSetCountAxioms(set)\
300         ((set)->members-ClauseSetCountGoals(set))
301 
302 long    ClauseSetCountUnit(ClauseSet_p set);
303 long    ClauseSetCountUnitGoals(ClauseSet_p set);
304 #define ClauseSetCountUnitAxioms(set)\
305         (ClauseSetCountUnit(set)-ClauseSetCountUnitGoals(set))
306 #define ClauseSetIsUnitSet(set) \
307         ((set)->members == ClauseSetCountUnit(set))
308 #define ClauseSetAxiomsAreUnit(set) \
309         (ClauseSetCountUnitAxioms(set) == ClauseSetCountAxioms(set))
310 #define ClauseSetGoalsAreUnit(set) \
311         (ClauseSetCountUnitGoals(set) == ClauseSetCountGoals(set))
312 
313 long    ClauseSetCountHorn(ClauseSet_p set);
314 long    ClauseSetCountHornGoals(ClauseSet_p set);
315 #define ClauseSetCountHornAxioms(set) \
316         (ClauseSetCountHorn(set)-ClauseSetCountHornGoals(set))
317 #define ClauseSetIsHornSet(set) \
318         ((set)->members == ClauseSetCountHorn(set))
319 #define ClauseSetAxiomsAreHorn(set) \
320         (ClauseSetCountHornAxioms(set) == ClauseSetCountAxioms(set))
321 #define ClauseSetGoalsAreHorn(set) \
322         (ClauseSetCountHornGoals(set) == ClauseSetCountGoals(set))
323 
324 long    ClauseSetCountEquational(ClauseSet_p set);
325 
326 /* Are all clauses equational? */
327 #define ClauseSetIsEquationalSet(set) \
328         ((set)->members == ClauseSetCountEquational(set))
329 /* Is there equality in the clause set? */
330 #define ClauseSetIsEquational(set) \
331         (ClauseSetCountEquational(set)>=1)
332 
333 long    ClauseSetCountPureEquational(ClauseSet_p set);
334 #define ClauseSetIsPureEquationalSet(set) \
335         ((set)->members == ClauseSetCountPureEquational(set))
336 
337 long    ClauseSetCountGroundGoals(ClauseSet_p set);
338 #define ClauseSetGoalsAreGround(set) \
339         (ClauseSetCountGoals(set)==ClauseSetCountGroundGoals(set))
340 
341 long    ClauseSetCountGround(ClauseSet_p set);
342 #define ClauseSetIsGround(set)\
343         (ClauseSetCountGround(set)==(set)->members)
344 
345 long    ClauseSetCountGroundPositiveAxioms(ClauseSet_p set);
346 long    ClauseSetCountPositiveAxioms(ClauseSet_p set);
347 
348 long    ClauseSetCountGroundUnitAxioms(ClauseSet_p set);
349 #define ClauseSetCountNonGroundUnitAxioms(set) \
350         (ClauseSetCountUnitAxioms(set)-ClauseSetCountGroundUnitAxioms(set))
351 long    ClauseSetCountTPTPRangeRestricted(ClauseSet_p set);
352 double  ClauseSetNonGoundAxiomPart(ClauseSet_p set);
353 
354 long    ClauseSetCollectArityInformation(ClauseSet_p set,
355                 Sig_p sig,
356                 int *max_fun_arity,
357                 int *avg_fun_arity,
358                 int *sum_fun_arity,
359                 int *max_pred_arity,
360                 int *avg_pred_arity,
361                 int *sum_pred_arity,
362                 int *non_const_funs,
363                 int *non_const_preds);
364 
365 long    ClauseSetCountMaximalTerms(ClauseSet_p set);
366 long    ClauseSetCountMaximalLiterals(ClauseSet_p set);
367 long    ClauseSetCountUnorientableLiterals(ClauseSet_p set);
368 long    ClauseSetCountEqnLiterals(ClauseSet_p set);
369 long    ClauseSetMaxStandardWeight(ClauseSet_p set);
370 
371 long    ClauseSetTermCells(ClauseSet_p set);
372 long    ClauseSetMaxLiteralNumber(ClauseSet_p set);
373 long    ClauseSetCountVariables(ClauseSet_p set);
374 long    ClauseSetCountSingletons(ClauseSet_p set);
375 long    ClauseSetTPTPDepthInfoAdd(ClauseSet_p set, long* depthmax,
376               long* depthsum, long* count);
377 void    SpecFeaturesCompute(SpecFeature_p features, ClauseSet_p set,
378              Sig_p sig);
379 void    SpecFeaturesAddEval(SpecFeature_p features, SpecLimits_p limits);
380 
381 void    SpecFeaturesPrint(FILE* out, SpecFeature_p features);
382 
383 void    SpecFeaturesParse(Scanner_p in, SpecFeature_p features);
384 
385 void    SpecTypePrint(FILE* out, SpecFeature_p features, char* mask);
386 
387 void    ClauseSetPrintPosUnits(FILE* out, ClauseSet_p set, bool
388                 printinfo);
389 void    ClauseSetPrintNegUnits(FILE* out, ClauseSet_p set, bool
390                 printinfo);
391 void    ClauseSetPrintNonUnits(FILE* out, ClauseSet_p set, bool
392                 printinfo);
393 void    ProofStatePrintSelective(FILE* out, ProofState_p state, char*
394              descriptor, bool printinfo);
395 
396 SpecLimits_p CreateDefaultSpecLimits(void);
397 
398 
399 
400 #endif
401 
402 /*---------------------------------------------------------------------*/
403 /*                        End of File                                  */
404 /*---------------------------------------------------------------------*/
405