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

Age	Commit message (Collapse)	Author
2018-02-09	Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)	Aina Niemetz

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

2017-03-02	Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵	ajreynol
	Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2016-07-26	Fix warnings in src/proof	Andres Notzli
	Fix warning due to `ProofLetCount` being defined as `struct` in `proof_utils.h` and `class` in `proof.h`. Fix warnings due to different number of arguments of `printConstantDisequalityProof()` and `printTheoryLemmaProof()` in subclasses.
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-06-01	Merge from proof branch	Guy

2016-06-01	Revert "Merging proof branch"	Guy
	This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01	Merging proof branch	Guy

2016-04-03	Updating the copyright headers and scripts.	Tim King

2016-01-26	Merged bit-vector and uf proof branch.	Liana Hadarean