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

Age	Commit message (Collapse)	Author
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-11-15	Adding garbage collection for Proof objects. (#1294)	Tim King

2017-07-20	Moving from the gnu extensions for hash maps to the c++11 hash maps	Tim King
	* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-07	Update copyright headers.	Mathias Preiner

2016-06-08	Support for printing a global let map in LFSC proofs.	Guy
	Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules.
2016-04-03	Updating the copyright headers and scripts.	Tim King

2015-12-24	Miscellaneous fixes	Tim King
	- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example. - Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems. - Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions. - Changing some headers to use iosfwd when possible.
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-06	* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues	Morgan Deters
	* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches.
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.)
2011-10-29	Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵	Morgan Deters
	SmtEngine::getProof(), a few other things..