summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.h
diff options
context:
space:
mode:
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