From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 8 Dec 2021 22:48:36 +0000 (-0800)
Subject: Eliminate rewriter from transcendental solver (#7772)
X-Git-Tag: cvc5-1.0.0~699
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0bcce88efaed441509c636640e19cf25a87a6be9;p=cvc5.git

Eliminate rewriter from transcendental solver (#7772)

This PR eliminates all static calls to the rewriter from the transcendental solver. We now either use the rewriter from the Env object or the theory evaluator. For this to work, the evaluator is extended to support division. In some places, the rewriting was removed altogether.
---

diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp
index ca1afb9f6..dc55632f4 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.cpp
+++ b/src/theory/arith/nl/transcendental/proof_checker.cpp
@@ -18,7 +18,7 @@
 #include "expr/sequence.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
-#include "theory/rewriter.h"
+#include "theory/evaluator.h"
 
 using namespace cvc5::kind;
 
@@ -42,18 +42,18 @@ Node mkBounds(TNode t, TNode lb, TNode ub)
 
 /**
  * Helper method to construct a secant plane:
- * ((evall - evalu) / (l - u)) * (t - l) + evall
+ * evall + ((evall - evalu) / (l - u)) * (t - l)
  */
 Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu)
 {
   NodeManager* nm = NodeManager::currentNM();
   return nm->mkNode(Kind::PLUS,
+                    evall,
                     nm->mkNode(Kind::MULT,
                                nm->mkNode(Kind::DIVISION,
                                           nm->mkNode(Kind::MINUS, evall, evalu),
                                           nm->mkNode(Kind::MINUS, l, u)),
-                               nm->mkNode(Kind::MINUS, t, l)),
-                    evall);
+                               nm->mkNode(Kind::MINUS, t, l)));
 }
 
 }  // namespace
@@ -154,16 +154,15 @@ Node TranscendentalProofRuleChecker::checkInternal(
     TaylorGenerator tg;
     TaylorGenerator::ApproximationBounds bounds;
     tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
-    Node evall = Rewriter::rewrite(
-        bounds.d_upperPos.substitute(tg.getTaylorVariable(), l));
-    Node evalu = Rewriter::rewrite(
-        bounds.d_upperPos.substitute(tg.getTaylorVariable(), u));
+    Evaluator eval(nullptr);
+    Node evall = eval.eval(bounds.d_upperPos, {tg.getTaylorVariable()}, {l});
+    Node evalu = eval.eval(bounds.d_upperPos, {tg.getTaylorVariable()}, {u});
     Node evalsecant = mkSecant(t, l, u, evall, evalu);
     Node lem = nm->mkNode(
         Kind::IMPLIES,
         mkBounds(t, l, u),
         nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
-    return Rewriter::rewrite(lem);
+    return lem;
   }
   else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG)
   {
@@ -182,16 +181,15 @@ Node TranscendentalProofRuleChecker::checkInternal(
     TaylorGenerator tg;
     TaylorGenerator::ApproximationBounds bounds;
     tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
-    Node evall = Rewriter::rewrite(
-        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
-    Node evalu = Rewriter::rewrite(
-        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
+    Evaluator eval(nullptr);
+    Node evall = eval.eval(bounds.d_upperNeg, {tg.getTaylorVariable()}, {l});
+    Node evalu = eval.eval(bounds.d_upperNeg, {tg.getTaylorVariable()}, {u});
     Node evalsecant = mkSecant(t, l, u, evall, evalu);
     Node lem = nm->mkNode(
         Kind::IMPLIES,
         mkBounds(t, l, u),
         nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
-    return Rewriter::rewrite(lem);
+    return lem;
   }
   else if (id == PfRule::ARITH_TRANS_EXP_APPROX_BELOW)
   {
@@ -206,10 +204,10 @@ Node TranscendentalProofRuleChecker::checkInternal(
     TaylorGenerator tg;
     TaylorGenerator::ApproximationBounds bounds;
     tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d, bounds);
-    Node eval =
-        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), t));
+    Evaluator eval(nullptr);
+    Node evalt = eval.eval(bounds.d_lower, {tg.getTaylorVariable()}, {t});
     return nm->mkNode(
-        Kind::GEQ, std::vector<Node>{nm->mkNode(Kind::EXPONENTIAL, t), eval});
+        Kind::GEQ, std::vector<Node>{nm->mkNode(Kind::EXPONENTIAL, t), evalt});
   }
   else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS)
   {
@@ -252,8 +250,7 @@ Node TranscendentalProofRuleChecker::checkInternal(
     Assert(args.size() == 1);
     Assert(args[0].getType().isReal());
     Node s1 = nm->mkNode(Kind::SINE, args[0]);
-    Node s2 = nm->mkNode(
-        Kind::SINE, Rewriter::rewrite(nm->mkNode(Kind::MULT, mone, args[0])));
+    Node s2 = nm->mkNode(Kind::SINE, nm->mkNode(Kind::MULT, mone, args[0]));
     return nm->mkNode(PLUS, s1, s2).eqNode(zero);
   }
   else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_ZERO)
