From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 May 2020 04:10:24 +0000 (-0500)
Subject: (proof-new) Minor update to strings solver state (#4510)
X-Git-Tag: cvc5-1.0.0~3303
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f9b0dd69bef6a108b1ccc185223733f1d8fa40d;p=cvc5.git

(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 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),