Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf-fun-rlv, fixes bug 723.

1 files changed, 0 insertions, 10 deletions

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 86bcb2cac..a2797dd8d 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -29,7 +29,6 @@ void RepSet::clear(){
   d_type_complete.clear();
   d_tmap.clear();
   d_values_to_terms.clear();
-  d_type_rlv_rep.clear();
 }
 
 bool RepSet::hasRep( TypeNode tn, Node n ) {
@@ -117,15 +116,6 @@ bool RepSet::complete( TypeNode t ){
   }
 }
 
-int RepSet::getNumRelevantGroundReps( TypeNode t ) {
-  std::map< TypeNode, int >::iterator it = d_type_rlv_rep.find( t );
-  if( it==d_type_rlv_rep.end() ){
-    return 0;
-  }else{
-    return it->second;
-  }
-}
-
 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() ){