Simplify storing of transcendental function applications that occur in assertions (#2458)

1 files changed, 2 insertions, 8 deletions

diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 1e5ca9ad1..c0af312b3 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -580,14 +580,8 @@ class NonlinearExtension {
   std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp;
   std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max;
 
-  /** transcendental function representative map
-   *
-   * For each transcendental function n = tf( x ),
-   * this stores ( n.getKind(), r ) -> n
-   * where r is the current representative of x
-   * in the equality engine assoiated with this class.
-   */
-  std::map<Kind, std::map<Node, Node> > d_tf_rep_map;
+  /** A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } */
+  std::map<Kind, std::vector<Node> > d_f_map;
 
   // factor skolems
   std::map< Node, Node > d_factor_skolem;