cprover
|
Static Public Member Functions | |
static std::ostream & | convert (std::ostream &os, const smt_termt &term) |
This function is complete the external interface to this class. More... | |
Private Types | |
using | output_functiont = std::function< void(std::ostream &)> |
Private Member Functions | |
output_functiont | make_output_function (const smt_termt &output) |
output_functiont | make_output_function (const std::vector< std::reference_wrapper< const smt_termt >> &output) |
template<typename outputt > | |
void | push_output (outputt &&output) |
Single argument version of push_outputs . More... | |
void | push_outputs () |
Base case for the recursive push_outputs function template below. More... | |
template<typename outputt , typename... outputst> | |
void | push_outputs (outputt &&output, outputst &&... outputs) |
Pushes outputting functions to the output_stack for each of the output values provided. More... | |
smt_term_to_string_convertert ()=default | |
void | visit (const smt_bool_literal_termt &bool_literal) override |
void | visit (const smt_identifier_termt &identifier_term) override |
void | visit (const smt_bit_vector_constant_termt &bit_vector_constant) override |
void | visit (const smt_function_application_termt &function_application) override |
Static Private Member Functions | |
static output_functiont | make_output_function (const std::string &output) |
static output_functiont | make_output_function (const smt_sortt &output) |
Private Attributes | |
std::stack< output_functiont > | output_stack |
smt_term_to_string_convertert
class is implemented using an explicit std::stack
rather than using recursion and the call stack. This is done in order to ensure we can print smt terms which are nested arbitrarily deeply without risk of exceeding the maximum depth of the call stack. The set of visit
functions push functions to output_stack
, which capture the value to be printed. When called these functions may either print to the output stream or push further functions to the stack in the case of nodes in the tree which have child nodes which also need to be printed. The push_output(s)
functions exist as convenience functions to allow pushing the capturing functions to the stack in the reverse order required for printing, whilst keeping the visit functions easier to read by keeping the outputs in reading order and separating the capturing code. Definition at line 69 of file smt_to_smt2_string.cpp.
|
private |
Definition at line 72 of file smt_to_smt2_string.cpp.
|
privatedefault |
|
static |
This function is complete the external interface to this class.
All construction of this class and printing of terms should be carried out via this function.
Definition at line 197 of file smt_to_smt2_string.cpp.
|
staticprivate |
Definition at line 125 of file smt_to_smt2_string.cpp.
|
private |
Definition at line 131 of file smt_to_smt2_string.cpp.
|
staticprivate |
Definition at line 118 of file smt_to_smt2_string.cpp.
|
private |
Definition at line 137 of file smt_to_smt2_string.cpp.
|
private |
Single argument version of push_outputs
.
Definition at line 149 of file smt_to_smt2_string.cpp.
|
private |
Base case for the recursive push_outputs
function template below.
Definition at line 154 of file smt_to_smt2_string.cpp.
|
private |
Pushes outputting functions to the output_stack for each of the output values provided.
This variadic template supports any (compile time fixed) number of output arguments. The arguments are pushed in order from right to left, so that they are subsequently in left to right order when popped off the stack. The types of argument supported are those supported by the overloads of the make_output_function
function.
Definition at line 159 of file smt_to_smt2_string.cpp.
|
overrideprivate |
Definition at line 180 of file smt_to_smt2_string.cpp.
|
overrideprivate |
Definition at line 167 of file smt_to_smt2_string.cpp.
|
overrideprivate |
Definition at line 188 of file smt_to_smt2_string.cpp.
|
overrideprivate |
Definition at line 173 of file smt_to_smt2_string.cpp.
|
private |
Definition at line 73 of file smt_to_smt2_string.cpp.