(proof-new) Minor update to strings solver state (#4510)

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 55539c802e39b5f35a44b8efbe8465be8e6763de..1766a4b24c43a8b11f66fc8aa0bc05160aee50f9 100644 (file)
--- 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 623a06941d59c3a1ea46cc2fce8eba8f4d8071cb..bd5bb2926caf527f45d02e2714f1a7377766bbb7 100644 (file)
--- 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 6f3b4c0cbbe4f1e08226788d1be82b6992da353a..5107fa3f954db3ecf0653a0a98e766ccd2ca6b6e 100644 (file)
--- 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),