diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 19 |
1 files changed, 1 insertions, 18 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 392fc269a..c35adef6a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -329,6 +329,7 @@ void TermDb::reset( Theory::Effort effort ){ if( !it->second.empty() ){ for( unsigned i=0; i<it->second.size(); i++ ){ Node n = it->second[i]; + //Assert( d_quantEngine->getEqualityQuery()->hasTerm( n ) ); computeModelBasisArgAttribute( n ); if( !n.getAttribute(NoMatchAttribute()) ){ computeArgReps( n ); @@ -794,24 +795,6 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){ return d_free_vars[tn]; } -const std::vector<Node> & TermDb::getParents(TNode n, TNode f, int arg){ - std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >,NodeHashFunction >,NodeHashFunction >::const_iterator - rn = d_parents.find( n ); - if( rn !=d_parents.end() ){ - std::hash_map< Node, std::hash_map< int, std::vector< Node > > , NodeHashFunction > ::const_iterator - rf = rn->second.find(f); - if( rf != rn->second.end() ){ - std::hash_map< int, std::vector< Node > > ::const_iterator - ra = rf->second.find(arg); - if( ra != rf->second.end() ){ - return ra->second; - } - } - } - static std::vector<Node> empty; - return empty; -} - void TermDb::computeVarContains( Node n ) { if( d_var_contains.find( n )==d_var_contains.end() ){ d_var_contains[n].clear(); |