Minor optimizations for term database (#7600)

A few minor optimizations for term database.

Also collects private/public blocks in quantifiers engine.

5 files changed, 116 insertions, 101 deletions

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_iter<d_term_iter_limit ){
-      Node n = d_treg.getTermDatabase()->getGroundTerm(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<TNode> 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<Node>& qs);
- /** get instantiation term vectors */
- void getInstantiationTermVectors(Node q,
-                                  std::vector<std::vector<Node> >& tvecs);
- void getInstantiationTermVectors(
-     std::map<Node, std::vector<std::vector<Node> > >& 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<Node>& 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<Node, std::vector<Node> >& 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<Node, std::map<Node, Node> >& sol_map);
- /** Declare pool */
- void declarePool(Node p, const std::vector<Node>& 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<Node>& qs);
+  /** get instantiation term vectors */
+  void getInstantiationTermVectors(Node q,
+                                   std::vector<std::vector<Node> >& tvecs);
+  void getInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node> > >& 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<Node>& 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<Node, std::vector<Node> >& 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<Node, std::map<Node, Node> >& sol_map);
+  /** Declare pool */
+  void declarePool(Node p, const std::vector<Node>& 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 */