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