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-23	(proof-new) Proofs for sets purification lemmas (#6416)	Andrew Reynolds
	This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.
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	Update copyright headers to 2021. (#6081)	Aina Niemetz

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-08	Split term registry from theory state in sets (#5037)	Andrew Reynolds
	Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies. This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas. Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative. A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory.