diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-05 22:28:18 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-05 22:28:18 -0600 |
commit | af18cd275f340d1896c3b635dbeecbea2e521db1 (patch) | |
tree | 438137ddb999a853b543baa70e8009da212c1e05 /src/expr/expr_iomanip.h | |
parent | ac8b2593bed81125cb1a494e4b8311e517d0e3d9 (diff) |
Simplify printing with respect to expression types (#5394)
This removes infrastructure for stream property related to printing type annotations on all variables.
This is towards refactoring the printers.
Diffstat (limited to 'src/expr/expr_iomanip.h')
-rw-r--r-- | src/expr/expr_iomanip.h | 62 |
1 files changed, 0 insertions, 62 deletions
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 82358bb68..e90366a81 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -92,56 +92,6 @@ public: };/* 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 { @@ -209,18 +159,6 @@ public: */ 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: |