Go to the documentation of this file.
9 #ifndef CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
10 #define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
13 #include <unordered_map>
38 using kindt =
enum { VARIABLE, BINDING, PARAMETER };
111 const std::vector<irep_idt> &_parameters)
115 (_type.
id() == ID_mathematical_function &&
117 _parameters.size()) ||
118 (_type.
id() != ID_mathematical_function && _parameters.empty()));
154 std::unordered_map<std::string, std::function<
typet()>>
sorts;
158 std::unordered_map<std::string, std::function<void()>>
commands;
161 void command(
const std::string &);
166 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
void command(const std::string &)
exprt quantifier_expression(irep_idt)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
irep_idt rename_id(const irep_idt &) const
smt2_tokenizert::smt2_errort error(const std::string &message)
renaming_counterst renaming_counters
smt2_tokenizert::smt2_errort error()
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
The type of an expression, extends irept.
std::unordered_map< std::string, std::function< typet()> > sorts
std::unordered_map< std::string, std::function< exprt()> > expressions
exprt function_application()
irep_idt add_fresh_id(const irep_idt &, idt::kindt, const exprt &)
signature_with_parameter_idst(const typet &_type, const std::vector< irep_idt > &_parameters)
std::vector< irep_idt > parameters
exprt binary(irep_idt, const exprt::operandst &)
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Base class for all expressions.
smt2_errort error(const std::string &message)
generate an error exception, pre-filled with a message
std::unordered_map< std::string, std::function< void()> > commands
Expression to hold a symbol (variable)
signature_with_parameter_idst function_signature_definition()
void add_unique_id(const irep_idt &, const exprt &)
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt unary(irep_idt, const exprt::operandst &)
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
std::size_t parenthesis_level
std::map< irep_idt, irep_idt > renaming_mapt
typet function_signature_declaration()
exprt function_application_fp(const exprt::operandst &)
#define PRECONDITION(CONDITION)
exprt binary_predicate(irep_idt, const exprt::operandst &)
named_termt(const exprt &_term, const symbol_exprt &_name)
Default-constructing a symbol_exprt is deprecated, thus make sure we always construct a named_termt f...
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
const irep_idt & id() const
std::vector< exprt > operandst
renaming_mapt renaming_map
signature_with_parameter_idst(const typet &_type)
std::map< irep_idt, idt > id_mapt
std::map< irep_idt, named_termt > named_termst
exprt function_application_ieee_float_eq(const exprt::operandst &)
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
enum { VARIABLE, BINDING, PARAMETER } kindt
smt2_tokenizert::tokent next_token()
std::map< irep_idt, unsigned > renaming_counterst
std::vector< irep_idt > parameters
exprt::operandst operands()
smt2_tokenizert smt2_tokenizer
idt(kindt _kind, const exprt &expr)
API to expression classes.
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
smt2_parsert(std::istream &_in)