From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 24 Nov 2017 12:44:46 +0000 (-0600)
Subject: Implement tangent and secant planes for transcendental functions (#1401)
X-Git-Tag: cvc5-1.0.0~5455
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb095659fb12e3733a73f1be31769ff5b5eb6055;p=cvc5.git

Implement tangent and secant planes for transcendental functions (#1401)
---

diff --git a/src/options/arith_options b/src/options/arith_options
index bddde7a16..3ba1b00f6 100644
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -177,6 +177,9 @@ option nlExtFactor --nl-ext-factor bool :default true
 option nlExtTangentPlanes --nl-ext-tplanes bool :default false
  use non-terminating tangent plane strategy for non-linear
 
+option nlExtTfTangentPlanes --nl-ext-tf-tplanes bool :default false
+ use non-terminating tangent plane strategy for transcendental functions for non-linear
+
 option nlExtEntailConflicts --nl-ext-ent-conf bool :default false
  check for entailed conflicts in non-linear solver
  
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index e3e078bbe..77c4e2e40 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -26,7 +26,6 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/theory_model.h"
 
-using namespace std;
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -199,7 +198,8 @@ bool hasNewMonomials(Node n, const std::vector<Node>& existing) {
     worklist.pop_back();
     if (!Contains(visited, current)) {
       visited.insert(current);
-      if (current.getKind() == kind::NONLINEAR_MULT) {
+      if (current.getKind() == NONLINEAR_MULT)
+      {
         if (!IsInVector(existing, current)) {
           return true;
         }
@@ -280,8 +280,8 @@ void NonlinearExtension::registerMonomialSubset(Node a, Node b) {
   d_m_contain_parent[a].push_back(b);
   d_m_contain_children[b].push_back(a);
 
-  Node mult_term = safeConstructNary(kind::MULT, diff_children);
-  Node nlmult_term = safeConstructNary(kind::NONLINEAR_MULT, diff_children);
+  Node mult_term = safeConstructNary(MULT, diff_children);
+  Node nlmult_term = safeConstructNary(NONLINEAR_MULT, diff_children);
   d_m_contain_mult[a][b] = mult_term;
   d_m_contain_umult[a][b] = nlmult_term;
   Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b
@@ -405,7 +405,10 @@ bool NonLinearExtentionSubstitutionSolver::solve(
                   if (!QuantArith::getMonomialSum(ns, msum)) {
                     success = false;
                   }else{
-                    d_rep_sum_unique_exp[n] = exp_rm.size()==1 ? exp_rm[0] : NodeManager::currentNM()->mkNode( kind::AND, exp_rm );
+                    d_rep_sum_unique_exp[n] =
+                        exp_rm.size() == 1
+                            ? exp_rm[0]
+                            : NodeManager::currentNM()->mkNode(AND, exp_rm);
                     d_rep_sum_unique[n] = ns;
                   }
                 }
@@ -487,9 +490,8 @@ bool NonLinearExtentionSubstitutionSolver::setSubstitutionConst(
   d_rep_to_const[r] = r_c;
   Node expn;
   if (!r_c_exp.empty()) {
-    expn = r_c_exp.size() == 1
-               ? r_c_exp[0]
-               : NodeManager::currentNM()->mkNode(kind::AND, r_c_exp);
+    expn = r_c_exp.size() == 1 ? r_c_exp[0]
+                               : NodeManager::currentNM()->mkNode(AND, r_c_exp);
     Trace("nl-subs-debug") << "...explanation is " << expn << std::endl;
     d_rep_to_const_exp[r] = expn;
   }
@@ -670,11 +672,11 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced(
     int effort, Node n, Node on, const std::vector<Node>& exp) const {
   if (n != d_zero) {
     Kind k = n.getKind();
-    return std::make_pair(k != kind::NONLINEAR_MULT && !isTranscendentalKind(k),
+    return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k),
                           Node::null());
   }
   Assert(n == d_zero);
-  if (on.getKind() == kind::NONLINEAR_MULT)
+  if (on.getKind() == NONLINEAR_MULT)
   {
     Trace("nl-ext-zero-exp") << "Infer zero : " << on << " == " << n
                              << std::endl;
@@ -686,15 +688,15 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced(
       Trace("nl-ext-zero-exp") << "  exp[" << i << "] = " << exp[i]
                                << std::endl;
       std::vector<Node> eqs;
-      if (exp[i].getKind() == kind::EQUAL)
+      if (exp[i].getKind() == EQUAL)
       {
         eqs.push_back(exp[i]);
       }
-      else if (exp[i].getKind() == kind::AND)
+      else if (exp[i].getKind() == AND)
       {
         for (const Node& ec : exp[i])
         {
-          if (ec.getKind() == kind::EQUAL)
+          if (ec.getKind() == EQUAL)
           {
             eqs.push_back(ec);
           }
@@ -727,7 +729,10 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) {
     Node ret;
     if (n.isConst()) {
       ret = n;
-    } else if (index == 1 && ( n.getKind() == kind::NONLINEAR_MULT || isTranscendentalKind( n.getKind() ) )) {
+    }
+    else if (index == 1 && (n.getKind() == NONLINEAR_MULT
+                            || isTranscendentalKind(n.getKind())))
+    {
       if (d_containing.getValuation().getModel()->hasTerm(n)) {
         // use model value for abstraction
         ret = d_containing.getValuation().getModel()->getRepresentative(n);
@@ -738,7 +743,8 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) {
       }
       //Assert( ret.isConst() );
     } else if (n.getNumChildren() == 0) {
-      if( n.getKind()==kind::PI ){
+      if (n.getKind() == PI)
+      {
         // we are interested in the exact value of PI, which cannot be computed.
         // hence, we return PI itself when asked for the concrete value.
         ret = n;
@@ -748,7 +754,8 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) {
     } else {    
       // otherwise, compute true value
       std::vector<Node> children;
-      if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      if (n.getMetaKind() == metakind::PARAMETERIZED)
+      {
         children.push_back(n.getOperator());
       }
       for (unsigned i = 0; i < n.getNumChildren(); i++) {
@@ -756,7 +763,8 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) {
         children.push_back(mc);
       }
       ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
-      if( n.getKind()==kind::APPLY_UF ){
+      if (n.getKind() == APPLY_UF)
+      {
         ret = d_containing.getValuation().getModel()->getValue(ret);
       }else{
         ret = Rewriter::rewrite(ret);
@@ -786,7 +794,8 @@ void NonlinearExtension::registerMonomial(Node n) {
   if (!IsInVector(d_monomials, n)) {
     d_monomials.push_back(n);
     Trace("nl-ext-debug") << "Register monomial : " << n << std::endl;
-    if (n.getKind() == kind::NONLINEAR_MULT) {
+    if (n.getKind() == NONLINEAR_MULT)
+    {
       // get exponent count
       for (unsigned k = 0; k < n.getNumChildren(); k++) {
         d_m_exp[n][n[k]]++;
@@ -886,7 +895,7 @@ void NonlinearExtension::registerConstraint(Node atom) {
 }
 
 bool NonlinearExtension::isArithKind(Kind k) {
-  return k == kind::PLUS || k == kind::MULT || k == kind::NONLINEAR_MULT;
+  return k == PLUS || k == MULT || k == NONLINEAR_MULT;
 }
 
 Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) {
@@ -896,7 +905,7 @@ Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) {
       return a_eq_b;
     } else {
       // return mkAbs( a ).eqNode( mkAbs( b ) );
-      Node negate_b = NodeManager::currentNM()->mkNode(kind::UMINUS, b);
+      Node negate_b = NodeManager::currentNM()->mkNode(UMINUS, b);
       return a_eq_b.orNode(a.eqNode(negate_b));
     }
   } else if (status < 0) {
@@ -904,16 +913,16 @@ Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) {
   } else {
     Assert(status == 1 || status == 2);
     NodeManager* nm = NodeManager::currentNM();
-    Kind greater_op = status == 1 ? kind::GEQ : kind::GT;
+    Kind greater_op = status == 1 ? GEQ : GT;
     if (orderType == 0) {
       return nm->mkNode(greater_op, a, b);
     } else {
       // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) );
       Node zero = mkRationalNode(0);
-      Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, zero);
-      Node b_is_nonnegative = nm->mkNode(kind::GEQ, b, zero);
-      Node negate_a = nm->mkNode(kind::UMINUS, a);
-      Node negate_b = nm->mkNode(kind::UMINUS, b);
+      Node a_is_nonnegative = nm->mkNode(GEQ, a, zero);
+      Node b_is_nonnegative = nm->mkNode(GEQ, b, zero);
+      Node negate_a = nm->mkNode(UMINUS, a);
+      Node negate_b = nm->mkNode(UMINUS, b);
       return a_is_nonnegative.iteNode(
           b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b),
                                    nm->mkNode(greater_op, a, negate_b)),
@@ -928,19 +937,21 @@ Node NonlinearExtension::mkAbs(Node a) {
     return mkRationalNode(a.getConst<Rational>().abs());
   } else {
     NodeManager* nm = NodeManager::currentNM();
-    Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, mkRationalNode(0));
-    return a_is_nonnegative.iteNode(a, nm->mkNode(kind::UMINUS, a));
+    Node a_is_nonnegative = nm->mkNode(GEQ, a, mkRationalNode(0));
+    return a_is_nonnegative.iteNode(a, nm->mkNode(UMINUS, a));
   }
 }
 
 Node NonlinearExtension::mkValidPhase(Node a, Node pi) {
-  return mkBounded( NodeManager::currentNM()->mkNode( kind::MULT, mkRationalNode(-1), pi ), a, pi );
+  return mkBounded(
+      NodeManager::currentNM()->mkNode(MULT, mkRationalNode(-1), pi), a, pi);
 }
 
 Node NonlinearExtension::mkBounded( Node l, Node a, Node u ) {
-  return NodeManager::currentNM()->mkNode( kind::AND, 
-           NodeManager::currentNM()->mkNode( kind::GEQ, a, l ),
-           NodeManager::currentNM()->mkNode( kind::LEQ, a, u ) );
+  return NodeManager::currentNM()->mkNode(
+      AND,
+      NodeManager::currentNM()->mkNode(GEQ, a, l),
+      NodeManager::currentNM()->mkNode(LEQ, a, u));
 }
 
 // by a <k1> b, a <k2> b, we know a <ret> b
@@ -950,24 +961,33 @@ Kind NonlinearExtension::joinKinds(Kind k1, Kind k2) {
   } else if (k1 == k2) {
     return k1;
   } else {
-    Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ ||
-           k1 == kind::GT || k1 == kind::GEQ);
-    Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ ||
-           k2 == kind::GT || k2 == kind::GEQ);
-    if (k1 == kind::EQUAL) {
-      if (k2 == kind::LEQ || k2 == kind::GEQ) {
+    Assert(k1 == EQUAL || k1 == LT || k1 == LEQ || k1 == GT || k1 == GEQ);
+    Assert(k2 == EQUAL || k2 == LT || k2 == LEQ || k2 == GT || k2 == GEQ);
+    if (k1 == EQUAL)
+    {
+      if (k2 == LEQ || k2 == GEQ)
+      {
         return k1;
       }
-    } else if (k1 == kind::LT) {
-      if (k2 == kind::LEQ) {
+    }
+    else if (k1 == LT)
+    {
+      if (k2 == LEQ)
+      {
         return k1;
       }
-    } else if (k1 == kind::LEQ) {
-      if (k2 == kind::GEQ) {
-        return kind::EQUAL;
+    }
+    else if (k1 == LEQ)
+    {
+      if (k2 == GEQ)
+      {
+        return EQUAL;
       }
-    } else if (k1 == kind::GT) {
-      if (k2 == kind::GEQ) {
+    }
+    else if (k1 == GT)
+    {
+      if (k2 == GEQ)
+      {
         return k1;
       }
     }
@@ -982,18 +1002,23 @@ Kind NonlinearExtension::transKinds(Kind k1, Kind k2) {
   } else if (k1 == k2) {
     return k1;
   } else {
-    Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ ||
-           k1 == kind::GT || k1 == kind::GEQ);
-    Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ ||
-           k2 == kind::GT || k2 == kind::GEQ);
-    if (k1 == kind::EQUAL) {
+    Assert(k1 == EQUAL || k1 == LT || k1 == LEQ || k1 == GT || k1 == GEQ);
+    Assert(k2 == EQUAL || k2 == LT || k2 == LEQ || k2 == GT || k2 == GEQ);
+    if (k1 == EQUAL)
+    {
       return k2;
-    } else if (k1 == kind::LT) {
-      if (k2 == kind::LEQ) {
+    }
+    else if (k1 == LT)
+    {
+      if (k2 == LEQ)
+      {
         return k1;
       }
-    } else if (k1 == kind::GT) {
-      if (k2 == kind::GEQ) {
+    }
+    else if (k1 == GT)
+    {
+      if (k2 == GEQ)
+      {
         return k1;
       }
     }
@@ -1002,8 +1027,8 @@ Kind NonlinearExtension::transKinds(Kind k1, Kind k2) {
 }
 
 bool NonlinearExtension::isTranscendentalKind(Kind k) {
-  Assert( k != kind::TANGENT && k != kind::COSINE ); //eliminated
-  return k==kind::EXPONENTIAL || k==kind::SINE || k==kind::PI;
+  Assert(k != TANGENT && k != COSINE);  // eliminated
+  return k == EXPONENTIAL || k == SINE || k == PI;
 }
  
 Node NonlinearExtension::mkMonomialRemFactor(
@@ -1023,7 +1048,7 @@ Node NonlinearExtension::mkMonomialRemFactor(
         << "......rem, now " << inc << " factors of " << v << std::endl;
     children.insert(children.end(), inc, v);
   }
-  Node ret = safeConstructNary(kind::MULT, children);
+  Node ret = safeConstructNary(MULT, children);
   ret = Rewriter::rewrite(ret);
   Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl;
   return ret;
@@ -1142,8 +1167,9 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                        << d_mv[0][a] << " ]" << std::endl;
     //Assert(d_mv[1][a].isConst());
     //Assert(d_mv[0][a].isConst());
-  
-    if( a.getKind()==kind::NONLINEAR_MULT ){
+
+    if (a.getKind() == NONLINEAR_MULT)
+    {
       d_ms.push_back( a );
       
       //context-independent registration
@@ -1177,7 +1203,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     }else if( a.getNumChildren()==1 ){
       bool consider = true;
       // get shifted version
-      if( a.getKind()==kind::SINE ){
+      if (a.getKind() == SINE)
+      {
         if( d_trig_is_base.find( a )==d_trig_is_base.end() ){
           consider = false;
           if( d_trig_base.find( a )==d_trig_base.end() ){
@@ -1193,12 +1220,21 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
             Node shift = NodeManager::currentNM()->mkSkolem( "s", NodeManager::currentNM()->integerType(), "number of shifts" );
             // FIXME : do not introduce shift here, instead needs model-based
             // refinement for constant shifts (#1284)
-            Node shift_lem = NodeManager::currentNM()->mkNode( kind::AND, mkValidPhase( y, d_pi ),
-                               a[0].eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, y, 
-                                              NodeManager::currentNM()->mkNode( kind::MULT, NodeManager::currentNM()->mkConst( Rational(2) ), shift, d_pi ) ) ),
-                               //particular case of above for shift=0
-                               NodeManager::currentNM()->mkNode( kind::IMPLIES, mkValidPhase( a[0], d_pi ), a[0].eqNode( y ) ),
-                               new_a.eqNode( a ) );
+            Node shift_lem = NodeManager::currentNM()->mkNode(
+                AND,
+                mkValidPhase(y, d_pi),
+                a[0].eqNode(NodeManager::currentNM()->mkNode(
+                    PLUS,
+                    y,
+                    NodeManager::currentNM()->mkNode(
+                        MULT,
+                        NodeManager::currentNM()->mkConst(Rational(2)),
+                        shift,
+                        d_pi))),
+                // particular case of above for shift=0
+                NodeManager::currentNM()->mkNode(
+                    IMPLIES, mkValidPhase(a[0], d_pi), a[0].eqNode(y)),
+                new_a.eqNode(a));
             //must do preprocess on this one
             Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : shift : " << shift_lem << std::endl;
             d_containing.getOutputChannel().lemma(shift_lem, false, true);
@@ -1213,7 +1249,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
           //verify they have the same model value
           if( d_mv[1][a]!=d_mv[1][itrm->second] ){
             // if not, add congruence lemma
-            Node cong_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, a[0].eqNode( itrm->second[0] ), a.eqNode( itrm->second ) );
+            Node cong_lemma = NodeManager::currentNM()->mkNode(
+                IMPLIES, a[0].eqNode(itrm->second[0]), a.eqNode(itrm->second));
             lemmas.push_back( cong_lemma );
             //Assert( false );
           }
@@ -1221,7 +1258,9 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
           d_tf_rep_map[a.getKind()][r] = a;
         }
       }
-    }else if( a.getKind()==kind::PI ){
+    }
+    else if (a.getKind() == PI)
+    {
       //TODO?
     }else{
       Assert( false );
@@ -1370,9 +1409,19 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
   
   //------------------------------------tangent planes
-  if (options::nlExtTangentPlanes()) {
-    lemmas = checkTangentPlanes();
-    lemmas_proc = flushLemmas(lemmas);
+  if (options::nlExtTangentPlanes() || options::nlExtTfTangentPlanes())
+  {
+    lemmas_proc = 0;
+    if (options::nlExtTangentPlanes())
+    {
+      lemmas = checkTangentPlanes();
+      lemmas_proc += flushLemmas(lemmas);
+    }
+    if (options::nlExtTfTangentPlanes())
+    {
+      lemmas = checkTranscendentalTangentPlanes();
+      lemmas_proc += flushLemmas(lemmas);
+    }
     if (lemmas_proc > 0) {
       Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
       return lemmas_proc;
@@ -1592,10 +1641,18 @@ int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const {
 
 void NonlinearExtension::mkPi(){
   if( d_pi.isNull() ){
-    d_pi = NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI );
-    d_pi_2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ) );
-    d_pi_neg_2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(-1)/Rational(2) ) ) );
-    d_pi_neg = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(-1) ) ) );
+    d_pi = NodeManager::currentNM()->mkNullaryOperator(
+        NodeManager::currentNM()->realType(), PI);
+    d_pi_2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
+        MULT,
+        d_pi,
+        NodeManager::currentNM()->mkConst(Rational(1) / Rational(2))));
+    d_pi_neg_2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
+        MULT,
+        d_pi,
+        NodeManager::currentNM()->mkConst(Rational(-1) / Rational(2))));
+    d_pi_neg = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
+        MULT, d_pi, NodeManager::currentNM()->mkConst(Rational(-1))));
     //initialize bounds
     d_pi_bound[0] = NodeManager::currentNM()->mkConst( Rational(333)/Rational(106) );
     d_pi_bound[1] = NodeManager::currentNM()->mkConst( Rational(355)/Rational(113) );
@@ -1603,9 +1660,10 @@ void NonlinearExtension::mkPi(){
 }
 
 void NonlinearExtension::getCurrentPiBounds( std::vector< Node >& lemmas ) {
-  Node pi_lem = NodeManager::currentNM()->mkNode( kind::AND, 
-                  NodeManager::currentNM()->mkNode( kind::GT, d_pi, d_pi_bound[0] ),
-                  NodeManager::currentNM()->mkNode( kind::LT, d_pi, d_pi_bound[1] ) );
+  Node pi_lem = NodeManager::currentNM()->mkNode(
+      AND,
+      NodeManager::currentNM()->mkNode(GT, d_pi, d_pi_bound[0]),
+      NodeManager::currentNM()->mkNode(LT, d_pi, d_pi_bound[1]));
   lemmas.push_back( pi_lem );
 }
 
@@ -1658,8 +1716,8 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index,
   Assert(d_mv[1].find(oa) != d_mv[1].end());
   if (a_index == d_m_vlist[a].size()) {
     if (d_mv[1][oa].getConst<Rational>().sgn() != status) {
-      Node lemma = safeConstructNary(kind::AND, exp)
-                       .impNode(mkLit(oa, d_zero, status * 2));
+      Node lemma =
+          safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2));
       lem.push_back(lemma);
     }
     return status;
@@ -1684,8 +1742,8 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index,
         exp.push_back(av.eqNode(d_zero).negate());
         return compareSign(oa, a, a_index + 1, status, exp, lem);
       } else {
-        exp.push_back(NodeManager::currentNM()->mkNode(
-            sgn == 1 ? kind::GT : kind::LT, av, d_zero));
+        exp.push_back(
+            NodeManager::currentNM()->mkNode(sgn == 1 ? GT : LT, av, d_zero));
         return compareSign(oa, a, a_index + 1, status * sgn, exp, lem);
       }
     }
@@ -1764,8 +1822,7 @@ bool NonlinearExtension::compareMonomial(
         }
       }
       Node clem = NodeManager::currentNM()->mkNode(
-          kind::IMPLIES, safeConstructNary(kind::AND, exp),
-          mkLit(oa, ob, status, 1));
+          IMPLIES, safeConstructNary(AND, exp), mkLit(oa, ob, status, 1));
       Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl;
       lem.push_back(clem);
       cmp_infers[status][oa][ob] = clem;
@@ -2149,21 +2206,21 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() {
               
                 // tangent plane
                 Node tplane = NodeManager::currentNM()->mkNode(
-                    kind::MINUS,
+                    MINUS,
                     NodeManager::currentNM()->mkNode(
-                        kind::PLUS,
-                        NodeManager::currentNM()->mkNode(kind::MULT, b_v, a),
-                        NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)),
-                    NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v));
+                        PLUS,
+                        NodeManager::currentNM()->mkNode(MULT, b_v, a),
+                        NodeManager::currentNM()->mkNode(MULT, a_v, b)),
+                    NodeManager::currentNM()->mkNode(MULT, a_v, b_v));
                 for (unsigned d = 0; d < 4; d++) {
                   Node aa = NodeManager::currentNM()->mkNode(
-                      d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v);
+                      d == 0 || d == 3 ? GEQ : LEQ, a, a_v);
                   Node ab = NodeManager::currentNM()->mkNode(
-                      d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v);
+                      d == 1 || d == 3 ? GEQ : LEQ, b, b_v);
                   Node conc = NodeManager::currentNM()->mkNode(
-                      d <= 1 ? kind::LEQ : kind::GEQ, t, tplane);
+                      d <= 1 ? LEQ : GEQ, t, tplane);
                   Node tlem = NodeManager::currentNM()->mkNode(
-                      kind::OR, aa.negate(), ab.negate(), conc);
+                      OR, aa.negate(), ab.negate(), conc);
                   Trace("nl-ext-tplanes")
                       << "Tangent plane lemma : " << tlem << std::endl;
                   lemmas.push_back(tlem);
@@ -2191,8 +2248,8 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
            d_containing.facts_begin();
        it != d_containing.facts_end(); ++it) {
     Node lit = (*it).assertion;
-    bool polarity = lit.getKind() != kind::NOT;
-    Node atom = lit.getKind() == kind::NOT ? lit[0] : lit;
+    bool polarity = lit.getKind() != NOT;
+    Node atom = lit.getKind() == NOT ? lit[0] : lit;
     registerConstraint(atom);
     bool is_false_lit = false_asserts.find(lit) != false_asserts.end();
     // add information about bounds to variables
@@ -2211,19 +2268,20 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
         Node exp = lit;
         if (!polarity) {
           // reverse
-          if (type == kind::EQUAL) {
+          if (type == EQUAL)
+          {
             // we will take the strict inequality in the direction of the
             // model
             Node lhs = QuantArith::mkCoeffTerm(coeff, x);
-            Node query = NodeManager::currentNM()->mkNode(kind::GT, lhs, rhs);
+            Node query = NodeManager::currentNM()->mkNode(GT, lhs, rhs);
             Node query_mv = computeModelValue(query, 1);
             if (query_mv == d_true) {
               exp = query;
-              type = kind::GT;
+              type = GT;
             } else {
               Assert(query_mv == d_false);
-              exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs);
-              type = kind::LT;
+              exp = NodeManager::currentNM()->mkNode(LT, lhs, rhs);
+              type = LT;
             }
           } else {
             type = negateKind(type);
@@ -2246,7 +2304,8 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
           Trace("nl-ext-bound-debug2")
               << "Joining kinds : " << type << " " << its->second << std::endl;
           Kind jk = joinKinds(type, its->second);
-          if (jk == kind::UNDEFINED_KIND) {
+          if (jk == UNDEFINED_KIND)
+          {
             updated = false;
           } else if (jk != its->second) {
             if (jk == type) {
@@ -2255,7 +2314,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
             } else {
               d_ci[x][coeff][rhs] = jk;
               d_ci_exp[x][coeff][rhs] = NodeManager::currentNM()->mkNode(
-                  kind::AND, d_ci_exp[x][coeff][rhs], exp);
+                  AND, d_ci_exp[x][coeff][rhs], exp);
             }
           } else {
             updated = false;
@@ -2282,20 +2341,25 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
               bool needsRefine = false;
               bool refineDir;
               if (rhs_v == x_v) {
-                if (type == kind::GT) {
+                if (type == GT)
+                {
                   needsRefine = true;
                   refineDir = true;
-                } else if (type == kind::LT) {
+                }
+                else if (type == LT)
+                {
                   needsRefine = true;
                   refineDir = false;
                 }
               } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) {
-                if (type != kind::GT && type != kind::GEQ) {
+                if (type != GT && type != GEQ)
+                {
                   needsRefine = true;
                   refineDir = false;
                 }
               } else {
-                if (type != kind::LT && type != kind::LEQ) {
+                if (type != LT && type != LEQ)
+                {
                   needsRefine = true;
                   refineDir = true;
                 }
@@ -2328,7 +2392,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
   Node null_coeff;
   for (unsigned j = 0; j < d_mterms.size(); j++) {
     Node n = d_mterms[j];
-    d_ci[n][null_coeff][n] = kind::EQUAL;
+    d_ci[n][null_coeff][n] = EQUAL;
     d_ci_exp[n][null_coeff][n] = d_true;
     d_ci_max[n][null_coeff][n] = false;
   }
@@ -2381,9 +2445,9 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
                     Kind infer_type =
                         mmv_sign == -1 ? reverseRelationKind(type) : type;
                     Node infer_lhs =
-                        NodeManager::currentNM()->mkNode(kind::MULT, mult, t);
+                        NodeManager::currentNM()->mkNode(MULT, mult, t);
                     Node infer_rhs =
-                        NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs);
+                        NodeManager::currentNM()->mkNode(MULT, mult, rhs);
                     Node infer = NodeManager::currentNM()->mkNode(
                         infer_type, infer_lhs, infer_rhs);
                     Trace("nl-ext-bound-debug") << "     " << infer << std::endl;
@@ -2397,12 +2461,12 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
                         << std::endl;
                     if (infer_mv == d_false) {
                       Node exp = NodeManager::currentNM()->mkNode(
-                          kind::AND,
+                          AND,
                           NodeManager::currentNM()->mkNode(
-                              mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero),
+                              mmv_sign == 1 ? GT : LT, mult, d_zero),
                           d_ci_exp[x][coeff][rhs]);
-                      Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
-                                                                    exp, infer);
+                      Node iblem =
+                          NodeManager::currentNM()->mkNode(IMPLIES, exp, infer);
                       Node pr_iblem = iblem;
                       iblem = Rewriter::rewrite(iblem);
                       bool introNewTerms = hasNewMonomials(iblem, d_ms);
@@ -2444,8 +2508,8 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals
            d_containing.facts_begin();
        it != d_containing.facts_end(); ++it) {
     Node lit = (*it).assertion;
-    bool polarity = lit.getKind() != kind::NOT;
-    Node atom = lit.getKind() == kind::NOT ? lit[0] : lit;
+    bool polarity = lit.getKind() != NOT;
+    Node atom = lit.getKind() == NOT ? lit[0] : lit;
     if( false_asserts.find(lit) != false_asserts.end() || d_skolem_atoms.find(atom)!=d_skolem_atoms.end() ){
       std::map<Node, Node> msum;
       if (QuantArith::getMonomialSumLit(atom, msum)) {
@@ -2470,7 +2534,7 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals
                   if( !itm->second.isNull() ){
                     children.push_back( itm->second );
                   }
-                  Node val = NodeManager::currentNM()->mkNode( kind::MULT, children );
+                  Node val = NodeManager::currentNM()->mkNode(MULT, children);
                   if( !itm->second.isNull() ){
                     children.pop_back();
                   }
@@ -2488,12 +2552,13 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals
         }
         for( std::map< Node, std::vector< Node > >::iterator itf = factor_to_mono.begin(); itf != factor_to_mono.end(); ++itf ){
           if( itf->second.size()>1 ){
-            Node sum = NodeManager::currentNM()->mkNode( kind::PLUS, itf->second );
+            Node sum = NodeManager::currentNM()->mkNode(PLUS, itf->second);
             sum = Rewriter::rewrite( sum );
             Trace("nl-ext-factor") << "* Factored sum for " << itf->first << " : " << sum << std::endl;
             Node kf = getFactorSkolem( sum, lemmas ); 
             std::vector< Node > poly;
-            poly.push_back( NodeManager::currentNM()->mkNode( kind::MULT, itf->first, kf ) );
+            poly.push_back(
+                NodeManager::currentNM()->mkNode(MULT, itf->first, kf));
             std::map< Node, std::vector< Node > >::iterator itfo = factor_to_mono_orig.find( itf->first );
             Assert( itfo!=factor_to_mono_orig.end() );
             for( std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
@@ -2501,7 +2566,9 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals
                 poly.push_back( QuantArith::mkCoeffTerm(itm->second, itm->first.isNull() ? d_one : itm->first) );
               }
             }
-            Node polyn = poly.size()==1 ? poly[0] : NodeManager::currentNM()->mkNode( kind::PLUS, poly );
+            Node polyn = poly.size() == 1
+                             ? poly[0]
+                             : NodeManager::currentNM()->mkNode(PLUS, poly);
             Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl;
             Node conc_lit = NodeManager::currentNM()->mkNode( atom.getKind(), polyn, d_zero );
             conc_lit = Rewriter::rewrite( conc_lit );
@@ -2513,7 +2580,7 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals
             std::vector< Node > lemma_disj;
             lemma_disj.push_back( lit.negate() );
             lemma_disj.push_back( conc_lit );
-            Node flem = NodeManager::currentNM()->mkNode( kind::OR, lemma_disj );
+            Node flem = NodeManager::currentNM()->mkNode(OR, lemma_disj);
             Trace("nl-ext-factor") << "...lemma is " << flem << std::endl;
             lemmas.push_back( flem ); 
           }
@@ -2585,8 +2652,8 @@ std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {
                        itcac->second.begin();
                    itcar != itcac->second.end(); ++itcar) {
                 Node rhs_a = itcar->first;
-                Node rhs_a_res_base = NodeManager::currentNM()->mkNode(
-                    kind::MULT, itb->second, rhs_a);
+                Node rhs_a_res_base =
+                    NodeManager::currentNM()->mkNode(MULT, itb->second, rhs_a);
                 rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
                 if (!hasNewMonomials(rhs_a_res_base, d_ms)) {
                   Kind type_a = itcar->second;
@@ -2604,7 +2671,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {
                          itcbr != itcbc->second.end(); ++itcbr) {
                       Node rhs_b = itcbr->first;
                       Node rhs_b_res = NodeManager::currentNM()->mkNode(
-                          kind::MULT, ita->second, rhs_b);
+                          MULT, ita->second, rhs_b);
                       rhs_b_res = QuantArith::mkCoeffTerm(coeff_a, rhs_b_res);
                       rhs_b_res = Rewriter::rewrite(rhs_b_res);
                       if (!hasNewMonomials(rhs_b_res, d_ms)) {
@@ -2632,25 +2699,25 @@ std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {
                           }
                           if (pivot_factor_sign == 1) {
                             exp.push_back(NodeManager::currentNM()->mkNode(
-                                kind::GT, pivot_factor, d_zero));
+                                GT, pivot_factor, d_zero));
                           } else {
                             exp.push_back(NodeManager::currentNM()->mkNode(
-                                kind::LT, pivot_factor, d_zero));
+                                LT, pivot_factor, d_zero));
                           }
                         }
                         Kind jk = transKinds(types[0], types[1]);
                         Trace("nl-ext-rbound-debug")
                             << "trans kind : " << types[0] << " + "
                             << types[1] << " = " << jk << std::endl;
-                        if (jk != kind::UNDEFINED_KIND) {
+                        if (jk != UNDEFINED_KIND)
+                        {
                           Node conc = NodeManager::currentNM()->mkNode(
                               jk, rhs_a_res, rhs_b_res);
                           Node conc_mv = computeModelValue(conc, 1);
                           if (conc_mv == d_false) {
                             Node rblem = NodeManager::currentNM()->mkNode(
-                                kind::IMPLIES,
-                                NodeManager::currentNM()->mkNode(kind::AND,
-                                                                 exp),
+                                IMPLIES,
+                                NodeManager::currentNM()->mkNode(AND, exp),
                                 conc);
                             Trace("nl-ext-rbound-lemma-debug")
                                 << "Resolution bound lemma "
@@ -2693,67 +2760,88 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
       if( d_tf_initial_refine.find( t )==d_tf_initial_refine.end() ){
         d_tf_initial_refine[t] = true;
         Node lem;
-        if( it->first==kind::SINE ){
-          Node symn = NodeManager::currentNM()->mkNode( kind::SINE, 
-                        NodeManager::currentNM()->mkNode( kind::MULT, d_neg_one, t[0] ) );
+        if (it->first == SINE)
+        {
+          Node symn = NodeManager::currentNM()->mkNode(
+              SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0]));
           symn = Rewriter::rewrite( symn );
           //can assume its basis since phase is split over 0
           d_trig_is_base[symn] = true;
           Assert( d_trig_is_base.find( t ) != d_trig_is_base.end() );
           std::vector< Node > children;
-          
-          lem = NodeManager::currentNM()->mkNode( kind::AND, 
-                  //bounds
-                  NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::LEQ, t, d_one ),
-                    NodeManager::currentNM()->mkNode( kind::GEQ, t, d_neg_one ) ),
-                  //symmetry
-                  NodeManager::currentNM()->mkNode( kind::PLUS, t, symn ).eqNode( d_zero ),
-                  //sign
-                  NodeManager::currentNM()->mkNode( kind::EQUAL, 
-                    NodeManager::currentNM()->mkNode( kind::LT, t[0], d_zero ),
-                    NodeManager::currentNM()->mkNode( kind::LT, t, d_zero ) ),
-                  //zero val
-                  NodeManager::currentNM()->mkNode( kind::EQUAL, 
-                    NodeManager::currentNM()->mkNode( kind::GT, t[0], d_zero ),
-                    NodeManager::currentNM()->mkNode( kind::GT, t, d_zero ) ) );
-           lem = NodeManager::currentNM()->mkNode( kind::AND, lem,
-                  //zero tangent
-                  NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
-                      NodeManager::currentNM()->mkNode( kind::GT, t[0], d_zero ),
-                      NodeManager::currentNM()->mkNode( kind::LT, t, t[0] ) ),
-                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
-                      NodeManager::currentNM()->mkNode( kind::LT, t[0], d_zero ),
-                      NodeManager::currentNM()->mkNode( kind::GT, t, t[0] ) ) ),
-                  //pi tangent
-                  NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
-                      NodeManager::currentNM()->mkNode( kind::LT, t[0], d_pi ),
-                      NodeManager::currentNM()->mkNode( kind::LT, t, NodeManager::currentNM()->mkNode( kind::MINUS, d_pi, t[0] ) ) ),
-                    NodeManager::currentNM()->mkNode( kind::IMPLIES,
-                      NodeManager::currentNM()->mkNode( kind::GT, t[0], d_pi_neg ),
-                      NodeManager::currentNM()->mkNode( kind::GT, t, NodeManager::currentNM()->mkNode( kind::MINUS, d_pi_neg, t[0] ) ) ) ) );
-        }else if( it->first==kind::EXPONENTIAL ){
+
+          lem = NodeManager::currentNM()->mkNode(
+              AND,
+              // bounds
+              NodeManager::currentNM()->mkNode(
+                  AND,
+                  NodeManager::currentNM()->mkNode(LEQ, t, d_one),
+                  NodeManager::currentNM()->mkNode(GEQ, t, d_neg_one)),
+              // symmetry
+              NodeManager::currentNM()->mkNode(PLUS, t, symn).eqNode(d_zero),
+              // sign
+              NodeManager::currentNM()->mkNode(
+                  EQUAL,
+                  NodeManager::currentNM()->mkNode(LT, t[0], d_zero),
+                  NodeManager::currentNM()->mkNode(LT, t, d_zero)),
+              // zero val
+              NodeManager::currentNM()->mkNode(
+                  EQUAL,
+                  NodeManager::currentNM()->mkNode(GT, t[0], d_zero),
+                  NodeManager::currentNM()->mkNode(GT, t, d_zero)));
+          lem = NodeManager::currentNM()->mkNode(
+              AND,
+              lem,
+              // zero tangent
+              NodeManager::currentNM()->mkNode(
+                  AND,
+                  NodeManager::currentNM()->mkNode(
+                      IMPLIES,
+                      NodeManager::currentNM()->mkNode(GT, t[0], d_zero),
+                      NodeManager::currentNM()->mkNode(LT, t, t[0])),
+                  NodeManager::currentNM()->mkNode(
+                      IMPLIES,
+                      NodeManager::currentNM()->mkNode(LT, t[0], d_zero),
+                      NodeManager::currentNM()->mkNode(GT, t, t[0]))),
+              // pi tangent
+              NodeManager::currentNM()->mkNode(
+                  AND,
+                  NodeManager::currentNM()->mkNode(
+                      IMPLIES,
+                      NodeManager::currentNM()->mkNode(LT, t[0], d_pi),
+                      NodeManager::currentNM()->mkNode(
+                          LT,
+                          t,
+                          NodeManager::currentNM()->mkNode(MINUS, d_pi, t[0]))),
+                  NodeManager::currentNM()->mkNode(
+                      IMPLIES,
+                      NodeManager::currentNM()->mkNode(GT, t[0], d_pi_neg),
+                      NodeManager::currentNM()->mkNode(
+                          GT,
+                          t,
+                          NodeManager::currentNM()->mkNode(
+                              MINUS, d_pi_neg, t[0])))));
+        }
+        else if (it->first == EXPONENTIAL)
+        {
           // ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) <
           // 1 ) ^ ( x <= 0 V exp( x ) > x + 1 )
           lem = NodeManager::currentNM()->mkNode(
-              kind::AND,
-              NodeManager::currentNM()->mkNode(kind::GT, t, d_zero),
+              AND,
+              NodeManager::currentNM()->mkNode(GT, t, d_zero),
               NodeManager::currentNM()->mkNode(
-                  kind::EQUAL, t[0].eqNode(d_zero), t.eqNode(d_one)),
+                  EQUAL, t[0].eqNode(d_zero), t.eqNode(d_one)),
               NodeManager::currentNM()->mkNode(
-                  kind::EQUAL,
-                  NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero),
-                  NodeManager::currentNM()->mkNode(kind::LT, t, d_one)),
+                  EQUAL,
+                  NodeManager::currentNM()->mkNode(LT, t[0], d_zero),
+                  NodeManager::currentNM()->mkNode(LT, t, d_one)),
               NodeManager::currentNM()->mkNode(
-                  kind::OR,
-                  NodeManager::currentNM()->mkNode(kind::LEQ, t[0], d_zero),
+                  OR,
+                  NodeManager::currentNM()->mkNode(LEQ, t[0], d_zero),
                   NodeManager::currentNM()->mkNode(
-                      kind::GT,
+                      GT,
                       t,
-                      NodeManager::currentNM()->mkNode(
-                          kind::PLUS, t[0], d_one))));
+                      NodeManager::currentNM()->mkNode(PLUS, t[0], d_one))));
         }
         if( !lem.isNull() ){
           lemmas.push_back( lem );
@@ -2805,13 +2893,16 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
       }
       std::vector< Node > mpoints;
       std::vector< Node > mpoints_vals;
