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

Age	Commit message (Collapse)	Author
2021-10-06	Eliminate more hard coded uses of user context (#7309)	Andrew Reynolds
	This is in preparation to make the "lemma context" configurable.
2021-09-13	Connect difficulty manager to TheoryEngine (#7161)	Andrew Reynolds
	This also introduces the produceDifficulty option which is analogous to produceUnsatCores. It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.
2021-05-13	Add std::hash overloads for Node, TNode and TypeNode. (#6534)	Mathias Preiner
	Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-14	Add interface for getting relevant assertions (#5131)	Andrew Reynolds
	This adds an interface to TheoryEngine for getting the current set of relevant assertions if it is available. An interface to this can further be added to the API in a future PR.
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-09	Some more cleanup of includes (#6083)	Gereon Kremer
	This PR does some more cleanup of the includes.
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-08-18	Add the relevance manager module (#4894)	Andrew Reynolds
	This PR adds the relevance manager module, which will be used in forthcoming PRs to query assignments for whether a literal is "relevant" (e.g. critical for satisfying the input formula). Leveraging this technique has led to noticeable improvements for non-linear arithmetic (https://github.com/ajreynol/CVC4/tree/relManager). This PR does not enable it, but adds the module only.