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

Age	Commit message (Collapse)	Author
2021-01-29	(proof-new) Distinguish pre vs post rewrites in term conversion proof ↵	Andrew Reynolds
	generator (#5833) This is work towards resolving two kinds of failures on proof-new: (1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things, (2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected. A followup PR will simplify and fix proofs for theory-preprocessing.
2020-10-20	(proof-new) Update add lazy step interface in LazyCDProof (#5299)	Andrew Reynolds
	Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments. Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).
2020-10-18	(proof-new) Witness axiom reconstruction for purification skolems (#5289)	Andrew Reynolds
	This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify. This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
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) Rewrites involving operators in term conversion proof generator ↵	Andrew Reynolds
	(#5072) In some cases, e.g. witness form conversion, we require traversing to operators in term conversion proofs. This updates the term conversion generator to support (term-context-sensitive) rewrites involving operators using HO_CONG. This requires updating the term context utilities with support for operators.
2020-08-12	(proof-new) Improve interfaces to proof generators (#4803)	Andrew Reynolds
	This includes configurable naming and a caching policy for term conversion proof generator. Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.
2020-08-12	(proof-new) Witness form proof generator (#4782)	Andrew Reynolds
	This class is responsible for the connection between terms and their witness form in the final proof.