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-05-13	Add std::hash overloads for Node, TNode and TypeNode. (#6534)	Mathias Preiner
	Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-12	Refactor and update copyright headers. (#6316)	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-10	Move ExprManager::isNAryKind to NodeManager. (#6107)	Aina Niemetz
	This also renames metakind::getLowerBoundForKind and metakind::getUpperBoundForKind for consistency. Note that the NodeManager class needs to be reordered to comply to our style guidelines. This PR does not reorder but introduces a public block at the top (where the rest of the public interface of the class should go eventually).
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.
2021-03-02	Clean up includes to reduce compile times (#6031)	Gereon Kremer
	This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
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-16	[proof-new] Extending eqproof conversion to HO congruence (#5071)	Haniel Barbosa

2020-09-01	Removes old proof code (#4964)	Haniel Barbosa
	This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure. It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
2020-08-12	[proof-new] Adding support for corner case of transitivity simulating ↵	Haniel Barbosa
	MERGED_THROUGH_CONSTANTS (#4879)
2020-08-12	generalize handling MERGED_THROUGH_CONSTANST in EqProof conversion (#4878)	Haniel Barbosa
	Now that we are using the constant folding in equality engine for more than equality it is necessary to generalize the previously-hard-coded handling of MERGED_THROUGH_CONSTANTS.
2020-07-16	Fix EqProof to ProofNode conversion (#4760)	Haniel Barbosa
	A wrong change slipped away during the cleaning of the module. This commit fixes the conversion.
2020-07-16	(proof-new) Implements the conversion between EqProof and ProofNode (#4756)	Haniel Barbosa

2020-07-15	(proof-new) Adding API for converting EqProof into ProofNode (#4747)	Haniel Barbosa
	Also puts EqProof into its own module. Next will come the implementation of the API.