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

Age	Commit message (Collapse)	Author
2014-12-03	Floating point infrastructure.	Martin Brain
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-11-20	Fix #lines in template.	Morgan Deters

2014-10-23	Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.	Morgan Deters
	* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
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