* 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
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 \
#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"
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<Node> all_vars;
+ sip.getAllVariables(all_vars);
+ std::vector<Node> si_vars;
+ sip.getSingleInvocationVariables(si_vars);
std::vector<Node> qe_vars;
std::vector<Node> 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);
}
// 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<Node, bool>::iterator it = sip.d_funcs.begin();
- it != sip.d_funcs.end();
- ++it)
+ std::vector<Node> 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
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;
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();
}
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;
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() ){
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 );
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;
#include <map>
#include <vector>
-#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 {
**/
#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;
std::map< Node, Node > single_inv_app_map;
for( unsigned j=0; j<progs.size(); j++ ){
Node prog = progs[j];
- std::map< Node, Node >::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();
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;
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<Node> 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; j<d_sip->d_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; j<q[1][0][0].getNumChildren(); j++ ){
new_bv.push_back( q[1][0][0][j] );
if( d_single_invocation ){
d_single_inv = d_sip->getSingleInvocation();
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<Node> 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; i<d_sip->d_si_vars.size(); i++ ){
- Node v = NodeManager::currentNM()->mkSkolem( "a", d_sip->d_si_vars[i].getType(), "single invocation arg" );
+ std::vector<Node> 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
if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
siss << " * single invocation: " << std::endl;
for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
- Assert( d_sip->d_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;
}
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<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< Node >& 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; 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< Node >& funcs, std::vector< TypeNode >& 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 );
- }
- 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<conj.size(); i++ ){
- std::vector< Node > 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<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< Node, Node > 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; 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< 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; 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< Node > bvs;
- TermUtil::getBoundVars( cr, bvs );
- std::vector< Node > terms;
- std::vector< Node > 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;
- }
-}
-
-bool SingleInvocationPartition::collectConjuncts( Node n, bool pol, std::vector< Node >& 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< Node, bool >& 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<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< Node, bool >::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; 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;
- 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<n.getNumChildren(); i++ ){
- Node nn = getSpecificationInst( n[i], lam, visited );
- children.push_back( nn );
- childChanged = childChanged || ( nn!=n[i] );
- }
- Node 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()==APPLY_UF ){
- f = n.getOperator();
- success = true;
- }
- }
- if( success ){
- std::map< Node, Node >::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; i<itl->second[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<d_si_vars.size(); i++ ){
- Trace(c) << d_si_vars[i] << " ";
- }
- Trace(c) << std::endl;
- Trace(c) << "Functions : " << std::endl;
- for( std::map< Node, bool >::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;
-}
-
-
bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){
if( index==val.size() ){
if( d_children.empty() ){
#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 {
bool addLemma( Node lem );
};
-
-class SingleInvocationPartition;
-
class DetTrace {
private:
class DetTraceTrie {
}
};
-// 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 */
--- /dev/null
+/********************* */
+/*! \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<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;
+ }
+}
+
+Node SingleInvocationPartition::getFirstOrderVariableForFunction(Node f) const
+{
+ std::map<Node, Node>::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<Node, Node>::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<Node, Node>::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<Node>& fvars) const
+{
+ fvars.insert(fvars.end(), d_func_vars.begin(), d_func_vars.end());
+}
+
+void SingleInvocationPartition::getFunctions(std::vector<Node>& fs) const
+{
+ fs.insert(fs.end(), d_all_funcs.begin(), d_all_funcs.end());
+}
+
+void SingleInvocationPartition::getSingleInvocationVariables(
+ std::vector<Node>& sivars) const
+{
+ sivars.insert(sivars.end(), d_si_vars.begin(), d_si_vars.end());
+}
+
+void SingleInvocationPartition::getAllVariables(std::vector<Node>& 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<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 < 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<Node>& 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; 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<Node>& funcs,
+ std::vector<TypeNode>& 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<Node> conj;
+ if (collectConjuncts(n, true, conj))
+ {
+ Trace("si-prt") << "...success." << std::endl;
+ for (unsigned i = 0; i < conj.size(); i++)
+ {
+ std::vector<Node> 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 < 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<Node, Node> 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; 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<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; 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<Node> bvs;
+ TermUtil::getBoundVars(cr, bvs);
+ std::vector<Node> terms;
+ std::vector<Node> 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<Node>& 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<Node, bool>& 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 < 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<Node, bool>::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; 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<Node, bool>::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 */
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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<Node>& 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<Node>& sivars) const;
+
+ /** get all variables
+ *
+ * Appends all free variables of the processed formula to vars.
+ */
+ void getAllVariables(std::vector<Node>& vars) const;
+
+ /** get function variables
+ *
+ * Appends all first-order variables corresponding to input functions to
+ * fvars.
+ */
+ void getFunctionVariables(std::vector<Node>& fvars) const;
+
+ /** get functions
+ *
+ * Gets all input functions. This has the same order as the list of
+ * function variables above.
+ */
+ void getFunctions(std::vector<Node>& 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<Node, bool> d_funcs;
+
+ /** map from functions to the invocation we inferred for them */
+ std::map<Node, Node> d_func_inv;
+
+ /** the list of first-order variables for functions
+ * In (EX1), this is the list { z }.
+ */
+ std::vector<Node> d_func_vars;
+
+ /** the arguments that we based the anti-skolemization on.
+ * In (EX1), this is the list { x, y }.
+ */
+ std::vector<Node> d_si_vars;
+
+ /** every free variable of conjuncts[2] */
+ std::vector<Node> d_all_vars;
+ /** map from functions to first-order variables that anti-skolemized them */
+ std::map<Node, Node> d_func_fo_var;
+ /** map from first-order variables to the function it anti-skolemized */
+ std::map<Node, Node> 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<TypeNode> 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<Node> 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<Node> d_input_funcs;
+ /** all input functions */
+ std::vector<Node> 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<TypeNode>& typs,
+ std::map<Node, bool>& 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<Node>& funcs,
+ std::vector<TypeNode>& 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<Node>& 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<Node, bool>& visited,
+ std::vector<Node>& args,
+ std::vector<Node>& terms,
+ std::vector<Node>& 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 */
projects / cvc5.git / commitdiff