Split collect model info by types in strings (#3847)

Towards a theory of sequences.

We will need to do similar splits per type for most of the functions throughout strings.

1 files changed, 17 insertions, 5 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 79681a5f9..84c9e60c6 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -121,6 +121,11 @@ class TheoryStrings : public Theory {
                               std::vector<Node>& vars,
                               std::vector<Node>& subs,
                               std::map<Node, std::vector<Node> >& exp) override;
+  /**
+   * Get all relevant information in this theory regarding the current
+   * model. Return false if a contradiction is discovered.
+   */
+  bool collectModelInfo(TheoryModel* m) override;
 
   // NotifyClass for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
@@ -231,11 +236,6 @@ private:
 
   std::map< Node, Node > d_eqc_to_len_term;
 
-  /////////////////////////////////////////////////////////////////////////////
-  // MODEL GENERATION
-  /////////////////////////////////////////////////////////////////////////////
- public:
-  bool collectModelInfo(TheoryModel* m) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // NOTIFICATIONS
@@ -298,6 +298,18 @@ private:
    */
   bool areCareDisequal(TNode x, TNode y);
 
+  /** 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.
+   *
+   * Returns false if a conflict is discovered while doing this assignment.
+   */
+  bool collectModelInfoType(
+      TypeNode tn,
+      const std::unordered_set<Node, NodeHashFunction>& repSet,
+      TheoryModel* m);
+
   /** assert pending fact
    *
    * This asserts atom with polarity to the equality engine of this class,