21 #define MAX_INTEGER_UNDERAPPROX 3 22 #define MAX_FLOAT_UNDERAPPROX 10 35 under_assumptions.push_back(l);
64 assert(operands.size()>=2);
70 if(type.
id()!=ID_floatbv)
71 if(operands[0].is_constant() || operands[1].is_constant())
78 if(type.
id()==ID_signedbv ||
79 type.
id()==ID_unsignedbv)
170 if(type.
id()==ID_floatbv)
187 to_integer(rounding_mode_expr, rounding_mode_int);
192 o0.rounding_mode=rounding_mode;
194 result.rounding_mode=rounding_mode;
196 if(a.
expr.
id()==ID_floatbv_plus)
198 else if(a.
expr.
id()==ID_floatbv_minus)
200 else if(a.
expr.
id()==ID_floatbv_mult)
202 else if(a.
expr.
id()==ID_floatbv_div)
214 debug() <<
"S1: " << o0 <<
" " << a.
expr.
id() <<
" " << o1
215 <<
" != " << rr <<
eom;
217 <<
" " << a.
expr.
id() <<
" " <<
221 <<
" " << a.
expr.
id() <<
" " <<
232 float_utils.
spec=spec;
259 float_utils.
spec=spec;
264 if(a.
expr.
id()==ID_floatbv_plus)
265 r=float_utils.
add(op0, op1);
266 else if(a.
expr.
id()==ID_floatbv_minus)
267 r=float_utils.
sub(op0, op1);
268 else if(a.
expr.
id()==ID_floatbv_mult)
269 r=float_utils.
mul(op0, op1);
270 else if(a.
expr.
id()==ID_floatbv_div)
271 r=float_utils.
div(op0, op1);
275 assert(
r.size()==res.size());
279 else if(type.
id()==ID_signedbv ||
280 type.
id()==ID_unsignedbv)
302 else if(a.
expr.
id()==ID_div)
304 else if(a.
expr.
id()==ID_mod)
324 else if(a.
expr.
id()==ID_div)
332 else if(a.
expr.
id()==ID_mod)
348 else if(type.
id()==ID_fixedbv)
389 float_utils.
spec=spec;
400 for(std::size_t i=0; i<fraction0.size(); i++)
403 for(std::size_t i=0; i<fraction1.size(); i++)
421 for(std::size_t i=x; i<fraction0.size(); i++)
424 for(std::size_t i=x; i<fraction1.size(); i++)
443 for(std::size_t i=x; i<a.
op0_bv.size(); i++)
446 for(std::size_t i=x; i<a.
op1_bv.size(); i++)
473 for(std::size_t i=0; i<a.
op0_bv.size(); i++)
476 for(std::size_t i=0; i<a.
op1_bv.size(); i++)
531 return std::to_string(id_nr)+
"/"+
id2string(expr.id());
The type of an expression.
const typet & follow(const typet &src) const
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)
bool is_in_conflict(approximationt &approximation)
check if an under-approximation is part of the conflict
Fixed-width bit-vector with IEEE floating-point interpretation.
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)
approximationst approximations
virtual literalt lor(literalt a, literalt b)=0
virtual void set_frozen(literalt a) override
literalt is_zero(const bvt &op)
static mstreamt & eom(mstreamt &m)
void add_under_assumption(literalt l)
void initialize(approximationt &approximation)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual bvt convert_mult(const exprt &expr)
virtual bvt convert_floatbv_op(const exprt &expr)
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)
bool do_arithmetic_refinement
virtual bvt convert_floatbv_op(const exprt &expr)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
virtual bvt convert_mult(const exprt &expr)
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.
virtual bvt convert_mod(const mod_exprt &expr)
std::vector< exprt > operandst
unsigned max_node_refinement
mp_integer get_value(const bvt &bv)
void get_values(approximationt &approximation)
literalt is_one(const bvt &op)
bvt add(const bvt &src1, const bvt &src2)
rounding_mode_bitst rounding_mode_bits
Base class for all expressions.
virtual bvt convert_mod(const mod_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
const std::string integer2binary(const mp_integer &n, std::size_t width)
#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 bvt convert_div(const div_exprt &expr)
virtual bool is_in_conflict(literalt l) const
#define MAX_INTEGER_UNDERAPPROX
virtual void check_UNSAT()
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 &)