diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-04 16:17:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-04 16:17:35 -0500 |
commit | 0811ba46a8a8818231e7f4e931b99d654c12a348 (patch) | |
tree | 02007a6dfc68675c804babff4a35a7cf271c44f8 /src/theory/quantifiers/ematching | |
parent | 541b880047374f3748fbf9fa93214bae1308b1aa (diff) |
Fix for corner case of higher-order matching (#1708)
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 84 |
1 files changed, 63 insertions, 21 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 0e0955119..fad6334b8 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -236,7 +236,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) { TNode var = ha.first; unsigned vnum = var.getAttribute(InstVarNumAttribute()); - Node value = m.d_vals[vnum]; + TNode value = m.d_vals[vnum]; Trace("ho-unif-debug") << " val[" << var << "] = " << value << std::endl; Trace("ho-unif-debug2") << "initialize lambda information..." @@ -256,7 +256,17 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) for (unsigned i = 0; i < ha.second.size(); i++) { std::vector<TNode> args; - Node f = uf::TheoryUfRewriter::decomposeHoApply(ha.second[i], args); + // must substitute the operator we matched with the original + // higher-order variable (var) that matched it. This ensures that the + // argument vector (args) below is of the proper length. This handles, + // for example, matches like: + // (@ x y) with (@ (@ k1 k2) k3) + // where k3 but not k2 should be an argument of the match. + Node hmatch = ha.second[i]; + Trace("ho-unif-debug2") << "Match is " << hmatch << std::endl; + hmatch = hmatch.substitute(value, var); + Trace("ho-unif-debug2") << "Pre-subs match is " << hmatch << std::endl; + Node f = uf::TheoryUfRewriter::decomposeHoApply(hmatch, args); // Assert( f==value ); for (unsigned k = 0, size = args.size(); k < size; k++) { @@ -348,7 +358,9 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) Trace("ho-unif-debug2") << "finished." << std::endl; } - return sendInstantiation(m, 0); + bool ret = sendInstantiation(m, 0); + Trace("ho-unif-debug") << "Finished, success = " << ret << std::endl; + return ret; } else { @@ -361,6 +373,8 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) // occurring as pattern operators (very small) bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index) { + Trace("ho-unif-debug2") << "send inst " << var_index << " / " + << d_ho_var_list.size() << std::endl; if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try @@ -394,13 +408,18 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m, Node lbvl, bool arg_changed) { + Trace("ho-unif-debug2") << "send inst arg " << arg_index << " / " + << lbvl.getNumChildren() << std::endl; if (arg_index == lbvl.getNumChildren()) { // construct the lambda if (arg_changed) { + Trace("ho-unif-debug2") + << " make lambda from children: " << d_lchildren[vnum] << std::endl; Node body = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]); + Trace("ho-unif-debug2") << " got " << body << std::endl; Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body); m.d_vals[vnum] = lam; Trace("ho-unif-debug2") << " try " << vnum << " -> " << lam << std::endl; @@ -438,35 +457,58 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m, int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() { + if (d_ho_var_types.empty()) + { + return 0; + } + Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl; unsigned numLemmas = 0; - if (!d_ho_var_types.empty()) + // this forces expansion of APPLY_UF terms to curried HO_APPLY chains + unsigned size = d_quantEngine->getTermDatabase()->getNumOperators(); + quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); + NodeManager* nm = NodeManager::currentNM(); + for (unsigned j = 0; j < size; j++) { - // this forces expansion of APPLY_UF terms to curried HO_APPLY chains - unsigned size = d_quantEngine->getTermDatabase()->getNumOperators(); - for (unsigned j = 0; j < size; j++) + Node f = d_quantEngine->getTermDatabase()->getOperator(j); + if (f.isVar()) { - Node f = d_quantEngine->getTermDatabase()->getOperator(j); - if (f.isVar()) + TypeNode tn = f.getType(); + if (tn.isFunction()) { - TypeNode tn = f.getType(); - if (d_ho_var_types.find(tn) != d_ho_var_types.end()) + std::vector<TypeNode> argTypes = tn.getArgTypes(); + Assert(argTypes.size() > 0); + TypeNode range = tn.getRangeType(); + // for each function type suffix of the type of f, for example if + // f : (Int -> (Int -> Int)) + // we iterate with stn = (Int -> (Int -> Int)) and (Int -> Int) + for (unsigned a = 0, size = argTypes.size(); a < size; a++) { - Node u = d_quantEngine->getTermUtil()->getHoTypeMatchPredicate(tn); - Node au = NodeManager::currentNM()->mkNode(kind::APPLY_UF, u, f); - if (d_quantEngine->addLemma(au)) + std::vector<TypeNode> sargts; + sargts.insert(sargts.begin(), argTypes.begin() + a, argTypes.end()); + Assert(sargts.size() > 0); + TypeNode stn = nm->mkFunctionType(sargts, range); + Trace("ho-quant-trigger-debug") + << "For " << f << ", check " << stn << "..." << std::endl; + // if a variable of this type occurs in this trigger + if (d_ho_var_types.find(stn) != d_ho_var_types.end()) { - // this forces f to be a first-class member of the quantifier-free - // equality engine, - // which in turn forces the quantifier-free theory solver to expand - // it to HO_APPLY - Trace("ho-quant") << "Added ho match predicate lemma : " << au - << std::endl; - numLemmas++; + Node u = tutil->getHoTypeMatchPredicate(tn); + Node au = nm->mkNode(kind::APPLY_UF, u, f); + if (d_quantEngine->addLemma(au)) + { + // this forces f to be a first-class member of the quantifier-free + // equality engine, which in turn forces the quantifier-free + // theory solver to expand it to an HO_APPLY chain. + Trace("ho-quant") + << "Added ho match predicate lemma : " << au << std::endl; + numLemmas++; + } } } } } } + return numLemmas; } |