22 #define MAX_INTEGER_UNDERAPPROX 3 23 #define MAX_FLOAT_UNDERAPPROX 10 36 under_assumptions.push_back(l);
42 return SUB::convert_floatbv_op(expr);
46 return SUB::convert_floatbv_op(expr);
56 return SUB::convert_mult(expr);
71 if(type.
id()!=ID_floatbv)
72 if(operands[0].is_constant() || operands[1].is_constant())
73 return SUB::convert_mult(expr);
79 if(type.
id()==ID_signedbv ||
80 type.
id()==ID_unsignedbv)
104 return SUB::convert_div(expr);
112 return SUB::convert_div(expr);
122 return SUB::convert_mod(expr);
130 return SUB::convert_mod(expr);
171 if(type.
id()==ID_floatbv)
190 to_integer(rounding_mode_expr, rounding_mode_int);
195 o0.rounding_mode=rounding_mode;
197 result.rounding_mode=rounding_mode;
199 if(a.
expr.
id()==ID_floatbv_plus)
201 else if(a.
expr.
id()==ID_floatbv_minus)
203 else if(a.
expr.
id()==ID_floatbv_mult)
205 else if(a.
expr.
id()==ID_floatbv_div)
217 debug() <<
"S1: " << o0 <<
" " << a.
expr.
id() <<
" " << o1
218 <<
" != " << rr <<
eom;
220 <<
" " << a.
expr.
id() <<
" " <<
224 <<
" " << a.
expr.
id() <<
" " <<
233 float_utils.
spec=spec;
260 float_utils.
spec=spec;
265 if(a.
expr.
id()==ID_floatbv_plus)
266 r=float_utils.
add(op0, op1);
267 else if(a.
expr.
id()==ID_floatbv_minus)
268 r=float_utils.
sub(op0, op1);
269 else if(a.
expr.
id()==ID_floatbv_mult)
270 r=float_utils.
mul(op0, op1);
271 else if(a.
expr.
id()==ID_floatbv_div)
272 r=float_utils.
div(op0, op1);
280 else if(type.
id()==ID_signedbv ||
281 type.
id()==ID_unsignedbv)
305 else if(a.
expr.
id()==ID_div)
307 else if(a.
expr.
id()==ID_mod)
327 else if(a.
expr.
id()==ID_div)
335 else if(a.
expr.
id()==ID_mod)
351 else if(type.
id()==ID_fixedbv)
392 float_utils.
spec=spec;
403 for(std::size_t i=0; i<fraction0.size(); i++)
406 for(std::size_t i=0; i<fraction1.size(); i++)
424 for(std::size_t i=x; i<fraction0.size(); i++)
427 for(std::size_t i=x; i<fraction1.size(); i++)
446 for(std::size_t i=x; i<a.
op0_bv.size(); i++)
449 for(std::size_t i=x; i<a.
op1_bv.size(); i++)
476 for(std::size_t i=0; i<a.
op0_bv.size(); i++)
479 for(std::size_t i=0; i<a.
op1_bv.size(); i++)
The type of an expression.
approximationt & add_approximation(const exprt &expr, bvt &bv)
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
const std::string & id2string(const irep_idt &d)
Fixed-width bit-vector with IEEE floating-point interpretation.
mstreamt & progress() const
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Deprecated expression utility functions.
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
boolbv_widtht boolbv_width
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::list< approximationt > approximations
virtual literalt lor(literalt a, literalt b)=0
literalt is_zero(const bvt &op)
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
void add_under_assumption(literalt l)
void initialize(approximationt &approximation)
virtual literalt limplies(literalt a, literalt b)=0
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
#define INVARIANT(CONDITION, REASON)
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
division (integer and real)
void add_over_assumption(literalt l)
void unpack(const mp_integer &i)
virtual const bvt & convert_bv(const exprt &expr)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
unsigned max_node_refinement
Max number of times we refine a formula node.
#define PRECONDITION(CONDITION)
bvt convert_mod(const mod_exprt &expr) override
const typet & follow(const typet &) const
virtual bvt div(const bvt &src1, const bvt &src2)
void set_equal(const bvt &a, const bvt &b)
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
std::vector< exprt > operandst
mp_integer get_value(const bvt &bv)
bvt convert_floatbv_op(const exprt &expr) override
bvt convert_mult(const exprt &expr) override
void get_values(approximationt &approximation)
literalt is_one(const bvt &op)
mstreamt & result() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
mstreamt & status() const
bvt add(const bvt &src1, const bvt &src2)
rounding_mode_bitst rounding_mode_bits
Base class for all expressions.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const std::string integer2binary(const mp_integer &n, std::size_t width)
#define string_refinement_invariantt(reason)
bool refine_arithmetic
Enable arithmetic refinement.
void set_frozen(literalt a) override
#define MAX_FLOAT_UNDERAPPROX
std::string as_string() const
void set(const ieee_floatt::rounding_modet mode)
rounding_modet rounding_mode
Abstraction Refinement Loop.
std::size_t width() const
bvt sub(const bvt &src1, const bvt &src2)
virtual bool is_in_conflict(literalt l) const
bvt convert_div(const div_exprt &expr) override
#define MAX_INTEGER_UNDERAPPROX
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
std::vector< literalt > bvt
void unpack(const mp_integer &i)
bvt build_constant(const ieee_floatt &)