diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-23 10:49:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-23 10:49:46 -0500 |
commit | 85121a067789d9c6ac7ff14c3e34a2bc5aa83d24 (patch) | |
tree | 33f66f207988fecbbdb13006386a547325989ee1 | |
parent | c9b7c3d6fcd49b6d75a85e1316e9918374d1ebbe (diff) |
Change transcendental function app slave list to unordered_set (#4139)
Fixes #4112.
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 8 | ||||
-rw-r--r-- | 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; |