diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 11:20:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-27 11:20:50 -0500 |
| commit | 079ed9540d498bcbb58f2f0fbe87bdae28101d1e (patch) | |
| tree | 8c3ba1818dc515c1714b23555460a3a39192acc5 /src/theory/quantifiers/equality_query.cpp | |
| parent | 03cc40cc070df0bc11c1556cef3016f784a95d23 (diff) | |
Refactor theory model (#1236)
* Refactor theory model, working on making RepSet references const.
* Encapsulation of members of rep set.
* More documentation on rep set.
* Swap names
* Reference issues.
* Minor
* Minor
* New clang format.
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
| -rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 4acc3e6b8..fb8ac4195 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -123,9 +123,10 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ //map back from values assigned by model, if any if( d_qe->getModel() ){ - std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); - if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){ - r = it->second; + Node tr = d_qe->getModel()->getRepSet()->getTermForRepresentative(r); + if (!tr.isNull()) + { + r = tr; r = getRepresentative( r ); }else{ if( r.getType().isSort() ){ |