Shuffling around public vs. private headers

- Adding a script contrib/test_install_headers.h that tests whether one can include all cvc4_public headers. CVC4 can pass this test after this commit.
- Making lib/{clock_gettime.h,ffs.h,strtok_r.h} cvc4_private.
- Making prop/sat_solver_factory.h cvc4_private.
- Moving the expr iostream manipulators into their own files: expr_iomanip.{h,cpp}.
- Setting the generated *_options.h files back to being cvc4_private.
-- Removing the usage of options/expr_options.h from expr.h.
-- Removing the include of base_options.h from options.h.
- Cleaning up CPP macros in cvc4_public headers.
-- Changing the ROLL macro in floatingpoint.h into an inline function.
-- Removing the now unused flag -D__BUILDING_STATISTICS_FOR_EXPORT.

1 files changed, 0 insertions, 338 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 2e2f17742..7d82cb222 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -33,7 +33,6 @@ ${includes}
 #include <string>
 
 #include "base/exception.h"
-#include "options/expr_options.h"
 #include "options/language.h"
 #include "util/hash.h"
 
@@ -77,10 +76,6 @@ namespace smt {
 }/* CVC4::smt namespace */
 
 namespace expr {
-  class CVC4_PUBLIC ExprSetDepth;
-  class CVC4_PUBLIC ExprPrintTypes;
-  class CVC4_PUBLIC ExprDag;
-
   class ExportPrivate;
 }/* CVC4::expr namespace */
 
@@ -513,42 +508,6 @@ public:
   Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;
 
   /**
-   * IOStream manipulator to set the maximum depth of Exprs when
-   * pretty-printing.  -1 means print to any depth.  E.g.:
-   *
-   *   // let a, b, c, and d be VARIABLEs
-   *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
-   *   out << setdepth(3) << e;
-   *
-   * gives "(OR a b (AND c (NOT d)))", but
-   *
-   *   out << setdepth(1) << [same expr as above]
-   *
-   * gives "(OR a b (...))"
-   */
-  typedef expr::ExprSetDepth setdepth;
-
-  /**
-   * IOStream manipulator to print type ascriptions or not.
-   *
-   *   // let a, b, c, and d be variables of sort U
-   *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
-   *   out << printtypes(true) << e;
-   *
-   * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
-   *
-   *   out << printtypes(false) << [same expr as above]
-   *
-   * gives "(OR a b (AND c (NOT d)))"
-   */
-  typedef expr::ExprPrintTypes printtypes;
-
-  /**
-   * IOStream manipulator to print expressions as a DAG (or not).
-   */
-  typedef expr::ExprDag dag;
-
-  /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
    * @param out output stream to print to.
@@ -592,307 +551,10 @@ private:
 
 };/* class Expr */
 
