From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 Dec 2020 23:55:06 +0000 (-0600)
Subject: Move trigger trie to own file (#5680)
X-Git-Tag: cvc5-1.0.0~2439
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aac53f510e1f21a46a49cb31475a8851a3097089;p=cvc5.git

Move trigger trie to own file (#5680)

Also updates minor things to meet coding standards and makes it so that children in the trie are not dynamically allocated.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d9c38ec65..ca124d90b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -648,6 +648,8 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/instantiation_engine.h
   theory/quantifiers/ematching/trigger.cpp
   theory/quantifiers/ematching/trigger.h
+  theory/quantifiers/ematching/trigger_trie.cpp
+  theory/quantifiers/ematching/trigger_trie.h
   theory/quantifiers/equality_infer.cpp
   theory/quantifiers/equality_infer.h
   theory/quantifiers/equality_query.cpp
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 62aa1bcc0..654b1fd12 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -942,66 +942,6 @@ int Trigger::getActiveScore() {
   return d_mg->getActiveScore( d_quantEngine );
 }
 
-TriggerTrie::TriggerTrie()
-{}
-
-TriggerTrie::~TriggerTrie() {
-  for(std::map< TNode, TriggerTrie* >::iterator i = d_children.begin(), iend = d_children.end();
-      i != iend; ++i) {
-    TriggerTrie* current = (*i).second;
-    delete current;
-  }
-  d_children.clear();
-
-  for( unsigned i=0; i<d_tr.size(); i++ ){
-    delete d_tr[i];
-  }
-}
-
-inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
-{
-  std::vector<Node> temp;
-  temp.insert(temp.begin(), nodes.begin(), nodes.end());
-  std::sort(temp.begin(), temp.end());
-  TriggerTrie* tt = this;
-  for (const Node& n : temp)
-  {
-    std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
-    if (itt == tt->d_children.end())
-    {
-      return NULL;
-    }
-    else
-    {
-      tt = itt->second;
-    }
-  }
-  return tt->d_tr.empty() ? NULL : tt->d_tr[0];
-}
-
-void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
-{
-  std::vector<Node> temp;
-  temp.insert(temp.begin(), nodes.begin(), nodes.end());
-  std::sort(temp.begin(), temp.end());
-  TriggerTrie* tt = this;
-  for (const Node& n : temp)
-  {
-    std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
-    if (itt == tt->d_children.end())
-    {
-      TriggerTrie* ttn = new TriggerTrie;
-      tt->d_children[n] = ttn;
-      tt = ttn;
-    }
-    else
-    {
-      tt = itt->second;
-    }
-  }
-  tt->d_tr.push_back(t);
-}
-
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 7b0b51fb6..890811c8b 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -447,35 +447,6 @@ class Trigger {
   IMGenerator* d_mg;
 }; /* class Trigger */
 
-/** A trie of triggers.
-*
-* This class is used to cache all Trigger objects that are generated in the
-* current context. We index Triggers in this data structure based on the
-* value of Trigger::d_nodes. When a Trigger is added to this data structure,
-* this Trie assumes responsibility for deleting it.
-*/
-class TriggerTrie {
-public:
-  TriggerTrie();
-  ~TriggerTrie();
-  /** get trigger
-  * This returns a Trigger t that is indexed by nodes,
-  * or NULL otherwise.
-  */
-  Trigger* getTrigger(std::vector<Node>& nodes);
-  /** add trigger
-  * This adds t to the trie, indexed by nodes.
-  * In typical use cases, nodes is t->d_nodes.
-  */
-  void addTrigger(std::vector<Node>& nodes, Trigger* t);
-
- private:
-  /** The trigger at this node in the trie. */
-  std::vector<Trigger*> d_tr;
-  /** The children of this node in the trie. */
-  std::map< TNode, TriggerTrie* > d_children;
-};/* class inst::Trigger::TriggerTrie */
-
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp
new file mode 100644
index 000000000..bb70a18fe
--- /dev/null
+++ b/src/theory/quantifiers/ematching/trigger_trie.cpp
@@ -0,0 +1,75 @@
+/*********************                                                        */
+/*! \file trigger_trie.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Implementation of trigger trie class
+ **/
+
+#include "theory/quantifiers/ematching/trigger_trie.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+TriggerTrie::TriggerTrie() {}
+
+TriggerTrie::~TriggerTrie()
+{
+  for (size_t i = 0, ntriggers = d_tr.size(); i < ntriggers; i++)
+  {
+    delete d_tr[i];
+  }
+}
+
+inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
+{
+  std::vector<Node> temp;
+  temp.insert(temp.begin(), nodes.begin(), nodes.end());
+  std::sort(temp.begin(), temp.end());
+  TriggerTrie* tt = this;
+  for (const Node& n : temp)
+  {
+    std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n);
+    if (itt == tt->d_children.end())
+    {
+      return nullptr;
+    }
+    else
+    {
+      tt = &(itt->second);
+    }
+  }
+  return tt->d_tr.empty() ? nullptr : tt->d_tr[0];
+}
+
+void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
+{
+  std::vector<Node> temp(nodes.begin(), nodes.end());
+  std::sort(temp.begin(), temp.end());
+  TriggerTrie* tt = this;
+  for (const Node& n : temp)
+  {
+    std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n);
+    if (itt == tt->d_children.end())
+    {
+      TriggerTrie* ttn = &tt->d_children[n];
+      tt = ttn;
+    }
+    else
+    {
+      tt = &(itt->second);
+    }
+  }
+  tt->d_tr.push_back(t);
+}
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h
new file mode 100644
index 000000000..1ff995bb8
--- /dev/null
+++ b/src/theory/quantifiers/ematching/trigger_trie.h
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file trigger_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 trigger trie class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
+#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/trigger.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace inst {
+
+/** A trie of triggers.
+ *
+ * This class is used to cache all Trigger objects that are generated in the
+ * current context. We index Triggers in this data structure based on the
+ * value of Trigger::d_nodes. When a Trigger is added to this data structure,
+ * this Trie assumes responsibility for deleting it.
+ */
+class TriggerTrie
+{
+ public:
+  TriggerTrie();
+  ~TriggerTrie();
+  /**
+   * This returns a Trigger t that is indexed by nodes, or nullptr otherwise.
+   */
+  Trigger* getTrigger(std::vector<Node>& nodes);
+  /**
+   * This adds t to the trie, indexed by nodes. In typical use cases, nodes i
+   * t->d_nodes.
+   */
+  void addTrigger(std::vector<Node>& nodes, Trigger* t);
+ private:
+  /** The trigger at this node in the trie. */
+  std::vector<Trigger*> d_tr;
+  /** The children of this node in the trie. */
+  std::map<TNode, TriggerTrie> d_children;
+}; /* class inst::Trigger::TriggerTrie */
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 8dcaf668f..5af914a9f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -24,7 +24,7 @@
 #include "context/cdlist.h"
 #include "expr/attribute.h"
 #include "expr/term_canonize.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_builder.h"