cprover
expr2statement_list.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Conversion from Expression or Type to Statement List Language
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
10 #define CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
11 
12 #include <util/irep.h>
13 #include <util/namespace.h>
14 #include <util/std_expr.h>
15 
16 #include <string>
17 
22 std::string expr2stl(const exprt &expr, const namespacet &ns);
23 
28 std::string type2stl(const typet &type, const namespacet &ns);
29 
31 class expr2stlt
32 {
36 
40 
42  const namespacet &ns;
43 
45  std::stringstream result;
46 
47 public:
50  explicit expr2stlt(const namespacet &ns);
51 
57  std::string convert(const exprt &expr);
58 
59 private:
65  void convert(const and_exprt &expr);
66 
72  void convert(const or_exprt &expr);
73 
79  void convert(const xor_exprt &expr);
80 
87  void convert(const notequal_exprt &expr);
88 
94  void convert(const equal_exprt &expr);
95 
102  void convert(const not_exprt &expr);
103 
108  void convert(const symbol_exprt &expr);
109 
115  void
116  convert_multiary_bool(std::vector<exprt> &operands, const char operation);
117 
123  const std::vector<exprt> &operands,
124  const char operation);
125 
128  void convert_bool_operand(const exprt &op);
129 
136  void convert_first_non_trivial_operand(std::vector<exprt> &operands);
137 
142  irep_idt id_shorthand(const irep_idt &identifier);
143 };
144 
145 #endif // CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
Boolean AND.
Definition: std_expr.h:1835
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1140
Class for saving the internal state of the conversion process.
void convert_multiary_bool(std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
void convert_bool_operand(const exprt &op)
Converts a single boolean operand and introduces an additional nesting layer if needed.
std::string convert(const exprt &expr)
Invokes the conversion process for the given expression and calls itself recursively in the process.
void convert_multiary_bool_operands(const std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
void convert_first_non_trivial_operand(std::vector< exprt > &operands)
Iterates through all the given operands in search for the first non-trivial operand (that encloses al...
bool is_reference
Flag to specify if the next symbol to convert is a reference to a variable.
expr2stlt(const namespacet &ns)
Creates a new instance of the converter.
const namespacet & ns
Contains the symbol table of the current program to convert.
irep_idt id_shorthand(const irep_idt &identifier)
Returns the given identifier in a form that is compatible with STL by looking up the symbol or cuttin...
std::stringstream result
Used for saving intermediate results of the conversion process.
bool inside_bit_string
Internal representation of the FC bit in STL.
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Boolean negation.
Definition: std_expr.h:2042
Disequality.
Definition: std_expr.h:1198
Boolean OR.
Definition: std_expr.h:1943
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The type of an expression, extends irept.
Definition: type.h:28
Boolean XOR.
Definition: std_expr.h:2006
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.
API to expression classes.