9 #ifndef CPROVER_SOLVERS_SMT2_SMT2_PARSER_H 10 #define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H 50 virtual void command(
const std::string &);
85 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H The type of an expression.
renaming_mapt renaming_map
typet function_signature_declaration()
exprt quantifier_expression(irep_idt)
irep_idt get_fresh_id(const irep_idt &)
exprt cast_bv_to_unsigned(const exprt &)
Apply typecast to unsignedbv to given expression.
std::map< irep_idt, idt > id_mapt
exprt::operandst operands()
renaming_counterst renaming_counters
exprt binary_predicate(irep_idt, const exprt::operandst &)
API to expression classes.
std::map< irep_idt, irep_idt > renaming_mapt
irep_idt rename_id(const irep_idt &) const
typet function_signature_definition()
std::vector< exprt > operandst
exprt multi_ary(irep_idt, const exprt::operandst &)
exprt unary(irep_idt, const exprt::operandst &)
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.
exprt::operandst cast_bv_to_signed(const exprt::operandst &)
Apply typecast to signedbv to expressions in vector.
exprt function_application()
smt2_parsert(std::istream &_in)