Cardinality-related inferences per type in theory of strings (#4585)

Towards theory of sequences.

This updates various inference steps in the theory of strings that are based on collecting all equivalence classes to be per string-like type.

7 files changed, 97 insertions, 36 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 16c83de78..4a03637d0 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -432,9 +432,19 @@ void BaseSolver::checkCardinality()
   // 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;
+  std::map<TypeNode, std::vector<std::vector<Node> > > cols;
+  std::map<TypeNode, std::vector<Node> > lts;
   d_state.separateByLength(d_stringsEqc, cols, lts);
+  for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& c : cols)
+  {
+    checkCardinalityType(c.first, c.second, lts[c.first]);
+  }
+}
+
+void BaseSolver::checkCardinalityType(TypeNode tn,
+                                      std::vector<std::vector<Node> >& cols,
+                                      std::vector<Node>& lts)
+{
   NodeManager* nm = NodeManager::currentNM();
   Trace("strings-card") << "Check cardinality...." << std::endl;
   // for each collection
@@ -448,6 +458,11 @@ void BaseSolver::checkCardinality()
       // no restriction on sets in the partition of size 1
       continue;
     }
+    if (!tn.isString())
+    {
+      // TODO (cvc4-projects #23): how to handle sequence for finite types?
+      continue;
+    }
     // size > c^k
     unsigned card_need = 1;
     double curr = static_cast<double>(cols[i].size());
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 1960b8352..334fdf596 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -200,6 +200,19 @@ class BaseSolver
                                        std::vector<Node>& vecc,
                                        bool ensureConst = true,
                                        bool isConst = true);
+  /**
+   * Check cardinality for type tn. This adds a lemma corresponding to
+   * cardinality for terms of type tn, if applicable.
+   *
+   * @param tn The string-like type of terms we are considering,
+   * @param cols The list of collections of equivalence classes. This is a
+   * partition of all string equivalence classes, grouped by those with equal
+   * lengths.
+   * @param lts The length of each of the collections in cols.
+   */
+  void checkCardinalityType(TypeNode tn,
+                            std::vector<std::vector<Node> >& cols,
+                            std::vector<Node>& lts);
   /** The solver state object */
   SolverState& d_state;
   /** The (custom) output channel of the theory of strings */
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 604abb1d7..b23562862 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -2239,8 +2239,6 @@ bool CoreSolver::isNormalFormPair( Node n1, Node n2 ) {
 void CoreSolver::checkNormalFormsDeq()
 {
   eq::EqualityEngine* ee = d_state.getEqualityEngine();
-  std::vector< std::vector< Node > > cols;
-  std::vector< Node > lts;
   std::map< Node, std::map< Node, bool > > processed;
   
   const context::CDList<Node>& deqs = d_state.getDisequalityList();
@@ -2270,9 +2268,18 @@ void CoreSolver::checkNormalFormsDeq()
     }
   }
 
