From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Mar 2021 21:44:06 +0000 (-0800)
Subject: New C++ Api: Migrate stats collection for consts, vars, terms. (#6090)
X-Git-Tag: cvc5-1.0.0~2125
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd92b4235e0a74b08ba02c0af11833bad27335ad;p=cvc5.git

New C++ Api: Migrate stats collection for consts, vars, terms. (#6090)
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0ce3ee058..2af24c89b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -59,11 +59,27 @@
 #include "theory/theory_model.h"
 #include "util/random.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 #include "util/utility.h"
 
 namespace CVC4 {
 namespace api {
 
+/* -------------------------------------------------------------------------- */
+/* Statistics                                                                 */
+/* -------------------------------------------------------------------------- */
+
+struct Statistics
+{
+  Statistics()
+      : d_consts("api::CONSTANT"), d_vars("api::VARIABLE"), d_terms("api::TERM")
+  {
+  }
+  IntegralHistogramStat<TypeConstant> d_consts;
+  IntegralHistogramStat<TypeConstant> d_vars;
+  IntegralHistogramStat<Kind> d_terms;
+};
+
 /* -------------------------------------------------------------------------- */
 /* Kind                                                                       */
 /* -------------------------------------------------------------------------- */
@@ -3255,6 +3271,12 @@ Solver::Solver(Options* opts)
   d_smtEngine->setSolver(this);
   Options& o = d_smtEngine->getOptions();
   d_rng.reset(new Random(o[options::seed]));
+#if CVC4_STATISTICS_ON
+  d_stats.reset(new Statistics());
+  d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_consts);
+  d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_vars);
+  d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_terms);
+#endif
 }
 
 Solver::~Solver() {}
@@ -3264,6 +3286,31 @@ Solver::~Solver() {}
 
 NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); }
 
+void Solver::increment_term_stats(Kind kind) const
+{
+#ifdef CVC4_STATISTICS_ON
+  d_stats->d_terms << kind;
+#endif
+}
+
+void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const
+{
+#ifdef CVC4_STATISTICS_ON
+  const TypeNode tn = sort.getTypeNode();
+  TypeConstant tc = tn.getKind() == CVC4::kind::TYPE_CONSTANT
+                        ? tn.getConst<TypeConstant>()
+                        : LAST_TYPE;
+  if (is_var)
+  {
+    d_stats->d_vars << tc;
+  }
+  else
+  {
+    d_stats->d_consts << tc;
+  }
+#endif
+}
+
 /* Split out to avoid nested API calls (problematic with API tracing).        */
 /* .......................................................................... */
 
@@ -3387,6 +3434,7 @@ Term Solver::mkTermFromKind(Kind kind) const
     res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI);
   }
   (void)res.getType(true); /* kick off type checking */
+  increment_term_stats(kind);
   return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -3485,6 +3533,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
   }
 
   (void)res.getType(true); /* kick off type checking */
+  increment_term_stats(kind);
   return Term(this, res);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4410,6 +4459,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
 
   Node res = d_nodeMgr->mkVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
+  increment_vars_consts_stats(sort, false);
   return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4424,6 +4474,7 @@ Term Solver::mkConst(Sort sort) const
 
   Node res = d_nodeMgr->mkVar(*sort.d_type);
   (void)res.getType(true); /* kick off type checking */
+  increment_vars_consts_stats(sort, false);
   return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4442,6 +4493,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
   Node res = symbol.empty() ? d_nodeMgr->mkBoundVar(*sort.d_type)
                             : d_nodeMgr->mkBoundVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
+  increment_vars_consts_stats(sort, true);
   return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 3d26f5c7b..43f79b480 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -74,6 +74,7 @@ class Result;
 namespace api {
 
 class Solver;
+struct Statistics;
 
 /* -------------------------------------------------------------------------- */
 /* Exception                                                                  */
@@ -3626,12 +3627,19 @@ class CVC4_PUBLIC Solver
   /** Check whether string s is a valid decimal integer. */
   bool isValidInteger(const std::string& s) const;
 
+  /** Increment the term stats counter. */
+  void increment_term_stats(Kind kind) const;
+  /** Increment the vars stats (if 'is_var') or consts stats counter. */
+  void increment_vars_consts_stats(const Sort& sort, bool is_var) const;
+
   /** The node manager of this solver. */
   std::unique_ptr<NodeManager> d_nodeMgr;
   /** The SMT engine of this solver. */
   std::unique_ptr<SmtEngine> d_smtEngine;
   /** The random number generator of this solver. */
   std::unique_ptr<Random> d_rng;
+  /** The statistics collected on the Api level. */
+  std::unique_ptr<Statistics> d_stats;
 };
 
 }  // namespace api