From 6d3ef3f8b8256f5e17f5a045e42b5dc1effb281f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 21 Jan 2022 12:20:45 -0600
Subject: [PATCH] Ref count nodes in trigger trie (#7972)

Fixes cvc5/cvc5-projects#437.
---
 src/theory/quantifiers/ematching/trigger_trie.cpp | 8 ++++----
 src/theory/quantifiers/ematching/trigger_trie.h   | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp
index 964338f62..eafbfa766 100644
--- 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 80a378d53..3b0775829 100644
--- 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
-- 
2.30.2