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

Age	Commit message (Collapse)	Author
2013-06-15	Fix in SMT2 parser for parametric datatypes	Andrew Reynolds

2013-06-07	Allow disabling include-file feature	Morgan Deters

2013-06-04	File inclusion in Smt2 parser.	Morgan Deters
	The extended command (include-file "filename") now includes file content.
2013-05-29	Merge branch '1.2.x'	Morgan Deters

2013-05-29	Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real ↵	Morgan Deters
	division
2013-05-28	Standardize SMT-LIBv2 set of logics to use LogicInfo.	Morgan Deters
	Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics.
2013-05-21	Merge branch '1.2.x'	Morgan Deters

2013-05-21	Fix an error that valgrind found.	Morgan Deters

2013-05-20	Merge branch '1.2.x'	Morgan Deters
	Conflicts: library_versions src/parser/parser.h
2013-05-20	Detect multiply-defined :named annotations and issue an error.	Morgan Deters
	Thanks to David Cok for pointing out this issue. Conflicts: library_versions
2013-05-20	Fix parsing of SMT-LIBv2 \|quoted\| symbols that span newlines in interactive ↵	Morgan Deters
	mode. Thanks to David Cok for raising this issue.
2013-05-20	Compliance fixes for :named annotations: they must name closed subterms, the ↵	Morgan Deters
	names must be user-permitted names, etc. Thanks to David Cok for raising this issue.
2013-05-20	As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵	Morgan Deters
	takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue.
2013-05-20	Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵	Morgan Deters
	in some places Thanks to David Cok for reporting these issues.
2013-05-20	Disallow construction of (_ BitVec 0).	Morgan Deters
	Thanks to David Cok for reporting this issue.
2013-05-20	Fixed "success" response to (push N) / (pop N) with N > 1.	Morgan Deters
	Thanks to David Cok for reporting this issue.
2013-05-17	As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵	Morgan Deters
	takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue.
2013-05-17	Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵	Morgan Deters
	in some places Thanks to David Cok for reporting these issues.
2013-05-17	Disallow construction of (_ BitVec 0).	Morgan Deters
	Thanks to David Cok for reporting this issue.
2013-05-17	Fixed "success" response to (push N) / (pop N) with N > 1.	Morgan Deters
	Thanks to David Cok for reporting this issue.
2013-05-10	Update casc run script. Work on compliance for SZS output.	Andrew Reynolds

2013-04-22	add bit0 and bit1 constants to smt-lib v1 parser	Morgan Deters

2013-04-09	Change TPTP parser to not use the STRING type; this necessary to repurpose ↵	Morgan Deters
	strings for the upcoming string theory
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-25	java input stream adapters working	Morgan Deters

2013-03-21	Add the ability to "mute" commands, needed for SMT-LIB compliance.	Morgan Deters

2013-03-21	Some model and printing fixes for defined functions in input.	Morgan Deters

2013-03-20	Interactive mode support for multiline input	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-15	Merge branch '1.0.x'	Morgan Deters

2013-02-15	Fix ECHO command in CVC language parser to not output quotation marks	Morgan Deters

2013-02-08	Fix user-values in SMT-LIB v1.2	Morgan Deters

2013-01-28	Fixes for Win32 (closes bugs 488 and 489)	Morgan Deters
	* timer statistics now supported (closes bug 488) * use of --mmap doesn't crash anymore (closes bug 489)
2013-01-24	Add win32 support (merge from mdeters/win32, with some cleanup).	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

2013-01-22	update ANTLR URLs (antlr.org -> antlr3.org)	Morgan Deters

2012-12-11	Ignore unknown term annotations (giving a warning). Resolves bug 479.	Morgan Deters

2012-11-30	fix the syntax of assert-rewrite/-propagation/-reduction by putting the ↵	François Bobot
	pattern first just after the bindings Do it before the release in order to not break user files later
2012-11-28	Bug fix:	Morgan Deters
	* Fix creation of bound variables in CVC native language parser * This corrects a problem with misleading model output (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	First chunk of boolean-terms support.	Morgan Deters
	Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	Tuples and records merge. Resolves bug 270.	Morgan Deters
	Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-26	some fixes to language bindings and function visibility	Morgan Deters

2012-11-18	Disable predicate subtyping:	Morgan Deters
	* remove from public interface (ExprManager, Type) * CVC parser reports an unimplemented feature error if used I didn't want to tear it out completely (from NodeManager, TypeNode, type-checking, pre-processing, etc.) because that's a lot of hassle and we'll add it back in after the release anyway. It does mean that CVC4::Predicate is in the public interface, but that it can't be used for anything (by users). (this commit was certified error- and warning-free by the test-and-commit script.)