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

2018-05-29	Track input language in a single place (#2003)	Andres Noetzli

2018-02-07	Fixing more inconsistent usages of override. (#1575)	Tim King

2018-01-06	Removing throw specifiers from src/parser/. (#1486)	Tim King

2017-07-07	Update copyright headers.	Mathias Preiner

2016-04-20	update from the master	PaulMeng

2015-12-03	Removing the generated directory from the parsers.	Tim King

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

2013-03-08	Disallow overflow in bitvector literals (parser only)	Morgan Deters
	* For example, (_ bv5 1) is now an error instead of being silently truncated. * Probably inappropriate for 1.0.x because it changes exception specifications.
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-09-28	Public interface review items:	Morgan Deters
	* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument() * Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only * CheckArgument() throws non-AssertionException * things outside the core library (parsers, driver) use regular C-style assert, or a public exception type. * auto-generated documentation for Smt options and internal options Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
2012-09-27	* Rename SMT parts (printer, parser) to SMT1	Morgan Deters
	* Change --lang smt to mean SMT-LIBv2 * --lang smt1 now means SMT-LIBv1 * SMT-LIBv2 parser now gives helpful error if input looks like v1 * SMT-LIBv1 parser now gives helpful error if input looks like v2 * CVC presentation language parser now gives helpful error if input looks like either SMT-LIB v1 or v2 * Other associated changes (this commit was certified error- and warning-free by the test-and-commit script.)