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

Age	Commit message (Collapse)	Author
2014-09-30	Proofs- and cores-related segfault fixes (mainly a usability issue), thanks ↵	Morgan Deters
	Christoph Sticksel for reporting these.
2014-07-12	Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵	Morgan Deters
	for the report.
2014-07-01	Update copyrights.	Morgan Deters

2014-06-28	Automatically make SMT options from command-line option names, warn when not ↵	Morgan Deters
	possible.
2014-06-25	Fix some #line annotations.	Morgan Deters

2014-06-22	Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:	Morgan Deters
	1. no decimals used for rational literals 2. queries/check-sats wrapped with PUSH/POP
2014-06-21	Minor fixes for man pages.	Morgan Deters

2014-06-19	More doc fixes; fixes some lintian warnings.	Morgan Deters

2014-06-18	Proper escaping in option documentation.	Morgan Deters

2014-06-18	Options script fix.	Morgan Deters

2014-06-16	More application-track fixes for use with trace executor.	Morgan Deters

2014-06-15	Careful there aren't too many "success" messages with ↵	Morgan Deters
	--tear-down-incremental (can confuse trace runner).
2014-06-09	Add missing set of braces, fixes --trace.	Morgan Deters
	Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.
2014-06-06	-{d,t} help => --show-{debug,trace}-tags	Kshitij Bansal

2014-06-06	option to hide stats which are zero (off by default), also some aliases	Kshitij Bansal

2014-05-16	minor improvements (fixes) to did-you-mean suggestions	Kshitij Bansal

2014-04-29	Mostly resolves bug #561 memory leaks, and more.	Morgan Deters

2014-04-29	fixed couple of more warnings	Kshitij Bansal

2014-04-19	Eh, what?	Kshitij Bansal

2014-04-09	Minor change to better support parameterized partial/total kinds (for ↵	Morgan Deters
	upcoming datatypes work).
2014-03-11	Fix for rewriterules build breakage.	Morgan Deters

2014-02-27	--stats-every-query option: print increment in addition to cumulative value ↵	Kshitij Bansal
	of each stat the increment is printed in parantheses at the end, e.g. sat::decisions, 100 (50)
2014-02-25	New translation work, support Z3-str-style string constraints.	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-01-02	Merge branch '1.3.x'	Morgan Deters

2014-01-02	Update copyright year.	Morgan Deters

2013-12-23	Proof-checking code; fixups of segfaults and missing functionality in proof ↵	Morgan Deters
	generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but not --check-proofs, since LFSC code uses globals) * proofs are not yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-11-29	Fix proofs build.	Morgan Deters

2013-11-11	Some fixes to build system with dependency-tracking is off; should fix ↵	Morgan Deters
	RPM/Debian builds.
2013-09-11	Theory of strings.	Tianyi Liang
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-08-13	--segv-nospin is now default.	Morgan Deters

2013-07-29	Fix numerous compiler warnings on various platforms	Morgan Deters

2013-07-24	Fixes for building with mingw win64.	Morgan Deters

2013-07-24	Don't allow --stats if not a statistics-enabled build	Morgan Deters

2013-07-23	Some fixes for (get-info :all-options)	Morgan Deters

2013-07-23	fix for win32 option parsing via mingw32	Morgan Deters

2013-07-23	(get-info :all-options) to get option values; also command-line option ↵	Morgan Deters
	suggestions
2013-06-06	IDL example theory (to be used with --use-theory=idl).	Dejan Jovanović

2013-05-17	A couple of fixes to the get-option command for compliance with SMT-LIB.	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-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-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-01-25	Fix errors and reduce warnings on clang (merge from mdeters/clang)	Morgan Deters

2013-01-19	Fix an options-processing bug on some platforms (e.g., MacOS).	Morgan Deters

2012-11-30	renaming --smtlib to --smtlib-strict; removing --smtlib2 option	Morgan Deters

2012-11-30	Adding smtname level options for tlimit, rlimit, etc. Fix to the internal ↵	Tim King
	documentation in base_options.
2012-10-26	build options sources into distribution tarballs (in the same way that antlr ↵	Morgan Deters
	grammars are pre-generated for tarballs). this speeds up user builds by not requiring them to run the mkoptions script (unless they change an options meta-file). i've tested this, but let me know if there are any problems you encounter.
2012-10-24	Includes many fixes to build system for Solaris (thanks Tim!), and also	Morgan Deters
	just in general, and some documentation adjustments.