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