Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-10-11 | Rename SmtScope to SolverEngineScope. (#7284) | Aina Niemetz | |
2021-09-30 | Rename SmtEngine to SolverEngine. (#7282) | Aina Niemetz | |
2021-04-14 | Refactor / reimplement statistics (#6162) | Gereon Kremer | |
This PR refactors how we collect statistics. It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic. It also extends the C++ API to obtain and inspect the statistics. To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered. | |||
2021-04-14 | Rename public and private headers in src/include. (#6352) | Aina Niemetz | |
2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz | |
2021-04-01 | Rename namespace CVC5 to cvc5. (#6258) | Aina Niemetz | |
2021-03-31 | Rename namespace CVC4 to CVC5. (#6249) | Aina Niemetz | |
2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz | |
2020-09-22 | Update copyright header script to support CMake and Python files (#5067) | Mathias Preiner | |
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header. | |||
2020-06-16 | Update copyright headers. | Aina Niemetz | |
2019-11-08 | cmake: Disable C++ GNU extensions. (#3446) | Mathias Preiner | |
Fixes #971. | |||
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2016-04-20 | update from the master | PaulMeng | |
2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King | |
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit. - Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor. - The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit. - The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope. - Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead. - The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h. - Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added. - Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang. - Most of the really confusing ifdef's in util/statistics_registry.h are gone. |