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

Age	Commit message (Collapse)	Author
2014-04-29	Fix for --force-logic to extend its reach to the parser.	Morgan Deters

2014-04-10	Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵	Andrew Reynolds
	Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
2014-01-02	Update copyright year.	Morgan Deters

2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-09-11	Theory of strings.	Tianyi Liang
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-04-22	add bit0 and bit1 constants to smt-lib v1 parser	Morgan Deters

2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2013-03-26	Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac	Morgan Deters

2013-03-19	Minor fixes to build system	Morgan Deters

2013-03-14	Merge branch '1.0.x'	Morgan Deters

2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
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.
2013-02-16	Some cleanup and copyright updating	Morgan Deters
	* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-08	Fix user-values in SMT-LIB v1.2	Morgan Deters

2013-01-23	fix to workaround ANTLR 3.2 issue with initialization	Morgan Deters

2013-01-23	add user patterns to the Smt1 parser; update NEWS file	Morgan Deters

2012-10-22	fix parser generation in distributed tarballs (should fix bug #427)	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-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.)