Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.

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() ){