diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-01 11:58:57 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-01 11:58:57 -0700 |
commit | 86c541cdf83e0b98def5a479d1da966f2e959408 (patch) | |
tree | b8171b21b360c421582cdb25dde28641f746730b /src/theory/strings/theory_strings.h | |
parent | 4874e4f9566b5e536e6c66b559574d2df97e20ec (diff) |
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.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 7 |
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 |