diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-24 13:31:56 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-24 13:31:56 -0500 |
| commit | c99aa755bd62205b3f7381e6d67c7a1f2d37a3a2 (patch) | |
| tree | e6c16ea6babc4463dc2f4edae1b07855f3a219c2 /src/theory/inference_id.cpp | |
| parent | f493ea93e925e3ad9bfe0036e1d876d5600d5b30 (diff) | |
Add new eager conflict detection in strings for integer equivalence classes (#7453)
Required to address Zelkova bottlenecks.
This generalizes the methods for eager prefix/suffix conflicts for strings to do eager lower/upper bound conflicts for integer equivalence classes based on string-specific reasoning about length terms. This avoids cases where Simplex fails to show a concise conflict due to not having access to string reasoning (e.g. strings::ArithEntail) for arithmetic bounds.
The approach can still be improved by inferring fixed length for regular expression memberships, analogous to what is done for prefix/suffix conflicts.
It also changes EqcInfo to store (str.len x) instead of x for length terms.
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 28557e472..af753dd26 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -429,6 +429,8 @@ const char* toString(InferenceId i) case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS"; case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION"; case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT"; + case InferenceId::STRINGS_ARITH_BOUND_CONFLICT: + return "STRINGS_ARITH_BOUND_CONFLICT"; case InferenceId::STRINGS_REGISTER_TERM_ATOMIC: return "STRINGS_REGISTER_TERM_ATOMIC"; case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM"; |