summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/equality_query.h
AgeCommit message (Collapse)Author
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-22Move equality query utility into quantifiers model (#6186)Andrew Reynolds
This simplifies the initialization of quantifiers engine. This PR also makes general improvements to EqualityQuery.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
2021-02-04Eliminate equality query dependence on quantifiers engine (#5831)Andrew Reynolds
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.
2021-01-28Use standard equality engine information in quantifiers state (#5824)Andrew Reynolds
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.
2021-01-26Refactor 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-09-22Update 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-06-16Update copyright headers.Aina Niemetz
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-08-17Remove miscellaneous unused code (#2333)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2017-10-28Document term db (#1220)Andrew Reynolds
* 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
2017-10-09Split term database (#1206)Andrew Reynolds
* 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback