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

Age	Commit message (Collapse)	Author
2014-04-06	fix for hiding prompt/header in shell, error-behavior options as in SMTLIB	Kshitij Bansal

2014-04-04	Allow turning off the interactive prompt while in interactive mode.	Morgan Deters

2014-03-26	Merge branch '1.3.x'	Morgan Deters
	Conflicts: src/theory/arith/normal_form.cpp
2014-03-26	Win32 build script fixes (to allow portfolio builds).	Morgan Deters

2014-03-19	Set dumping options from (set-option..) and API more directly.	Morgan Deters

2014-03-19	Move the translator binary from src/main to examples, no longer built by ↵	Morgan Deters
	default.
2014-03-11	Merge branch '1.3.x'	Morgan Deters

2014-03-11	Fix for portfolio.	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	option to print stats after every satisfiability or validity query	Kshitij Bansal

2014-02-20	portfolio: add stat to track time spent waiting for interrupted threads to stop	Kshitij Bansal

2013-12-24	Merge branch '1.3.x'	Morgan Deters
	Conflicts: NEWS
2013-12-24	Minor code cleanup.	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-12-22	Fix to interactive mode determination.	Morgan Deters

2013-12-22	Fix option specification.	Morgan Deters

2013-12-17	some config changes: new --bsd option, readline gives warning, default build ↵	Morgan Deters
	is now production.
2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-11-29	Fix portfolio compile error.	Morgan Deters

2013-11-27	Incremental is now on by default when using from API, off for command-line ↵	Morgan Deters
	driver except in interactive mode.
2013-11-12	Minor portfolio fixes for some platforms.	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-12	fix bug 534: portfolio define-fun duplicate model	Kshitij Bansal

2013-09-09	Fix portfolio on bug411.smt2. (get-model command should only go to last winner)	Morgan Deters

2013-08-13	--segv-nospin is now default.	Morgan Deters

2013-07-24	some portfolio driver cleanup	Morgan Deters

2013-07-13	Fix language bindings and portfolio builds.	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-28	Fix portfolio builds after yesterday's commits.	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-05-17	Add support for --dump-models option, in preparation for casc.	Andrew Reynolds

2013-05-17	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-04-26	FCSimplex branch merge	Tim King

2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

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-26	Make --incremental the default when running interactively	Morgan Deters

2013-03-25	finish removal of separateOutput	Kshitij Bansal

2013-03-23	Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.	Morgan Deters

2013-03-20	Better reporting of detached git state in --version and --show-config	Morgan Deters

2013-03-20	Interactive mode support for multiline input	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-20	Single -q quiets messages/warnings. Double -qq silences sat/unsat output too.	Morgan Deters

2013-02-16	Fix version identification for new git repository.	Morgan Deters

2013-02-15	Merge branch '1.0.x'	Kshitij Bansal

2013-02-15	prvs commit: lower warning to notice	Kshitij Bansal
	Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>
2013-02-15	make incremental+portfolio experimental	Kshitij Bansal

2013-02-15	make incremental+portfolio experimental	Kshitij Bansal