diff options
Diffstat (limited to 'src/theory/quantifiers/anti_skolem.cpp')
-rw-r--r-- | src/theory/quantifiers/anti_skolem.cpp | 38 |
1 files changed, 27 insertions, 11 deletions
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 681c168f2..1303b7627 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -116,9 +116,15 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) } if( success ){ //sort the argument variables - d_ask_types[q].insert( d_ask_types[q].end(), d_quant_sip[q].d_arg_types.begin(), d_quant_sip[q].d_arg_types.end() ); + std::vector<Node> sivars; + d_quant_sip[q].getSingleInvocationVariables(sivars); + for (const Node& v : sivars) + { + d_ask_types[q].push_back(v.getType()); + } std::map< TypeNode, std::vector< unsigned > > indices; - for( unsigned j=0; j<d_ask_types[q].size(); j++ ){ + for (unsigned j = 0, size = d_ask_types[q].size(); j < size; j++) + { indices[d_ask_types[q][j]].push_back( j ); } sortTypeOrder sto; @@ -165,8 +171,10 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool for( unsigned i=0; i<quants.size(); i++ ){ Node q = quants[i]; std::vector< int > eqcs; - for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){ - Node f = it->first; + std::vector<Node> funcs; + d_quant_sip[q].getFunctions(funcs); + for (const Node& f : funcs) + { std::map< Node, int >::iterator itf = func_to_eqc.find( f ); if( itf == func_to_eqc.end() ){ if( eqcs.empty() ){ @@ -222,7 +230,8 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool std::vector< Node > outer_vars; std::vector< Node > inner_vars; Node q = quants[0]; - for( unsigned i=0; i<d_ask_types[q].size(); i++ ){ + for (unsigned i = 0, size = d_ask_types[q].size(); i < size; i++) + { Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] ); Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl; outer_vars.push_back( v ); @@ -237,15 +246,22 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool std::vector< Node > subs_rhs; //get outer variable substitution Assert( d_ask_types_index[q].size()==d_ask_types[q].size() ); - for( unsigned j=0; j<d_ask_types_index[q].size(); j++ ){ - Trace("anti-sk-debug") << " o_subs : " << d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] << " -> " << outer_vars[j] << std::endl; - subs_lhs.push_back( d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] ); + std::vector<Node> sivars; + d_quant_sip[q].getSingleInvocationVariables(sivars); + for (unsigned j = 0, size = d_ask_types_index[q].size(); j < size; j++) + { + Trace("anti-sk-debug") + << " o_subs : " << sivars[d_ask_types_index[q][j]] << " -> " + << outer_vars[j] << std::endl; + subs_lhs.push_back(sivars[d_ask_types_index[q][j]]); subs_rhs.push_back( outer_vars[j] ); } //get function substitution - for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){ - Node f = it->first; - Node fv = d_quant_sip[q].d_func_fo_var[it->first]; + std::vector<Node> funcs; + d_quant_sip[q].getFunctions(funcs); + for (const Node& f : funcs) + { + Node fv = d_quant_sip[q].getFirstOrderVariableForFunction(f); if( func_to_var.find( f )==func_to_var.end() ){ Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() ); Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl; |