cprover
|
#include "mp_arith.h"
#include <cassert>
#include <cctype>
#include <cstdlib>
#include <limits>
#include <ostream>
#include <sstream>
#include <vector>
#include "arith_tools.h"
#include "invariant.h"
Go to the source code of this file.
Typedefs | |
typedef BigInt::ullong_t | ullong_t |
typedef BigInt::llong_t | llong_t |
Functions | |
mp_integer | operator>> (const mp_integer &a, const mp_integer &b) |
mp_integer | operator<< (const mp_integer &a, const mp_integer &b) |
std::ostream & | operator<< (std::ostream &out, const mp_integer &n) |
const mp_integer | string2integer (const std::string &n, unsigned base) |
const std::string | integer2binary (const mp_integer &n, std::size_t width) |
const std::string | integer2string (const mp_integer &n, unsigned base) |
const mp_integer | binary2integer (const std::string &n, bool is_signed) |
convert binary string representation to mp_integer More... | |
mp_integer::ullong_t | integer2ulong (const mp_integer &n) |
std::size_t | integer2size_t (const mp_integer &n) |
unsigned | integer2unsigned (const mp_integer &n) |
mp_integer | bitwise_or (const mp_integer &a, const mp_integer &b) |
bitwise or bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | bitwise_and (const mp_integer &a, const mp_integer &b) |
bitwise and bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | bitwise_xor (const mp_integer &a, const mp_integer &b) |
bitwise xor bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | bitwise_neg (const mp_integer &a) |
bitwise negation bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | arith_left_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size) |
arithmetic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | arith_right_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size) |
arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | logic_left_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size) |
logic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | logic_right_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size) |
logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | rotate_right (const mp_integer &a, const mp_integer &b, std::size_t true_size) |
rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
mp_integer | rotate_left (const mp_integer &a, const mp_integer &b, std::size_t true_size) |
rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More... | |
typedef BigInt::llong_t llong_t |
Definition at line 23 of file mp_arith.cpp.
typedef BigInt::ullong_t ullong_t |
Definition at line 22 of file mp_arith.cpp.
mp_integer arith_left_shift | ( | const mp_integer & | a, |
const mp_integer & | b, | ||
std::size_t | true_size | ||
) |
arithmetic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 252 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
mp_integer arith_right_shift | ( | const mp_integer & | a, |
const mp_integer & | b, | ||
std::size_t | true_size | ||
) |
arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 273 of file mp_arith.cpp.
References pad(), PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
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(), and messaget::result().
Referenced by bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), smt2_convt::convert_constant(), expr2ct::convert_constant(), 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(), get_thread_block_identifier(), exprt::is_one(), mul_expr(), smt2_convt::parse_literal(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_typecast(), sum_expr(), sum_over_map(), and to_integer().
mp_integer bitwise_and | ( | const mp_integer & | a, |
const mp_integer & | b | ||
) |
bitwise and bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 222 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
mp_integer bitwise_neg | ( | const mp_integer & | a | ) |
bitwise negation bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 242 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
mp_integer bitwise_or | ( | const mp_integer & | a, |
const mp_integer & | b | ||
) |
bitwise or bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 212 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
mp_integer bitwise_xor | ( | const mp_integer & | a, |
const mp_integer & | b | ||
) |
bitwise xor bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 232 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
const std::string integer2binary | ( | const mp_integer & | n, |
std::size_t | width | ||
) |
Definition at line 67 of file mp_arith.cpp.
References neg(), and messaget::result().
Referenced by 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(), linker_script_merget::ls_data2instructions(), mul_expr(), smt2_convt::parse_literal(), simplify_exprt::simplify_bitwise(), sum_expr(), 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(), and PRECONDITION.
Referenced by add_padding(), add_padding_gcc(), add_padding_msvc(), as_vcd_binary(), interpretert::assign(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), endianness_mapt::build_little_endian(), bv_pointerst::bv_get_rec(), 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::evaluate(), interpretert::execute_assign(), expr_initializert< nondet >::expr_initializer_rec(), flatten_byte_update(), rw_range_sett::get_objects_byte_extract(), interpretert::get_value(), lower_popcount(), linker_script_merget::ls_data2instructions(), c_typecheck_baset::make_designator(), smt2_convt::parse_rec(), interpretert::read_unbounded(), remove_vector(), 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 & | n, |
unsigned | base | ||
) |
Definition at line 106 of file mp_arith.cpp.
References messaget::result().
Referenced by inv_object_storet::build_string(), string_abstractiont::build_symbol_constant(), boolbvt::bv_get_rec(), boolbvt::bv_get_unbounded_array(), expr2javat::convert_constant(), expr2ct::convert_constant(), java_bytecode_convert_methodt::convert_if(), java_bytecode_convert_methodt::convert_if_cmp(), java_bytecode_convert_methodt::convert_ifnonull(), java_bytecode_convert_methodt::convert_ifnull(), java_bytecode_convert_methodt::convert_instructions(), expr2ct::convert_rec(), java_bytecode_convert_methodt::convert_switch(), expr2ct::convert_with_precedence(), cpp_typecheck_resolvet::do_builtin(), fixedbvt::format(), bv_arithmetict::format(), from_integer(), from_rational(), get_thread_block_identifier(), mul_expr(), format_constantt::operator()(), operator<<(), value_set_fit::output(), value_set_fivrt::output(), value_sett::output(), value_set_fivrnst::output_entry(), pointer_offset_bits_as_string(), range_typet::set_from(), range_typet::set_to(), sum_expr(), cpp_typecheckt::template_suffix(), ieee_floatt::to_string_decimal(), ieee_floatt::to_string_scientific(), trace_value_binary(), type2name(), 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.
References PRECONDITION.
Referenced by interpretert::allocate(), interpretert::assign(), interpretert::base_address_to_actual_size(), interpretert::build_memory_map(), bv_refinementt::check_SAT(), expr2ct::convert_constant(), interpretert::execute_assign(), goto_convertt::get_string_constant(), interpretert::get_value(), integer2size_t(), integer2unsigned(), interpretert::read(), and string_constraint_generatort::to_integer_or_default().
unsigned integer2unsigned | ( | const mp_integer & | ) |
Definition at line 202 of file mp_arith.cpp.
References integer2ulong(), and PRECONDITION.
Referenced by expr2ct::convert_array(), boolbvt::convert_byte_update(), boolbvt::convert_extractbits(), java_bytecode_convert_methodt::convert_if(), java_bytecode_convert_methodt::convert_if_cmp(), java_bytecode_convert_methodt::convert_ifnonull(), java_bytecode_convert_methodt::convert_ifnull(), boolbvt::convert_lambda(), boolbvt::convert_replication(), java_bytecode_convert_methodt::convert_switch(), boolbvt::convert_with_array(), flatten_byte_extract(), flatten_byte_update(), string_constantt::from_array_expr(), boolbv_widtht::get_entry(), boolbvt::literal(), linker_script_merget::ls_data2instructions(), qbf_qube_coret::prop_solve(), to_unsigned_integer(), and unsigned_from_ns().
mp_integer logic_left_shift | ( | const mp_integer & | a, |
const mp_integer & | b, | ||
std::size_t | true_size | ||
) |
logic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 293 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
mp_integer logic_right_shift | ( | const mp_integer & | a, |
const mp_integer & | b, | ||
std::size_t | true_size | ||
) |
logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 319 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
mp_integer operator<< | ( | const mp_integer & | a, |
const mp_integer & | b | ||
) |
Definition at line 43 of file mp_arith.cpp.
References power().
std::ostream& operator<< | ( | std::ostream & | out, |
const mp_integer & | n | ||
) |
Definition at line 48 of file mp_arith.cpp.
References integer2string().
mp_integer operator>> | ( | const mp_integer & | a, |
const mp_integer & | b | ||
) |
Definition at line 25 of file mp_arith.cpp.
References power().
mp_integer rotate_left | ( | const mp_integer & | a, |
const mp_integer & | b, | ||
std::size_t | true_size | ||
) |
rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 356 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
mp_integer rotate_right | ( | const mp_integer & | a, |
const mp_integer & | b, | ||
std::size_t | true_size | ||
) |
rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)
Definition at line 336 of file mp_arith.cpp.
References PRECONDITION, and messaget::result().
Referenced by interpretert::evaluate().
const mp_integer string2integer | ( | const std::string & | n, |
unsigned | base | ||
) |
Definition at line 57 of file mp_arith.cpp.
Referenced by boolbvt::bv_get_rec(), boolbvt::convert_constant(), java_bytecode_convert_methodt::convert_instructions(), convert_integer_literal(), bv_pointerst::convert_pointer_type(), expr2ct::convert_rec(), boolbvt::convert_typecast(), smt2_parsert::expression(), smt2_parsert::function_application(), boolbv_widtht::get_entry(), range_typet::get_from(), range_typet::get_to(), exprt::is_one(), linker_script_merget::ls_data2instructions(), mul_expr(), parse_field_width(), parse_floatt::parse_floatt(), smt2_convt::parse_literal(), parse_precision(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), sum_expr(), to_integer(), and to_rational().