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 The type of an expression, extends irept.
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
std::size_t parenthesis_level
renaming_mapt renaming_map
typet function_signature_declaration()
exprt quantifier_expression(irep_idt)
irep_idt get_fresh_id(const irep_idt &)
std::map< irep_idt, named_termt > named_termst
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
std::map< irep_idt, idt > id_mapt
exprt::operandst operands()
const irep_idt & id() const
signature_with_parameter_idst(const typet &_type, const std::vector< irep_idt > &_parameters)
renaming_counterst renaming_counters
exprt binary_predicate(irep_idt, const exprt::operandst &)
exprt function_application_ieee_float_op(const irep_idt &, const exprt::operandst &)
tokent next_token() override
API to expression classes.
std::map< irep_idt, irep_idt > renaming_mapt
#define PRECONDITION(CONDITION)
irep_idt rename_id(const irep_idt &) const
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::vector< exprt > operandst
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt unary(irep_idt, const exprt::operandst &)
std::vector< irep_idt > parameters
std::map< irep_idt, unsigned > renaming_counterst
virtual void command(const std::string &)
exprt binary(irep_idt, const exprt::operandst &)
Base class for all expressions.
signature_with_parameter_idst(const typet &_type)
signature_with_parameter_idst function_signature_definition()
The NIL type, i.e., an invalid type, no value.
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
std::vector< irep_idt > parameters
exprt function_application()
Expression to hold a symbol (variable)
smt2_parsert(std::istream &_in)
exprt function_application_fp(const exprt::operandst &)