@@ -306,16 +303,15 @@ Node TranscendentalProofRuleChecker::checkInternal(
     TaylorGenerator tg;
     TaylorGenerator::ApproximationBounds bounds;
     tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
-    Node evall = Rewriter::rewrite(
-        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
-    Node evalu = Rewriter::rewrite(
-        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
+    Evaluator eval(nullptr);
+    Node evall = eval.eval(bounds.d_upperNeg, {tg.getTaylorVariable()}, {l});
+    Node evalu = eval.eval(bounds.d_upperNeg, {tg.getTaylorVariable()}, {u});
     Node lem = nm->mkNode(
         Kind::IMPLIES,
         mkBounds(t, lb, ub),
         nm->mkNode(
             Kind::LEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
-    return Rewriter::rewrite(lem);
+    return lem;
   }
   else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS)
   {
@@ -335,12 +331,11 @@ Node TranscendentalProofRuleChecker::checkInternal(
     TaylorGenerator tg;
     TaylorGenerator::ApproximationBounds bounds;
     tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
-    Node eval = Rewriter::rewrite(
-        bounds.d_upperPos.substitute(tg.getTaylorVariable(), c));
-    return Rewriter::rewrite(
-        nm->mkNode(Kind::IMPLIES,
-                   mkBounds(t, lb, ub),
-                   nm->mkNode(Kind::LEQ, nm->mkNode(Kind::SINE, t), eval)));
+    Evaluator eval(nullptr);
+    Node evalc = eval.eval(bounds.d_upperPos, {tg.getTaylorVariable()}, {c});
+    return nm->mkNode(Kind::IMPLIES,
+                      mkBounds(t, lb, ub),
+                      nm->mkNode(Kind::LEQ, nm->mkNode(Kind::SINE, t), evalc));
   }
   else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS)
   {
@@ -363,16 +358,15 @@ Node TranscendentalProofRuleChecker::checkInternal(
     TaylorGenerator tg;
     TaylorGenerator::ApproximationBounds bounds;
     tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
-    Node evall =
-        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), l));
-    Node evalu =
-        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), u));
+    Evaluator eval(nullptr);
+    Node evall = eval.eval(bounds.d_lower, {tg.getTaylorVariable()}, {l});
+    Node evalu = eval.eval(bounds.d_lower, {tg.getTaylorVariable()}, {u});
     Node lem = nm->mkNode(
         Kind::IMPLIES,
         mkBounds(t, lb, ub),
         nm->mkNode(
             Kind::GEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
-    return Rewriter::rewrite(lem);
+    return lem;
   }
   else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG)
   {
@@ -392,12 +386,11 @@ Node TranscendentalProofRuleChecker::checkInternal(
     TaylorGenerator tg;
     TaylorGenerator::ApproximationBounds bounds;
     tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
-    Node eval =
-        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), c));
-    return Rewriter::rewrite(
-        nm->mkNode(Kind::IMPLIES,
-                   mkBounds(t, lb, ub),
-                   nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SINE, t), eval)));
+    Evaluator eval(nullptr);
+    Node evalc = eval.eval(bounds.d_lower, {tg.getTaylorVariable()}, {c});
+    return nm->mkNode(Kind::IMPLIES,
+                      mkBounds(t, lb, ub),
+                      nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SINE, t), evalc));
   }
   return Node::null();
 }
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index b6b5c92c1..583a54a51 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -385,9 +385,6 @@ void SineSolver::doTangentLemma(
                  e,
                  poly_approx));
 
