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

Age	Commit message (Collapse)	Author
2018-06-25	Updated copyright headers.	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-04-20	update from the master	PaulMeng

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

2015-11-09	Replacing an inefficient use of std::find(...) to use std::set's find() instead.	Tim King

2014-08-04	Some fixes to symmetry breaker (resolves bug 576).	Morgan Deters

2014-07-01	Update copyrights.	Morgan Deters

2013-05-21	Fix incremental bug in symmetry breaker.	Morgan Deters
	Thanks to Christoph Sticksel for reporting this.
2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

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-08-03	fix uses of getMetaKind() from outside the expr package. (they now use ↵	Morgan Deters
	isConst() and isVar() as appropriate) also some base infrastructure for the new ::isConst().
2012-06-11	Merge from quantifiers2-trunkmerge branch.	Morgan Deters
	Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.
2011-09-16	final(?) documentation fixes	Morgan Deters

2011-09-16	fix up more documentation	Morgan Deters

2011-09-16	fix numerous documentation issues; doxygen complains much less, now	Morgan Deters

2011-07-11	merge from symmetry branch	Morgan Deters