Explain non-emptiness by non-zero length in strings (#4257)

[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 5eb0818b71253c68899aac734099476d50757936..55539c802e39b5f35a44b8efbe8465be8e6763de 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;
@@ -24,120 +25,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-EqcInfo::EqcInfo(context::Context* c)
-    : d_lengthTerm(c),
-      d_codeTerm(c),
-      d_cardinalityLemK(c),
-      d_normalizedLength(c),
-      d_prefixC(c),
-      d_suffixC(c)
-{
-}
-
-Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
-{
-  // check conflict
-  Node prev = isSuf ? d_suffixC : d_prefixC;
-  if (!prev.isNull())
-  {
-    Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
-                                       << " post=" << isSuf << std::endl;
-    Node prevC = utils::getConstantEndpoint(prev, isSuf);
-    Assert(!prevC.isNull());
-    Assert(prevC.getKind() == CONST_STRING);
-    if (c.isNull())
-    {
-      c = utils::getConstantEndpoint(t, isSuf);
-      Assert(!c.isNull());
-    }
-    Assert(c.getKind() == CONST_STRING);
-    bool conflict = false;
-    // if the constant prefixes are different
-    if (c != prevC)
-    {
-      // conflicts between constants should be handled by equality engine
-      Assert(!t.isConst() || !prev.isConst());
-      Trace("strings-eager-pconf-debug")
-          << "Check conflict constants " << prevC << ", " << c << std::endl;
-      const String& ps = prevC.getConst<String>();
-      const String& cs = c.getConst<String>();
-      unsigned pvs = ps.size();
-      unsigned cvs = cs.size();
-      if (pvs == cvs || (pvs > cvs && t.isConst())
-          || (cvs > pvs && prev.isConst()))
-      {
-        // If equal length, cannot be equal due to node check above.
-        // If one is fully constant and has less length than the other, then the
-        // other will not fit and we are in conflict.
-        conflict = true;
-      }
-      else
-      {
-        const String& larges = pvs > cvs ? ps : cs;
-        const String& smalls = pvs > cvs ? cs : ps;
-        if (isSuf)
-        {
-          conflict = !larges.hasSuffix(smalls);
-        }
-        else
-        {
-          conflict = !larges.hasPrefix(smalls);
-        }
-      }
-      if (!conflict && (pvs > cvs || prev.isConst()))
-      {
-        // current is subsumed, either shorter prefix or the other is a full
-        // constant
-        return Node::null();
-      }
-    }
-    else if (!t.isConst())
-    {
-      // current is subsumed since the other may be a full constant
-      return Node::null();
-    }
-    if (conflict)
-    {
-      Trace("strings-eager-pconf")
-          << "Conflict for " << prevC << ", " << c << std::endl;
-      std::vector<Node> ccs;
-      Node r[2];
-      for (unsigned i = 0; i < 2; i++)
-      {
-        Node tp = i == 0 ? t : prev;
-        if (tp.getKind() == STRING_IN_REGEXP)
-        {
-          ccs.push_back(tp);
-          r[i] = tp[0];
-        }
-        else
-        {
-          r[i] = tp;
-        }
-      }
-      if (r[0] != r[1])
-      {
-        ccs.push_back(r[0].eqNode(r[1]));
-      }
-      Assert(!ccs.empty());
-      Node ret =
-          ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
-      Trace("strings-eager-pconf")
-          << "String: eager prefix conflict: " << ret << std::endl;
-      return ret;
-    }
-  }
-  if (isSuf)
-  {
-    d_suffixC = t;
-  }
-  else
-  {
-    d_prefixC = t;
-  }
-  return Node::null();
-}
-
 SolverState::SolverState(context::Context* c,
                          eq::EqualityEngine& ee,
                          Valuation& v)
@@ -148,7 +35,9 @@ SolverState::SolverState(context::Context* c,
       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)
@@ -209,7 +98,7 @@ const context::CDList<Node>& SolverState::getDisequalityList() const
 void SolverState::eqNotifyNewClass(TNode t)
 {
   Kind k = t.getKind();
-  if (k == STRING_LENGTH || k == STRING_CODE)
+  if (k == STRING_LENGTH || k == STRING_TO_CODE)
   {
     Node r = d_ee.getRepresentative(t[0]);
     EqcInfo* ei = getOrMakeEqcInfo(r);
@@ -222,7 +111,7 @@ void SolverState::eqNotifyNewClass(TNode t)
       ei->d_codeTerm = t[0];
     }
   }
-  else if (k == CONST_STRING)
+  else if (t.isConst())
   {
     EqcInfo* ei = getOrMakeEqcInfo(t);
     ei->d_prefixC = t;
@@ -273,7 +162,7 @@ void SolverState::eqNotifyPreMerge(TNode t1, TNode t2)
 
 void SolverState::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
 {
-  if (t1.getType().isString())
+  if (t1.getType().isStringLike())
   {
     // store disequalities between strings, may need to check if their lengths
     // are equal/disequal
@@ -354,6 +243,22 @@ 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();
+}
+
 void SolverState::setConflict() { d_conflict = true; }
 bool SolverState::isInConflict() const { return d_conflict; }