diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-17 14:38:07 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-17 12:38:07 -0700 |
| commit | c90b5b15ca93e64683c2bbf85def8d7afb4edab8 (patch) | |
| tree | 725385999cf96340d7d70adb1845f8f2ce817461 /src/theory/strings/theory_strings.h | |
| parent | fc07d6af4156fde8af048ca5db8ff1f43de48ebc (diff) | |
Make strings model construction robust to lengths that are not propagated equal (#2444)
This fixes #2429.
This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment.
We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.
Regardless, the strings model construction should be robust to handle this case, which this PR does.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 5bc6b019f..77dae0cf3 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -578,8 +578,18 @@ private: /** get concat vector */ void getConcatVec(Node n, std::vector<Node>& c); - // get equivalence classes + /** get equivalence classes + * + * This adds the representative of all equivalence classes to eqcs + */ void getEquivalenceClasses(std::vector<Node>& eqcs); + /** get relevant equivalence classes + * + * This adds the representative of all equivalence classes that contain at + * least one term in termSet. + */ + void getRelevantEquivalenceClasses(std::vector<Node>& eqcs, + std::set<Node>& termSet); // separate into collections with equal length void separateByLength(std::vector<Node>& n, |