diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-09 14:32:32 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-09 12:32:32 -0800 |
| commit | 33c5eb093a7f032a7d9c9263da595eb53fdd223b (patch) | |
| tree | a08a2ab95bb8e09b6be768b18b99346c48488dec /src/theory/rep_set.cpp | |
| parent | b6ce0f23ce0aaa0552767e8067fe58dbceee11cb (diff) | |
Fix case of uninterpreted constant instantiation in FMF (#3543)
Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).
Diffstat (limited to 'src/theory/rep_set.cpp')
| -rw-r--r-- | src/theory/rep_set.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index ea462e55c..d293890bf 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -201,6 +201,8 @@ unsigned RepSetIterator::domainSize(unsigned i) return d_domain_elements[v].size(); } +TypeNode RepSetIterator::getTypeOf(unsigned i) const { return d_types[i]; } + bool RepSetIterator::setQuantifier(Node q) { Trace("rsi") << "Make rsi for quantified formula " << q << std::endl; @@ -403,14 +405,16 @@ int RepSetIterator::increment(){ bool RepSetIterator::isFinished() const { return d_index.empty(); } -Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm) const +Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const { - unsigned ii = d_index_order[v]; + unsigned ii = d_index_order[i]; unsigned curr = d_index[ii]; - Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl; - Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl; - Assert(0 <= curr && curr < d_domain_elements[v].size()); - Node t = d_domain_elements[v][curr]; + Trace("rsi-debug") << "rsi : get term " << i + << ", index order = " << d_index_order[i] << std::endl; + Trace("rsi-debug") << "rsi : curr = " << curr << " / " + << d_domain_elements[i].size() << std::endl; + Assert(0 <= curr && curr < d_domain_elements[i].size()); + Node t = d_domain_elements[i][curr]; if (valTerm) { Node tt = d_rs->getTermForRepresentative(t); |