diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-15 08:23:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-15 08:23:27 -0500 |
| commit | 42c765eb255e5bfa65682cd812973f0f3c90017c (patch) | |
| tree | 7d45554cfc628cfd457e731d2f0d1bc6f6f029c8 /test | |
| parent | 0f3e4d1c802e1fe5fd90e712a6382ff9ca2bab34 (diff) | |
Split TermRegistry object from TheoryStrings (#4312)
This consolidates functionalities from TheoryStrings and InferenceManager related to registering terms, including sending "preregistration lemmas" for them. The main purpose of this PR is to detangle this module from InferenceManager so that these two modules have exactly one call to OutputChannel::lemma each.
For the purposes of the theory solvers, TermRegistry contains the official SkolemCache of TheoryStrings, and can be seen as subsuming the previous interface for this class.
This PR is needed for further progress on strings proofs, marking as major since this will be a blocker shortly for this project.
A few things were cleaned in this PR. One function changed name InferenceManager::registerTerm --> TermRegistry::getRegisterTermLemma. No major behavior changes.
Diffstat (limited to 'test')
0 files changed, 0 insertions, 0 deletions