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.

1 files changed, 22 insertions, 13 deletions

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