cprover
smt2_parsert Class Reference

#include <smt2_parser.h>

+ Inheritance diagram for smt2_parsert:
+ Collaboration diagram for smt2_parsert:

Classes

struct  idt
 
struct  named_termt
 
struct  signature_with_parameter_idst
 

Public Types

using id_mapt = std::map< irep_idt, idt >
 
using named_termst = std::map< irep_idt, named_termt >
 

Public Member Functions

 smt2_parsert (std::istream &_in)
 
void parse ()
 
smt2_tokenizert::smt2_errort error (const std::string &message)
 
smt2_tokenizert::smt2_errort error ()
 
void skip_to_end_of_list ()
 This skips tokens until all bracketed expressions are closed. More...
 

Public Attributes

id_mapt id_map
 
named_termst named_terms
 
bool exit
 

Protected Types

using renaming_mapt = std::map< irep_idt, irep_idt >
 
using renaming_counterst = std::map< irep_idt, unsigned >
 

Protected Member Functions

smt2_tokenizert::tokent next_token ()
 
irep_idt add_fresh_id (const irep_idt &, idt::kindt, const exprt &)
 
void add_unique_id (const irep_idt &, const exprt &)
 
irep_idt rename_id (const irep_idt &) const
 
void setup_expressions ()
 
exprt expression ()
 
exprt function_application ()
 
exprt function_application_ieee_float_op (const irep_idt &, const exprt::operandst &)
 
exprt function_application_ieee_float_eq (const exprt::operandst &)
 
exprt function_application_fp (const exprt::operandst &)
 
exprt::operandst operands ()
 
typet function_signature_declaration ()
 
signature_with_parameter_idst function_signature_definition ()
 
exprt multi_ary (irep_idt, const exprt::operandst &)
 
exprt binary_predicate (irep_idt, const exprt::operandst &)
 
exprt binary (irep_idt, const exprt::operandst &)
 
exprt unary (irep_idt, const exprt::operandst &)
 
exprt let_expression ()
 
exprt quantifier_expression (irep_idt)
 
exprt function_application (const symbol_exprt &function, const exprt::operandst &op)
 
exprt::operandst cast_bv_to_signed (const exprt::operandst &)
 Apply typecast to signedbv to expressions in vector. More...
 
exprt cast_bv_to_unsigned (const exprt &)
 Apply typecast to unsignedbv to given expression. More...
 
typet sort ()
 
void setup_sorts ()
 
void command_sequence ()
 
void command (const std::string &)
 
void ignore_command ()
 
void setup_commands ()
 

Protected Attributes

smt2_tokenizert smt2_tokenizer
 
std::size_t parenthesis_level
 
renaming_mapt renaming_map
 
renaming_counterst renaming_counters
 
std::unordered_map< std::string, std::function< exprt()> > expressions
 
std::unordered_map< std::string, std::function< typet()> > sorts
 
std::unordered_map< std::string, std::function< void()> > commands
 

Detailed Description

Definition at line 20 of file smt2_parser.h.

Member Typedef Documentation

◆ id_mapt

using smt2_parsert::id_mapt = std::map<irep_idt, idt>

Definition at line 51 of file smt2_parser.h.

◆ named_termst

Definition at line 67 of file smt2_parser.h.

◆ renaming_counterst

using smt2_parsert::renaming_counterst = std::map<irep_idt, unsigned>
protected

Definition at line 94 of file smt2_parser.h.

◆ renaming_mapt

using smt2_parsert::renaming_mapt = std::map<irep_idt, irep_idt>
protected

Definition at line 92 of file smt2_parser.h.

Constructor & Destructor Documentation

◆ smt2_parsert()

smt2_parsert::smt2_parsert ( std::istream &  _in)
inlineexplicit

Definition at line 23 of file smt2_parser.h.

Member Function Documentation

◆ add_fresh_id()

irep_idt smt2_parsert::add_fresh_id ( const irep_idt id,
idt::kindt  kind,
const exprt expr 
)
protected

Definition at line 131 of file smt2_parser.cpp.

◆ add_unique_id()

void smt2_parsert::add_unique_id ( const irep_idt id,
const exprt expr 
)
protected

Definition at line 155 of file smt2_parser.cpp.

◆ binary()

exprt smt2_parsert::binary ( irep_idt  id,
const exprt::operandst op 
)
protected

Definition at line 403 of file smt2_parser.cpp.

◆ binary_predicate()

exprt smt2_parsert::binary_predicate ( irep_idt  id,
const exprt::operandst op 
)
protected

Definition at line 379 of file smt2_parser.cpp.

◆ cast_bv_to_signed()

exprt::operandst smt2_parsert::cast_bv_to_signed ( const exprt::operandst op)
protected

Apply typecast to signedbv to expressions in vector.

Definition at line 323 of file smt2_parser.cpp.

◆ cast_bv_to_unsigned()

exprt smt2_parsert::cast_bv_to_unsigned ( const exprt expr)
protected

Apply typecast to unsignedbv to given expression.

Definition at line 346 of file smt2_parser.cpp.

◆ command()

void smt2_parsert::command ( const std::string &  c)
protected

Definition at line 1236 of file smt2_parser.cpp.

◆ command_sequence()

void smt2_parsert::command_sequence ( )
protected

