From 85121a067789d9c6ac7ff14c3e34a2bc5aa83d24 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Mar 2020 10:49:46 -0500
Subject: [PATCH] Change transcendental function app slave list to
 unordered_set (#4139)

Fixes #4112.
---
 src/theory/arith/nonlinear_extension.cpp | 8 ++++----
 src/theory/arith/nonlinear_extension.h   | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 72f570f67..f11d55855 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -984,7 +984,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
         else
         {
           d_trMaster[a] = a;
-          d_trSlaves[a].push_back(a);
+          d_trSlaves[a].insert(a);
         }
       }
     }
@@ -1087,8 +1087,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     Node y =
         nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
     Node new_a = nm->mkNode(k, y);
-    d_trSlaves[new_a].push_back(new_a);
-    d_trSlaves[new_a].push_back(a);
+    d_trSlaves[new_a].insert(new_a);
+    d_trSlaves[new_a].insert(a);
     d_trMaster[a] = new_a;
     d_trMaster[new_a] = new_a;
     Node lem;
@@ -2828,7 +2828,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
           // Can assume it is its own master since phase is split over 0,
           // hence  -pi <= t[0] <= pi implies -pi <= -t[0] <= pi.
           d_trMaster[symn] = symn;
-          d_trSlaves[symn].push_back(symn);
+          d_trSlaves[symn].insert(symn);
           Assert(d_trSlaves.find(t) != d_trSlaves.end());
           std::vector< Node > children;
 
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 2fda9a895..19810730f 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -524,7 +524,7 @@ class NonlinearExtension {
    * that contain transcendental functions.
    */
   std::map<Node, Node> d_trMaster;
-  std::map<Node, std::vector<Node> > d_trSlaves;
+  std::map<Node, std::unordered_set<Node, NodeHashFunction>> d_trSlaves;
   /** The transcendental functions we have done initial refinements on */
   std::map< Node, bool > d_tf_initial_refine;
 
-- 
2.30.2