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

Age	Commit message (Collapse)	Author
2014-02-26	smt-lib syntax change: str.contain -> str.contains; add some prefix syntax ↵	Tianyi Liang
	for cvc format
2014-02-25	Minor code clean up in parser.	Morgan Deters

2014-02-21	add new theory (sets)	Kshitij Bansal
	Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment
2014-02-20	add negative int2str	Tianyi Liang

2014-02-20	String parsing example in CVC parser	Morgan Deters

2014-02-17	type conversion	Tianyi Liang

2014-02-11	lexer fix: disable smt-lib conversion for string literals	Tianyi Liang

2014-02-06	Minor fix for previous commit	Morgan Deters

2014-02-06	Oops.. premature push on lexer fix (remove debugging output)	Morgan Deters

2014-02-06	Fixes for escape-handling for string literals in SMT-LIBv2 lexer	Morgan Deters

2014-01-29	add prefixof, suffixof	Tianyi Liang

2014-01-09	add constant replace, indexof	Tianyi Liang

2014-01-02	Merge branch '1.3.x'	Morgan Deters

2014-01-02	Update copyright year.	Morgan Deters

2013-12-27	minor fix	Tianyi Liang

2013-12-27	Merge branch '1.3.x'	Morgan Deters

2013-12-27	Fix for ANTLR warning.	Morgan Deters

2013-12-26	new functions in strings	Tianyi Liang

2013-12-24	Better get-value parse error message for common user error.	Morgan Deters

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

2013-12-02	Minor cleanup.	Morgan Deters

2013-11-14	Allow empty record literals (fixing an oversight in previous work on empty ↵	Morgan Deters
	tuples/records)
2013-11-11	Expanded usefulness of (set-info :cvc4-logic ...)	Morgan Deters

2013-11-07	Flatten libcvc4 build structure; remove some #include interdependences	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	Fix declare-datatypes dumping bug (bug 385).	Morgan Deters

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

2013-09-09	Support empty (and 1-ary) tuples and records.	Morgan Deters

2013-09-05	Fix FLOOR and DISTINCT in CVC language parser.	Morgan Deters

2013-09-05	Fix lambda handling in CVC parser	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-29	Fix numerous compiler warnings on various platforms	Morgan Deters

2013-07-11	Remove auto-aritization from TPTP parser	Morgan Deters

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-27	Remove output.h from public space, to avoid clashes with symbols defined in ↵	Morgan Deters
	users' space. Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's not installed on users' machines, and public headers should not include it. Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-27	Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they ↵	Morgan Deters
	don't escape to user space Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
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