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 118 of file smt_to_smt2_string.cpp.
Member Typedef Documentation
◆ output_functiont
|
private |
Definition at line 121 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 299 of file smt_to_smt2_string.cpp.
◆ make_output_function() [1/6]
|
staticprivate |
Definition at line 179 of file smt_to_smt2_string.cpp.
◆ make_output_function() [2/6]
|
staticprivate |
Definition at line 185 of file smt_to_smt2_string.cpp.
◆ make_output_function() [3/6]
|
private |
Definition at line 191 of file smt_to_smt2_string.cpp.
◆ make_output_function() [4/6]
|
private |
Definition at line 210 of file smt_to_smt2_string.cpp.
◆ make_output_function() [5/6]
|
staticprivate |
Definition at line 172 of file smt_to_smt2_string.cpp.
◆ make_output_function() [6/6]
|
private |
Definition at line 198 of file smt_to_smt2_string.cpp.
◆ push_output()
|
private |
Single argument version of push_outputs.
Definition at line 229 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 234 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 239 of file smt_to_smt2_string.cpp.
◆ visit() [1/6]
|
overrideprivate |
Definition at line 268 of file smt_to_smt2_string.cpp.
◆ visit() [2/6]
|
overrideprivate |
Definition at line 247 of file smt_to_smt2_string.cpp.
◆ visit() [3/6]
|
overrideprivate |
Definition at line 291 of file smt_to_smt2_string.cpp.
◆ visit() [4/6]
|
overrideprivate |
Definition at line 284 of file smt_to_smt2_string.cpp.
◆ visit() [5/6]
|
overrideprivate |
Definition at line 276 of file smt_to_smt2_string.cpp.
◆ visit() [6/6]
|
overrideprivate |
Definition at line 253 of file smt_to_smt2_string.cpp.
Member Data Documentation
◆ output_stack
|
private |
Definition at line 122 of file smt_to_smt2_string.cpp.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt_to_smt2_string.cpp
