diff options
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. */ |