From 9a4deadddfd3d4489ba15f65f0e3dab72b2fcccc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 24 Aug 2021 15:54:31 -0500 Subject: [PATCH] Split higher-order term database (#7045) This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database. This eliminates many of the references to the deprecated option uf-ho. This is work towards eliminating that option. --- src/CMakeLists.txt | 2 + src/expr/skolem_manager.cpp | 1 + src/expr/skolem_manager.h | 2 + .../quantifiers/ematching/ho_trigger.cpp | 7 +- src/theory/quantifiers/ho_term_database.cpp | 252 +++++++++++++++ src/theory/quantifiers/ho_term_database.h | 120 +++++++ src/theory/quantifiers/term_database.cpp | 305 ++++-------------- src/theory/quantifiers/term_database.h | 88 ++--- src/theory/quantifiers/term_registry.cpp | 4 +- 9 files changed, 473 insertions(+), 308 deletions(-) create mode 100644 src/theory/quantifiers/ho_term_database.cpp create mode 100644 src/theory/quantifiers/ho_term_database.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f5af58aeb..306420a2c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -803,6 +803,8 @@ libcvc5_add_sources( theory/quantifiers/fmf/model_engine.h theory/quantifiers/fun_def_evaluator.cpp theory/quantifiers/fun_def_evaluator.h + theory/quantifiers/ho_term_database.cpp + theory/quantifiers/ho_term_database.h theory/quantifiers/index_trie.cpp theory/quantifiers/index_trie.h theory/quantifiers/inst_match.cpp diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 8e1c5e54c..c06f016c4 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -54,6 +54,7 @@ const char* toString(SkolemFunId id) case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR"; case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB"; case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT"; + case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED"; default: return "?"; } } diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index a7d35d155..1d35fa4b5 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -51,6 +51,8 @@ enum class SkolemFunId * i = 0, ..., n. */ RE_UNFOLD_POS_COMPONENT, + /** Higher-order type match predicate, see HoTermDb */ + HO_TYPE_MATCH_PRED, }; /** Converts a skolem function name to a string. */ const char* toString(SkolemFunId id); diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 73a894081..cb4bac254 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -13,14 +13,15 @@ * Implementation of higher-order trigger class. */ +#include "theory/quantifiers/ematching/ho_trigger.h" + #include -#include "theory/quantifiers/ematching/ho_trigger.h" +#include "theory/quantifiers/ho_term_database.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/uf/theory_uf_rewriter.h" @@ -503,7 +504,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() // if a variable of this type occurs in this trigger if (d_ho_var_types.find(stn) != d_ho_var_types.end()) { - Node u = tdb->getHoTypeMatchPredicate(tn); + Node u = HoTermDb::getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); if (d_qim.addPendingLemma(au, InferenceId::QUANTIFIERS_HO_MATCH_PRED)) diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp new file mode 100644 index 000000000..3b97409cc --- /dev/null +++ b/src/theory/quantifiers/ho_term_database.cpp @@ -0,0 +1,252 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of higher-order term database class. + */ + +#include "theory/quantifiers/ho_term_database.h" + +#include "expr/skolem_manager.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/rewriter.h" +#include "theory/uf/equality_engine.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +HoTermDb::HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr) + : TermDb(qs, qr) +{ +} + +HoTermDb::~HoTermDb() {} + +void HoTermDb::addTermInternal(Node n) +{ + if (n.getType().isFunction()) + { + // nothing special to do with functions + return; + } + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node curr = n; + std::vector args; + while (curr.getKind() == HO_APPLY) + { + args.insert(args.begin(), curr[1]); + curr = curr[0]; + if (!curr.isVar()) + { + // purify the term + std::map::iterator itp = d_hoFunOpPurify.find(curr); + Node psk; + if (itp == d_hoFunOpPurify.end()) + { + psk = sm->mkPurifySkolem( + curr, "pfun", "purify for function operator term indexing"); + d_hoFunOpPurify[curr] = psk; + // we do not add it to d_ops since it is an internal operator + } + else + { + psk = itp->second; + } + std::vector children; + children.push_back(psk); + children.insert(children.end(), args.begin(), args.end()); + Node p_n = nm->mkNode(APPLY_UF, children); + Trace("term-db") << "register term in db (via purify) " << p_n + << std::endl; + // also add this one internally + DbList* dblp = getOrMkDbListForOp(psk); + dblp->d_list.push_back(p_n); + // maintain backwards mapping + d_hoPurifyToTerm[p_n] = n; + } + } + if (!args.empty() && curr.isVar()) + { + // also add standard application version + args.insert(args.begin(), curr); + Node uf_n = nm->mkNode(APPLY_UF, args); + addTerm(uf_n); + } +} + +void HoTermDb::getOperatorsFor(TNode f, std::vector& ops) +{ + ops.push_back(f); + ops.insert(ops.end(), d_hoOpSlaves[f].begin(), d_hoOpSlaves[f].end()); +} + +Node HoTermDb::getOperatorRepresentative(TNode op) const +{ + std::map::const_iterator it = d_hoOpRep.find(op); + if (it != d_hoOpRep.end()) + { + return it->second; + } + return op; +} + +bool HoTermDb::resetInternal(Theory::Effort effort) +{ + Trace("quant-ho") + << "HoTermDb::reset : assert higher-order purify equalities..." + << std::endl; + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); + for (std::pair& pp : d_hoPurifyToTerm) + { + if (ee->hasTerm(pp.second) + && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first))) + { + Node eq; + std::map::iterator itpe = d_hoPurifyToEq.find(pp.first); + if (itpe == d_hoPurifyToEq.end()) + { + eq = Rewriter::rewrite(pp.first.eqNode(pp.second)); + d_hoPurifyToEq[pp.first] = eq; + } + else + { + eq = itpe->second; + } + Trace("quant-ho") << "- assert purify equality : " << eq << std::endl; + // Note that ee may be the central equality engine, in which case this + // equality is explained trivially with "true", since both sides of + // eq are HOL and FOL encodings of the same thing. + ee->assertEquality(eq, true, d_true); + if (!ee->consistent()) + { + // In some rare cases, purification functions (in the domain of + // d_hoPurifyToTerm) may escape the term database. For example, + // matching algorithms may construct instantiations involving these + // functions. As a result, asserting these equalities internally may + // cause a conflict. In this case, we insist that the purification + // equality is sent out as a lemma here. + Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl; + d_qim->addPendingLemma(eq, InferenceId::QUANTIFIERS_HO_PURIFY); + d_qstate.notifyInConflict(); + d_consistent_ee = false; + return false; + } + } + } + return true; +} + +bool HoTermDb::finishResetInternal(Theory::Effort effort) +{ + if (!d_qstate.options().quantifiers.hoMergeTermDb) + { + return true; + } + Trace("quant-ho") << "HoTermDb::reset : compute equal functions..." + << std::endl; + // build operator representative map + d_hoOpRep.clear(); + d_hoOpSlaves.clear(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + while (!eqcs_i.isFinished()) + { + TNode r = (*eqcs_i); + if (r.getType().isFunction()) + { + Trace("quant-ho") << " process function eqc " << r << std::endl; + Node first; + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); + while (!eqc_i.isFinished()) + { + TNode n = (*eqc_i); + Node n_use; + if (n.isVar()) + { + n_use = n; + } + else + { + // use its purified variable, if it exists + std::map::iterator itp = d_hoFunOpPurify.find(n); + if (itp != d_hoFunOpPurify.end()) + { + n_use = itp->second; + } + } + Trace("quant-ho") << " - process " << n_use << ", from " << n + << std::endl; + if (!n_use.isNull() && d_opMap.find(n_use) != d_opMap.end()) + { + if (first.isNull()) + { + first = n_use; + d_hoOpRep[n_use] = n_use; + } + else + { + Trace("quant-ho") << " have : " << n_use << " == " << first + << ", type = " << n_use.getType() << std::endl; + d_hoOpRep[n_use] = first; + d_hoOpSlaves[first].push_back(n_use); + } + } + ++eqc_i; + } + } + ++eqcs_i; + } + Trace("quant-ho") << "...finished compute equal functions." << std::endl; + + return true; +} +bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) +{ + if (!d_qstate.areDisequal(a, b)) + { + return false; + } + exp.push_back(a.eqNode(b)); + // operators might be disequal + Node af = getMatchOperator(a); + Node bf = getMatchOperator(b); + if (af != bf) + { + if (a.getKind() == APPLY_UF && b.getKind() == APPLY_UF) + { + exp.push_back(af.eqNode(bf).negate()); + } + else + { + Assert(false); + return false; + } + } + return true; +} + +Node HoTermDb::getHoTypeMatchPredicate(TypeNode tn) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType()); + return sm->mkSkolemFunction(SkolemFunId::HO_TYPE_MATCH_PRED, ptn); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/ho_term_database.h b/src/theory/quantifiers/ho_term_database.h new file mode 100644 index 000000000..12bf0b49f --- /dev/null +++ b/src/theory/quantifiers/ho_term_database.h @@ -0,0 +1,120 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Higher-order term database class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__HO_TERM_DATABASE_H +#define CVC5__THEORY__QUANTIFIERS__HO_TERM_DATABASE_H + +#include + +#include "expr/node.h" +#include "theory/quantifiers/term_database.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +/** + * Higher-order term database, which extends the normal term database based on + * techniques from Barbosa et al CADE 2019. + */ +class HoTermDb : public TermDb +{ + public: + HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr); + ~HoTermDb(); + /** identify */ + std::string identify() const override { return "HoTermDb"; } + /** get higher-order type match predicate + * + * This predicate is used to force certain functions f of type tn to appear as + * first-class representatives in the quantifier-free UF solver. For a typical + * use case, we call getHoTypeMatchPredicate which returns a fresh predicate + * P of type (tn -> Bool). Then, we add P( f ) as a lemma. + */ + static Node getHoTypeMatchPredicate(TypeNode tn); + + private: + /** + * Reset internal, called when reset(e) is called. Returning false will cause + * the overall reset to terminate early, returning false. + */ + bool resetInternal(Theory::Effort e) override; + /** Performs merging of term indices based on higher-order reasoning */ + bool finishResetInternal(Theory::Effort e) override; + /** add term higher-order + * + * This registers additional terms corresponding to (possibly multiple) + * purifications of a higher-order term n. + * + * Consider the example: + * g : Int -> Int, f : Int x Int -> Int + * constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3 + * pattern: (g x) + * where @ is HO_APPLY. + * We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1). + * With the standard registration in addTerm, we construct term indices for + * f, g, @ : Int x Int -> Int, @ : Int -> Int. + * However, to match (g x) with (@ (@ f 0) 1), we require that + * [1] -> (@ (@ f 0) 1) + * is an entry in the term index of g. To do this, we maintain a term + * index for a fresh variable pfun, the purification variable for + * (@ f 0). Thus, we register the term (pfun 1) in the call to this function + * for (@ (@ f 0) 1). This ensures that, when processing the equality + * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry + * [1] -> (@ (@ f 0) 1) + * is added to the term index of g, assuming g is the representative of + * the equivalence class of g and pfun. + * + * Above, we set d_hoFunOpPurify[(@ f 0)] = pfun, and + * d_hoPurifyToTerm[(pfun 1)] = (@ (@ f 0) 1). + */ + void addTermInternal(Node n) override; + /** Get operators that we know are equivalent to f */ + void getOperatorsFor(TNode f, std::vector& ops) override; + /** get the chosen representative for operator op */ + Node getOperatorRepresentative(TNode op) const override; + /** check if we are in conflict based on congruent terms a and b */ + bool checkCongruentDisequal(TNode a, + TNode b, + std::vector& exp) override; + //------------------------------higher-order term indexing + /** + * Map from non-variable function terms to the operator used to purify it in + * this database. For details, see addTermHo. + */ + std::map d_hoFunOpPurify; + /** + * Map from terms to the term that they purified. For details, see addTermHo. + */ + std::map d_hoPurifyToTerm; + /** + * Map from terms in the domain of the above map to an equality between that + * term and its range in the above map. + */ + std::map d_hoPurifyToEq; + /** a map from matchable operators to their representative */ + std::map d_hoOpRep; + /** for each representative matchable operator, the list of other matchable + * operators in their equivalence class */ + std::map > d_hoOpSlaves; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__QUANTIFIERS__HO_TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 655fd2df7..d2f872afb 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -224,10 +224,7 @@ void TermDb::addTerm(Node n) DbList* dlo = getOrMkDbListForOp(op); dlo->d_list.push_back(n); // If we are higher-order, we may need to register more terms. - if (options::ufHo()) - { - addTermHo(n); - } + addTermInternal(n); } } else @@ -290,11 +287,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { d_func_map_eqc_trie[f].clear(); // get the matchable operators in the equivalence class of f std::vector ops; - ops.push_back(f); - if (options::ufHo()) - { - ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); - } + getOperatorsFor(f, ops); eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); for (TNode ff : ops) { @@ -321,11 +314,7 @@ void TermDb::computeUfTerms( TNode f ) { d_op_nonred_count[f] = 0; // get the matchable operators in the equivalence class of f std::vector ops; - ops.push_back(f); - if (options::ufHo()) - { - ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); - } + getOperatorsFor(f, ops); Trace("term-db-debug") << "computeUfTerms for " << f << std::endl; unsigned congruentCount = 0; unsigned nonCongruentCount = 0; @@ -385,60 +374,34 @@ void TermDb::computeUfTerms( TNode f ) { congruentCount++; continue; } - if (d_qstate.areDisequal(at, n)) + std::vector lits; + if (checkCongruentDisequal(at, n, lits)) { - std::vector lits; - lits.push_back(nm->mkNode(EQUAL, at, n)); - bool success = true; - if (options::ufHo()) + Assert(at.getNumChildren() == n.getNumChildren()); + for (size_t k = 0, size = at.getNumChildren(); k < size; k++) { - // operators might be disequal - if (ops.size() > 1) + if (at[k] != n[k]) { - Node atf = getMatchOperator(at); - Node nf = getMatchOperator(n); - if (atf != nf) - { - if (at.getKind() == APPLY_UF && n.getKind() == APPLY_UF) - { - lits.push_back(atf.eqNode(nf).negate()); - } - else - { - success = false; - Assert(false); - } - } + lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate()); } } - if (success) + Node lem = nm->mkOr(lits); + if (Trace.isOn("term-db-lemma")) { - Assert(at.getNumChildren() == n.getNumChildren()); - for (unsigned k = 0, size = at.getNumChildren(); k < size; k++) - { - if (at[k] != n[k]) - { - lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate()); - } - } - Node lem = lits.size() == 1 ? lits[0] : nm->mkNode(OR, lits); - if (Trace.isOn("term-db-lemma")) + Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " + << n << "!!!!" << std::endl; + if (!d_qstate.getValuation().needCheck()) { - Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " - << n << "!!!!" << std::endl; - if (!d_qstate.getValuation().needCheck()) - { - Trace("term-db-lemma") << " all theories passed with no lemmas." - << std::endl; - // we should be a full effort check, prior to theory combination - } - Trace("term-db-lemma") << " add lemma : " << lem << std::endl; + Trace("term-db-lemma") + << " all theories passed with no lemmas." << std::endl; + // we should be a full effort check, prior to theory combination } - d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG); - d_qstate.notifyInConflict(); - d_consistent_ee = false; - return; + Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } + d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG); + d_qstate.notifyInConflict(); + d_consistent_ee = false; + return; } nonCongruentCount++; d_op_nonred_count[f]++; @@ -457,73 +420,21 @@ void TermDb::computeUfTerms( TNode f ) { } } -void TermDb::addTermHo(Node n) +Node TermDb::getOperatorRepresentative(TNode op) const { return op; } + +bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) { - Assert(options::ufHo()); - if (n.getType().isFunction()) - { - // nothing special to do with functions - return; - } - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - Node curr = n; - std::vector args; - while (curr.getKind() == HO_APPLY) + if (d_qstate.areDisequal(a, b)) { - args.insert(args.begin(), curr[1]); - curr = curr[0]; - if (!curr.isVar()) - { - // purify the term - std::map::iterator itp = d_ho_fun_op_purify.find(curr); - Node psk; - if (itp == d_ho_fun_op_purify.end()) - { - psk = sm->mkPurifySkolem( - curr, "pfun", "purify for function operator term indexing"); - d_ho_fun_op_purify[curr] = psk; - // we do not add it to d_ops since it is an internal operator - } - else - { - psk = itp->second; - } - std::vector children; - children.push_back(psk); - children.insert(children.end(), args.begin(), args.end()); - Node p_n = nm->mkNode(APPLY_UF, children); - Trace("term-db") << "register term in db (via purify) " << p_n - << std::endl; - // also add this one internally - DbList* dblp = getOrMkDbListForOp(psk); - dblp->d_list.push_back(p_n); - // maintain backwards mapping - d_ho_purify_to_term[p_n] = n; - } - } - if (!args.empty() && curr.isVar()) - { - // also add standard application version - args.insert(args.begin(), curr); - Node uf_n = nm->mkNode(APPLY_UF, args); - addTerm(uf_n); - } -} - -Node TermDb::getOperatorRepresentative( TNode op ) const { - std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op ); - if( it!=d_ho_op_rep.end() ){ - return it->second; - }else{ - return op; + exp.push_back(a.eqNode(b)); + return true; } + return false; } bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { - if( options::ufHo() ){ - f = getOperatorRepresentative( f ); - } + // notice if we are not higher-order, getOperatorRepresentative is a no-op + f = getOperatorRepresentative(f); computeUfTerms( f ); Assert(!d_qstate.getEqualityEngine()->hasTerm(r) || d_qstate.getEqualityEngine()->getRepresentative(r) == r); @@ -981,6 +892,28 @@ Node TermDb::getEligibleTermInEqc( TNode r ) { } } +bool TermDb::resetInternal(Theory::Effort e) +{ + // do nothing + return true; +} + +bool TermDb::finishResetInternal(Theory::Effort e) +{ + // do nothing + return true; +} + +void TermDb::addTermInternal(Node n) +{ + // do nothing +} + +void TermDb::getOperatorsFor(TNode f, std::vector& ops) +{ + ops.push_back(f); +} + void TermDb::setHasTerm( Node n ) { Trace("term-db-debug2") << "hasTerm : " << n << std::endl; if( d_has_map.find( n )==d_has_map.end() ){ @@ -1011,49 +944,9 @@ bool TermDb::reset( Theory::Effort effort ){ Assert(ee->consistent()); // if higher-order, add equalities for the purification terms now - if (options::ufHo()) + if (!resetInternal(effort)) { - Trace("quant-ho") - << "TermDb::reset : assert higher-order purify equalities..." - << std::endl; - for (std::pair& pp : d_ho_purify_to_term) - { - if (ee->hasTerm(pp.second) - && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first))) - { - Node eq; - std::map::iterator itpe = d_ho_purify_to_eq.find(pp.first); - if (itpe == d_ho_purify_to_eq.end()) - { - eq = Rewriter::rewrite(pp.first.eqNode(pp.second)); - d_ho_purify_to_eq[pp.first] = eq; - } - else - { - eq = itpe->second; - } - Trace("quant-ho") << "- assert purify equality : " << eq << std::endl; - // Note that ee may be the central equality engine, in which case this - // equality is explained trivially with "true", since both sides of - // eq are HOL and FOL encodings of the same thing. - ee->assertEquality(eq, true, d_true); - if (!ee->consistent()) - { - // In some rare cases, purification functions (in the domain of - // d_ho_purify_to_term) may escape the term database. For example, - // matching algorithms may construct instantiations involving these - // functions. As a result, asserting these equalities internally may - // cause a conflict. In this case, we insist that the purification - // equality is sent out as a lemma here. - Trace("term-db-lemma") - << "Purify equality lemma: " << eq << std::endl; - d_qim->addPendingLemma(eq, InferenceId::QUANTIFIERS_HO_PURIFY); - d_qstate.notifyInConflict(); - d_consistent_ee = false; - return false; - } - } - } + return false; } //compute has map @@ -1100,68 +993,13 @@ bool TermDb::reset( Theory::Effort effort ){ } } } - - if( options::ufHo() && options::hoMergeTermDb() ){ - Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl; - // build operator representative map - d_ho_op_rep.clear(); - d_ho_op_slaves.clear(); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - if( r.getType().isFunction() ){ - Trace("quant-ho") << " process function eqc " << r << std::endl; - Node first; - eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); - while( !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - Node n_use; - if (n.isVar()) - { - n_use = n; - } - else - { - // use its purified variable, if it exists - std::map::iterator itp = d_ho_fun_op_purify.find(n); - if (itp != d_ho_fun_op_purify.end()) - { - n_use = itp->second; - } - } - Trace("quant-ho") << " - process " << n_use << ", from " << n - << std::endl; - if (!n_use.isNull() && d_opMap.find(n_use) != d_opMap.end()) - { - if (first.isNull()) - { - first = n_use; - d_ho_op_rep[n_use] = n_use; - } - else - { - Trace("quant-ho") << " have : " << n_use << " == " << first - << ", type = " << n_use.getType() << std::endl; - d_ho_op_rep[n_use] = first; - d_ho_op_slaves[first].push_back(n_use); - } - } - ++eqc_i; - } - } - ++eqcs_i; - } - Trace("quant-ho") << "...finished compute equal functions." << std::endl; - } - - return true; + // finish reset + return finishResetInternal(effort); } TNodeTrie* TermDb::getTermArgTrie(Node f) { - if( options::ufHo() ){ - f = getOperatorRepresentative( f ); - } + f = getOperatorRepresentative(f); computeUfTerms( f ); std::map::iterator itut = d_func_map_trie.find(f); if( itut!=d_func_map_trie.end() ){ @@ -1173,9 +1011,7 @@ TNodeTrie* TermDb::getTermArgTrie(Node f) TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f) { - if( options::ufHo() ){ - f = getOperatorRepresentative( f ); - } + f = getOperatorRepresentative(f); computeUfEqcTerms( f ); std::map::iterator itut = d_func_map_eqc_trie.find(f); if( itut==d_func_map_eqc_trie.end() ){ @@ -1196,9 +1032,7 @@ TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f) } TNode TermDb::getCongruentTerm( Node f, Node n ) { - if( options::ufHo() ){ - f = getOperatorRepresentative( f ); - } + f = getOperatorRepresentative(f); computeUfTerms( f ); std::map::iterator itut = d_func_map_trie.find(f); if( itut!=d_func_map_trie.end() ){ @@ -1210,28 +1044,11 @@ TNode TermDb::getCongruentTerm( Node f, Node n ) { } TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { - if( options::ufHo() ){ - f = getOperatorRepresentative( f ); - } + f = getOperatorRepresentative(f); computeUfTerms( f ); return d_func_map_trie[f].existsTerm( args ); } -Node TermDb::getHoTypeMatchPredicate(TypeNode tn) -{ - std::map::iterator ithp = d_ho_type_match_pred.find(tn); - if (ithp != d_ho_type_match_pred.end()) - { - return ithp->second; - } - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType()); - Node k = sm->mkDummySkolem("U", ptn, "predicate to force higher-order types"); - d_ho_type_match_pred[tn] = k; - return k; -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 72126302f..a4e95487c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -75,7 +75,7 @@ class TermDb : public QuantifiersUtil { public: TermDb(QuantifiersState& qs, QuantifiersRegistry& qr); - ~TermDb(); + virtual ~TermDb(); /** Finish init, which sets the inference manager */ void finishInit(QuantifiersInferenceManager* qim); /** presolve (called once per user check-sat) */ @@ -279,16 +279,8 @@ class TermDb : public QuantifiersUtil { bool isTermEligibleForInstantiation(TNode n, TNode f); /** get eligible term in equivalence class of r */ Node getEligibleTermInEqc(TNode r); - /** get higher-order type match predicate - * - * This predicate is used to force certain functions f of type tn to appear as - * first-class representatives in the quantifier-free UF solver. For a typical - * use case, we call getHoTypeMatchPredicate which returns a fresh predicate - * P of type (tn -> Bool). Then, we add P( f ) as a lemma. - */ - Node getHoTypeMatchPredicate(TypeNode tn); - private: + protected: /** The quantifiers state object */ QuantifiersState& d_qstate; /** Pointer to the quantifiers inference manager */ @@ -336,6 +328,32 @@ class TermDb : public QuantifiersUtil { * of equality engine (for higher-order). */ std::map d_ho_type_match_pred; + //----------------------------- implementation-specific + /** + * Reset internal, called when reset(e) is called. Returning false will cause + * the overall reset to terminate early, returning false. + */ + virtual bool resetInternal(Theory::Effort e); + /** + * Finish reset internal, called at the end of reset(e). Returning false will + * cause the overall reset to return false. + */ + virtual bool finishResetInternal(Theory::Effort e); + /** Add term internal, called when addTerm(n) is called */ + virtual void addTermInternal(Node n); + /** Get operators that we know are equivalent to f, typically only f itself */ + virtual void getOperatorsFor(TNode f, std::vector& ops); + /** get the chosen representative for operator op */ + virtual Node getOperatorRepresentative(TNode op) const; + /** + * This method is called when terms a and b are indexed by the same operator, + * and have equivalent arguments. This method checks if we are in conflict, + * which is the case if a and b are disequal in the equality engine. + * If so, it adds the set of literals that are implied but do not hold, e.g. + * the equality (= a b). + */ + virtual bool checkCongruentDisequal(TNode a, TNode b, std::vector& exp); + //----------------------------- end implementation-specific /** set has term */ void setHasTerm( Node n ); /** helper for evaluate term */ @@ -368,56 +386,6 @@ class TermDb : public QuantifiersUtil { * Ensure that an entry for n is in d_arg_reps */ void computeArgReps(TNode n); - //------------------------------higher-order term indexing - /** - * Map from non-variable function terms to the operator used to purify it in - * this database. For details, see addTermHo. - */ - std::map d_ho_fun_op_purify; - /** - * Map from terms to the term that they purified. For details, see addTermHo. - */ - std::map d_ho_purify_to_term; - /** - * Map from terms in the domain of the above map to an equality between that - * term and its range in the above map. - */ - std::map d_ho_purify_to_eq; - /** a map from matchable operators to their representative */ - std::map< TNode, TNode > d_ho_op_rep; - /** for each representative matchable operator, the list of other matchable operators in their equivalence class */ - std::map > d_ho_op_slaves; - /** add term higher-order - * - * This registers additional terms corresponding to (possibly multiple) - * purifications of a higher-order term n. - * - * Consider the example: - * g : Int -> Int, f : Int x Int -> Int - * constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3 - * pattern: (g x) - * where @ is HO_APPLY. - * We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1). - * With the standard registration in addTerm, we construct term indices for - * f, g, @ : Int x Int -> Int, @ : Int -> Int. - * However, to match (g x) with (@ (@ f 0) 1), we require that - * [1] -> (@ (@ f 0) 1) - * is an entry in the term index of g. To do this, we maintain a term - * index for a fresh variable pfun, the purification variable for - * (@ f 0). Thus, we register the term (pfun 1) in the call to this function - * for (@ (@ f 0) 1). This ensures that, when processing the equality - * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry - * [1] -> (@ (@ f 0) 1) - * is added to the term index of g, assuming g is the representative of - * the equivalence class of g and pfun. - * - * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and - * d_ho_purify_to_term[(pfun 1)] = (@ (@ f 0) 1). - */ - void addTermHo(Node n); - /** get operator representative */ - Node getOperatorRepresentative( TNode op ) const; - //------------------------------end higher-order term indexing };/* class TermDb */ } // namespace quantifiers diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 3d17099cb..324217798 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -20,6 +20,7 @@ #include "options/smt_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" +#include "theory/quantifiers/ho_term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" @@ -33,7 +34,8 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) d_presolveCache(qs.getUserContext()), d_termEnum(new TermEnumeration), d_termPools(new TermPools(qs)), - d_termDb(new TermDb(qs, qr)), + d_termDb(qs.getEnv().getLogicInfo().isHigherOrder() ? new HoTermDb(qs, qr) + : new TermDb(qs, qr)), d_sygusTdb(nullptr), d_qmodel(nullptr) { -- 2.30.2