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

Age	Commit message (Collapse)	Author
2020-07-02	(proof-new) Updates to skolem manager interface (#4664)	Andrew Reynolds
	Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs.
2020-06-16	Update copyright headers.	Aina Niemetz

2020-06-09	(proof-new) Refactor skolemization (#4586)	Andrew Reynolds
	This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized. This additionally adds more utility functions that will be used in the internal proof checker for quantifiers.
2020-06-05	(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)	Andrew Reynolds
	This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing. This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form. Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler. Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.