Compute model values for nested sequences in order (#6631)

Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.

While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.

This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.

cc @yoni206

5 files changed, 78 insertions, 25 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b1f5a0765..f4daed85d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -211,7 +211,10 @@ bool TheoryStrings::collectModelValues(TheoryModel* m,
     Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl;
   }
   Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl;
+  // Collects representatives by types and orders sequence types by how nested
+  // they are
   std::map<TypeNode, std::unordered_set<Node> > repSet;
+  std::unordered_set<TypeNode> toProcess;
   // Generate model
   // get the relevant string equivalence classes
   for (const Node& s : termSet)
@@ -221,31 +224,51 @@ bool TheoryStrings::collectModelValues(TheoryModel* m,
     {
       Node r = d_state.getRepresentative(s);
       repSet[tn].insert(r);
+      toProcess.insert(tn);
     }
   }
-  for (const std::pair<const TypeNode, std::unordered_set<Node> >& rst : repSet)
+
+  while (!toProcess.empty())
   {
-    // 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))
+    // Pick one of the remaining types to collect model values for
+    TypeNode tn = *toProcess.begin();
+    if (!collectModelInfoType(tn, toProcess, repSet, m))
     {
       return false;
     }
   }
+
   return true;
 }
 
-bool TheoryStrings::collectModelInfoType(TypeNode tn,
-                                         const std::unordered_set<Node>& repSet,
-                                         std::vector<std::vector<Node> >& col,
-                                         std::vector<Node>& lts,
-                                         TheoryModel* m)
+bool TheoryStrings::collectModelInfoType(
+    TypeNode tn,
+    std::unordered_set<TypeNode>& toProcess,
+    const std::map<TypeNode, std::unordered_set<Node> >& repSet,
+    TheoryModel* m)
 {
+  // Make sure that the model values for the element type of sequences are
+  // computed first
+  if (tn.isSequence() && tn.getSequenceElementType().isSequence())
+  {
+    TypeNode tnElem = tn.getSequenceElementType();
+    if (toProcess.find(tnElem) != toProcess.end()
+        && !collectModelInfoType(tnElem, toProcess, repSet, m))
+    {
+      return false;
+    }
+  }
+  toProcess.erase(tn);
+
+  // get partition of strings of equal lengths for the representatives of the
+  // current type
+  std::map<TypeNode, std::vector<std::vector<Node> > > colT;
+  std::map<TypeNode, std::vector<Node> > ltsT;
+  const std::vector<Node> repVec(repSet.at(tn).begin(), repSet.at(tn).end());
+  d_state.separateByLength(repVec, colT, ltsT);
+  const std::vector<std::vector<Node> >& col = colT[tn];
+  const std::vector<Node>& lts = ltsT[tn];
+
   NodeManager* nm = NodeManager::currentNM();
   std::map< Node, Node > processed;
   //step 1 : get all values for known lengths
@@ -322,7 +345,10 @@ bool TheoryStrings::collectModelInfoType(TypeNode tn,
             Node argVal;
             if (nfe.d_nf[0][0].getType().isStringLike())
             {
-              argVal = d_state.getRepresentative(nfe.d_nf[0][0]);
+              // By this point, we should have assigned model values for the
+              // elements of this sequence type because of the check in the
+              // beginning of this method
+              argVal = m->getRepresentative(nfe.d_nf[0][0]);
             }
             else
             {
@@ -479,7 +505,7 @@ bool TheoryStrings::collectModelInfoType(TypeNode tn,
   }
   Trace("strings-model") << "String Model : Pure Assigned." << std::endl;
   //step 4 : assign constants to all other equivalence classes
-  for (const Node& rn : repSet)
+  for (const Node& rn : repVec)
   {
     if (processed.find(rn) == processed.end())
     {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index a671129d4..fc5e47194 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -190,17 +190,19 @@ 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. Furthermore,
-   * col is a partition of repSet where equivalence classes are grouped into
-   * sets having equal length, where these lengths are stored in lts.
+   * tn in the current context, which are stored in repSet[tn].
    *
-   * Returns false if a conflict is discovered while doing this assignment.
+   * @param tn The type to compute model values for
+   * @param toProcess Remaining types to compute model values for
+   * @param repSet A map of types to the representatives of the equivalence
+   *               classes of the given type
+   * @return false if a conflict is discovered while doing this assignment.
    */
-  bool collectModelInfoType(TypeNode tn,
-                            const std::unordered_set<Node>& repSet,
-                            std::vector<std::vector<Node>>& col,
-                            std::vector<Node>& lts,
-                            TheoryModel* m);
+  bool collectModelInfoType(
+      TypeNode tn,
+      std::unordered_set<TypeNode>& toProcess,
+      const std::map<TypeNode, std::unordered_set<Node>>& repSet,
+      TheoryModel* m);
 
   /** assert pending fact
    *
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7de2d9789..cff39938c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -997,6 +997,8 @@ set(regress_0_tests
   regress0/seq/issue5543-unit-cmv.smt2
   regress0/seq/issue5547-seq-len-unit.smt2
   regress0/seq/issue5547-small-seq-len-unit.smt2
+  regress0/seq/issue5665-invalid-model.smt2
+  regress0/seq/issue6337-seq.smt2
   regress0/seq/len_simplify.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
diff --git a/test/regress/regress0/seq/issue5665-invalid-model.smt2 b/test/regress/regress0/seq/issue5665-invalid-model.smt2
new file mode 100644
index 000000000..5a4b1186d
--- /dev/null
+++ b/test/regress/regress0/seq/issue5665-invalid-model.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_SLIA)
+(declare-fun a () (Seq (Seq Int)))
+(declare-fun b () (Seq (Seq Int)))
+(declare-fun c () (Seq (Seq Int)))
+(declare-fun d () (Seq Int))
+(declare-fun e () Int)
+(declare-fun f () Int)
+(assert (= (seq.extract d e 1) (seq.unit f)))
+(assert (distinct a b (seq.++ (seq.unit d) c)))
+(set-info :status sat)
+(check-sat)
diff --git a/test/regress/regress0/seq/issue6337-seq.smt2 b/test/regress/regress0/seq/issue6337-seq.smt2
new file mode 100644
index 000000000..f6436f412
--- /dev/null
+++ b/test/regress/regress0/seq/issue6337-seq.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_SLIA)
+(declare-fun x () (Seq (Seq Int)))
+(declare-fun y () (Seq (Seq Int)))
+(declare-fun z () (Seq Int))
+(declare-fun w () (Seq Int))
+(declare-fun j () Int)
+(assert (= w (seq.unit j)))
+(assert (not (= x (seq.unit z))))
+(assert (not (= y (seq.unit w))))
+(assert (not (= x y)))
+(set-info :status sat)
+(check-sat)