diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-28 09:13:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-28 09:13:13 -0500 |
| commit | 34e84a25a044e3af192bb69089467c2125911900 (patch) | |
| tree | 924a3ae0894bfec136f91949a1bf55e19c4125da /src/theory/quantifiers/relevant_domain.cpp | |
| parent | 675e82e32a34911163f9de0e6389eb107be5b0f1 (diff) | |
Document term db (#1220)
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 749026b66..dcd24b433 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -98,6 +98,7 @@ bool RelevantDomain::reset( Theory::Effort e ) { return true; } +void RelevantDomain::registerQuantifier(Node q) {} void RelevantDomain::compute(){ if( !d_is_computed ){ d_is_computed = true; @@ -116,11 +117,12 @@ void RelevantDomain::compute(){ Trace("rel-dom-debug") << "account for ground terms" << std::endl; TermDb * db = d_qe->getTermDatabase(); - for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){ - Node op = it->first; + for (unsigned k = 0; k < db->getNumOperators(); k++) + { + Node op = db->getOperator(k); unsigned sz = db->getNumGroundTerms( op ); for( unsigned i=0; i<sz; i++ ){ - Node n = it->second[i]; + Node n = db->getGroundTerm(op, i); //if it is a non-redundant term if( db->isTermActive( n ) ){ for( unsigned j=0; j<n.getNumChildren(); j++ ){ |