diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-16 18:44:17 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-16 16:44:17 -0700 |
| commit | 207245fef36ccad1281fefe9d3f3403cd4f6d15b (patch) | |
| tree | aa364b8701f01cb9e30afb8b85c615fae0ee6f40 /src/theory/strings/regexp_solver.h | |
| parent | 80b14c0965678fb91467de287b00a9a1d8a39be5 (diff) | |
Solver state for theory of strings (#3181)
This refactors the theory of strings to use a solver state object, which manages state information regarding assertions.
It also deletes some unused/undefined functions in theory_strings.h.
There are no major changes to the behavior of the code or its documentation in this PR.
This is work towards #1881.
Diffstat (limited to 'src/theory/strings/regexp_solver.h')
| -rw-r--r-- | src/theory/strings/regexp_solver.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index c4d6afda0..0b84ebc79 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "theory/strings/inference_manager.h" #include "theory/strings/regexp_operation.h" +#include "theory/strings/solver_state.h" #include "util/regexp.h" namespace CVC4 { @@ -44,6 +45,7 @@ class RegExpSolver public: RegExpSolver(TheoryStrings& p, + SolverState& s, InferenceManager& im, context::Context* c, context::UserContext* u); @@ -100,6 +102,8 @@ class RegExpSolver 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; // check membership constraints |