diff options
author | Tim King <taking@cs.nyu.edu> | 2018-02-05 15:17:45 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-05 17:17:45 -0600 |
commit | 66a7932c7d4bd986665a041293ed23f8f58570f4 (patch) | |
tree | a69141491694be5653d1708884aa42b3ff138926 /src/theory/rep_set.cpp | |
parent | b458d1768202f7f9e117693b83985794665f73e2 (diff) |
Cleaning up the printing of theory model representative sets. (#1538)
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index bff5e36cd..04c39c897 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -43,12 +43,8 @@ bool RepSet::hasRep(TypeNode tn, Node n) const unsigned RepSet::getNumRepresentatives(TypeNode tn) const { - std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn ); - if( it!=d_type_reps.end() ){ - return it->second.size(); - }else{ - return 0; - } + const std::vector<Node>* reps = getTypeRepsOrNull(tn); + return (reps != nullptr) ? reps->size() : 0; } Node RepSet::getRepresentative(TypeNode tn, unsigned i) const @@ -60,14 +56,18 @@ Node RepSet::getRepresentative(TypeNode tn, unsigned i) const return it->second[i]; } -void RepSet::getRepresentatives(TypeNode tn, std::vector<Node>& reps) const +const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const { - std::map<TypeNode, std::vector<Node> >::const_iterator it = - d_type_reps.find(tn); - Assert(it != d_type_reps.end()); - reps.insert(reps.end(), it->second.begin(), it->second.end()); + auto it = d_type_reps.find(tn); + if (it == d_type_reps.end()) + { + return nullptr; + } + return &(it->second); } +namespace { + bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache) { if( std::find( cache.begin(), cache.end(), n )==cache.end() ){ @@ -85,6 +85,8 @@ bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache) return false; } +} // namespace + void RepSet::add( TypeNode tn, Node n ){ //for now, do not add array constants FIXME if( tn.isArray() ){ @@ -264,7 +266,12 @@ bool RepSetIterator::initialize() if (d_rs->hasType(tn)) { d_enum_type.push_back( ENUM_DEFAULT ); - d_rs->getRepresentatives(tn, d_domain_elements[v]); + if (const auto* type_reps = d_rs->getTypeRepsOrNull(tn)) + { + std::vector<Node>& v_domain_elements = d_domain_elements[v]; + v_domain_elements.insert(v_domain_elements.end(), + type_reps->begin(), type_reps->end()); + } }else{ Assert( d_incomplete ); return false; |