diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-05 19:57:24 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-05 19:57:30 +0100 |
commit | 2b64e19e84787c7f510a2e7a536be563072e1c8e (patch) | |
tree | fcc7d8072951ab7ff2eef90c1b3b524c92cafa73 /src/theory/rep_set.cpp | |
parent | 7e8413ccb5a5f831b9814edd025d0c239b104d9f (diff) |
Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index ee14d6fc1..db0524034 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -28,6 +28,15 @@ void RepSet::clear(){ d_tmap.clear(); } +bool RepSet::hasRep( TypeNode tn, Node n ) { + std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn ); + if( it==d_type_reps.end() ){ + return false; + }else{ + return std::find( it->second.begin(), it->second.end(), n )!=it->second.end(); + } +} + int 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() ){ |