-      if( it->first==kind::SINE ){
+      if (it->first == SINE)
+      {
         mpoints.push_back( d_pi );
         mpoints.push_back( d_pi_2 );
         mpoints.push_back(d_zero);
         mpoints.push_back( d_pi_neg_2 );
         mpoints.push_back( d_pi_neg );
-      }else if( it->first==kind::EXPONENTIAL ){
+      }
+      else if (it->first == EXPONENTIAL)
+      {
         mpoints.push_back( Node::null() );
       }
       if( !mpoints.empty() ){
@@ -2877,22 +2968,26 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
           if( !tval.isNull() ){
             Node mono_lem;
             if( monotonic_dir==1 && sval.getConst<Rational>() > tval.getConst<Rational>() ){
-              mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, 
-                            NodeManager::currentNM()->mkNode( kind::GEQ, targ, sarg ),
-                            NodeManager::currentNM()->mkNode( kind::GEQ, t, s ) );
+              mono_lem = NodeManager::currentNM()->mkNode(
+                  IMPLIES,
+                  NodeManager::currentNM()->mkNode(GEQ, targ, sarg),
+                  NodeManager::currentNM()->mkNode(GEQ, t, s));
             }else if( monotonic_dir==-1 && sval.getConst<Rational>() < tval.getConst<Rational>() ){
-              mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, 
-                            NodeManager::currentNM()->mkNode( kind::LEQ, targ, sarg ),
-                            NodeManager::currentNM()->mkNode( kind::LEQ, t, s ) );
+              mono_lem = NodeManager::currentNM()->mkNode(
+                  IMPLIES,
+                  NodeManager::currentNM()->mkNode(LEQ, targ, sarg),
+                  NodeManager::currentNM()->mkNode(LEQ, t, s));
             }
             if( !mono_lem.isNull() ){        
               if( !mono_bounds[0].isNull() ){
                 Assert( !mono_bounds[1].isNull() );
-                mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, 
-                             NodeManager::currentNM()->mkNode( kind::AND, 
-                               mkBounded( mono_bounds[0], targ, mono_bounds[1] ), 
-                               mkBounded( mono_bounds[0], sarg, mono_bounds[1] ) ),
-                             mono_lem );
+                mono_lem = NodeManager::currentNM()->mkNode(
+                    IMPLIES,
+                    NodeManager::currentNM()->mkNode(
+                        AND,
+                        mkBounded(mono_bounds[0], targ, mono_bounds[1]),
+                        mkBounded(mono_bounds[0], sarg, mono_bounds[1])),
+                    mono_lem);
               }      
               Trace("nl-ext-tf-mono") << "Monotonicity lemma : " << mono_lem << std::endl;
               lemmas.push_back( mono_lem );
@@ -2910,16 +3005,424 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
   return lemmas;
 }
 
