cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
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-09	Rename CVC4__ header guards to CVC5__. (#6326)	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-15	Replace HistogramStat by IntegralHistogramStat (#6126)	Gereon Kremer
	This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
2021-03-11	First refactoring of statistics classes (#6105)	Gereon Kremer
	This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes. It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation. Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
2021-03-09	Some more cleanup of includes (#6083)	Gereon Kremer
	This PR does some more cleanup of the includes.
2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2020-09-28	Implement bags rewriter (#5132)	mudathirmahgoub
	This PR implements rewrite rules for bags. This PR focuses on rewrite rules for non constant nodes. Rewriting nodes with constant children is delegated to bags::NormalForm class (future PR).