-  Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem
-                       << std::endl;
-  lem = rewrite(lem);
   Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl;
   Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
   // Figure 3 : line 9
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index 2a231bc2b..898d81c27 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/evaluator.h"
 #include "theory/rewriter.h"
 
 using namespace cvc5::kind;
@@ -28,8 +29,8 @@ namespace nl {
 namespace transcendental {
 
 TaylorGenerator::TaylorGenerator()
-    : d_nm(NodeManager::currentNM()),
-      d_taylor_real_fv(d_nm->mkBoundVar("x", d_nm->realType()))
+    : d_taylor_real_fv(NodeManager::currentNM()->mkBoundVar(
+        "x", NodeManager::currentNM()->realType()))
 {
 }
 
@@ -79,15 +80,11 @@ std::pair<Node, Node> TaylorGenerator::getTaylor(Kind k, std::uint64_t n)
       }
     }
     factorial *= counter;
-    varpow =
-        Rewriter::rewrite(nm->mkNode(Kind::MULT, d_taylor_real_fv, varpow));
+    varpow = nm->mkNode(Kind::MULT, d_taylor_real_fv, varpow);
   }
-  Node taylor_sum =
-      Rewriter::rewrite(sum.size() == 1 ? sum[0] : nm->mkNode(Kind::PLUS, sum));
-  Node taylor_rem = Rewriter::rewrite(
-      nm->mkNode(Kind::DIVISION,
-                 varpow,
-                 nm->mkConst<Rational>(CONST_RATIONAL, factorial)));
+  Node taylor_sum = (sum.size() == 1 ? sum[0] : nm->mkNode(Kind::PLUS, sum));
+  Node taylor_rem = nm->mkNode(
+      Kind::DIVISION, varpow, nm->mkConst<Rational>(CONST_RATIONAL, factorial));
 
   auto res = std::make_pair(taylor_sum, taylor_rem);
 
