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/rep_set.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/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 66 |
1 files changed, 59 insertions, 7 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 303e65eff..dd139d5ec 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -12,6 +12,8 @@ ** \brief Implementation of representative set **/ +#include <unordered_set> + #include "theory/rep_set.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" @@ -31,8 +33,10 @@ void RepSet::clear(){ d_values_to_terms.clear(); } -bool RepSet::hasRep( TypeNode tn, Node n ) { - std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn ); +bool RepSet::hasRep(TypeNode tn, Node n) const +{ + std::map<TypeNode, std::vector<Node> >::const_iterator it = + d_type_reps.find(tn); if( it==d_type_reps.end() ){ return false; }else{ @@ -40,18 +44,29 @@ bool RepSet::hasRep( TypeNode tn, Node n ) { } } -int RepSet::getNumRepresentatives( TypeNode tn ) 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 (int)it->second.size(); + return it->second.size(); }else{ return 0; } } -bool containsStoreAll( Node n, std::vector< Node >& cache ){ +Node RepSet::getRepresentative(TypeNode tn, unsigned i) const +{ + std::map<TypeNode, std::vector<Node> >::const_iterator it = + d_type_reps.find(tn); + Assert(it != d_type_reps.end()); + Assert(i < it->second.size()); + return it->second[i]; +} + +bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache) +{ if( std::find( cache.begin(), cache.end(), n )==cache.end() ){ - cache.push_back( n ); + cache.insert(n); if( n.getKind()==STORE_ALL ){ return true; }else{ @@ -68,7 +83,7 @@ bool containsStoreAll( Node n, std::vector< Node >& cache ){ void RepSet::add( TypeNode tn, Node n ){ //for now, do not add array constants FIXME if( tn.isArray() ){ - std::vector< Node > cache; + std::unordered_set<Node, NodeHashFunction> cache; if( containsStoreAll( n, cache ) ){ return; } @@ -116,6 +131,43 @@ bool RepSet::complete( TypeNode t ){ } } +Node RepSet::getTermForRepresentative(Node n) const +{ + std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n); + if (it != d_values_to_terms.end()) + { + return it->second; + } + else + { + return Node::null(); + } +} + +void RepSet::setTermForRepresentative(Node n, Node t) +{ + d_values_to_terms[n] = t; +} + +Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const +{ + std::map<TypeNode, std::vector<Node> >::const_iterator it = + d_type_reps.find(tn); + if (it != d_type_reps.end()) + { + // try to find a pre-existing arbitrary element + for (size_t i = 0; i < it->second.size(); i++) + { + if (std::find(exclude.begin(), exclude.end(), it->second[i]) + == exclude.end()) + { + return it->second[i]; + } + } + } + return Node::null(); +} + void RepSet::toStream(std::ostream& out){ for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ if( !it->first.isFunction() && !it->first.isPredicate() ){ |