1 2 /* 3 * File Statistics.hpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file Statistics.hpp 21 * Defines proof-search statistics 22 * 23 * @since 02/01/2008 Manchester 24 */ 25 26 #ifndef __Statistics__ 27 #define __Statistics__ 28 29 #include <ostream> 30 31 #include "Forwards.hpp" 32 33 #include "Lib/RCPtr.hpp" 34 #include "Lib/ScopedPtr.hpp" 35 36 #include "Lib/Allocator.hpp" 37 38 39 extern const char* VERSION_STRING; 40 41 namespace Kernel { 42 class Unit; 43 } 44 45 namespace Shell { 46 47 using namespace Kernel; 48 using namespace Solving; 49 50 /** 51 * Class Statistics 52 * @since 02/01/2008 Manchester 53 */ 54 class Statistics 55 { 56 public: 57 CLASS_NAME(Statistics); 58 USE_ALLOCATOR(Statistics); 59 60 Statistics(); 61 62 void print(ostream& out); 63 void explainRefutationNotFound(ostream& out); 64 65 // Input 66 /** number of input clauses */ 67 unsigned inputClauses; 68 /** number of input formulas */ 69 unsigned inputFormulas; 70 /** has types */ 71 bool hasTypes; 72 73 // Preprocessing 74 /** number of formula names introduced during preprocessing */ 75 unsigned formulaNames; 76 /** number of skolem functions (also predicates in FOOL) introduced during skolemization */ 77 unsigned skolemFunctions; 78 /** number of initial clauses */ 79 unsigned initialClauses; 80 /** number of inequality splittings performed */ 81 unsigned splitInequalities; 82 /** number of pure predicates */ 83 unsigned purePredicates; 84 /** number of trivial predicates */ 85 unsigned trivialPredicates; 86 /** number of unused predicate definitions */ 87 unsigned unusedPredicateDefinitions; 88 /** number of eliminated function definitions */ 89 unsigned functionDefinitions; 90 /** number of formulas selected by SInE selector */ 91 unsigned selectedBySine; 92 /** number of iterations before SInE reached fixpoint */ 93 unsigned sineIterations; 94 /** number of detected blocked clauses */ 95 unsigned blockedClauses; 96 97 //Generating inferences 98 /** number of clauses generated by factoring*/ 99 unsigned factoring; 100 /** number of clauses generated by binary resolution*/ 101 unsigned resolution; 102 /** number of clauses generated by unit resulting resolution*/ 103 unsigned urResolution; 104 /** number of clauses generated by constrained resolution */ 105 unsigned cResolution; 106 /** number of clauses generated by forward superposition*/ 107 unsigned forwardSuperposition; 108 /** number of clauses generated by backward superposition*/ 109 unsigned backwardSuperposition; 110 /** number of clauses generated by self superposition*/ 111 unsigned cSelfSuperposition; 112 /** number of clauses generated by forward superposition*/ 113 unsigned cForwardSuperposition; 114 /** number of clauses generated by backward superposition*/ 115 unsigned cBackwardSuperposition; 116 /** number of clauses generated by self superposition*/ 117 unsigned selfSuperposition; 118 /** number of clauses generated by equality factoring*/ 119 unsigned equalityFactoring; 120 /** number of clauses generated by equality resolution*/ 121 unsigned equalityResolution; 122 /** number of clauses generated by forward extensionality resolution*/ 123 unsigned forwardExtensionalityResolution; 124 /** number of clauses generated by backward extensionality resolution*/ 125 unsigned backwardExtensionalityResolution; 126 /** number of theory inst simp **/ 127 unsigned theoryInstSimp; 128 /** number of theoryInstSimp candidates **/ 129 unsigned theoryInstSimpCandidates; 130 /** number of theoryInstSimp tautologies **/ 131 unsigned theoryInstSimpTautologies; 132 /** number of theoryInstSimp solutions lost as we could not represent them **/ 133 unsigned theoryInstSimpLostSolution; 134 /** number of induction applications **/ 135 unsigned induction; 136 unsigned maxInductionDepth; 137 unsigned inductionInProof; 138 unsigned generalizedInduction; 139 unsigned generalizedInductionInProof; 140 141 // Simplifying inferences 142 /** number of duplicate literals deleted */ 143 unsigned duplicateLiterals; 144 /** number of literals s |= s deleted */ 145 unsigned trivialInequalities; 146 /** number of forward subsumption resolutions */ 147 unsigned forwardSubsumptionResolution; 148 /** number of backward subsumption resolutions */ 149 unsigned backwardSubsumptionResolution; 150 /** number of forward demodulations */ 151 unsigned forwardDemodulations; 152 /** number of forward demodulations into equational tautologies */ 153 unsigned forwardDemodulationsToEqTaut; 154 /** number of backward demodulations */ 155 unsigned backwardDemodulations; 156 /** number of backward demodulations into equational tautologies */ 157 unsigned backwardDemodulationsToEqTaut; 158 /** number of forward subsumption demodulations */ 159 unsigned forwardSubsumptionDemodulations; 160 /** number of forward subsumption demodulations into equational tautologies */ 161 unsigned forwardSubsumptionDemodulationsToEqTaut; 162 /** number of backward subsumption demodulations */ 163 unsigned backwardSubsumptionDemodulations; 164 /** number of backward subsumption demodulations into equational tautologies */ 165 unsigned backwardSubsumptionDemodulationsToEqTaut; 166 /** number of forward literal rewrites */ 167 unsigned forwardLiteralRewrites; 168 /** number of condensations */ 169 unsigned condensations; 170 /** number of global subsumptions */ 171 unsigned globalSubsumption; 172 /** number of evaluations */ 173 unsigned evaluations; 174 /** number of interpreted simplifications */ 175 unsigned interpretedSimplifications; 176 /** number of (proper) inner rewrites */ 177 unsigned innerRewrites; 178 /** number of inner rewrites into equational tautologies */ 179 unsigned innerRewritesToEqTaut; 180 /** number of equational tautologies discovered by CC */ 181 unsigned deepEquationalTautologies; 182 183 // Deletion inferences 184 /** number of tautologies A \/ ~A */ 185 unsigned simpleTautologies; 186 /** number of equational tautologies s=s */ 187 unsigned equationalTautologies; 188 /** number of forward subsumed clauses */ 189 unsigned forwardSubsumed; 190 /** number of backward subsumed clauses */ 191 unsigned backwardSubsumed; 192 193 /** statistics of term algebra rules */ 194 unsigned taDistinctnessSimplifications; 195 unsigned taDistinctnessTautologyDeletions; 196 unsigned taInjectivitySimplifications; 197 unsigned taNegativeInjectivitySimplifications; 198 unsigned taAcyclicityGeneratedDisequalities; 199 200 // Saturation 201 /** all clauses ever occurring in the unprocessed queue */ 202 unsigned generatedClauses; 203 /** all passive clauses */ 204 unsigned passiveClauses; 205 /** all active clauses */ 206 unsigned activeClauses; 207 /** all extensionality clauses */ 208 unsigned extensionalityClauses; 209 210 unsigned discardedNonRedundantClauses; 211 212 unsigned inferencesBlockedForOrderingAftercheck; 213 214 bool smtReturnedUnknown; 215 bool smtDidNotEvaluate; 216 217 unsigned inferencesSkippedDueToColors; 218 219 /** passive clauses at the end of the saturation algorithm run */ 220 unsigned finalPassiveClauses; 221 /** active clauses at the end of the saturation algorithm run */ 222 unsigned finalActiveClauses; 223 /** extensionality clauses at the end of the saturation algorithm run */ 224 unsigned finalExtensionalityClauses; 225 226 unsigned splitClauses; 227 unsigned splitComponents; 228 //TODO currently not set, set it? 229 unsigned uniqueComponents; 230 /** Number of clauses generated for the SAT solver */ 231 unsigned satClauses; 232 /** Number of unit clauses generated for the SAT solver */ 233 unsigned unitSatClauses; 234 /** Number of binary clauses generated for the SAT solver */ 235 unsigned binarySatClauses; 236 /** Number of clauses learned by the SAT solver */ 237 unsigned learntSatClauses; 238 /** Number of literals in clauses learned by the SAT solver */ 239 unsigned learntSatLiterals; 240 241 unsigned satSplits; 242 unsigned satSplitRefutations; 243 244 unsigned smtFallbacks; 245 246 /* the next three variables keep statistics for Vampire default sat solver*/ 247 unsigned satTWLClauseCount; 248 unsigned satTWLVariablesCount; 249 unsigned satTWLSATCalls; 250 251 unsigned instGenGeneratedClauses; 252 unsigned instGenRedundantClauses; 253 unsigned instGenKeptClauses; 254 unsigned instGenIterations; 255 256 unsigned maxBFNTModelSize; 257 258 /** Number of pure variables eliminated by SAT solver */ 259 unsigned satPureVarsEliminated; 260 261 #if GNUMP 262 /** 263 * added for the purpose of Bound propagation 264 * @since 25.10.2012 Vienna 265 * @author Ioan Dragan 266 */ 267 268 // Input 269 /** number of input constraints */ 270 unsigned inputConstraints; 271 /** number of input variables */ 272 unsigned inputVariables; 273 /** number of constraints after preprocessing */ 274 unsigned preprocessedConstraints; 275 /** number of variables after preprocessing */ 276 unsigned preprocessedVariables; 277 278 // Preprocessing 279 /** number of variables that were equivalent to some other 280 * variable and were eliminated */ 281 unsigned equivalentVariables; 282 /** number of variables eliminated by equality propagation */ 283 unsigned equalityPropagationVariables; 284 /** number of constraints affected by equality propagation */ 285 unsigned equalityPropagationConstraints; 286 /** number of eliminated constant variables */ 287 unsigned constantVariables; 288 /** number of constraints updated by constant propagation */ 289 unsigned updatedByConstantPropagation; 290 /** number of subsumed constraints */ 291 unsigned subsumedConstraints; 292 /** number of variables appearing either only positively or only 293 * negatively */ 294 unsigned halfBoundingVariables; 295 /** number of constraints deleted due to half-bounding variables */ 296 unsigned halfBoundingConstraints; 297 /** number of variables appearing either only positively or only 298 * negatively except for one constraint */ 299 unsigned almostHalfBoundingVariables; 300 /** number of constraints removed or replaced due to almost half-bounding variables */ 301 unsigned almostHalfBoundingConstraints; 302 /** number of variables that were eliminated by Fourier-Motzkin because the 303 * elimination introduced allowed amount of clauses */ 304 unsigned fmRemovedVariables; 305 /** number of constraints introduced by Fourier-Motzkin variable elimination 306 * in preprocessing */ 307 unsigned preprocessingFMIntroduced; 308 /** number of constraints removed by Fourier-Motzkin variable elimination 309 * in preprocessing */ 310 unsigned preprocessingFMRemoved; 311 312 // Solving 313 /** number of decision points where the variable was picked by heuristics */ 314 unsigned freeDecisionPoints; 315 /** number of decision points where the variable was predetermined */ 316 unsigned forcedDecisionPoints; 317 /** maximal number of decision points at a moment*/ 318 DecisionLevel maxDecisionDepth; 319 /** number of backtracks */ 320 unsigned backtracks; 321 /** number of backtracks by more than one decision level */ 322 unsigned longBacktracks; 323 /** number of propagated bounds */ 324 unsigned propagatedBounds; 325 /** number of generated conflict clauses */ 326 unsigned conflictClauses; 327 /** how many times the conservative assigment selector reused previous assignment */ 328 unsigned assignmentsReusedByConservative; 329 /** number of selected conflict that were not the most recent conflicts available */ 330 unsigned nonRecentConflicts; 331 /** number of collapsing clauses that we retained for bound propagation */ 332 unsigned retainedConstraints; 333 334 //Number representation 335 /** True if native numbers were used during computation */ 336 bool nativeUsed; 337 /** True if precise numbers were used during computation */ 338 bool preciseUsed; 339 /** Time (in ms) when we switched from native to precise numbers */ 340 unsigned switchToPreciseTimeInMs; 341 342 /** refutation if @c terminationReason==REFUTATION */ 343 ConstraintRCPtr bpRefutation; 344 /** satisfying assignment if @c terminationReason==SATISFIABLE */ 345 ScopedPtr<Assignment> satisfyingAssigment; 346 347 #endif //GNUMP 348 349 /** termination reason */ 350 enum TerminationReason { 351 /** refutation found */ 352 REFUTATION, 353 /** SAT SATISFIABLE */ 354 SAT_SATISFIABLE, 355 /** satisfiability detected (saturated set built) */ 356 SATISFIABLE, 357 /** sat solver Unsatisfiable */ 358 SAT_UNSATISFIABLE, 359 /** saturation terminated but an incomplete strategy was used */ 360 REFUTATION_NOT_FOUND, 361 /** inappropriate strategy **/ 362 INAPPROPRIATE, 363 /** unknown termination reason */ 364 UNKNOWN, 365 /** time limit reached */ 366 TIME_LIMIT, 367 /** memory limit reached */ 368 MEMORY_LIMIT, 369 /** activation limit reached */ 370 ACTIVATION_LIMIT 371 }; 372 /** termination reason */ 373 TerminationReason terminationReason; 374 /** refutation, if any */ 375 Kernel::Unit* refutation; 376 /** the saturated set of clauses, if any */ 377 Kernel::UnitList* saturatedSet; 378 /** if problem is satisfiable and we obtained a model, contains its 379 * representation; otherwise it is an empty string */ 380 vstring model; 381 382 enum ExecutionPhase { 383 /** Whatever happens before we start parsing the problem */ 384 INITIALIZATION, 385 PARSING, 386 /** Scanning for properties to be passed to preprocessing */ 387 PROPERTY_SCANNING, 388 NORMALIZATION, 389 SINE_SELECTION, 390 INCLUDING_THEORY_AXIOMS, 391 PREPROCESS_1, 392 PREDIACTE_DEFINITION_MERGING, 393 PREDICATE_DEFINITION_INLINING, 394 UNUSED_PREDICATE_DEFINITION_REMOVAL, 395 BLOCKED_CLAUSE_ELIMINATION, 396 PREPROCESS_2, 397 NEW_CNF, 398 NAMING, 399 PREPROCESS_3, 400 CLAUSIFICATION, 401 FUNCTION_DEFINITION_ELIMINATION, 402 INEQUALITY_SPLITTING, 403 EQUALITY_RESOLUTION_WITH_DELETION, 404 EQUALITY_PROXY, 405 GENERAL_SPLITTING, 406 SATURATION, 407 /** The actual run of the conflict resolution algorithm */ 408 SOLVING, 409 /** The actual run of the SAT solver*/ 410 SAT_SOLVING, 411 PREPROCESSING, 412 /** Whatever happens after the saturation algorithm finishes */ 413 FINALIZATION, 414 FMB_PREPROCESSING, 415 FMB_CONSTRAINT_GEN, 416 FMB_SOLVING, 417 UNKNOWN_PHASE 418 }; 419 420 ExecutionPhase phase; 421 422 private: 423 static const char* phaseToString(ExecutionPhase p); 424 }; // class Statistics 425 426 } 427 428 #endif 429