cprover
Loading...
Searching...
No Matches
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) const
smt2_tokenizert::smt2_errort error () const
void skip_to_end_of_list ()
 This skips tokens until all bracketed expressions are closed.

Public Attributes

id_mapt id_map
named_termst named_terms
bool exit

Protected Member Functions

smt2_tokenizert::tokent next_token ()
void add_unique_id (irep_idt, exprt)
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 ()
void check_matching_operand_types (const exprt::operandst &) const
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 bv_division (const exprt::operandst &, bool is_signed)
exprt bv_mod (const exprt::operandst &, bool is_signed)
std::pair< binding_exprt::variablest, exprt > binding (irep_idt)
exprt lambda_expression ()
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.
exprt cast_bv_to_unsigned (const exprt &)
 Apply typecast to unsignedbv to given expression.
typet sort ()
typet function_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
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 57 of file smt2_parser.h.

◆ named_termst

using smt2_parsert::named_termst = std::map<irep_idt, named_termt>

Definition at line 73 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_unique_id()

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

Definition at line 135 of file smt2_parser.cpp.

◆ binary()

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

Definition at line 396 of file smt2_parser.cpp.

◆ binary_predicate()

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

Definition at line 378 of file smt2_parser.cpp.

◆ binding()

std::pair< binding_exprt::variablest, exprt > smt2_parsert::binding ( irep_idt id)
protected

Definition at line 220 of file smt2_parser.cpp.

◆ bv_division()

exprt smt2_parsert::bv_division ( const exprt::operandst & operands,
bool is_signed )
protected

Definition at line 1004 of file smt2_parser.cpp.

◆ bv_mod()

exprt smt2_parsert::bv_mod ( const exprt::operandst & operands,
bool is_signed )
protected

Definition at line 1033 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 316 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 339 of file smt2_parser.cpp.

◆ check_matching_operand_types()

void smt2_parsert::check_matching_operand_types ( const exprt::operandst & op) const
protected

Definition at line 351 of file smt2_parser.cpp.

◆ command()

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

Definition at line 1753 of file smt2_parser.cpp.

◆ command_sequence()

void smt2_parsert::command_sequence ( )
protected

Definition at line 44 of file smt2_parser.cpp.

◆ error() [1/2]

smt2_tokenizert::smt2_errort smt2_parsert::error ( ) const
inline

Definition at line 83 of file smt2_parser.h.

◆ error() [2/2]

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

Definition at line 78 of file smt2_parser.h.

◆ expression()

exprt smt2_parsert::expression ( )
protected

Definition at line 1062 of file smt2_parser.cpp.

◆ function_application() [1/2]

exprt smt2_parsert::function_application ( )
protected

Definition at line 491 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 297 of file smt2_parser.cpp.

◆ function_application_fp()

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

Definition at line 454 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 406 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 425 of file smt2_parser.cpp.

◆ function_signature_declaration()

typet smt2_parsert::function_signature_declaration ( )
protected

Definition at line 1730 of file smt2_parser.cpp.

◆ function_signature_definition()

smt2_parsert::signature_with_parameter_idst smt2_parsert::function_signature_definition ( )
protected

Definition at line 1690 of file smt2_parser.cpp.

◆ function_sort()

typet smt2_parsert::function_sort ( )
protected

Definition at line 1534 of file smt2_parser.cpp.

◆ ignore_command()

void smt2_parsert::ignore_command ( )
protected

Definition at line 90 of file smt2_parser.cpp.

◆ lambda_expression()

exprt smt2_parsert::lambda_expression ( )
protected

Definition at line 281 of file smt2_parser.cpp.

◆ let_expression()

exprt smt2_parsert::let_expression ( )
protected

Definition at line 149 of file smt2_parser.cpp.

◆ multi_ary()

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

Definition at line 366 of file smt2_parser.cpp.

◆ next_token()

smt2_tokenizert::tokent smt2_parsert::next_token ( )
protected

Definition at line 25 of file smt2_parser.cpp.

◆ operands()

exprt::operandst smt2_parsert::operands ( )
protected

Definition at line 123 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 287 of file smt2_parser.cpp.

◆ setup_commands()

void smt2_parsert::setup_commands ( )
protected

Definition at line 1765 of file smt2_parser.cpp.

◆ setup_expressions()

void smt2_parsert::setup_expressions ( )
protected

Definition at line 1134 of file smt2_parser.cpp.

◆ setup_sorts()

void smt2_parsert::setup_sorts ( )
protected

Definition at line 1614 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 37 of file smt2_parser.cpp.

◆ sort()

typet smt2_parsert::sort ( )
protected

Definition at line 1560 of file smt2_parser.cpp.

◆ unary()

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

Definition at line 388 of file smt2_parser.cpp.

Member Data Documentation

◆ commands

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

Definition at line 190 of file smt2_parser.h.

◆ exit

bool smt2_parsert::exit

Definition at line 76 of file smt2_parser.h.

◆ expressions

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

Definition at line 149 of file smt2_parser.h.

◆ id_map

id_mapt smt2_parsert::id_map

Definition at line 58 of file smt2_parser.h.

◆ named_terms

named_termst smt2_parsert::named_terms

Definition at line 74 of file smt2_parser.h.

◆ parenthesis_level

std::size_t smt2_parsert::parenthesis_level
protected

Definition at line 94 of file smt2_parser.h.

◆ smt2_tokenizer

smt2_tokenizert smt2_parsert::smt2_tokenizer
protected

Definition at line 92 of file smt2_parser.h.

◆ sorts

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

Definition at line 186 of file smt2_parser.h.

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