cprover
|
Loop Acceleration. More...
#include <util/std_types.h>
Go to the source code of this file.
Functions | |
signedbv_typet | signed_poly_type () |
unsignedbv_typet | unsigned_poly_type () |
bool | is_bitvector (const typet &t) |
Convenience function – is the type a bitvector of some kind? More... | |
typet | join_types (const typet &t1, const typet &t2) |
Return the smallest type that both t1 and t2 can be cast to without losing information. More... | |
Loop Acceleration.
Definition in file util.h.
bool is_bitvector | ( | const typet & | t | ) |
Convenience function – is the type a bitvector of some kind?
Definition at line 33 of file util.cpp.
References irept::id().
Referenced by polynomial_acceleratort::fit_polynomial_sliced(), and join_types().
Return the smallest type that both t1 and t2 can be cast to without losing information.
e.g.
join_types(unsignedbv_typet(32), unsignedbv_typet(16))=unsignedbv_typet(32) join_types(signedbv_typet(16), unsignedbv_typet(16))=signedbv_typet(17) join_types(signedbv_typet(32), signedbv_typet(32))=signedbv_typet(32)
Definition at line 70 of file util.cpp.
References bitvector_typet::get_width(), INVARIANT, is_bitvector(), is_signed(), is_unsigned(), irept::pretty(), and to_bitvector_type().
Referenced by disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), overflow_instrumentert::fix_types(), and polynomialt::to_expr().
signedbv_typet signed_poly_type | ( | ) |
Definition at line 20 of file util.cpp.
References configt::ansi_c, config, and configt::ansi_ct::int_width.
Referenced by acceleration_utilst::do_arrays(), and disjunctive_polynomial_accelerationt::fit_polynomial().
unsignedbv_typet unsigned_poly_type | ( | ) |
Definition at line 25 of file util.cpp.
References configt::ansi_c, config, and configt::ansi_ct::int_width.
Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), acceleration_utilst::assign_array(), acceleration_utilst::do_arrays(), and acceleratet::insert_automaton().