From a7524f1f72c324dae36bd4a461d31e5e26fdca15 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Nov 2017 15:19:25 -0600 Subject: [PATCH] (Refactor) Document and clean single invocation partition. (#1364) * Documenting single invocation partiion. * More * More encapsulation. * More, documentation complete. * Split to own file. * Format * Fully encapsulate. * Format * Improvements to doc. * Format * Address * Format * Missed comment * Newline * Address * Format --- src/Makefile.am | 2 + src/smt/smt_engine.cpp | 61 +- src/theory/quantifiers/anti_skolem.cpp | 38 +- src/theory/quantifiers/anti_skolem.h | 6 +- .../quantifiers/ce_guided_single_inv.cpp | 495 ++------------- src/theory/quantifiers/ce_guided_single_inv.h | 59 +- .../quantifiers/single_inv_partition.cpp | 590 ++++++++++++++++++ src/theory/quantifiers/single_inv_partition.h | 295 +++++++++ 8 files changed, 991 insertions(+), 555 deletions(-) create mode 100644 src/theory/quantifiers/single_inv_partition.cpp create mode 100644 src/theory/quantifiers/single_inv_partition.h diff --git a/src/Makefile.am b/src/Makefile.am index 75fdd32ae..acd94a90a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -433,6 +433,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/relevant_domain.h \ theory/quantifiers/rewrite_engine.cpp \ theory/quantifiers/rewrite_engine.h \ + theory/quantifiers/single_inv_partition.cpp \ + theory/quantifiers/single_inv_partition.h \ theory/quantifiers/skolemize.cpp \ theory/quantifiers/skolemize.h \ theory/quantifiers/sygus_explain.cpp \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d703e8e83..1a35c9901 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -93,6 +93,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/term_util.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" @@ -4631,14 +4632,18 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { Trace("smt-synth") << "Property is non-ground single invocation, run " "QE to obtain single invocation." << std::endl; + NodeManager* nm = NodeManager::currentNM(); // partition variables + std::vector all_vars; + sip.getAllVariables(all_vars); + std::vector si_vars; + sip.getSingleInvocationVariables(si_vars); std::vector qe_vars; std::vector nqe_vars; - for (unsigned i = 0; i < sip.d_all_vars.size(); i++) + for (unsigned i = 0, size = all_vars.size(); i < size; i++) { - Node v = sip.d_all_vars[i]; - if (std::find(sip.d_si_vars.begin(), sip.d_si_vars.end(), v) - == sip.d_si_vars.end()) + Node v = all_vars[i]; + if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) { qe_vars.push_back(v); } @@ -4652,27 +4657,29 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { // skolemize non-qe variables for (unsigned i = 0; i < nqe_vars.size(); i++) { - Node k = NodeManager::currentNM()->mkSkolem( - "k", - nqe_vars[i].getType(), - "qe for non-ground single invocation"); + Node k = nm->mkSkolem("k", + nqe_vars[i].getType(), + "qe for non-ground single invocation"); orig.push_back(nqe_vars[i]); subs.push_back(k); Trace("smt-synth") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; } - for (std::map::iterator it = sip.d_funcs.begin(); - it != sip.d_funcs.end(); - ++it) + std::vector funcs; + sip.getFunctions(funcs); + for (unsigned i = 0, size = funcs.size(); i < size; i++) { - orig.push_back(sip.d_func_inv[it->first]); - Node k = NodeManager::currentNM()->mkSkolem( - "k", - sip.d_func_fo_var[it->first].getType(), - "qe for function in non-ground single invocation"); + Node f = funcs[i]; + Node fi = sip.getFunctionInvocationFor(f); + Node fv = sip.getFirstOrderVariableForFunction(f); + Assert(!fi.isNull()); + orig.push_back(fi); + Node k = + nm->mkSkolem("k", + fv.getType(), + "qe for function in non-ground single invocation"); subs.push_back(k); - Trace("smt-synth") << " subs : " << sip.d_func_inv[it->first] - << " -> " << k << std::endl; + Trace("smt-synth") << " subs : " << fi << " -> " << k << std::endl; } Node conj_se_ngsi = sip.getFullSpecification(); Trace("smt-synth") << "Full specification is " << conj_se_ngsi @@ -4680,10 +4687,10 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end()); Assert(!qe_vars.empty()); - conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( - kind::EXISTS, - NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qe_vars), - conj_se_ngsi_subs.negate()); + conj_se_ngsi_subs = + nm->mkNode(kind::EXISTS, + nm->mkNode(kind::BOUND_VAR_LIST, qe_vars), + conj_se_ngsi_subs.negate()); Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; @@ -4697,14 +4704,12 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { subs.begin(), subs.end(), orig.begin(), orig.end()); if (!nqe_vars.empty()) { - qe_res_n = NodeManager::currentNM()->mkNode( - kind::EXISTS, - NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, nqe_vars), - qe_res_n); + qe_res_n = nm->mkNode(kind::EXISTS, + nm->mkNode(kind::BOUND_VAR_LIST, nqe_vars), + qe_res_n); } Assert(conj.getNumChildren() == 3); - qe_res_n = NodeManager::currentNM()->mkNode( - kind::FORALL, conj[0], qe_res_n, conj[2]); + qe_res_n = nm->mkNode(kind::FORALL, conj[0], qe_res_n, conj[2]); Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl; e_check = qe_res_n.toExpr(); 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 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& quants, bool for( unsigned i=0; i 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 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; imkBoundVar( 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 " << outer_vars[j] << std::endl; - subs_lhs.push_back( d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] ); + std::vector 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 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; diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index bad98c04b..bf8b99f1c 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -20,11 +20,11 @@ #include #include -#include "expr/node.h" -#include "expr/type_node.h" #include "context/cdhashset.h" #include "context/cdo.h" -#include "theory/quantifiers/ce_guided_single_inv.h" +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index c810ed5cf..03026069f 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -14,16 +14,10 @@ **/ #include "theory/quantifiers/ce_guided_single_inv.h" -#include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" -#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; @@ -153,11 +147,11 @@ void CegConjectureSingleInv::initialize( Node q ) { std::map< Node, Node > single_inv_app_map; for( unsigned j=0; j::iterator it_fov = d_sip->d_func_fo_var.find( prog ); - if( it_fov!=d_sip->d_func_fo_var.end() ){ - Node pv = it_fov->second; - Assert( d_sip->d_func_inv.find( prog )!=d_sip->d_func_inv.end() ); - Node inv = d_sip->d_func_inv[prog]; + Node pv = d_sip->getFirstOrderVariableForFunction(prog); + if (!pv.isNull()) + { + Node inv = d_sip->getFunctionInvocationFor(prog); + Assert(!inv.isNull()); single_inv_app_map[prog] = inv; Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl; d_prog_to_sol_index[prog] = order_vars.size(); @@ -166,14 +160,10 @@ void CegConjectureSingleInv::initialize( Node q ) { Trace("cegqi-si") << " " << prog << " has no fo var." << std::endl; } } - //reorder the variables - Assert( d_sip->d_func_vars.size()==order_vars.size() ); - d_sip->d_func_vars.clear(); - d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() ); - //check if it is single invocation - if( !d_sip->d_conjuncts[1].empty() ){ + if (!d_sip->isPurelySingleInvocation()) + { if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ //if we are doing invariant templates, then construct the template Trace("cegqi-si") << "- Do transition inference..." << std::endl; @@ -188,17 +178,25 @@ void CegConjectureSingleInv::initialize( Node q ) { d_trans_post[prog] = d_ti[q].getComponent( -1 ); Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + std::vector sivars; + d_sip->getSingleInvocationVariables(sivars); Node invariant = single_inv_app_map[prog]; - invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), prog_templ_vars.begin(), prog_templ_vars.end() ); + invariant = invariant.substitute(sivars.begin(), + sivars.end(), + prog_templ_vars.begin(), + prog_templ_vars.end()); Trace("cegqi-inv") << " invariant : " << invariant << std::endl; // store simplified version of quantified formula - d_simp_quant = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] ); + d_simp_quant = d_sip->getFullSpecification(); std::vector< Node > new_bv; - for( unsigned j=0; jd_si_vars.size(); j++ ){ - new_bv.push_back( NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() ) ); + for (unsigned j = 0, size = sivars.size(); j < size; j++) + { + new_bv.push_back( + NodeManager::currentNM()->mkBoundVar(sivars[j].getType())); } - d_simp_quant = d_simp_quant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_bv.begin(), new_bv.end() ); + d_simp_quant = d_simp_quant.substitute( + sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end()); Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ); for( unsigned j=0; jgetSingleInvocation(); d_single_inv = TermUtil::simpleNegate( d_single_inv ); - if( !d_sip->d_func_vars.empty() ){ - Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_func_vars ); + std::vector func_vars; + d_sip->getFunctionVariables(func_vars); + if (!func_vars.empty()) + { + Node pbvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, func_vars); d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv ); } //now, introduce the skolems - for( unsigned i=0; id_si_vars.size(); i++ ){ - Node v = NodeManager::currentNM()->mkSkolem( "a", d_sip->d_si_vars[i].getType(), "single invocation arg" ); + std::vector sivars; + d_sip->getSingleInvocationVariables(sivars); + for (unsigned i = 0, size = sivars.size(); i < size; i++) + { + Node v = NodeManager::currentNM()->mkSkolem( + "a", sivars[i].getType(), "single invocation arg"); d_single_inv_arg_sk.push_back( v ); } - d_single_inv = d_single_inv.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), - d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); + d_single_inv = d_single_inv.substitute(sivars.begin(), + sivars.end(), + d_single_inv_arg_sk.begin(), + d_single_inv_arg_sk.end()); Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl; if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){ //just invoke the presolve now @@ -317,10 +324,9 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ siss << " * single invocation: " << std::endl; for( unsigned j=0; jd_fo_var_to_func.find( d_single_inv[0][j] )!=d_sip->d_fo_var_to_func.end() ); - Node op = d_sip->d_fo_var_to_func[d_single_inv[0][j]]; - Node prog = op; - siss << " * " << prog; + Node op = d_sip->getFunctionForFirstOrderVariable(d_single_inv[0][j]); + Assert(!op.isNull()); + siss << " * " << op; siss << " (" << d_single_inv_sk[j] << ")"; siss << " -> " << subs[j] << std::endl; } @@ -616,431 +622,6 @@ void CegConjectureSingleInv::preregisterConjecture( Node q ) { d_orig_conjecture = q; } -bool SingleInvocationPartition::init( Node n ) { - //first, get types of arguments for functions - std::vector< TypeNode > typs; - std::map< Node, bool > visited; - std::vector< Node > funcs; - if( inferArgTypes( n, typs, visited ) ){ - return init( funcs, typs, n, false ); - }else{ - Trace("si-prt") << "Could not infer argument types." << std::endl; - return false; - } -} - -// gets the argument type list for the first APPLY_UF we see -bool SingleInvocationPartition::inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.getKind()!=FORALL ){ - if( n.getKind()==APPLY_UF ){ - for( unsigned i=0; i& funcs, Node n ) { - Trace("si-prt") << "Initialize with " << funcs.size() << " input functions..." << std::endl; - std::vector< TypeNode > typs; - if( !funcs.empty() ){ - TypeNode tn0 = funcs[0].getType(); - for( unsigned i=1; i1 ){ - for( unsigned j=0; jmkBoundVar( ss.str(), d_arg_types[j] ); - d_si_vars.push_back( si_v ); - } - Trace("si-prt") << "Process the formula..." << std::endl; - process( n ); - return true; -} - - -void SingleInvocationPartition::process( Node n ) { - Assert( d_si_vars.size()==d_arg_types.size() ); - Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl; - Trace("si-prt") << "Get conjuncts..." << std::endl; - std::vector< Node > conj; - if( collectConjuncts( n, true, conj ) ){ - Trace("si-prt") << "...success." << std::endl; - for( unsigned i=0; i si_terms; - std::vector< Node > si_subs; - Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl; - //do DER on conjunct - Node cr = TermUtil::getQuantSimplify( conj[i] ); - if( cr!=conj[i] ){ - Trace("si-prt-debug") << "...rewritten to " << cr << std::endl; - } - std::map< Node, bool > visited; - // functions to arguments - std::vector< Node > args; - std::vector< Node > terms; - std::vector< Node > subs; - bool singleInvocation = true; - bool ngroundSingleInvocation = false; - if( processConjunct( cr, visited, args, terms, subs ) ){ - for( unsigned j=0; j subs_map; - std::map< Node, Node > subs_map_rev; - std::vector< Node > funcs; - //normalize the invocations - if( !terms.empty() ){ - Assert( terms.size()==subs.size() ); - cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); - } - std::vector< Node > children; - children.push_back( cr ); - terms.clear(); - subs.clear(); - Trace("si-prt") << "...single invocation, with arguments: " << std::endl; - for( unsigned j=0; jmkNode( OR, children ); - Assert( terms.size()==subs.size() ); - cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); - Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; - //now must check if it has other bound variables - std::vector< Node > bvs; - TermUtil::getBoundVars( cr, bvs ); - if( bvs.size()>d_si_vars.size() ){ - // getBoundVars also collects functions in the rare case that we are synthesizing a function with 0 arguments - // take these into account below. - unsigned n_const_synth_fun = 0; - for( unsigned j=0; jd_si_vars.size() ){ - Trace("si-prt") << "...not ground single invocation." << std::endl; - ngroundSingleInvocation = true; - singleInvocation = false; - }else{ - Trace("si-prt") << "...ground single invocation : success, after removing 0-arg synth functions." << std::endl; - } - }else{ - Trace("si-prt") << "...ground single invocation : success." << std::endl; - } - }else{ - Trace("si-prt") << "...not single invocation." << std::endl; - singleInvocation = false; - //rename bound variables with maximal overlap with si_vars - std::vector< Node > bvs; - TermUtil::getBoundVars( cr, bvs ); - std::vector< Node > terms; - std::vector< Node > subs; - for( unsigned j=0; j& conj ) { - if( ( !pol && n.getKind()==OR ) || ( pol && n.getKind()==AND ) ){ - for( unsigned i=0; i& visited, std::vector< Node >& args, - std::vector< Node >& terms, std::vector< Node >& subs ) { - std::map< Node, bool >::iterator it = visited.find( n ); - if( it!=visited.end() ){ - return true; - }else{ - bool ret = true; - //if( TermUtil::hasBoundVarAttr( n ) ){ - for( unsigned i=0; i::iterator it = d_funcs.find( f ); - if( it!=d_funcs.end() ){ - return it->second; - }else{ - TypeNode tn = f.getType(); - bool ret = false; - if( tn.getNumChildren()==d_arg_types.size()+1 || ( d_arg_types.empty() && tn.getNumChildren()==0 ) ){ - ret = true; - std::vector< Node > children; - children.push_back( f ); - //TODO: permutations of arguments - for( unsigned i=0; i1 ){ - t = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); - }else{ - t = children[0]; - } - d_func_inv[f] = t; - d_inv_to_func[t] = f; - std::stringstream ss; - ss << "F_" << f; - TypeNode rt; - if( d_arg_types.empty() ){ - rt = tn; - }else{ - rt = tn.getRangeType(); - } - Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), rt ); - d_func_fo_var[f] = v; - d_fo_var_to_func[v] = f; - d_func_vars.push_back( v ); - } - } - d_funcs[f] = ret; - return ret; - } -} - -Node SingleInvocationPartition::getConjunct( int index ) { - return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst( true ) : - ( d_conjuncts[index].size()==1 ? d_conjuncts[index][0] : NodeManager::currentNM()->mkNode( AND, d_conjuncts[index] ) ); -} - -Node SingleInvocationPartition::getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited ) { - std::map< Node, Node >::iterator it = visited.find( n ); - if( it!=visited.end() ){ - return it->second; - }else{ - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; i::iterator itl = lam.find( f ); - if( itl!=lam.end() ){ - Assert( itl->second[0].getNumChildren()==children.size() ); - std::vector< Node > terms; - std::vector< Node > subs; - for( unsigned i=0; isecond[0].getNumChildren(); i++ ){ - terms.push_back( itl->second[0][i] ); - subs.push_back( children[i] ); - } - ret = itl->second[1].substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); - ret = Rewriter::rewrite( ret ); - } - } - if( ret.isNull() ){ - ret = n; - if( childChanged ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), n.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - return ret; - } -} - -Node SingleInvocationPartition::getSpecificationInst( int index, std::map< Node, Node >& lam ) { - Node conj = getConjunct( index ); - std::map< Node, Node > visited; - return getSpecificationInst( conj, lam, visited ); -} - -void SingleInvocationPartition::debugPrint( const char * c ) { - Trace(c) << "Single invocation variables : "; - for( unsigned i=0; i::iterator it = d_funcs.begin(); it != d_funcs.end(); ++it ){ - Trace(c) << " " << it->first << " : "; - if( it->second ){ - Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first] << std::endl; - }else{ - Trace(c) << "not incorporated." << std::endl; - } - } - for( unsigned i=0; i<4; i++ ){ - Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : ( i==2 ? "All" : "Non-ground single invocation" ) ) ); - Trace(c) << " conjuncts: " << std::endl; - for( unsigned j=0; j& val, unsigned index ){ if( index==val.size() ){ if( d_children.empty() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index ffcdb7075..8e63e8909 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -17,11 +17,12 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H -#include "context/cdhashmap.h" #include "context/cdchunk_list.h" -#include "theory/quantifiers_engine.h" +#include "context/cdhashmap.h" #include "theory/quantifiers/ce_guided_single_inv_sol.h" #include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/quantifiers/single_inv_partition.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { @@ -41,9 +42,6 @@ public: bool addLemma( Node lem ); }; - -class SingleInvocationPartition; - class DetTrace { private: class DetTraceTrie { @@ -243,57 +241,6 @@ class CegConjectureSingleInv { } }; -// A utility to group formulas into single invocation/non-single -// invocation parts. Only processes functions having argument types exactly matching -// "d_arg_types", and all invocations are in the same order across all -// functions -class SingleInvocationPartition { -private: - bool d_has_input_funcs; - std::vector< Node > d_input_funcs; - //options - bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ); - void process( Node n ); - bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj ); - bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args, - std::vector< Node >& terms, std::vector< Node >& subs ); - Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited ); - bool init( std::vector< Node >& funcs, std::vector< TypeNode >& typs, Node n, bool has_funcs ); -public: - SingleInvocationPartition() : d_has_input_funcs( false ){} - ~SingleInvocationPartition(){} - bool init( Node n ); - bool init( std::vector< Node >& funcs, Node n ); - - //outputs (everything is with bound var) - std::vector< TypeNode > d_arg_types; - std::map< Node, bool > d_funcs; - std::map< Node, Node > d_func_inv; - std::map< Node, Node > d_inv_to_func; - std::map< Node, Node > d_func_fo_var; - std::map< Node, Node > d_fo_var_to_func; - std::vector< Node > d_func_vars; //the first-order variables corresponding to all functions - std::vector< Node > d_si_vars; //the arguments that we based the anti-skolemization on - std::vector< Node > d_all_vars; //every free variable of conjuncts[2] - // si, nsi, all, non-ground si - std::vector< Node > d_conjuncts[4]; - - bool isAntiSkolemizableType( Node f ); - - Node getConjunct( int index ); - Node getSingleInvocation() { return getConjunct( 0 ); } - Node getNonSingleInvocation() { return getConjunct( 1 ); } - Node getFullSpecification() { return getConjunct( 2 ); } - - Node getSpecificationInst( int index, std::map< Node, Node >& lam ); - - bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); } - bool isNonGroundSingleInvocation() { return d_conjuncts[3].size()==d_conjuncts[1].size(); } - - void debugPrint( const char * c ); -}; - - }/* namespace CVC4::theory::quantifiers */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp new file mode 100644 index 000000000..890b7fcd3 --- /dev/null +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -0,0 +1,590 @@ +/********************* */ +/*! \file single_inv_partition.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief utility for processing single invocation synthesis conjectures + ** + **/ +#include "theory/quantifiers/single_inv_partition.h" + +#include "theory/quantifiers/term_util.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +bool SingleInvocationPartition::init(Node n) +{ + // first, get types of arguments for functions + std::vector typs; + std::map visited; + std::vector funcs; + if (inferArgTypes(n, typs, visited)) + { + return init(funcs, typs, n, false); + } + else + { + Trace("si-prt") << "Could not infer argument types." << std::endl; + return false; + } +} + +Node SingleInvocationPartition::getFirstOrderVariableForFunction(Node f) const +{ + std::map::const_iterator it = d_func_fo_var.find(f); + if (it != d_func_fo_var.end()) + { + return it->second; + } + return Node::null(); +} + +Node SingleInvocationPartition::getFunctionForFirstOrderVariable(Node v) const +{ + std::map::const_iterator it = d_fo_var_to_func.find(v); + if (it != d_fo_var_to_func.end()) + { + return it->second; + } + return Node::null(); +} + +Node SingleInvocationPartition::getFunctionInvocationFor(Node f) const +{ + std::map::const_iterator it = d_func_inv.find(f); + if (it != d_func_inv.end()) + { + return it->second; + } + return Node::null(); +} + +void SingleInvocationPartition::getFunctionVariables( + std::vector& fvars) const +{ + fvars.insert(fvars.end(), d_func_vars.begin(), d_func_vars.end()); +} + +void SingleInvocationPartition::getFunctions(std::vector& fs) const +{ + fs.insert(fs.end(), d_all_funcs.begin(), d_all_funcs.end()); +} + +void SingleInvocationPartition::getSingleInvocationVariables( + std::vector& sivars) const +{ + sivars.insert(sivars.end(), d_si_vars.begin(), d_si_vars.end()); +} + +void SingleInvocationPartition::getAllVariables(std::vector& vars) const +{ + vars.insert(vars.end(), d_all_vars.begin(), d_all_vars.end()); +} + +// gets the argument type list for the first APPLY_UF we see +bool SingleInvocationPartition::inferArgTypes(Node n, + std::vector& typs, + std::map& visited) +{ + if (visited.find(n) == visited.end()) + { + visited[n] = true; + if (n.getKind() != FORALL) + { + if (n.getKind() == APPLY_UF) + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + typs.push_back(n[i].getType()); + } + return true; + } + else + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + if (inferArgTypes(n[i], typs, visited)) + { + return true; + } + } + } + } + } + return false; +} + +bool SingleInvocationPartition::init(std::vector& funcs, Node n) +{ + Trace("si-prt") << "Initialize with " << funcs.size() << " input functions..." + << std::endl; + std::vector typs; + if (!funcs.empty()) + { + TypeNode tn0 = funcs[0].getType(); + for (unsigned i = 1; i < funcs.size(); i++) + { + if (funcs[i].getType() != tn0) + { + // can't anti-skolemize functions of different sort + Trace("si-prt") << "...type mismatch" << std::endl; + return false; + } + } + if (tn0.getNumChildren() > 1) + { + for (unsigned j = 0; j < tn0.getNumChildren() - 1; j++) + { + typs.push_back(tn0[j]); + } + } + } + Trace("si-prt") << "#types = " << typs.size() << std::endl; + return init(funcs, typs, n, true); +} + +bool SingleInvocationPartition::init(std::vector& funcs, + std::vector& typs, + Node n, + bool has_funcs) +{ + Assert(d_arg_types.empty()); + Assert(d_input_funcs.empty()); + Assert(d_si_vars.empty()); + d_has_input_funcs = has_funcs; + d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end()); + d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end()); + Trace("si-prt") << "Initialize..." << std::endl; + for (unsigned j = 0; j < d_arg_types.size(); j++) + { + std::stringstream ss; + ss << "s_" << j; + Node si_v = NodeManager::currentNM()->mkBoundVar(ss.str(), d_arg_types[j]); + d_si_vars.push_back(si_v); + } + Assert(d_si_vars.size() == d_arg_types.size()); + Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl; + Trace("si-prt") << "Get conjuncts..." << std::endl; + std::vector conj; + if (collectConjuncts(n, true, conj)) + { + Trace("si-prt") << "...success." << std::endl; + for (unsigned i = 0; i < conj.size(); i++) + { + std::vector si_terms; + std::vector si_subs; + Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl; + // do DER on conjunct + Node cr = TermUtil::getQuantSimplify(conj[i]); + if (cr != conj[i]) + { + Trace("si-prt-debug") << "...rewritten to " << cr << std::endl; + } + std::map visited; + // functions to arguments + std::vector args; + std::vector terms; + std::vector subs; + bool singleInvocation = true; + bool ngroundSingleInvocation = false; + if (processConjunct(cr, visited, args, terms, subs)) + { + for (unsigned j = 0; j < terms.size(); j++) + { + si_terms.push_back(subs[j]); + Node op = subs[j].hasOperator() ? subs[j].getOperator() : subs[j]; + Assert(d_func_fo_var.find(op) != d_func_fo_var.end()); + si_subs.push_back(d_func_fo_var[op]); + } + std::map subs_map; + std::map subs_map_rev; + std::vector funcs; + // normalize the invocations + if (!terms.empty()) + { + Assert(terms.size() == subs.size()); + cr = cr.substitute( + terms.begin(), terms.end(), subs.begin(), subs.end()); + } + std::vector children; + children.push_back(cr); + terms.clear(); + subs.clear(); + Trace("si-prt") << "...single invocation, with arguments: " + << std::endl; + for (unsigned j = 0; j < args.size(); j++) + { + Trace("si-prt") << args[j] << " "; + if (args[j].getKind() == BOUND_VARIABLE + && std::find(terms.begin(), terms.end(), args[j]) == terms.end()) + { + terms.push_back(args[j]); + subs.push_back(d_si_vars[j]); + } + else + { + children.push_back(d_si_vars[j].eqNode(args[j]).negate()); + } + } + Trace("si-prt") << std::endl; + cr = children.size() == 1 + ? children[0] + : NodeManager::currentNM()->mkNode(OR, children); + Assert(terms.size() == subs.size()); + cr = + cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end()); + Trace("si-prt-debug") << "...normalized invocations to " << cr + << std::endl; + // now must check if it has other bound variables + std::vector bvs; + TermUtil::getBoundVars(cr, bvs); + if (bvs.size() > d_si_vars.size()) + { + // getBoundVars also collects functions in the rare case that we are + // synthesizing a function with 0 arguments + // take these into account below. + unsigned n_const_synth_fun = 0; + for (unsigned j = 0; j < bvs.size(); j++) + { + if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bvs[j]) + != d_input_funcs.end()) + { + n_const_synth_fun++; + } + } + if (bvs.size() - n_const_synth_fun > d_si_vars.size()) + { + Trace("si-prt") << "...not ground single invocation." << std::endl; + ngroundSingleInvocation = true; + singleInvocation = false; + } + else + { + Trace("si-prt") << "...ground single invocation : success, after " + "removing 0-arg synth functions." + << std::endl; + } + } + else + { + Trace("si-prt") << "...ground single invocation : success." + << std::endl; + } + } + else + { + Trace("si-prt") << "...not single invocation." << std::endl; + singleInvocation = false; + // rename bound variables with maximal overlap with si_vars + std::vector bvs; + TermUtil::getBoundVars(cr, bvs); + std::vector terms; + std::vector subs; + for (unsigned j = 0; j < bvs.size(); j++) + { + TypeNode tn = bvs[j].getType(); + Trace("si-prt-debug") << "Fit bound var #" << j << " : " << bvs[j] + << " with si." << std::endl; + for (unsigned k = 0; k < d_si_vars.size(); k++) + { + if (tn == d_arg_types[k]) + { + if (std::find(subs.begin(), subs.end(), d_si_vars[k]) + == subs.end()) + { + terms.push_back(bvs[j]); + subs.push_back(d_si_vars[k]); + Trace("si-prt-debug") << " ...use " << d_si_vars[k] + << std::endl; + break; + } + } + } + } + Assert(terms.size() == subs.size()); + cr = + cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end()); + } + cr = Rewriter::rewrite(cr); + Trace("si-prt") << ".....got si=" << singleInvocation + << ", result : " << cr << std::endl; + d_conjuncts[2].push_back(cr); + TermUtil::getBoundVars(cr, d_all_vars); + if (singleInvocation) + { + // replace with single invocation formulation + Assert(si_terms.size() == si_subs.size()); + cr = cr.substitute( + si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end()); + cr = Rewriter::rewrite(cr); + Trace("si-prt") << ".....si version=" << cr << std::endl; + d_conjuncts[0].push_back(cr); + } + else + { + d_conjuncts[1].push_back(cr); + if (ngroundSingleInvocation) + { + d_conjuncts[3].push_back(cr); + } + } + } + } + else + { + Trace("si-prt") << "...failed." << std::endl; + } + return true; +} + +bool SingleInvocationPartition::collectConjuncts(Node n, + bool pol, + std::vector& conj) +{ + if ((!pol && n.getKind() == OR) || (pol && n.getKind() == AND)) + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + if (!collectConjuncts(n[i], pol, conj)) + { + return false; + } + } + } + else if (n.getKind() == NOT) + { + return collectConjuncts(n[0], !pol, conj); + } + else if (n.getKind() == FORALL) + { + return false; + } + else + { + if (!pol) + { + n = TermUtil::simpleNegate(n); + } + Trace("si-prt") << "Conjunct : " << n << std::endl; + conj.push_back(n); + } + return true; +} + +bool SingleInvocationPartition::processConjunct(Node n, + std::map& visited, + std::vector& args, + std::vector& terms, + std::vector& subs) +{ + std::map::iterator it = visited.find(n); + if (it != visited.end()) + { + return true; + } + else + { + bool ret = true; + // if( TermUtil::hasBoundVarAttr( n ) ){ + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + if (!processConjunct(n[i], visited, args, terms, subs)) + { + ret = false; + } + } + if (ret) + { + Node f; + bool success = false; + if (d_has_input_funcs) + { + f = n.hasOperator() ? n.getOperator() : n; + if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f) + != d_input_funcs.end()) + { + success = true; + } + } + else + { + if (n.getKind() == kind::APPLY_UF) + { + f = n.getOperator(); + success = true; + } + } + if (success) + { + if (std::find(terms.begin(), terms.end(), n) == terms.end()) + { + // check if it matches the type requirement + if (isAntiSkolemizableType(f)) + { + if (args.empty()) + { + // record arguments + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + args.push_back(n[i]); + } + } + else + { + // arguments must be the same as those already recorded + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + if (args[i] != n[i]) + { + Trace("si-prt-debug") << "...bad invocation : " << n + << " at arg " << i << "." << std::endl; + ret = false; + break; + } + } + } + if (ret) + { + terms.push_back(n); + subs.push_back(d_func_inv[f]); + } + } + else + { + Trace("si-prt-debug") << "... " << f << " is a bad operator." + << std::endl; + ret = false; + } + } + } + } + //} + visited[n] = ret; + return ret; + } +} + +bool SingleInvocationPartition::isAntiSkolemizableType(Node f) +{ + std::map::iterator it = d_funcs.find(f); + if (it != d_funcs.end()) + { + return it->second; + } + else + { + TypeNode tn = f.getType(); + bool ret = false; + if (tn.getNumChildren() == d_arg_types.size() + 1 + || (d_arg_types.empty() && tn.getNumChildren() == 0)) + { + ret = true; + std::vector children; + children.push_back(f); + // TODO: permutations of arguments + for (unsigned i = 0; i < d_arg_types.size(); i++) + { + children.push_back(d_si_vars[i]); + if (tn[i] != d_arg_types[i]) + { + ret = false; + break; + } + } + if (ret) + { + Node t; + if (children.size() > 1) + { + t = NodeManager::currentNM()->mkNode(kind::APPLY_UF, children); + } + else + { + t = children[0]; + } + d_func_inv[f] = t; + std::stringstream ss; + ss << "F_" << f; + TypeNode rt; + if (d_arg_types.empty()) + { + rt = tn; + } + else + { + rt = tn.getRangeType(); + } + Node v = NodeManager::currentNM()->mkBoundVar(ss.str(), rt); + d_func_fo_var[f] = v; + d_fo_var_to_func[v] = f; + d_func_vars.push_back(v); + d_all_funcs.push_back(f); + } + } + d_funcs[f] = ret; + return ret; + } +} + +Node SingleInvocationPartition::getConjunct(int index) +{ + return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst(true) + : (d_conjuncts[index].size() == 1 + ? d_conjuncts[index][0] + : NodeManager::currentNM()->mkNode( + AND, d_conjuncts[index])); +} + +void SingleInvocationPartition::debugPrint(const char* c) +{ + Trace(c) << "Single invocation variables : "; + for (unsigned i = 0; i < d_si_vars.size(); i++) + { + Trace(c) << d_si_vars[i] << " "; + } + Trace(c) << std::endl; + Trace(c) << "Functions : " << std::endl; + for (std::map::iterator it = d_funcs.begin(); it != d_funcs.end(); + ++it) + { + Trace(c) << " " << it->first << " : "; + if (it->second) + { + Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first] + << std::endl; + } + else + { + Trace(c) << "not incorporated." << std::endl; + } + } + for (unsigned i = 0; i < 4; i++) + { + Trace(c) << (i == 0 ? "Single invocation" + : (i == 1 ? "Non-single invocation" + : (i == 2 ? "All" + : "Non-ground single invocation"))); + Trace(c) << " conjuncts: " << std::endl; + for (unsigned j = 0; j < d_conjuncts[i].size(); j++) + { + Trace(c) << " " << (j + 1) << " : " << d_conjuncts[i][j] << std::endl; + } + } + Trace(c) << std::endl; +} + +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h new file mode 100644 index 000000000..f346285fa --- /dev/null +++ b/src/theory/quantifiers/single_inv_partition.h @@ -0,0 +1,295 @@ +/********************* */ +/*! \file single_inv_partition.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief utility for single invocation partitioning + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H +#define __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H + +#include +#include + +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** single invocation partition + * + * This is a utility to group formulas into single invocation/non-single + * invocation parts, relative to a set of "input functions". + * It can be used when either the set of input functions is fixed, + * or is unknown. + * + * (EX1) For example, if input functions are { f }, + * then the formula is ( f( x, y ) = g( y ) V f( x, y ) = b ) + * is single invocation since there is only one + * unique application of f, that is, f( x, y ). + * Notice that + * exists f. forall xy. f( x, y ) = g( y ) V f( x, y ) = b + * is equivalent to: + * forall xy. exists z. z = g( y ) V z = b + * + * When handling multiple input functions, we only infer a formula + * is single invocation if all (relevant) input functions have the + * same argument types. An input function is relevant if it is + * specified by the input in a call to init() or occurs in the + * formula we are processing. + * + * Notice that this class may introduce auxiliary variables to + * coerce a formula into being single invocation. For example, + * see Example 5 of Reynolds et al. SYNT 2017. + * + */ +class SingleInvocationPartition +{ + public: + SingleInvocationPartition() : d_has_input_funcs(false) {} + ~SingleInvocationPartition() {} + /** initialize this partition for formula n, with input functions funcs + * + * This initializes this class to check whether formula n is single + * invocation with respect to the input functions in funcs only. + * Below, the "processed formula" is a formula generated by this + * call that is equivalent to n (if this call is successful). + * + * This method returns true if all input functions have identical + * argument types, and false otherwise. Notice that all + * access functions below are only valid if this class is + * successfully initialized. + */ + bool init(std::vector& funcs, Node n); + + /** initialize this partition for formula n + * + * In contrast to the above method, this version assumes that + * all uninterpreted functions are input functions. That is, this + * method is equivalent to the above function with funcs containing + * all uninterpreted functions occurring in n. + */ + bool init(Node n); + + /** is the processed formula purely single invocation? + * + * A formula is purely single invocation if it is equivalent to: + * t[ f1( x ), ..., fn( x ), x ], + * for some F, where f1...fn are the input functions. + * Notice that the free variables of t are exactly x. + */ + bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); } + /** is the processed formula non-ground single invocation? + * + * A formula is non-ground single invocation if it is equivalent to: + * F[ f1( x ), ..., fn( x ), x, y ], + * for some F, where f1...fn are the input functions. + */ + bool isNonGroundSingleInvocation() + { + return d_conjuncts[3].size() == d_conjuncts[1].size(); + } + + /** Get the (portion of) the processed formula that is single invocation + * + * Notice this method returns the anti-skolemized version of the input + * formula. In (EX1), this method returns: + * z = g( y ) V z = b + * where z is the first-order variable for f (see + * getFirstOrderVariableForFunction). + */ + Node getSingleInvocation() { return getConjunct(0); } + /** Get the (portion of) the processed formula that is not single invocation + * + * This formula and the above form a partition of the conjuncts of the + * processed formula, that is: + * getSingleInvocation() * sigma ^ getNonSingleInvocation() + * is equivalent to the processed formula, where sigma is a substitution of + * the form: + * z_1 -> f_1( x ) .... z_n -> f_n( x ) + * where z_i are the first-order variables for input functions f_i + * for all i=1,...,n, and x are the single invocation arguments of the input + * formulas (see d_si_vars). + */ + Node getNonSingleInvocation() { return getConjunct(1); } + /** get full specification + * + * This returns getSingleInvocation() * sigma ^ getNonSingleInvocation(), + * which is equivalent to the processed formula, where sigma is the + * substitution described above. + */ + Node getFullSpecification() { return getConjunct(2); } + /** get first order variable for input function f + * + * This corresponds to the variable that we used when anti-skolemizing + * function f. For example, in (EX1), if getSingleInvocation() returns: + * z = g( y ) V z = b + * Then, getFirstOrderVariableForFunction(f) = z. + */ + Node getFirstOrderVariableForFunction(Node f) const; + + /** get function for first order variable + * + * Opposite direction of above, where: + * getFunctionForFirstOrderVariable(z) = f. + */ + Node getFunctionForFirstOrderVariable(Node v) const; + + /** get function invocation for + * + * Returns f( x ) where x are the single invocation arguments of the input + * formulas (see d_si_vars). If f is not an input function, it returns null. + */ + Node getFunctionInvocationFor(Node f) const; + + /** get single invocation variables, appends them to sivars */ + void getSingleInvocationVariables(std::vector& sivars) const; + + /** get all variables + * + * Appends all free variables of the processed formula to vars. + */ + void getAllVariables(std::vector& vars) const; + + /** get function variables + * + * Appends all first-order variables corresponding to input functions to + * fvars. + */ + void getFunctionVariables(std::vector& fvars) const; + + /** get functions + * + * Gets all input functions. This has the same order as the list of + * function variables above. + */ + void getFunctions(std::vector& fs) const; + + /** print debugging information on Trace c */ + void debugPrint(const char* c); + + private: + /** map from input functions to whether they have an anti-skolemizable type + * An anti-skolemizable type is one of the form: + * ( T1, ..., Tn ) -> T + * where Ti = d_arg_types[i] for i = 1,...,n. + */ + std::map d_funcs; + + /** map from functions to the invocation we inferred for them */ + std::map d_func_inv; + + /** the list of first-order variables for functions + * In (EX1), this is the list { z }. + */ + std::vector d_func_vars; + + /** the arguments that we based the anti-skolemization on. + * In (EX1), this is the list { x, y }. + */ + std::vector d_si_vars; + + /** every free variable of conjuncts[2] */ + std::vector d_all_vars; + /** map from functions to first-order variables that anti-skolemized them */ + std::map d_func_fo_var; + /** map from first-order variables to the function it anti-skolemized */ + std::map d_fo_var_to_func; + + /** The argument types for this single invocation partition. + * These are the argument types of the input functions we are + * processing, where notice that: + * d_si_vars[i].getType()==d_arg_types[i] + */ + std::vector d_arg_types; + + /** the list of conjuncts with various properties : + * 0 : the single invocation conjuncts (stored in anti-skolemized form), + * 1 : the non-single invocation conjuncts, + * 2 : all conjuncts, + * 3 : non-ground single invocation conjuncts. + */ + std::vector d_conjuncts[4]; + + /** did we initialize this class with input functions? */ + bool d_has_input_funcs; + /** the input functions we initialized this class with */ + std::vector d_input_funcs; + /** all input functions */ + std::vector d_all_funcs; + + /** infer the argument types of uninterpreted function applications + * + * If this method returns true, then typs contains the list of types of + * the arguments (in order) of all uninterpreted functions in n. + * If this method returns false, then there exists (at least) two + * uninterpreted functions in n whose argument types are not identical. + */ + bool inferArgTypes(Node n, + std::vector& typs, + std::map& visited); + + /** is anti-skolemizable type + * + * This method returns true if f's argument types are equal to the + * argument types we have fixed in this class (see d_arg_types). + */ + bool isAntiSkolemizableType(Node f); + + /** + * This is the entry point for initializing this class, + * which is called by the public init(...) methods. + * funcs are the input functions (if any were explicitly provide), + * typs is the types of the arguments of funcs, + * n is the formula to process, + * has_funcs is whether input functions were explicitly provided. + */ + bool init(std::vector& funcs, + std::vector& typs, + Node n, + bool has_funcs); + + /** + * Collect the top-level conjuncts of the formula (equivalent to) + * n or the negation of n if pol=false, and store them in conj. + */ + bool collectConjuncts(Node n, bool pol, std::vector& conj); + + /** process conjunct n + * + * This function is called when n is a top-level conjunction in a + * formula that is equivalent to the input formula given to this + * class via init. + * + * args : stores the arguments (if any) that we have seen in an application + * of an application of an input function in this conjunct. + * terms/subs : this stores a term substitution with entries of the form: + * f(args) -> z + * where z is the first-order variable for input function f. + */ + bool processConjunct(Node n, + std::map& visited, + std::vector& args, + std::vector& terms, + std::vector& subs); + + /** get the and node corresponding to d_conjuncts[index] */ + Node getConjunct(int index); +}; + +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ -- 2.30.2