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-30	Miscellaneous elimination of dependencies on quantifiers engine (#6238)	Andrew Reynolds
	This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
2021-03-29	Move decision manager into theory inference manager (#6231)	Andrew Reynolds
	This makes it so that the decision manager is accessible from TheoryInferenceManager. This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.
2021-03-26	Pass term registry to quantifiers modules (#6216)	Andrew Reynolds

2021-03-24	Use inference manager to access intantiate utility instead of quantifiers ↵	Andrew Reynolds
	engine (#6198) Towards breaking dependencies on quantifers engine.
2021-03-23	Passing term registry to ematching utilities (#6190)	Andrew Reynolds
	Model is now nested into term registry. This PR also resolves some complications due to namespaces within quantifiers.
2021-03-19	Refactor initialization of quantifiers model and builder (#6175)	Andrew Reynolds
	This is in preparation for breaking several circular dependencies and moving the instantiate utility into the theory inference manager.
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-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-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.
2021-02-04	Introduce quantifiers registry utility (#5829)	Andrew Reynolds
	This is a simple module for determining which quantifiers module has ownership of quantified formulas. This is work towards eliminating dependencies of quantifiers modules. Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.
2021-01-26	Introduce quantifiers inference manager (#5821)	Andrew Reynolds
	This is the second prerequisite for eliminating dependencies on quantifiers engine. This PR threads a quantifiers inference manager through all modules in quantifiers that add lemmas. The code for adding lemmas in quantifiers engine will be migrated to this class.
2021-01-26	Remove deprecated quantifiers modules (#5820)	Andrew Reynolds

2021-01-26	Refactor quantifiers engine initialization (#5813)	Andrew Reynolds
	This is a step towards breaking up the quantifiers engine. The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed. This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.
2020-12-02	Update copyright headers.	Aina Niemetz

2020-09-14	Move quantifiers engine private to own file (#5053)	Andrew Reynolds
	This moves and renames the quantifiers engine private class to QuantifiersModules. This is in preparation for using a standard state and inference manager object in TheoryQuantifiers and QuantifiersEngine. Initializing quantifiers engine is a bit non-standard since it is intentionally a separate entity from TheoryQuantifiers. However, the plan is for quantifiers engine to use the state and inference manager of TheoryQuantifiers. This PR additionally moves the initialization of quantifiers modules to a QuantifiersEngine::finishInit() method. The motivation for is that we do not have a state and inference manager during construction of QuantifiersEngine, since these will live in TheoryQuantifiers and will be passed to QuantifiersEngine during TheoryQuantifiers::finishInit. This means that we need a final pass to initialize quantifiers engine after these are initialized, which thus must come as the last step of TheoryEngine::finishInit. The next PR will connect the state and inference manager to QuantifiersEngine during TheoryQuantifiers::finishInit. Then, the plan is for many of the core utilities in QuantifiersEngine to migrate to state/inference manager, and finally for its modules to reference state and inference manager instead of QuantifiersEngine.