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

Age	Commit message (Collapse)	Author
2021-10-07	Use skolem lemma in prop layer interfaces (#7320)	Andrew Reynolds

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-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-11	(proof-new) Clean up uses of witness with skolem lemmas (#6109)	Andrew Reynolds
	This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy. It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.
2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-03-08	(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)	Andrew Reynolds
	Due to recent simplifications in the internal calculus, we will no longer reason about WITNESS terms in conclusions of ProofNode, instead WITNESS terms will only be for bookkeeping.This means that some implementations of ppRewrite must change to return SKOLEM instead of WITNESS terms. Since witness terms are currently used as a way of specifying "replace t by skolem k, and send a lemma about k", a followup PR will update Theory::ppRewrite to take an additional argument std::vector<SkolemLemma>& lems where new lemmas must be explicitly added to a vector (instead of encoded as witness). Then, all Theory::ppRewrite will return skolems instead of witness terms. This PR changes arithmetic in preparation for this change. Notice that I'm introducing SkolemLemma in this PR, which is a very common pattern that can simplify some of our interfaces, e.g. see https://github.com/CVC4/CVC4/blob/master/src/smt/term_formula_removal.h#L93, https://github.com/CVC4/CVC4/blob/master/src/prop/prop_engine.h#L94. Note that the indentation of code in operator_elim.cpp changed.