From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Sep 2012 17:52:07 +0000 (+0000)
Subject: minor cleanup leftover from fmf-devel
X-Git-Tag: cvc5-1.0.0~7830
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5d9670acc3c8eacdebdbb07302a8e35f837d0e52;p=cvc5.git

minor cleanup leftover from fmf-devel
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6dbabfe4d..b0a290b7d 100644
--- 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)) {