cprover
refine_arithmetic.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "bv_refinement.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/bv_arithmetic.h>
13 #include <util/expr_util.h>
14 #include <util/floatbv_expr.h>
15 #include <util/ieee_float.h>
16 
18 
19 // Parameters
20 #define MAX_INTEGER_UNDERAPPROX 3
21 #define MAX_FLOAT_UNDERAPPROX 10
22 
24 {
25  // if it's a constant already, give up
26  if(!l.is_constant())
27  over_assumptions.push_back(literal_exprt(l));
28 }
29 
31 {
32  // if it's a constant already, give up
33  if(!l.is_constant())
34  under_assumptions.push_back(literal_exprt(l));
35 }
36 
38 {
40  return SUB::convert_floatbv_op(expr);
41 
42  if(expr.type().id() != ID_floatbv)
43  return SUB::convert_floatbv_op(expr);
44 
45  bvt bv;
46  add_approximation(expr, bv);
47  return bv;
48 }
49 
51 {
52  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
53  return SUB::convert_mult(expr);
54 
55  // we catch any multiplication
56  // unless it involves a constant
57 
58  const exprt::operandst &operands=expr.operands();
59 
60  const typet &type = expr.type();
61 
62  PRECONDITION(operands.size()>=2);
63 
64  if(operands.size()>2)
65  return convert_mult(to_mult_expr(make_binary(expr))); // make binary
66 
67  // we keep multiplication by a constant for integers
68  if(type.id()!=ID_floatbv)
69  if(operands[0].is_constant() || operands[1].is_constant())
70  return SUB::convert_mult(expr);
71 
72  bvt bv;
73  approximationt &a=add_approximation(expr, bv);
74 
75  // initially, we have a partial interpretation for integers
76  if(type.id()==ID_signedbv ||
77  type.id()==ID_unsignedbv)
78  {
79  // x*0==0 and 0*x==0
80  literalt op0_zero=bv_utils.is_zero(a.op0_bv);
81  literalt op1_zero=bv_utils.is_zero(a.op1_bv);
82  literalt res_zero=bv_utils.is_zero(a.result_bv);
84  prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));
85 
86  // x*1==x and 1*x==x
87  literalt op0_one=bv_utils.is_one(a.op0_bv);
88  literalt op1_one=bv_utils.is_one(a.op1_bv);
89  literalt res_op0=bv_utils.equal(a.op0_bv, a.result_bv);
90  literalt res_op1=bv_utils.equal(a.op1_bv, a.result_bv);
91  prop.l_set_to_true(prop.limplies(op0_one, res_op1));
92  prop.l_set_to_true(prop.limplies(op1_one, res_op0));
93  }
94 
95  return bv;
96 }
97 
99 {
100  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
101  return SUB::convert_div(expr);
102 
103  // we catch any division
104  // unless it's integer division by a constant
105 
106  PRECONDITION(expr.operands().size()==2);
107 
108  if(expr.op1().is_constant())
109  return SUB::convert_div(expr);
110 
111  bvt bv;
112  add_approximation(expr, bv);
113  return bv;
114 }
115 
117 {
118  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
119  return SUB::convert_mod(expr);
120 
121  // we catch any mod
122  // unless it's integer + constant
123 
124  PRECONDITION(expr.operands().size()==2);
125 
126  if(expr.op1().is_constant())
127  return SUB::convert_mod(expr);
128 
129  bvt bv;
130  add_approximation(expr, bv);
131  return bv;
132 }
133 
135 {
136  std::size_t o=a.expr.operands().size();
137 
138  if(o==1)
140  else if(o==2)
141  {
144  }
145  else if(o==3)
146  {
150  }
151  else
152  UNREACHABLE;
153 
155 }
156 
160 {
161  // see if the satisfying assignment is spurious in any way
162 
163  const typet &type = a.expr.type();
164 
165  if(type.id()==ID_floatbv)
166  {
167  const auto &float_op = to_ieee_float_op_expr(a.expr);
168 
169  if(a.over_state==MAX_STATE)
170  return;
171 
172  ieee_float_spect spec(to_floatbv_type(type));
173  ieee_floatt o0(spec), o1(spec);
174 
175  o0.unpack(a.op0_value);
176  o1.unpack(a.op1_value);
177 
178  // get actual rounding mode
179  constant_exprt rounding_mode_expr =
180  to_constant_expr(get(float_op.rounding_mode()));
181  const std::size_t rounding_mode_int =
182  numeric_cast_v<std::size_t>(rounding_mode_expr);
183  ieee_floatt::rounding_modet rounding_mode =
184  (ieee_floatt::rounding_modet)rounding_mode_int;
185 
186  ieee_floatt result=o0;
187  o0.rounding_mode=rounding_mode;
188  o1.rounding_mode=rounding_mode;
189  result.rounding_mode=rounding_mode;
190 
191  if(a.expr.id()==ID_floatbv_plus)
192  result+=o1;
193  else if(a.expr.id()==ID_floatbv_minus)
194  result-=o1;
195  else if(a.expr.id()==ID_floatbv_mult)
196  result*=o1;
197  else if(a.expr.id()==ID_floatbv_div)
198  result/=o1;
199  else
200  UNREACHABLE;
201 
202  if(result.pack()==a.result_value) // ok
203  return;
204 
205 #ifdef DEBUG
206  ieee_floatt rr(spec);
207  rr.unpack(a.result_value);
208 
209  log.debug() << "S1: " << o0 << " " << a.expr.id() << " " << o1
210  << " != " << rr << messaget::eom;
211  log.debug() << "S2: " << integer2binary(a.op0_value, spec.width()) << " "
212  << a.expr.id() << " "
213  << integer2binary(a.op1_value, spec.width())
214  << "!=" << integer2binary(a.result_value, spec.width())
215  << messaget::eom;
216  log.debug() << "S3: " << integer2binary(a.op0_value, spec.width()) << " "
217  << a.expr.id() << " "
218  << integer2binary(a.op1_value, spec.width())
219  << "==" << integer2binary(result.pack(), spec.width())
220  << messaget::eom;
221 #endif
222 
224  {
225  bvt r;
226  float_utilst float_utils(prop);
227  float_utils.spec=spec;
228  float_utils.rounding_mode_bits.set(rounding_mode);
229 
230  literalt op0_equal=
231  bv_utils.equal(a.op0_bv, float_utils.build_constant(o0));
232 
233  literalt op1_equal=
234  bv_utils.equal(a.op1_bv, float_utils.build_constant(o1));
235 
236  literalt result_equal=
237  bv_utils.equal(a.result_bv, float_utils.build_constant(result));
238 
239  literalt op0_and_op1_equal=
240  prop.land(op0_equal, op1_equal);
241 
243  prop.limplies(op0_and_op1_equal, result_equal));
244  }
245  else
246  {
247  // give up
248  // remove any previous over-approximation
249  a.over_assumptions.clear();
251 
252  bvt r;
253  float_utilst float_utils(prop);
254  float_utils.spec=spec;
255  float_utils.rounding_mode_bits.set(rounding_mode);
256 
257  bvt op0=a.op0_bv, op1=a.op1_bv, res=a.result_bv;
258 
259  if(a.expr.id()==ID_floatbv_plus)
260  r=float_utils.add(op0, op1);
261  else if(a.expr.id()==ID_floatbv_minus)
262  r=float_utils.sub(op0, op1);
263  else if(a.expr.id()==ID_floatbv_mult)
264  r=float_utils.mul(op0, op1);
265  else if(a.expr.id()==ID_floatbv_div)
266  r=float_utils.div(op0, op1);
267  else
268  UNREACHABLE;
269 
270  CHECK_RETURN(r.size()==res.size());
271  bv_utils.set_equal(r, res);
272  }
273  }
274  else if(type.id()==ID_signedbv ||
275  type.id()==ID_unsignedbv)
276  {
277  // these are all binary
278  INVARIANT(
279  a.expr.operands().size() == 2, "all (un)signedbv typed exprs are binary");
280 
281  // already full interpretation?
282  if(a.over_state>0)
283  return;
284 
285  bv_spect spec(type);
286  bv_arithmetict o0(spec), o1(spec);
287  o0.unpack(a.op0_value);
288  o1.unpack(a.op1_value);
289 
290  // division by zero is never spurious
291 
292  if((a.expr.id()==ID_div || a.expr.id()==ID_mod) &&
293  o1==0)
294  return;
295 
296  if(a.expr.id()==ID_mult)
297  o0*=o1;
298  else if(a.expr.id()==ID_div)
299  o0/=o1;
300  else if(a.expr.id()==ID_mod)
301  o0%=o1;
302  else
303  UNREACHABLE;
304 
305  if(o0.pack()==a.result_value) // ok
306  return;
307 
308  if(a.over_state==0)
309  {
310  // we give up right away and add the full interpretation
311  bvt r;
312  if(a.expr.id()==ID_mult)
313  {
315  a.op0_bv, a.op1_bv,
316  a.expr.type().id()==ID_signedbv?
319  }
320  else if(a.expr.id()==ID_div)
321  {
323  a.op0_bv, a.op1_bv,
324  a.expr.type().id()==ID_signedbv?
327  }
328  else if(a.expr.id()==ID_mod)
329  {
331  a.op0_bv, a.op1_bv,
332  a.expr.type().id()==ID_signedbv?
335  }
336  else
337  UNREACHABLE;
338 
340  }
341  else
342  UNREACHABLE;
343  }
344  else if(type.id()==ID_fixedbv)
345  {
346  // TODO: not implemented
347  TODO;
348  }
349  else
350  {
351  UNREACHABLE;
352  }
353 
354  log.status() << "Found spurious '" << a.as_string() << "' (state "
355  << a.over_state << ")" << messaget::eom;
356 
357  progress=true;
358  if(a.over_state<MAX_STATE)
359  a.over_state++;
360 }
361 
365 {
366  // part of the conflict?
367  if(!this->conflicts_with(a))
368  return;
369 
370  log.status() << "Found assumption for '" << a.as_string()
371  << "' in proof (state " << a.under_state << ")" << messaget::eom;
372 
373  PRECONDITION(!a.under_assumptions.empty());
374 
375  a.under_assumptions.clear();
376 
377  if(a.expr.type().id()==ID_floatbv)
378  {
379  const floatbv_typet &floatbv_type=to_floatbv_type(a.expr.type());
380  ieee_float_spect spec(floatbv_type);
381 
382  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
383 
384  float_utilst float_utils(prop);
385  float_utils.spec=spec;
386 
387  // the fraction without hidden bit
388  const bvt fraction0=float_utils.get_fraction(a.op0_bv);
389  const bvt fraction1=float_utils.get_fraction(a.op1_bv);
390 
391  if(a.under_state==0)
392  {
393  // we first set sign and exponent free,
394  // but keep the fraction zero
395 
396  for(std::size_t i=0; i<fraction0.size(); i++)
397  a.add_under_assumption(!fraction0[i]);
398 
399  for(std::size_t i=0; i<fraction1.size(); i++)
400  a.add_under_assumption(!fraction1[i]);
401  }
402  else
403  {
404  // now fraction: make this grow quadratically
405  unsigned x=a.under_state*a.under_state;
406 
407  if(x>=MAX_FLOAT_UNDERAPPROX && x>=a.result_bv.size())
408  {
409  // make it free altogether, this guarantees progress
410  }
411  else
412  {
413  // set x bits of both exponent and mantissa free
414  // need to start with most-significant bits
415 
416  #if 0
417  for(std::size_t i=x; i<fraction0.size(); i++)
418  a.add_under_assumption(!fraction0[fraction0.size()-i-1]);
419 
420  for(std::size_t i=x; i<fraction1.size(); i++)
421  a.add_under_assumption(!fraction1[fraction1.size()-i-1]);
422  #endif
423  }
424  }
425  }
426  else
427  {
428  unsigned x=a.under_state+1;
429 
430  if(x>=MAX_INTEGER_UNDERAPPROX && x>=a.result_bv.size())
431  {
432  // make it free altogether, this guarantees progress
433  }
434  else
435  {
436  // set x least-significant bits free
437  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
438 
439  for(std::size_t i=x; i<a.op0_bv.size(); i++)
440  a.add_under_assumption(!a.op0_bv[i]);
441 
442  for(std::size_t i=x; i<a.op1_bv.size(); i++)
443  a.add_under_assumption(!a.op1_bv[i]);
444  }
445  }
446 
447  a.under_state++;
448  progress=true;
449 }
450 
453 {
454  for(std::size_t i=0; i<a.under_assumptions.size(); i++)
455  {
456  if(prop.is_in_conflict(
458  {
459  return true;
460  }
461  }
462 
463  return false;
464 }
465 
467 {
468  a.over_state=a.under_state=0;
469 
470  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
471 
472  // initially, we force the operands to be all zero
473 
474  for(std::size_t i=0; i<a.op0_bv.size(); i++)
475  a.add_under_assumption(!a.op0_bv[i]);
476 
477  for(std::size_t i=0; i<a.op1_bv.size(); i++)
478  a.add_under_assumption(!a.op1_bv[i]);
479 }
480 
483  const exprt &expr, bvt &bv)
484 {
485  approximations.push_back(approximationt(approximations.size()));
486  approximationt &a=approximations.back();
487 
488  std::size_t width=boolbv_width(expr.type());
489  PRECONDITION(width!=0);
490 
491  a.expr=expr;
492  a.result_bv=prop.new_variables(width);
493  a.no_operands=expr.operands().size();
495 
496  if(a.no_operands==1)
497  {
498  a.op0_bv = convert_bv(to_unary_expr(expr).op());
499  set_frozen(a.op0_bv);
500  }
501  else if(a.no_operands==2)
502  {
503  a.op0_bv = convert_bv(to_binary_expr(expr).op0());
504  a.op1_bv = convert_bv(to_binary_expr(expr).op1());
505  set_frozen(a.op0_bv);
506  set_frozen(a.op1_bv);
507  }
508  else if(a.no_operands==3)
509  {
510  a.op0_bv = convert_bv(to_multi_ary_expr(expr).op0());
511  a.op1_bv = convert_bv(to_multi_ary_expr(expr).op1());
512  a.op2_bv = convert_bv(to_multi_ary_expr(expr).op2());
513  set_frozen(a.op0_bv);
514  set_frozen(a.op1_bv);
515  set_frozen(a.op2_bv);
516  }
517  else
518  UNREACHABLE;
519 
520  bv=a.result_bv;
521 
522  initialize(a);
523 
524  return a;
525 }
526 
528 {
529  return std::to_string(id_nr)+"/"+id2string(expr.id());
530 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
bv_refinementt::convert_div
bvt convert_div(const div_exprt &expr) override
Definition: refine_arithmetic.cpp:98
bv_refinementt::configt::max_node_refinement
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:26
ieee_floatt
Definition: ieee_float.h:120
bv_refinementt::conflicts_with
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
Definition: refine_arithmetic.cpp:452
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
literal_exprt::get_literal
literalt get_literal() const
Definition: literal_expr.h:26
float_utilst::rounding_mode_bits
rounding_mode_bitst rounding_mode_bits
Definition: float_utils.h:67
arith_tools.h
arrayst::log
messaget log
Definition: arrays.h:55
propt::new_variables
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
bv_refinementt::approximationt::expr
exprt expr
Definition: bv_refinement.h:73
TODO
#define TODO
Definition: invariant.h:522
bv_refinementt::approximationt::over_assumptions
std::vector< exprt > over_assumptions
Definition: bv_refinement.h:80
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
float_utilst
Definition: float_utils.h:18
typet
The type of an expression, extends irept.
Definition: type.h:28
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
messaget::status
mstreamt & status() const
Definition: message.h:414
bv_refinementt::add_approximation
approximationt & add_approximation(const exprt &expr, bvt &bv)
Definition: refine_arithmetic.cpp:482
bv_pointerst::boolbv_width
std::size_t boolbv_width(const typet &type) const override
Definition: bv_pointers.h:29
bv_arithmetict::unpack
void unpack(const mp_integer &i)
Definition: bv_arithmetic.h:118
float_utilst::sub
bvt sub(const bvt &src1, const bvt &src2)
Definition: float_utils.h:116
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1386
bv_refinement.h
Abstraction Refinement Loop.
ieee_floatt::unpack
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:315
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
bv_refinementt::check_SAT
void check_SAT()
Definition: bv_refinement_loop.cpp:120
bv_utilst::set_equal
void set_equal(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:33
bv_refinementt::configt::refine_arithmetic
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:30
float_utilst::add
bvt add(const bvt &src1, const bvt &src2)
Definition: float_utils.h:111
exprt
Base class for all expressions.
Definition: expr.h:54
bv_arithmetic.h
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
bv_refinementt::approximationt::op1_bv
bvt op1_bv
Definition: bv_refinement.h:76
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:37
div_exprt
Division.
Definition: std_expr.h:981
propt::land
virtual literalt land(literalt a, literalt b)=0
to_literal_expr
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:44
ieee_float_spect
Definition: ieee_float.h:26
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
bv_refinementt::convert_mult
bvt convert_mult(const mult_exprt &expr) override
Definition: refine_arithmetic.cpp:50
bv_refinementt::approximations
std::list< approximationt > approximations
Definition: bv_refinement.h:108
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
prop_conv_solvert::set_frozen
void set_frozen(literalt)
Definition: prop_conv_solver.cpp:28
bv_refinementt::initialize
void initialize(approximationt &approximation)
Definition: refine_arithmetic.cpp:466
bv_refinementt::approximationt::add_under_assumption
void add_under_assumption(literalt l)
Definition: refine_arithmetic.cpp:30
ieee_float_spect::width
std::size_t width() const
Definition: ieee_float.h:54
bv_spect
Definition: bv_arithmetic.h:23
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:961
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
bv_refinementt::approximationt::add_over_assumption
void add_over_assumption(literalt l)
Definition: refine_arithmetic.cpp:23
bv_refinementt::approximationt
Definition: bv_refinement.h:63
bv_utilst::representationt::SIGNED
@ SIGNED
bv_refinementt::approximationt::op2_value
mp_integer op2_value
Definition: bv_refinement.h:77
float_utilst::div
virtual bvt div(const bvt &src1, const bvt &src2)
Definition: float_utils.cpp:460
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
literal_exprt
Definition: literal_expr.h:18
float_utilst::build_constant
bvt build_constant(const ieee_floatt &)
Definition: float_utils.cpp:139
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:936
ieee_floatt::pack
mp_integer pack() const
Definition: ieee_float.cpp:370
MAX_STATE
#define MAX_STATE
Definition: bv_refinement.h:17
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
bv_refinementt::check_UNSAT
void check_UNSAT()
Definition: bv_refinement_loop.cpp:134
floatbv_expr.h
API to expression classes for floating-point arithmetic.
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:126
bv_refinementt::approximationt::op0_value
mp_integer op0_value
Definition: bv_refinement.h:77
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:38
bv_refinementt::approximationt::result_bv
bvt result_bv
Definition: bv_refinement.h:76
bv_refinementt::progress
bool progress
Definition: bv_refinement.h:107
MAX_FLOAT_UNDERAPPROX
#define MAX_FLOAT_UNDERAPPROX
Definition: refine_arithmetic.cpp:21
boolbvt::get_value
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:84
propt::is_in_conflict
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
bv_refinementt::approximationt::over_state
unsigned over_state
Definition: bv_refinement.h:83
ieee_floatt::rounding_mode
rounding_modet rounding_mode
Definition: ieee_float.h:132
bv_refinementt::convert_mod
bvt convert_mod(const mod_exprt &expr) override
Definition: refine_arithmetic.cpp:116
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
bv_utilst::remainder
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:94
expr_util.h
Deprecated expression utility functions.
bv_refinementt::config_
configt config_
Definition: bv_refinement.h:112
float_utilst::get_fraction
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition: float_utils.cpp:684
bv_refinementt::get_values
void get_values(approximationt &approximation)
Definition: refine_arithmetic.cpp:134
bv_refinementt::approximationt::op2_bv
bvt op2_bv
Definition: bv_refinement.h:76
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:109
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
bv_refinementt::convert_floatbv_op
bvt convert_floatbv_op(const ieee_float_op_exprt &) override
Definition: refine_arithmetic.cpp:37
literalt
Definition: literal.h:26
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
float_utilst::rounding_mode_bitst::set
void set(const ieee_floatt::rounding_modet mode)
Definition: float_utils.h:37
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:808
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
MAX_INTEGER_UNDERAPPROX
#define MAX_INTEGER_UNDERAPPROX
Definition: refine_arithmetic.cpp:20
exprt::operands
operandst & operands()
Definition: expr.h:96
r
static int8_t r
Definition: irep_hash.h:59
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
messaget::debug
mstreamt & debug() const
Definition: message.h:429
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
bv_refinementt::approximationt::under_state
unsigned under_state
Definition: bv_refinement.h:83
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1111
bv_utilst::is_zero
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
bv_refinementt::approximationt::op1_value
mp_integer op1_value
Definition: bv_refinement.h:77
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:30
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
bv_arithmetict
Definition: bv_arithmetic.h:51
bv_refinementt::approximationt::no_operands
std::size_t no_operands
Definition: bv_refinement.h:74
bv_refinementt::approximationt::op0_bv
bvt op0_bv
Definition: bv_refinement.h:76
bv_refinementt::approximationt::result_value
mp_integer result_value
Definition: bv_refinement.h:77
bv_utilst::is_one
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:24
float_utilst::spec
ieee_float_spect spec
Definition: float_utils.h:88
boolbvt::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:20
float_utilst::mul
virtual bvt mul(const bvt &src1, const bvt &src2)
Definition: float_utils.cpp:408
bv_refinementt::approximationt::under_assumptions
std::vector< exprt > under_assumptions
Definition: bv_refinement.h:79
mod_exprt
Modulo.
Definition: std_expr.h:1050
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128
bv_refinementt::approximationt::as_string
std::string as_string() const
Definition: refine_arithmetic.cpp:527
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701