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

Age	Commit message (Collapse)	Author
2013-12-02	Minor cleanup.	Morgan Deters

2013-11-11	Expanded usefulness of (set-info :cvc4-logic ...)	Morgan Deters

2013-10-20	adds regular expression range	Tianyi Liang

2013-10-01	adds partial function substr. the use of this function should be guarded, ↵	Tianyi Liang
	especially for disequalities
2013-10-01	Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535	Andrew Reynolds

2013-09-27	removes unsound cases, adds unrolling	Tianyi Liang

2013-09-27	for morgan to see the regression problems	Tianyi Liang

2013-09-18	Support for bv2nat/int2bv in parser and BV rewriter.	Morgan Deters

2013-09-13	Documentation fixes, some code typo fixes, file perms, other minor things.	Morgan Deters

2013-09-11	Theory of strings.	Tianyi Liang
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-09-09	Add support for check-sat with argument.	Morgan Deters

2013-09-09	Support per-command verbosity settings.	Morgan Deters

2013-09-05	Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a ↵	Morgan Deters
	segfault in smt2 printer
2013-07-11	Support for TPTP's TFF0 (with arithmetic)	Morgan Deters
	This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
2013-07-05	Fix for a datatype parsing bug that Tim found.	Morgan Deters

2013-06-27	Fix minor warnings found by recent clang/gcc.	Morgan Deters

2013-06-24	Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵	Morgan Deters
	allows linearization of div,mod,/ by a constant.
2013-06-19	Fix to the "include" extended feature of the SMT-LIB parser	Morgan Deters

2013-06-19	Give a more useful parse error message for "undeclared variable -1".	Morgan Deters
	Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small change to the parser to detect when something like "-1" is used but undeclared, and adds a note to the error message giving the syntax for unary minus.
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	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-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-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-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-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
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-08	added support for parametric datatypes in smt2 parser, includes support for ↵	Andrew Reynolds
	'as' qualifier
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-10-10	Abstract values for SMT-LIB.	Morgan Deters
	Also fix bug 421 relating to incrementality and models. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09	* make Model class private (as discussed at meeting today)	Morgan Deters
	* fix minor issue with s-expr parsing in CVC and SMT grammars * other minor things (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-08	fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't ↵	Morgan Deters
	allow use of any BV ops
2012-10-06	* Fix some regressions' expected outputs.	Morgan Deters
	* Ensure Rewriter::init() is called before ::rewrite(). The array type enumerator recently gave us an end-run around ::init(). TheoryEngine no longer calls these, they're done via static initialization. * Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412). (this commit was certified error- and warning-free by the test-and-commit script.)