diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 64965f5ce..36859ddaa 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -48,6 +48,14 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ } } +void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { + for( std::map< Node, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + for( unsigned i=0; i<depth; i++ ){ Debug(c) << " "; } + Debug(c) << it->first << std::endl; + it->second.debugPrint( c, n, depth+1 ); + } +} + TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { } @@ -204,6 +212,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Debug("term-db-cong") << "TermDb: Reset" << std::endl; Debug("term-db-cong") << "Congruent/Non-Congruent = "; Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl; + if( Debug.isOn("term-db") ){ + Debug("term-db") << "functions : " << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ + if( it->second.size()>0 ){ + Debug("term-db") << "- " << it->first << std::endl; + d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]); + } + } + } } Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ |