diff options
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 95 |
1 files changed, 33 insertions, 62 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 4167c3ad9..fdb64f6b0 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -281,61 +281,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { } Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { - Assert( !tn.isNull() ); - while( d_free_var[tn].size()<=i ){ - std::stringstream oss; - oss << tn; - std::string typ_name = oss.str(); - while( typ_name[0]=='(' ){ - typ_name.erase( typ_name.begin() ); - } - std::stringstream os; - os << typ_name[0] << i; - Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn ); - d_free_var_num[x] = d_free_var[tn].size(); - d_free_var[tn].push_back( x ); - } - return d_free_var[tn][i]; -} - - - -Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) { - if( n.getKind()==BOUND_VARIABLE ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it==subs.end() ){ - TypeNode tn = n.getType(); - //allocate variable - unsigned vn = var_count[tn]; - var_count[tn]++; - subs[n] = getFreeVar( tn, vn ); - return subs[n]; - }else{ - return it->second; - } - }else{ - std::vector< Node > children; - if( n.getKind()!=EQUAL ){ - if( n.hasOperator() ){ - TNode op = n.getOperator(); - if( !d_tge.isRelevantFunc( op ) ){ - return Node::null(); - } - children.push_back( op ); - }else{ - return Node::null(); - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node cn = getCanonicalTerm( n[i], var_count, subs ); - if( cn.isNull() ){ - return Node::null(); - }else{ - children.push_back( cn ); - } - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } + return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i ); } bool ConjectureGenerator::isHandledTerm( TNode n ){ @@ -555,11 +501,14 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { TNode nr = q[1][r==0 ? 1 : 0]; Node eq = nl.eqNode( nr ); if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){ - //must make it canonical - std::map< TypeNode, unsigned > var_count; - std::map< TNode, TNode > subs; - Trace("sg-proc-debug") << "get canonical " << eq << std::endl; - eq = getCanonicalTerm( eq, var_count, subs ); + //check if it contains only relevant functions + if( d_tge.isRelevantTerm( eq ) ){ + //make it canonical + Trace("sg-proc-debug") << "get canonical " << eq << std::endl; + eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq ); + }else{ + eq = Node::null(); + } } if( !eq.isNull() ){ if( r==0 ){ @@ -697,7 +646,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { typ_to_subs_index[it->first] = sum; sum += it->second; for( unsigned i=0; i<it->second; i++ ){ - gsubs_vars.push_back( getFreeVar( it->first, i ) ); + gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) ); } } } @@ -993,7 +942,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< }else{ //check for max/min TypeNode tn = pat.getType(); - unsigned vn = d_free_var_num[pat]; + unsigned vn = pat.getAttribute(InstVarNumAttribute()); std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn ); if( it!=mnvn.end() ){ if( vn<it->second ){ @@ -2012,6 +1961,28 @@ bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){ bool TermGenEnv::isRelevantFunc( Node f ) { return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end(); } + +bool TermGenEnv::isRelevantTerm( Node t ) { + if( t.getKind()!=BOUND_VARIABLE ){ + if( t.getKind()!=EQUAL ){ + if( t.hasOperator() ){ + TNode op = t.getOperator(); + if( !isRelevantFunc( op ) ){ + return false; + } + }else{ + return false; + } + } + for( unsigned i=0; i<t.getNumChildren(); i++ ){ + if( !isRelevantTerm( t[i] ) ){ + return false; + } + } + } + return true; +} + TermDb * TermGenEnv::getTermDatabase() { return d_cg->getTermDatabase(); } |