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

Age	Commit message (Collapse)	Author
2021-09-09	Remove `TheoryState::options()` (#7148)	Andres Noetzli
	This commit removes TheoryState::options() by changing more classes to EnvObjs.
2021-09-07	Use `EnvObj` methods instead of `Theory` methods (#7144)	Andres Noetzli
	This removes the methods `getEnv()`, `options()`, `getSatContext()`, and `getUserContext()` from the `Theory` class because they are now part of `EnvObj`. Additionally, this commit converts the inference managers to `EnvObj` because of there were some calls to retrieve the contexts from `Theory` in those classes.
2021-08-24	Uniform treatment of trusted theory inferences in proofs (#7044)	Andrew Reynolds
	Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.
2021-04-14	Refactor / reimplement statistics (#6162)	Gereon Kremer
	This PR refactors how we collect statistics. It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic. It also extends the C++ API to obtain and inspect the statistics. To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
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	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-03-02	Clean up includes to reduce compile times (#6031)	Gereon Kremer
	This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
2021-02-19	Refactoring theory inference process (#5920)	Andrew Reynolds
	This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.
2021-02-18	Add statistic for InferenceId to TheoryInferenceManager. (#5913)	Gereon Kremer
	This PR uses the IntegralHistogramStat to obtain statistics about the sent inferences within the TheoryInferenceManager. All theories are adapted to provide a proper name (prefix) for the name of the statistic.
2021-02-17	Add InferenceIds for theory of arrays (#5910)	Gereon Kremer
	This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
2021-02-11	Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)	Gereon Kremer
	This PR makes most methods of the TheoryInferenceManager expect an InferenceId. All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere. In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs. The InferenceIds are not yet used, but will be used for statistics and debug output.
2021-02-02	(proof-new) Miscellaneous fixes and regressions (#5841)	Andrew Reynolds

2020-12-02	Update copyright headers.	Aina Niemetz

2020-10-01	(proof-new) Make arrays proof producing (#5112)	Andrew Reynolds
	This includes adding a basic inference manager to arrays that ensures that the correct applications of PfRule are given to the inference manager. Note that some calls to lemma are yet to be converted. Also note that some minor simplifications were made for unnecessary parts of the code.