cprover
smt_term_to_string_convertert Class Reference
+ 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)
 
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_functiontoutput_stack
 

Detailed Description

Note
The printing algorithm in the 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.

Member Typedef Documentation

◆ output_functiont

using smt_term_to_string_convertert::output_functiont = std::function<void(std::ostream &)>
private

Definition at line 72 of file smt_to_smt2_string.cpp.

Constructor & Destructor Documentation

◆ smt_term_to_string_convertert()

smt_term_to_string_convertert::smt_term_to_string_convertert ( )
privatedefault

Member Function Documentation

◆ convert()

std::ostream & smt_term_to_string_convertert::convert ( std::ostream &  os,
const smt_termt term 
)
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.

◆ make_output_function() [1/4]

smt_term_to_string_convertert::output_functiont smt_term_to_string_convertert::make_output_function ( const smt_sortt output)
staticprivate

Definition at line 125 of file smt_to_smt2_string.cpp.

◆ make_output_function() [2/4]

smt_term_to_string_convertert::output_functiont smt_term_to_string_convertert::make_output_function ( const smt_termt output)
private

Definition at line 131 of file smt_to_smt2_string.cpp.

◆ make_output_function() [3/4]

smt_term_to_string_convertert::output_functiont smt_term_to_string_convertert::make_output_function ( const std::string &  output)
staticprivate

Definition at line 118 of file smt_to_smt2_string.cpp.

◆ make_output_function() [4/4]

smt_term_to_string_convertert::output_functiont smt_term_to_string_convertert::make_output_function ( const std::vector< std::reference_wrapper< const smt_termt >> &  output)
private

Definition at line 137 of file smt_to_smt2_string.cpp.

◆ push_output()

template<typename outputt >
void smt_term_to_string_convertert::push_output ( outputt &&  output)
private

Single argument version of push_outputs.

Definition at line 149 of file smt_to_smt2_string.cpp.

◆ push_outputs() [1/2]

void smt_term_to_string_convertert::push_outputs ( )
private

Base case for the recursive push_outputs function template below.

Definition at line 154 of file smt_to_smt2_string.cpp.

◆ push_outputs() [2/2]

template<typename outputt , typename... outputst>
void smt_term_to_string_convertert::push_outputs ( outputt &&  output,
outputst &&...  outputs 
)
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 159 of file smt_to_smt2_string.cpp.

◆ visit() [1/4]

void smt_term_to_string_convertert::visit ( const smt_bit_vector_constant_termt bit_vector_constant)
overrideprivate

Definition at line 180 of file smt_to_smt2_string.cpp.

◆ visit() [2/4]

void smt_term_to_string_convertert::visit ( const smt_bool_literal_termt bool_literal)
overrideprivate

Definition at line 167 of file smt_to_smt2_string.cpp.

◆ visit() [3/4]

void smt_term_to_string_convertert::visit ( const smt_function_application_termt function_application)
overrideprivate

Definition at line 188 of file smt_to_smt2_string.cpp.

◆ visit() [4/4]

void smt_term_to_string_convertert::visit ( const smt_identifier_termt identifier_term)
overrideprivate

Definition at line 173 of file smt_to_smt2_string.cpp.

Member Data Documentation

◆ output_stack

std::stack<output_functiont> smt_term_to_string_convertert::output_stack
private

Definition at line 73 of file smt_to_smt2_string.cpp.


The documentation for this class was generated from the following file: