CBMC
smt_to_smt2_string.cpp File Reference
#include <util/range.h>
#include <util/string_utils.h>
#include <solvers/smt2/smt2_conv.h>
#include <solvers/smt2_incremental/ast/smt_commands.h>
#include <solvers/smt2_incremental/ast/smt_index.h>
#include <solvers/smt2_incremental/ast/smt_logics.h>
#include <solvers/smt2_incremental/ast/smt_sorts.h>
#include <solvers/smt2_incremental/ast/smt_terms.h>
#include <solvers/smt2_incremental/smt_to_smt2_string.h>
#include <functional>
#include <sstream>
#include <stack>
#include <string>
#include "solvers/smt2_incremental/ast/smt_logics.def"
+ Include dependency graph for smt_to_smt2_string.cpp:

Go to the source code of this file.

Classes

class  smt_index_output_visitort
 
class  smt_sort_output_visitort
 
struct  sorted_variablest
 
class  smt_term_to_string_convertert
 
class  smt_option_to_string_convertert
 
class  smt_logic_to_string_convertert
 
class  smt_command_to_string_convertert
 

Macros

#define LOGIC_ID(the_id, the_name)
 

Functions

static std::string escape_identifier (const irep_idt &identifier)
 
std::ostream & operator<< (std::ostream &os, const smt_indext &index)
 
std::string smt_to_smt2_string (const smt_indext &index)
 
std::ostream & operator<< (std::ostream &os, const smt_sortt &sort)
 
std::string smt_to_smt2_string (const smt_sortt &sort)
 
std::ostream & operator<< (std::ostream &os, const smt_termt &term)
 
std::string smt_to_smt2_string (const smt_termt &term)
 
std::ostream & operator<< (std::ostream &os, const smt_optiont &option)
 
std::string smt_to_smt2_string (const smt_optiont &option)
 
std::ostream & operator<< (std::ostream &os, const smt_logict &logic)
 
std::string smt_to_smt2_string (const smt_logict &logic)
 
std::ostream & operator<< (std::ostream &os, const smt_commandt &command)
 
std::string smt_to_smt2_string (const smt_commandt &command)
 

Macro Definition Documentation

◆ LOGIC_ID

#define LOGIC_ID (   the_id,
  the_name 
)
Value:
void visit(const smt_logic_##the_id##t &) override \
{ \
os << #the_name; \
}

Definition at line 364 of file smt_to_smt2_string.cpp.

Function Documentation

◆ escape_identifier()

static std::string escape_identifier ( const irep_idt identifier)
static

Definition at line 19 of file smt_to_smt2_string.cpp.

◆ operator<<() [1/6]

std::ostream& operator<< ( std::ostream &  os,
const smt_commandt command 
)

Definition at line 464 of file smt_to_smt2_string.cpp.

◆ operator<<() [2/6]

std::ostream& operator<< ( std::ostream &  os,
const smt_indext index 
)

Definition at line 45 of file smt_to_smt2_string.cpp.

◆ operator<<() [3/6]

std::ostream& operator<< ( std::ostream &  os,
const smt_logict logic 
)

Definition at line 374 of file smt_to_smt2_string.cpp.

◆ operator<<() [4/6]

std::ostream& operator<< ( std::ostream &  os,
const smt_optiont option 
)

Definition at line 341 of file smt_to_smt2_string.cpp.

◆ operator<<() [5/6]

std::ostream& operator<< ( std::ostream &  os,
const smt_sortt sort 
)

Definition at line 85 of file smt_to_smt2_string.cpp.

◆ operator<<() [6/6]

std::ostream& operator<< ( std::ostream &  os,
const smt_termt term 
)

Definition at line 312 of file smt_to_smt2_string.cpp.

◆ smt_to_smt2_string() [1/6]

std::string smt_to_smt2_string ( const smt_commandt command)

Definition at line 470 of file smt_to_smt2_string.cpp.

◆ smt_to_smt2_string() [2/6]

std::string smt_to_smt2_string ( const smt_indext index)

Definition at line 52 of file smt_to_smt2_string.cpp.

◆ smt_to_smt2_string() [3/6]

std::string smt_to_smt2_string ( const smt_logict logic)

Definition at line 380 of file smt_to_smt2_string.cpp.

◆ smt_to_smt2_string() [4/6]

std::string smt_to_smt2_string ( const smt_optiont option)

Definition at line 347 of file smt_to_smt2_string.cpp.

◆ smt_to_smt2_string() [5/6]

std::string smt_to_smt2_string ( const smt_sortt sort)

Definition at line 91 of file smt_to_smt2_string.cpp.

◆ smt_to_smt2_string() [6/6]

std::string smt_to_smt2_string ( const smt_termt term)

Definition at line 317 of file smt_to_smt2_string.cpp.