Merge branch 'master' into fixClangWarningsfixClangWarnings

28 files changed, 387 insertions, 218 deletions

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 1e031c322..f4016d032 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -18,7 +18,6 @@
 #include <vector>
 
 #include "base/output.h"
-#include "expr/expr.h"
 #include "expr/node_algorithm.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 7d7d0c23c..482e3bc21 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -170,31 +170,41 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx)
   d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true);
 }
 
-void ExponentialSolver::doSecantLemmas(
-    TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d)
+void ExponentialSolver::doSecantLemmas(TNode e,
+                                       TNode poly_approx,
+                                       TNode center,
+                                       TNode cval,
+                                       unsigned d,
+                                       unsigned actual_d)
 {
-  d_data->doSecantLemmas(
-      getSecantBounds(e, c, d), poly_approx, c, poly_approx_c, e, d, 1);
+  d_data->doSecantLemmas(getSecantBounds(e, center, d),
+                         poly_approx,
+                         center,
+                         cval,
+                         e,
+                         Convexity::CONVEX,
+                         d,
+                         actual_d);
 }
 
 std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e,
-                                                         TNode c,
+                                                         TNode center,
                                                          unsigned d)
 {
-  std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, c, d);
+  std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, center, d);
 
   // Check if we already have neighboring secant points
   if (bounds.first.isNull())
   {
     // pick c-1
     bounds.first = Rewriter::rewrite(
-        NodeManager::currentNM()->mkNode(Kind::MINUS, c, d_data->d_one));
+        NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one));
   }
   if (bounds.second.isNull())
   {
     // pick c+1
     bounds.second = Rewriter::rewrite(
-        NodeManager::currentNM()->mkNode(Kind::PLUS, c, d_data->d_one));
+        NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one));
   }
   return bounds;
 }
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index b20c23e56..b4d08559a 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -87,12 +87,16 @@ class ExponentialSolver
   void doTangentLemma(TNode e, TNode c, TNode poly_approx);
 
   /** Sent secant lemmas around c for e */
-  void doSecantLemmas(
-      TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d);
+  void doSecantLemmas(TNode e,
+                      TNode poly_approx,
+                      TNode center,
+                      TNode cval,
+                      unsigned d,
+                      unsigned actual_d);
 
  private:
   /** Generate bounds for secant lemmas */
-  std::pair<Node, Node> getSecantBounds(TNode e, TNode c, unsigned d);
+  std::pair<Node, Node> getSecantBounds(TNode e, TNode center, unsigned d);
 
   /** Holds common state for transcendental solvers */
   TranscendentalState* d_data;
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 31fd47503..cba85b80e 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -266,19 +266,20 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region)
   // Figure 3: T( x )
   // We use zero slope tangent planes, since the concavity of the Taylor
   // approximation cannot be easily established.
-  int concavity = regionToConcavity(region);
+  Convexity convexity = regionToConvexity(region);
   int mdir = regionToMonotonicityDir(region);
+  bool usec = (mdir == 1) == (convexity == Convexity::CONCAVE);
   Node lem = nm->mkNode(
       Kind::IMPLIES,
       nm->mkNode(
           Kind::AND,
-          nm->mkNode(Kind::GEQ,
-                     e[0],
-                     mdir == concavity ? Node(c) : regionToLowerBound(region)),
-          nm->mkNode(Kind::LEQ,
-                     e[0],
-                     mdir != concavity ? Node(c) : regionToUpperBound(region))),
-      nm->mkNode(concavity == 1 ? Kind::GEQ : Kind::LEQ, e, poly_approx));
+          nm->mkNode(
+              Kind::GEQ, e[0], usec ? Node(c) : regionToLowerBound(region)),
+          nm->mkNode(
+              Kind::LEQ, e[0], usec ? Node(c) : regionToUpperBound(region))),
+      nm->mkNode(convexity == Convexity::CONVEX ? Kind::GEQ : Kind::LEQ,
+                 e,
+                 poly_approx));
 
   Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem
                        << std::endl;
@@ -294,6 +295,7 @@ void SineSolver::doSecantLemmas(TNode e,
                                 TNode c,
                                 TNode poly_approx_c,
                                 unsigned d,
+                                unsigned actual_d,
                                 int region)
 {
   d_data->doSecantLemmas(getSecantBounds(e, c, d, region),
@@ -301,8 +303,9 @@ void SineSolver::doSecantLemmas(TNode e,
                          c,
                          poly_approx_c,
                          e,
+                         regionToConvexity(region),
                          d,
-                         regionToConcavity(region));
+                         actual_d);
 }
 
 std::pair<Node, Node> SineSolver::getSecantBounds(TNode e,
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 9f9102a53..e41e6bd4f 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -93,6 +93,7 @@ class SineSolver
                       TNode c,
                       TNode poly_approx_c,
                       unsigned d,
+                      unsigned actual_d,
                       int region);
 
  private:
@@ -152,15 +153,15 @@ class SineSolver
       default: return 0;
     }
   }
