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 /src/theory/strings/extf_solver.h | |
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 'src/theory/strings/extf_solver.h')
-rw-r--r-- | src/theory/strings/extf_solver.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index f0f0d790b..c5dd24f70 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -87,7 +87,7 @@ class ExtfSolver context::UserContext* u, SolverState& s, InferenceManager& im, - SkolemCache& skc, + TermRegistry& tr, StringsRewriter& rewriter, BaseSolver& bs, CoreSolver& cs, @@ -181,8 +181,8 @@ class ExtfSolver SolverState& d_state; /** The (custom) output channel of the theory of strings */ InferenceManager& d_im; - /** cache of all skolems */ - SkolemCache& d_skCache; + /** Reference to the term registry of theory of strings */ + TermRegistry& d_termReg; /** The theory rewriter for this theory. */ StringsRewriter& d_rewriter; /** reference to the base solver, used for certain queries */ |