Move statistics from the driver into the SmtEngine (#6170)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 22 Mar 2021 21:09:55 +0000 (22:09 +0100)
committerGitHub <noreply@github.com>
Mon, 22 Mar 2021 21:09:55 +0000 (21:09 +0000)
commit442bc26b6ce093efed14bfd6764dac30bfdf918f
tree2c3452bb40116de7e9e0437c29aea654324fc7eb
parent134985065820077d2628023b9b72f78471392968
Move statistics from the driver into the SmtEngine (#6170)

This PR does some refactoring on how we handle statistics in the driver, and some minor cleanup along the way.

    The SmtEngine now has dedicated statistics for the data collected within the driver and provides utility functions to set them.
    The driver pushes the collected statistics to the SmtEngine instead of adding them itself to the statistics registry.
    The node manager no longer holds a statistics registry (that nobody used anymore anyway)
    The command executor no longer holds a pointer to the SmtEngine itself. The pointer is not necessary and seems to become stale after we call reset on the command executor (which, luckily, we don't seem to do usually)

The main motivation for this change is to make the whole statistics infrastructure private to the library and not exporting it to the outside world.
14 files changed:
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/main/command_executor.cpp
src/main/command_executor.h
src/main/driver_unified.cpp
src/main/main.cpp
src/main/main.h
src/main/signal_handlers.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/smt_engine_stats.cpp
src/smt/smt_engine_stats.h