cprover
|
Expression Pretty Printing. More...
#include "format_expr.h"
#include "arith_tools.h"
#include "expr.h"
#include "expr_iterator.h"
#include "fixedbv.h"
#include "format_type.h"
#include "ieee_float.h"
#include "invariant.h"
#include "mp_arith.h"
#include "rational.h"
#include "rational_tools.h"
#include "std_code.h"
#include "std_expr.h"
#include "string2int.h"
#include "string_utils.h"
#include <ostream>
#include <stack>
Go to the source code of this file.
Functions | |
static bool | bracket_subexpression (const exprt &sub_expr, const exprt &expr) |
We use the precendences that most readers expect (i.e., the ones you learn in primary school), and stay clear of the surprising ones that C has. More... | |
static std::ostream & | format_rec (std::ostream &os, const multi_ary_exprt &src) |
This formats a multi-ary expression, adding parentheses where indicated by bracket_subexpression. More... | |
static std::ostream & | format_rec (std::ostream &os, const binary_exprt &src) |
This formats a binary expression, which we do as for multi-ary expressions. More... | |
static std::ostream & | format_rec (std::ostream &os, const unary_exprt &src) |
This formats a unary expression, adding parentheses very aggressively. More... | |
static std::ostream & | format_rec (std::ostream &os, const constant_exprt &src) |
This formats a constant. More... | |
std::ostream & | fallback_format_rec (std::ostream &os, const exprt &expr) |
std::ostream & | format_rec (std::ostream &os, const exprt &expr) |
Formats an expression in a generic syntax that is inspired by C/C++/Java, and is meant for debugging. More... | |
Expression Pretty Printing.
Definition in file format_expr.cpp.
We use the precendences that most readers expect (i.e., the ones you learn in primary school), and stay clear of the surprising ones that C has.
Definition at line 35 of file format_expr.cpp.
References exprt::has_operands(), and irept::id().
Referenced by format_rec().
std::ostream& fallback_format_rec | ( | std::ostream & | os, |
const exprt & | expr | ||
) |
Definition at line 138 of file format_expr.cpp.
References format(), irept::get_named_sub(), exprt::has_operands(), irept::id(), and exprt::operands().
Referenced by format_rec().
|
static |
This formats a multi-ary expression, adding parentheses where indicated by bracket_subexpression.
Definition at line 61 of file format_expr.cpp.
References bracket_subexpression(), format(), irept::id(), and exprt::operands().
Referenced by format_rec(), and operator<<().
|
static |
This formats a binary expression, which we do as for multi-ary expressions.
Definition at line 88 of file format_expr.cpp.
References format_rec(), and to_multi_ary_expr().
|
static |
This formats a unary expression, adding parentheses very aggressively.
Definition at line 95 of file format_expr.cpp.
References format(), exprt::has_operands(), irept::id(), exprt::op0(), and irept::pretty().
|
static |
This formats a constant.
Definition at line 111 of file format_expr.cpp.
References escape(), constant_exprt::get_value(), irept::id(), id2string(), exprt::is_false(), exprt::is_true(), exprt::is_zero(), irept::pretty(), and exprt::type().
std::ostream& format_rec | ( | std::ostream & | os, |
const exprt & | expr | ||
) |
Formats an expression in a generic syntax that is inspired by C/C++/Java, and is meant for debugging.
Definition at line 170 of file format_expr.cpp.
References fallback_format_rec(), format(), format_rec(), member_exprt::get_component_name(), symbol_exprt::get_identifier(), irept::id(), exprt::operands(), to_binary_expr(), to_code(), to_code_assign(), to_code_block(), to_constant_expr(), to_if_expr(), to_index_expr(), to_let_expr(), to_member_expr(), to_multi_ary_expr(), to_quantifier_expr(), to_symbol_expr(), to_typecast_expr(), to_unary_expr(), and exprt::type().