diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-16 09:50:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-16 09:50:43 -0500 |
| commit | f0e6c103304fc5c00c9bdfb699ad878ead5c66ed (patch) | |
| tree | b18b69c9793125d8d1f3e995b8aaa0b538ae43b6 /src/theory/strings/regexp_solver.h | |
| parent | 912b65006615fe4074cde54b080f48e3d6c12042 (diff) | |
Eliminate remaining references to parent TheoryStrings object (#4315)
This PR makes it so that the module dependencies in the theory of strings are acyclic. This is important for further organization towards proofs for strings.
The main change in this PR is to ensure that InferenceManager has a pointer to ExtTheory, which is needed for several of its methods. This required changing several solvers into unique_ptr to properly initialize.
Diffstat (limited to 'src/theory/strings/regexp_solver.h')
| -rw-r--r-- | src/theory/strings/regexp_solver.h | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index 1d065181b..b44c6c8d9 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -34,8 +34,6 @@ namespace CVC4 { namespace theory { namespace strings { -class TheoryStrings; - class RegExpSolver { typedef context::CDList<Node> NodeList; @@ -46,9 +44,9 @@ class RegExpSolver typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - RegExpSolver(TheoryStrings& p, - SolverState& s, + RegExpSolver(SolverState& s, InferenceManager& im, + CoreSolver& cs, ExtfSolver& es, SequencesStatistics& stats, context::Context* c, @@ -113,12 +111,12 @@ class RegExpSolver Node d_emptyRegexp; Node d_true; Node d_false; - /** the parent of this object */ - TheoryStrings& d_parent; /** The solver state of the parent of this object */ SolverState& d_state; /** the output channel of the parent of this object */ InferenceManager& d_im; + /** reference to the core solver, used for certain queries */ + CoreSolver& d_csolver; /** reference to the extended function solver of the parent */ ExtfSolver& d_esolver; /** Reference to the statistics for the theory of strings/sequences. */ |