Convert more uses of strings to words (#4527)

[cvc5.git] / src / theory / strings / solver_state.cpp

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 30acba9fdd63edbaa8ab13af67f00ccf5f877192..622e919f790efb6911a880c960721ad687fcad61 100644 (file)
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/solver_state.h"
 
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -25,16 +26,20 @@ 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),
       d_conflict(c, false),
       d_pendingConflict(c)
 {
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
 }
+
 SolverState::~SolverState()
 {
   for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
@@ -43,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))
@@ -240,6 +248,36 @@ Node SolverState::getLength(Node t, std::vector<Node>& exp)
   return getLengthExp(t, exp, t);
 }
 
+Node SolverState::explainNonEmpty(Node s)
+{
+  Assert(s.getType().isStringLike());
+  Node emp = Word::mkEmptyWord(s.getType());
+  if (areDisequal(s, emp))
+  {
+    return s.eqNode(emp).negate();
+  }
+  Node sLen = utils::mkNLength(s);
+  if (areDisequal(sLen, d_zero))
+  {
+    return sLen.eqNode(d_zero).negate();
+  }
+  return Node::null();
+}
+
+bool SolverState::isEqualEmptyWord(Node s, Node& emps)
+{
+  Node sr = getRepresentative(s);
+  if (sr.isConst())
+  {
+    if (Word::getLength(sr) == 0)
+    {
+      emps = sr;
+      return true;
+    }
+  }
+  return false;
+}
+
 void SolverState::setConflict() { d_conflict = true; }
 bool SolverState::isInConflict() const { return d_conflict; }