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

Age	Commit message (Collapse)	Author
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-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-30	Adding has bound counts and tracking for rows.	Tim King

2013-04-26	FCSimplex branch merge	Tim King

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-07-07	Various fixes to documentation---typos, some incomplete documentation fixed, ↵	Morgan Deters
	\file tags corrected, copyright added to files that had it missing, etc. I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
2012-05-17	This fixes a fascinating segfault. This is the sequence of events:	Tim King
	1) A restart occurs 2) A shared term is registered to arithmetic. 3) Arithmetic sets this up. 4) No new linear relations are added to arithmetic. 5) Eventually a restart occurs. 6) Arithmetic resets the tableau as it has not had a row added since the last restart. 7) A new variable is added. 8) This exceeds the size of the column vector of the saved tableau by exactly one. 9) segfault
2012-04-27	This merges in the branch cvc4/branches/arithmetic/matrix into trunk.	Tim King
	- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau. - Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code. - No performance loss!