From a7524f1f72c324dae36bd4a461d31e5e26fdca15 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Nov 2017 15:19:25 -0600 Subject: (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/theory/quantifiers/single_inv_partition.cpp | 590 ++++++++++++++++++++++++ 1 file changed, 590 insertions(+) create mode 100644 src/theory/quantifiers/single_inv_partition.cpp (limited to 'src/theory/quantifiers/single_inv_partition.cpp') 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 */ -- cgit v1.2.3