diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 64 |
1 files changed, 48 insertions, 16 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3d3646d7d..ef301c2cf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -78,8 +78,8 @@ TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argInd void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { for( std::map< TNode, 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; + for( unsigned i=0; i<depth; i++ ){ Trace(c) << " "; } + Trace(c) << it->first << std::endl; it->second.debugPrint( c, n, depth+1 ); } } @@ -111,6 +111,20 @@ Node TermDb::getGroundTerm( Node f, unsigned i ) { return d_op_map[f][i]; } +unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) { + std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn ); + if( it!=d_type_map.end() ){ + return it->second.size(); + }else{ + return 0; + } +} + +Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) { + Assert( i<d_type_map[tn].size() ); + return d_type_map[tn][i]; +} + Node TermDb::getMatchOperator( Node n ) { //return n.getOperator(); Kind k = n.getKind(); @@ -205,6 +219,21 @@ void TermDb::computeUfEqcTerms( TNode f ) { } } +bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { + Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r ); + std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); + if( it != d_func_map_rel_dom.end() ){ + std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i ); + if( it2!=it->second.end() ){ + return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end(); + }else{ + return false; + } + }else{ + return false; + } +} + //return a term n' equivalent to n // maximal subterms of n' are representatives in the equality engine qy Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) { @@ -533,6 +562,7 @@ bool TermDb::reset( Theory::Effort effort ){ d_arg_reps.clear(); d_func_map_trie.clear(); d_func_map_eqc_trie.clear(); + d_func_map_rel_dom.clear(); d_consistent_ee = true; eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); @@ -596,16 +626,18 @@ bool TermDb::reset( Theory::Effort effort ){ } computeArgReps( n ); - if( Trace.isOn("term-db-debug") ){ - Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; - for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){ - Trace("term-db-debug") << d_arg_reps[n][i] << " "; - } - Trace("term-db-debug") << std::endl; - if( ee->hasTerm( n ) ){ - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; + Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; + for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){ + Trace("term-db-debug") << d_arg_reps[n][i] << " "; + if( std::find( d_func_map_rel_dom[it->first][i].begin(), + d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){ + d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] ); } } + Trace("term-db-debug") << std::endl; + if( ee->hasTerm( n ) ){ + Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; + } Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] ); if( at!=n && ee->areEqual( at, n ) ){ NoMatchAttribute nma; @@ -650,12 +682,12 @@ bool TermDb::reset( Theory::Effort effort ){ Trace("term-db-stats") << "TermDb: Reset" << std::endl; Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; - if( Debug.isOn("term-db") ){ - Debug("term-db") << "functions : " << std::endl; + if( Trace.isOn("term-db-index") ){ + Trace("term-db-index") << "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]); + Trace("term-db-index") << "- " << it->first << std::endl; + d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]); } } } @@ -929,10 +961,10 @@ Node TermDb::getInstantiationConstant( Node q, int i ) const { } /** get number of instantiation constants for q */ -int TermDb::getNumInstantiationConstants( Node q ) const { +unsigned TermDb::getNumInstantiationConstants( Node q ) const { std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); if( it!=d_inst_constants.end() ){ - return (int)it->second.size(); + return it->second.size(); }else{ return 0; } |