(proof-new) Split operator elimination from arithmetic (#4581)

This class will be undergoing further refactoring for the sake of proofs.

This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility.

5 files changed, 647 insertions, 648 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d16164562..6850ef450 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -316,6 +316,8 @@ libcvc4_add_sources(
   theory/arith/nl/transcendental_solver.h
   theory/arith/normal_form.cpp
   theory/arith/normal_form.h
+  theory/arith/operator_elim.cpp
+  theory/arith/operator_elim.h
   theory/arith/partial_model.cpp
   theory/arith/partial_model.h
   theory/arith/simplex.cpp
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
new file mode 100644
index 000000000..593fbd584
--- /dev/null
+++ b/src/theory/arith/operator_elim.cpp
@@ -0,0 +1,508 @@
+/*********************                                                        */
+/*! \file operator_elim.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of operator elimination for arithmetic
+ **/
+
+#include "theory/arith/operator_elim.h"
+
+#include "expr/skolem_manager.h"
+#include "options/arith_options.h"
+#include "smt/logic_exception.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+OperatorElim::OperatorElim(const LogicInfo& info) : d_info(info) {}
+
+void OperatorElim::checkNonLinearLogic(Node term)
+{
+  if (d_info.isLinear())
+  {
+    Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term
+                         << std::endl;
+    std::stringstream serr;
+    serr << "A non-linear fact was asserted to arithmetic in a linear logic."
+         << std::endl;
+    serr << "The fact in question: " << term << std::endl;
+    throw LogicException(serr.str());
+  }
+}
+
+Node OperatorElim::eliminateOperatorsRec(Node n)
+{
+  Trace("arith-elim") << "Begin elim: " << n << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<Node, Node, TNodeHashFunction> visited;
+  std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
+  std::vector<Node> visit;
+  Node cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (Theory::theoryOf(cur) != THEORY_ARITH)
+    {
+      visited[cur] = cur;
+    }
+    else if (it == visited.end())
+    {
+      visited[cur] = Node::null();
+      visit.push_back(cur);
+      for (const Node& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      for (const Node& cn : cur)
+      {
+        it = visited.find(cn);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cn != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      Node retElim = eliminateOperators(ret);
+      if (retElim != ret)
+      {
+        // recursively eliminate operators in result, since some eliminations
+        // are defined in terms of other non-standard operators.
+        ret = eliminateOperatorsRec(retElim);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
+}
+
+Node OperatorElim::eliminateOperators(Node node)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+
+  Kind k = node.getKind();
+  switch (k)
+  {
+    case TANGENT:
+    case COSECANT:
+    case SECANT:
+    case COTANGENT:
+    {
+      // these are eliminated by rewriting
+      return Rewriter::rewrite(node);
+      break;
+    }
+    case TO_INTEGER:
+    case IS_INTEGER:
+    {
+      Node toIntSkolem;
+      std::map<Node, Node>::const_iterator it = d_to_int_skolem.find(node[0]);
+      if (it == d_to_int_skolem.end())
+      {
+        // node[0] - 1 < toIntSkolem <= node[0]
+        // -1 < toIntSkolem - node[0] <= 0
+        // 0 <= node[0] - toIntSkolem < 1
+        Node v = nm->mkBoundVar(nm->integerType());
+        Node one = mkRationalNode(1);
+        Node zero = mkRationalNode(0);
+        Node diff = nm->mkNode(MINUS, node[0], v);
+        Node lem = mkInRange(diff, zero, one);
+        toIntSkolem = sm->mkSkolem(
+            v, lem, "toInt", "a conversion of a Real term to its Integer part");
+        toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem);
+        d_to_int_skolem[node[0]] = toIntSkolem;
+      }
+      else
+      {
+        toIntSkolem = (*it).second;
+      }
+      if (k == IS_INTEGER)
+      {
+        return nm->mkNode(EQUAL, node[0], toIntSkolem);
+      }
+      Assert(k == TO_INTEGER);
+      return toIntSkolem;
+    }
+
+    case INTS_DIVISION_TOTAL:
+    case INTS_MODULUS_TOTAL:
+    {
+      Node den = Rewriter::rewrite(node[1]);
+      Node num = Rewriter::rewrite(node[0]);
+      Node intVar;
+      Node rw = nm->mkNode(k, num, den);
+      std::map<Node, Node>::const_iterator it = d_int_div_skolem.find(rw);
+      if (it == d_int_div_skolem.end())
+      {
+        Node v = nm->mkBoundVar(nm->integerType());
+        Node lem;
+        Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
+        if (den.isConst())
+        {
+          const Rational& rat = den.getConst<Rational>();
+          if (num.isConst() || rat == 0)
+          {
+            // just rewrite
+            return Rewriter::rewrite(node);
+          }
+          if (rat > 0)
+          {
+            lem = nm->mkNode(
+                AND,
+                leqNum,
+                nm->mkNode(
+                    LT,
+                    num,
+                    nm->mkNode(MULT,
+                               den,
+                               nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
+          }
+          else
+          {
+            lem = nm->mkNode(
+                AND,
+                leqNum,
+                nm->mkNode(
+                    LT,
+                    num,
+                    nm->mkNode(
+                        MULT,
+                        den,
+                        nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
+          }
+        }
+        else
+        {
+          checkNonLinearLogic(node);
+          lem = nm->mkNode(
+              AND,
+              nm->mkNode(
+                  IMPLIES,
+                  nm->mkNode(GT, den, nm->mkConst(Rational(0))),
+                  nm->mkNode(
+                      AND,
+                      leqNum,
+                      nm->mkNode(
+                          LT,
+                          num,
+                          nm->mkNode(
+                              MULT,
+                              den,
+                              nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
+              nm->mkNode(
+                  IMPLIES,
+                  nm->mkNode(LT, den, nm->mkConst(Rational(0))),
+                  nm->mkNode(
+                      AND,
+                      leqNum,
+                      nm->mkNode(
+                          LT,
+                          num,
+                          nm->mkNode(
+                              MULT,
+                              den,
+                              nm->mkNode(
+                                  PLUS, v, nm->mkConst(Rational(-1))))))));
+        }
+        intVar = sm->mkSkolem(
+            v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
+        intVar = SkolemManager::getWitnessForm(intVar);
+        d_int_div_skolem[rw] = intVar;
+      }
+      else
+      {
+        intVar = (*it).second;
+      }
+      if (k == INTS_MODULUS_TOTAL)
+      {
+        Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
+        return nn;
+      }
+      else
+      {
+        return intVar;
+      }
+      break;
+    }
+    case DIVISION_TOTAL:
+    {
+      Node num = Rewriter::rewrite(node[0]);
+      Node den = Rewriter::rewrite(node[1]);
+      if (den.isConst())
+      {
+        // No need to eliminate here, can eliminate via rewriting later.
+        // Moreover, rewriting may change the type of this node from real to
+        // int, which impacts certain issues with subtyping.
+        return node;
+      }
+      checkNonLinearLogic(node);
+      Node var;
+      Node rw = nm->mkNode(k, num, den);
+      std::map<Node, Node>::const_iterator it = d_div_skolem.find(rw);
+      if (it == d_div_skolem.end())
+      {
+        Node v = nm->mkBoundVar(nm->realType());
+        Node lem = nm->mkNode(IMPLIES,
+                              den.eqNode(nm->mkConst(Rational(0))).negate(),
+                              nm->mkNode(MULT, den, v).eqNode(num));
+        var = sm->mkSkolem(
+            v, lem, "nonlinearDiv", "the result of a non-linear div term");
+        var = SkolemManager::getWitnessForm(var);
+        d_div_skolem[rw] = var;
+      }
+      else
+      {
+        var = (*it).second;
+      }
+      return var;
+      break;
+    }
+    case DIVISION:
+    {
+      Node num = Rewriter::rewrite(node[0]);
+      Node den = Rewriter::rewrite(node[1]);
+      Node ret = nm->mkNode(DIVISION_TOTAL, num, den);
+      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
+      {
+        checkNonLinearLogic(node);
+        Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO);
+        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
+        ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
+      }
+      return ret;
+      break;
+    }
+
+    case INTS_DIVISION:
+    {
+      // partial function: integer div
+      Node num = Rewriter::rewrite(node[0]);
+      Node den = Rewriter::rewrite(node[1]);
+      Node ret = nm->mkNode(INTS_DIVISION_TOTAL, num, den);
+      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
+      {
+        checkNonLinearLogic(node);
+        Node intDivByZeroNum =
+            getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO);
+        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
+        ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
+      }
+      return ret;
+      break;
+    }
+
+    case INTS_MODULUS:
+    {
+      // partial function: mod
+      Node num = Rewriter::rewrite(node[0]);
+      Node den = Rewriter::rewrite(node[1]);
+      Node ret = nm->mkNode(INTS_MODULUS_TOTAL, num, den);
+      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
+      {
+        checkNonLinearLogic(node);
+        Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO);
+        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
+        ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
+      }
+      return ret;
+      break;
+    }
+
+    case ABS:
+    {
+      return nm->mkNode(ITE,
+                        nm->mkNode(LT, node[0], nm->mkConst(Rational(0))),
+                        nm->mkNode(UMINUS, node[0]),
+                        node[0]);
+      break;
+    }
+    case SQRT:
+    case ARCSINE:
+    case ARCCOSINE:
+    case ARCTANGENT:
+    case ARCCOSECANT:
+    case ARCSECANT:
+    case ARCCOTANGENT:
+    {
+      checkNonLinearLogic(node);
+      // eliminate inverse functions here
+      std::map<Node, Node>::const_iterator it =
+          d_nlin_inverse_skolem.find(node);
+      if (it == d_nlin_inverse_skolem.end())
+      {
+        Node var = nm->mkBoundVar(nm->realType());
+        Node lem;
+        if (k == SQRT)
+        {
+          Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
+          Node uf = skolemApp.eqNode(var);
+          Node nonNeg =
+              nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
+
+          // sqrt(x) reduces to:
+          // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
+          //
+          // Uf(x) makes sure that the reduction still behaves like a function,
+          // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
+          // satisfiable. On the original formula, this would require that we
+          // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
+          // model.
+          lem = nm->mkNode(ITE,
+                           nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
+                           nonNeg,
+                           uf);
+        }
+        else
+        {
+          Node pi = mkPi();
+
+          // range of the skolem
+          Node rlem;
+          if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
+          {
+            Node half = nm->mkConst(Rational(1) / Rational(2));
+            Node pi2 = nm->mkNode(MULT, half, pi);
+            Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
+            // -pi/2 < var <= pi/2
+            rlem = nm->mkNode(
+                AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
+          }
+          else
+          {
+            // 0 <= var < pi
+            rlem = nm->mkNode(AND,
+                              nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
+                              nm->mkNode(LT, var, pi));
+          }
+
+          Kind rk = k == ARCSINE
+                        ? SINE
+                        : (k == ARCCOSINE
+                               ? COSINE
+                               : (k == ARCTANGENT
+                                      ? TANGENT
+                                      : (k == ARCCOSECANT
+                                             ? COSECANT
+                                             : (k == ARCSECANT ? SECANT
+                                                               : COTANGENT))));
+          Node invTerm = nm->mkNode(rk, var);
+          lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
+        }
+        Assert(!lem.isNull());
+        Node ret = sm->mkSkolem(
+            var,
+            lem,
+            "tfk",
+            "Skolem to eliminate a non-standard transcendental function");
+        ret = SkolemManager::getWitnessForm(ret);
+        d_nlin_inverse_skolem[node] = ret;
+        return ret;
+      }
+      return (*it).second;
+      break;
+    }
+
+    default: break;
+  }
+  return node;
+}
+
+Node OperatorElim::getArithSkolem(ArithSkolemId asi)
+{
+  std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
+  if (it == d_arith_skolem.end())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+
+    TypeNode tn;
+    std::string name;
+    std::string desc;
+    switch (asi)
+    {
+      case ArithSkolemId::DIV_BY_ZERO:
+        tn = nm->realType();
+        name = std::string("divByZero");
+        desc = std::string("partial real division");
+        break;
+      case ArithSkolemId::INT_DIV_BY_ZERO:
+        tn = nm->integerType();
+        name = std::string("intDivByZero");
+        desc = std::string("partial int division");
+        break;
+      case ArithSkolemId::MOD_BY_ZERO:
+        tn = nm->integerType();
+        name = std::string("modZero");
+        desc = std::string("partial modulus");
+        break;
+      case ArithSkolemId::SQRT:
+        tn = nm->realType();
+        name = std::string("sqrtUf");
+        desc = std::string("partial sqrt");
+        break;
+      default: Unhandled();
+    }
+
+    Node skolem;
+    if (options::arithNoPartialFun())
+    {
+      // partial function: division
+      skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
+    }
+    else
+    {
+      // partial function: division
+      skolem = nm->mkSkolem(name,
+                            nm->mkFunctionType(tn, tn),
+                            desc,
+                            NodeManager::SKOLEM_EXACT_NAME);
+    }
+    d_arith_skolem[asi] = skolem;
+    return skolem;
+  }
+  return it->second;
+}
+
+Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
+{
+  Node skolem = getArithSkolem(asi);
+  if (!options::arithNoPartialFun())
+  {
+    skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
+  }
+  return skolem;
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
new file mode 100644
index 000000000..2cdf9bc49
--- /dev/null
+++ b/src/theory/arith/operator_elim.h
@@ -0,0 +1,123 @@
+/*********************                                                        */
+/*! \file operator_elim.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Operator elimination for arithmetic
+ **/
+
+#pragma once
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/logic_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class OperatorElim
+{
+ public:
+  OperatorElim(const LogicInfo& info);
+  ~OperatorElim() {}
+  /**
+   * Eliminate operators in term n. If n has top symbol that is not a core
+   * one (including division, int division, mod, to_int, is_int, syntactic sugar
+   * transcendental functions), then we replace it by a form that eliminates
+   * that operator. This may involve the introduction of witness terms.
+   *
+   * One exception to the above rule is that we may leave certain applications
+   * like (/ 4 1) unchanged, since replacing this by 4 changes its type from
+   * real to int. This is important for some subtyping issues during
+   * expandDefinition. Moreover, applications like this can be eliminated
+   * trivially later by rewriting.
+   *
+   * This method is called both during expandDefinition and during ppRewrite.
+   *
+   * @param n The node to eliminate operators from.
+   * @return The (single step) eliminated form of n.
+   */
+  Node eliminateOperators(Node n);
+  /**
+   * Recursively ensure that n has no non-standard operators. This applies
+   * the above method on all subterms of n.
+   *
+   * @param n The node to eliminate operators from.
+   * @return The eliminated form of n.
+   */
+  Node eliminateOperatorsRec(Node n);
+
+ private:
+  /** Logic info of the owner of this class */
+  const LogicInfo& d_info;
+
+  /**
+   *  Maps for Skolems for to-integer, real/integer div-by-k, and inverse
+   *  non-linear operators that are introduced during ppRewriteTerms.
+   */
+  std::map<Node, Node> d_to_int_skolem;
+  std::map<Node, Node> d_div_skolem;
+  std::map<Node, Node> d_int_div_skolem;
+  std::map<Node, Node> d_nlin_inverse_skolem;
+
+  /** Arithmetic skolem identifier */
+  enum class ArithSkolemId
+  {
+    /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
+    DIV_BY_ZERO,
+    /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
+    INT_DIV_BY_ZERO,
+    /* an uninterpreted function f s.t. f(x) = x mod 0 */
+    MOD_BY_ZERO,
+    /* an uninterpreted function f s.t. f(x) = sqrt(x) */
+    SQRT,
+  };
+
+  /**
+   * Function symbols used to implement:
+   * (1) Uninterpreted division-by-zero semantics.  Needed to deal with partial
+   * division function ("/"),
+   * (2) Uninterpreted int-division-by-zero semantics.  Needed to deal with
+   * partial function "div",
+   * (3) Uninterpreted mod-zero semantics.  Needed to deal with partial
+   * function "mod".
+   *
+   * If the option arithNoPartialFun() is enabled, then the range of this map
+   * stores Skolem constants instead of Skolem functions, meaning that the
+   * function-ness of e.g. division by zero is ignored.
+   */
+  std::map<ArithSkolemId, Node> d_arith_skolem;
+  /** get arithmetic skolem
+   *
+   * Returns the Skolem in the above map for the given id, creating it if it
+   * does not already exist.
+   */
+  Node getArithSkolem(ArithSkolemId asi);
+  /** get arithmetic skolem application
+   *
+   * By default, this returns the term f( n ), where f is the Skolem function
+   * for the identifier asi.
+   *
+   * If the option arithNoPartialFun is enabled, this returns f, where f is
+   * the Skolem constant for the identifier asi.
+   */
+  Node getArithSkolemApp(Node n, ArithSkolemId asi);
+
+  /**
+   * Called when a non-linear term n is given to this class. Throw an exception
+   * if the logic is linear.
+   */
+  void checkNonLinearLogic(Node term);
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index ed0adc59e..7b7f5a411 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -156,10 +156,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_solveIntMaybeHelp(0u),
       d_solveIntAttempts(0u),
       d_statistics(),
-      d_to_int_skolem(u),
-      d_div_skolem(u),
-      d_int_div_skolem(u),
-      d_nlin_inverse_skolem(u)
+      d_opElim(logicInfo)
 {
   if( options::nlExt() ){
     d_nonlinearExtension = new nl::NonlinearExtension(
@@ -1088,427 +1085,16 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
   // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
   // introduce non-standard arithmetic terms appearing in grammars.
   // call eliminate operators
-  Node nn = eliminateOperators(n);
+  Node nn = d_opElim.eliminateOperators(n);
   if (nn != n)
   {
     // since elimination may introduce new operators to eliminate, we must
     // recursively eliminate result
-    return eliminateOperatorsRec(nn);
+    return d_opElim.eliminateOperatorsRec(nn);
   }
   return n;
 }
 
-void TheoryArithPrivate::checkNonLinearLogic(Node term)
-{
-  if (getLogicInfo().isLinear())
-  {
-    Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term
-                         << std::endl;
-    std::stringstream serr;
-    serr << "A non-linear fact was asserted to arithmetic in a linear logic."
-         << std::endl;
-    serr << "The fact in question: " << term << endl;
-    throw LogicException(serr.str());
-  }
-}
-
-Node TheoryArithPrivate::eliminateOperatorsRec(Node n)
-{
-  Trace("arith-elim") << "Begin elim: " << n << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  std::unordered_map<Node, Node, TNodeHashFunction> visited;
-  std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
-  std::vector<Node> visit;
-  Node cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur);
-    if (Theory::theoryOf(cur) != THEORY_ARITH)
-    {
-      visited[cur] = cur;
-    }
-    else if (it == visited.end())
-    {
-      visited[cur] = Node::null();
-      visit.push_back(cur);
-      for (const Node& cn : cur)
-      {
-        visit.push_back(cn);
-      }
-    }
-    else if (it->second.isNull())
-    {
-      Node ret = cur;
-      bool childChanged = false;
-      std::vector<Node> children;
-      if (cur.getMetaKind() == metakind::PARAMETERIZED)
-      {
-        children.push_back(cur.getOperator());
-      }
-      for (const Node& cn : cur)
-      {
-        it = visited.find(cn);
-        Assert(it != visited.end());
-        Assert(!it->second.isNull());
-        childChanged = childChanged || cn != it->second;
-        children.push_back(it->second);
-      }
-      if (childChanged)
-      {
-        ret = nm->mkNode(cur.getKind(), children);
-      }
-      Node retElim = eliminateOperators(ret);
-      if (retElim != ret)
-      {
-        // recursively eliminate operators in result, since some eliminations
-        // are defined in terms of other non-standard operators.
-        ret = eliminateOperatorsRec(retElim);
-      }
-      visited[cur] = ret;
-    }
-  } while (!visit.empty());
-  Assert(visited.find(n) != visited.end());
-  Assert(!visited.find(n)->second.isNull());
-  return visited[n];
-}
-
-Node TheoryArithPrivate::eliminateOperators(Node node)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-
-  Kind k = node.getKind();
-  switch (k)
-  {
-    case kind::TANGENT:
-    case kind::COSECANT:
-    case kind::SECANT:
-    case kind::COTANGENT:
-    {
-      // these are eliminated by rewriting
-      return Rewriter::rewrite(node);
-      break;
-    }
-    case kind::TO_INTEGER:
-    case kind::IS_INTEGER:
-    {
-      Node toIntSkolem;
-      NodeMap::const_iterator it = d_to_int_skolem.find(node[0]);
-      if (it == d_to_int_skolem.end())
-      {
-        // node[0] - 1 < toIntSkolem <= node[0]
-        // -1 < toIntSkolem - node[0] <= 0
-        // 0 <= node[0] - toIntSkolem < 1
-        Node v = nm->mkBoundVar(nm->integerType());
-        Node one = mkRationalNode(1);
-        Node zero = mkRationalNode(0);
-        Node diff = nm->mkNode(kind::MINUS, node[0], v);
-        Node lem = mkInRange(diff, zero, one);
-        toIntSkolem = sm->mkSkolem(
-            v, lem, "toInt", "a conversion of a Real term to its Integer part");
-        toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem);
-        d_to_int_skolem[node[0]] = toIntSkolem;
-      }
-      else
-      {
-        toIntSkolem = (*it).second;
-      }
-      if (k == kind::IS_INTEGER)
-      {
-        return nm->mkNode(kind::EQUAL, node[0], toIntSkolem);
-      }
-      Assert(k == kind::TO_INTEGER);
-      return toIntSkolem;
-    }
-
-    case kind::INTS_DIVISION_TOTAL:
-    case kind::INTS_MODULUS_TOTAL:
-    {
-      Node den = Rewriter::rewrite(node[1]);
-      Node num = Rewriter::rewrite(node[0]);
-      Node intVar;
-      Node rw = nm->mkNode(k, num, den);
-      NodeMap::const_iterator it = d_int_div_skolem.find(rw);
-      if (it == d_int_div_skolem.end())
-      {
-        Node v = nm->mkBoundVar(nm->integerType());
-        Node lem;
-        Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
-        if (den.isConst())
-        {
-          const Rational& rat = den.getConst<Rational>();
-          if (num.isConst() || rat == 0)
-          {
-            // just rewrite
-            return Rewriter::rewrite(node);
-          }
-          if (rat > 0)
-          {
-            lem = nm->mkNode(
-                AND,
-                leqNum,
-                nm->mkNode(
-                    LT,
-                    num,
-                    nm->mkNode(MULT,
-                               den,
-                               nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
-          }
-          else
-          {
-            lem = nm->mkNode(
-                AND,
-                leqNum,
-                nm->mkNode(
-                    LT,
-                    num,
-                    nm->mkNode(
-                        MULT,
-                        den,
-                        nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
-          }
-        }
-        else
-        {
-          checkNonLinearLogic(node);
-          lem = nm->mkNode(
-              AND,
-              nm->mkNode(
-                  IMPLIES,
-                  nm->mkNode(GT, den, nm->mkConst(Rational(0))),
-                  nm->mkNode(
-                      AND,
-                      leqNum,
-                      nm->mkNode(
-                          LT,
-                          num,
-                          nm->mkNode(
-                              MULT,
-                              den,
-                              nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
-              nm->mkNode(
-                  IMPLIES,
-                  nm->mkNode(LT, den, nm->mkConst(Rational(0))),
-                  nm->mkNode(
-                      AND,
-                      leqNum,
-                      nm->mkNode(
-                          LT,
-                          num,
-                          nm->mkNode(
-                              MULT,
-                              den,
-                              nm->mkNode(
-                                  PLUS, v, nm->mkConst(Rational(-1))))))));
-        }
-        intVar = sm->mkSkolem(
-            v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
-        intVar = SkolemManager::getWitnessForm(intVar);
-        d_int_div_skolem[rw] = intVar;
-      }
-      else
-      {
-        intVar = (*it).second;
-      }
-      if (k == kind::INTS_MODULUS_TOTAL)
-      {
-        Node nn =
-            nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar));
-        return nn;
-      }
-      else
-      {
-        return intVar;
-      }
-      break;
-    }
-    case kind::DIVISION_TOTAL:
-    {
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
-      if (den.isConst())
-      {
-        // No need to eliminate here, can eliminate via rewriting later.
-        // Moreover, rewriting may change the type of this node from real to
-        // int, which impacts certain issues with subtyping.
-        return node;
-      }
-      checkNonLinearLogic(node);
-      Node var;
-      Node rw = nm->mkNode(k, num, den);
-      NodeMap::const_iterator it = d_div_skolem.find(rw);
-      if (it == d_div_skolem.end())
-      {
-        Node v = nm->mkBoundVar(nm->realType());
-        Node lem = nm->mkNode(IMPLIES,
-                              den.eqNode(nm->mkConst(Rational(0))).negate(),
-                              nm->mkNode(MULT, den, v).eqNode(num));
-        var = sm->mkSkolem(
-            v, lem, "nonlinearDiv", "the result of a non-linear div term");
-        var = SkolemManager::getWitnessForm(var);
-        d_div_skolem[rw] = var;
-      }
-      else
-      {
-        var = (*it).second;
-      }
-      return var;
-      break;
-    }
-    case kind::DIVISION:
-    {
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
-      Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den);
-      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
-      {
-        checkNonLinearLogic(node);
-        Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO);
-        Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret);
-      }
-      return ret;
-      break;
-    }
-
-    case kind::INTS_DIVISION:
-    {
-      // partial function: integer div
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
-      Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
-      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
-      {
-        checkNonLinearLogic(node);
-        Node intDivByZeroNum =
-            getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO);
-        Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret);
-      }
-      return ret;
-      break;
-    }
-
-    case kind::INTS_MODULUS:
-    {
-      // partial function: mod
-      Node num = Rewriter::rewrite(node[0]);
-      Node den = Rewriter::rewrite(node[1]);
-      Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
-      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
-      {
-        checkNonLinearLogic(node);
-        Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO);
-        Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret);
-      }
-      return ret;
-      break;
-    }
-
-    case kind::ABS:
-    {
-      return nm->mkNode(kind::ITE,
-                        nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))),
-                        nm->mkNode(kind::UMINUS, node[0]),
-                        node[0]);
-      break;
-    }
-    case kind::SQRT:
-    case kind::ARCSINE:
-    case kind::ARCCOSINE:
-    case kind::ARCTANGENT:
-    case kind::ARCCOSECANT:
-    case kind::ARCSECANT:
-    case kind::ARCCOTANGENT:
-    {
-      checkNonLinearLogic(node);
-      // eliminate inverse functions here
-      NodeMap::const_iterator it = d_nlin_inverse_skolem.find(node);
-      if (it == d_nlin_inverse_skolem.end())
-      {
-        Node var = nm->mkBoundVar(nm->realType());
-        Node lem;
-        if (k == kind::SQRT)
-        {
-          Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
-          Node uf = skolemApp.eqNode(var);
-          Node nonNeg = nm->mkNode(
-              kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf);
-
-          // sqrt(x) reduces to:
-          // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
-          //
-          // Uf(x) makes sure that the reduction still behaves like a function,
-          // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
-          // satisfiable. On the original formula, this would require that we
-          // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
-          // model.
-          lem = nm->mkNode(
-              kind::ITE,
-              nm->mkNode(kind::GEQ, node[0], nm->mkConst(Rational(0))),
-              nonNeg,
-              uf);
-        }
-        else
-        {
-          Node pi = mkPi();
-
-          // range of the skolem
-          Node rlem;
-          if (k == kind::ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
-          {
-            Node half = nm->mkConst(Rational(1) / Rational(2));
-            Node pi2 = nm->mkNode(kind::MULT, half, pi);
-            Node npi2 = nm->mkNode(kind::MULT, nm->mkConst(Rational(-1)), pi2);
-            // -pi/2 < var <= pi/2
-            rlem = nm->mkNode(
-                AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
-          }
-          else
-          {
-            // 0 <= var < pi
-            rlem = nm->mkNode(AND,
-                              nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
-                              nm->mkNode(LT, var, pi));
-          }
-
-          Kind rk = k == kind::ARCSINE
-                        ? kind::SINE
-                        : (k == kind::ARCCOSINE
-                               ? kind::COSINE
-                               : (k == kind::ARCTANGENT
-                                      ? kind::TANGENT
-                                      : (k == kind::ARCCOSECANT
-                                             ? kind::COSECANT
-                                             : (k == kind::ARCSECANT
-                                                    ? kind::SECANT
-                                                    : kind::COTANGENT))));
-          Node invTerm = nm->mkNode(rk, var);
-          lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
-        }
-        Assert(!lem.isNull());
-        Node ret = sm->mkSkolem(
-            var,
-            lem,
-            "tfk",
-            "Skolem to eliminate a non-standard transcendental function");
-        ret = SkolemManager::getWitnessForm(ret);
-        d_nlin_inverse_skolem[node] = ret;
-        return ret;
-      }
-      return (*it).second;
-      break;
-    }
-
-    default: break;
-  }
-  return node;
-}
-
 Node TheoryArithPrivate::ppRewrite(TNode atom) {
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
@@ -5218,155 +4804,16 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
 Node TheoryArithPrivate::expandDefinition(Node node)
 {
   // call eliminate operators
-  Node nn = eliminateOperators(node);
+  Node nn = d_opElim.eliminateOperators(node);
   if (nn != node)
   {
     // since elimination may introduce new operators to eliminate, we must
     // recursively eliminate result
-    return eliminateOperatorsRec(nn);
+    return d_opElim.eliminateOperatorsRec(nn);
   }
   return node;
 }
 
-Node TheoryArithPrivate::getArithSkolem(ArithSkolemId asi)
-{
-  std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
-  if (it == d_arith_skolem.end())
-  {
-    NodeManager* nm = NodeManager::currentNM();
-
-    TypeNode tn;
-    std::string name;
-    std::string desc;
-    switch (asi)
-    {
-      case ArithSkolemId::DIV_BY_ZERO:
-        tn = nm->realType();
-        name = std::string("divByZero");
-        desc = std::string("partial real division");
-        break;
-      case ArithSkolemId::INT_DIV_BY_ZERO:
-        tn = nm->integerType();
-        name = std::string("intDivByZero");
-        desc = std::string("partial int division");
-        break;
-      case ArithSkolemId::MOD_BY_ZERO:
-        tn = nm->integerType();
-        name = std::string("modZero");
-        desc = std::string("partial modulus");
-        break;
-      case ArithSkolemId::SQRT:
-        tn = nm->realType();
-        name = std::string("sqrtUf");
-        desc = std::string("partial sqrt");
-        break;
-      default: Unhandled();
-    }
-
-    Node skolem;
-    if (options::arithNoPartialFun())
-    {
-      // partial function: division
-      skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
-    }
-    else
-    {
-      // partial function: division
-      skolem = nm->mkSkolem(name,
-                            nm->mkFunctionType(tn, tn),
-                            desc,
-                            NodeManager::SKOLEM_EXACT_NAME);
-    }
-    d_arith_skolem[asi] = skolem;
-    return skolem;
-  }
-  return it->second;
-}
-
-Node TheoryArithPrivate::getArithSkolemApp(Node n, ArithSkolemId asi)
-{
-  Node skolem = getArithSkolem(asi);
-  if (!options::arithNoPartialFun())
-  {
-    skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
-  }
-  return skolem;
-}
-
-// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const
-// InferBoundsParameters& param){
-//   Node t = Rewriter::rewrite(term);
-//   Assert(Polynomial::isMember(t));
-//   Polynomial p = Polynomial::parsePolynomial(t);
-//   if(p.containsConstant()){
-//     Constant c = p.getHead().getConstant();
-//     if(p.isConstant()){
-//       InferBoundsResult res(t, param.findLowerBound());
-//       res.setBound((DeltaRational)c.getValue(), mkBoolNode(true));
-//       return res;
-//     }else{
-//       Polynomial tail = p.getTail();
-//       InferBoundsResult res = inferBound(tail.getNode(), param);
-//       if(res.foundBound()){
-//         DeltaRational newBound = res.getValue() + c.getValue();
-//         if(tail.isIntegral()){
-//           Integer asInt  = (param.findLowerBound()) ? newBound.ceiling() :
-//           newBound.floor(); newBound = DeltaRational(asInt);
-//         }
-//         res.setBound(newBound, res.getExplanation());
-//       }
-//       return res;
-//     }
-//   }else if(param.findLowerBound()){
-//     InferBoundsParameters find_ub = param;
-//     find_ub.setFindUpperBound();
-//     if(param.useThreshold()){
-//       find_ub.setThreshold(- param.getThreshold() );
-//     }
-//     Polynomial negP = -p;
-//     InferBoundsResult res = inferBound(negP.getNode(), find_ub);
-//     res.setFindLowerBound();
-//     if(res.foundBound()){
-//       res.setTerm(p.getNode());
-//       res.setBound(-res.getValue(), res.getExplanation());
-//     }
-//     return res;
-//   }else{
-//     Assert(param.findUpperBound());
-//     // does not contain a constant
-//     switch(param.getEffort()){
-//     case InferBoundsParameters::Lookup:
-//       return inferUpperBoundLookup(t, param);
-//     case InferBoundsParameters::Simplex:
-//       return inferUpperBoundSimplex(t, param);
-//     case InferBoundsParameters::LookupAndSimplexOnFailure:
-//     case InferBoundsParameters::TryBoth:
-//       {
-//         InferBoundsResult lookup = inferUpperBoundLookup(t, param);
-//         if(lookup.foundBound()){
-//           if(param.getEffort() ==
-//           InferBoundsParameters::LookupAndSimplexOnFailure ||
-//              lookup.boundIsOptimal()){
-//             return lookup;
-//           }
-//         }
-//         InferBoundsResult simplex = inferUpperBoundSimplex(t, param);
-//         if(lookup.foundBound() && simplex.foundBound()){
-//           return (lookup.getValue() <= simplex.getValue()) ? lookup :
-//           simplex;
-//         }else if(lookup.foundBound()){
-//           return lookup;
-//         }else{
-//           return simplex;
-//         }
-//       }
-//     default:
-//       Unreachable();
-//       return InferBoundsResult();
-//     }
-//   }
-// }
-
 std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
   using namespace inferbounds;
 
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 8252326bf..867029e3c 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -35,15 +35,12 @@
 #include "smt/logic_exception.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/arith/arith_rewriter.h"
-#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/attempt_solution_simplex.h"
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint.h"
-#include "theory/arith/constraint.h"
-#include "theory/arith/delta_rational.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/dio_solver.h"
 #include "theory/arith/dual_simplex.h"
@@ -51,9 +48,8 @@
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/matrix.h"
-#include "theory/arith/matrix.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/partial_model.h"
+#include "theory/arith/operator_elim.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/soi_simplex.h"
@@ -421,40 +417,13 @@ private:
   // handle linear /, div, mod, and also is_int, to_int
   Node ppRewriteTerms(TNode atom);
 
-  /**
-   * Called when a non-linear term n is given to this class. Throw an exception
-   * if the logic is linear.
-   */
-  void checkNonLinearLogic(Node term);
-  /**
-   * Eliminate operators in term n. If n has top symbol that is not a core
-   * one (including division, int division, mod, to_int, is_int, syntactic sugar
-   * transcendental functions), then we replace it by a form that eliminates
-   * that operator. This may involve the introduction of witness terms.
-   *
-   * One exception to the above rule is that we may leave certain applications
-   * like (/ 4 1) unchanged, since replacing this by 4 changes its type from
-   * real to int. This is important for some subtyping issues during
-   * expandDefinition. Moreover, applications like this can be eliminated
-   * trivially later by rewriting.
-   *
-   * This method is called both during expandDefinition and during ppRewrite.
-   *
-   * @param n The node to eliminate operators from.
-   * @return The (single step) eliminated form of n.
-   */
-  Node eliminateOperators(Node n);
-  /**
-   * Recursively ensure that n has no non-standard operators. This applies
-   * the above method on all subterms of n.
-   *
-   * @param n The node to eliminate operators from.
-   * @return The eliminated form of n.
-   */
-  Node eliminateOperatorsRec(Node n);
-
  public:
-  TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryArithPrivate(TheoryArith& containing,
+                     context::Context* c,
+                     context::UserContext* u,
+                     OutputChannel& out,
+                     Valuation valuation,
+                     const LogicInfo& logicInfo);
   ~TheoryArithPrivate();
 
   TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
@@ -862,60 +831,10 @@ private:
 
   Statistics d_statistics;
 
-  enum class ArithSkolemId
-  {
-    /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
-    DIV_BY_ZERO,
-    /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
-    INT_DIV_BY_ZERO,
-    /* an uninterpreted function f s.t. f(x) = x mod 0 */
-    MOD_BY_ZERO,
-    /* an uninterpreted function f s.t. f(x) = sqrt(x) */
-    SQRT,
-  };
-
-  /**
-   * Function symbols used to implement:
-   * (1) Uninterpreted division-by-zero semantics.  Needed to deal with partial
-   * division function ("/"),
-   * (2) Uninterpreted int-division-by-zero semantics.  Needed to deal with
-   * partial function "div",
-   * (3) Uninterpreted mod-zero semantics.  Needed to deal with partial
-   * function "mod".
-   *
-   * If the option arithNoPartialFun() is enabled, then the range of this map
-   * stores Skolem constants instead of Skolem functions, meaning that the
-   * function-ness of e.g. division by zero is ignored.
-   */
-  std::map<ArithSkolemId, Node> d_arith_skolem;
-  /** get arithmetic skolem
-   *
-   * Returns the Skolem in the above map for the given id, creating it if it
-   * does not already exist.
-   */
-  Node getArithSkolem(ArithSkolemId asi);
-  /** get arithmetic skolem application
-   *
-   * By default, this returns the term f( n ), where f is the Skolem function
-   * for the identifier asi.
-   *
-   * If the option arithNoPartialFun is enabled, this returns f, where f is
-   * the Skolem constant for the identifier asi.
-   */
-  Node getArithSkolemApp(Node n, ArithSkolemId asi);
-
-  /**
-   *  Maps for Skolems for to-integer, real/integer div-by-k, and inverse
-   *  non-linear operators that are introduced during ppRewriteTerms.
-   */
-  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-  NodeMap d_to_int_skolem;
-  NodeMap d_div_skolem;
-  NodeMap d_int_div_skolem;
-  NodeMap d_nlin_inverse_skolem;
-
   /** The theory rewriter for this theory. */
   ArithRewriter d_rewriter;
+  /** The operator elimination utility */
+  OperatorElim d_opElim;
 };/* class TheoryArithPrivate */
 
 }/* CVC4::theory::arith namespace */