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

Age	Commit message (Collapse)	Author
2013-12-17	Merge branch '1.3.x'	Morgan Deters
	Conflicts: COPYING NEWS
2013-12-17	some config changes: new --bsd option, readline gives warning, default build ↵	Morgan Deters
	is now production.
2013-12-16	First attempt at incorporating LFSC proof checker into CVC4.	Morgan Deters

2013-12-10	Update NEWS.	Morgan Deters

2013-12-06	Initializing 1.3.x branch.	Morgan Deters

2013-12-05	Fix NEWS.	Morgan Deters

2013-12-05	NEWS reorganization.	Morgan Deters

2013-12-04	Don't put define-funs in model output; bug 411 testcase no longer relevant.	Morgan Deters

2013-12-03	change string news	Tianyi Liang

2013-12-02	Update NEWS file.	Morgan Deters

2013-11-27	Some versioning in advance of the 1.3 release.	Morgan Deters

2013-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2013-09-11	Theory of strings.	Tianyi Liang
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-09-09	Support per-command verbosity settings.	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-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-05-29	Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵	Morgan Deters
	unknown key.
2013-05-20	Don't allow get-model & co after a user push/pop	Morgan Deters
	This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this.
2013-05-08	Prerelease versioning for 1.2.x	Morgan Deters

2013-05-08	Cutting release 1.2.1.2	Morgan Deters

2013-04-03	Pre-release versioning	Morgan Deters

2013-04-03	Some final minor changes before cutting 1.1.	Morgan Deters
	* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-04-03	updated NEWS to include inequality solver	Liana Hadarean

2013-04-01	Merging some cleanup work:	Morgan Deters
	* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-03-22	Support for Boolean term conversion in datatypes.	Morgan Deters

2013-03-20	Interactive mode support for multiline input	Morgan Deters

2013-02-20	Single -q quiets messages/warnings. Double -qq silences sat/unsat output too.	Morgan Deters

2013-02-04	Printing commands as they're executed now requires verbosity 3+	Morgan Deters

2013-01-28	Updated NEWS for recent changes.	Morgan Deters

2013-01-23	add user patterns to the Smt1 parser; update NEWS file	Morgan Deters

2012-12-06	* tuple and record support in compatibility library	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01	Cutting release 1.0.1.0	Morgan Deters

2012-10-06	* Clean up some options documentation	Morgan Deters
	* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.)
2009-11-03	commit of project structure including autotools support	Morgan Deters