Branch data Line data Source code
1 : : /****************************************************************************** 2 : : * This file is part of the cvc5 project. 3 : : * 4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS 5 : : * in the top-level source directory and their institutional affiliations. 6 : : * All rights reserved. See the file COPYING in the top-level source 7 : : * directory for licensing information. 8 : : * **************************************************************************** 9 : : * 10 : : * Implementation of statistics for SMT engine. 11 : : */ 12 : : 13 : : #include "smt/solver_engine_stats.h" 14 : : 15 : : namespace cvc5::internal { 16 : : namespace smt { 17 : : 18 : 75664 : SolverEngineStatistics::SolverEngineStatistics(StatisticsRegistry& sr, 19 : 75664 : const std::string& name) 20 : : : d_definitionExpansionTime( 21 : 75664 : sr.registerTimer(name + "definitionExpansionTime")), 22 : 75664 : d_numConstantProps(sr.registerInt(name + "numConstantProps")), 23 : 75664 : d_numAssertionsPre(sr.registerInt(name + "numAssertionsPreITERemoval")), 24 : 75664 : d_numAssertionsPost(sr.registerInt(name + "numAssertionsPostITERemoval")), 25 : 75664 : d_checkModelTime(sr.registerTimer(name + "checkModelTime")), 26 : 75664 : d_checkUnsatCoreTime(sr.registerTimer(name + "checkUnsatCoreTime")), 27 : 75664 : d_solveTime(sr.registerTimer(name + "solveTime")), 28 : 75664 : d_pushPopTime(sr.registerTimer(name + "pushPopTime")), 29 : 75664 : d_processAssertionsTime(sr.registerTimer(name + "processAssertionsTime")), 30 : 75664 : d_simplifiedToFalse(sr.registerInt(name + "simplifiedToFalse")) 31 : : { 32 : 75664 : } 33 : : 34 : : } // namespace smt 35 : : } // namespace cvc5::internal