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

Age	Commit message (Collapse)	Author
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-20	Improved tracing for equivalence classes of EE (#6169)	Andrew Reynolds
	Helps debugging model issues.
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

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-23	Add interface to TheoryState for sort inference and facts (#5967)	Andrew Reynolds
	This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality. This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
2021-02-02	Cleanup some includes (#5847)	Andrew Reynolds
	In particular, theory_engine.h is included many places spuriously. A few blocks of code changed indentation, updated to guidelines.
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-20	More flexible design for model manager distributed (#4976)	Andrew Reynolds
	This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture. This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine. This PR is not intended to make any behavior changes to the current architecture.
2020-08-26	Add irrelevant kinds infrastructure to TheoryModel (#4945)	Andrew Reynolds
	Currently, Theory is responsible for implementing a computeRelevantTerms method collects the union of: (1) The terms appearing in its assertions and its shared terms, (2) The set of additional terms the theory believes are relevant. Currently, (1) is computed by an internal Theory method computeRelevantTermsInternal, and the overall computeRelevantTerms is overridden by the theory (for datatypes and arrays only) for also including (2). The new plan is that Theory will only need to compute (2). Computing (1) will be the job of ModelManager::collectAssertedTerms and the model manager will call Theory::computeRelevantTerms as an additional step prior to its calls to collect model info. This will make certain optimizations possible in theory combination (e.g. tracking asserted terms incrementally). This PR adds the ModelManager::collectAssertedTerms method and also adds infrastructure for irrelevant kinds in the model object (which have an analogous interface as when "unevaluated" kinds are marked during initialization). It does not connect the implementation yet. FYI @barrettcw
2020-08-24	Add the distributed model manager (#4934)	Andrew Reynolds
	This class is responsible for model building when using a distributed approach for equality engines. This PR defines the class but does not yet activate it in TheoryEngine. This includes some model-specific things from TheoryEngine which will be migrated to this class on the next PR.