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.
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
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 "?";
}
}
* 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);
* Implementation of higher-order trigger class.
*/
+#include "theory/quantifiers/ematching/ho_trigger.h"
+
#include <stack>
-#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"
// 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))
--- /dev/null
+/******************************************************************************
+ * 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<Node> args;
+ while (curr.getKind() == HO_APPLY)
+ {
+ args.insert(args.begin(), curr[1]);
+ curr = curr[0];
+ if (!curr.isVar())
+ {
+ // purify the term
+ std::map<Node, Node>::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<Node> 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<TNode>& 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<TNode, TNode>::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<const Node, Node>& pp : d_hoPurifyToTerm)
+ {
+ if (ee->hasTerm(pp.second)
+ && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first)))
+ {
+ Node eq;
+ std::map<Node, Node>::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<Node, Node>::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<Node>& 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
--- /dev/null
+/******************************************************************************
+ * 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 <map>
+
+#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<TNode>& 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<Node>& 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<Node, Node> d_hoFunOpPurify;
+ /**
+ * Map from terms to the term that they purified. For details, see addTermHo.
+ */
+ std::map<Node, Node> 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<Node, Node> d_hoPurifyToEq;
+ /** a map from matchable operators to their representative */
+ std::map<TNode, TNode> d_hoOpRep;
+ /** for each representative matchable operator, the list of other matchable
+ * operators in their equivalence class */
+ std::map<TNode, std::vector<TNode> > d_hoOpSlaves;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS__HO_TERM_DATABASE_H */
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
d_func_map_eqc_trie[f].clear();
// get the matchable operators in the equivalence class of f
std::vector<TNode> 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)
{
d_op_nonred_count[f] = 0;
// get the matchable operators in the equivalence class of f
std::vector<TNode> 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;
congruentCount++;
continue;
}
- if (d_qstate.areDisequal(at, n))
+ std::vector<Node> lits;
+ if (checkCongruentDisequal(at, n, lits))
{
- std::vector<Node> 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]++;
}
}
-void TermDb::addTermHo(Node n)
+Node TermDb::getOperatorRepresentative(TNode op) const { return op; }
+
+bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& 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<Node> 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<Node, Node>::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<Node> 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);
}
}
+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<TNode>& 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() ){
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<const Node, Node>& 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<Node, Node>::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
}
}
}
-
- 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<Node, Node>::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<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
if( itut!=d_func_map_trie.end() ){
TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
{
- if( options::ufHo() ){
- f = getOperatorRepresentative( f );
- }
+ f = getOperatorRepresentative(f);
computeUfEqcTerms( f );
std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
if( itut==d_func_map_eqc_trie.end() ){
}
TNode TermDb::getCongruentTerm( Node f, Node n ) {
- if( options::ufHo() ){
- f = getOperatorRepresentative( f );
- }
+ f = getOperatorRepresentative(f);
computeUfTerms( f );
std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
if( itut!=d_func_map_trie.end() ){
}
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<TypeNode, Node>::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
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) */
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 */
* of equality engine (for higher-order).
*/
std::map<TypeNode, Node> 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<TNode>& 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<Node>& exp);
+ //----------------------------- end implementation-specific
/** set has term */
void setHasTerm( Node n );
/** helper for evaluate term */
* 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<Node, Node> d_ho_fun_op_purify;
- /**
- * Map from terms to the term that they purified. For details, see addTermHo.
- */
- std::map<Node, Node> 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<Node, Node> 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<TNode, std::vector<TNode> > 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
#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"
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)
{
projects / cvc5.git / commitdiff