diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-08 18:47:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-08 23:47:40 +0000 |
| commit | ccd52accc3bd19c5bc5203d091d1fc0f8d48f8a3 (patch) | |
| tree | f28b36f9194ccb0a43d37cc0e472f171f3645c15 /src/theory/rep_set.cpp | |
| parent | 0ec38bbddf9b9e37f4535a6c782f42e03f4593e0 (diff) | |
Fix for 2 dimensional dependent bounded quantifiers (#6710)
This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re.
Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635.
Diffstat (limited to 'src/theory/rep_set.cpp')
| -rw-r--r-- | src/theory/rep_set.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index d0eee1886..f6af5b680 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -429,14 +429,17 @@ Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const << d_domain_elements[i].size() << std::endl; Assert(0 <= curr && curr < d_domain_elements[i].size()); Node t = d_domain_elements[i][curr]; + Trace("rsi-debug") << "rsi : term = " << t << std::endl; if (valTerm) { Node tt = d_rs->getTermForRepresentative(t); if (!tt.isNull()) { + Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl; return tt; } } + Trace("rsi-debug") << "rsi : return" << std::endl; return t; } |