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

Age	Commit message (Collapse)	Author
2020-09-01	Removes old proof code (#4964)	Haniel Barbosa
	This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure. It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
2020-07-28	Use lemma property enum for OutputChannel::lemma (#4755)	Andrew Reynolds
	There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance. This makes them into a enum.
2020-06-16	Update copyright headers.	Aina Niemetz

2019-10-30	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)	Mathias Preiner

2019-03-26	Update copyright headers.	Aina Niemetz

2018-08-17	Remove support for flipDecision (#2319)	Andrew Reynolds

2018-06-25	Updated copyright headers.	Aina Niemetz

2017-11-15	Adding garbage collection for Proof objects. (#1294)	Tim King

2017-10-25	Removing throw specifiers from OutputChannel and subclasses. (#1209)	Tim King

2017-07-07	Update copyright headers.	Mathias Preiner

2016-11-18	Removing some throw specifiers from OutputChannel. Fixes bug 716.	Tim King

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