Go to the documentation of this file.
9 #ifndef CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
10 #define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
67 virtual void command(
const std::string &);
88 const std::vector<irep_idt> &_parameters)
92 (_type.
id() == ID_mathematical_function &&
94 _parameters.size()) ||
95 (_type.
id() != ID_mathematical_function && _parameters.empty()));
128 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
virtual 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
#define PRECONDITION(CONDITION)
renaming_counterst renaming_counters
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
The type of an expression, extends irept.
exprt function_application()
tokent next_token() override
The NIL type, i.e., an invalid type, no value.
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.
Expression to hold a symbol (variable)
signature_with_parameter_idst function_signature_definition()
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt unary(irep_idt, const exprt::operandst &)
std::size_t parenthesis_level
std::map< irep_idt, irep_idt > renaming_mapt
typet function_signature_declaration()
exprt function_application_fp(const exprt::operandst &)
exprt binary_predicate(irep_idt, const exprt::operandst &)
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
irep_idt get_fresh_id(const irep_idt &)
std::map< irep_idt, named_termt > named_termst
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
std::map< irep_idt, unsigned > renaming_counterst
std::vector< irep_idt > parameters
exprt::operandst operands()
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
smt2_parsert(std::istream &_in)