From 5d9670acc3c8eacdebdbb07302a8e35f837d0e52 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 3 Sep 2012 17:52:07 +0000 Subject: [PATCH] minor cleanup leftover from fmf-devel --- src/theory/theory_engine.cpp | 28 ---------------------------- 1 file changed, 28 deletions(-) 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)) { -- 2.30.2