diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
commit | 1c779966545190efa59b019572237562eea66dbf (patch) | |
tree | f827fe0e4bcbbca8c84174f815948b3212391423 /src/theory/quantifiers/term_database.cpp | |
parent | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (diff) |
more minor updates to inst gen and representative selection, clean up of equality query
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 55 |
1 files changed, 38 insertions, 17 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d637fa25f..591270ab0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -161,27 +161,29 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } for( int i=0; i<2; i++ ){ Node n = NodeManager::currentNM()->mkConst( i==1 ); - eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ), - d_quantEngine->getEqualityQuery()->getEngine() ); - while( !eqc.isFinished() ){ - Node en = (*eqc); - computeModelBasisArgAttribute( en ); - if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ - if( !en.getAttribute(NoMatchAttribute()) ){ - Node op = en.getOperator(); - if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ - NoMatchAttribute nma; - en.setAttribute(nma,true); - congruentCount++; + if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ), + d_quantEngine->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + computeModelBasisArgAttribute( en ); + if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ + if( !en.getAttribute(NoMatchAttribute()) ){ + Node op = en.getOperator(); + if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ + NoMatchAttribute nma; + en.setAttribute(nma,true); + congruentCount++; + }else{ + nonCongruentCount++; + d_op_count[ op ]++; + } }else{ - nonCongruentCount++; - d_op_count[ op ]++; + alreadyCongruentCount++; } - }else{ - alreadyCongruentCount++; } + ++eqc; } - ++eqc; } } Debug("term-db-cong") << "TermDb: Reset" << std::endl; @@ -300,6 +302,25 @@ void TermDb::setInstantiationConstantAttr( Node n, Node f ){ } } +/** get the i^th instantiation constant of f */ +Node TermDb::getInstantiationConstant( Node f, int i ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); + if( it!=d_inst_constants.end() ){ + return it->second[i]; + }else{ + return Node::null(); + } +} + +/** get number of instantiation constants for f */ +int TermDb::getNumInstantiationConstants( Node f ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); + if( it!=d_inst_constants.end() ){ + return (int)it->second.size(); + }else{ + return 0; + } +} Node TermDb::getInstConstantBody( Node f ){ std::map< Node, Node >::iterator it = d_inst_const_body.find( f ); |