src/theory/strings/sequences_stats.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Andres Noetzli, Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Statistics for the theory of strings/sequences.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__STRINGS__SEQUENCES_STATS_H
  19 #define CVC5__THEORY__STRINGS__SEQUENCES_STATS_H
  20
  21 #include "expr/kind.h"
  22 #include "theory/strings/infer_info.h"
  23 #include "theory/strings/rewrites.h"
  24 #include "util/statistics_stats.h"
  25
  26 namespace cvc5 {
  27 namespace theory {
  28 namespace strings {
  29
  30 /**
  31  * Statistics for the theory of strings.
  32  *
  33  * This is roughly broken up into the following parts:
  34  * (1) Inferences,
  35  * (2) Conflicts,
  36  * (3) Lemmas.
  37  *
  38  * "Inferences" (1) are steps invoked during solving, which either trigger:
  39  * (a) An internal update to the state of the solver (e.g. adding an inferred
  40  * equality to the equality engine),
  41  * (b) A call to OutputChannel::conflict,
  42  * (c) A call to OutputChannel::lemma.
  43  * For details, see InferenceManager. We track stats on each kind of
  44  * inference that have been indicated by the solvers in TheoryStrings.
  45  * Some kinds of inferences are further distinguished by the Kind of the node
  46  * they operate on (see d_cdSimplifications, d_reductions, d_regexpUnfoldings).
  47  *
  48  * "Conflicts" (2) arise from various kinds of reasoning, listed below,
  49  * where inferences are one of the possible methods for deriving conflicts.
  50  */
  51 class SequencesStatistics
  52 {
  53  public:
  54   SequencesStatistics();
  55   /** Number of calls to run a check where strategy is present */
  56   IntStat d_checkRuns;
  57   /** Number of calls to run the strategy */
  58   IntStat d_strategyRuns;
  59   //--------------- inferences
  60   /**
  61    * Counts the number of applications of each type of inference that were not
  62    * processed as a proof step. This is a subset of the statistics in
  63    * TheoryInferenceManager, i.e.
  64    * (theory::strings::inferences{Facts,Lemmas,Conflicts}).
  65    */
  66   HistogramStat<InferenceId> d_inferencesNoPf;
  67   /**
  68    * Counts the number of applications of each type of context-dependent
  69    * simplification. The sum of this map is equal to the number of EXTF or
  70    * EXTF_N inferences.
  71    */
  72   HistogramStat<Kind> d_cdSimplifications;
  73   /**
  74    * Counts the number of applications of each type of reduction. The sum of
  75    * this map is equal to the number of REDUCTION inferences (when
  76    * options::stringLazyPreproc is true).
  77    */
  78   HistogramStat<Kind> d_reductions;
  79   /**
  80    * Counts the number of applications of each type of regular expression
  81    * positive (resp. negative) unfoldings. The sum of this map is equal to the
  82    * number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences.
  83    */
  84   HistogramStat<Kind> d_regexpUnfoldingsPos;
  85   HistogramStat<Kind> d_regexpUnfoldingsNeg;
  86   //--------------- end of inferences
  87   /** Counts the number of applications of each type of rewrite rule */
  88   HistogramStat<Rewrite> d_rewrites;
  89   //--------------- conflicts, partition of calls to OutputChannel::conflict
  90   /** Number of equality engine conflicts */
  91   IntStat d_conflictsEqEngine;
  92   /** Number of eager conflicts */
  93   IntStat d_conflictsEager;
  94   /** Number of inference conflicts */
  95   IntStat d_conflictsInfer;
  96   //--------------- end of conflicts
  97 };
  98
  99 }
 100 }
 101 }  // namespace cvc5
 102
 103 #endif /* CVC5__THEORY__STRINGS__SEQUENCES_STATS_H */