Definition at line 41 of file smt2_parser.cpp.

◆ error() [1/2]

smt2_tokenizert::smt2_errort smt2_parsert::error ( )
inline

Definition at line 77 of file smt2_parser.h.

◆ error() [2/2]

smt2_tokenizert::smt2_errort smt2_parsert::error ( const std::string &  message)
inline

Definition at line 72 of file smt2_parser.h.

◆ expression()

exprt smt2_parsert::expression ( )
protected

Definition at line 736 of file smt2_parser.cpp.

◆ function_application() [1/2]

exprt smt2_parsert::function_application ( )
protected

Definition at line 489 of file smt2_parser.cpp.

◆ function_application() [2/2]

exprt smt2_parsert::function_application ( const symbol_exprt function,
const exprt::operandst op 
)
protected

Definition at line 304 of file smt2_parser.cpp.

◆ function_application_fp()

exprt smt2_parsert::function_application_fp ( const exprt::operandst op)
protected

Definition at line 462 of file smt2_parser.cpp.

◆ function_application_ieee_float_eq()

exprt smt2_parsert::function_application_ieee_float_eq ( const exprt::operandst op)
protected

Definition at line 414 of file smt2_parser.cpp.

◆ function_application_ieee_float_op()

exprt smt2_parsert::function_application_ieee_float_op ( const irep_idt id,
const exprt::operandst op 
)
protected

Definition at line 433 of file smt2_parser.cpp.

◆ function_signature_declaration()

typet smt2_parsert::function_signature_declaration ( )
protected

Definition at line 1202 of file smt2_parser.cpp.

◆ function_signature_definition()

smt2_parsert::signature_with_parameter_idst smt2_parsert::function_signature_definition ( )
protected

Definition at line 1161 of file smt2_parser.cpp.

◆ ignore_command()

void smt2_parsert::ignore_command ( )
protected

Definition at line 86 of file smt2_parser.cpp.

◆ let_expression()

exprt smt2_parsert::let_expression ( )
protected

Definition at line 179 of file smt2_parser.cpp.

◆ multi_ary()

exprt smt2_parsert::multi_ary ( irep_idt  id,
const exprt::operandst op 
)
protected

Definition at line 358 of file smt2_parser.cpp.

◆ next_token()

smt2_tokenizert::tokent smt2_parsert::next_token ( )
protected

Definition at line 22 of file smt2_parser.cpp.

◆ operands()

exprt::operandst smt2_parsert::operands ( )
protected

Definition at line 119 of file smt2_parser.cpp.

◆ parse()

void smt2_parsert::parse ( )
inline

Definition at line 31 of file smt2_parser.h.

◆ quantifier_expression()

exprt smt2_parsert::quantifier_expression ( irep_idt  id)
protected

Definition at line 241 of file smt2_parser.cpp.

◆ rename_id()

irep_idt smt2_parsert::rename_id ( const irep_idt id) const
protected

Definition at line 169 of file smt2_parser.cpp.

◆ setup_commands()

void smt2_parsert::setup_commands ( )
protected

Definition at line 1248 of file smt2_parser.cpp.

◆ setup_expressions()

void smt2_parsert::setup_expressions ( )
protected

Definition at line 807 of file smt2_parser.cpp.

◆ setup_sorts()

void smt2_parsert::setup_sorts ( )
protected

Definition at line 1105 of file smt2_parser.cpp.

◆ skip_to_end_of_list()

void smt2_parsert::skip_to_end_of_list ( )

This skips tokens until all bracketed expressions are closed.

Definition at line 34 of file smt2_parser.cpp.

◆ sort()

typet smt2_parsert::sort ( )
protected

Definition at line 1060 of file smt2_parser.cpp.

◆ unary()

exprt smt2_parsert::unary ( irep_idt  id,
const exprt::operandst op 
)
protected

Definition at line 395 of file smt2_parser.cpp.

Member Data Documentation

◆ commands

std::unordered_map<std::string, std::function<void()> > smt2_parsert::commands
protected

Definition at line 158 of file smt2_parser.h.

◆ exit

bool smt2_parsert::exit

Definition at line 70 of file smt2_parser.h.

◆ expressions

std::unordered_map<std::string, std::function<exprt()> > smt2_parsert::expressions
protected

Definition at line 123 of file smt2_parser.h.

◆ id_map

id_mapt smt2_parsert::id_map

Definition at line 52 of file smt2_parser.h.

◆ named_terms

named_termst smt2_parsert::named_terms

Definition at line 68 of file smt2_parser.h.

◆ parenthesis_level

std::size_t smt2_parsert::parenthesis_level
protected

Definition at line 88 of file smt2_parser.h.

◆ renaming_counters

renaming_counterst smt2_parsert::renaming_counters
protected

Definition at line 95 of file smt2_parser.h.

◆ renaming_map

renaming_mapt smt2_parsert::renaming_map
protected

Definition at line 93 of file smt2_parser.h.

◆ smt2_tokenizer

smt2_tokenizert smt2_parsert::smt2_tokenizer
protected

Definition at line 86 of file smt2_parser.h.

◆ sorts

std::unordered_map<std::string, std::function<typet()> > smt2_parsert::sorts
protected

Definition at line 154 of file smt2_parser.h.


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