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, 239 insertions, 0 deletions

diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
new file mode 100644
index 000000000..b3370e75a
--- /dev/null
+++ b/src/expr/expr_iomanip.h
@@ -0,0 +1,239 @@
+/*********************                                                        */
+/*! \file expr_iomanip.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Expr IO manipulation classes.
+ **
+ ** Expr IO manipulation classes.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXPR__EXPR_IOMANIP_H
+#define __CVC4__EXPR__EXPR_IOMANIP_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+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 {
+public:
+
+  /**
+   * Construct a ExprSetDepth with the given depth.
+   */
+  ExprSetDepth(long depth);
+
+  void applyDepth(std::ostream& out);
+
+  static long getDepth(std::ostream& out);
+
+  static void setDepth(std::ostream& out, long 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 {
+  public:
+    Scope(std::ostream& out, long depth);
+    ~Scope();
+
+  private:
+    std::ostream& d_out;
+    long d_oldDepth;
+  };/* class ExprSetDepth::Scope */
+
+ private:
+  /**
+   * 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;
+};/* 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 {
+public:
+  /**
+   * Construct a ExprPrintTypes with the given setting.
+   */
+  ExprPrintTypes(bool printTypes);
+
+  void applyPrintTypes(std::ostream& out);
+
+  static bool getPrintTypes(std::ostream& out);
+
+  static void setPrintTypes(std::ostream& out, bool 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 {
+  public:
+    Scope(std::ostream& out, bool printTypes);
+    ~Scope();
+
+  private:
+    std::ostream& d_out;
+    bool d_oldPrintTypes;
+  };/* class ExprPrintTypes::Scope */
+
+ private:
+  /**
+   * 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;
+};/* class ExprPrintTypes */
+
+/**
+ * IOStream manipulator to print expressions as a dag (or not).
+ */
+class CVC4_PUBLIC ExprDag {
+public:
+  /**
+   * Construct a ExprDag with the given setting (dagification on or off).
+   */
+  explicit ExprDag(bool dag);
+
+  /**
+   * 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);
+
+  void applyDag(std::ostream& out);
+
+  static size_t getDag(std::ostream& out);
+
+  static void setDag(std::ostream& out, size_t dag);
+
+  /**
+   * 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 {
+  public:
+    Scope(std::ostream& out, size_t dag);
+    ~Scope();
+
+  private:
+    std::ostream& d_out;
+    size_t d_oldDag;
+  };/* class ExprDag::Scope */
+
+ private:
+  /**
+   * 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;
+};/* class ExprDag */
+
+/**
+ * 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.
+ */
+std::ostream& operator<<(std::ostream& out, ExprDag d) CVC4_PUBLIC;
+
+
+/**
+ * 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.
+ */
+std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) CVC4_PUBLIC;
+
+/**
+ * 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.
+ */
+std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) CVC4_PUBLIC;
+
+}/* namespace CVC4::expr */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__EXPR_IOMANIP_H */