1
2 /*
3 * File Statistics.cpp.
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.cpp
21 * Implements proof-search statistics
22 *
23 * @since 02/01/2008 Manchester
24 */
25
26 #include <iostream>
27
28 #include "Debug/RuntimeStatistics.hpp"
29
30 #include "Lib/Allocator.hpp"
31 #include "Lib/Environment.hpp"
32 #include "Lib/TimeCounter.hpp"
33 #include "Lib/Timer.hpp"
34
35 #include "Shell/UIHelper.hpp"
36
37 #include "Saturation/SaturationAlgorithm.hpp"
38
39 #if GNUMP
40 #include "Kernel/Assignment.hpp"
41 #include "Kernel/Constraint.hpp"
42 #endif
43
44 #include "Options.hpp"
45 #include "Statistics.hpp"
46
47
48 using namespace Lib;
49 using namespace Saturation;
50 using namespace Shell;
51
52 /**
53 * Initialise statistics.
54 * @since 02/01/2008 Manchester
55 */
Statistics()56 Statistics::Statistics()
57 : inputClauses(0),
58 inputFormulas(0),
59 hasTypes(false),
60 formulaNames(0),
61 initialClauses(0),
62 splitInequalities(0),
63 purePredicates(0),
64 trivialPredicates(0),
65 unusedPredicateDefinitions(0),
66 functionDefinitions(0),
67 selectedBySine(0),
68 sineIterations(0),
69 factoring(0),
70 resolution(0),
71 urResolution(0),
72 cResolution(0),
73 forwardSuperposition(0),
74 backwardSuperposition(0),
75 cSelfSuperposition(0),
76 cForwardSuperposition(0),
77 cBackwardSuperposition(0),
78 selfSuperposition(0),
79 equalityFactoring(0),
80 equalityResolution(0),
81 forwardExtensionalityResolution(0),
82 backwardExtensionalityResolution(0),
83 theoryInstSimp(0),
84 theoryInstSimpCandidates(0),
85 theoryInstSimpTautologies(0),
86 theoryInstSimpLostSolution(0),
87 induction(0),
88 maxInductionDepth(0),
89 inductionInProof(0),
90 generalizedInduction(0),
91 generalizedInductionInProof(0),
92 duplicateLiterals(0),
93 trivialInequalities(0),
94 forwardSubsumptionResolution(0),
95 backwardSubsumptionResolution(0),
96 forwardDemodulations(0),
97 forwardDemodulationsToEqTaut(0),
98 backwardDemodulations(0),
99 backwardDemodulationsToEqTaut(0),
100 forwardSubsumptionDemodulations(0),
101 forwardSubsumptionDemodulationsToEqTaut(0),
102 backwardSubsumptionDemodulations(0),
103 backwardSubsumptionDemodulationsToEqTaut(0),
104 forwardLiteralRewrites(0),
105 condensations(0),
106 globalSubsumption(0),
107 evaluations(0),
108 interpretedSimplifications(0),
109 innerRewrites(0),
110 innerRewritesToEqTaut(0),
111 deepEquationalTautologies(0),
112 simpleTautologies(0),
113 equationalTautologies(0),
114 forwardSubsumed(0),
115 backwardSubsumed(0),
116 taDistinctnessSimplifications(0),
117 taDistinctnessTautologyDeletions(0),
118 taInjectivitySimplifications(0),
119 taNegativeInjectivitySimplifications(0),
120 taAcyclicityGeneratedDisequalities(0),
121 generatedClauses(0),
122 passiveClauses(0),
123 activeClauses(0),
124 extensionalityClauses(0),
125 discardedNonRedundantClauses(0),
126 inferencesBlockedForOrderingAftercheck(0),
127 smtReturnedUnknown(false),
128 smtDidNotEvaluate(false),
129 inferencesSkippedDueToColors(0),
130 finalPassiveClauses(0),
131 finalActiveClauses(0),
132 finalExtensionalityClauses(0),
133 splitClauses(0),
134 splitComponents(0),
135 uniqueComponents(0),
136 satClauses(0),
137 unitSatClauses(0),
138 binarySatClauses(0),
139 learntSatClauses(0),
140 learntSatLiterals(0),
141
142 satSplits(0),
143 satSplitRefutations(0),
144
145 smtFallbacks(0),
146
147 /**TODO Remove the next var*/
148 satTWLClauseCount(0),
149 satTWLVariablesCount(0),
150 satTWLSATCalls(0),
151
152 instGenGeneratedClauses(0),
153 instGenRedundantClauses(0),
154 instGenKeptClauses(0),
155 instGenIterations(0),
156
157 maxBFNTModelSize(0),
158
159 satPureVarsEliminated(0),
160 terminationReason(UNKNOWN),
161 refutation(0),
162 saturatedSet(0),
163 phase(INITIALIZATION)
164 {
165 } // Statistics::Statistics
166
explainRefutationNotFound(ostream & out)167 void Statistics::explainRefutationNotFound(ostream& out)
168 {
169 // should be a one-liner for each case!
170 if (discardedNonRedundantClauses) {
171 out << "Refutation not found, non-redundant clauses discarded";
172 }
173 else if (inferencesSkippedDueToColors) {
174 out << "Refutation not found, inferences skipped due to colors\n";
175 }
176 else if(smtReturnedUnknown){
177 out << "Refutation not found, SMT solver inside AVATAR returned Unknown";
178 }
179 else if (smtDidNotEvaluate) {
180 out << "Refutation not found, SMT solver inside AVATAR failed to evaluate a literal\n";
181 }
182 else {
183 out << "Refutation not found, incomplete strategy";
184 }
185 }
186
print(ostream & out)187 void Statistics::print(ostream& out)
188 {
189 if (env.options->statistics()==Options::Statistics::NONE) {
190 return;
191 }
192
193 SaturationAlgorithm::tryUpdateFinalClauseCount();
194
195 bool separable=false;
196 #define HEADING(text,num) if (num) { addCommentSignForSZS(out); out << ">>> " << (text) << endl;}
197 #define COND_OUT(text, num) if (num) { addCommentSignForSZS(out); out << (text) << ": " << (num) << endl; separable = true; }
198 #define SEPARATOR if (separable) { addCommentSignForSZS(out); out << endl; separable = false; }
199
200 addCommentSignForSZS(out);
201 out << "------------------------------\n";
202 addCommentSignForSZS(out);
203 out << "Version: " << VERSION_STRING << endl;
204
205 addCommentSignForSZS(out);
206 out << "Termination reason: ";
207 switch(terminationReason) {
208 case Statistics::REFUTATION:
209 out << "Refutation";
210 break;
211 case Statistics::TIME_LIMIT:
212 out << "Time limit";
213 break;
214 case Statistics::MEMORY_LIMIT:
215 out << "Memory limit";
216 break;
217 case Statistics::ACTIVATION_LIMIT:
218 out << "Activation limit";
219 break;
220 case Statistics::REFUTATION_NOT_FOUND:
221 explainRefutationNotFound(out);
222 break;
223 case Statistics::SATISFIABLE:
224 out << "Satisfiable";
225 break;
226 case Statistics::SAT_SATISFIABLE:
227 out << "SAT Satisfiable";
228 break;
229 case Statistics::SAT_UNSATISFIABLE:
230 out << "SAT Unsatisfiable";
231 break;
232 case Statistics::UNKNOWN:
233 out << "Unknown";
234 break;
235 case Statistics::INAPPROPRIATE:
236 out << "Inappropriate";
237 break;
238 default:
239 ASSERTION_VIOLATION;
240 }
241 out << endl;
242 if (phase!=FINALIZATION) {
243 addCommentSignForSZS(out);
244 out << "Termination phase: " << phaseToString(phase) << endl;
245 }
246 out << endl;
247
248 if (env.options->statistics()==Options::Statistics::FULL) {
249
250 HEADING("Input",inputClauses+inputFormulas);
251 COND_OUT("Input clauses", inputClauses);
252 COND_OUT("Input formulas", inputFormulas);
253
254 HEADING("Preprocessing",formulaNames+purePredicates+trivialPredicates+
255 unusedPredicateDefinitions+functionDefinitions+selectedBySine+
256 sineIterations+splitInequalities);
257 COND_OUT("Introduced names",formulaNames);
258 COND_OUT("Introduced skolems",skolemFunctions);
259 COND_OUT("Pure predicates", purePredicates);
260 COND_OUT("Trivial predicates", trivialPredicates);
261 COND_OUT("Unused predicate definitions", unusedPredicateDefinitions);
262 COND_OUT("Function definitions", functionDefinitions);
263 COND_OUT("Selected by SInE selection", selectedBySine);
264 COND_OUT("SInE iterations", sineIterations);
265 COND_OUT("Split inequalities", splitInequalities);
266 SEPARATOR;
267
268 HEADING("Saturation",activeClauses+passiveClauses+extensionalityClauses+
269 generatedClauses+finalActiveClauses+finalPassiveClauses+finalExtensionalityClauses+
270 discardedNonRedundantClauses+inferencesSkippedDueToColors+inferencesBlockedForOrderingAftercheck);
271 COND_OUT("Initial clauses", initialClauses);
272 COND_OUT("Generated clauses", generatedClauses);
273 COND_OUT("Active clauses", activeClauses);
274 COND_OUT("Passive clauses", passiveClauses);
275 COND_OUT("Extensionality clauses", extensionalityClauses);
276 COND_OUT("Blocked clauses", blockedClauses);
277 COND_OUT("Final active clauses", finalActiveClauses);
278 COND_OUT("Final passive clauses", finalPassiveClauses);
279 COND_OUT("Final extensionality clauses", finalExtensionalityClauses);
280 COND_OUT("Discarded non-redundant clauses", discardedNonRedundantClauses);
281 COND_OUT("Inferences skipped due to colors", inferencesSkippedDueToColors);
282 COND_OUT("Inferences blocked due to ordering aftercheck", inferencesBlockedForOrderingAftercheck);
283 SEPARATOR;
284
285
286 HEADING("Simplifying Inferences",duplicateLiterals+trivialInequalities+
287 forwardSubsumptionResolution+backwardSubsumptionResolution+
288 forwardDemodulations+backwardDemodulations+forwardLiteralRewrites+
289 forwardSubsumptionDemodulations+backwardSubsumptionDemodulations+
290 condensations+globalSubsumption+evaluations+innerRewrites);
291 COND_OUT("Duplicate literals", duplicateLiterals);
292 COND_OUT("Trivial inequalities", trivialInequalities);
293 COND_OUT("Fw subsumption resolutions", forwardSubsumptionResolution);
294 COND_OUT("Bw subsumption resolutions", backwardSubsumptionResolution);
295 COND_OUT("Fw demodulations", forwardDemodulations);
296 COND_OUT("Bw demodulations", backwardDemodulations);
297 COND_OUT("Fw subsumption demodulations", forwardSubsumptionDemodulations);
298 COND_OUT("Bw subsumption demodulations", backwardSubsumptionDemodulations);
299 COND_OUT("Fw literal rewrites", forwardLiteralRewrites);
300 COND_OUT("Inner rewrites", innerRewrites);
301 COND_OUT("Condensations", condensations);
302 COND_OUT("Global subsumptions", globalSubsumption);
303 COND_OUT("Evaluations", evaluations);
304 //COND_OUT("Interpreted simplifications", interpretedSimplifications);
305 SEPARATOR;
306
307 HEADING("Deletion Inferences",simpleTautologies+equationalTautologies+
308 forwardSubsumed+backwardSubsumed+forwardDemodulationsToEqTaut+
309 forwardSubsumptionDemodulationsToEqTaut+backwardSubsumptionDemodulationsToEqTaut+
310 backwardDemodulationsToEqTaut+innerRewritesToEqTaut);
311 COND_OUT("Simple tautologies", simpleTautologies);
312 COND_OUT("Equational tautologies", equationalTautologies);
313 COND_OUT("Deep equational tautologies", deepEquationalTautologies);
314 COND_OUT("Forward subsumptions", forwardSubsumed);
315 COND_OUT("Backward subsumptions", backwardSubsumed);
316 COND_OUT("Fw demodulations to eq. taut.", forwardDemodulationsToEqTaut);
317 COND_OUT("Bw demodulations to eq. taut.", backwardDemodulationsToEqTaut);
318 COND_OUT("Fw subsumption demodulations to eq. taut.", forwardSubsumptionDemodulationsToEqTaut);
319 COND_OUT("Bw subsumption demodulations to eq. taut.", backwardSubsumptionDemodulationsToEqTaut);
320 COND_OUT("Inner rewrites to eq. taut.", innerRewritesToEqTaut);
321 SEPARATOR;
322
323 HEADING("Generating Inferences",resolution+urResolution+cResolution+factoring+
324 forwardSuperposition+backwardSuperposition+selfSuperposition+
325 cForwardSuperposition+cBackwardSuperposition+cSelfSuperposition+
326 equalityFactoring+equalityResolution+forwardExtensionalityResolution+
327 backwardExtensionalityResolution+
328 theoryInstSimp+theoryInstSimpCandidates+theoryInstSimpTautologies+theoryInstSimpLostSolution+induction);
329 COND_OUT("Binary resolution", resolution);
330 COND_OUT("Unit resulting resolution", urResolution);
331 COND_OUT("Binary resolution with abstraction",cResolution);
332 COND_OUT("Factoring", factoring);
333 COND_OUT("Forward superposition", forwardSuperposition);
334 COND_OUT("Backward superposition", backwardSuperposition);
335 COND_OUT("Self superposition", selfSuperposition);
336 COND_OUT("Forward superposition with abstraction", cForwardSuperposition);
337 COND_OUT("Backward superposition with abstraction", cBackwardSuperposition);
338 COND_OUT("Self superposition with abstraction", cSelfSuperposition);
339 COND_OUT("Equality factoring", equalityFactoring);
340 COND_OUT("Equality resolution", equalityResolution);
341 COND_OUT("Fw extensionality resolution", forwardExtensionalityResolution);
342 COND_OUT("Bw extensionality resolution", backwardExtensionalityResolution);
343 COND_OUT("TheoryInstSimp",theoryInstSimp);
344 COND_OUT("TheoryInstSimpCandidates",theoryInstSimpCandidates);
345 COND_OUT("TheoryInstSimpTautologies",theoryInstSimpTautologies);
346 COND_OUT("TheoryInstSimpLostSolution",theoryInstSimpLostSolution);
347 COND_OUT("Induction",induction);
348 COND_OUT("MaxInductionDepth",maxInductionDepth);
349 COND_OUT("InductionStepsInProof",inductionInProof);
350 COND_OUT("GeneralizedInduction",generalizedInduction);
351 COND_OUT("GeneralizedInductionInProof",generalizedInductionInProof);
352 SEPARATOR;
353
354 HEADING("Term algebra simplifications",taDistinctnessSimplifications+
355 taDistinctnessTautologyDeletions+taInjectivitySimplifications+
356 taAcyclicityGeneratedDisequalities+taNegativeInjectivitySimplifications);
357 COND_OUT("Distinctness simplifications",taDistinctnessSimplifications);
358 COND_OUT("Distinctness tautology deletions",taDistinctnessTautologyDeletions);
359 COND_OUT("Injectivity simplifications",taInjectivitySimplifications);
360 COND_OUT("Negative injectivity simplifications",taNegativeInjectivitySimplifications);
361 COND_OUT("Disequalities generated from acyclicity",taAcyclicityGeneratedDisequalities);
362
363 HEADING("AVATAR",splitClauses+splitComponents+uniqueComponents+satSplits+
364 satSplitRefutations);
365 COND_OUT("Split clauses", splitClauses);
366 COND_OUT("Split components", splitComponents);
367 COND_OUT("Unique components", uniqueComponents);
368 //COND_OUT("Sat splits", satSplits); // same as split clauses
369 COND_OUT("Sat splitting refutations", satSplitRefutations);
370 COND_OUT("SMT fallbacks",smtFallbacks);
371 SEPARATOR;
372
373 HEADING("Instance Generation",instGenGeneratedClauses+instGenRedundantClauses+
374 instGenKeptClauses+instGenIterations);
375 COND_OUT("InstGen generated clauses", instGenGeneratedClauses);
376 COND_OUT("InstGen redundant clauses", instGenRedundantClauses);
377 COND_OUT("InstGen kept clauses", instGenKeptClauses);
378 COND_OUT("InstGen iterations", instGenIterations);
379 SEPARATOR;
380
381 //TODO record statistics for FMB
382 HEADING("Model Building",maxBFNTModelSize);
383 COND_OUT("Max BFNT model size", maxBFNTModelSize);
384 SEPARATOR;
385
386
387 //TODO record statistics for MiniSAT
388 HEADING("SAT Solver Statistics",satTWLClauseCount+satTWLVariablesCount+
389 satTWLSATCalls+satClauses+unitSatClauses+binarySatClauses+
390 learntSatClauses+learntSatLiterals+satPureVarsEliminated);
391 COND_OUT("SAT solver clauses", satClauses);
392 COND_OUT("SAT solver unit clauses", unitSatClauses);
393 COND_OUT("SAT solver binary clauses", binarySatClauses);
394 COND_OUT("TWL SAT solver learnt clauses", learntSatClauses);
395 COND_OUT("TWL SAT solver learnt literals", learntSatLiterals);
396 COND_OUT("TWLsolver clauses", satTWLClauseCount);
397 COND_OUT("TWLsolver variables", satTWLVariablesCount);
398 COND_OUT("TWLsolver calls for satisfiability", satTWLSATCalls);
399 COND_OUT("Pure propositional variables eliminated by SAT solver", satPureVarsEliminated);
400 SEPARATOR;
401
402 }
403
404 COND_OUT("Memory used [KB]", Allocator::getUsedMemory()/1024);
405
406 addCommentSignForSZS(out);
407 out << "Time elapsed: ";
408 Timer::printMSString(out,env.timer->elapsedMilliseconds());
409 out << endl;
410 addCommentSignForSZS(out);
411 out << "------------------------------\n";
412
413 RSTAT_PRINT(out);
414 addCommentSignForSZS(out);
415 out << "------------------------------\n";
416
417 #undef SEPARATOR
418 #undef COND_OUT
419
420 if (env.options && env.options->timeStatistics()) {
421 TimeCounter::printReport(out);
422 }
423 }
424
phaseToString(ExecutionPhase p)425 const char* Statistics::phaseToString(ExecutionPhase p)
426 {
427 switch(p) {
428 case INITIALIZATION:
429 return "Initialization";
430 case PARSING:
431 return "Parsing";
432 case PROPERTY_SCANNING:
433 return "Property scanning";
434 case NORMALIZATION:
435 return "Normalization";
436 case SINE_SELECTION:
437 return "SInE selection";
438 case INCLUDING_THEORY_AXIOMS:
439 return "Including theory axioms";
440 case PREPROCESS_1:
441 return "Preprocessing 1";
442 case PREDIACTE_DEFINITION_MERGING:
443 return "Predicate definition merging";
444 case PREDICATE_DEFINITION_INLINING:
445 return "Predicate definition inlining";
446 case UNUSED_PREDICATE_DEFINITION_REMOVAL:
447 return "Unused predicate definition removal";
448 case BLOCKED_CLAUSE_ELIMINATION:
449 return "Blocked clause elimination";
450 case PREPROCESS_2:
451 return "Preprocessing 2";
452 case NEW_CNF:
453 return "NewCNF";
454 case NAMING:
455 return "Naming";
456 case PREPROCESS_3:
457 return "Preprocessing 3";
458 case CLAUSIFICATION:
459 return "Clausification";
460 case FUNCTION_DEFINITION_ELIMINATION:
461 return "Function definition elimination";
462 case INEQUALITY_SPLITTING:
463 return "Inequality splitting";
464 case EQUALITY_RESOLUTION_WITH_DELETION:
465 return "Equality resolution with deletion";
466 case EQUALITY_PROXY:
467 return "Equality proxy";
468 case GENERAL_SPLITTING:
469 return "General splitting";
470 case SATURATION:
471 return "Saturation";
472 case FINALIZATION:
473 return "Finalization";
474 case UNKNOWN_PHASE:
475 return "Unknown";
476 case PREPROCESSING:
477 return "BP Preprocessing ";
478 case SOLVING:
479 return "Solving with Conflict Resolution";
480 case SAT_SOLVING:
481 return "SAT Solving";
482 case FMB_PREPROCESSING:
483 return "Finite model building preprocessing";
484 case FMB_CONSTRAINT_GEN:
485 return "Finite model building constraint generation";
486 case FMB_SOLVING:
487 return "Finite model building SAT solving";
488 default:
489 ASSERTION_VIOLATION;
490 return "Invalid ExecutionPhase value";
491 }
492 }
493