-namespace expr {
-
-/**
- * IOStream manipulator to set the maximum depth of Exprs when
- * pretty-printing.  -1 means print to any depth.  E.g.:
- *
- *   // let a, b, c, and d be VARIABLEs
- *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
- *   out << setdepth(3) << e;
- *
- * gives "(OR a b (AND c (NOT d)))", but
- *
- *   out << setdepth(1) << [same expr as above]
- *
- * gives "(OR a b (...))".
- *
- * The implementation of this class serves two purposes; it holds
- * information about the depth setting (such as the index of the
- * allocated word in ios_base), and serves also as the manipulator
- * itself (as above).
- */
-class CVC4_PUBLIC ExprSetDepth {
-  /**
-   * The allocated index in ios_base for our depth setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * The default depth to print, for ostreams that haven't yet had a
-   * setdepth() applied to them.
-   */
-  static const int s_defaultPrintDepth = -1;
-
-  /**
-   * When this manipulator is used, the depth is stored here.
-   */
-  long d_depth;
-
-public:
-  /**
-   * Construct a ExprSetDepth with the given depth.
-   */
-  ExprSetDepth(long depth) : d_depth(depth) {}
-
-  inline void applyDepth(std::ostream& out) {
-    out.iword(s_iosIndex) = d_depth;
-  }
-
-  static inline long getDepth(std::ostream& out) {
-    long& l = out.iword(s_iosIndex);
-    if(l == 0) {
-      // set the default print depth on this ostream
-      if(not Options::isCurrentNull()) {
-        l = options::defaultExprDepth();
-      }
-      if(l == 0) {
-        // if called from outside the library, we may not have options
-        // available to us at this point (or perhaps the output language
-        // is not set in Options).  Default to something reasonable, but
-        // don't set "l" since that would make it "sticky" for this
-        // stream.
-        return s_defaultPrintDepth;
-      }
-    }
-    return l;
-  }
-
-  static inline void setDepth(std::ostream& out, long depth) {
-    out.iword(s_iosIndex) = depth;
-  }
-
-  /**
-   * Set the expression depth on the output stream for the current
-   * stack scope.  This makes sure the old depth is reset on the stream
-   * after normal OR exceptional exit from the scope, using the RAII
-   * C++ idiom.
-   */
-  class Scope {
-    std::ostream& d_out;
-    long d_oldDepth;
-
-  public:
-
-    inline Scope(std::ostream& out, long depth) :
-      d_out(out),
-      d_oldDepth(ExprSetDepth::getDepth(out)) {
-      ExprSetDepth::setDepth(out, depth);
-    }
-
-    inline ~Scope() {
-      ExprSetDepth::setDepth(d_out, d_oldDepth);
-    }
-
-  };/* class ExprSetDepth::Scope */
-
-};/* class ExprSetDepth */
-
-/**
- * IOStream manipulator to print type ascriptions or not.
- *
- *   // let a, b, c, and d be variables of sort U
- *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
- *   out << e;
- *
- * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
- */
-class CVC4_PUBLIC ExprPrintTypes {
-  /**
-   * The allocated index in ios_base for our setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * When this manipulator is used, the setting is stored here.
-   */
-  bool d_printTypes;
-
-public:
-  /**
-   * Construct a ExprPrintTypes with the given setting.
-   */
-  ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
-
-  inline void applyPrintTypes(std::ostream& out) {
-    out.iword(s_iosIndex) = d_printTypes;
-  }
-
-  static inline bool getPrintTypes(std::ostream& out) {
-    return out.iword(s_iosIndex);
-  }
-
-  static inline void setPrintTypes(std::ostream& out, bool printTypes) {
-    out.iword(s_iosIndex) = printTypes;
-  }
-
-  /**
-   * Set the print-types state on the output stream for the current
-   * stack scope.  This makes sure the old state is reset on the
-   * stream after normal OR exceptional exit from the scope, using the
-   * RAII C++ idiom.
-   */
-  class Scope {
-    std::ostream& d_out;
-    bool d_oldPrintTypes;
-
-  public:
-
-    inline Scope(std::ostream& out, bool printTypes) :
-      d_out(out),
-      d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
-      ExprPrintTypes::setPrintTypes(out, printTypes);
-    }
-
-    inline ~Scope() {
-      ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
-    }
-
-  };/* class ExprPrintTypes::Scope */
-
-};/* class ExprPrintTypes */
-
-/**
- * IOStream manipulator to print expressions as a dag (or not).
- */
-class CVC4_PUBLIC ExprDag {
-  /**
-   * The allocated index in ios_base for our setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * The default setting, for ostreams that haven't yet had a
-   * dag() applied to them.
-   */
-  static const size_t s_defaultDag = 1;
-
-  /**
-   * When this manipulator is used, the setting is stored here.
-   */
-  size_t d_dag;
-
-public:
-  /**
-   * Construct a ExprDag with the given setting (dagification on or off).
-   */
-  explicit ExprDag(bool dag) : d_dag(dag ? 1 : 0) {}
-
-  /**
-   * Construct a ExprDag with the given setting (letify only common
-   * subexpressions that appear more than 'dag' times).  dag <= 0 means
-   * don't dagify.
-   */
-  explicit ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {}
-
-  inline void applyDag(std::ostream& out) {
-    // (offset by one to detect whether default has been set yet)
-    out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1;
-  }
-
-  static inline size_t getDag(std::ostream& out) {
-    long& l = out.iword(s_iosIndex);
-    if(l == 0) {
-      // set the default dag setting on this ostream
-      // (offset by one to detect whether default has been set yet)
-      if(not Options::isCurrentNull()) {
-        l = options::defaultDagThresh() + 1;
-      }
-      if(l == 0) {
-        // if called from outside the library, we may not have options
-        // available to us at this point (or perhaps the output language
-        // is not set in Options).  Default to something reasonable, but
-        // don't set "l" since that would make it "sticky" for this
-        // stream.
-        return s_defaultDag + 1;
-      }
-    }
-    return static_cast<size_t>(l - 1);
-  }
-
-  static inline void setDag(std::ostream& out, size_t dag) {
-    // (offset by one to detect whether default has been set yet)
-    out.iword(s_iosIndex) = static_cast<long>(dag) + 1;
-  }
-
-  /**
-   * Set the dag state on the output stream for the current
-   * stack scope.  This makes sure the old state is reset on the
-   * stream after normal OR exceptional exit from the scope, using the
-   * RAII C++ idiom.
-   */
-  class Scope {
-    std::ostream& d_out;
-    size_t d_oldDag;
-
-  public:
-
-    inline Scope(std::ostream& out, size_t dag) :
-      d_out(out),
-      d_oldDag(ExprDag::getDag(out)) {
-      ExprDag::setDag(out, dag);
-    }
-
-    inline ~Scope() {
-      ExprDag::setDag(d_out, d_oldDag);
-    }
-
-  };/* class ExprDag::Scope */
-
-};/* class ExprDag */
-}/* CVC4::expr namespace */
-
 ${getConst_instantiations}
 
 #line 939 "${template}"
 
-namespace expr {
-
-/**
- * Sets the default depth when pretty-printing a Expr to an ostream.
- * Use like this:
- *
- *   // let out be an ostream, e an Expr
- *   out << Expr::setdepth(n) << e << endl;
- *
- * The depth stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
-  sd.applyDepth(out);
-  return out;
-}
-
-/**
- * Sets the default print-types setting when pretty-printing an Expr
- * to an ostream.  Use like this:
- *
- *   // let out be an ostream, e an Expr
- *   out << Expr::printtypes(true) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
-  pt.applyPrintTypes(out);
-  return out;
-}
-
-/**
- * Sets the default dag setting when pretty-printing a Expr to an ostream.
- * Use like this:
- *
- *   // let out be an ostream, e an Expr
- *   out << Expr::dag(true) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
-  d.applyDag(out);
-  return out;
-}
-
-}/* CVC4::expr namespace */
-
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
   return (size_t) e.getId();
 }