Adds the interface for the CAD-based arithmetic solver. (#4773)

This PR adds some utilities and, most importantly, the interface of the new
CAD-based solver.
The approach is based on https://arxiv.org/pdf/2003.05633.pdf and the code
structure follows the paper rather closely.

13 files changed, 697 insertions, 145 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 992da9a85..59b559cb2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -306,6 +306,10 @@ libcvc4_add_sources(
   theory/arith/linear_equality.h
   theory/arith/matrix.cpp
   theory/arith/matrix.h
+  theory/arith/nl/cad/cdcac.cpp
+  theory/arith/nl/cad/cdcac.h
+  theory/arith/nl/cad/cdcac_utils.cpp
+  theory/arith/nl/cad/cdcac_utils.h
   theory/arith/nl/cad/constraints.cpp
   theory/arith/nl/cad/constraints.h
   theory/arith/nl/cad/projections.cpp
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
new file mode 100644
index 000000000..18b16bbe8
--- /dev/null
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file cdcac.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implements the CDCAC approach.
+ **
+ ** Implements the CDCAC approach as described in
+ ** https://arxiv.org/pdf/2003.05633.pdf.
+ **/
+
+#include "theory/arith/nl/cad/cdcac.h"
+
+#include "theory/arith/nl/cad/projections.h"
+#include "theory/arith/nl/cad/variable_ordering.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+CDCAC::CDCAC() {}
+
+CDCAC::CDCAC(const std::vector<poly::Variable>& ordering)
+    : d_variableOrdering(ordering)
+{
+}
+
+void CDCAC::reset()
+{
+  d_constraints.reset();
+  d_assignment.clear();
+}
+
+void CDCAC::computeVariableOrdering() {}
+
+Constraints& CDCAC::getConstraints() { return d_constraints; }
+const Constraints& CDCAC::getConstraints() const { return d_constraints; }
+
+const poly::Assignment& CDCAC::getModel() const { return d_assignment; }
+
+const std::vector<poly::Variable>& CDCAC::getVariableOrdering() const
+{
+  return d_variableOrdering;
+}
+
+std::vector<CACInterval> CDCAC::getUnsatIntervals(
+    std::size_t cur_variable) const
+{
+  return {};
+}
+
+std::vector<poly::Polynomial> CDCAC::requiredCoefficients(
+    const poly::Polynomial& p) const
+{
+  return {};
+}
+
+std::vector<poly::Polynomial> CDCAC::constructCharacterization(
+    std::vector<CACInterval>& intervals)
+{
+  return {};
+}
+
+CACInterval CDCAC::intervalFromCharacterization(
+    const std::vector<poly::Polynomial>& characterization,
+    std::size_t cur_variable,
+    const poly::Value& sample)
+{
+  return {};
+}
+
+std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
+{
+  return {};
+}
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
new file mode 100644
index 000000000..88e260ada
--- /dev/null
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -0,0 +1,138 @@
+/*********************                                                        */
+/*! \file cdcac.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implements the CDCAC approach.
+ **
+ ** Implements the CDCAC approach as described in
+ ** https://arxiv.org/pdf/2003.05633.pdf.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
+#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
+
+#include <poly/polyxx.h>
+
+#include <vector>
+
+#include "theory/arith/nl/cad/cdcac_utils.h"
+#include "theory/arith/nl/cad/constraints.h"
+#include "theory/arith/nl/cad/variable_ordering.h"
+#include "theory/arith/nl/nl_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+/**
+ * This class implements Cylindrical Algebraic Coverings as presented in
+ * https://arxiv.org/pdf/2003.05633.pdf
+ */
+class CDCAC
+{
+ public:
+  /** Initialize without a variable ordering. */
+  CDCAC();
+  /** Initialize this method with the given variable ordering. */
+  CDCAC(const std::vector<poly::Variable>& ordering);
+
+  /** Reset this instance. */
+  void reset();
+
+  /** Collect variables from the constraints and compute a variable ordering. */
+  void computeVariableOrdering();
+
+  /**
+   * Returns the constraints as a non-const reference. Can be used to add new
+   * constraints.
+   */
+  Constraints& getConstraints();
+  /** Returns the constraints as a const reference. */
+  const Constraints& getConstraints() const;
+
+  /**
+   * Returns the current assignment. This is a satisfying model if
+   * get_unsat_cover() returned an empty vector.
+   */
+  const poly::Assignment& getModel() const;
+
+  /** Returns the current variable ordering. */
+  const std::vector<poly::Variable>& getVariableOrdering() const;
+
+  /**
+   * Collect all unsatisfiable intervals for the given variable.
+   * Combines unsatisfiable regions from d_constraints evaluated over
+   * d_assignment. Implements Algorithm 2.
+   */
+  std::vector<CACInterval> getUnsatIntervals(std::size_t cur_variable) const;
+
+  /**
+   * Collects the coefficients required for projection from the given
+   * polynomial. Implements Algorithm 6.
+   */
+  std::vector<poly::Polynomial> requiredCoefficients(
+      const poly::Polynomial& p) const;
+
+  /**
+   * Constructs a characterization of the given covering.
+   * A characterization contains polynomials whose roots bound the region around
+   * the current assignment. Implements Algorithm 4.
+   */
+  std::vector<poly::Polynomial> constructCharacterization(
+      std::vector<CACInterval>& intervals);
+
+  /**
+   * Constructs an infeasible interval from a characterization.
+   * Implements Algorithm 5.
+   */
+  CACInterval intervalFromCharacterization(
+      const std::vector<poly::Polynomial>& characterization,
+      std::size_t cur_variable,
+      const poly::Value& sample);
+
+  /**
+   * Main method that checks for the satisfiability of the constraints.
+   * Recursively explores possible assignments and excludes regions based on the
+   * coverings. Returns either a covering for the lowest dimension or an empty
+   * vector. If the covering is empty, the result is SAT and an assignment can
+   * be obtained from d_assignment. If the covering is not empty, the result is
+   * UNSAT and an infeasible subset can be extracted from the returned covering.
+   * Implements Algorithm 2.
+   */
+  std::vector<CACInterval> getUnsatCover(std::size_t cur_variable = 0);
+
+ private:
+  /**
+   * The current assignment. When the method terminates with SAT, it contains a
+   * model for the input constraints.
+   */
+  poly::Assignment d_assignment;
+
+  /** The set of input constraints to be checked for consistency. */
+  Constraints d_constraints;
+
+  /** The computed variable ordering used for this method. */
+  std::vector<poly::Variable> d_variableOrdering;
+
+  /** The object computing the variable ordering. */
+  VariableOrdering d_varOrder;
+};
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp
new file mode 100644
index 000000000..02df1a323
--- /dev/null
+++ b/src/theory/arith/nl/cad/cdcac_utils.cpp
@@ -0,0 +1,269 @@
+/*********************                                                        */
+/*! \file cdcac_utils.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implements utilities for cdcac.
+ **
+ ** Implements utilities for cdcac.
+ **/
+
+#include "theory/arith/nl/cad/cdcac_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+using namespace poly;
+
+bool operator==(const CACInterval& lhs, const CACInterval& rhs)
+{
+  return lhs.d_interval == rhs.d_interval;
+}
+bool operator<(const CACInterval& lhs, const CACInterval& rhs)
+{
+  return lhs.d_interval < rhs.d_interval;
+}
+
+/**
+ * Induces an ordering on poly intervals that is suitable for redundancy
+ * removal as implemented in clean_intervals.
+ */
+inline bool compareForCleanup(const Interval& lhs, const Interval& rhs)
+{
+  const lp_value_t* ll = &(lhs.get_internal()->a);
+  const lp_value_t* lu =
+      lhs.get_internal()->is_point ? ll : &(lhs.get_internal()->b);
+  const lp_value_t* rl = &(rhs.get_internal()->a);
+  const lp_value_t* ru =
+      rhs.get_internal()->is_point ? rl : &(rhs.get_internal()->b);
+
+  int lc = lp_value_cmp(ll, rl);
+  // Lower bound is smaller
+  if (lc < 0) return true;
+  // Lower bound is larger
+  if (lc > 0) return false;
+  // Lower bound type is smaller
+  if (!lhs.get_internal()->a_open && rhs.get_internal()->a_open) return true;
+  // Lower bound type is larger
+  if (lhs.get_internal()->a_open && !rhs.get_internal()->a_open) return false;
+
+  // Attention: Here it differs from the regular interval ordering!
+  int uc = lp_value_cmp(lu, ru);
+  // Upper bound is smaller
+  if (uc < 0) return false;
+  // Upper bound is larger
+  if (uc > 0) return true;
+  // Upper bound type is smaller
+  if (lhs.get_internal()->b_open && !rhs.get_internal()->b_open) return false;
+  // Upper bound type is larger
+  if (!lhs.get_internal()->b_open && rhs.get_internal()->b_open) return true;
+
+  // Identical
+  return false;
+}
+
+bool intervalCovers(const Interval& lhs, const Interval& rhs)
+{
+  const lp_value_t* ll = &(lhs.get_internal()->a);
+  const lp_value_t* lu =
+      lhs.get_internal()->is_point ? ll : &(lhs.get_internal()->b);
+  const lp_value_t* rl = &(rhs.get_internal()->a);
+  const lp_value_t* ru =
+      rhs.get_internal()->is_point ? rl : &(rhs.get_internal()->b);
+
+  int lc = lp_value_cmp(ll, rl);
+  int uc = lp_value_cmp(lu, ru);
+
+  // Lower bound is smaller and upper bound is larger
+  if (lc < 0 && uc > 0) return true;
+  // Lower bound is larger or upper bound is smaller
+  if (lc > 0 || uc < 0) return false;
+
+  // Now both bounds are identical.
+  Assert(lc <= 0 && uc >= 0);
+  Assert(lc == 0 || uc == 0);
+
+  // Lower bound is the same and the bound type is stricter
+  if (lc == 0 && lhs.get_internal()->a_open && !rhs.get_internal()->a_open)
+    return false;
+  // Upper bound is the same and the bound type is stricter
+  if (uc == 0 && lhs.get_internal()->b_open && !rhs.get_internal()->b_open)
+    return false;
+
+  // Both bounds are weaker
+  return true;
+}
+
+bool intervalConnect(const Interval& lhs, const Interval& rhs)
+{
+  Assert(lhs < rhs) << "Can only check for a connection if lhs < rhs.";
+  const lp_value_t* lu = lhs.get_internal()->is_point
+                             ? &(lhs.get_internal()->a)
+                             : &(lhs.get_internal()->b);
+  const lp_value_t* rl = &(rhs.get_internal()->a);
+  int c = lp_value_cmp(lu, rl);
+  if (c < 0)
+  {
+    Trace("libpoly::interval_connect")
+        << lhs << " and " << rhs << " are separated." << std::endl;
+    return false;
+  }
+  if (c > 0)
+  {
+    Trace("libpoly::interval_connect")
+        << lhs << " and " << rhs << " overlap." << std::endl;
+    return true;
+  }
+  Assert(c == 0);
+  if (lhs.get_internal()->is_point || rhs.get_internal()->is_point
+      || !lhs.get_internal()->b_open || !rhs.get_internal()->a_open)
+  {
+    Trace("libpoly::interval_connect")
+        << lhs << " and " << rhs
+        << " touch and the intermediate point is covered." << std::endl;
+    return true;
+  }
+  return false;
+}
+
+void cleanIntervals(std::vector<CACInterval>& intervals)
+{
+  // Simplifies removal of redundancies later on.
+  if (intervals.size() < 2) return;
+
+  // Sort intervals.
+  std::sort(intervals.begin(),
+            intervals.end(),
+            [](const CACInterval& lhs, const CACInterval& rhs) {
+              return compareForCleanup(lhs.d_interval, rhs.d_interval);
+            });
+
+  // Remove intervals that are covered by others.
+  // Implementation roughly follows
+  // https://en.cppreference.com/w/cpp/algorithm/remove Find first interval that
+  // covers the next one.
+  std::size_t first = 0;
+  for (std::size_t n = intervals.size(); first < n - 1; ++first)
+  {
+    if (intervalCovers(intervals[first].d_interval,
+                       intervals[first + 1].d_interval))
+    {
+      break;
+    }
+  }
+  // If such an interval exists, remove accordingly.
+  if (first < intervals.size() - 1)
+  {
+    for (std::size_t i = first + 2, n = intervals.size(); i < n; ++i)
+    {
+      if (!intervalCovers(intervals[first].d_interval, intervals[i].d_interval))
+      {
+        // Interval is not covered. Move it to the front and bump front.
+        ++first;
+        intervals[first] = std::move(intervals[i]);
+      }
+      // Else: Interval is covered as well.
+    }
+    // Erase trailing values
+    while (intervals.size() > first + 1)
+    {
+      intervals.pop_back();
+    }
+  }
+}
+
+std::vector<Node> collectConstraints(const std::vector<CACInterval>& intervals)
+{
+  std::vector<Node> res;
+  for (const auto& i : intervals)
+  {
+    res.insert(res.end(), i.d_origins.begin(), i.d_origins.end());
+  }
+  std::sort(res.begin(), res.end());
+  auto it = std::unique(res.begin(), res.end());
+  res.erase(it, res.end());
+  return res;
+}
+
+bool sampleOutside(const std::vector<CACInterval>& infeasible, Value& sample)
+{
+  if (infeasible.empty())
+  {
+    // No infeasible region, just take anything: zero
+    sample = poly::Integer();
+    return true;
+  }
+  if (!is_minus_infinity(get_lower(infeasible.front().d_interval)))
+  {
+    // First does not cover -oo, just take sufficiently low value
+    Trace("cdcac") << "Sample before " << infeasible.front().d_interval
+                   << std::endl;
+    const auto* i = infeasible.front().d_interval.get_internal();
+    sample = value_between(
+        Value::minus_infty().get_internal(), true, &i->a, !i->a_open);
+    return true;
+  }
+  for (std::size_t i = 0, n = infeasible.size(); i < n - 1; ++i)
+  {
+    // Search for two subsequent intervals that do not connect
+    if (!intervalConnect(infeasible[i].d_interval,
+                         infeasible[i + 1].d_interval))
+    {
+      // Two intervals do not connect, take something from the gap
+      const auto* l = infeasible[i].d_interval.get_internal();
+      const auto* r = infeasible[i + 1].d_interval.get_internal();
+
+      Trace("cdcac") << "Sample between " << infeasible[i].d_interval << " and "
+                     << infeasible[i + 1].d_interval << std::endl;
+
+      if (l->is_point)
+      {
+        sample = value_between(&l->a, true, &r->a, !r->a_open);
+      }
+      else
+      {
+        sample = value_between(&l->b, !l->b_open, &r->a, !r->a_open);
+      }
+      return true;
+    }
+    else
+    {
+      Trace("cdcac") << infeasible[i].d_interval << " and "
+                     << infeasible[i + 1].d_interval << " connect" << std::endl;
+    }
+  }
+  if (!is_plus_infinity(get_upper(infeasible.back().d_interval)))
+  {
+    // Last does not cover oo, just take something sufficiently large
+    Trace("cdcac") << "Sample above " << infeasible.back().d_interval
+                   << std::endl;
+    const auto* i = infeasible.back().d_interval.get_internal();
+    if (i->is_point)
+    {
+      sample =
+          value_between(&i->a, true, Value::plus_infty().get_internal(), true);
+    }
+    else
+    {
+      sample = value_between(
+          &i->b, !i->b_open, Value::plus_infty().get_internal(), true);
+    }
+    return true;
+  }
+  return false;
+}
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
\ No newline at end of file
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
new file mode 100644
index 000000000..d5fa70bd9
--- /dev/null
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -0,0 +1,100 @@
+/*********************                                                        */
+/*! \file cdcac_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implements utilities for cdcac.
+ **
+ ** Implements utilities for cdcac.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
+#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
+
+#include <poly/polyxx.h>
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+/**
+ * An interval as specified in section 4.1 of
+ * https://arxiv.org/pdf/2003.05633.pdf.
+ *
+ * It consists of
+ * - the actual interval, either an open or a point interal,
+ * - the characterizing polynomials of the lower and upper bound,
+ * - the characterizing polynomials in the main variable,
+ * - the characterizing polynomials in lower variables and
+ * - the constraints used to derive this interval.
+ */
+struct CACInterval
+{
+  /** The actual interval. */
+  poly::Interval d_interval;
+  /** The polynomials characterizing the lower bound. */
+  std::vector<poly::Polynomial> d_lowerPolys;
+  /** The polynomials characterizing the upper bound. */
+  std::vector<poly::Polynomial> d_upperPolys;
+  /** The characterizing polynomials in the main variable. */
+  std::vector<poly::Polynomial> d_mainPolys;
+  /** The characterizing polynomials in lower variables. */
+  std::vector<poly::Polynomial> d_downPolys;
+  /** The constraints used to derive this interval. */
+  std::vector<Node> d_origins;
+};
+/** Check whether to intervals are the same. */
+bool operator==(const CACInterval& lhs, const CACInterval& rhs);
+/** Compare two intervals. */
+bool operator<(const CACInterval& lhs, const CACInterval& rhs);
+
+/** Check whether lhs covers rhs. */
+bool intervalCovers(const poly::Interval& lhs, const poly::Interval& rhs);
+/**
+ * Check whether two intervals connect, assuming lhs < rhs.
+ * They connect, if their union has no gap.
+ */
+bool intervalConnect(const poly::Interval& lhs, const poly::Interval& rhs);
+
+/**
+ * Sort intervals according to section 4.4.1.
+ * Also removes fully redundant intervals as in 4.5. 1.
+ */
+void cleanIntervals(std::vector<CACInterval>& intervals);
+
+/**
+ * Collect all origins from the list of intervals to construct the origins for a
+ * whole covering.
+ */
+std::vector<Node> collectConstraints(const std::vector<CACInterval>& intervals);
+
+/**
+ * Sample a point outside of the infeasible intervals.
+ * Stores the sample in sample, returns whether such a sample exists.
+ * If false is returned, the infeasible intervals cover the real line.
+ * Implements sample_outside() from section 4.3
+ */
+bool sampleOutside(const std::vector<CACInterval>& infeasible,
+                   poly::Value& sample);
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp
index b1b9edccc..1e6ca9b5e 100644
--- a/src/theory/arith/nl/cad/constraints.cpp
+++ b/src/theory/arith/nl/cad/constraints.cpp
@@ -9,24 +9,18 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Implements a container for CAD constraints.
  **
  ** Implements a container for CAD constraints.
  **/
 
-#include "constraints.h"
+#include "theory/arith/nl/cad/constraints.h"
 
 #ifdef CVC4_POLY_IMP
 
 #include <algorithm>
 
-#include "../poly_conversion.h"
+#include "theory/arith/nl/poly_conversion.h"
 #include "util/poly_util.h"
 
 namespace CVC4 {
@@ -35,13 +29,33 @@ namespace arith {
 namespace nl {
 namespace cad {
 
-using namespace poly;
+void Constraints::addConstraint(const poly::Polynomial& lhs,
+                                poly::SignCondition sc,
+                                Node n)
+{
+  d_constraints.emplace_back(lhs, sc, n);
+  sortConstraints();
+}
+
+void Constraints::addConstraint(Node n)
+{
+  auto c = as_poly_constraint(n, d_varMapper);
+  addConstraint(c.first, c.second, n);
+  sortConstraints();
+}
 
-void Constraints::sort_constraints()
+const Constraints::ConstraintVector& Constraints::getConstraints() const
+{
+  return d_constraints;
+}
+
+void Constraints::reset() { d_constraints.clear(); }
+
+void Constraints::sortConstraints()
 {
   using Tpl = std::tuple<poly::Polynomial, poly::SignCondition, Node>;
-  std::sort(mConstraints.begin(),
-            mConstraints.end(),
+  std::sort(d_constraints.begin(),
+            d_constraints.end(),
             [](const Tpl& at, const Tpl& bt) {
               // Check if a is smaller than b
               const poly::Polynomial& a = std::get<0>(at);
@@ -54,35 +68,13 @@ void Constraints::sort_constraints()
               if (tda != tdb) return tda < tdb;
               return degree(a) < degree(b);
             });
-  for (auto& c : mConstraints)
+  for (auto& c : d_constraints)
   {
     auto* p = std::get<0>(c).get_internal();
     lp_polynomial_set_external(p);
   }
 }
 
-void Constraints::add_constraint(const Polynomial& lhs,
-                                 SignCondition sc,
-                                 Node n)
-{
-  mConstraints.emplace_back(lhs, sc, n);
-  sort_constraints();
-}
-
-void Constraints::add_constraint(Node n)
-{
-  auto c = as_poly_constraint(n, mVarMapper);
-  add_constraint(c.first, c.second, n);
-  sort_constraints();
-}
-
-const Constraints::ConstraintVector& Constraints::get_constraints() const
-{
-  return mConstraints;
-}
-
-void Constraints::reset() { mConstraints.clear(); }
-
 }  // namespace cad
 }  // namespace nl
 }  // namespace arith
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index eda785d8e..a7989fcb6 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -9,17 +9,13 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Implements a container for CAD constraints.
  **
  ** Implements a container for CAD constraints.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 #define CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 
@@ -33,9 +29,9 @@
 #include <tuple>
 #include <vector>
 
-#include "../poly_conversion.h"
 #include "expr/kind.h"
 #include "expr/node_manager_attributes.h"
+#include "theory/arith/nl/poly_conversion.h"
 
 namespace CVC4 {
 namespace theory {
@@ -50,47 +46,46 @@ class Constraints
   using Constraint = std::tuple<poly::Polynomial, poly::SignCondition, Node>;
   using ConstraintVector = std::vector<Constraint>;
 
- private:
-  /**
-   * A list of constraints, each comprised of a polynomial and a sign
-   * condition.
-   */
-  ConstraintVector mConstraints;
-
-  /**
-   * A mapping from CVC4 variables to poly variables.
-   */
-  VariableMapper mVarMapper;
-
-  void sort_constraints();
-
- public:
-  VariableMapper& var_mapper() { return mVarMapper; }
+  VariableMapper& varMapper() { return d_varMapper; }
 
   /**
    * Add a constraint (represented by a polynomial and a sign condition) to the
    * list of constraints.
    */
-  void add_constraint(const poly::Polynomial& lhs,
-                      poly::SignCondition sc,
-                      Node n);
+  void addConstraint(const poly::Polynomial& lhs,
+                     poly::SignCondition sc,
+                     Node n);
 
   /**
    * Add a constraints (represented by a node) to the list of constraints.
    * The given node can either be a negation (NOT) or a suitable relation symbol
    * as checked by is_suitable_relation().
    */
-  void add_constraint(Node n);
+  void addConstraint(Node n);
 
   /**
    * Gives the list of added constraints.
    */
-  const ConstraintVector& get_constraints() const;
+  const ConstraintVector& getConstraints() const;
 
   /**
    * Remove all constraints.
    */
   void reset();
+
+ private:
+  /**
+   * A list of constraints, each comprised of a polynomial and a sign
+   * condition.
+   */
+  ConstraintVector d_constraints;
+
+  /**
+   * A mapping from CVC4 variables to poly variables.
+   */
+  VariableMapper d_varMapper;
+
+  void sortConstraints();
 };
 
 }  // namespace cad
diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp
index 87d8a3945..488a1f1c6 100644
--- a/src/theory/arith/nl/cad/projections.cpp
+++ b/src/theory/arith/nl/cad/projections.cpp
@@ -9,18 +9,12 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Implements utilities for CAD projection operators.
  **
  ** Implements utilities for CAD projection operators.
  **/
 
-#include "projections.h"
+#include "theory/arith/nl/cad/projections.h"
 
 #ifdef CVC4_POLY_IMP
 
@@ -32,14 +26,14 @@ namespace cad {
 
 using namespace poly;
 
-void reduce_projection_polynomials(std::vector<Polynomial>& polys)
+void reduceProjectionPolynomials(std::vector<Polynomial>& polys)
 {
   std::sort(polys.begin(), polys.end());
   auto it = std::unique(polys.begin(), polys.end());
   polys.erase(it, polys.end());
 }
 
-void add_polynomial(std::vector<Polynomial>& polys, const Polynomial& poly)
+void addPolynomial(std::vector<Polynomial>& polys, const Polynomial& poly)
 {
   for (const auto& p : square_free_factors(poly))
   {
@@ -48,13 +42,13 @@ void add_polynomial(std::vector<Polynomial>& polys, const Polynomial& poly)
   }
 }
 
-void add_polynomials(std::vector<Polynomial>& polys,
-                     const std::vector<Polynomial>& p)
+void addPolynomials(std::vector<Polynomial>& polys,
+                    const std::vector<Polynomial>& p)
 {
-  for (const auto& q : p) add_polynomial(polys, q);
+  for (const auto& q : p) addPolynomial(polys, q);
 }
 
-void make_finest_square_free_basis(std::vector<Polynomial>& polys)
+void makeFinestSquareFreeBasis(std::vector<Polynomial>& polys)
 {
   for (std::size_t i = 0, n = polys.size(); i < n; ++i)
   {
@@ -73,11 +67,11 @@ void make_finest_square_free_basis(std::vector<Polynomial>& polys)
     return is_constant(p);
   });
   polys.erase(it, polys.end());
-  reduce_projection_polynomials(polys);
+  reduceProjectionPolynomials(polys);
 }
 
-void make_finest_square_free_basis(std::vector<poly::Polynomial>& lhs,
-                                   std::vector<poly::Polynomial>& rhs)
+void makeFinestSquareFreeBasis(std::vector<poly::Polynomial>& lhs,
+                               std::vector<poly::Polynomial>& rhs)
 {
   for (std::size_t i = 0, ln = lhs.size(); i < ln; ++i)
   {
@@ -94,8 +88,8 @@ void make_finest_square_free_basis(std::vector<poly::Polynomial>& lhs,
       }
     }
   }
-  reduce_projection_polynomials(lhs);
-  reduce_projection_polynomials(rhs);
+  reduceProjectionPolynomials(lhs);
+  reduceProjectionPolynomials(rhs);
 }
 
 std::vector<Polynomial> projection_mccallum(
@@ -107,19 +101,19 @@ std::vector<Polynomial> projection_mccallum(
   {
     for (const auto& coeff : coefficients(p))
     {
-      add_polynomial(res, coeff);
+      addPolynomial(res, coeff);
     }
-    add_polynomial(res, discriminant(p));
+    addPolynomial(res, discriminant(p));
   }
   for (std::size_t i = 0, n = polys.size(); i < n; ++i)
   {
     for (std::size_t j = i + 1; j < n; ++j)
     {
-      add_polynomial(res, resultant(polys[i], polys[j]));
+      addPolynomial(res, resultant(polys[i], polys[j]));
     }
   }
 
-  reduce_projection_polynomials(res);
+  reduceProjectionPolynomials(res);
   return res;
 }
 
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 39d2b1221..c4a34ee56 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -9,17 +9,13 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Implements utilities for CAD projection operators.
  **
  ** Implements utilities for CAD projection operators.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 #define CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 
@@ -40,33 +36,33 @@ namespace nl {
 namespace cad {
 
 /** Sort and remove duplicates from the list of polynomials. */
-void reduce_projection_polynomials(std::vector<poly::Polynomial>& polys);
+void reduceProjectionPolynomials(std::vector<poly::Polynomial>& polys);
 
 /**
  * Adds a polynomial to the list of projection polynomials.
  * Before adding, it factorizes the polynomials and removed constant factors.
  */
-void add_polynomial(std::vector<poly::Polynomial>& polys,
-                    const poly::Polynomial& poly);
+void addPolynomial(std::vector<poly::Polynomial>& polys,
+                   const poly::Polynomial& poly);
 
 /** Adds a list of polynomials using add_polynomial(). */
-void add_polynomials(std::vector<poly::Polynomial>& polys,
-                     const std::vector<poly::Polynomial>& p);
+void addPolynomials(std::vector<poly::Polynomial>& polys,
+                    const std::vector<poly::Polynomial>& p);
 
 /** Make a set of polynomials a finest square-free basis. */
-void make_finest_square_free_basis(std::vector<poly::Polynomial>& polys);
+void makeFinestSquareFreeBasis(std::vector<poly::Polynomial>& polys);
 
 /**
  * Ensure that two sets of polynomials are finest square-free basis relative to
  * each other.
  */
-void make_finest_square_free_basis(std::vector<poly::Polynomial>& lhs,
-                                   std::vector<poly::Polynomial>& rhs);
+void makeFinestSquareFreeBasis(std::vector<poly::Polynomial>& lhs,
+                               std::vector<poly::Polynomial>& rhs);
 
 /**
  * Computes McCallum's projection operator.
  */
-std::vector<poly::Polynomial> projection_mccallum(
+std::vector<poly::Polynomial> projectionMcCallum(
     const std::vector<poly::Polynomial>& polys);
 
 }  // namespace cad
diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp
index efb2e6350..ca87f8a83 100644
--- a/src/theory/arith/nl/cad/variable_ordering.cpp
+++ b/src/theory/arith/nl/cad/variable_ordering.cpp
@@ -9,18 +9,12 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Implements variable orderings tailored to CAD.
  **
  ** Implements variable orderings tailored to CAD.
  **/
 
-#include "variable_ordering.h"
+#include "theory/arith/nl/cad/variable_ordering.h"
 
 #ifdef CVC4_POLY_IMP
 
@@ -32,12 +26,10 @@ namespace arith {
 namespace nl {
 namespace cad {
 
-using namespace poly;
-
-std::vector<poly_utils::VariableInformation> collect_information(
+std::vector<poly_utils::VariableInformation> collectInformation(
     const Constraints::ConstraintVector& polys, bool with_totals)
 {
-  VariableCollector vc;
+  poly::VariableCollector vc;
   for (const auto& c : polys)
   {
     vc(std::get<0>(c));
@@ -63,7 +55,7 @@ std::vector<poly_utils::VariableInformation> collect_information(
   return res;
 }
 
-std::vector<poly::Variable> get_variables(
+std::vector<poly::Variable> getVariables(
     const std::vector<poly_utils::VariableInformation>& vi)
 {
   std::vector<poly::Variable> res;
@@ -74,22 +66,21 @@ std::vector<poly::Variable> get_variables(
   return res;
 }
 
-std::vector<poly::Variable> sort_byid(
-    const Constraints::ConstraintVector& polys)
+std::vector<poly::Variable> sortByid(const Constraints::ConstraintVector& polys)
 {
-  auto vi = collect_information(polys);
+  auto vi = collectInformation(polys);
   std::sort(
       vi.begin(),
       vi.end(),
       [](const poly_utils::VariableInformation& a,
          const poly_utils::VariableInformation& b) { return a.var < b.var; });
-  return get_variables(vi);
+  return getVariables(vi);
 };
 
-std::vector<poly::Variable> sort_brown(
+std::vector<poly::Variable> sortBrown(
     const Constraints::ConstraintVector& polys)
 {
-  auto vi = collect_information(polys);
+  auto vi = collectInformation(polys);
   std::sort(vi.begin(),
             vi.end(),
             [](const poly_utils::VariableInformation& a,
@@ -100,13 +91,13 @@ std::vector<poly::Variable> sort_brown(
                 return a.max_terms_tdegree > b.max_terms_tdegree;
               return a.num_terms > b.num_terms;
             });
-  return get_variables(vi);
+  return getVariables(vi);
 };
 
-std::vector<poly::Variable> sort_triangular(
+std::vector<poly::Variable> sortTriangular(
     const Constraints::ConstraintVector& polys)
 {
-  auto vi = collect_information(polys);
+  auto vi = collectInformation(polys);
   std::sort(vi.begin(),
             vi.end(),
             [](const poly_utils::VariableInformation& a,
@@ -117,7 +108,7 @@ std::vector<poly::Variable> sort_triangular(
                 return a.max_lc_degree > b.max_lc_degree;
               return a.sum_poly_degree > b.sum_poly_degree;
             });
-  return get_variables(vi);
+  return getVariables(vi);
 };
 
 VariableOrdering::VariableOrdering() {}
@@ -129,9 +120,9 @@ std::vector<poly::Variable> VariableOrdering::operator()(
 {
   switch (vos)
   {
-    case VariableOrderingStrategy::BYID: return sort_byid(polys);
-    case VariableOrderingStrategy::BROWN: return sort_brown(polys);
-    case VariableOrderingStrategy::TRIANGULAR: return sort_triangular(polys);
+    case VariableOrderingStrategy::BYID: return sortByid(polys);
+    case VariableOrderingStrategy::BROWN: return sortBrown(polys);
+    case VariableOrderingStrategy::TRIANGULAR: return sortTriangular(polys);
     default: Assert(false) << "Unsupported variable ordering.";
   }
   return {};
diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h
index 3d4bee861..8973003f7 100644
--- a/src/theory/arith/nl/cad/variable_ordering.h
+++ b/src/theory/arith/nl/cad/variable_ordering.h
@@ -9,17 +9,13 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Implements variable orderings tailored to CAD.
  **
  ** Implements variable orderings tailored to CAD.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 #define CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 
@@ -29,7 +25,7 @@
 
 #include <poly/polyxx.h>
 
-#include "constraints.h"
+#include "theory/arith/nl/cad/constraints.h"
 #include "util/poly_util.h"
 
 namespace CVC4 {
@@ -64,7 +60,7 @@ class VariableOrdering
  * If with_totals is set, the last element of the vector contains totals as
  * computed by get_variable_information if no variable is specified.
  */
-std::vector<poly_utils::VariableInformation> collect_information(
+std::vector<poly_utils::VariableInformation> collectInformation(
     const Constraints::ConstraintVector& polys, bool with_totals = false);
 
 }  // namespace cad
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 8292380f9..8345fc5a1 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -9,12 +9,6 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Utilities for converting to and from LibPoly objects.
  **
  ** Utilities for converting to and from LibPoly objects.
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 73509f83c..82ae565d2 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -9,12 +9,6 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Utilities for converting to and from LibPoly objects.
  **
  ** Utilities for converting to and from LibPoly objects.