From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Mar 2020 15:49:46 +0000 (-0500)
Subject: Change transcendental function app slave list to unordered_set (#4139)
X-Git-Tag: cvc5-1.0.0~3455
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=85121a067789d9c6ac7ff14c3e34a2bc5aa83d24;p=cvc5.git

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 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;