/********************* */ /*! \file inst_match_trie.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2019 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.\endverbatim ** ** \brief inst match class **/ #include "cvc4_private.h" #ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H #define CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H #include #include "context/cdlist.h" #include "context/cdo.h" #include "expr/node.h" #include "theory/quantifiers/inst_match.h" namespace CVC4 { namespace theory { class QuantifiersEngine; class EqualityQuery; namespace inst { /** trie for InstMatch objects * * This class is used for storing instantiations of a quantified formula q. * It is a trie data structure for which entries can be added and removed. * This class has interfaces for adding instantiations that are either * represented by std::vectors or InstMatch objects (see inst_match.h). */ class InstMatchTrie { public: /** index ordering */ class ImtIndexOrder { public: std::vector d_order; }; public: InstMatchTrie() {} ~InstMatchTrie() {} /** exists inst match * * This method considers the entry given by m, starting at the given index. * The domain of m is the bound variables of quantified formula q. * It returns true if (the suffix) of m exists in this trie. * If modEq is true, we check for duplication modulo equality the current * equalities in the active equality engine of qe. */ bool existsInstMatch(QuantifiersEngine* qe, Node q, InstMatch& m, bool modEq = false, ImtIndexOrder* imtio = NULL, unsigned index = 0) { return !addInstMatch(qe, q, m, modEq, imtio, true, index); } /** exists inst match, vector version */ bool existsInstMatch(QuantifiersEngine* qe, Node q, std::vector& m, bool modEq = false, ImtIndexOrder* imtio = NULL, unsigned index = 0) { return !addInstMatch(qe, q, m, modEq, imtio, true, index); } /** add inst match * * This method adds (the suffix of) m starting at the given index to this * trie, and returns true if and only if m did not already occur in this trie. * The domain of m is the bound variables of quantified formula q. * If modEq is true, we check for duplication modulo equality the current * equalities in the active equality engine of qe. */ bool addInstMatch(QuantifiersEngine* qe, Node q, InstMatch& m, bool modEq = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, unsigned index = 0) { return addInstMatch(qe, q, m.d_vals, modEq, imtio, onlyExist, index); } /** add inst match, vector version */ bool addInstMatch(QuantifiersEngine* qe, Node f, std::vector& m, bool modEq = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, unsigned index = 0); /** remove inst match * * This removes (the suffix of) m starting at the given index from this trie. * It returns true if and only if this entry existed in this trie. * The domain of m is the bound variables of quantified formula q. */ bool removeInstMatch(Node f, std::vector& m, ImtIndexOrder* imtio = NULL, unsigned index = 0); /** record instantiation lemma * * This records that the instantiation lemma lem corresponds to the entry * given by (the suffix of) m starting at the given index. */ bool recordInstLemma(Node q, std::vector& m, Node lem, ImtIndexOrder* imtio = NULL, unsigned index = 0); /** get instantiations * * This gets the set of instantiation lemmas that were recorded in this trie * via calls to recordInstLemma. If useActive is true, we only add * instantiations that occur in active. */ void getInstantiations(std::vector& insts, Node q, QuantifiersEngine* qe, bool useActive, std::vector& active) { std::vector terms; getInstantiations(insts, q, terms, qe, useActive, active); } /** get explanation for inst lemmas * * This gets the explanation for the instantiation lemmas in lems for * quantified formula q, for which this trie stores instantiation matches for. * For each instantiation lemma lem recording in this trie via calls to * recordInstLemma, we map lem to q in map quant, and lem to its corresponding * vector of terms in tvec. */ void getExplanationForInstLemmas( Node q, const std::vector& lems, std::map& quant, std::map >& tvec) const { std::vector terms; getExplanationForInstLemmas(q, terms, lems, quant, tvec); } /** clear the data of this class */ void clear() { d_data.clear(); } /** print this class */ void print(std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector& active) const { std::vector terms; print(out, q, terms, firstTime, useActive, active); } /** the data */ std::map d_data; private: /** helper for print * terms accumulates the path we are on in the trie. */ void print(std::ostream& out, Node q, std::vector& terms, bool& firstTime, bool useActive, std::vector& active) const; /** helper for get instantiations * terms accumulates the path we are on in the trie. */ void getInstantiations(std::vector& insts, Node q, std::vector& terms, QuantifiersEngine* qe, bool useActive, std::vector& active) const; /** helper for get explantaion for inst lemmas * terms accumulates the path we are on in the trie. */ void getExplanationForInstLemmas( Node q, std::vector& terms, const std::vector& lems, std::map& quant, std::map >& tvec) const; /** set instantiation lemma at this node in the trie */ void setInstLemma(Node n) { d_data.clear(); d_data[n].clear(); } /** does this node of the trie store an instantiation lemma? */ bool hasInstLemma() const { return !d_data.empty(); } /** get the instantiation lemma stored in this node of the trie */ Node getInstLemma() const { return d_data.begin()->first; } }; /** trie for InstMatch objects * * This is a context-dependent version of the above class. */ class CDInstMatchTrie { public: CDInstMatchTrie(context::Context* c) : d_valid(c, false) {} ~CDInstMatchTrie(); /** exists inst match * * This method considers the entry given by m, starting at the given index. * The domain of m is the bound variables of quantified formula q. * It returns true if (the suffix) of m exists in this trie. * If modEq is true, we check for duplication modulo equality the current * equalities in the active equality engine of qe. * It additionally takes a context c, for which the entry is valid in. */ bool existsInstMatch(QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, unsigned index = 0) { return !addInstMatch(qe, q, m, c, modEq, index, true); } /** exists inst match, vector version */ bool existsInstMatch(QuantifiersEngine* qe, Node q, std::vector& m, context::Context* c, bool modEq = false, unsigned index = 0) { return !addInstMatch(qe, q, m, c, modEq, index, true); } /** add inst match * * This method adds (the suffix of) m starting at the given index to this * trie, and returns true if and only if m did not already occur in this trie. * The domain of m is the bound variables of quantified formula q. * If modEq is true, we check for duplication modulo equality the current * equalities in the active equality engine of qe. * It additionally takes a context c, for which the entry is valid in. */ bool addInstMatch(QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, unsigned index = 0, bool onlyExist = false) { return addInstMatch(qe, q, m.d_vals, c, modEq, index, onlyExist); } /** add inst match, vector version */ bool addInstMatch(QuantifiersEngine* qe, Node q, std::vector& m, context::Context* c, bool modEq = false, unsigned index = 0, bool onlyExist = false); /** remove inst match * * This removes (the suffix of) m starting at the given index from this trie. * It returns true if and only if this entry existed in this trie. * The domain of m is the bound variables of quantified formula q. */ bool removeInstMatch(Node q, std::vector& m, unsigned index = 0); /** record instantiation lemma * * This records that the instantiation lemma lem corresponds to the entry * given by (the suffix of) m starting at the given index. */ bool recordInstLemma(Node q, std::vector& m, Node lem, unsigned index = 0); /** get instantiations * * This gets the set of instantiation lemmas that were recorded in this class * via calls to recordInstLemma. If useActive is true, we only add * instantiations that occur in active. */ void getInstantiations(std::vector& insts, Node q, QuantifiersEngine* qe, bool useActive, std::vector& active) { std::vector terms; getInstantiations(insts, q, terms, qe, useActive, active); } /** get explanation for inst lemmas * * This gets the explanation for the instantiation lemmas in lems for * quantified formula q, for which this trie stores instantiation matches for. * For each instantiation lemma lem recording in this trie via calls to * recordInstLemma, we map lem to q in map quant, and lem to its corresponding * vector of terms in tvec. */ void getExplanationForInstLemmas( Node q, const std::vector& lems, std::map& quant, std::map >& tvec) const { std::vector terms; getExplanationForInstLemmas(q, terms, lems, quant, tvec); } /** print this class */ void print(std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector& active) const { std::vector terms; print(out, q, terms, firstTime, useActive, active); } private: /** the data */ std::map d_data; /** is valid */ context::CDO d_valid; /** helper for print * terms accumulates the path we are on in the trie. */ void print(std::ostream& out, Node q, std::vector& terms, bool& firstTime, bool useActive, std::vector& active) const; /** helper for get instantiations * terms accumulates the path we are on in the trie. */ void getInstantiations(std::vector& insts, Node q, std::vector& terms, QuantifiersEngine* qe, bool useActive, std::vector& active) const; /** helper for get explanation for inst lemma * terms accumulates the path we are on in the trie. */ void getExplanationForInstLemmas( Node q, std::vector& terms, const std::vector& lems, std::map& quant, std::map >& tvec) const; /** set instantiation lemma at this node in the trie */ void setInstLemma(Node n) { d_data.clear(); d_data[n] = NULL; } /** does this node of the trie store an instantiation lemma? */ bool hasInstLemma() const { return !d_data.empty(); } /** get the instantiation lemma stored in this node of the trie */ Node getInstLemma() const { return d_data.begin()->first; } }; /** inst match trie ordered * * This is an ordered version of the context-independent instantiation match * trie. It stores a variable order and a base InstMatchTrie. */ class InstMatchTrieOrdered { public: InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {} ~InstMatchTrieOrdered() {} /** get the ordering */ InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; } /** get the trie data */ InstMatchTrie* getTrie() { return &d_imt; } /** add match m for quantified formula q * * This method returns true if the match m was not previously added to this * class. If modEq is true, we consider duplicates modulo the current * equalities stored in the active equality engine of quantifiers engine. */ bool addInstMatch(QuantifiersEngine* qe, Node q, InstMatch& m, bool modEq = false) { return d_imt.addInstMatch(qe, q, m, modEq, d_imtio); } /** returns true if this trie contains m * * This method returns true if the match m exists in this * class. If modEq is true, we consider duplicates modulo the current * equalities stored in the active equality engine of quantifiers engine. */ bool existsInstMatch(QuantifiersEngine* qe, Node q, InstMatch& m, bool modEq = false) { return d_imt.existsInstMatch(qe, q, m, modEq, d_imtio); } private: /** the ordering */ InstMatchTrie::ImtIndexOrder* d_imtio; /** the data of this class */ InstMatchTrie d_imt; }; } /* CVC4::theory::inst namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ #endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */