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

Age	Commit message (Collapse)	Author
2020-11-12	(proof-new) Fix true explanations of propagations in pf equality engine (#5338)	Andrew Reynolds
	This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.
2020-10-18	(proof-new) Refactoring cyclic checks (#5291)	Andrew Reynolds
	This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true. It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.
2020-10-06	(proof-new) Allow null proofs from generators in LazyCDProof (#5196)	Andrew Reynolds
	In some cases, a proof generator provided to a LazyCDProof may provide a null proof, which causes a segfault on proof-new currently. This PR makes LazyCDProof robust to this case; nullptr is interpreted as the fact is an assumption.
2020-09-30	(proof-new) Add the term conversion sequence generator (#5097)	Andrew Reynolds
	This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.
2020-09-22	Update copyright header script to support CMake and Python files (#5067)	Mathias Preiner
	This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
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.