cprover
|
#include <string>
#include <iosfwd>
#include "big-int/bigint.hh"
Go to the source code of this file.
Typedefs | |
typedef BigInt | mp_integer |
Functions | |
std::ostream & | operator<< (std::ostream &, const mp_integer &) |
mp_integer | operator>> (const mp_integer &, const mp_integer &) |
mp_integer | operator<< (const mp_integer &, const mp_integer &) |
const std::string | integer2string (const mp_integer &, unsigned base=10) |
const mp_integer | string2integer (const std::string &, unsigned base=10) |
const std::string | integer2binary (const mp_integer &, std::size_t width) |
const mp_integer | binary2integer (const std::string &, bool is_signed) |
convert binary string representation to mp_integer More... | |
mp_integer::ullong_t | integer2ulong (const mp_integer &) |
std::size_t | integer2size_t (const mp_integer &) |
unsigned | integer2unsigned (const mp_integer &) |
typedef BigInt mp_integer |
Definition at line 19 of file mp_arith.h.
const mp_integer binary2integer | ( | const std::string & | n, |
bool | is_signed | ||
) |
convert binary string representation to mp_integer
Definition at line 120 of file mp_arith.cpp.
References is_signed().
Referenced by bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), smt1_convt::ce_value(), smt1_convt::convert_constant(), smt2_convt::convert_constant(), expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), smt2_convt::convert_rounding_mode_FPA(), interpretert::evaluate(), acceleration_utilst::extract_polynomial(), polynomial_acceleratort::fit_const(), polynomialt::from_expr(), fixedbvt::from_expr(), bv_arithmetict::from_expr(), ieee_floatt::from_expr(), goto_convertt::get_string_constant(), exprt::is_one(), exprt::mul(), exprt::negate(), smt2_convt::parse_literal(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_typecast(), exprt::subtract(), exprt::sum(), string_refinementt::sum_over_map(), and to_integer().
const std::string integer2binary | ( | const mp_integer & | n, |
std::size_t | width | ||
) |
Definition at line 63 of file mp_arith.cpp.
References neg().
Referenced by dplib_convt::array_index(), cvc_convt::array_index(), bv_utilst::build_constant(), bv_refinementt::check_SAT(), smt2_convt::convert_constant(), boolbvt::convert_constant(), convert_float_literal(), smt2_convt::convert_typecast(), interpretert::evaluate(), from_integer(), smt1_dect::mathsat_value(), exprt::mul(), smt2_convt::parse_literal(), smt1_dect::read_result_cvc3(), simplify_exprt::simplify_bitwise(), smt1_dect::string_to_expr_z3(), exprt::subtract(), exprt::sum(), fixedbvt::to_expr(), bv_arithmetict::to_expr(), and ieee_floatt::to_expr().
std::size_t integer2size_t | ( | const mp_integer & | ) |
Definition at line 195 of file mp_arith.cpp.
References integer2ulong().
Referenced by path_symex_statet::array_theory(), as_vcd_binary(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), endianness_mapt::build_little_endian(), boolbvt::bv_get_unbounded_array(), boolbvt::convert_byte_update(), boolbvt::convert_extractbit(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), boolbvt::convert_shift(), boolbvt::convert_update_rec(), boolbvt::convert_with_bv(), c_typecheck_baset::designator_enter(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer_rec(), interpretert::execute_function_call(), path_symex_statet::expand_structs_and_arrays(), flatten_byte_update(), rw_range_sett::get_objects_byte_extract(), c_typecheck_baset::make_designator(), smt2_convt::parse_rec(), interpretert::read(), remove_vector(), float_bvt::rounder(), float_utilst::rounder(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_index(), simplify_exprt::simplify_member(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), ieee_floatt::to_string_decimal(), remove_const_function_pointerst::try_resolve_index_of(), c_typecheck_baset::typecheck_c_bit_field_type(), and java_bytecode_convert_methodt::variable().
const std::string integer2string | ( | const mp_integer & | , |
unsigned | base = 10 |
||
) |
Definition at line 104 of file mp_arith.cpp.
Referenced by path_symex_statet::array_index_as_string(), inv_object_storet::build_string(), string_abstractiont::build_symbol_constant(), boolbvt::bv_get_rec(), boolbvt::bv_get_unbounded_array(), concatenate_array_id(), expr2javat::convert_constant(), expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), java_bytecode_convert_methodt::convert_instructions(), expr2ct::convert_rec(), expr2ct::convert_with_precedence(), cpp_typecheck_resolvet::do_builtin(), fixedbvt::format(), bv_arithmetict::format(), from_integer(), from_rational(), json(), exprt::mul(), exprt::negate(), format_constantt::operator()(), operator<<(), value_sett::output(), value_set_fit::output(), value_set_fivrt::output(), value_set_fivrnst::output_entry(), range_typet::set_from(), range_typet::set_to(), exprt::subtract(), exprt::sum(), cpp_typecheckt::template_suffix(), ieee_floatt::to_string_decimal(), ieee_floatt::to_string_scientific(), type2name(), type_max(), c_typecheck_baset::typecheck_c_enum_type(), c_typecheck_baset::typecheck_custom_type(), and xml().
mp_integer::ullong_t integer2ulong | ( | const mp_integer & | ) |
Definition at line 189 of file mp_arith.cpp.
Referenced by bv_refinementt::check_SAT(), expr2ct::convert_constant(), goto_convertt::get_string_constant(), integer2size_t(), and integer2unsigned().
unsigned integer2unsigned | ( | const mp_integer & | ) |
Definition at line 203 of file mp_arith.cpp.
References integer2ulong().
Referenced by add_padding(), interpretert::assign(), partial_order_concurrencyt::build_clock_type(), bv_pointerst::bv_get_rec(), smt1_convt::ce_value(), expr2ct::convert_array(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), boolbvt::convert_extractbit(), boolbvt::convert_extractbits(), boolbvt::convert_lambda(), boolbvt::convert_replication(), boolbvt::convert_with_array(), flatten_byte_extract(), flatten_byte_update(), string_constantt::from_array_expr(), boolbv_widtht::get_entry(), interpretert::get_size(), float_bvt::limit_distance(), float_utilst::limit_distance(), boolbvt::literal(), float_bvt::normalization_shift(), float_utilst::normalization_shift(), qbf_qube_coret::prop_solve(), smt1_dect::read_result_cvc3(), smt1_dect::string_to_expr_z3(), to_unsigned_integer(), unsigned_from_ns(), and zero_initializert::zero_initializer_rec().
std::ostream& operator<< | ( | std::ostream & | , |
const mp_integer & | |||
) |
Definition at line 44 of file mp_arith.cpp.
References integer2string().
mp_integer operator<< | ( | const mp_integer & | , |
const mp_integer & | |||
) |
Definition at line 39 of file mp_arith.cpp.
References power().
mp_integer operator>> | ( | const mp_integer & | , |
const mp_integer & | |||
) |
Definition at line 21 of file mp_arith.cpp.
References power().
const mp_integer string2integer | ( | const std::string & | n, |
unsigned | base | ||
) |
Definition at line 53 of file mp_arith.cpp.
Referenced by as_vcd_binary(), boolbvt::bv_get_rec(), concatenate_array_id(), boolbvt::convert_constant(), java_bytecode_convert_methodt::convert_instructions(), convert_integer_literal(), bv_pointerst::convert_pointer_type(), expr2ct::convert_rec(), boolbvt::convert_typecast(), boolbv_widtht::get_entry(), range_typet::get_from(), range_typet::get_to(), exprt::is_one(), smt1_dect::mathsat_value(), exprt::mul(), exprt::negate(), parse_field_width(), parse_float(), smt2_convt::parse_literal(), parse_precision(), smt1_dect::read_result_cvc3(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), smt1_dect::string_to_expr_z3(), exprt::subtract(), exprt::sum(), to_integer(), and to_rational().