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

Age	Commit message (Collapse)	Author
2021-05-24	Move proof utilities to src/proof/ (#6611)	Andrew Reynolds
	This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/. It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
2021-04-14	Rename public and private headers in src/include. (#6352)	Aina Niemetz

2021-04-12	Refactor and update copyright headers. (#6316)	Aina Niemetz

2021-04-09	Rename CVC4__ header guards to CVC5__. (#6326)	Aina Niemetz

2021-04-07	(proof-new) Proper implementation of proof node cloning (#6285)	Andrew Reynolds
	Previously, we were traversing proof node as a tree, now we use a dag traversal. This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat.
2021-04-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

2021-03-31	Rename namespace CVC4 to CVC5. (#6249)	Aina Niemetz

2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-03-03	More cleanup of includes to reduce compilation times (#6037)	Gereon Kremer
	Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
2020-12-02	Update copyright headers.	Aina Niemetz

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-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-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.