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

Age	Commit message (Collapse)	Author
2021-05-27	Update proof namespaces (#6614)	Andrew Reynolds
	This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
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-05-13	Add std::hash overloads for Node, TNode and TypeNode. (#6534)	Mathias Preiner
	Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
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-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

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

2021-03-09	Some more cleanup of includes (#6083)	Gereon Kremer
	This PR does some more cleanup of the includes.
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-20	(proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487)	Gereon Kremer
	This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.
2020-10-19	(proof-new) Updates to assertions pipeline and preprocess generator (#5300)	Andrew Reynolds
	This updates and improves assertions pipeline and preprocess generator so that they avoid cyclic proofs and have better infrastructure for catching pedantic failures. This is in preparation for making the non-clausal-simplification pass proof producing.
2020-10-13	(proof-new) Generalize preprocess proof generator (#5245)	Andrew Reynolds
	This class is of general use, not just as the overall maintainer of proofs of preprocessing, but also locally within preprocessing passes. This generalizes the interface slightly and also does some minor cleaning.
2020-09-29	(proof-new) Fixes for preprocess proof generator and proofs in assertion ↵	Andrew Reynolds
	pipeline (#5136) This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline. Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.
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-07-13	(proof-new) SMT Preprocess proof generator (#4708)	Andrew Reynolds
	This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine. It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.