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 /src/theory/strings/solver_state.h | |
| parent | 863f229f992cbe02a64889675fc31950e0fe2859 (diff) | |
(proof-new) Minor update to strings solver state (#4510)
Diffstat (limited to 'src/theory/strings/solver_state.h')
| -rw-r--r-- | src/theory/strings/solver_state.h | 11 |
1 files changed, 10 insertions, 1 deletions
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; /** |