Move cardinality inference scheme to base solver in strings (#3792)

Moves handling of cardinality to the base solver, refactors how cardinality is accessed.

No intended behavior change in this commit.

1 files changed, 133 insertions, 0 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 2f5bc8e2b..343f6e4f8 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -35,6 +35,7 @@ BaseSolver::BaseSolver(context::Context* c,
 {
   d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
   d_false = NodeManager::currentNM()->mkConst(false);
+  d_cardSize = utils::getAlphabetCardinality();
 }
 
 BaseSolver::~BaseSolver() {}
@@ -359,6 +360,138 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
   }
 }
 
+void BaseSolver::checkCardinality()
+{
+  // This will create a partition of eqc, where each collection has length that
+  // are pairwise propagated to be equal. We do not require disequalities
+  // between the lengths of each collection, since we split on disequalities
+  // between lengths of string terms that are disequal (DEQ-LENGTH-SP).
+  std::vector<std::vector<Node> > cols;
+  std::vector<Node> lts;
+  d_state.separateByLength(d_stringsEqc, cols, lts);
+  NodeManager* nm = NodeManager::currentNM();
+  Trace("strings-card") << "Check cardinality...." << std::endl;
+  // for each collection
+  for (unsigned i = 0, csize = cols.size(); i < csize; ++i)
+  {
+    Node lr = lts[i];
+    Trace("strings-card") << "Number of strings with length equal to " << lr
+                          << " is " << cols[i].size() << std::endl;
+    if (cols[i].size() <= 1)
+    {
+      // no restriction on sets in the partition of size 1
+      continue;
+    }
+    // size > c^k
+    unsigned card_need = 1;
+    double curr = static_cast<double>(cols[i].size());
+    while (curr > d_cardSize)
+    {
+      curr = curr / static_cast<double>(d_cardSize);
+      card_need++;
+    }
+    Trace("strings-card")
+        << "Need length " << card_need
+        << " for this number of strings (where alphabet size is " << d_cardSize
+        << ")." << std::endl;
+    // check if we need to split
+    bool needsSplit = true;
+    if (lr.isConst())
+    {
+      // if constant, compare
+      Node cmp = nm->mkNode(GEQ, lr, nm->mkConst(Rational(card_need)));
+      cmp = Rewriter::rewrite(cmp);
+      needsSplit = !cmp.getConst<bool>();
+    }
+    else
+    {
+      // find the minimimum constant that we are unknown to be disequal from, or
+      // otherwise stop if we increment such that cardinality does not apply
+      unsigned r = 0;
+      bool success = true;
+      while (r < card_need && success)
+      {
+        Node rr = nm->mkConst(Rational(r));
+        if (d_state.areDisequal(rr, lr))
+        {
+          r++;
+        }
+        else
+        {
+          success = false;
+        }
+      }
+      if (r > 0)
+      {
+        Trace("strings-card")
+            << "Symbolic length " << lr << " must be at least " << r
+            << " due to constant disequalities." << std::endl;
+      }
+      needsSplit = r < card_need;
+    }
+
+    if (!needsSplit)
+    {
+      // don't need to split
+      continue;
+    }
+    // first, try to split to merge equivalence classes
+    for (std::vector<Node>::iterator itr1 = cols[i].begin();
+         itr1 != cols[i].end();
+         ++itr1)
+    {
+      for (std::vector<Node>::iterator itr2 = itr1 + 1; itr2 != cols[i].end();
+           ++itr2)
+      {
+        if (!d_state.areDisequal(*itr1, *itr2))
+        {
+          // add split lemma
+          if (d_im.sendSplit(*itr1, *itr2, "CARD-SP"))
+          {
+            return;
+          }
+        }
+      }
+    }
+    // otherwise, we need a length constraint
+    uint32_t int_k = static_cast<uint32_t>(card_need);
+    EqcInfo* ei = d_state.getOrMakeEqcInfo(lr, true);
+    Trace("strings-card") << "Previous cardinality used for " << lr << " is "
+                          << ((int)ei->d_cardinalityLemK.get() - 1)
+                          << std::endl;
+    if (int_k + 1 > ei->d_cardinalityLemK.get())
+    {
+      Node k_node = nm->mkConst(Rational(int_k));
+      // add cardinality lemma
+      Node dist = nm->mkNode(DISTINCT, cols[i]);
+      std::vector<Node> vec_node;
+      vec_node.push_back(dist);
+      for (std::vector<Node>::iterator itr1 = cols[i].begin();
+           itr1 != cols[i].end();
+           ++itr1)
+      {
+        Node len = nm->mkNode(STRING_LENGTH, *itr1);
+        if (len != lr)
+        {
+          Node len_eq_lr = len.eqNode(lr);
+          vec_node.push_back(len_eq_lr);
+        }
+      }
+      Node len = nm->mkNode(STRING_LENGTH, cols[i][0]);
+      Node cons = nm->mkNode(GEQ, len, k_node);
+      cons = Rewriter::rewrite(cons);
+      ei->d_cardinalityLemK.set(int_k + 1);
+      if (!cons.isConst() || !cons.getConst<bool>())
+      {
+        std::vector<Node> emptyVec;
+        d_im.sendInference(emptyVec, vec_node, cons, "CARDINALITY", true);
+        return;
+      }
+    }
+  }
+  Trace("strings-card") << "...end check cardinality" << std::endl;
+}
+
 bool BaseSolver::isCongruent(Node n)
 {
   return d_congruent.find(n) != d_congruent.end();