@@ -118,19 +115,17 @@ void TaylorGenerator::getPolynomialApproximationBounds(
     if (k == Kind::EXPONENTIAL)
     {
       pbounds.d_lower = taylor_sum;
-      pbounds.d_upperNeg =
-          Rewriter::rewrite(nm->mkNode(Kind::PLUS, taylor_sum, ru));
-      pbounds.d_upperPos = Rewriter::rewrite(nm->mkNode(
+      pbounds.d_upperNeg = nm->mkNode(Kind::PLUS, taylor_sum, ru);
+      pbounds.d_upperPos = nm->mkNode(
           Kind::MULT,
           taylor_sum,
-          nm->mkNode(
-              Kind::PLUS, nm->mkConst(CONST_RATIONAL, Rational(1)), ru)));
+          nm->mkNode(Kind::PLUS, nm->mkConst(CONST_RATIONAL, Rational(1)), ru));
     }
     else
     {
       Assert(k == Kind::SINE);
-      Node l = Rewriter::rewrite(nm->mkNode(Kind::MINUS, taylor_sum, ru));
-      Node u = Rewriter::rewrite(nm->mkNode(Kind::PLUS, taylor_sum, ru));
+      Node l = nm->mkNode(Kind::MINUS, taylor_sum, ru);
+      Node u = nm->mkNode(Kind::PLUS, taylor_sum, ru);
       pbounds.d_lower = l;
       pbounds.d_upperNeg = u;
       pbounds.d_upperPos = u;
@@ -160,6 +155,7 @@ std::uint64_t TaylorGenerator::getPolynomialApproximationBoundForArg(
     std::uint64_t ds = d;
     TNode ttrf = getTaylorVariable();
     TNode tc = c;
+    Evaluator eval(nullptr);
     do
     {
       success = true;
@@ -167,8 +163,7 @@ std::uint64_t TaylorGenerator::getPolynomialApproximationBoundForArg(
       std::pair<Node, Node> taylor = getTaylor(k, n);
       // check that 1-c^{n+1}/(n+1)! > 0
       Node ru = taylor.second;
-      Node rus = ru.substitute(ttrf, tc);
-      rus = Rewriter::rewrite(rus);
+      Node rus = eval.eval(ru, {ttrf}, {tc});
       Assert(rus.isConst());
       if (rus.getConst<Rational>() > 1)
       {
@@ -221,6 +216,7 @@ std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf,
   std::vector<Node> bounds;
   TNode tfv = getTaylorVariable();
   TNode tfs = tf[0];
+  Evaluator eval(nullptr);
   for (unsigned d2 = 0; d2 < 2; d2++)
   {
     Node pab = (d2 == 0 ? pbounds.d_lower
@@ -235,8 +231,7 @@ std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf,
       // M_A( x*x { x -> t } ) = M_A( t*t )
       // where M_A denotes the abstract model.
       Node mtfs = model.computeAbstractModelValue(tfs);
-      pab = pab.substitute(tfv, mtfs);
-      pab = Rewriter::rewrite(pab);
+      pab = eval.eval(pab, {tfv}, {mtfs});
       Assert(pab.isConst());
       bounds.push_back(pab);
     }
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index df4cb128c..ea082d87b 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -104,7 +104,6 @@ class TaylorGenerator
                                          NlModel& model);
 
  private:
-  NodeManager* d_nm;
   const Node d_taylor_real_fv;
 
   /**
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 9e204f582..25a5a511f 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -41,11 +41,11 @@ TranscendentalSolver::TranscendentalSolver(Env& env,
                                            InferenceManager& im,
                                            NlModel& m)
     : EnvObj(env),
-      d_tstate(im, m, env),
+      d_tstate(env, im, m),
       d_expSlv(env, &d_tstate),
       d_sineSlv(env, &d_tstate)
 {
-  d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree;
+  d_taylor_degree = options().arith.nlExtTfTaylorDegree;
 }
 
 TranscendentalSolver::~TranscendentalSolver() {}
@@ -187,7 +187,7 @@ void TranscendentalSolver::processSideEffect(const NlLemma& se)
     auto it = secant_points.find(d);
     if (it == secant_points.end())
     {
-      it = secant_points.emplace(d, d_tstate.d_env.getUserContext()).first;
+      it = secant_points.emplace(d, userContext()).first;
     }
     it->second.push_back(c);
   }
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 870eddc86..7c2f1a058 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -30,10 +30,10 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
-TranscendentalState::TranscendentalState(InferenceManager& im,
-                                         NlModel& model,
-                                         Env& env)
-    : d_im(im), d_model(model), d_env(env)
+TranscendentalState::TranscendentalState(Env& env,
+                                         InferenceManager& im,
+                                         NlModel& model)
+    : EnvObj(env), d_im(im), d_model(model)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -204,15 +204,15 @@ void TranscendentalState::mkPi()
   if (d_pi.isNull())
   {
     d_pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
-    d_pi_2 = Rewriter::rewrite(
+    d_pi_2 = rewrite(
         nm->mkNode(Kind::MULT,
                    d_pi,
                    nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2))));
-    d_pi_neg_2 = Rewriter::rewrite(
+    d_pi_neg_2 = rewrite(
         nm->mkNode(Kind::MULT,
                    d_pi,
                    nm->mkConst(CONST_RATIONAL, Rational(-1) / Rational(2))));
-    d_pi_neg = Rewriter::rewrite(nm->mkNode(
+    d_pi_neg = rewrite(nm->mkNode(
         Kind::MULT, d_pi, nm->mkConst(CONST_RATIONAL, Rational(-1))));
     // initialize bounds
     d_pi_bound[0] =
@@ -274,7 +274,7 @@ Node TranscendentalState::mkSecantPlane(
 {
   NodeManager* nm = NodeManager::currentNM();
   // Figure 3: S_l( x ), S_u( x ) for s = 0,1
-  Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, lower, upper));
+  Node rcoeff_n = rewrite(nm->mkNode(Kind::MINUS, lower, upper));
   Assert(rcoeff_n.isConst());
   Rational rcoeff = rcoeff_n.getConst<Rational>();
   Assert(rcoeff.sgn() != 0);
@@ -291,7 +291,7 @@ Node TranscendentalState::mkSecantPlane(
   Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( "
                     << upper << " ; " << uval << " )" << std::endl;
   Trace("nl-trans") << "\t" << res << std::endl;
-  Trace("nl-trans") << "\trewritten: " << Rewriter::rewrite(res) << std::endl;
+  Trace("nl-trans") << "\trewritten: " << rewrite(res) << std::endl;
   return res;
 }
 
@@ -331,9 +331,6 @@ NlLemma TranscendentalState::mkSecantLemma(TNode lower,
       antec_n,
       nm->mkNode(
           convexity == Convexity::CONVEX ? Kind::LEQ : Kind::GEQ, tf, splane));
-  Trace("nl-trans-lemma") << "*** Secant plane lemma (pre-rewrite) : " << lem
-                          << std::endl;
-  lem = Rewriter::rewrite(lem);
   Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl;
   Assert(d_model.computeAbstractModelValue(lem) == d_false);
   CDProof* proof = nullptr;
@@ -419,8 +416,8 @@ void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
   if (lower != center)
   {
     // Figure 3 : P(l), P(u), for s = 0
-    Node lval = Rewriter::rewrite(
-        poly_approx.substitute(d_taylor.getTaylorVariable(), lower));
+    Node lval =
+        rewrite(poly_approx.substitute(d_taylor.getTaylorVariable(), lower));
     Node splane = mkSecantPlane(tf[0], lower, center, lval, cval);
     NlLemma nlem = mkSecantLemma(
         lower, center, lval, cval, csign, convexity, tf, splane, actual_d);
@@ -438,8 +435,8 @@ void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
   if (center != upper)
   {
     // Figure 3 : P(l), P(u), for s = 1
-    Node uval = Rewriter::rewrite(
-        poly_approx.substitute(d_taylor.getTaylorVariable(), upper));
+    Node uval =
+        rewrite(poly_approx.substitute(d_taylor.getTaylorVariable(), upper));
     Node splane = mkSecantPlane(tf[0], center, upper, cval, uval);
     NlLemma nlem = mkSecantLemma(
         center, upper, cval, uval, csign, convexity, tf, splane, actual_d);
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 77fcf57fb..ede8079a4 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -60,9 +60,9 @@ inline std::ostream& operator<<(std::ostream& os, Convexity c) {
  * This includes common lookups and caches as well as generic utilities for
  * secant plane lemmas and taylor approximations.
  */
-struct TranscendentalState
+struct TranscendentalState : protected EnvObj
 {
-  TranscendentalState(InferenceManager& im, NlModel& model, Env& env);
+  TranscendentalState(Env& env, InferenceManager& im, NlModel& model);
 
   /**
    * Checks whether proofs are enabled.
@@ -168,8 +168,6 @@ struct TranscendentalState
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
-  /** Reference to the environment */
-  Env& d_env;
   /** Utility to compute taylor approximations */
   TaylorGenerator d_taylor;
   /**
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 27e67dd9f..9451f9995 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -458,6 +458,29 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(res);
           break;
         }
+        case kind::DIVISION:
+        case kind::DIVISION_TOTAL:
+        {
+          Rational res = results[currNode[0]].d_rat;
+          bool divbyzero = false;
+          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+          {
+            if (results[currNode[i]].d_rat.isZero())
+            {
+              Trace("evaluator")
+                  << "Division by zero not supported" << std::endl;
+              divbyzero = true;
+              results[currNode] = EvalResult();
+              break;
+            }
+            res = res / results[currNode[i]].d_rat;
+          }
+          if (!divbyzero)
+          {
+            results[currNode] = EvalResult(res);
+          }
+          break;
+        }
 
         case kind::GEQ:
         {