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)
189 const std::size_t rounding_mode_int =
190 numeric_cast_v<std::size_t>(rounding_mode_expr);
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, extends irept.
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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
literalt is_zero(const bvt &op)
#define CHECK_RETURN(CONDITION)
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
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
void add_over_assumption(literalt l)
void unpack(const mp_integer &i)
bvt convert_mult(const mult_exprt &expr) override
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
Resolve type symbol to the type it points to.
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.
bool is_constant() const
Return whether the expression is a constant.
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
mp_integer get_value(const bvt &bv)
bvt convert_floatbv_op(const exprt &expr) override
void get_values(approximationt &approximation)
literalt is_one(const bvt &op)
exprt get(const exprt &expr) const override
mstreamt & result() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a 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.
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
const std::string integer2binary(const mp_integer &n, std::size_t width)
#define UNREACHABLE
This should be used to mark dead code.
#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)
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 &)