diff options
author | Tim King <taking@google.com> | 2015-12-30 11:45:37 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-30 11:45:37 -0800 |
commit | fa7f30a4ba08afe066604daee87006b4fb5f21f7 (patch) | |
tree | 6eecac7cce64fa00f4ac5c18f023f1bc234435a3 /src/expr | |
parent | 1ce397129214a427a10ff3e33069e315fe13eec1 (diff) |
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.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 2 | ||||
-rw-r--r-- | src/expr/expr_iomanip.cpp | 160 | ||||
-rw-r--r-- | src/expr/expr_iomanip.h | 239 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 8 | ||||
-rw-r--r-- | src/expr/expr_template.h | 338 | ||||
-rw-r--r-- | src/expr/node.h | 1 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 1 | ||||
-rw-r--r-- | src/expr/statistics_registry.cpp | 8 | ||||
-rw-r--r-- | src/expr/statistics_registry.h | 13 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 12 | ||||
-rw-r--r-- | src/expr/type_node.h | 7 |
11 files changed, 422 insertions, 367 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index dc6ad5833..63f31ed67 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -32,6 +32,8 @@ libexpr_la_SOURCES = \ chain.h \ emptyset.cpp \ emptyset.h \ + expr_iomanip.cpp \ + expr_iomanip.h \ expr_manager_scope.h \ expr_stream.h \ kind_map.h \ diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp new file mode 100644 index 000000000..4c7ab3c8b --- /dev/null +++ b/src/expr/expr_iomanip.cpp @@ -0,0 +1,160 @@ +/********************* */ +/*! \file expr_iomanip.cpp + ** \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 "expr/expr_iomanip.h" + +#include <iomanip> +#include <iostream> + +#include "options/options.h" +#include "options/expr_options.h" + +namespace CVC4 { +namespace expr { + +const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); +const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); +const int ExprDag::s_iosIndex = std::ios_base::xalloc(); + + + +ExprSetDepth::ExprSetDepth(long depth) : d_depth(depth) {} + +void ExprSetDepth::applyDepth(std::ostream& out) { + out.iword(s_iosIndex) = d_depth; +} + +long ExprSetDepth::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; +} + +void ExprSetDepth::setDepth(std::ostream& out, long depth) { + out.iword(s_iosIndex) = depth; +} + + +ExprSetDepth::Scope::Scope(std::ostream& out, long depth) + : d_out(out), d_oldDepth(ExprSetDepth::getDepth(out)) +{ + ExprSetDepth::setDepth(out, depth); +} + +ExprSetDepth::Scope::~Scope() { + ExprSetDepth::setDepth(d_out, d_oldDepth); +} + + +ExprPrintTypes::ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {} + +void ExprPrintTypes::applyPrintTypes(std::ostream& out) { + out.iword(s_iosIndex) = d_printTypes; +} + +bool ExprPrintTypes::getPrintTypes(std::ostream& out) { + return out.iword(s_iosIndex); +} + +void ExprPrintTypes::setPrintTypes(std::ostream& out, bool printTypes) { + out.iword(s_iosIndex) = printTypes; +} + +ExprPrintTypes::Scope::Scope(std::ostream& out, bool printTypes) + : d_out(out), + d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) { + ExprPrintTypes::setPrintTypes(out, printTypes); +} + +ExprPrintTypes::Scope::~Scope() { + ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes); +} + +ExprDag::ExprDag(bool dag) : d_dag(dag ? 1 : 0) {} + +ExprDag::ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {} + +void ExprDag::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; +} + +size_t ExprDag::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); +} + +void ExprDag::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; +} + +ExprDag::Scope::Scope(std::ostream& out, size_t dag) + : d_out(out), + d_oldDag(ExprDag::getDag(out)) { + ExprDag::setDag(out, dag); +} + +ExprDag::Scope::~Scope() { + ExprDag::setDag(d_out, d_oldDag); +} + +std::ostream& operator<<(std::ostream& out, ExprDag d) { + d.applyDag(out); + return out; +} + +std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { + pt.applyPrintTypes(out); + return out; +} + +std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { + sd.applyDepth(out); + return out; +} + + +}/* namespace CVC4::expr */ +}/* namespace CVC4 */ 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 */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index dfbe179be..a6cdedd00 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -40,14 +40,6 @@ namespace CVC4 { class ExprManager; -namespace expr { - -const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); -const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); -const int ExprDag::s_iosIndex = std::ios_base::xalloc(); - -}/* CVC4::expr namespace */ - std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) { return out << e.getMessage() << ": " << e.getExpression(); } 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(); } diff --git a/src/expr/node.h b/src/expr/node.h index f345ba552..c0e2a5542 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -37,6 +37,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/expr.h" +#include "expr/expr_iomanip.h" #include "options/language.h" #include "options/set_language.h" #include "util/configuration.h" diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index dbe7d09eb..ab18973cb 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -24,6 +24,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node.h" +#include "options/base_options.h" #include "options/language.h" #include "options/options.h" #include "printer/printer.h" diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp index bf36236f7..3f9124a2f 100644 --- a/src/expr/statistics_registry.cpp +++ b/src/expr/statistics_registry.cpp @@ -21,10 +21,8 @@ #include "expr/expr_manager.h" #include "lib/clock_gettime.h" #include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" -#ifndef __BUILDING_STATISTICS_FOR_EXPORT -# include "smt/smt_engine_scope.h" -#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ #ifdef CVC4_STATISTICS_ON # define __CVC4_USE_STATISTICS true @@ -65,8 +63,6 @@ inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) { }/* CVC4::stats namespace */ -#ifndef __BUILDING_STATISTICS_FOR_EXPORT - StatisticsRegistry* StatisticsRegistry::current() { return stats::getStatisticsRegistry(smt::currentSmtEngine()); } @@ -91,8 +87,6 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentExce #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ - void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s); diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h index 4793f1301..3feb0d5d7 100644 --- a/src/expr/statistics_registry.h +++ b/src/expr/statistics_registry.h @@ -32,7 +32,6 @@ #include "base/exception.h" #include "expr/statistics.h" -#include "lib/clock_gettime.h" namespace CVC4 { @@ -617,10 +616,10 @@ public: d_prefix = d_name = name; } -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) /** Get a pointer to the current statistics registry */ static StatisticsRegistry* current(); -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ /** Overridden to avoid the name being printed */ void flushStat(std::ostream &out) const; @@ -638,13 +637,13 @@ public: return SExpr(v); } -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) /** Register a new statistic, making it active. */ static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); /** Unregister an active statistic, making it inactive. */ static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */ +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) */ /** Register a new statistic */ void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException); @@ -887,7 +886,7 @@ class RegisterStatistic { public: -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && ! defined(__BUILDING_STATISTICS_FOR_EXPORT) +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) RegisterStatistic(Stat* stat) : d_reg(StatisticsRegistry::current()), d_stat(stat) { @@ -896,7 +895,7 @@ public: } StatisticsRegistry::registerStat(d_stat); } -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : d_reg(reg), diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 659e80550..ea185f98b 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -13,12 +13,14 @@ ** ** Reference-counted encapsulation of a pointer to node information. **/ +#include "expr/type_node.h" #include <vector> #include "expr/node_manager_attributes.h" -#include "expr/type_node.h" #include "expr/type_properties.h" +#include "options/base_options.h" +#include "options/expr_options.h" using namespace std; @@ -564,4 +566,12 @@ bool TypeNode::isSortConstructor() const { return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); } +std::string TypeNode::toString() const { + std::stringstream ss; + OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + d_nv->toStream(ss, -1, false, 0, outlang); + return ss.str(); +} + + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index ce006a4f1..59f602f09 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -372,12 +372,7 @@ public: * * @return the string representation of this type. */ - inline std::string toString() const { - std::stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); - d_nv->toStream(ss, -1, false, 0, outlang); - return ss.str(); - } + std::string toString() const; /** * Converts this node into a string representation and sends it to the |