Fix and refactor TheoryStrings::checkFlatForms() (#3326)

This commit fixes some minor (performance) issues in
`TheoryStrings::checkFlatForms()`: The `inelig` vector was initialized
with copies of the `start` element instead of all the elements before
`start` and the `else` branch of `count == asize` was looping over all
elements from `1` instead of `start + 1`. Additionally, this commit
refactors the code to be a bit more readable.

1 files changed, 4 insertions, 3 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 9db40f8fe..54ea0d158 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -453,10 +453,11 @@ private:
   /**
    * This checks whether there are flat form inferences between eqc[start] and
    * eqc[j] for some j>start. If the flag isRev is true, we check for flat form
-   * interferences in the reverse direction of the flat forms. For more details,
-   * see checkFlatForms below.
+   * interferences in the reverse direction of the flat forms (note:
+   * `d_flat_form` and `d_flat_form_index` must be in reverse order if `isRev`
+   * is true). For more details, see checkFlatForms below.
    */
-  void checkFlatForm(std::vector<Node>& eqc, unsigned start, bool isRev);
+  void checkFlatForm(std::vector<Node>& eqc, size_t start, bool isRev);
   //--------------------------end for checkFlatForm
 
   //--------------------------for checkCycles