diff options
Diffstat (limited to 'src/theory/quantifiers/alpha_equivalence.cpp')
-rwxr-xr-x | src/theory/quantifiers/alpha_equivalence.cpp | 78 |
1 files changed, 39 insertions, 39 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index e4dcccdff..84bf2ec14 100755 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -29,54 +29,54 @@ struct sortTypeOrder { } }; -bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { - if( tt.size()==arg_index.size()+1 ){ - Node t = tt.back(); - Node op = t.hasOperator() ? t.getOperator() : t; - arg_index.push_back( 0 ); - Trace("aeq-debug") << op << " "; - return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index ); - }else if( tt.empty() ){ - //we are finished - Trace("aeq-debug") << std::endl; - if( d_quant.isNull() ){ - d_quant = q; - return true; +bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { + while( !tt.empty() ){ + if( tt.size()==arg_index.size()+1 ){ + Node t = tt.back(); + Node op = t.hasOperator() ? t.getOperator() : t; + arg_index.push_back( 0 ); + Trace("aeq-debug") << op << " "; + aen = &(aen->d_children[op][t.getNumChildren()]); }else{ - //lemma ( q <=> d_quant ) - Trace("alpha-eq") << "Alpha equivalent : " << std::endl; - Trace("alpha-eq") << " " << q << std::endl; - Trace("alpha-eq") << " " << d_quant << std::endl; - qe->getOutputChannel().lemma( q.iffNode( d_quant ) ); - return false; + Node t = tt.back(); + int i = arg_index.back(); + if( i==(int)t.getNumChildren() ){ + tt.pop_back(); + arg_index.pop_back(); + }else{ + tt.push_back( t[i] ); + arg_index[arg_index.size()-1]++; + } } + } + Trace("aeq-debug") << std::endl; + if( aen->d_quant.isNull() ){ + aen->d_quant = q; + return true; }else{ - Node t = tt.back(); - int i = arg_index.back(); - if( i==(int)t.getNumChildren() ){ - tt.pop_back(); - arg_index.pop_back(); - }else{ - tt.push_back( t[i] ); - arg_index[arg_index.size()-1]++; - } - return registerNode( qe, q, tt, arg_index ); + //lemma ( q <=> d_quant ) + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << aen->d_quant << std::endl; + qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); + return false; } } -bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ - if( index==(int)typs.size() ){ - std::vector< Node > tt; - std::vector< int > arg_index; - tt.push_back( t ); - Trace("aeq-debug") << " : "; - return d_data.registerNode( qe, q, tt, arg_index ); - }else{ +bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn, + QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ + while( index<(int)typs.size() ){ TypeNode curr = typs[index]; Assert( typ_count.find( curr )!=typ_count.end() ); Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] "; - return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 ); + aetn = &(aetn->d_children[curr][typ_count[curr]]); + index = index + 1; } + std::vector< Node > tt; + std::vector< int > arg_index; + tt.push_back( t ); + Trace("aeq-debug") << " : "; + return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index ); } bool AlphaEquivalence::registerQuantifier( Node q ) { @@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) { sto.d_tdb = d_qe->getTermDatabase(); std::sort( typs.begin(), typs.end(), sto ); Trace("aeq-debug") << " "; - bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count ); + bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); Trace("aeq") << " ...result : " << ret << std::endl; return ret; } |