Change transcendental function app slave list to unordered_set (#4139)

Fixes #4112.

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 72f570f678f8a50da3070e9fc7ab21f910116c33..f11d55855c6e8da781ad7effb53045fd05e793b5 100644 (file)
--- 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 2fda9a895ad91916ae93cef208f1c287080a05e5..19810730f7cfcfe23ff531eba85e67ed6c35cacf 100644 (file)
--- 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;