minor cleanup leftover from fmf-devel

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6dbabfe4df43ed3d064f6d0da8b676b8496d8710..b0a290b7d35936e8b12366dde93f6a3b6db3b6f7 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -42,10 +42,6 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 
-//hack
-#include "theory/arith/options.h"
-#include "theory/uf/options.h"
-
 
 using namespace std;
 
@@ -149,30 +145,6 @@ void TheoryEngine::preRegister(TNode preprocessed) {
   }
 }
 
-void collectGroundTerms( Node n, std::vector< Node >& defineFuns,
-                         std::vector< Node >& groundTerms ){
-  if( std::find( groundTerms.begin(), groundTerms.end(), n )==groundTerms.end() ){
-    groundTerms.push_back( n );
-    if( n.getKind()==kind::APPLY_UF ){
-      if( std::find( defineFuns.begin(), defineFuns.end(), n.getOperator() )==defineFuns.end() ){
-        defineFuns.push_back( n.getOperator() );
-      }
-    }else if( n.getNumChildren()==0 ){
-      if( std::find( defineFuns.begin(), defineFuns.end(), n )==defineFuns.end() ){
-        defineFuns.push_back( n );
-      }
-    }
-    if( n.getKind()==kind::FORALL ){
-      std::cout << "Bad ground assertion : " << n << std::endl;
-      std::cout << "...possible nested quantifiers?" << std::endl;
-      exit( -1 );
-    }
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      collectGroundTerms( n[i], defineFuns, groundTerms );
-    }
-  }
-}
-
 void TheoryEngine::printAssertions(const char* tag) {
   if (Trace.isOn(tag)) {