Age | Commit message (Collapse) | Author |
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
|
|
|
|
|
|
|
|
|
|
This simplifies the initialization of quantifiers engine.
This PR also makes general improvements to EqualityQuery.
|
|
|
|
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
|
|
This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on.
|
|
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
Adds missing override keywords.
|
|
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
|
|
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
|