diff options
Diffstat (limited to 'src/smt/solver_engine_stats.h')
-rw-r--r-- | src/smt/solver_engine_stats.h | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/smt/solver_engine_stats.h b/src/smt/solver_engine_stats.h new file mode 100644 index 000000000..7701f7c07 --- /dev/null +++ b/src/smt/solver_engine_stats.h @@ -0,0 +1,55 @@ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Statistics for SMT engine. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__SMT__SOLVER_ENGINE_STATS_H +#define CVC5__SMT__SOLVER_ENGINE_STATS_H + +#include "util/statistics_stats.h" + +namespace cvc5 { +namespace smt { + +struct SolverEngineStatistics +{ + SolverEngineStatistics(const std::string& name = "smt::SolverEngine::"); + /** time spent in definition-expansion */ + TimerStat d_definitionExpansionTime; + /** number of constant propagations found during nonclausal simp */ + IntStat d_numConstantProps; + /** Number of assertions before ite removal */ + IntStat d_numAssertionsPre; + /** Number of assertions after ite removal */ + IntStat d_numAssertionsPost; + /** time spent in checkModel() */ + TimerStat d_checkModelTime; + /** time spent in checkUnsatCore() */ + TimerStat d_checkUnsatCoreTime; + /** time spent in PropEngine::checkSat() */ + TimerStat d_solveTime; + /** time spent in pushing/popping */ + TimerStat d_pushPopTime; + /** time spent in processAssertions() */ + TimerStat d_processAssertionsTime; + + /** Has something simplified to false? */ + IntStat d_simplifiedToFalse; +}; /* struct SolverEngineStatistics */ + +} // namespace smt +} // namespace cvc5 + +#endif /* CVC5__SMT__SMT_ENGINE_STATS_H */ |