1 /*----------------------------------------------------------------------- 2 3 File : ccl_clauses.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Clauses - Infrastructure functions 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> Thu Apr 16 19:38:16 MET DST 1998 20 New 21 <2> Mon Jan 11 00:05:24 MET 1999 22 Added properties, proof_depth and proof_size 23 24 -----------------------------------------------------------------------*/ 25 26 #ifndef CCL_CLAUSES 27 28 #define CCL_CLAUSES 29 30 #include <ccl_neweval.h> 31 #include <ccl_eqnlist.h> 32 #include <ccl_clauseinfo.h> 33 #include <clb_properties.h> 34 35 /*---------------------------------------------------------------------*/ 36 /* Data type declarations */ 37 /*---------------------------------------------------------------------*/ 38 39 /* Properties of clauses (also used for formulas) */ 40 41 typedef enum 42 { 43 CPIgnoreProps = 0, /* For masking properties 44 * out */ 45 CPInitial = 1, /* Initial clause */ 46 CPInputFormula = 2*CPInitial, /* _Really_ initial 47 * clause/formula in TSTP 48 * sense */ 49 CPIsProcessed = 2*CPInputFormula, /* Clause has been processed 50 * previously */ 51 CPIsOriented = 2*CPIsProcessed, /* Term and literal 52 comparisons are up to 53 date */ 54 CPIsDIndexed = 2*CPIsOriented, /* Clause is in the 55 * demod_index of its set */ 56 CPIsSIndexed = 2*CPIsDIndexed, /* Clause is in the fvindex 57 * of its set */ 58 CPIsGlobalIndexed = 2*CPIsSIndexed, /* Clause is in the 59 Subterm FPIndex */ 60 CPRWDetected = 2*CPIsGlobalIndexed, /* Rewritability of the 61 clause has been 62 established. Temporary 63 property. */ 64 CPDeleteClause = 2*CPRWDetected, /* Clause should be deleted 65 * for some reason */ 66 CPType1 = 2*CPDeleteClause,/* Three bits used to encode 67 * the Clause type, taken 68 * from TPTP or TSTP input 69 * format or assumed */ 70 CPType2 = 2*CPType1, 71 CPType3 = 2*CPType2, 72 CPTypeMask = CPType1|CPType2|CPType3, 73 CPTypeUnknown = 0, /* Also used as wildcard */ 74 CPTypeAxiom = CPType1, /* Clause is Axiom */ 75 CPTypeHypothesis = CPType2, /* Clause is Hypothesis */ 76 CPTypeConjecture = CPType1|CPType2, /* Clause is Conjecture */ 77 CPTypeLemma = CPType3, /* Clause is Lemma */ 78 CPTypeNegConjecture = CPType1|CPType3, /* Clause is an negated 79 * conjecture (used for 80 * refutation) */ 81 CPTypeQuestion = CPType2|CPType3, /* `Clause is a question - 82 * only used for FOF, really. */ 83 CPTypeWatchClause = CPType1|CPType2|CPType3, 84 /* Clause is intended as a 85 * watch list clause */ 86 CPIsIRVictim = 2*CPType3, /* Clause has just been 87 simplified in 88 interreduction */ 89 CPOpFlag = 2*CPIsIRVictim, /* Temporary marker */ 90 CPIsSelected = 2*CPOpFlag, /* For analysis of selected 91 * clauses only */ 92 CPIsFinal = 2*CPIsSelected, /* Clause is a final clause, 93 i.e. a clause that 94 might be used by a 95 postprocessor. */ 96 CPIsProofClause = 2*CPIsFinal, /* Clause is part of a 97 successful proof. */ 98 CPIsSOS = 2*CPIsProofClause, /* Clause is in the set of support.*/ 99 CPNoGeneration = 2*CPIsSOS, /* No generating inferences 100 with this clause are 101 necessary */ 102 CP_CSSCPA_1 = 2*CPNoGeneration, /* CSSCPA clause sources */ 103 CP_CSSCPA_2 = 2*CP_CSSCPA_1, 104 CP_CSSCPA_4 = 2*CP_CSSCPA_2, 105 CP_CSSCPA_8 = 2*CP_CSSCPA_4, 106 CP_CSSCPA_Mask = CP_CSSCPA_1|CP_CSSCPA_2|CP_CSSCPA_4|CP_CSSCPA_8, 107 CP_CSSCPA_Unkown = 0, 108 CPIsProtected = 2*CP_CSSCPA_8, /* Unprocessed clause has 109 been used in 110 simplification and cannot 111 be deleted even if 112 parents die. */ 113 CPWatchOnly = 2*CPIsProtected, 114 CPSubsumesWatch = 2*CPWatchOnly, 115 CPLimitedRW = 2*CPSubsumesWatch, /* Clause has been processed 116 * and hence can only be 117 * rewritten in limited 118 * ways. */ 119 CPIsRelevant = 2*CPLimitedRW /* Clause is selected as 120 * relevant for a proof 121 * attempt (used by SInE). */ 122 }FormulaProperties; 123 124 125 typedef struct clause_cell 126 { 127 long ident; /* Hopefully unique ident for 128 all clauses created during 129 proof run */ 130 #ifdef CLAUSE_PERM_IDENT 131 long perm_ident; /* Running number, given on 132 alloc, never modified */ 133 #endif 134 SysDate date; /* ...at which this clause 135 became a demodulator */ 136 Eqn_p literals; /* List of literals */ 137 short neg_lit_no; /* Negative literals */ 138 short pos_lit_no; /* Positive literals */ 139 FormulaProperties properties; /* Anything we want to note at 140 the clause? */ 141 long weight; /* ClauseStandardWeight() 142 precomputed at some points in 143 the program */ 144 Eval_p evaluations; /* List of evaluations */ 145 ClauseInfo_p info; /* Currently about source in 146 input, NULL for derived clauses */ 147 PStack_p derivation; /* Derivation of the clause for 148 proof reconstruction. */ 149 long create_date; /* At what iteration of the 150 main loop has this 151 clause been created? */ 152 long proof_depth; /* How long is the longest 153 derivation chain from this 154 clause to an axiom? */ 155 long proof_size; /* How many (generating) 156 inferences were necessary to 157 create this clause? */ 158 PTree_p children; /* Which can be removed if this 159 clause changes significantly */ 160 struct clause_cell* parent1; /* Parents need to be notified */ 161 struct clause_cell* parent2; /* if their children are removed! */ 162 struct clausesetcell* set; /* Is the clause in a set? */ 163 struct clause_cell* pred; /* For clause sets = doubly */ 164 struct clause_cell* succ; /* linked lists */ 165 }ClauseCell, *Clause_p; 166 167 168 /*---------------------------------------------------------------------*/ 169 /* Exported Functions and Variables */ 170 /*---------------------------------------------------------------------*/ 171 172 extern bool ClausesHaveLocalVariables; 173 extern bool ClausesHaveDisjointVariables; 174 extern long ClauseIdentCounter; 175 176 #define ClauseSetProp(clause, prop) SetProp((clause), (prop)) 177 #define ClauseDelProp(clause, prop) DelProp((clause), (prop)) 178 #define ClauseGiveProps(clause, prop) GiveProps((clause), (prop)) 179 180 /* Are _all_ properties in prop set in clause? */ 181 #define ClauseQueryProp(clause, prop) QueryProp((clause), (prop)) 182 183 /* Are any properties in prop set in clause? */ 184 #define ClauseIsAnyPropSet(clause, prop) IsAnyPropSet((clause), (prop)) 185 186 void TSTPSkipSource(Scanner_p in); 187 188 void ClauseSetTPTPType(Clause_p clause, FormulaProperties type); 189 190 #define ClauseQueryTPTPType(clause) \ 191 ((clause)->properties&CPTypeMask) 192 193 #define TPTPTypesCombine(type1, type2)\ 194 ((type1)==CPTypeAxiom?(type2):\ 195 ((type2)==CPTypeConjecture?CPTypeConjecture:(type1))) 196 197 #define ClauseSetCSSCPASource(clause,prop)\ 198 ClauseDelProp((clause),CP_CSSCPA_Mask);\ 199 ClauseSetProp((clause),(prop*CP_CSSCPA_1)) 200 #define ClauseQueryCSSCPASource(clause)\ 201 (((clause)->properties&CP_CSSCPA_Mask)/CP_CSSCPA_1) 202 203 #define ClauseCellAllocRaw() (ClauseCell*)SizeMalloc(sizeof(ClauseCell)) 204 #define ClauseCellFree(junk) SizeFree(junk, sizeof(ClauseCell)) 205 206 #ifdef CONSTANT_MEM_ESTIMATE 207 #define CLAUSECELL_MEM 68 208 #else 209 #define CLAUSECELL_MEM (MEMSIZE(ClauseCell)+PSTACK_AVG_MEM) 210 #endif 211 212 Clause_p ClauseCellAlloc(void); 213 Clause_p EmptyClauseAlloc(void); 214 Clause_p ClauseAlloc(Eqn_p literals); 215 void ClauseFree(Clause_p junk); 216 void ClauseRecomputeLitCounts(Clause_p clause); 217 218 219 #define ClauseGCMarkTerms(clause) EqnListGCMarkTerms((clause)->literals) 220 221 #define ClauseLiteralNumber(clause)\ 222 ((clause)->pos_lit_no+(clause)->neg_lit_no) 223 224 #define ClausePropLitNumber(clause, prop)\ 225 EqnListQueryPropNumber((clause)->literals,(prop)) 226 227 #define ClauseIsEmpty(clause) (ClauseLiteralNumber(clause)==0) 228 229 bool ClauseIsSemFalse(Clause_p clause); 230 bool ClauseIsSemEmpty(Clause_p clause); 231 #define ClauseIsGoal(clause) (!((clause)->pos_lit_no)) 232 #define ClauseIsHorn(clause) ((clause)->pos_lit_no <= 1) 233 #define ClauseIsUnit(clause) (ClauseLiteralNumber(clause)==1) 234 #define ClauseIsDemodulator(clause)\ 235 (((clause)->pos_lit_no == 1) && \ 236 ((clause)->neg_lit_no == 0)) 237 #define ClauseIsRWRule(clause)\ 238 (ClauseIsDemodulator(clause)&&EqnIsOriented((clause)->literals)) 239 #define ClauseIsGround(clause) EqnListIsGround(clause->literals) 240 #define ClauseIsPositive(clause) ((clause)->neg_lit_no == 0) 241 #define ClauseIsNegative(clause) ((clause)->pos_lit_no == 0) 242 #define ClauseIsMixed(clause)\ 243 (!(ClauseIsPositive(clause)||ClauseIsNegative(clause))) 244 #define ClauseIsHypothesis(clause) (ClauseQueryTPTPType(clause)==CPTypeHypothesis) 245 #define ClauseIsConjecture(clause) \ 246 ((ClauseQueryTPTPType(clause)==CPTypeNegConjecture) ||\ 247 (ClauseQueryTPTPType(clause)==CPTypeConjecture)) 248 249 #define ClauseFindNegPureVarLit(clause) \ 250 EqnListFindNegPureVarLit((clause)->literals) 251 #define ClauseIsTrivial(clause) \ 252 EqnListIsTrivial(clause->literals) 253 254 bool ClauseHasMaxPosEqLit(Clause_p clause); 255 256 257 Clause_p ClauseSortLiterals(Clause_p clause, ComparisonFunctionType cmp_fun); 258 Clause_p ClauseCanonize(Clause_p clause); 259 #define ClauseSubsumeOrderSortLits(clause) \ 260 ClauseSortLiterals((clause), \ 261 (ComparisonFunctionType)EqnSubsumeInverseRefinedCompareRef) 262 bool ClauseIsSorted(Clause_p clause, ComparisonFunctionType cmp_fun); 263 #define ClauseIsSubsumeOrdered(clause) \ 264 ClauseIsSorted((clause), \ 265 (ComparisonFunctionType)EqnSubsumeInverseCompareRef) 266 267 long ClauseStructWeightCompare(Clause_p c1, Clause_p c2); 268 long ClauseStructWeightLexCompare(Clause_p c1, Clause_p c2); 269 #define ClauseToStack(clause) EqnListToStack((clause)->literals) 270 271 bool ClauseIsACRedundant(Clause_p clause); 272 273 #define ClauseIsEquational(clause) \ 274 EqnListIsEquational(clause->literals) 275 #define ClauseIsPureEquational(clause) \ 276 EqnListIsPureEquational(clause->literals) 277 278 #define ClauseTermSetProp(clause, prop) \ 279 EqnListTermSetProp((clause)->literals, (prop)) 280 #define ClauseTBTermDelPropCount(clause, prop) \ 281 EqnListTBTermDelPropCount((clause)->literals, (prop)) 282 #define ClauseTermDelProp(clause, prop) \ 283 EqnListTermDelProp((clause)->literals, (prop)) 284 285 #define ClauseIsSOS(clause) ClauseQueryProp((clause), CPIsSOS) 286 287 bool ClauseIsRangeRestricted(Clause_p clause); 288 bool ClauseIsAntiRangeRestricted(Clause_p clause); 289 bool ClauseIsTPTPRangeRestricted(Clause_p clause); 290 bool ClauseIsStronglyRangeRestricted(Clause_p clause); 291 EqnSide ClauseIsEqDefinition(Clause_p clause, int min_arity); 292 293 Clause_p ClauseCopy(Clause_p clause, TB_p bank); 294 Clause_p ClauseFlatCopy(Clause_p clause); 295 Clause_p ClauseCopyOpt(Clause_p clause); 296 Clause_p ClauseCopyDisjoint(Clause_p clause); 297 298 Clause_p ClauseSkolemize(Clause_p clause, TB_p bank); 299 300 void ClausePrintList(FILE* out, Clause_p clause, bool fullterms); 301 void ClausePrintAxiom(FILE* out, Clause_p clause, bool fullterms); 302 void ClausePrintRule(FILE* out, Clause_p clause, bool fullterms); 303 void ClausePrintGoal(FILE* out, Clause_p clause, bool fullterms); 304 void ClausePrintQuery(FILE* out, Clause_p clause, bool fullterms); 305 void ClausePrintTPTPFormat(FILE* out, Clause_p clause); 306 void ClausePrintLOPFormat(FILE* out, Clause_p clause, bool fullterms); 307 308 void ClausePrint(FILE* out, Clause_p clause, bool fullterms); 309 void ClausePCLPrint(FILE* out, Clause_p clause, bool fullterms); 310 void ClauseTSTPCorePrint(FILE* out, Clause_p clause, bool fullterms); 311 void ClauseTSTPPrint(FILE* out, Clause_p clause, bool fullterms, 312 bool complete); 313 314 bool ClauseStartsMaybe(Scanner_p in); 315 FormulaProperties ClauseTypeParse(Scanner_p in, char *legal_types); 316 Clause_p ClauseParse(Scanner_p in, TB_p bank); 317 Clause_p ClausePCLParse(Scanner_p in, TB_p bank); 318 319 void ClauseMarkMaximalTerms(OCB_p ocb, Clause_p clause); 320 #define ClauseCondMarkMaximalTerms(ocb, clause)\ 321 if(!ClauseQueryProp(clause, CPIsOriented))\ 322 {ClauseMarkMaximalTerms(ocb,clause);} 323 324 #define ClauseOrientLiterals(ocb, clause) \ 325 EqnListOrient((ocb), (clause)->literals) 326 #define ClauseMarkMaximalLiterals(ocb, clause) \ 327 EqnListMaximalLiterals((ocb), (clause)->literals) 328 329 #define ClauseDeleteTermProperties(clause, props) \ 330 EqnListDeleteTermProperties((clause)->literals, props) 331 332 bool ClauseParentsAreSubset(Clause_p clause1, Clause_p clause2); 333 void ClauseDetachParents(Clause_p clause); 334 void ClauseRegisterChild(Clause_p clause, Clause_p child); 335 336 void ClauseAddEvalCell(Clause_p clause, Eval_p evaluation); 337 338 void ClauseRemoveEvaluations(Clause_p clause); 339 340 double ClauseWeight(Clause_p clause, double max_term_multiplier, 341 double max_literal_multiplier, double 342 pos_multiplier, long vweight, long fweight, bool 343 count_eq_encoding); 344 345 double ClauseFunWeight(Clause_p clause, double max_term_multiplier, 346 double max_literal_multiplier, double 347 pos_multiplier, long vweight, long flimit, 348 long *fweights, long default_fweight); 349 350 double ClauseNonLinearWeight(Clause_p clause, double 351 max_term_multiplier, double 352 max_literal_multiplier, double 353 pos_multiplier, long vlweight, long 354 vweight, long fweight, bool 355 count_eq_encoding); 356 double ClauseSymTypeWeight(Clause_p clause, double 357 max_term_multiplier, double 358 max_literal_multiplier, double 359 pos_multiplier, long vweight, long 360 fweight, long cweight, long pweight); 361 362 363 double ClauseStandardWeight(Clause_p clause); 364 365 double ClauseOrientWeight(Clause_p clause, double 366 unorientable_literal_multiplier, 367 double max_literal_multiplier, double 368 pos_multiplier, long vweight, long 369 fweight, bool count_eq_encoding); 370 371 #define ClauseDepth(clause) EqnListDepth((clause)->literals) 372 373 bool ClauseNotGreaterEqual(OCB_p ocb, 374 Clause_p clause1, Clause_p clause2); 375 376 int ClauseCompareFun(const void *c1, const void* c2); 377 int ClauseCmpById(const void* clause1, const void* clause2); 378 #ifdef CLAUSE_PERM_IDENT 379 int ClauseCmpByPermId(const void* clause1, const void* clause2); 380 int ClauseCmpByPermIdR(const void* clause1, const void* clause2); 381 #endif 382 int ClauseCmpByStructWeight(const void* clause1, const void* clause2); 383 384 int ClauseCmpByPtr(const void* clause1, const void* clause2); 385 386 #define NormSubstClause(clause, subst, vars)\ 387 NormSubstEqnListExcept((clause)->literals,\ 388 NULL, (subst), (vars)) 389 390 Clause_p ClauseNormalizeVars(Clause_p clause, VarBank_p fresh_vars); 391 392 #define ClauseAddSymbolDistribution(clause, dist_array) \ 393 EqnListAddSymbolDistribution((clause)->literals, (dist_array)) 394 #define ClauseAddSymbolDistExist(clause, dist_array, exists) \ 395 EqnListAddSymbolDistExist((clause)->literals, (dist_array), (exists)) 396 397 #define ClauseAddSymbolFeatures(clause, mod_stack, feature_array)\ 398 EqnListAddSymbolFeatures((clause)->literals, (mod_stack), (feature_array)) 399 400 #define ClauseComputeFunctionRanks(clause, rank_array, count)\ 401 EqnListComputeFunctionRanks((clause)->literals, (rank_array), (count)) 402 #define ClauseCollectVariables(clause,tree)\ 403 EqnListCollectVariables((clause)->literals,(tree)) 404 405 #define ClauseAddFunOccs(clause, f_occur, res_stack) \ 406 EqnListAddFunOccs((clause)->literals, (f_occur), (res_stack)) 407 408 long ClauseCollectSubterms(Clause_p clause, PStack_p collector); 409 long ClauseReturnFCodes(Clause_p clause, PStack_p f_codes); 410 411 #define CLAUSE_ENSURE_DERIVATION(clause) \ 412 {if(!(clause)->derivation){(clause)->derivation=PStackVarAlloc(3);}} 413 414 bool ClauseIsUntyped(Clause_p clause); 415 416 #endif 417 418 /*---------------------------------------------------------------------*/ 419 /* End of File */ 420 /*---------------------------------------------------------------------*/ 421