diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-03 17:52:07 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-03 17:52:07 +0000 |
commit | 5d9670acc3c8eacdebdbb07302a8e35f837d0e52 (patch) | |
tree | df7d6705a1af799db88445feba5cc1b77750eb6f /src | |
parent | 3c4935c7c0c6774588af94c82307a960e58a1154 (diff) |
minor cleanup leftover from fmf-devel
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_engine.cpp | 28 |
1 files changed, 0 insertions, 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)) { |