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/bitvector_types.h>
13 #include <util/bv_arithmetic.h>
14 #include <util/expr_util.h>
15 #include <util/floatbv_expr.h>
16 #include <util/ieee_float.h>
17 
19 
20 // Parameters
21 #define MAX_INTEGER_UNDERAPPROX 3
22 #define MAX_FLOAT_UNDERAPPROX 10
23 
25 {
26  // if it's a constant already, give up
27  if(!l.is_constant())
28  over_assumptions.push_back(literal_exprt(l));
29 }
30 
32 {
33  // if it's a constant already, give up
34  if(!l.is_constant())
35  under_assumptions.push_back(literal_exprt(l));
36 }
37 
39 {
41  return SUB::convert_floatbv_op(expr);
42 
43  if(expr.type().id() != ID_floatbv)
44  return SUB::convert_floatbv_op(expr);
45 
46  bvt bv;
47  add_approximation(expr, bv);
48  return bv;
49 }
50 
52 {
53  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
54  return SUB::convert_mult(expr);
55 
56  // we catch any multiplication
57  // unless it involves a constant
58 
59  const exprt::operandst &operands=expr.operands();
60 
61  const typet &type = expr.type();
62 
63  PRECONDITION(operands.size()>=2);
64 
65  if(operands.size()>2)
66  return convert_mult(to_mult_expr(make_binary(expr))); // make binary
67 
68  // we keep multiplication by a constant for integers
69  if(type.id()!=ID_floatbv)
70  if(operands[0].is_constant() || operands[1].is_constant())
71  return SUB::convert_mult(expr);
72 
73  bvt bv;
74  approximationt &a=add_approximation(expr, bv);
75 
76  // initially, we have a partial interpretation for integers
77  if(type.id()==ID_signedbv ||
78  type.id()==ID_unsignedbv)
79  {
80  // x*0==0 and 0*x==0
81  literalt op0_zero=bv_utils.is_zero(a.op0_bv);
82  literalt op1_zero=bv_utils.is_zero(a.op1_bv);
83  literalt res_zero=bv_utils.is_zero(a.result_bv);
85  prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));
86 
87  // x*1==x and 1*x==x
88  literalt op0_one=bv_utils.is_one(a.op0_bv);
89  literalt op1_one=bv_utils.is_one(a.op1_bv);
90  literalt res_op0=bv_utils.equal(a.op0_bv, a.result_bv);
91  literalt res_op1=bv_utils.equal(a.op1_bv, a.result_bv);
92  prop.l_set_to_true(prop.limplies(op0_one, res_op1));
93  prop.l_set_to_true(prop.limplies(op1_one, res_op0));
94  }
95 
96  return bv;
97 }
98 
100 {
101  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
102  return SUB::convert_div(expr);
103 
104  // we catch any division
105  // unless it's integer division by a constant
106 
107  PRECONDITION(expr.operands().size()==2);
108 
109  if(expr.op1().is_constant())
110  return SUB::convert_div(expr);
111 
112  bvt bv;
113  add_approximation(expr, bv);
114  return bv;
115 }
116 
118 {
119  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
120  return SUB::convert_mod(expr);
121 
122  // we catch any mod
123  // unless it's integer + constant
124 
125  PRECONDITION(expr.operands().size()==2);
126 
127  if(expr.op1().is_constant())
128  return SUB::convert_mod(expr);
129 
130  bvt bv;
131  add_approximation(expr, bv);
132  return bv;
133 }
134 
136 {
137  std::size_t o=a.expr.operands().size();
138 
139  if(o==1)
141  else if(o==2)
142  {
145  }
146  else if(o==3)
147  {
151  }
152  else
153  UNREACHABLE;
154 
156 }
157 
161 {
162  // see if the satisfying assignment is spurious in any way
163 
164  const typet &type = a.expr.type();
165 
166  if(type.id()==ID_floatbv)
167  {
168  const auto &float_op = to_ieee_float_op_expr(a.expr);
169 
170  if(a.over_state==MAX_STATE)
171  return;
172 
173  ieee_float_spect spec(to_floatbv_type(type));
174  ieee_floatt o0(spec), o1(spec);
175 
176  o0.unpack(a.op0_value);
177  o1.unpack(a.op1_value);
178 
179  // get actual rounding mode
180  constant_exprt rounding_mode_expr =
181  to_constant_expr(get(float_op.rounding_mode()));
182  const std::size_t rounding_mode_int =
183  numeric_cast_v<std::size_t>(rounding_mode_expr);
184  ieee_floatt::rounding_modet rounding_mode =
185  (ieee_floatt::rounding_modet)rounding_mode_int;
186 
187  ieee_floatt result=o0;
188  o0.rounding_mode=rounding_mode;
189  o1.rounding_mode=rounding_mode;
190  result.rounding_mode=rounding_mode;
191 
192  if(a.expr.id()==ID_floatbv_plus)
193  result+=o1;
194  else if(a.expr.id()==ID_floatbv_minus)
195  result-=o1;
196  else if(a.expr.id()==ID_floatbv_mult)
197  result*=o1;
198  else if(a.expr.id()==ID_floatbv_div)
199  result/=o1;
200  else
201  UNREACHABLE;
202 
203  if(result.pack()==a.result_value) // ok
204  return;
205 
206 #ifdef DEBUG
207  ieee_floatt rr(spec);
208  rr.unpack(a.result_value);
209 
210  log.debug() << "S1: " << o0 << " " << a.expr.id() << " " << o1
211  << " != " << rr << messaget::eom;
212  log.debug() << "S2: " << integer2binary(a.op0_value, spec.width()) << " "
213  << a.expr.id() << " "
214  << integer2binary(a.op1_value, spec.width())
215  << "!=" << integer2binary(a.result_value, spec.width())
216  << messaget::eom;
217  log.debug() << "S3: " << integer2binary(a.op0_value, spec.width()) << " "
218  << a.expr.id() << " "
219  << integer2binary(a.op1_value, spec.width())
220  << "==" << integer2binary(result.pack(), spec.width())
221  << messaget::eom;
222 #endif
223 
225  {
226  bvt r;
227  float_utilst float_utils(prop);
228  float_utils.spec=spec;
229  float_utils.rounding_mode_bits.set(rounding_mode);
230 
231  literalt op0_equal=
232  bv_utils.equal(a.op0_bv, float_utils.build_constant(o0));
233 
234  literalt op1_equal=
235  bv_utils.equal(a.op1_bv, float_utils.build_constant(o1));
236 
237  literalt result_equal=
238  bv_utils.equal(a.result_bv, float_utils.build_constant(result));
239 
240  literalt op0_and_op1_equal=
241  prop.land(op0_equal, op1_equal);
242 
244  prop.limplies(op0_and_op1_equal, result_equal));
245  }
246  else
247  {
248  // give up
249  // remove any previous over-approximation
250  a.over_assumptions.clear();
252 
253  bvt r;
254  float_utilst float_utils(prop);
255  float_utils.spec=spec;
256  float_utils.rounding_mode_bits.set(rounding_mode);
257 
258  bvt op0=a.op0_bv, op1=a.op1_bv, res=a.result_bv;
259 
260  if(a.expr.id()==ID_floatbv_plus)
261  r=float_utils.add(op0, op1);
262  else if(a.expr.id()==ID_floatbv_minus)
263  r=float_utils.sub(op0, op1);
264  else if(a.expr.id()==ID_floatbv_mult)
265  r=float_utils.mul(op0, op1);
266  else if(a.expr.id()==ID_floatbv_div)
267  r=float_utils.div(op0, op1);
268  else
269  UNREACHABLE;
270 
271  CHECK_RETURN(r.size()==res.size());
272  bv_utils.set_equal(r, res);
273  }
274  }
275  else if(type.id()==ID_signedbv ||
276  type.id()==ID_unsignedbv)
277  {
278  // these are all binary
279  INVARIANT(
280  a.expr.operands().size() == 2, "all (un)signedbv typed exprs are binary");
281 
282  // already full interpretation?
283  if(a.over_state>0)
284  return;
285 
286  bv_spect spec(type);
287  bv_arithmetict o0(spec), o1(spec);
288  o0.unpack(a.op0_value);
289  o1.unpack(a.op1_value);
290 
291  // division by zero is never spurious
292 
293  if((a.expr.id()==ID_div || a.expr.id()==ID_mod) &&
294  o1==0)
295  return;
296 
297  if(a.expr.id()==ID_mult)
298  o0*=o1;
299  else if(a.expr.id()==ID_div)
300  o0/=o1;
301  else if(a.expr.id()==ID_mod)
302  o0%=o1;
303  else
304  UNREACHABLE;
305 
306  if(o0.pack()==a.result_value) // ok
307  return;
308 
309  if(a.over_state==0)
310  {
311  // we give up right away and add the full interpretation
312  bvt r;
313  if(a.expr.id()==ID_mult)
314  {
316  a.op0_bv, a.op1_bv,
317  a.expr.type().id()==ID_signedbv?
320  }
321  else if(a.expr.id()==ID_div)
322  {
324  a.op0_bv, a.op1_bv,
325  a.expr.type().id()==ID_signedbv?
328  }
329  else if(a.expr.id()==ID_mod)
330  {
332  a.op0_bv, a.op1_bv,
333  a.expr.type().id()==ID_signedbv?
336  }
337  else
338  UNREACHABLE;
339 
341  }
342  else
343  UNREACHABLE;
344  }
345  else if(type.id()==ID_fixedbv)
346  {
347  // TODO: not implemented
348  TODO;
349  }
350  else
351  {
352  UNREACHABLE;
353  }
354 
355  log.status() << "Found spurious '" << a.as_string() << "' (state "
356  << a.over_state << ")" << messaget::eom;
357 
358  progress=true;
359  if(a.over_state<MAX_STATE)
360  a.over_state++;
361 }
362 
366 {
367  // part of the conflict?
368  if(!this->conflicts_with(a))
369  return;
370 
371  log.status() << "Found assumption for '" << a.as_string()
372  << "' in proof (state " << a.under_state << ")" << messaget::eom;
373 
374  PRECONDITION(!a.under_assumptions.empty());
375 
376  a.under_assumptions.clear();
377 
378  if(a.expr.type().id()==ID_floatbv)
379  {
380  const floatbv_typet &floatbv_type=to_floatbv_type(a.expr.type());
381  ieee_float_spect spec(floatbv_type);
382 
383  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
384 
385  float_utilst float_utils(prop);
386  float_utils.spec=spec;
387 
388  // the fraction without hidden bit
389  const bvt fraction0=float_utils.get_fraction(a.op0_bv);
390  const bvt fraction1=float_utils.get_fraction(a.op1_bv);
391 
392  if(a.under_state==0)
393  {
394  // we first set sign and exponent free,
395  // but keep the fraction zero
396 
397  for(std::size_t i=0; i<fraction0.size(); i++)
398  a.add_under_assumption(!fraction0[i]);
399 
400  for(std::size_t i=0; i<fraction1.size(); i++)
401  a.add_under_assumption(!fraction1[i]);
402  }
403  else
404  {
405  // now fraction: make this grow quadratically
406  unsigned x=a.under_state*a.under_state;
407 
408  if(x>=MAX_FLOAT_UNDERAPPROX && x>=a.result_bv.size())
409  {
410  // make it free altogether, this guarantees progress
411  }
412  else
413  {
414  // set x bits of both exponent and mantissa free
415  // need to start with most-significant bits
416 
417  #if 0
418  for(std::size_t i=x; i<fraction0.size(); i++)
419  a.add_under_assumption(!fraction0[fraction0.size()-i-1]);
420 
421  for(std::size_t i=x; i<fraction1.size(); i++)
422  a.add_under_assumption(!fraction1[fraction1.size()-i-1]);
423  #endif
424  }
425  }
426  }
427  else
428  {
429  unsigned x=a.under_state+1;
430 
431  if(x>=MAX_INTEGER_UNDERAPPROX && x>=a.result_bv.size())
432  {
433  // make it free altogether, this guarantees progress
434  }
435  else
436  {
437  // set x least-significant bits free
438  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
439 
440  for(std::size_t i=x; i<a.op0_bv.size(); i++)
441  a.add_under_assumption(!a.op0_bv[i]);
442 
443  for(std::size_t i=x; i<a.op1_bv.size(); i++)
444  a.add_under_assumption(!a.op1_bv[i]);
445  }
446  }
447 
448  a.under_state++;
449  progress=true;
450 }
451 
454 {
455  for(std::size_t i=0; i<a.under_assumptions.size(); i++)
456  {
457  if(prop.is_in_conflict(
459  {
460  return true;
461  }
462  }
463 
464  return false;
465 }
466 
468 {
469  a.over_state=a.under_state=0;
470 
471  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
472 
473  // initially, we force the operands to be all zero
474 
475  for(std::size_t i=0; i<a.op0_bv.size(); i++)
476  a.add_under_assumption(!a.op0_bv[i]);
477 
478  for(std::size_t i=0; i<a.op1_bv.size(); i++)
479  a.add_under_assumption(!a.op1_bv[i]);
480 }
481 
484  const exprt &expr, bvt &bv)
485 {
486  approximations.push_back(approximationt(approximations.size()));
487  approximationt &a=approximations.back();
488 
489  std::size_t width=boolbv_width(expr.type());
490  PRECONDITION(width!=0);
491 
492  a.expr=expr;
493  a.result_bv=prop.new_variables(width);
494  a.no_operands=expr.operands().size();
496 
497  if(a.no_operands==1)
498  {
499  a.op0_bv = convert_bv(to_unary_expr(expr).op());
500  set_frozen(a.op0_bv);
501  }
502  else if(a.no_operands==2)
503  {
504  a.op0_bv = convert_bv(to_binary_expr(expr).op0());
505  a.op1_bv = convert_bv(to_binary_expr(expr).op1());
506  set_frozen(a.op0_bv);
507  set_frozen(a.op1_bv);
508  }
509  else if(a.no_operands==3)
510  {
511  a.op0_bv = convert_bv(to_multi_ary_expr(expr).op0());
512  a.op1_bv = convert_bv(to_multi_ary_expr(expr).op1());
513  a.op2_bv = convert_bv(to_multi_ary_expr(expr).op2());
514  set_frozen(a.op0_bv);
515  set_frozen(a.op1_bv);
516  set_frozen(a.op2_bv);
517  }
518  else
519  UNREACHABLE;
520 
521  bv=a.result_bv;
522 
523  initialize(a);
524 
525  return a;
526 }
527 
529 {
530  return std::to_string(id_nr)+"/"+id2string(expr.id());
531 }
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:99
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:453
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
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
virtual 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
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
bv_refinementt::add_approximation
approximationt & add_approximation(const exprt &expr, bvt &bv)
Definition: refine_arithmetic.cpp:483
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: bitvector_types.h:322
bv_refinement.h
Abstraction Refinement Loop.
ieee_floatt::unpack
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:316
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:38
div_exprt
Division.
Definition: std_expr.h:980
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:627
bv_refinementt::convert_mult
bvt convert_mult(const mult_exprt &expr) override
Definition: refine_arithmetic.cpp:51
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:467
bv_refinementt::approximationt::add_under_assumption
void add_under_assumption(literalt l)
Definition: refine_arithmetic.cpp:31
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:960
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:24
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
bitvector_types.h
Pre-defined bitvector types.
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:935
ieee_floatt::pack
mp_integer pack() const
Definition: ieee_float.cpp:371
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:47
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:22
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:117
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:135
bv_refinementt::approximationt::op2_bv
bvt op2_bv
Definition: bv_refinement.h:76
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:111
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
bv_refinementt::convert_floatbv_op
bvt convert_floatbv_op(const ieee_float_op_exprt &) override
Definition: refine_arithmetic.cpp:38
literalt
Definition: literal.h:26
bv_utilst::divider
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
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:21
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:1105
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:2667
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:29
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:815
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:1049
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:528
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700