Move more string utility functions (#3398)

This is work towards splitting a "core solver" object from TheoryStrings.

This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects.

It also corrects an issue where we were maintaining two `d_conflict` fields.

1 files changed, 195 insertions, 4 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 5c08fdee3..c9a2bcd70 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -34,10 +34,14 @@ InferenceManager::InferenceManager(TheoryStrings& p,
                                    context::UserContext* u,
                                    SolverState& s,
                                    OutputChannel& out)
-    : d_parent(p), d_state(s), d_out(out), d_keep(c)
+    : d_parent(p), d_state(s), d_out(out), d_keep(c), d_lengthLemmaTermsCache(u)
 {
-  d_true = NodeManager::currentNM()->mkConst(true);
-  d_false = NodeManager::currentNM()->mkConst(false);
+  NodeManager* nm = NodeManager::currentNM();
+  d_zero = nm->mkConst(Rational(0));
+  d_one = nm->mkConst(Rational(1));
+  d_emptyString = nm->mkConst(::CVC4::String(""));
+  d_true = nm->mkConst(true);
+  d_false = nm->mkConst(false);
 }
 
 bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
@@ -131,7 +135,7 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
     Node eq_exp;
     if (options::stringRExplainLemmas())
     {
-      eq_exp = d_parent.mkExplain(exp, exp_n);
+      eq_exp = mkExplain(exp, exp_n);
     }
     else
     {
@@ -279,6 +283,95 @@ void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
   d_pendingReqPhase[lit] = pol;
 }
 
+void InferenceManager::registerLength(Node n, LengthStatus s)
+{
+  if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
+  {
+    return;
+  }
+  d_lengthLemmaTermsCache.insert(n);
+
+  if (s == LENGTH_IGNORE)
+  {
+    // ignore it
+    return;
+  }
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
+
+  if (s == LENGTH_GEQ_ONE)
+  {
+    Node neq_empty = n.eqNode(d_emptyString).negate();
+    Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
+    Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
+    Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
+                           << std::endl;
+    Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
+    d_out.lemma(len_geq_one);
+    return;
+  }
+
+  if (s == LENGTH_ONE)
+  {
+    Node len_one = n_len.eqNode(d_one);
+    Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
+                           << std::endl;
+    Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
+    d_out.lemma(len_one);
+    return;
+  }
+  Assert(s == LENGTH_SPLIT);
+
+  if (options::stringSplitEmp() || !options::stringLenGeqZ())
+  {
+    Node n_len_eq_z = n_len.eqNode(d_zero);
+    Node n_len_eq_z_2 = n.eqNode(d_emptyString);
+    Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
+    case_empty = Rewriter::rewrite(case_empty);
+    Node case_nempty = nm->mkNode(GT, n_len, d_zero);
+    if (!case_empty.isConst())
+    {
+      Node lem = nm->mkNode(OR, case_empty, case_nempty);
+      d_out.lemma(lem);
+      Trace("strings-lemma")
+          << "Strings::Lemma LENGTH >= 0 : " << lem << std::endl;
+      // prefer trying the empty case first
+      // notice that requirePhase must only be called on rewritten literals that
+      // occur in the CNF stream.
+      n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
+      Assert(!n_len_eq_z.isConst());
+      d_out.requirePhase(n_len_eq_z, true);
+      n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
+      Assert(!n_len_eq_z_2.isConst());
+      d_out.requirePhase(n_len_eq_z_2, true);
+    }
+    else if (!case_empty.getConst<bool>())
+    {
+      // the rewriter knows that n is non-empty
+      Trace("strings-lemma")
+          << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty
+          << std::endl;
+      d_out.lemma(case_nempty);
+    }
+    else
+    {
+      // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
+      // n ---> "". Since this method is only called on non-constants n, it must
+      // be that n = "" ^ len( n ) = 0 does not rewrite to true.
+      Assert(false);
+    }
+  }
+
+  // additionally add len( x ) >= 0 ?
+  if (options::stringLenGeqZ())
+  {
+    Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero);
+    n_len_geq = Rewriter::rewrite(n_len_geq);
+    d_out.lemma(n_len_geq);
+  }
+}
+
 void InferenceManager::addToExplanation(Node a,
                                         Node b,
                                         std::vector<Node>& exp) const
@@ -435,6 +528,104 @@ void InferenceManager::inferSubstitutionProxyVars(
   }
 }
 
+Node InferenceManager::mkExplain(const std::vector<Node>& a) const
+{
+  std::vector<Node> an;
+  return mkExplain(a, an);
+}
+
+Node InferenceManager::mkExplain(const std::vector<Node>& a,
+                                 const std::vector<Node>& an) const
+{
+  std::vector<TNode> antec_exp;
+  // copy to processing vector
+  std::vector<Node> aconj;
+  for (const Node& ac : a)
+  {
+    utils::flattenOp(AND, ac, aconj);
+  }
+  eq::EqualityEngine* ee = d_state.getEqualityEngine();
+  for (const Node& apc : aconj)
+  {
+    Assert(apc.getKind() != AND);
+    Debug("strings-explain") << "Add to explanation " << apc << std::endl;
+    if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
+    {
+      Assert(ee->hasTerm(apc[0][0]));
+      Assert(ee->hasTerm(apc[0][1]));
+      // ensure that we are ready to explain the disequality
+      AlwaysAssert(ee->areDisequal(apc[0][0], apc[0][1], true));
+    }
+    Assert(apc.getKind() != EQUAL || ee->areEqual(apc[0], apc[1]));
+    // now, explain
+    explain(apc, antec_exp);
+  }
+  for (const Node& anc : an)
+  {
+    if (std::find(antec_exp.begin(), antec_exp.end(), anc) == antec_exp.end())
+    {
+      Debug("strings-explain")
+          << "Add to explanation (new literal) " << anc << std::endl;
+      antec_exp.push_back(anc);
+    }
+  }
+  Node ant;
+  if (antec_exp.empty())
+  {
+    ant = d_true;
+  }
+  else if (antec_exp.size() == 1)
+  {
+    ant = antec_exp[0];
+  }
+  else
+  {
+    ant = NodeManager::currentNM()->mkNode(kind::AND, antec_exp);
+  }
+  return ant;
+}
+
+void InferenceManager::explain(TNode literal,
+                               std::vector<TNode>& assumptions) const
+{
+  Debug("strings-explain") << "Explain " << literal << " "
+                           << d_state.isInConflict() << std::endl;
+  eq::EqualityEngine* ee = d_state.getEqualityEngine();
+  bool polarity = literal.getKind() != NOT;
+  TNode atom = polarity ? literal : literal[0];
+  std::vector<TNode> tassumptions;
+  if (atom.getKind() == EQUAL)
+  {
+    if (atom[0] != atom[1])
+    {
+      Assert(ee->hasTerm(atom[0]));
+      Assert(ee->hasTerm(atom[1]));
+      ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
+    }
+  }
+  else
+  {
+    ee->explainPredicate(atom, polarity, tassumptions);
+  }
+  for (const TNode a : tassumptions)
+  {
+    if (std::find(assumptions.begin(), assumptions.end(), a)
+        == assumptions.end())
+    {
+      assumptions.push_back(a);
+    }
+  }
+  if (Debug.isOn("strings-explain-debug"))
+  {
+    Debug("strings-explain-debug")
+        << "Explanation for " << literal << " was " << std::endl;
+    for (const TNode a : tassumptions)
+    {
+      Debug("strings-explain-debug") << "   " << a << std::endl;
+    }
+  }
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4