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

Age	Commit message (Collapse)	Author
2020-09-01	Removes old proof code (#4964)	Haniel Barbosa
	This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure. It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
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..