Ref count nodes in trigger trie (#7972)

Fixes cvc5/cvc5-projects#437.

diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp
index 964338f621c033f68990a4d8a9e19c02fed37fe8..eafbfa766a8b371d0068fbe2e82270e196d082ac 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger_trie.cpp
+++ b/src/theory/quantifiers/ematching/trigger_trie.cpp
@@ -30,7 +30,7 @@ TriggerTrie::~TriggerTrie()
   }
 }
 
-inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
+inst::Trigger* TriggerTrie::getTrigger(const std::vector<Node>& nodes)
 {
   std::vector<Node> temp;
   temp.insert(temp.begin(), nodes.begin(), nodes.end());
@@ -38,7 +38,7 @@ inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
   TriggerTrie* tt = this;
   for (const Node& n : temp)
   {
-    std::map<TNode, TriggerTrie>::iterator itt = tt->d_children.find(n);
+    std::map<Node, TriggerTrie>::iterator itt = tt->d_children.find(n);
     if (itt == tt->d_children.end())
     {
       return nullptr;
@@ -51,14 +51,14 @@ inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
   return tt->d_tr.empty() ? nullptr : tt->d_tr[0];
 }
 
-void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
+void TriggerTrie::addTrigger(const 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);
+    std::map<Node, TriggerTrie>::iterator itt = tt->d_children.find(n);
     if (itt == tt->d_children.end())
     {
       TriggerTrie* ttn = &tt->d_children[n];

diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h
index 80a378d533873ebe467ba91b1f0bc04be1757600..3b0775829833ede06acbfca20e7aba35af5384a3 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger_trie.h
+++ b/src/theory/quantifiers/ematching/trigger_trie.h
@@ -43,17 +43,17 @@ class TriggerTrie
   /**
    * This returns a Trigger t that is indexed by nodes, or nullptr otherwise.
    */
-  Trigger* getTrigger(std::vector<Node>& nodes);
+  Trigger* getTrigger(const 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);
+  void addTrigger(const 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;
+  std::map<Node, TriggerTrie> d_children;
 }; /* class inst::Trigger::TriggerTrie */
 
 }  // namespace inst