-  if (!d_im.hasProcessed())
+  if (d_im.hasProcessed())
   {
-    d_state.separateByLength(d_strings_eqc, cols, lts);
+    // added splitting lemma above
+    return;
+  }
+  // otherwise, look at pairs of equivalence classes with equal lengths
+  std::map<TypeNode, std::vector<std::vector<Node> > > colsT;
+  std::map<TypeNode, std::vector<Node> > ltsT;
+  d_state.separateByLength(d_strings_eqc, colsT, ltsT);
+  for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& ct : colsT)
+  {
+    std::vector<std::vector<Node> >& cols = ct.second;
     for( unsigned i=0; i<cols.size(); i++ ){
       if (cols[i].size() > 1 && !d_im.hasPendingLemma())
       {
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 622e919f7..465b237ba 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -297,31 +297,39 @@ std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
   return d_valuation.entailmentCheck(mode, lit);
 }
 
-void SolverState::separateByLength(const std::vector<Node>& n,
-                                   std::vector<std::vector<Node> >& cols,
-                                   std::vector<Node>& lts)
+void SolverState::separateByLength(
+    const std::vector<Node>& n,
+    std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
+    std::map<TypeNode, std::vector<Node>>& lts)
 {
   unsigned leqc_counter = 0;
-  std::map<Node, unsigned> eqc_to_leqc;
-  std::map<unsigned, Node> leqc_to_eqc;
+  // map (length, type) to an equivalence class identifier
+  std::map<std::pair<Node, TypeNode>, unsigned> eqc_to_leqc;
+  // backwards map
+  std::map<unsigned, std::pair<Node, TypeNode>> leqc_to_eqc;
+  // Collection of eqc for each identifier. Notice that some identifiers may
+  // not have an associated length in the mappings above, if the length of
+  // an equivalence class is unknown.
   std::map<unsigned, std::vector<Node> > eqc_to_strings;
   NodeManager* nm = NodeManager::currentNM();
   for (const Node& eqc : n)
   {
     Assert(d_ee.getRepresentative(eqc) == eqc);
+    TypeNode tnEqc = eqc.getType();
     EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
     Node lt = ei ? ei->d_lengthTerm : Node::null();
     if (!lt.isNull())
     {
       lt = nm->mkNode(STRING_LENGTH, lt);
       Node r = d_ee.getRepresentative(lt);
-      if (eqc_to_leqc.find(r) == eqc_to_leqc.end())
+      std::pair<Node, TypeNode> lkey(r, tnEqc);
+      if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
       {
-        eqc_to_leqc[r] = leqc_counter;
-        leqc_to_eqc[leqc_counter] = r;
+        eqc_to_leqc[lkey] = leqc_counter;
+        leqc_to_eqc[leqc_counter] = lkey;
         leqc_counter++;
       }
-      eqc_to_strings[eqc_to_leqc[r]].push_back(eqc);
+      eqc_to_strings[eqc_to_leqc[lkey]].push_back(eqc);
     }
     else
     {
@@ -331,9 +339,11 @@ void SolverState::separateByLength(const std::vector<Node>& n,
   }
   for (const std::pair<const unsigned, std::vector<Node> >& p : eqc_to_strings)
   {
-    cols.push_back(std::vector<Node>());
-    cols.back().insert(cols.back().end(), p.second.begin(), p.second.end());
-    lts.push_back(leqc_to_eqc[p.first]);
+    Assert(!p.second.empty());
+    // get the type of the collection
+    TypeNode stn = p.second[0].getType();
+    cols[stn].emplace_back(p.second.begin(), p.second.end());
+    lts[stn].push_back(leqc_to_eqc[p.first].first);
   }
 }
 
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index d43c600f4..5db3a3707 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -171,11 +171,14 @@ class SolverState
    *
    * Separate the string representatives in argument n into a partition cols
    * whose collections have equal length. The i^th vector in cols has length
-   * lts[i] for all elements in col.
+   * lts[i] for all elements in col. These vectors are furthmore separated
+   * by string-like type.
    */
-  void separateByLength(const std::vector<Node>& n,
-                        std::vector<std::vector<Node> >& cols,
-                        std::vector<Node>& lts);
+  void separateByLength(
+      const std::vector<Node>& n,
+      std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
+      std::map<TypeNode, std::vector<Node>>& lts);
+
  private:
   /** Common constants */
   Node d_zero;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d83d5ca49..5ac8b8f7e 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -108,6 +108,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
   d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
   d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE);
+  d_equalityEngine.addFunctionKind(kind::SEQ_UNIT);
 
   // extended functions
   d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
@@ -296,7 +297,14 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
                        std::unordered_set<Node, NodeHashFunction> >& rst :
        repSet)
   {
-    if (!collectModelInfoType(rst.first, rst.second, m))
+    // get partition of strings of equal lengths, per type
+    std::map<TypeNode, std::vector<std::vector<Node> > > colT;
+    std::map<TypeNode, std::vector<Node> > ltsT;
+    std::vector<Node> repVec(rst.second.begin(), rst.second.end());
+    d_state.separateByLength(repVec, colT, ltsT);
+    // now collect model info for the type
+    TypeNode st = rst.first;
+    if (!collectModelInfoType(st, rst.second, colT[st], ltsT[st], m))
     {
       return false;
     }
@@ -307,14 +315,12 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
 bool TheoryStrings::collectModelInfoType(
     TypeNode tn,
     const std::unordered_set<Node, NodeHashFunction>& repSet,
+    std::vector<std::vector<Node> >& col,
+    std::vector<Node>& lts,
     TheoryModel* m)
 {
   NodeManager* nm = NodeManager::currentNM();
-  std::vector<Node> nodes(repSet.begin(), repSet.end());
   std::map< Node, Node > processed;
-  std::vector< std::vector< Node > > col;
-  std::vector< Node > lts;
-  d_state.separateByLength(nodes, col, lts);
   //step 1 : get all values for known lengths
   std::vector< Node > lts_values;
   std::map<unsigned, Node> values_used;
@@ -445,7 +451,7 @@ bool TheoryStrings::collectModelInfoType(
       }
       else
       {
-        Unimplemented() << "Collect model info not implemented for type " << tn;
+        sel.reset(new SeqEnumLen(tn, nullptr, currLen, currLen));
       }
       for (const Node& eqc : pure_eq)
       {
@@ -521,13 +527,15 @@ bool TheoryStrings::collectModelInfoType(
   }
   Trace("strings-model") << "String Model : Pure Assigned." << std::endl;
   //step 4 : assign constants to all other equivalence classes
-  for( unsigned i=0; i<nodes.size(); i++ ){
-    if( processed.find( nodes[i] )==processed.end() ){
-      NormalForm& nf = d_csolver->getNormalForm(nodes[i]);
+  for (const Node& rn : repSet)
+  {
+    if (processed.find(rn) == processed.end())
+    {
+      NormalForm& nf = d_csolver->getNormalForm(rn);
       if (Trace.isOn("strings-model"))
       {
         Trace("strings-model")
-            << "Construct model for " << nodes[i] << " based on normal form ";
+            << "Construct model for " << rn << " based on normal form ";
         for (unsigned j = 0, size = nf.d_nf.size(); j < size; j++)
         {
           Node n = nf.d_nf[j];
@@ -553,9 +561,10 @@ bool TheoryStrings::collectModelInfoType(
       }
       Node cc = utils::mkNConcat(nc, tn);
       Assert(cc.isConst());
-      Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
-      processed[nodes[i]] = cc;
-      if (!m->assertEquality(nodes[i], cc, true))
+      Trace("strings-model")
+          << "*** Determined constant " << cc << " for " << rn << std::endl;
+      processed[rn] = cc;
+      if (!m->assertEquality(rn, cc, true))
       {
         // this should never happen due to the model soundness argument
         // for strings
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 7c99b6968..6468f1d3a 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -281,13 +281,17 @@ class TheoryStrings : public Theory {
   /** Collect model info for type tn
    *
    * Assigns model values (in m) to all relevant terms of the string-like type
-   * tn in the current context, which are stored in repSet.
+   * tn in the current context, which are stored in repSet. Furthermore,
+   * col is a partition of repSet where equivalence classes are grouped into
+   * sets having equal length, where these lengths are stored in lts.
    *
    * Returns false if a conflict is discovered while doing this assignment.
    */
   bool collectModelInfoType(
       TypeNode tn,
       const std::unordered_set<Node, NodeHashFunction>& repSet,
+      std::vector<std::vector<Node> >& col,
+      std::vector<Node>& lts,
       TheoryModel* m);
 
   /** assert pending fact