Use choice when expanding definitions for inverse transcendental functions (#1742)

1 files changed, 0 insertions, 11 deletions

diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 8b1a320a2..1264a0fb8 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -121,15 +121,6 @@ class NonlinearExtension {
   void check(Theory::Effort e);
   /** Does this class need a call to check(...) at last call effort? */
   bool needsCheckLastEffort() const { return d_needsLastCall; }
-  /** add definition
-   *
-   * This function notifies this class that lem is a formula that defines or
-   * constrains an auxiliary variable. For example, during
-   * TheoryArith::expandDefinitions, we replace a term like arcsin( x ) with an
-   * auxiliary variable k. The lemmas 0 <= k < pi and sin( x ) = k are added as
-   * definitions to this class.
-   */
-  void addDefinition(Node lem);
   /** presolve
    *
    * This function is called during TheoryArith's presolve command.
@@ -419,8 +410,6 @@ class NonlinearExtension {
   // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors
   std::map<Node, std::map<Node, Node> > d_mono_diff;
 
-  /** cache of definition lemmas (user-context-dependent) */
-  NodeSet d_def_lemmas;
   /** cache of all lemmas sent on the output channel (user-context-dependent) */
   NodeSet d_lemmas;
   /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */