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 ca1afb9f6e71b7e34cbd5fa6ab2adcbb9501c857..dc55632f45ac9d1aa81a9673a46d03f8f2bf2577 100644 (file)
--- 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 b6b5c92c12fd692d72b6743fa6f86d150dd22f29..583a54a51344a9895215abf76b125b9364c653ae 100644 (file)
--- 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 2a231bc2b4c13cd9aab704632c3e9f20ac82a418..898d81c27c2aa923a1279c0e2038dbe3c45270ec 100644 (file)
--- 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 df4cb128cc85fbd6f26165a58e67e8770ba8e2ca..ea082d87b5404ae2b015f7cc76ae18845e9216f9 100644 (file)
--- 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 9e204f582ac654eb18382926934f8710c2c99d27..25a5a511fa8d1f019d5234c563759604dd35ed3c 100644 (file)
--- 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 870eddc869b19e79f3bcaca90e1b223eb103803d..7c2f1a0587b981b67cef49663a630051c5a7ab69 100644 (file)
--- 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 77fcf57fbdddd30c8fa4e660e31830760ff70f3c..ede8079a4b59da9bc659169c7ab026e535cac313 100644 (file)
--- 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 27e67dd9faa20c39475f12f901712a21ee859b57..9451f999587c0dd606ba7a2c7ee127a7d2709ad9 100644 (file)
--- 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:
         {