-  int regionToConcavity(int region)
+  Convexity regionToConvexity(int region)
   {
     switch (region)
     {
       case 1:
-      case 2: return -1;
+      case 2: return Convexity::CONCAVE;
       case 3:
-      case 4: return 1;
-      default: return 0;
+      case 4: return Convexity::CONVEX;
+      default: return Convexity::UNKNOWN;
     }
   }
 
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index a373339e9..1b7257f8f 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -212,7 +212,7 @@ void TaylorGenerator::getPolynomialApproximationBounds(
   }
 }
 
-void TaylorGenerator::getPolynomialApproximationBoundForArg(
+unsigned TaylorGenerator::getPolynomialApproximationBoundForArg(
     Kind k, Node c, unsigned d, std::vector<Node>& pbounds)
 {
   getPolynomialApproximationBounds(k, d, pbounds);
@@ -252,7 +252,9 @@ void TaylorGenerator::getPolynomialApproximationBoundForArg(
       getPolynomialApproximationBounds(k, ds, pboundss);
       pbounds[2] = pboundss[2];
     }
+    return ds;
   }
+  return d;
 }
 
 std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf, unsigned d, NlModel& model)
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index c647f7fd2..2dbfcccde 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -79,11 +79,13 @@ class TaylorGenerator
    * polynomials may depend on c. In particular, for P_u+[x] for <k>( c ) where
    * c>0, we return the P_u+[x] from the function above for the minimum degree
    * d' >= d such that (1-c^{2*d'+1}/(2*d'+1)!) is positive.
+   * @return the actual degree of the polynomial approximations (which may be
+   * larger than d).
    */
-  void getPolynomialApproximationBoundForArg(Kind k,
-                                             Node c,
-                                             unsigned d,
-                                             std::vector<Node>& pbounds);
+  unsigned getPolynomialApproximationBoundForArg(Kind k,
+                                                 Node c,
+                                                 unsigned d,
+                                                 std::vector<Node>& pbounds);
 
   /** get transcendental function model bounds
    *
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 8eb69e50b..ad3f49576 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -233,7 +233,8 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
   // mapped to for signs of c
   std::map<int, Node> poly_approx_bounds[2];
   std::vector<Node> pbounds;
-  d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds);
+  unsigned actual_d =
+      d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds);
   poly_approx_bounds[0][1] = pbounds[0];
   poly_approx_bounds[0][-1] = pbounds[1];
   poly_approx_bounds[1][1] = pbounds[2];
@@ -362,11 +363,12 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
   {
     if (k == EXPONENTIAL)
     {
-      d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d);
+      d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, actual_d);
     }
     else if (k == Kind::SINE)
     {
-      d_sineSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, region);
+      d_sineSlv.doSecantLemmas(
+          tf, poly_approx, c, poly_approx_c, d, actual_d, region);
     }
   }
   return true;
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 41ed2c53d..69678c621 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -267,26 +267,26 @@ void TranscendentalState::getCurrentPiBounds()
 }
 
 std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,
-                                                                  TNode c,
+                                                                  TNode center,
                                                                   unsigned d)
 {
   // bounds are the minimum and maximum previous secant points
   // should not repeat secant points: secant lemmas should suffice to
   // rule out previous assignment
-  Assert(
-      std::find(d_secant_points[e][d].begin(), d_secant_points[e][d].end(), c)
-      == d_secant_points[e][d].end());
+  Assert(std::find(
+             d_secant_points[e][d].begin(), d_secant_points[e][d].end(), center)
+         == d_secant_points[e][d].end());
   // Insert into the (temporary) vector. We do not update this vector
   // until we are sure this secant plane lemma has been processed. We do
   // this by mapping the lemma to a side effect below.
   std::vector<Node> spoints = d_secant_points[e][d];
-  spoints.push_back(c);
+  spoints.push_back(center);
 
   // sort
   sortByNlModel(spoints.begin(), spoints.end(), &d_model);
   // get the resulting index of c
   unsigned index =
-      std::find(spoints.begin(), spoints.end(), c) - spoints.begin();
+      std::find(spoints.begin(), spoints.end(), center) - spoints.begin();
 
   // bounds are the next closest upper/lower bound values
   return {index > 0 ? spoints[index - 1] : Node(),
@@ -294,24 +294,40 @@ std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,
 }
 
 Node TranscendentalState::mkSecantPlane(
-    TNode arg, TNode b, TNode c, TNode approx_b, TNode approx_c)
+    TNode arg, TNode lower, TNode upper, TNode lval, TNode uval)
 {
   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, b, c));
+  Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, lower, upper));
   Assert(rcoeff_n.isConst());
   Rational rcoeff = rcoeff_n.getConst<Rational>();
   Assert(rcoeff.sgn() != 0);
-  return nm->mkNode(Kind::PLUS,
-                    approx_b,
-                    nm->mkNode(Kind::MULT,
-                               nm->mkNode(Kind::MINUS, approx_b, approx_c),
-                               nm->mkConst(rcoeff.inverse()),
-                               nm->mkNode(Kind::MINUS, arg, b)));
+  Node res =
+      nm->mkNode(Kind::PLUS,
+                 lval,
+                 nm->mkNode(Kind::MULT,
+                            nm->mkNode(Kind::DIVISION,
+                                       nm->mkNode(Kind::MINUS, lval, uval),
+                                       nm->mkNode(Kind::MINUS, lower, upper)),
+                            nm->mkNode(Kind::MINUS, arg, lower)));
+  Trace("nl-trans") << "Creating secant plane for transcendental function of "
+                    << arg << std::endl;
+  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;
+  return res;
 }
 
-NlLemma TranscendentalState::mkSecantLemma(
-    TNode lower, TNode upper, int concavity, TNode tf, TNode splane)
+NlLemma TranscendentalState::mkSecantLemma(TNode lower,
+                                           TNode upper,
+                                           TNode lapprox,
+                                           TNode uapprox,
+                                           int csign,
+                                           Convexity convexity,
+                                           TNode tf,
+                                           TNode splane,
+                                           unsigned actual_d)
 {
   NodeManager* nm = NodeManager::currentNM();
   // With respect to Figure 3, this is slightly different.
@@ -329,60 +345,73 @@ NlLemma TranscendentalState::mkSecantLemma(
   Node antec_n = nm->mkNode(Kind::AND,
                             nm->mkNode(Kind::GEQ, tf[0], lower),
                             nm->mkNode(Kind::LEQ, tf[0], upper));
+  Trace("nl-trans") << "Bound for secant plane: " << lower << " <= " << tf[0]
+                    << " <= " << upper << std::endl;
+  Trace("nl-trans") << "\t" << antec_n << std::endl;
+  // Convex: actual value is below the secant
+  // Concave: actual value is above the secant
   Node lem = nm->mkNode(
       Kind::IMPLIES,
       antec_n,
-      nm->mkNode(concavity == 1 ? Kind::LEQ : Kind::GEQ, tf, splane));
-  Trace("nl-ext-tftp-debug2")
-      << "*** Secant plane lemma (pre-rewrite) : " << lem << std::endl;
+      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-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl;
+  Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl;
   Assert(d_model.computeAbstractModelValue(lem) == d_false);
   return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_SECANT);
 }
 
 void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
                                          TNode poly_approx,
-                                         TNode c,
-                                         TNode approx_c,
+                                         TNode center,
+                                         TNode cval,
                                          TNode tf,
+                                         Convexity convexity,
                                          unsigned d,
-                                         int concavity)
+                                         unsigned actual_d)
 {
-  Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds.first
-                              << " ... " << bounds.second << std::endl;
-  // take the model value of l or u (since may contain PI)
-  // Make secant from bounds.first to c
-  Node lval = d_model.computeAbstractModelValue(bounds.first);
-  Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.first
-                              << " is " << lval << std::endl;
-  if (lval != c)
+  int csign = center.getConst<Rational>().sgn();
+  Trace("nl-trans") << "...do secant lemma with center " << center << " val "
+                    << cval << " sign " << csign << std::endl;
+  Trace("nl-trans") << "...secant bounds are : " << bounds.first << " ... "
+                    << bounds.second << std::endl;
+  // take the model value of lower (since may contain PI)
+  // Make secant from bounds.first to center
+  Node lower = d_model.computeAbstractModelValue(bounds.first);
+  Trace("nl-trans") << "...model value of bound " << bounds.first << " is "
+                    << lower << std::endl;
+  if (lower != center)
   {
     // Figure 3 : P(l), P(u), for s = 0
-    Node approx_l = Rewriter::rewrite(
-        poly_approx.substitute(d_taylor.getTaylorVariable(), lval));
-    Node splane = mkSecantPlane(tf[0], lval, c, approx_l, approx_c);
-    NlLemma nlem = mkSecantLemma(lval, c, concavity, tf, splane);
+    Node lval = Rewriter::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);
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
-    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
     d_im.addPendingArithLemma(nlem, true);
   }
 
-  // Make secant from c to bounds.second
-  Node uval = d_model.computeAbstractModelValue(bounds.second);
-  Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.second
-                              << " is " << uval << std::endl;
-  if (c != uval)
+  // take the model value of upper (since may contain PI)
+  // Make secant from center to bounds.second
+  Node upper = d_model.computeAbstractModelValue(bounds.second);
+  Trace("nl-trans") << "...model value of bound " << bounds.second << " is "
+                    << upper << std::endl;
+  if (center != upper)
   {
     // Figure 3 : P(l), P(u), for s = 1
-    Node approx_u = Rewriter::rewrite(
-        poly_approx.substitute(d_taylor.getTaylorVariable(), uval));
-    Node splane = mkSecantPlane(tf[0], c, uval, approx_c, approx_u);
-    NlLemma nlem = mkSecantLemma(c, uval, concavity, tf, splane);
+    Node uval = Rewriter::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);
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
-    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
     d_im.addPendingArithLemma(nlem, true);
   }
 }
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 0a4e46eca..e1510c3b3 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -27,6 +27,24 @@ namespace nl {
 namespace transcendental {
 
 /**
+ * This enum indicates whether some function is convex, concave or unknown at
+ * some point.
+ */
+enum class Convexity
+{
+  CONVEX,
+  CONCAVE,
+  UNKNOWN
+};
+inline std::ostream& operator<<(std::ostream& os, Convexity c) {
+  switch (c) {
+    case Convexity::CONVEX: return os << "CONVEX";
+    case Convexity::CONCAVE: return os << "CONCAVE";
+    default: return os << "UNKNOWN";
+  }
+}
+
+/**
  * Holds common state and utilities for transcendental solvers.
  *
  * This includes common lookups and caches as well as generic utilities for
@@ -60,20 +78,24 @@ struct TranscendentalState
    * Get the two closest secant points from the once stored already.
    * "closest" is determined according to the current model.
    * @param e The transcendental term (like (exp t))
-   * @param c The point currently under consideration (probably the model of t)
+   * @param center The point currently under consideration (probably the model
+   * of t)
    * @param d The taylor degree.
    */
-  std::pair<Node, Node> getClosestSecantPoints(TNode e, TNode c, unsigned d);
+  std::pair<Node, Node> getClosestSecantPoints(TNode e,
+                                               TNode center,
+                                               unsigned d);
 
   /**
-   * Construct a secant plane between b and c
+   * Construct a secant plane as function in arg between lower and upper
    * @param arg The argument of the transcendental term
-   * @param b Left secant point
-   * @param c Right secant point
-   * @param approx Approximation for b (not yet substituted)
-   * @param approx_c Approximation for c (already substituted)
+   * @param lower Left secant point
+   * @param upper Right secant point
+   * @param lval Evaluation at lower
+   * @param uval Evaluation at upper
    */
-  Node mkSecantPlane(TNode arg, TNode b, TNode c, TNode approx, TNode approx_c);
+  Node mkSecantPlane(
+      TNode arg, TNode lower, TNode upper, TNode lval, TNode uval);
 
   /**
    * Construct a secant lemma between lower and upper for tf.
@@ -83,26 +105,34 @@ struct TranscendentalState
    * @param tf Current transcendental term
    * @param splane Secant plane as computed by mkSecantPlane()
    */
-  NlLemma mkSecantLemma(
-      TNode lower, TNode upper, int concavity, TNode tf, TNode splane);
+  NlLemma mkSecantLemma(TNode lower,
+                        TNode upper,
+                        TNode lapprox,
+                        TNode uapprox,
+                        int csign,
+                        Convexity convexity,
+                        TNode tf,
+                        TNode splane,
+                        unsigned actual_d);
 
   /**
    * Construct and send secant lemmas (if appropriate)
    * @param bounds Secant bounds
    * @param poly_approx Polynomial approximation
-   * @param c Current point
-   * @param approx_c Approximation for c
+   * @param center Current point
+   * @param cval Evaluation at c
    * @param tf Current transcendental term
    * @param d Current taylor degree
    * @param concavity Concavity in region of c
    */
   void doSecantLemmas(const std::pair<Node, Node>& bounds,
                       TNode poly_approx,
-                      TNode c,
-                      TNode approx_c,
+                      TNode center,
+                      TNode cval,
                       TNode tf,
+                      Convexity convexity,
                       unsigned d,
-                      int concavity);
+                      unsigned actual_d);
 
   Node d_true;
   Node d_false;
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index a0def66c5..a090a58fe 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -21,7 +21,6 @@
 
 #include "expr/dtype.h"
 #include "expr/kind.h"
