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

Age	Commit message (Collapse)	Author
2019-03-26	Update copyright headers.	Aina Niemetz

2018-06-25	Updated copyright headers.	Aina Niemetz

2018-01-15	Removing more miscellaneous throw specifiers. (#1509)	Tim King
	Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places.
2017-07-07	Update copyright headers.	Mathias Preiner

2016-04-20	update from the master	PaulMeng

2014-07-01	Update copyrights.	Morgan Deters

2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

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.)
2011-09-28	variety of visibility fixes (should clean up some of the many warnings on ↵	Morgan Deters
	MacOS-production-dynamic builds)
2011-09-02	Merge from my post-smtcomp branch. Includes:	Morgan Deters
	Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-07-12	fix bug 272, array unsoundness, and some array cleanup	Morgan Deters

2011-05-05	Merge from nonclausal-simplification-v2 branch:	Morgan Deters
	* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-01-05	Commit for the theory engine and rewriter changes. Changes are substantial ↵	Dejan Jovanović
	and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.