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

Age	Commit message (Collapse)	Author
2021-08-16	Push Env class into TheoryState (#7012)	Gereon Kremer
	This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.
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-25	Refactor construction of triggers (#6209)	Andrew Reynolds
	This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.
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-13	Moving methods from quantifiers engine to quantifiers state (#5881)	Andrew Reynolds
	Towards eliminating dependencies on quantifiers engine.
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-20	Add TheoryState objects to each Theory (#4920)	Andrew Reynolds
	This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one). Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects. Notice this PR does not update the theories to use these states yet, it simply adds the objects.