Inheritance diagram for smt_term_to_string_convertert: Collaboration diagram for smt_term_to_string_convertert: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) |
| template<typename elementt > | |
| output_functiont | make_output_function (const std::vector< std::reference_wrapper< const elementt >> &output) |
| output_functiont | make_output_function (const sorted_variablest &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 |
| void | visit (const smt_forall_termt &forall) override |
| void | visit (const smt_exists_termt &exists) override |
Static Private Member Functions | |
| static output_functiont | make_output_function (const std::string &output) |
| static output_functiont | make_output_function (const smt_indext &output) |
| static output_functiont | make_output_function (const smt_sortt &output) |
Private Attributes | |
| std::stack< output_functiont > | output_stack |
Detailed Description
- Note
- The printing algorithm in the
smt_term_to_string_convertertclass is implemented using an explicitstd::stackrather 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 119 of file smt_to_smt2_string.cpp.
Member Typedef Documentation
◆ output_functiont
|
private |
Definition at line 122 of file smt_to_smt2_string.cpp.
Constructor & Destructor Documentation
◆ smt_term_to_string_convertert()
|
privatedefault |
Member Function Documentation
◆ convert()
|
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 300 of file smt_to_smt2_string.cpp.
◆ make_output_function() [1/6]
|
staticprivate |
Definition at line 180 of file smt_to_smt2_string.cpp.
◆ make_output_function() [2/6]
|
staticprivate |
Definition at line 186 of file smt_to_smt2_string.cpp.
◆ make_output_function() [3/6]
|
private |
Definition at line 192 of file smt_to_smt2_string.cpp.
◆ make_output_function() [4/6]
|
private |
Definition at line 211 of file smt_to_smt2_string.cpp.
◆ make_output_function() [5/6]
|
staticprivate |
Definition at line 173 of file smt_to_smt2_string.cpp.
◆ make_output_function() [6/6]
|
private |
Definition at line 199 of file smt_to_smt2_string.cpp.
◆ push_output()
|
private |
Single argument version of push_outputs.
Definition at line 230 of file smt_to_smt2_string.cpp.
◆ push_outputs() [1/2]
|
private |
Base case for the recursive push_outputs function template below.
Definition at line 235 of file smt_to_smt2_string.cpp.
◆ push_outputs() [2/2]
|
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.
- Note
- This is implemented recursively, but does not risk exceeding the maximum depth of the call stack. This is because the number of times it recurses depends only on the number of arguments supplied in the source code at compile time.
Definition at line 240 of file smt_to_smt2_string.cpp.
◆ visit() [1/6]
|
overrideprivate |
Definition at line 269 of file smt_to_smt2_string.cpp.
◆ visit() [2/6]
|
overrideprivate |
Definition at line 248 of file smt_to_smt2_string.cpp.
◆ visit() [3/6]
|
overrideprivate |
Definition at line 292 of file smt_to_smt2_string.cpp.
◆ visit() [4/6]
|
overrideprivate |
Definition at line 285 of file smt_to_smt2_string.cpp.
◆ visit() [5/6]
|
overrideprivate |
Definition at line 277 of file smt_to_smt2_string.cpp.
◆ visit() [6/6]
|
overrideprivate |
Definition at line 254 of file smt_to_smt2_string.cpp.
Member Data Documentation
◆ output_stack
|
private |
Definition at line 123 of file smt_to_smt2_string.cpp.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2_incremental/smt_to_smt2_string.cpp
