diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-25 14:12:00 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-25 14:12:00 -0600 |
commit | f3270fb3629cbc62012ae7eb30843a1bc6d4e3c2 (patch) | |
tree | 1b0ee90651913c1f59513ecf8c3703f20c3d2827 /src | |
parent | 3ab0db55341e7e752411bb003fb203fcd9ec9120 (diff) |
Fixes for higher-order (#1405)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/ho_trigger.cpp | 109 | ||||
-rw-r--r-- | src/theory/quantifiers/ho_trigger.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 |
4 files changed, 94 insertions, 50 deletions
diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ho_trigger.cpp index 0386c0cf0..6354047cf 100644 --- a/src/theory/quantifiers/ho_trigger.cpp +++ b/src/theory/quantifiers/ho_trigger.cpp @@ -72,45 +72,87 @@ HigherOrderTrigger::HigherOrderTrigger( HigherOrderTrigger::~HigherOrderTrigger() {} void HigherOrderTrigger::collectHoVarApplyTerms( - Node q, TNode n, std::map<Node, std::vector<Node> >& apps) + Node q, Node& n, std::map<Node, std::vector<Node> >& apps) { std::vector<Node> ns; ns.push_back(n); collectHoVarApplyTerms(q, ns, apps); + Assert(ns.size() == 1); + n = ns[0]; } void HigherOrderTrigger::collectHoVarApplyTerms( Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps) { - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_map<TNode, Node, TNodeHashFunction> visited; + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; // whether the visited node is a child of a HO_APPLY chain std::unordered_map<TNode, bool, TNodeHashFunction> withinApply; - std::stack<TNode> visit; + std::vector<TNode> visit; TNode cur; - for (unsigned i = 0; i < ns.size(); i++) + for (unsigned i = 0, size = ns.size(); i < size; i++) { - visit.push(ns[i]); + visit.push_back(ns[i]); withinApply[ns[i]] = false; do { - cur = visit.top(); - visit.pop(); + cur = visit.back(); + visit.pop_back(); - if (visited.find(cur) == visited.end()) + it = visited.find(cur); + if (it == visited.end()) { - visited.insert(cur); - bool curWithinApply = withinApply[cur]; - if (!curWithinApply) + // do not look in nested quantifiers + if (cur.getKind() == FORALL) + { + visited[cur] = cur; + } + else + { + bool curWithinApply = withinApply[cur]; + visited[cur] = Node::null(); + visit.push_back(cur); + for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++) + { + withinApply[cur[j]] = curWithinApply && j == 0; + visit.push_back(cur[j]); + } + } + } + else if (it->second.isNull()) + { + // carry the conversion + Node ret = cur; + bool childChanged = false; + std::vector<Node> children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& nc : cur) + { + it = visited.find(nc); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || nc != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); + } + // now, convert and store the application + if (!withinApply[cur]) { TNode op; - if (cur.getKind() == kind::APPLY_UF) + if (ret.getKind() == kind::APPLY_UF) { // could be a fully applied function variable - op = cur.getOperator(); + op = ret.getOperator(); } - else if (cur.getKind() == kind::HO_APPLY) + else if (ret.getKind() == kind::HO_APPLY) { - op = cur; + op = ret; while (op.getKind() == kind::HO_APPLY) { op = op[0]; @@ -120,42 +162,27 @@ void HigherOrderTrigger::collectHoVarApplyTerms( { if (op.getKind() == kind::INST_CONSTANT) { - Assert(quantifiers::TermUtil::getInstConstAttr(cur) == q); + Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q); Trace("ho-quant-trigger-debug") - << "Ho variable apply term : " << cur << " with head " << op + << "Ho variable apply term : " << ret << " with head " << op << std::endl; - Node app = cur; - if (app.getKind() == kind::APPLY_UF) + if (ret.getKind() == kind::APPLY_UF) { + Node prev = ret; // for consistency, convert to HO_APPLY if fully applied - app = uf::TheoryUfRewriter::getHoApplyForApplyUf(app); + ret = uf::TheoryUfRewriter::getHoApplyForApplyUf(ret); } - apps[op].push_back(cur); - } - if (cur.getKind() == kind::HO_APPLY) - { - curWithinApply = true; + apps[op].push_back(ret); } } } - else - { - if (cur.getKind() != HO_APPLY) - { - curWithinApply = false; - } - } - // do not look in nested quantifiers - if (cur.getKind() != FORALL) - { - for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++) - { - withinApply[cur[i]] = curWithinApply && i == 0; - visit.push(cur[i]); - } - } + visited[cur] = ret; } } while (!visit.empty()); + + // store the conversion + Assert(visited.find(ns[i]) != visited.end()); + ns[i] = visited[ns[i]]; } } diff --git a/src/theory/quantifiers/ho_trigger.h b/src/theory/quantifiers/ho_trigger.h index 16d676353..e5112abce 100644 --- a/src/theory/quantifiers/ho_trigger.h +++ b/src/theory/quantifiers/ho_trigger.h @@ -101,16 +101,18 @@ class HigherOrderTrigger : public Trigger public: /** Collect higher order var apply terms * - * Collect all top-level HO_APPLY terms in n whose head is a variable in - * quantified formula q. Append all such terms in apps. + * Collect all top-level HO_APPLY terms in n whose head is a variable x in + * quantified formula q. Append all such terms in apps[x]. + * This method may modify n so that it is in the expected form required for + * higher-order matching, in particular, APPLY_UF terms with variable + * operators are converted to curried applications of HO_APPLY. */ static void collectHoVarApplyTerms(Node q, - TNode n, + Node& n, std::map<Node, std::vector<Node> >& apps); /** Collect higher order var apply terms * - * Collect all top-level HO_APPLY terms in terms ns whose head is a variable - * in quantified formula q, store in apps. + * Same as above, but with multiple terms ns. */ static void collectHoVarApplyTerms(Node q, std::vector<Node>& ns, diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 4e75f7df8..def9a68bc 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -113,10 +113,19 @@ Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) Node TermUtil::getInstConstAttr( Node n ) { if (!n.hasAttribute(InstConstantAttribute()) ){ Node q; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - q = getInstConstAttr(n[i]); - if( !q.isNull() ){ - break; + if (n.hasOperator()) + { + q = getInstConstAttr(n.getOperator()); + } + if (q.isNull()) + { + for (const Node& nc : n) + { + q = getInstConstAttr(nc); + if (!q.isNull()) + { + break; + } } } InstConstantAttribute ica; @@ -277,6 +286,10 @@ void TermUtil::computeVarContains2( Node n, Kind k, std::vector< Node >& varCont varContains.push_back( n ); } }else{ + if (n.hasOperator()) + { + computeVarContains2(n.getOperator(), k, varContains, visited); + } for( unsigned i=0; i<n.getNumChildren(); i++ ){ computeVarContains2( n[i], k, varContains, visited ); } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 61920250e..d06b5268b 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -223,6 +223,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& Trace("trigger") << "Collect higher-order variable triggers..." << std::endl; std::map<Node, std::vector<Node> > ho_apps; HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps); + Trace("trigger") << "...got " << ho_apps.size() + << " higher-order applications." << std::endl; Trigger* t; if (!ho_apps.empty()) { |