Split TermRegistry object from TheoryStrings (#4312)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Apr 2020 13:23:27 +0000 (08:23 -0500)
committerGitHub <noreply@github.com>
Wed, 15 Apr 2020 13:23:27 +0000 (08:23 -0500)
commit42c765eb255e5bfa65682cd812973f0f3c90017c
tree7d45554cfc628cfd457e731d2f0d1bc6f6f029c8
parent0f3e4d1c802e1fe5fd90e712a6382ff9ca2bab34
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.
13 files changed:
src/CMakeLists.txt
src/theory/strings/core_solver.cpp
src/theory/strings/core_solver.h
src/theory/strings/extf_solver.cpp
src/theory/strings/extf_solver.h
src/theory/strings/inference_manager.cpp
src/theory/strings/inference_manager.h
src/theory/strings/strings_fmf.cpp
src/theory/strings/strings_fmf.h
src/theory/strings/term_registry.cpp [new file with mode: 0644]
src/theory/strings/term_registry.h [new file with mode: 0644]
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h