+std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes()
+{
+  std::vector<Node> lemmas;
+  Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..."
+                  << std::endl;
+
+  NodeManager* nm = NodeManager::currentNM();
+  // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
+  // via Incremental Linearization" by Cimatti et al
+  for (std::pair<const Kind, std::map<Node, Node> >& tfs : d_tf_rep_map)
+  {
+    Kind k = tfs.first;
+    Node tft = nm->mkNode(k, d_zero);
+    Trace("nl-ext-tf-tplanes-debug") << "Taylor variables: " << std::endl;
+    Trace("nl-ext-tf-tplanes-debug")
+        << "          taylor_real_fv : " << d_taylor_real_fv << std::endl;
+    Trace("nl-ext-tf-tplanes-debug")
+        << "     taylor_real_fv_base : " << d_taylor_real_fv_base << std::endl;
+    Trace("nl-ext-tf-tplanes-debug")
+        << " taylor_real_fv_base_rem : " << d_taylor_real_fv_base_rem
+        << std::endl;
+    Trace("nl-ext-tf-tplanes-debug") << std::endl;
+
+    // we substitute into the Taylor sum P_{n,f(0)}( x )
+    std::vector<Node> taylor_vars;
+    taylor_vars.push_back(d_taylor_real_fv);
+
+    // Figure 3: P_l, P_u
+    // mapped to for signs of c
+    std::map<int, Node> poly_approx_bounds[2];
+    std::map<int, Node>
+        poly_approx_bounds_neg[2];  // the negative case is different for exp
+    // n is the Taylor degree we are currently considering
+    unsigned n = 8;
+    // n must be even
+    std::pair<Node, Node> taylor = getTaylor(tft, n);
+    Trace("nl-ext-tf-tplanes-debug") << "Taylor for " << k
+                                     << " is : " << taylor.first << std::endl;
+    Node taylor_sum = Rewriter::rewrite(taylor.first);
+    Trace("nl-ext-tf-tplanes-debug") << "Taylor for " << k
+                                     << " is (post-rewrite) : " << taylor_sum
+                                     << std::endl;
+    Assert(taylor.second.getKind() == MULT);
+    Assert(taylor.second.getNumChildren() == 2);
+    Assert(taylor.second[0].getKind() == DIVISION);
+    Trace("nl-ext-tf-tplanes-debug") << "Taylor remainder for " << k << " is "
+                                     << taylor.second << std::endl;
+    // ru is x^{n+1}/(n+1)!
+    Node ru = nm->mkNode(DIVISION, taylor.second[1], taylor.second[0][1]);
+    ru = Rewriter::rewrite(ru);
+    Trace("nl-ext-tf-tplanes-debug")
+        << "Taylor remainder factor is (post-rewrite) : " << ru << std::endl;
+    if (k == EXPONENTIAL)
+    {
+      poly_approx_bounds[0][1] = taylor_sum;
+      poly_approx_bounds[0][-1] = taylor_sum;
+      poly_approx_bounds[1][1] = Rewriter::rewrite(
+          nm->mkNode(MULT, taylor_sum, nm->mkNode(PLUS, d_one, ru)));
+      poly_approx_bounds[1][-1] =
+          Rewriter::rewrite(nm->mkNode(PLUS, taylor_sum, ru));
+    }
+    else
+    {
+      Assert(k == SINE);
+      poly_approx_bounds[0][1] =
+          Rewriter::rewrite(nm->mkNode(MINUS, taylor_sum, ru));
+      poly_approx_bounds[0][-1] = poly_approx_bounds[0][1];
+      poly_approx_bounds[1][1] =
+          Rewriter::rewrite(nm->mkNode(PLUS, taylor_sum, ru));
+      poly_approx_bounds[1][-1] = poly_approx_bounds[1][1];
+    }
+    Trace("nl-ext-tf-tplanes") << "Polynomial approximation for " << k
+                               << " is: " << std::endl;
+    Trace("nl-ext-tf-tplanes") << " Lower (pos): " << poly_approx_bounds[0][1]
+                               << std::endl;
+    Trace("nl-ext-tf-tplanes") << " Upper (pos): " << poly_approx_bounds[1][1]
+                               << std::endl;
+    Trace("nl-ext-tf-tplanes") << " Lower (neg): " << poly_approx_bounds[0][-1]
+                               << std::endl;
+    Trace("nl-ext-tf-tplanes") << " Upper (neg): " << poly_approx_bounds[1][-1]
+                               << std::endl;
+
+    for (std::pair<const Node, Node>& tfr : tfs.second)
+    {
+      // Figure 3 : tf( x )
+      Node tf = tfr.second;
+
+      bool consider = true;
+      if (k == SINE)
+      {
+        // we do not consider e.g. sin( -1*x ), since considering sin( x ) will
+        // have the same effect
+        consider = tf[0].isVar();
+      }
+      int csign;
+      Node c;
+      if (consider)
+      {
+        // Figure 3 : c
+        c = computeModelValue(tf[0], 1);
+        Assert(c.isConst());
+        csign = c.getConst<Rational>().sgn();
+        consider = csign != 0;
+      }
+
+      if (consider)
+      {
+        Assert(csign == 1 || csign == -1);
+
+        // Figure 3 : v
+        Node v = computeModelValue(tf, 1);
+
+        // check value of tf
+        Trace("nl-ext-tf-tplanes") << "Process tangent plane refinement for "
+                                   << tf << "..." << std::endl;
+        Trace("nl-ext-tf-tplanes") << "  value in model : v = " << v
+                                   << std::endl;
+        Trace("nl-ext-tf-tplanes") << "  arg value in model : c = " << c
+                                   << std::endl;
+
+        // compute the concavity
+        int region = -1;
+        std::unordered_map<Node, int, NodeHashFunction>::iterator itr =
+            d_tf_region.find(tf);
+        if (itr != d_tf_region.end())
+        {
+          region = itr->second;
+          Trace("nl-ext-tf-tplanes") << "  region is : " << region << std::endl;
+        }
+        // Figure 3 : conc
+        int concavity = regionToConcavity(k, itr->second);
+        Trace("nl-ext-tf-tplanes") << "  concavity is : " << concavity
+                                   << std::endl;
+        if (concavity != 0)
+        {
+          // bounds for which we are this concavity
+          // Figure 3: < l, u >
+          Node bounds[2];
+          if (k == SINE)
+          {
+            bounds[0] = regionToLowerBound(k, region);
+            Assert(!bounds[0].isNull());
+            bounds[1] = regionToUpperBound(k, region);
+            Assert(!bounds[1].isNull());
+          }
+
+          // Figure 3: P
+          Node poly_approx;
+
+          // compute whether this is a tangent refinement or a secant refinement
+          bool is_tangent = false;
+          bool is_secant = false;
+          std::map<unsigned, Node> model_values;
+          for (unsigned d = 0; d < 2; d++)
+          {
+            Node pab = poly_approx_bounds[d][csign];
+            if (!pab.isNull())
+            {
+              // { x -> tf[0] }
+              std::vector<Node> taylor_subs;
+              taylor_subs.push_back(tf[0]);
+              Assert(taylor_vars.size() == taylor_subs.size());
+              pab = pab.substitute(taylor_vars.begin(),
+                                   taylor_vars.end(),
+                                   taylor_subs.begin(),
+                                   taylor_subs.end());
+              pab = Rewriter::rewrite(pab);
+              Node v_pab = computeModelValue(pab, 1);
+              model_values[d] = v_pab;
+              Assert(v_pab.isConst());
+              Trace("nl-ext-tf-tplanes-debug") << "...model value of " << pab
+                                               << " is " << v_pab << std::endl;
+              Node comp = nm->mkNode(d == 0 ? LT : GT, v, v_pab);
+              Trace("nl-ext-tf-tplanes-debug") << "...compare : " << comp
+                                               << std::endl;
+              Node compr = Rewriter::rewrite(comp);
+              Trace("nl-ext-tf-tplanes-debug") << "...got : " << compr
+                                               << std::endl;
+              if (compr == d_true)
+              {
+                // beyond the bounds
+                if (d == 0)
+                {
+                  poly_approx = poly_approx_bounds[d][csign];
+                  is_tangent = concavity == 1;
+                  is_secant = concavity == -1;
+                }
+                else
+                {
+                  poly_approx = poly_approx_bounds[d][csign];
+                  is_tangent = concavity == -1;
+                  is_secant = concavity == 1;
+                }
+                Trace("nl-ext-tf-tplanes") << "*** Outside boundary point (";
+                Trace("nl-ext-tf-tplanes") << (d == 0 ? "low" : "high") << ") ";
+                Trace("nl-ext-tf-tplanes") << comp << ", will refine..."
+                                           << std::endl;
+                Trace("nl-ext-tf-tplanes")
+                    << "    poly_approx = " << poly_approx << std::endl;
+                Trace("nl-ext-tf-tplanes") << "    is_tangent = " << is_tangent
+                                           << std::endl;
+                Trace("nl-ext-tf-tplanes") << "    is_secant = " << is_secant
+                                           << std::endl;
+                break;
+              }
+              else
+              {
+                Trace("nl-ext-tf-tplanes") << "  ...within "
+                                           << (d == 0 ? "low" : "high")
+                                           << " bound : ";
+                Trace("nl-ext-tf-tplanes") << comp << std::endl;
+              }
+            }
+          }
+
+          // Figure 3: P( c )
+          Node poly_approx_c;
+          if (is_tangent || is_secant)
+          {
+            Assert(!poly_approx.isNull());
+            std::vector<Node> taylor_subs;
+            taylor_subs.push_back(c);
+            Assert(taylor_vars.size() == taylor_subs.size());
+            poly_approx_c = poly_approx.substitute(taylor_vars.begin(),
+                                                   taylor_vars.end(),
+                                                   taylor_subs.begin(),
+                                                   taylor_subs.end());
+            Trace("nl-ext-tf-tplanes-debug") << "...poly appoximation at c is "
+                                             << poly_approx_c << std::endl;
+          }
+
+          if (is_tangent)
+          {
+            // compute tangent plane
+            // Figure 3: T( x )
+            Node tplane;
+            Node poly_approx_deriv =
+                getDerivative(poly_approx, d_taylor_real_fv);
+            Assert(!poly_approx_deriv.isNull());
+            poly_approx_deriv = Rewriter::rewrite(poly_approx_deriv);
+            Trace("nl-ext-tf-tplanes-debug") << "...derivative of "
+                                             << poly_approx << " is "
+                                             << poly_approx_deriv << std::endl;
+            std::vector<Node> taylor_subs;
+            taylor_subs.push_back(c);
+            Assert(taylor_vars.size() == taylor_subs.size());
+            Node poly_approx_c_deriv =
+                poly_approx_deriv.substitute(taylor_vars.begin(),
+                                             taylor_vars.end(),
+                                             taylor_subs.begin(),
+                                             taylor_subs.end());
+            tplane = nm->mkNode(
+                PLUS,
+                poly_approx_c,
+                nm->mkNode(
+                    MULT, poly_approx_c_deriv, nm->mkNode(MINUS, tf[0], c)));
+
+            Node lem = nm->mkNode(concavity == 1 ? GEQ : LEQ, tf, tplane);
+            std::vector<Node> antec;
+            for (unsigned i = 0; i < 2; i++)
+            {
+              if (!bounds[i].isNull())
+              {
+                antec.push_back(
+                    nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], bounds[i]));
+              }
+            }
+            if (!antec.empty())
+            {
+              Node antec_n =
+                  antec.size() == 1 ? antec[0] : nm->mkNode(AND, antec);
+              lem = nm->mkNode(IMPLIES, antec_n, lem);
+            }
+            Trace("nl-ext-tf-tplanes") << "*** Tangent plane lemma : " << lem
+                                       << std::endl;
+            // Figure 3 : line 9
+            lemmas.push_back(lem);
+          }
+          else if (is_secant)
+          {
+            // bounds are the minimum and maximum previous secant points
+            Assert(std::find(d_secant_points[tf].begin(),
+                             d_secant_points[tf].end(),
+                             c)
+                   == d_secant_points[tf].end());
+            // insert into the vector
+            d_secant_points[tf].push_back(c);
+            // sort
+            SortNonlinearExtension smv;
+            smv.d_nla = this;
+            smv.d_order_type = 0;
+            std::sort(
+                d_secant_points[tf].begin(), d_secant_points[tf].end(), smv);
+            // get the resulting index of c
+            unsigned index =
+                std::find(
+                    d_secant_points[tf].begin(), d_secant_points[tf].end(), c)
+                - d_secant_points[tf].begin();
+            // bounds are the next closest upper/lower bound values
+            if (index > 0)
+            {
+              bounds[0] = d_secant_points[tf][index - 1];
+            }
+            else
+            {
+              // otherwise, we use the lower boundary point for this concavity
+              // region
+              if (k == SINE)
+              {
+                Assert(!bounds[0].isNull());
+              }
+              else if (k == EXPONENTIAL)
+              {
+                // pick c-1
+                bounds[0] = Rewriter::rewrite(nm->mkNode(MINUS, c, d_one));
+              }
+            }
+            if (index < d_secant_points[tf].size() - 1)
+            {
+              bounds[1] = d_secant_points[tf][index + 1];
+            }
+            else
+            {
+              // otherwise, we use the upper boundary point for this concavity
+              // region
+              if (k == SINE)
+              {
+                Assert(!bounds[1].isNull());
+              }
+              else if (k == EXPONENTIAL)
+              {
+                // pick c+1
+                bounds[1] = Rewriter::rewrite(nm->mkNode(PLUS, c, d_one));
+              }
+            }
+            Trace("nl-ext-tf-tplanes-debug")
+                << "...secant bounds are : " << bounds[0] << " ... "
+                << bounds[1] << std::endl;
+
+            for (unsigned s = 0; s < 2; s++)
+            {
+              // compute secant plane
+              Assert(!poly_approx.isNull());
+              Assert(!bounds[s].isNull());
+              // take the model value of l or u (since may contain PI)
+              Node b = computeModelValue(bounds[s], 1);
+              Trace("nl-ext-tf-tplanes-debug") << "...model value of bound "
+                                               << bounds[s] << " is " << b
+                                               << std::endl;
+              Assert(b.isConst());
+              if (c != b)
+              {
+                // Figure 3 : P(l), P(u), for s = 0,1
+                Node poly_approx_b;
+                std::vector<Node> taylor_subs;
+                taylor_subs.push_back(b);
+                Assert(taylor_vars.size() == taylor_subs.size());
+                poly_approx_b = poly_approx.substitute(taylor_vars.begin(),
+                                                       taylor_vars.end(),
+                                                       taylor_subs.begin(),
+                                                       taylor_subs.end());
+                // Figure 3: S_l( x ), S_u( x ) for s = 0,1
+                Node splane;
+                Node rcoeff_n = Rewriter::rewrite(nm->mkNode(MINUS, b, c));
+                Assert(rcoeff_n.isConst());
+                Rational rcoeff = rcoeff_n.getConst<Rational>();
+                Assert(rcoeff.sgn() != 0);
+                splane = nm->mkNode(
+                    PLUS,
+                    poly_approx_b,
+                    nm->mkNode(MULT,
+                               nm->mkNode(MINUS, poly_approx_b, poly_approx_c),
+                               nm->mkConst(Rational(1) / rcoeff),
+                               nm->mkNode(MINUS, tf[0], b)));
+
+                Node lem = nm->mkNode(concavity == 1 ? LEQ : GEQ, tf, splane);
+                // With respect to Figure 3, this is slightly different.
+                // In particular, we chose b to be the model value of bounds[s],
+                // which is a constant although bounds[s] may not be (e.g. if it
+                // contains PI).
+                // To ensure that c...b does not cross an inflection point,
+                // we guard with the symbolic version of bounds[s].
+                // This leads to lemmas e.g. of this form:
+                //   ( c <= x <= PI/2 ) => ( sin(x) < ( P( b ) - P( c ) )*( x -
+                //   b ) + P( b ) )
+                // where b = (PI/2)^M, the current value of PI/2 in the model.
+                // This is sound since we are guarded by the symbolic
+                // representation of PI/2.
+                Node antec_n =
+                    nm->mkNode(AND,
+                               nm->mkNode(GEQ, tf[0], s == 0 ? bounds[s] : c),
+                               nm->mkNode(LEQ, tf[0], s == 0 ? c : bounds[s]));
+                lem = nm->mkNode(IMPLIES, antec_n, lem);
+                Trace("nl-ext-tf-tplanes") << "*** Secant plane lemma : " << lem
+                                           << std::endl;
+                // Figure 3 : line 22
+                lemmas.push_back(lem);
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+
+  return lemmas;
+}
+
 int NonlinearExtension::regionToMonotonicityDir(Kind k, int region)
 {
-  if (k == kind::EXPONENTIAL)
+  if (k == EXPONENTIAL)
   {
     if (region == 1)
     {
       return 1;
     }
   }
-  else if (k == kind::SINE)
+  else if (k == SINE)
   {
     if (region == 1 || region == 4)
     {
@@ -2935,14 +3438,14 @@ int NonlinearExtension::regionToMonotonicityDir(Kind k, int region)
 
 int NonlinearExtension::regionToConcavity(Kind k, int region)
 {
-  if (k == kind::EXPONENTIAL)
+  if (k == EXPONENTIAL)
   {
     if (region == 1)
     {
       return 1;
     }
   }
-  else if (k == kind::SINE)
+  else if (k == SINE)
   {
     if (region == 1 || region == 2)
     {
@@ -2958,7 +3461,7 @@ int NonlinearExtension::regionToConcavity(Kind k, int region)
 
 Node NonlinearExtension::regionToLowerBound(Kind k, int region)
 {
-  if (k == kind::SINE)
+  if (k == SINE)
   {
     if (region == 1)
     {
@@ -2982,7 +3485,7 @@ Node NonlinearExtension::regionToLowerBound(Kind k, int region)
 
 Node NonlinearExtension::regionToUpperBound(Kind k, int region)
 {
-  if (k == kind::SINE)
+  if (k == SINE)
   {
     if (region == 1)
     {
@@ -3008,24 +3511,24 @@ Node NonlinearExtension::getDerivative(Node n, Node x)
 {
   Assert(x.isVar());
   // only handle the cases of the taylor expansion of d
-  if (n.getKind() == kind::EXPONENTIAL)
+  if (n.getKind() == EXPONENTIAL)
   {
     if (n[0] == x)
     {
       return n;
     }
   }
-  else if (n.getKind() == kind::SINE)
+  else if (n.getKind() == SINE)
   {
     if (n[0] == x)
     {
-      Node na = NodeManager::currentNM()->mkNode(kind::MINUS, d_pi_2, n[0]);
-      Node ret = NodeManager::currentNM()->mkNode(kind::SINE, na);
+      Node na = NodeManager::currentNM()->mkNode(MINUS, d_pi_2, n[0]);
+      Node ret = NodeManager::currentNM()->mkNode(SINE, na);
       ret = Rewriter::rewrite(ret);
       return ret;
     }
   }
-  else if (n.getKind() == kind::PLUS)
+  else if (n.getKind() == PLUS)
   {
     std::vector<Node> dchildren;
     for (unsigned i = 0; i < n.getNumChildren(); i++)
@@ -3039,18 +3542,18 @@ Node NonlinearExtension::getDerivative(Node n, Node x)
         dchildren.push_back(dc);
       }
     }
-    return NodeManager::currentNM()->mkNode(kind::PLUS, dchildren);
+    return NodeManager::currentNM()->mkNode(PLUS, dchildren);
   }
-  else if (n.getKind() == kind::MULT)
+  else if (n.getKind() == MULT)
   {
     Assert(n[0].isConst());
     Node dc = getDerivative(n[1], x);
     if (!dc.isNull())
     {
-      return NodeManager::currentNM()->mkNode(kind::MULT, n[0], dc);
+      return NodeManager::currentNM()->mkNode(MULT, n[0], dc);
     }
   }
-  else if (n.getKind() == kind::NONLINEAR_MULT)
+  else if (n.getKind() == NONLINEAR_MULT)
   {
     unsigned xcount = 0;
     std::vector<Node> children;
@@ -3072,7 +3575,7 @@ Node NonlinearExtension::getDerivative(Node n, Node x)
     {
       children[xindex] = NodeManager::currentNM()->mkConst(Rational(xcount));
     }
-    return NodeManager::currentNM()->mkNode(kind::MULT, children);
+    return NodeManager::currentNM()->mkNode(MULT, children);
   }
   else if (n.isVar())
   {
@@ -3115,7 +3618,7 @@ std::pair<Node, Node> NonlinearExtension::getTaylor(TNode fa, unsigned n)
     else
     {
       i_exp_base = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
-          kind::MINUS, d_taylor_real_fv, d_taylor_real_fv_base));
+          MINUS, d_taylor_real_fv, d_taylor_real_fv_base));
     }
     Node i_derv = fac;
     Node i_fact = d_one;
@@ -3126,17 +3629,17 @@ std::pair<Node, Node> NonlinearExtension::getTaylor(TNode fa, unsigned n)
     do
     {
       counter++;
-      if (fa.getKind() == kind::EXPONENTIAL)
+      if (fa.getKind() == EXPONENTIAL)
       {
         // unchanged
       }
-      else if (fa.getKind() == kind::SINE)
+      else if (fa.getKind() == SINE)
       {
         if (i_derv_status % 2 == 1)
         {
           Node arg = NodeManager::currentNM()->mkNode(
-              kind::PLUS, d_pi_2, d_taylor_real_fv_base);
-          i_derv = NodeManager::currentNM()->mkNode(kind::SINE, arg);
+              PLUS, d_pi_2, d_taylor_real_fv_base);
+          i_derv = NodeManager::currentNM()->mkNode(SINE, arg);
         }
         else
         {
@@ -3144,8 +3647,7 @@ std::pair<Node, Node> NonlinearExtension::getTaylor(TNode fa, unsigned n)
         }
         if (i_derv_status >= 2)
         {
-          i_derv =
-              NodeManager::currentNM()->mkNode(kind::MINUS, d_zero, i_derv);
+          i_derv = NodeManager::currentNM()->mkNode(MINUS, d_zero, i_derv);
         }
         i_derv = Rewriter::rewrite(i_derv);
         i_derv_status = i_derv_status == 3 ? 0 : i_derv_status + 1;
@@ -3156,8 +3658,8 @@ std::pair<Node, Node> NonlinearExtension::getTaylor(TNode fa, unsigned n)
         i_derv = i_derv.substitute(x, d_taylor_real_fv_base_rem);
       }
       Node curr = NodeManager::currentNM()->mkNode(
-          kind::MULT,
-          NodeManager::currentNM()->mkNode(kind::DIVISION, i_derv, i_fact),
+          MULT,
+          NodeManager::currentNM()->mkNode(DIVISION, i_derv, i_fact),
           i_exp);
       if (counter == (n + 1))
       {
@@ -3167,16 +3669,15 @@ std::pair<Node, Node> NonlinearExtension::getTaylor(TNode fa, unsigned n)
       {
         sum.push_back(curr);
         i_fact = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
-            kind::MULT,
+            MULT,
             NodeManager::currentNM()->mkConst(Rational(counter)),
             i_fact));
         i_exp = Rewriter::rewrite(
-            NodeManager::currentNM()->mkNode(kind::MULT, i_exp_base, i_exp));
+            NodeManager::currentNM()->mkNode(MULT, i_exp_base, i_exp));
       }
     } while (counter <= n);
-    taylor_sum = sum.size() == 1
-                     ? sum[0]
-                     : NodeManager::currentNM()->mkNode(kind::PLUS, sum);
+    taylor_sum =
+        sum.size() == 1 ? sum[0] : NodeManager::currentNM()->mkNode(PLUS, sum);
 
     if (fac[0] != d_taylor_real_fv_base)
     {
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 7c41fa096..d95b3c0f4 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -705,6 +705,65 @@ private:
   */
   std::vector<Node> checkTranscendentalMonotonic();
 
+  /** check transcendental tangent planes
+  *
+  * Returns a set of valid theory lemmas, based on
+  * computing an "incremental linearization" of
+  * transcendental functions based on the model values
+  * of transcendental functions and their arguments.
+  * It is based on Figure 3 of "Satisfiability
+  * Modulo Transcendental Functions via Incremental
+  * Linearization" by Cimatti et al., CADE 2017.
+  * This schema is not terminating in general.
+  * It is not enabled by default, and can
+  * be enabled by --nl-ext-tf-tplanes.
+  *
+  * Example:
+  *
+  * Assume we have a term sin(y) where M( y ) = 1 where M is the current model.
+  * Note that:
+  *   sin(1) ~= .841471
+  *
+  * The Taylor series and remainder of sin(y) of degree 7 is
+  *   P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5
+  *   R_{7,sin(0),b}( x ) = (-1/5040)*x^7
+  *
+  * This gives us lower and upper bounds :
+  *   P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x )
+  *     ...where note P_u( 1 ) = 4243/5040 ~= .841865
+  *   P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x )
+  *     ...where note P_l( 1 ) = 4241/5040 ~= .841468
+  *
+  * Assume that M( sin(y) ) > P_u( 1 ).
+  * Since the concavity of sine in the region 0 < x < PI/2 is -1,
+  * we add a tangent plane refinement.
+  * The tangent plane at the point 1 in P_u is
+  * given by the formula:
+  *   T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 )
+  * We add the lemma:
+  *   ( 0 < y < PI/2 ) => sin( y ) <= T( y )
+  * which is:
+  *   ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506)
+  *
+  * Assume that M( sin(y) ) < P_u( 1 ).
+  * Since the concavity of sine in the region 0 < x < PI/2 is -1,
+  * we add a secant plane refinement for some constants ( l, u )
+  * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose
+  * l = 0 and u = M( PI/2 ) = 150517/47912.
+  * The secant planes at point 1 for P_l
+  * are given by the formulas:
+  *   S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l )
+  *   S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u )
+  * We add the lemmas:
+  *   ( 0 < y < 1 ) => sin( y ) >= S_l( y )
+  *   ( 1 < y < PI/2 ) => sin( y ) >= S_u( y )
+  * which are:
+  *   ( 0 < y < 1 ) => (sin y) >= 4251/5040*y
+  *   ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
+  *     where c1, c2 are rationals (for brevity, omitted here)
+  *     such that c1 ~= .277 and c2 ~= 2.032.
+  */
+  std::vector<Node> checkTranscendentalTangentPlanes();
   //-------------------------------------------- end lemma schemas
 }; /* class NonlinearExtension */
 
diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index d26d53d07..9881b3e72 100644
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -66,7 +66,20 @@ TESTS =	\
   nta/tan-rewrite.smt2 \
   nta/arrowsmith-050317.smt2 \
   nta/sin-init-tangents.smt2 \
-  nta/cos1-tc.smt2
+  nta/cos1-tc.smt2 \
+  nta/sin1-ub.smt2 \
+  nta/sin1-lb.smt2 \
+  nta/sin2-ub.smt2 \
+  nta/sin2-lb.smt2 \
+  nta/exp1-ub.smt2 \
+  nta/exp1-lb.smt2 \
+  nta/exp-4.5-lt.smt2 \
+  nta/exp-n0.5-ub.smt2 \
+  nta/exp-n0.5-lb.smt2 \
+  nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \
+  nta/NAVIGATION2.smt2
+
+# unsolved : garbage_collect.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/nl/nta/NAVIGATION2.smt2 b/test/regress/regress0/nl/nta/NAVIGATION2.smt2
new file mode 100644
index 000000000..445b8a21e
--- /dev/null
+++ b/test/regress/regress0/nl/nta/NAVIGATION2.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :source |printed by MathSAT|)
+(declare-fun X () Real)
+
+(assert (let ((.def_44 (* (- (/ 11 10)) X)))
+(let ((.def_45 (exp .def_44)))
+(let ((.def_50 (* 250 .def_45)))
+(let ((.def_40 (* (- (/ 13 10)) X)))
+(let ((.def_41 (exp .def_40)))
+(let ((.def_52 (* 173 .def_41)))
+(let ((.def_53 (+ .def_52 .def_50)))
+(let ((.def_54 (* 250 X)))
+(let ((.def_55 (+ .def_54 .def_53)))
+(let ((.def_56 (<= .def_55 (/ 595 2))))
+(let ((.def_57 (not .def_56)))
+(let ((.def_31 (<= 0 X)))
+(let ((.def_32 (not .def_31)))
+(let ((.def_58 (or .def_32 .def_57)))
+(let ((.def_59 (not .def_58)))
+.def_59))))))))))))))))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 b/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
new file mode 100644
index 000000000..5dce6ddca
--- /dev/null
+++ b/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-fun time__AT0@0 () Real)
+(declare-fun instance.y__AT0@0 () Real)
+(declare-fun instance.x__AT0@0 () Real)
+(declare-fun instance.y__AT0@2 () Real)
+(declare-fun event_is_timed__AT0@2 () Bool)
+(declare-fun instance.EVENT.0__AT0@1 () Bool)
+(declare-fun instance.EVENT.1__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@0 () Bool)
+(declare-fun instance.EVENT.0__AT0@0 () Bool)
+(declare-fun instance.EVENT.1__AT0@0 () Bool)
+(declare-fun instance.y__AT0@1 () Real)
+(declare-fun instance.x__AT0@1 () Real)
+(declare-fun time__AT0@1 () Real)
+(declare-fun instance.x__AT0@2 () Real)
+(declare-fun time__AT0@2 () Real)
+(assert (let ((.def_0 (<= instance.y__AT0@2 2.0))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@1))) (let ((.def_3 (not instance.EVENT.0__AT0@1))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_6 (<= time__AT0@1 time__AT0@2))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@1 time__AT0@2))) (let ((.def_10 (or instance.EVENT.1__AT0@1 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) time__AT0@1))) (let ((.def_13 (+ .def_12 time__AT0@2))) (let ((.def_14 (exp .def_13))) (let ((.def_15 (* instance.y__AT0@1 .def_14))) (let ((.def_16 (= instance.y__AT0@2 .def_15))) (let ((.def_17 (* 970143.0 instance.x__AT0@2))) (let ((.def_18 (* (- 970143.0) instance.x__AT0@1))) (let ((.def_19 (+ .def_18 .def_17))) (let ((.def_20 (* (- 242536.0) instance.y__AT0@1))) (let ((.def_21 (+ .def_20 .def_19))) (let ((.def_22 (* 242536.0 instance.y__AT0@2))) (let ((.def_23 (+ .def_22 .def_21))) (let ((.def_24 (= .def_23 0.0))) (let ((.def_25 (and .def_24 .def_16))) (let ((.def_26 (not .def_9))) (let ((.def_27 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_28 (= instance.y__AT0@2 instance.y__AT0@1))) (let ((.def_29 (and .def_28 .def_27))) (let ((.def_30 (or .def_29 .def_26))) (let ((.def_31 (and .def_30 .def_25))) (let ((.def_32 (and .def_31 .def_6))) (let ((.def_33 (or .def_2 .def_32))) (let ((.def_34 (and .def_33 .def_10))) (let ((.def_35 (and .def_3 .def_2))) (let ((.def_36 (or .def_35 .def_34))) (let ((.def_37 (and .def_36 .def_11))) (let ((.def_38 (not .def_35))) (let ((.def_39 (or .def_38 .def_29))) (let ((.def_40 (and .def_39 .def_37))) (let ((.def_41 (not event_is_timed__AT0@1))) (let ((.def_42 (= event_is_timed__AT0@2 .def_41))) (let ((.def_43 (and .def_42 .def_40))) (let ((.def_44 (and .def_43 .def_4))) (let ((.def_45 (not instance.EVENT.1__AT0@0))) (let ((.def_46 (not instance.EVENT.0__AT0@0))) (let ((.def_47 (or .def_46 .def_45))) (let ((.def_48 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_49 (<= time__AT0@0 time__AT0@1))) (let ((.def_50 (or .def_45 .def_49))) (let ((.def_51 (and .def_50 .def_48))) (let ((.def_52 (= time__AT0@0 time__AT0@1))) (let ((.def_53 (or instance.EVENT.1__AT0@0 .def_52))) (let ((.def_54 (and .def_53 .def_51))) (let ((.def_55 (* (- 1.0) time__AT0@0))) (let ((.def_56 (+ .def_55 time__AT0@1))) (let ((.def_57 (exp .def_56))) (let ((.def_58 (* instance.y__AT0@0 .def_57))) (let ((.def_59 (= instance.y__AT0@1 .def_58))) (let ((.def_60 (+ .def_20 .def_18))) (let ((.def_61 (* 970143.0 instance.x__AT0@0))) (let ((.def_62 (+ .def_61 .def_60))) (let ((.def_63 (* 242536.0 instance.y__AT0@0))) (let ((.def_64 (+ .def_63 .def_62))) (let ((.def_65 (= .def_64 0.0))) (let ((.def_66 (and .def_65 .def_59))) (let ((.def_67 (not .def_52))) (let ((.def_68 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_69 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_70 (and .def_69 .def_68))) (let ((.def_71 (or .def_70 .def_67))) (let ((.def_72 (and .def_71 .def_66))) (let ((.def_73 (and .def_72 .def_49))) (let ((.def_74 (or .def_45 .def_73))) (let ((.def_75 (and .def_74 .def_53))) (let ((.def_76 (and .def_46 .def_45))) (let ((.def_77 (or .def_76 .def_75))) (let ((.def_78 (and .def_77 .def_54))) (let ((.def_79 (not .def_76))) (let ((.def_80 (or .def_79 .def_70))) (let ((.def_81 (and .def_80 .def_78))) (let ((.def_82 (not event_is_timed__AT0@0))) (let ((.def_83 (= event_is_timed__AT0@1 .def_82))) (let ((.def_84 (and .def_83 .def_81))) (let ((.def_85 (and .def_84 .def_47))) (let ((.def_86 (<= instance.x__AT0@0 (- (/ 1 2))))) (let ((.def_87 (not .def_86))) (let ((.def_88 (<= 0.0 instance.x__AT0@0))) (let ((.def_89 (not .def_88))) (let ((.def_90 (and .def_89 .def_87))) (let ((.def_91 (<= 0.0 instance.y__AT0@0))) (let ((.def_92 (not .def_91))) (let ((.def_93 (<= (- (/ 1 2)) instance.y__AT0@0))) (let ((.def_94 (and .def_93 .def_92))) (let ((.def_95 (and .def_94 .def_90))) (let ((.def_96 (= time__AT0@0 0.0))) (let ((.def_97 (and .def_96 .def_95))) (let ((.def_98 (and .def_97 .def_85 .def_44 .def_1))) .def_98))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/nta/exp-4.5-lt.smt2 b/test/regress/regress0/nl/nta/exp-4.5-lt.smt2
new file mode 100644
index 000000000..b0d39ff44
--- /dev/null
+++ b/test/regress/regress0/nl/nta/exp-4.5-lt.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(declare-fun x () Real)
+
+(assert (> (exp x) 2000.0))
+(assert (< x 4.5))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
new file mode 100644
index 000000000..33806cf75
--- /dev/null
+++ b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(declare-fun x () Real)
+
+(assert (> (exp (- (/ 1 2))) 0.65))
+(assert (= x (exp (- (/ 1 2)))))
+
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
new file mode 100644
index 000000000..b0ea1b39e
--- /dev/null
+++ b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(declare-fun x () Real)
+
+(assert (< (exp (- (/ 1 2))) 0.6))
+(assert (= x (exp (- (/ 1 2)))))
+
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/exp1-lb.smt2 b/test/regress/regress0/nl/nta/exp1-lb.smt2
new file mode 100644
index 000000000..b0bc3079c
--- /dev/null
+++ b/test/regress/regress0/nl/nta/exp1-lb.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (> (exp 1) 2.719))
+(assert (= x (exp 1)))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/exp1-ub.smt2 b/test/regress/regress0/nl/nta/exp1-ub.smt2
new file mode 100644
index 000000000..3b3a14c89
--- /dev/null
+++ b/test/regress/regress0/nl/nta/exp1-ub.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (< (exp 1) 2.717))
+(assert (= x (exp 1)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin1-lb.smt2 b/test/regress/regress0/nl/nta/sin1-lb.smt2
new file mode 100644
index 000000000..f8070cdb8
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin1-lb.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (> (sin 1) 0.842))
+(assert (= x (sin 1)))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin1-ub.smt2 b/test/regress/regress0/nl/nta/sin1-ub.smt2
new file mode 100644
index 000000000..47d322a77
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin1-ub.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (< (sin 1) 0.8414))
+(assert (= x (sin 1)))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin2-lb.smt2 b/test/regress/regress0/nl/nta/sin2-lb.smt2
new file mode 100644
index 000000000..686708230
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin2-lb.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (> (sin 2) 0.96))
+(assert (= x (sin 2)))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin2-ub.smt2 b/test/regress/regress0/nl/nta/sin2-ub.smt2
new file mode 100644
index 000000000..51c9eb8a9
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin2-ub.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (< (sin 2) 0.901))
+(assert (= x (sin 2)))
+
+(check-sat)