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	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-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-04-24	Do not use __ prefix for header guards. (#2974)	Mathias Preiner
	Fixes 2887.
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

2014-07-01	Update copyrights.	Morgan Deters

2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2012-12-05	Improved garbage collection for TheoryArith. The merges all of the code ↵	Tim King
	over from branches/arithmetic/converge except for the new code for simplex.
2012-10-11	Standardizing copyright notice. Touches ALL sources, guys, sorry.. it's	Morgan Deters
	just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-03-02	This commit merges in the changes from branches/arithmetic/refactor0	Tim King
	- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work. - Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver. - Fix to an assertion in CDQueue. - Implements a CDArithVarSet using a vector of booleans and CDList. - Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.
2012-03-02	CDMap -> CDHashMap	Dejan Jovanović
	CDSet -> CDHashSet
2011-09-02	Partial merge of integers work; this is simple B&B and some pseudoboolean	Morgan Deters
	infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-04-18	This commit merges the branch arithmetic/propagation-again into trunk.	Tim King
	- This adds code for bounds refinement, and conflict weakening. - This adds util/boolean_simplification.h. - This adds a propagation manager to theory of arithmetic. - Propagation is disabled by default. - Propagation can be enabled by the command line flag "--enable-arithmetic-propagation" - Propagation interacts heavily with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.