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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index db4c9012c..0e44c9461 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -34,10 +34,12 @@ namespace theory { namespace strings { RegExpSolver::RegExpSolver(TheoryStrings& p, + SolverState& s, InferenceManager& im, context::Context* c, context::UserContext* u) : d_parent(p), + d_state(s), d_im(im), d_regexp_ucached(u), d_regexp_ccached(c), @@ -134,7 +136,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) bool flag = true; Node x = atom[0]; Node r = atom[1]; - Assert(rep == d_parent.getRepresentative(x)); + Assert(rep == d_state.getRepresentative(x)); // The following code takes normal forms into account for the purposes // of simplifying a regular expression membership x in R. For example, // if x = "A" in the current context, then we may be interested in @@ -250,7 +252,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) repUnfold.insert(rep); } } - if (d_im.hasConflict()) + if (d_state.isInConflict()) { break; } @@ -259,7 +261,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) } if (addedLemma) { - if (!d_im.hasConflict()) + if (!d_state.isInConflict()) { for (unsigned i = 0; i < processed.size(); i++) { @@ -468,7 +470,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) bool RegExpSolver::checkPDerivative( Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp) { - if (d_parent.areEqual(x, d_emptyString)) + if (d_state.areEqual(x, d_emptyString)) { Node exp; switch (d_regexp_opr.delta(r, exp)) |