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

Age	Commit message (Collapse)	Author
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-16	Moving to static_assert now that c++11 is available.	Tim King

2017-07-07	Update copyright headers.	Mathias Preiner

2016-04-20	update from the master	PaulMeng

2014-07-01	Update copyrights.	Morgan Deters

2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

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

2013-04-01	update copyrights	Morgan Deters

2013-01-28	compiling implementation of new slicer finished; need to add debugging ↵	lianah
	information and debug.
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-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!