From f3270fb3629cbc62012ae7eb30843a1bc6d4e3c2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 25 Nov 2017 14:12:00 -0600 Subject: [PATCH] Fixes for higher-order (#1405) --- src/theory/quantifiers/ho_trigger.cpp | 109 ++++++++++++++++---------- src/theory/quantifiers/ho_trigger.h | 12 +-- src/theory/quantifiers/term_util.cpp | 21 ++++- src/theory/quantifiers/trigger.cpp | 2 + test/regress/regress0/ho/Makefile.am | 16 ++-- 5 files changed, 101 insertions(+), 59 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 >& apps) + Node q, Node& n, std::map >& apps) { std::vector ns; ns.push_back(n); collectHoVarApplyTerms(q, ns, apps); + Assert(ns.size() == 1); + n = ns[0]; } void HigherOrderTrigger::collectHoVarApplyTerms( Node q, std::vector& ns, std::map >& apps) { - std::unordered_set visited; + std::unordered_map visited; + std::unordered_map::iterator it; // whether the visited node is a child of a HO_APPLY chain std::unordered_map withinApply; - std::stack visit; + std::vector 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 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 >& 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& 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& varCont varContains.push_back( n ); } }else{ + if (n.hasOperator()) + { + computeVarContains2(n.getOperator(), k, varContains, visited); + } for( unsigned i=0; i& Trace("trigger") << "Collect higher-order variable triggers..." << std::endl; std::map > 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()) { diff --git a/test/regress/regress0/ho/Makefile.am b/test/regress/regress0/ho/Makefile.am index b6c494d29..4a7ceb96f 100644 --- a/test/regress/regress0/ho/Makefile.am +++ b/test/regress/regress0/ho/Makefile.am @@ -37,18 +37,16 @@ TESTS = \ ho-std-fmf.smt2 \ fta0409.smt2 \ auth0068.smt2 \ - modulo-func-equality.smt2 - + modulo-func-equality.smt2 \ + ho-matching-enum.smt2 \ + ho-matching-enum-2.smt2 \ + ho-matching-nested-app.smt2 \ + simple-matching.smt2 \ + simple-matching-partial.smt2 + EXTRA_DIST = $(TESTS) -# need PR 1204 : - # hoa0102.smt2 -# ho-matching-enum.smt2 -# ho-matching-enum-2.smt2 -# ho-matching-nested-app.smt2 -# simple-matching.smt2 -# simple-matching-partial.smt2 #if CVC4_BUILD_PROFILE_COMPETITION -- 2.30.2