-#include "expr/type.h"
 #include "expr/type_node.h"
 #include "options/quantifiers_options.h"
 #include "theory/type_enumerator.h"
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 85482bf6d..858710746 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
 }
 
 FpConverter::FpConverter(context::UserContext* user)
-    :
+    : d_additionalAssertions(user)
 #ifdef CVC4_USE_SYMFPU
+      ,
       d_fpMap(user),
       d_rmMap(user),
       d_boolMap(user),
       d_ubvMap(user),
-      d_sbvMap(user),
+      d_sbvMap(user)
 #endif
-      d_additionalAssertions(user)
 {
 }
 
+FpConverter::~FpConverter() {}
+
 #ifdef CVC4_USE_SYMFPU
 Node FpConverter::ufToNode(const fpt &format, const uf &u) const
 {
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 59e65c9e1..6688e8607 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -14,6 +14,8 @@
  ** Uses the symfpu library to convert from floating-point operations to
  ** bit-vectors and propositions allowing the theory to be solved by
  ** 'bit-blasting'.
+ **
+ ** !!! This header is not to be included in any other headers !!!
  **/
 
 #include "cvc4_private.h"
@@ -26,7 +28,7 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "theory/valuation.h"
 #include "util/bitvector.h"
 #include "util/floatingpoint_size.h"
@@ -49,10 +51,6 @@ namespace CVC4 {
 namespace theory {
 namespace fp {
 
-typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction,
-                         TypeNodeHashFunction>
-    PairTypeNodeHashFunction;
-
 /**
  * This is a symfpu symbolic "back-end".  It allows the library to be used to
  * construct bit-vector expressions that compute floating-point operations.
@@ -302,6 +300,20 @@ class floatingPointTypeInfo : public FloatingPointSize
  */
 class FpConverter
 {
+ public:
+  /** Constructor. */
+  FpConverter(context::UserContext*);
+  /** Destructor. */
+  ~FpConverter();
+
+  /** Adds a node to the conversion, returns the converted node */
+  Node convert(TNode);
+
+  /** Gives the node representing the value of a given variable */
+  Node getValue(Valuation&, TNode);
+
+  context::CDList<Node> d_additionalAssertions;
+
  protected:
 #ifdef CVC4_USE_SYMFPU
   typedef symfpuSymbolic::traits traits;
@@ -338,17 +350,6 @@ class FpConverter
   /* Creates the relevant components for a variable */
   uf buildComponents(TNode current);
 #endif
-
- public:
-  context::CDList<Node> d_additionalAssertions;
-
-  FpConverter(context::UserContext *);
-
-  /** Adds a node to the conversion, returns the converted node */
-  Node convert(TNode);
-
-  /** Gives the node representing the value of a given variable */
-  Node getValue(Valuation &, TNode);
 };
 
 }  // namespace fp
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 0b15486e2..01fab92c8 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "options/fp_options.h"
+#include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -108,7 +109,7 @@ TheoryFp::TheoryFp(context::Context* c,
     : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
       d_notification(*this),
       d_registeredTerms(u),
-      d_conv(u),
+      d_conv(new FpConverter(u)),
       d_expansionRequested(false),
       d_conflictNode(c, Node::null()),
       d_minMap(u),
@@ -116,9 +117,9 @@ TheoryFp::TheoryFp(context::Context* c,
       d_toUBVMap(u),
       d_toSBVMap(u),
       d_toRealMap(u),
-      realToFloatMap(u),
-      floatToRealMap(u),
-      abstractionMap(u),
+      d_realToFloatMap(u),
+      d_floatToRealMap(u),
+      d_abstractionMap(u),
       d_state(c, u, valuation)
 {
   // indicate we are using the default theory state object
@@ -341,10 +342,10 @@ Node TheoryFp::abstractRealToFloat(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
-  ComparisonUFMap::const_iterator i(realToFloatMap.find(t));
+  ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
 
   Node fun;
-  if (i == realToFloatMap.end())
+  if (i == d_realToFloatMap.end())
   {
     std::vector<TypeNode> args(2);
     args[0] = node[0].getType();
@@ -353,7 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
                        nm->mkFunctionType(args, node.getType()),
                        "floatingpoint_abstract_real_to_float",
                        NodeManager::SKOLEM_EXACT_NAME);
-    realToFloatMap.insert(t, fun);
+    d_realToFloatMap.insert(t, fun);
   }
   else
   {
@@ -361,7 +362,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
   }
   Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
 
-  abstractionMap.insert(uf, node);
+  d_abstractionMap.insert(uf, node);
 
   return uf;
 }
@@ -373,10 +374,10 @@ Node TheoryFp::abstractFloatToReal(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
-  ComparisonUFMap::const_iterator i(floatToRealMap.find(t));
+  ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
 
   Node fun;
-  if (i == floatToRealMap.end())
+  if (i == d_floatToRealMap.end())
   {
     std::vector<TypeNode> args(2);
     args[0] = t;
@@ -385,7 +386,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
                        nm->mkFunctionType(args, nm->realType()),
                        "floatingpoint_abstract_float_to_real",
                        NodeManager::SKOLEM_EXACT_NAME);
-    floatToRealMap.insert(t, fun);
+    d_floatToRealMap.insert(t, fun);
   }
   else
   {
@@ -393,7 +394,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
   }
   Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
 
-  abstractionMap.insert(uf, node);
+  d_abstractionMap.insert(uf, node);
 
   return uf;
 }
@@ -737,9 +738,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
 
 void TheoryFp::convertAndEquateTerm(TNode node) {
   Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
-  size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size();
+  size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size();
 
-  Node converted(d_conv.convert(node));
+  Node converted(d_conv->convert(node));
 
   if (converted != node) {
     Debug("fp-convertTerm")
@@ -748,11 +749,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
         << "TheoryFp::convertTerm(): after  " << converted << std::endl;
   }
 
-  size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size();
+  size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
   Assert(oldAdditionalAssertions <= newAdditionalAssertions);
 
   while (oldAdditionalAssertions < newAdditionalAssertions) {
-    Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions];
+    Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
 
     Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
                             << addA << std::endl;
@@ -953,8 +954,8 @@ void TheoryFp::postCheck(Effort level)
     TheoryModel* m = getValuation().getModel();
     bool lemmaAdded = false;
 
-    for (abstractionMapType::const_iterator i = abstractionMap.begin();
-         i != abstractionMap.end();
+    for (AbstractionMap::const_iterator i = d_abstractionMap.begin();
+         i != d_abstractionMap.end();
          ++i)
     {
       if (m->hasTerm((*i).first))
@@ -1016,7 +1017,7 @@ TrustNode TheoryFp::explain(TNode n)
 }
 
 Node TheoryFp::getModelValue(TNode var) {
-  return d_conv.getValue(d_valuation, var);
+  return d_conv->getValue(d_valuation, var);
 }
 
 bool TheoryFp::collectModelInfo(TheoryModel* m,
@@ -1069,14 +1070,16 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
   }
 
   for (std::set<TNode>::const_iterator i(relevantVariables.begin());
-       i != relevantVariables.end(); ++i) {
+       i != relevantVariables.end();
+       ++i)
+  {
     TNode node = *i;
 
     Trace("fp-collectModelInfo")
         << "TheoryFp::collectModelInfo(): relevantVariable " << node
         << std::endl;
 
-    if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true))
+    if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true))
     {
       return false;
     }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 42c009893..fe91a39bd 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -24,7 +24,6 @@
 #include <utility>
 
 #include "context/cdo.h"
-#include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -33,7 +32,10 @@ namespace CVC4 {
 namespace theory {
 namespace fp {
 
-class TheoryFp : public Theory {
+class FpConverter;
+
+class TheoryFp : public Theory
+{
  public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
   TheoryFp(context::Context* c,
@@ -42,8 +44,9 @@ class TheoryFp : public Theory {
            Valuation valuation,
            const LogicInfo& logicInfo,
            ProofNodeManager* pnm = nullptr);
+
   //--------------------------------- initialization
-  /** get the official theory rewriter of this theory */
+  /** Get the official theory rewriter of this theory. */
   TheoryRewriter* getTheoryRewriter() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
@@ -51,7 +54,7 @@ class TheoryFp : public Theory {
    * documentation in Theory::needsEqualityEngine.
    */
   bool needsEqualityEngine(EeSetupInfo& esi) override;
-  /** finish initialization */
+  /** Finish initialization. */
   void finishInit() override;
   //--------------------------------- end initialization
 
@@ -77,8 +80,10 @@ class TheoryFp : public Theory {
   Node getModelValue(TNode var) override;
   bool collectModelInfo(TheoryModel* m,
                         const std::set<Node>& relevantTerms) override;
-  /** Collect model values in m based on the relevant terms given by
-   * relevantTerms */
+  /**
+   * Collect model values in m based on the relevant terms given by
+   * relevantTerms.
+   */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& relevantTerms) override;
 
@@ -87,7 +92,20 @@ class TheoryFp : public Theory {
   TrustNode explain(TNode n) override;
 
  protected:
-  /** Equality engine */
+  using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
+                                                    TypeNode,
+                                                    TypeNodeHashFunction,
+                                                    TypeNodeHashFunction>;
+  /** Uninterpreted functions for undefined cases of non-total operators. */
+  using ComparisonUFMap =
+      context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
+  /** Uninterpreted functions for lazy handling of conversions. */
+  using ConversionUFMap = context::
+      CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
+  using ConversionAbstractionMap = ComparisonUFMap;
+  using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+
+  /** Equality engine. */
   class NotifyClass : public eq::EqualityEngineNotify {
    protected:
     TheoryFp& d_theorySolver;
@@ -108,14 +126,15 @@ class TheoryFp : public Theory {
 
   NotifyClass d_notification;
 
-  /** General utility **/
+  /** General utility. */
   void registerTerm(TNode node);
   bool isRegistered(TNode node);
 
   context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
 
-  /** Bit-blasting conversion */
-  FpConverter d_conv;
+  /** The word-blaster. Translates FP -> BV. */
+  std::unique_ptr<FpConverter> d_conv;
+
   bool d_expansionRequested;
 
   void convertAndEquateTerm(TNode node);
@@ -133,44 +152,30 @@ class TheoryFp : public Theory {
    */
   void conflictEqConstantMerge(TNode t1, TNode t2);
 
-  context::CDO<Node> d_conflictNode;
-
-  typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
-      ComparisonUFMap;
-
-  ComparisonUFMap d_minMap;
-  ComparisonUFMap d_maxMap;
+  bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
 
   Node minUF(Node);
   Node maxUF(Node);
 
-  typedef context::CDHashMap<std::pair<TypeNode, TypeNode>, Node,
-                             PairTypeNodeHashFunction>
-      ConversionUFMap;
-
-  ConversionUFMap d_toUBVMap;
-  ConversionUFMap d_toSBVMap;
-
   Node toUBVUF(Node);
   Node toSBVUF(Node);
 
-  ComparisonUFMap d_toRealMap;
-
   Node toRealUF(Node);
 
-  /** Uninterpretted functions for lazy handling of conversions */
-  typedef ComparisonUFMap conversionAbstractionMap;
-
-  conversionAbstractionMap realToFloatMap;
-  conversionAbstractionMap floatToRealMap;
-
   Node abstractRealToFloat(Node);
   Node abstractFloatToReal(Node);
 
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType;
-  abstractionMapType abstractionMap;  // abstract -> original
+ private:
+  context::CDO<Node> d_conflictNode;
 
-  bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
+  ComparisonUFMap d_minMap;
+  ComparisonUFMap d_maxMap;
+  ConversionUFMap d_toUBVMap;
+  ConversionUFMap d_toSBVMap;
+  ComparisonUFMap d_toRealMap;
+  ConversionAbstractionMap d_realToFloatMap;
+  ConversionAbstractionMap d_floatToRealMap;
+  AbstractionMap d_abstractionMap;  // abstract -> original
 
   /** The theory rewriter for this theory. */
   TheoryFpRewriter d_rewriter;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 1a67a2b16..1d917b8f4 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -156,7 +156,11 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         {
           d_parent_quant[q].push_back(qi);
           d_children_quant[qi].push_back(q);
-          Assert(hasAddedCbqiLemma(qi));
+          // may not have added the CEX lemma, but the literal is created by
+          // the following call regardless. One rare case where this can happen
+          // is if both sygus-inst and CEGQI are being run in parallel, and
+          // a parent quantified formula is not handled by CEGQI, but a child
+          // is.
           Node qicel = getCounterexampleLiteral(qi);
           dep.push_back(qi);
           dep.push_back(qicel);
@@ -164,6 +168,9 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       }
       if (!dep.empty())
       {
+        // This lemma states that if the child is active, then the parent must
+        // be asserted, in particular G => Q where G is the CEX literal for the
+        // child and Q is the parent.
         Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
         Trace("cegqi-lemma")
             << "Counterexample dependency lemma : " << dep_lemma << std::endl;
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index aa0e62891..a3938412d 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -21,8 +21,7 @@
 #include <memory>
 #include <vector>
 
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/node.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h
index 9fc8e703c..d39d2a377 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.h
+++ b/src/theory/quantifiers/sygus/sygus_abduct.h
@@ -19,7 +19,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index acafeec3c..48a5dbe06 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -24,7 +24,6 @@
 
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
-#include "expr/type.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/term_util.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 916f2d9b5..4db5f261a 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -20,7 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "smt/smt_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 2c49d9f58..545b35af0 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -18,7 +18,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 297f11690..da9fdd022 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -336,6 +336,8 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
 
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
+  d_lemmas_waiting.clear();
+  d_phase_req_waiting.clear();
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index f68900ccc..e2742c812 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -22,7 +22,6 @@
 #include <memory>
 #include <vector>
 
-#include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "smt/smt_engine.h"
 
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 0b6cf6652..2726097bc 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -438,9 +438,20 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
   }
   else if (id == PfRule::RE_ELIM)
   {
-    Assert(children.size() == 1);
-    Assert(args.empty());
-    return RegExpElimination::eliminate(children[0]);
+    Assert(children.empty());
+    Assert(args.size() == 2);
+    bool isAgg;
+    if (!getBool(args[1], isAgg))
+    {
+      return Node::null();
+    }
+    Node ea = RegExpElimination::eliminate(args[0], isAgg);
+    // if we didn't eliminate, then this trivially proves the reflexive equality
+    if (ea.isNull())
+    {
+      ea = args[0];
+    }
+    return args[0].eqNode(ea);
   }
   else if (id == PfRule::STRING_CODE_INJ)
   {
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 1d0db0e4d..aaa9ffc48 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -20,30 +20,58 @@
 #include "theory/strings/regexp_entail.h"
 #include "theory/strings/theory_strings_utils.h"
 
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::strings;
 
-RegExpElimination::RegExpElimination()
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+RegExpElimination::RegExpElimination(bool isAgg,
+                                     ProofNodeManager* pnm,
+                                     context::Context* c)
+    : d_isAggressive(isAgg),
+      d_pnm(pnm),
+      d_epg(pnm == nullptr
+                ? nullptr
+                : new EagerProofGenerator(pnm, c, "RegExpElimination::epg"))
 {
 }
 
-Node RegExpElimination::eliminate(Node atom)
+Node RegExpElimination::eliminate(Node atom, bool isAgg)
 {
   Assert(atom.getKind() == STRING_IN_REGEXP);
   if (atom[1].getKind() == REGEXP_CONCAT)
   {
-    return eliminateConcat(atom);
+    return eliminateConcat(atom, isAgg);
   }
   else if (atom[1].getKind() == REGEXP_STAR)
   {
-    return eliminateStar(atom);
+    return eliminateStar(atom, isAgg);
   }
   return Node::null();
 }
 
-Node RegExpElimination::eliminateConcat(Node atom)
+TrustNode RegExpElimination::eliminateTrusted(Node atom)
+{
+  Node eatom = eliminate(atom, d_isAggressive);
+  if (!eatom.isNull())
+  {
+    // Currently aggressive doesnt work due to fresh bound variables
+    if (isProofEnabled() && !d_isAggressive)
+    {
+      Node eq = atom.eqNode(eatom);
+      Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive);
+      std::shared_ptr<ProofNode> pn =
+          d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq);
+      d_epg->setProofFor(eq, pn);
+      return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get());
+    }
+    return TrustNode::mkTrustRewrite(atom, eatom, nullptr);
+  }
+  return TrustNode::null();
+}
+
+Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node x = atom[0];
@@ -217,7 +245,7 @@ Node RegExpElimination::eliminateConcat(Node atom)
         // otherwise, we can use indexof to represent some next occurrence
         if (gap_exact[i + 1] && i + 1 != size)
         {
-          if (!options::regExpElimAgg())
+          if (!isAgg)
           {
             canProcess = false;
             break;
@@ -330,7 +358,7 @@ Node RegExpElimination::eliminateConcat(Node atom)
     }
   }
 
-  if (!options::regExpElimAgg())
+  if (!isAgg)
   {
     return Node::null();
   }
@@ -455,9 +483,9 @@ Node RegExpElimination::eliminateConcat(Node atom)
   return Node::null();
 }
 
-Node RegExpElimination::eliminateStar(Node atom)
+Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
 {
-  if (!options::regExpElimAgg())
+  if (!isAgg)
   {
     return Node::null();
   }
@@ -580,3 +608,8 @@ Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id)
                    << "." << std::endl;
   return atomElim;
 }
+bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; }
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h
index 0c1acd29d..9d6fecc93 100644
--- a/src/theory/strings/regexp_elim.h
+++ b/src/theory/strings/regexp_elim.h
@@ -18,6 +18,8 @@
 #define CVC4__THEORY__STRINGS__REGEXP_ELIM_H
 
 #include "expr/node.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace theory {
@@ -33,14 +35,32 @@ namespace strings {
 class RegExpElimination
 {
  public:
-  RegExpElimination();
+  /**
+   * @param isAgg Whether aggressive eliminations are enabled
+   * @param pnm The proof node manager to use (for proofs)
+   * @param c The context to use (for proofs)
+   */
+  RegExpElimination(bool isAgg = false,
+                    ProofNodeManager* pnm = nullptr,
+                    context::Context* c = nullptr);
   /** eliminate membership
    *
    * This method takes as input a regular expression membership atom of the
    * form (str.in.re x R). If this method returns a non-null node ret, then ret
    * is equivalent to atom.
+   *
+   * @param atom The node to eliminate
+   * @param isAgg Whether we apply aggressive elimination techniques
+   * @return The node with regular expressions eliminated, or null if atom
+   * was unchanged.
+   */
+  static Node eliminate(Node atom, bool isAgg);
+
+  /**
+   * Return the trust node corresponding to rewriting n based on eliminate
+   * above.
    */
-  static Node eliminate(Node atom);
+  TrustNode eliminateTrusted(Node atom);
 
  private:
   /** return elimination
@@ -50,9 +70,17 @@ class RegExpElimination
    */
   static Node returnElim(Node atom, Node atomElim, const char* id);
   /** elimination for regular expression concatenation */
-  static Node eliminateConcat(Node atom);
+  static Node eliminateConcat(Node atom, bool isAgg);
   /** elimination for regular expression star */
-  static Node eliminateStar(Node atom);
+  static Node eliminateStar(Node atom, bool isAgg);
+  /** Are proofs enabled? */
+  bool isProofEnabled() const;
+  /** Are aggressive eliminations enabled? */
+  bool d_isAggressive;
+  /** Pointer to the proof node manager */
+  ProofNodeManager* d_pnm;
+  /** An eager proof generator for storing proofs in eliminate trusted above */
+  std::unique_ptr<EagerProofGenerator> d_epg;
 }; /* class RegExpElimination */
 
 }  // namespace strings
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 932b5c8cc..575c33501 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -251,15 +251,13 @@ Node StringsRewriter::rewriteStringLeq(Node n)
   {
     String s = n1[0].getConst<String>();
     String t = n2[0].getConst<String>();
-    // only need to truncate if s is longer
-    if (s.size() > t.size())
+    size_t prefixLen = std::min(s.size(), t.size());
+    s = s.prefix(prefixLen);
+    t = t.prefix(prefixLen);
+    // if the prefixes are not the same, then we can already decide the outcome
+    if (s != t)
     {
-      s = s.prefix(t.size());
-    }
-    // if prefix is not leq, then entire string is not leq
-    if (!s.isLeq(t))
-    {
-      Node ret = nm->mkConst(false);
+      Node ret = nm->mkConst(s.isLeq(t));
       return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX);
     }
   }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a9e2c0051..d3e9e34f1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -997,27 +997,28 @@ void TheoryStrings::checkRegisterTermsNormalForms()
 TrustNode TheoryStrings::ppRewrite(TNode atom)
 {
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
+  TrustNode ret;
   Node atomRet = atom;
   if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
   {
     // aggressive elimination of regular expression membership
-    Node atomElim = d_regexp_elim.eliminate(atomRet);
-    if (!atomElim.isNull())
+    ret = d_regexp_elim.eliminateTrusted(atomRet);
+    if (!ret.isNull())
     {
-      Trace("strings-ppr") << "  rewrote " << atom << " -> " << atomElim
+      Trace("strings-ppr") << "  rewrote " << atom << " -> " << ret.getNode()
                            << " via regular expression elimination."
                            << std::endl;
-      atomRet = atomElim;
+      atomRet = ret.getNode();
     }
   }
   if( !options::stringLazyPreproc() ){
     //eager preprocess here
     std::vector< Node > new_nodes;
     StringsPreprocess* p = d_esolver.getPreprocess();
-    Node ret = p->processAssertion(atomRet, new_nodes);
-    if (ret != atomRet)
+    Node pret = p->processAssertion(atomRet, new_nodes);
+    if (pret != atomRet)
     {
-      Trace("strings-ppr") << "  rewrote " << atomRet << " -> " << ret
+      Trace("strings-ppr") << "  rewrote " << atomRet << " -> " << pret
                            << ", with " << new_nodes.size() << " lemmas."
                            << std::endl;
       for (const Node& lem : new_nodes)
@@ -1026,16 +1027,16 @@ TrustNode TheoryStrings::ppRewrite(TNode atom)
         ++(d_statistics.d_lemmasEagerPreproc);
         d_out->lemma(lem);
       }
-      atomRet = ret;
+      atomRet = pret;
+      // Don't support proofs yet, thus we must return nullptr. This is the
+      // case even if we had proven the elimination via regexp elimination
+      // above.
+      ret = TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
     }else{
       Assert(new_nodes.empty());
     }
   }
-  if (atomRet != atom)
-  {
-    return TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
-  }
-  return TrustNode::null();
+  return ret;
 }
 
 /** run the given inference step */