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

Age	Commit message (Collapse)	Author
2016-06-08	Support for printing a global let map in LFSC proofs.	Guy
	Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules.
2016-06-01	Merge from proof branch	Guy

2016-06-01	Revert "Merging proof branch"	Guy
	This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01	Merging proof branch	Guy

2016-04-03	Updating the copyright headers and scripts.	Tim King

2016-03-23	squash-merge from proof branch	Guy

2016-02-24	Unifying the definitions of ClauseId to a single source of truth.	Tim King

2016-01-26	Merged bit-vector and uf proof branch.	Liana Hadarean

2015-12-24	Miscellaneous fixes	Tim King
	- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example. - Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems. - Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions. - Changing some headers to use iosfwd when possible.
2015-03-10	CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵	ajreynol
	signature. Add regressions.
2014-08-22	Unsat core infrastruture and API (SMT-LIB compliance to come).	Morgan Deters

2014-07-01	Update copyrights.	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-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-10-09	cleaned up proof code	lianah

2013-10-08	fixed uf proof with holes bugs	lianah

2013-10-07	first draft implementation of uf proofs with holes	Liana Hadarean

2013-05-10	now proofs print mapping between atom and propositional variable as a ↵	lianah
	comment in LFSC
2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2012-10-11	Standardizing copyright notice. Touches ALL sources, guys, sorry.. it's	Morgan Deters
	just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-24	Fix the memout issue seen in recent nightly regressions (was due to a	Morgan Deters
	Statistics-printing problem, limited to certain benchmarks). Mark some unlabeled header files "cvc4_private.h". Other minor cleanup. (this commit was certified error- and warning-free by the test-and-commit script.)
2011-10-28	* ability to output NodeBuilders without first converting them to ↵	Morgan Deters
	Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup
2011-10-28	merged the proofgen3 branch into trunk:	Liana Hadarean
	- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.