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

Age	Commit message (Collapse)	Author
2020-09-17	[proof-new] Have mkScope agnostic to True assumptions (#5086)	Haniel Barbosa

2020-09-16	[proof-new] Adds Lazy CDProof chain data-structure (#5060)	Haniel Barbosa
	A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
2020-09-11	(proof-new) Handle mismatched assumptions in proof equality engine during ↵	Andrew Reynolds
	mkScope (#5012) This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases. A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
2020-09-02	(proof-new) Improve debugging infrastructure for open proofs (#4984)	Andrew Reynolds
	This includes more versions of checking whether a proof node is closed and standardizing output.
2020-06-23	(proof-new) Updates to proof node manager (#4617)	Andrew Reynolds
	Main feature added is the mkScope interface, which is agnostic to symmetry of (dis)equalities. It also adds a check for cyclic proofs when using the interface ProofNodeManager::updateNode. Note that an earlier version of this method was agnostics to predicates vs Boolean equality with constants. This is no longer required.
2020-06-16	Update copyright headers.	Aina Niemetz

2020-06-05	(proof-new) Updates to CDProof (#4565)	Andrew Reynolds
	This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites.
2020-04-16	Add ProofNodeManager and ProofChecker (#4317)	Andrew Reynolds
	Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure. ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker). ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker. This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.