9#ifndef CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
10#define CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
132 const std::vector<exprt> &operands,
133 const char operation);
Boolean AND All operands must be boolean, and the result is always boolean.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
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.
typet & type()
Return the type of the expression.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Boolean OR All operands must be boolean, and the result is always boolean.
Expression to hold a symbol (variable)
The type of an expression, extends irept.
Boolean XOR All operands must be boolean, and the result is always boolean.
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.