From: Andrew Reynolds Date: Tue, 9 Nov 2021 21:19:48 +0000 (-0600) Subject: Minor optimizations for term database (#7600) X-Git-Tag: cvc5-1.0.0~845 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78f08ed4f7ed72aadce466235266dfae7fafafdf;p=cvc5.git Minor optimizations for term database (#7600) A few minor optimizations for term database. Also collects private/public blocks in quantifiers engine. --- diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 583a70e3d..513a3965b 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -48,8 +48,8 @@ CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat) : CandidateGenerator(qs, tr), - d_term_iter(-1), - d_term_iter_limit(0), + d_termIter(0), + d_termIterList(nullptr), d_mode(cand_term_none) { d_op = d_treg.getTermDatabase()->getMatchOperator(pat); @@ -60,11 +60,16 @@ void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); } void CandidateGeneratorQE::resetForOperator(Node eqc, Node op) { - d_term_iter = 0; + d_termIter = 0; d_eqc = eqc; d_op = op; - d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op); - if( eqc.isNull() ){ + d_termIterList = d_treg.getTermDatabase()->getGroundTermList(d_op); + if (d_termIterList == nullptr) + { + d_mode = cand_term_none; + } + else if (eqc.isNull()) + { d_mode = cand_term_db; }else{ if( isExcludedEqc( eqc ) ){ @@ -104,11 +109,14 @@ Node CandidateGeneratorQE::getNextCandidate(){ Node CandidateGeneratorQE::getNextCandidateInternal() { if( d_mode==cand_term_db ){ + Assert(d_termIterList != nullptr); Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; //get next candidate term in the uf term database - while( d_term_itergetGroundTerm(d_op, d_term_iter); - d_term_iter++; + size_t tlSize = d_termIterList->d_list.size(); + while (d_termIter < tlSize) + { + Node n = d_termIterList->d_list[d_termIter]; + d_termIter++; if( isLegalCandidate( n ) ){ if (d_treg.getTermDatabase()->hasTermCurrent(n)) { @@ -243,10 +251,11 @@ CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs, void CandidateGeneratorConsExpand::reset(Node eqc) { - d_term_iter = 0; + d_termIter = 0; if (eqc.isNull()) { - d_mode = cand_term_db; + d_termIterList = d_treg.getTermDatabase()->getGroundTermList(d_op); + d_mode = d_termIterList == nullptr ? cand_term_none : cand_term_db; } else { diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 4272c0484..5c85d118f 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -27,6 +27,7 @@ namespace quantifiers { class QuantifiersState; class TermRegistry; +class DbList; namespace inst { @@ -121,9 +122,9 @@ class CandidateGeneratorQE : public CandidateGenerator /** the equality class iterator (for cand_term_eqc) */ eq::EqClassIterator d_eqc_iter; /** the TermDb index of the current ground term (for cand_term_db) */ - int d_term_iter; + size_t d_termIter; /** the TermDb index of the current ground term (for cand_term_db) */ - int d_term_iter_limit; + DbList* d_termIterList; /** the current equivalence class */ Node d_eqc; /** candidate generation modes */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2a16069f5..5c9e91d32 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -86,7 +86,7 @@ Node TermDb::getOperator(size_t i) const } /** ground terms */ -size_t TermDb::getNumGroundTerms(Node f) const +size_t TermDb::getNumGroundTerms(TNode f) const { NodeDbListMap::const_iterator it = d_opMap.find(f); if (it != d_opMap.end()) @@ -96,7 +96,7 @@ size_t TermDb::getNumGroundTerms(Node f) const return 0; } -Node TermDb::getGroundTerm(Node f, size_t i) const +Node TermDb::getGroundTerm(TNode f, size_t i) const { NodeDbListMap::const_iterator it = d_opMap.find(f); if (it != d_opMap.end()) @@ -108,6 +108,16 @@ Node TermDb::getGroundTerm(Node f, size_t i) const return Node::null(); } +DbList* TermDb::getGroundTermList(TNode f) const +{ + NodeDbListMap::const_iterator it = d_opMap.find(f); + if (it != d_opMap.end()) + { + return it->second.get(); + } + return nullptr; +} + size_t TermDb::getNumTypeGroundTerms(TypeNode tn) const { TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn); @@ -286,7 +296,8 @@ void TermDb::computeUfEqcTerms( TNode f ) { { return; } - d_func_map_eqc_trie[f].clear(); + TNodeTrie& tnt = d_func_map_eqc_trie[f]; + tnt.clear(); // get the matchable operators in the equivalence class of f std::vector ops; getOperatorsFor(f, ops); @@ -300,7 +311,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { { computeArgReps(n); TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n); - d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]); + tnt.d_data[r].addTerm(n, d_arg_reps[n]); } } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 62b625846..214b9ca96 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -93,11 +93,13 @@ class TermDb : public QuantifiersUtil { * Get the number of ground terms with operator f that have been added to the * database */ - size_t getNumGroundTerms(Node f) const; + size_t getNumGroundTerms(TNode f) const; /** get ground term for operator * Get the i^th ground term with operator f that has been added to the database */ - Node getGroundTerm(Node f, size_t i) const; + Node getGroundTerm(TNode f, size_t i) const; + /** Get ground term list */ + DbList* getGroundTermList(TNode f) const; /** get num type terms * Get the number of ground terms of tn that have been added to the database */ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 547c30797..9ecc3c7ee 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -77,21 +77,6 @@ class QuantifiersEngine : protected EnvObj /** get term database sygus */ quantifiers::TermDbSygus* getTermDatabaseSygus() const; //---------------------- end utilities - private: - //---------------------- private initialization - /** - * Finish initialize, which passes pointers to the objects that quantifiers - * engine needs but were not available when it was created. This is - * called after theories have been created but before they have finished - * initialization. - * - * @param te The theory engine - * @param dm The decision manager of the theory engine - */ - void finishInit(TheoryEngine* te); - //---------------------- end private initialization - - public: /** presolve */ void presolve(); /** notify preprocessed assertion */ @@ -108,76 +93,83 @@ class QuantifiersEngine : protected EnvObj void preRegisterQuantifier(Node q); /** assert universal quantifier */ void assertQuantifier( Node q, bool pol ); -private: - /** (context-indepentent) register quantifier internal - * - * This is called when a quantified formula q is pre-registered to the - * quantifiers theory, and updates the modules in this class with - * context-independent information about how to handle q. This includes basic - * information such as which module owns q. - */ - void registerQuantifierInternal(Node q); - /** reduceQuantifier, return true if reduced */ - bool reduceQuantifier(Node q); - -public: - /** notification when master equality engine is updated */ - void eqNotifyNewClass(TNode t); - /** mark relevant quantified formula, this will indicate it should be checked - * before the others */ - void markRelevant(Node q); - /** - * Get quantifiers name, which returns a variable corresponding to the name of - * quantified formula q if q has a name, or otherwise returns q itself. - */ - Node getNameForQuant(Node q) const; - /** - * Get name for quantified formula. Returns true if q has a name or if req - * is false. Sets name to the result of the above method. - */ - bool getNameForQuant(Node q, Node& name, bool req = true) const; - -public: - //----------user interface for instantiations (see quantifiers/instantiate.h) - /** get list of quantified formulas that were instantiated */ - void getInstantiatedQuantifiedFormulas(std::vector& qs); - /** get instantiation term vectors */ - void getInstantiationTermVectors(Node q, - std::vector >& tvecs); - void getInstantiationTermVectors( - std::map > >& insts); - /** - * Get instantiations for quantified formula q. If q is (forall ((x T)) (P x)), - * this is a list of the form (P t1) ... (P tn) for ground terms ti. - */ - void getInstantiations(Node q, std::vector& insts); - /** - * Get skolemization vectors, where for each quantified formula that was - * skolemized, this is the list of skolems that were used to witness the - * negation of that quantified formula. - */ - void getSkolemTermVectors(std::map >& sks) const; - - /** get synth solutions - * - * This method returns true if there is a synthesis solution available. This - * is the case if the last call to check satisfiability originated in a - * check-synth call, and the synthesis engine module of this class - * successfully found a solution for all active synthesis conjectures. - * - * This method adds entries to sol_map that map functions-to-synthesize with - * their solutions, for all active conjectures. This should be called - * immediately after the solver answers unsat for sygus input. - * - * For details on what is added to sol_map, see - * SynthConjecture::getSynthSolutions. - */ - bool getSynthSolutions(std::map >& sol_map); - /** Declare pool */ - void declarePool(Node p, const std::vector& initValue); - //----------end user interface for instantiations + /** notification when master equality engine is updated */ + void eqNotifyNewClass(TNode t); + /** mark relevant quantified formula, this will indicate it should be checked + * before the others */ + void markRelevant(Node q); + /** + * Get quantifiers name, which returns a variable corresponding to the name of + * quantified formula q if q has a name, or otherwise returns q itself. + */ + Node getNameForQuant(Node q) const; + /** + * Get name for quantified formula. Returns true if q has a name or if req + * is false. Sets name to the result of the above method. + */ + bool getNameForQuant(Node q, Node& name, bool req = true) const; + //----------user interface for instantiations (see quantifiers/instantiate.h) + /** get list of quantified formulas that were instantiated */ + void getInstantiatedQuantifiedFormulas(std::vector& qs); + /** get instantiation term vectors */ + void getInstantiationTermVectors(Node q, + std::vector >& tvecs); + void getInstantiationTermVectors( + std::map > >& insts); + /** + * Get instantiations for quantified formula q. If q is (forall ((x T)) (P + * x)), this is a list of the form (P t1) ... (P tn) for ground terms ti. + */ + void getInstantiations(Node q, std::vector& insts); + /** + * Get skolemization vectors, where for each quantified formula that was + * skolemized, this is the list of skolems that were used to witness the + * negation of that quantified formula. + */ + void getSkolemTermVectors(std::map >& sks) const; + /** get synth solutions + * + * This method returns true if there is a synthesis solution available. This + * is the case if the last call to check satisfiability originated in a + * check-synth call, and the synthesis engine module of this class + * successfully found a solution for all active synthesis conjectures. + * + * This method adds entries to sol_map that map functions-to-synthesize with + * their solutions, for all active conjectures. This should be called + * immediately after the solver answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * SynthConjecture::getSynthSolutions. + */ + bool getSynthSolutions(std::map >& sol_map); + /** Declare pool */ + void declarePool(Node p, const std::vector& initValue); + //----------end user interface for instantiations private: + //---------------------- private initialization + /** + * Finish initialize, which passes pointers to the objects that quantifiers + * engine needs but were not available when it was created. This is + * called after theories have been created but before they have finished + * initialization. + * + * @param te The theory engine + * @param dm The decision manager of the theory engine + */ + void finishInit(TheoryEngine* te); + //---------------------- end private initialization + /** (context-indepentent) register quantifier internal + * + * This is called when a quantified formula q is pre-registered to the + * quantifiers theory, and updates the modules in this class with + * context-independent information about how to handle q. This includes basic + * information such as which module owns q. + */ + void registerQuantifierInternal(Node q); + /** reduceQuantifier, return true if reduced */ + bool reduceQuantifier(Node q); + /** The quantifiers state object */ quantifiers::QuantifiersState& d_qstate; /** The quantifiers inference manager */