diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-21 23:10:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-21 21:10:24 -0700 |
| commit | 0f9b0dd69bef6a108b1ccc185223733f1d8fa40d (patch) | |
| tree | ae0668647ed08def249039bb320cfd84106f0788 | |
| parent | 863f229f992cbe02a64889675fc31950e0fe2859 (diff) | |
(proof-new) Minor update to strings solver state (#4510)
| -rw-r--r-- | src/theory/strings/solver_state.cpp | 5 | ||||
| -rw-r--r-- | src/theory/strings/solver_state.h | 11 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
3 files changed, 16 insertions, 2 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 55539c802..1766a4b24 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -26,9 +26,11 @@ namespace theory { namespace strings { SolverState::SolverState(context::Context* c, + context::UserContext* u, eq::EqualityEngine& ee, Valuation& v) : d_context(c), + d_ucontext(u), d_ee(ee), d_eeDisequalities(c), d_valuation(v), @@ -46,6 +48,9 @@ SolverState::~SolverState() } } +context::Context* SolverState::getSatContext() const { return d_context; } +context::UserContext* SolverState::getUserContext() const { return d_ucontext; } + Node SolverState::getRepresentative(Node t) const { if (d_ee.hasTerm(t)) diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 623a06941..bd5bb2926 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -44,8 +44,15 @@ class SolverState typedef context::CDList<Node> NodeList; public: - SolverState(context::Context* c, eq::EqualityEngine& ee, Valuation& v); + SolverState(context::Context* c, + context::UserContext* u, + eq::EqualityEngine& ee, + Valuation& v); ~SolverState(); + /** Get the SAT context */ + context::Context* getSatContext() const; + /** Get the user context */ + context::UserContext* getUserContext() const; //-------------------------------------- equality information /** * Get the representative of t in the equality engine of this class, or t @@ -167,6 +174,8 @@ class SolverState Node d_zero; /** Pointer to the SAT context object used by the theory of strings. */ context::Context* d_context; + /** Pointer to the user context object used by the theory of strings. */ + context::UserContext* d_ucontext; /** Reference to equality engine of the theory of strings. */ eq::EqualityEngine& d_ee; /** diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6f3b4c0cb..5107fa3f9 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -71,7 +71,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_notify(*this), d_statistics(), d_equalityEngine(d_notify, c, "theory::strings::ee", true), - d_state(c, d_equalityEngine, d_valuation), + d_state(c, u, d_equalityEngine, d_valuation), d_termReg(c, u, d_equalityEngine, out, d_statistics), d_im(nullptr), d_rewriter(&d_statistics.d_rewrites), |