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

Age	Commit message (Collapse)	Author
2021-09-02	Implement lazy proof checking modes (#7106)	Andrew Reynolds
	This implements several variants of lazy proof checking in the core proof checker. Note this extends the ProofNode class with an additional Boolean d_provenChecked indicating whether the d_proven field was checked by the underlying proof checker. This PR updates the default proof checking mode to lazy. The previous default can now be enabled by --proof-check=eager-simple.
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").