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

Age	Commit message (Collapse)	Author
2021-04-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

2021-03-31	Rename namespace CVC4 to CVC5. (#6249)	Aina Niemetz

2021-03-31	Eliminate dependencies on quantifiers engine in internal quantifiers code ↵	Andrew Reynolds
	(#6240) This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned. Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine.
2021-03-26	Pass term registry to quantifiers modules (#6216)	Andrew Reynolds

2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-02-17	Eliminate non-static members in term util (#5919)	Andrew Reynolds
	This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods. This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
2021-02-17	Move methods from term util to quantifiers registry (#5916)	Andrew Reynolds
	Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class. Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.