summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.h
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-03-09 13:44:06 -0800
committerGitHub <noreply@github.com>2021-03-09 21:44:06 +0000
commitdd92b4235e0a74b08ba02c0af11833bad27335ad (patch)
treecb97183ab43e2a1edaf91fdd6919a993486c6078 /src/api/cvc4cpp.h
parent4da1a65539d3c7481a1f4121f0e9bc09694f889d (diff)
New C++ Api: Migrate stats collection for consts, vars, terms. (#6090)
Diffstat (limited to 'src/api/cvc4cpp.h')
-rw-r--r--src/api/cvc4cpp.h8
1 files changed, 8 insertions, 0 deletions
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback