cprover
boolbv_typecast.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 "boolbv.h"
10 
11 #include <cassert>
12 
13 #include <util/std_types.h>
14 
16 
17 #include "boolbv_type.h"
19 
21 {
22  const exprt &op=expr.op();
23  const bvt &op_bv=convert_bv(op);
24 
25  bvt bv;
26 
27  if(type_conversion(op.type(), op_bv, expr.type(), bv))
28  return conversion_failed(expr);
29 
30  return bv;
31 }
32 
34  const typet &src_type, const bvt &src,
35  const typet &dest_type, bvt &dest)
36 {
37  bvtypet dest_bvtype=get_bvtype(dest_type);
38  bvtypet src_bvtype=get_bvtype(src_type);
39 
40  if(src_bvtype==bvtypet::IS_C_BIT_FIELD)
41  return
44  src,
45  dest_type,
46  dest);
47 
48  if(dest_bvtype==bvtypet::IS_C_BIT_FIELD)
49  return
51  src_type,
52  src,
54  dest);
55 
56  std::size_t src_width=src.size();
57  std::size_t dest_width=boolbv_width(dest_type);
58 
59  if(dest_width==0 || src_width==0)
60  return true;
61 
62  dest.clear();
63  dest.reserve(dest_width);
64 
65  if(dest_type.id()==ID_complex)
66  {
67  if(src_type==dest_type.subtype())
68  {
69  forall_literals(it, src)
70  dest.push_back(*it);
71 
72  // pad with zeros
73  for(std::size_t i=src.size(); i<dest_width; i++)
74  dest.push_back(const_literal(false));
75 
76  return false;
77  }
78  else if(src_type.id()==ID_complex)
79  {
80  // recursively do both halfs
81  bvt lower, upper, lower_res, upper_res;
82  lower.assign(src.begin(), src.begin()+src.size()/2);
83  upper.assign(src.begin()+src.size()/2, src.end());
85  src_type.subtype(), lower, dest_type.subtype(), lower_res);
87  src_type.subtype(), upper, dest_type.subtype(), upper_res);
88  INVARIANT(
89  lower_res.size() + upper_res.size() == dest_width,
90  "lower result bitvector size plus upper result bitvector size shall "
91  "equal the destination bitvector size");
92  dest=lower_res;
93  dest.insert(dest.end(), upper_res.begin(), upper_res.end());
94  return false;
95  }
96  }
97 
98  if(src_type.id()==ID_complex)
99  {
100  INVARIANT(
101  dest_type.id() == ID_complex,
102  "destination type shall be of complex type when source type is of "
103  "complex type");
104  if(dest_type.id()==ID_signedbv ||
105  dest_type.id()==ID_unsignedbv ||
106  dest_type.id()==ID_floatbv ||
107  dest_type.id()==ID_fixedbv ||
108  dest_type.id()==ID_c_enum ||
109  dest_type.id()==ID_c_enum_tag ||
110  dest_type.id()==ID_bool)
111  {
112  // A cast from complex x to real T
113  // is (T) __real__ x.
114  bvt tmp_src(src);
115  tmp_src.resize(src.size()/2); // cut off imag part
116  return type_conversion(src_type.subtype(), tmp_src, dest_type, dest);
117  }
118  }
119 
120  switch(dest_bvtype)
121  {
122  case bvtypet::IS_RANGE:
123  if(src_bvtype==bvtypet::IS_UNSIGNED ||
124  src_bvtype==bvtypet::IS_SIGNED ||
125  src_bvtype==bvtypet::IS_C_BOOL)
126  {
127  mp_integer dest_from=to_range_type(dest_type).get_from();
128 
129  if(dest_from==0)
130  {
131  // do zero extension
132  dest.resize(dest_width);
133  for(std::size_t i=0; i<dest.size(); i++)
134  dest[i]=(i<src.size()?src[i]:const_literal(false));
135 
136  return false;
137  }
138  }
139  else if(src_bvtype==bvtypet::IS_RANGE) // range to range
140  {
141  mp_integer src_from=to_range_type(src_type).get_from();
142  mp_integer dest_from=to_range_type(dest_type).get_from();
143 
144  if(dest_from==src_from)
145  {
146  // do zero extension, if needed
147  dest=bv_utils.zero_extension(src, dest_width);
148  return false;
149  }
150  else
151  {
152  // need to do arithmetic: add src_from-dest_from
153  mp_integer offset=src_from-dest_from;
154  dest=
155  bv_utils.add(
156  bv_utils.zero_extension(src, dest_width),
157  bv_utils.build_constant(offset, dest_width));
158  }
159 
160  return false;
161  }
162  break;
163 
164  case bvtypet::IS_FLOAT: // to float
165  {
166  float_utilst float_utils(prop);
167 
168  switch(src_bvtype)
169  {
170  case bvtypet::IS_FLOAT: // float to float
171  // we don't have a rounding mode here,
172  // which is why we refuse.
173  break;
174 
175  case bvtypet::IS_SIGNED: // signed to float
176  case bvtypet::IS_C_ENUM:
177  float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
178  dest=float_utils.from_signed_integer(src);
179  return false;
180 
181  case bvtypet::IS_UNSIGNED: // unsigned to float
182  case bvtypet::IS_C_BOOL: // _Bool to float
183  float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
184  dest=float_utils.from_unsigned_integer(src);
185  return false;
186 
187  case bvtypet::IS_BV:
188  INVARIANT(
189  src_width == dest_width,
190  "source bitvector size shall equal the destination bitvector size");
191  dest=src;
192  return false;
193 
195  case bvtypet::IS_UNKNOWN:
196  case bvtypet::IS_RANGE:
199  case bvtypet::IS_FIXED:
200  if(src_type.id()==ID_bool)
201  {
202  // bool to float
203 
204  // build a one
205  ieee_floatt f(to_floatbv_type(dest_type));
206  f.from_integer(1);
207 
208  dest=convert_bv(f.to_expr());
209 
210  INVARIANT(
211  src_width == 1, "bitvector of type boolean shall have width one");
212 
213  Forall_literals(it, dest)
214  *it=prop.land(*it, src[0]);
215 
216  return false;
217  }
218  }
219  }
220  break;
221 
222  case bvtypet::IS_FIXED:
223  if(src_bvtype==bvtypet::IS_FIXED)
224  {
225  // fixed to fixed
226 
227  std::size_t dest_fraction_bits=
228  to_fixedbv_type(dest_type).get_fraction_bits();
229  std::size_t dest_int_bits=dest_width-dest_fraction_bits;
230  std::size_t op_fraction_bits=
232  std::size_t op_int_bits=src_width-op_fraction_bits;
233 
234  dest.resize(dest_width);
235 
236  // i == position after dot
237  // i == 0: first position after dot
238 
239  for(std::size_t i=0; i<dest_fraction_bits; i++)
240  {
241  // position in bv
242  std::size_t p=dest_fraction_bits-i-1;
243 
244  if(i<op_fraction_bits)
245  dest[p]=src[op_fraction_bits-i-1];
246  else
247  dest[p]=const_literal(false); // zero padding
248  }
249 
250  for(std::size_t i=0; i<dest_int_bits; i++)
251  {
252  // position in bv
253  std::size_t p=dest_fraction_bits+i;
254  INVARIANT(p < dest_width, "bit index shall be within bounds");
255 
256  if(i<op_int_bits)
257  dest[p]=src[i+op_fraction_bits];
258  else
259  dest[p]=src[src_width-1]; // sign extension
260  }
261 
262  return false;
263  }
264  else if(src_bvtype==bvtypet::IS_BV)
265  {
266  INVARIANT(
267  src_width == dest_width,
268  "source bitvector width shall equal the destination bitvector width");
269  dest=src;
270  return false;
271  }
272  else if(src_bvtype==bvtypet::IS_UNSIGNED ||
273  src_bvtype==bvtypet::IS_SIGNED ||
274  src_bvtype==bvtypet::IS_C_BOOL ||
275  src_bvtype==bvtypet::IS_C_ENUM)
276  {
277  // integer to fixed
278 
279  std::size_t dest_fraction_bits=
280  to_fixedbv_type(dest_type).get_fraction_bits();
281 
282  for(std::size_t i=0; i<dest_fraction_bits; i++)
283  dest.push_back(const_literal(false)); // zero padding
284 
285  for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
286  {
287  literalt l;
288 
289  if(i<src_width)
290  l=src[i];
291  else
292  {
293  if(src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM)
294  l=src[src_width-1]; // sign extension
295  else
296  l=const_literal(false); // zero extension
297  }
298 
299  dest.push_back(l);
300  }
301 
302  return false;
303  }
304  else if(src_type.id()==ID_bool)
305  {
306  // bool to fixed
307  std::size_t fraction_bits=
308  to_fixedbv_type(dest_type).get_fraction_bits();
309 
310  INVARIANT(
311  src_width == 1, "bitvector of type boolean shall have width one");
312 
313  for(std::size_t i=0; i<dest_width; i++)
314  {
315  if(i==fraction_bits)
316  dest.push_back(src[0]);
317  else
318  dest.push_back(const_literal(false));
319  }
320 
321  return false;
322  }
323  break;
324 
326  case bvtypet::IS_SIGNED:
327  case bvtypet::IS_C_ENUM:
328  switch(src_bvtype)
329  {
330  case bvtypet::IS_FLOAT: // float to integer
331  // we don't have a rounding mode here,
332  // which is why we refuse.
333  break;
334 
335  case bvtypet::IS_FIXED: // fixed to integer
336  {
337  std::size_t op_fraction_bits=
339 
340  for(std::size_t i=0; i<dest_width; i++)
341  {
342  if(i<src_width-op_fraction_bits)
343  dest.push_back(src[i+op_fraction_bits]);
344  else
345  {
346  if(dest_bvtype==bvtypet::IS_SIGNED)
347  dest.push_back(src[src_width-1]); // sign extension
348  else
349  dest.push_back(const_literal(false)); // zero extension
350  }
351  }
352 
353  // we might need to round up in case of negative numbers
354  // e.g., (int)(-1.00001)==1
355 
356  bvt fraction_bits_bv=src;
357  fraction_bits_bv.resize(op_fraction_bits);
358  literalt round_up=
359  prop.land(prop.lor(fraction_bits_bv), src.back());
360 
361  dest=bv_utils.incrementer(dest, round_up);
362 
363  return false;
364  }
365 
366  case bvtypet::IS_UNSIGNED: // integer to integer
367  case bvtypet::IS_SIGNED:
368  case bvtypet::IS_C_ENUM:
369  case bvtypet::IS_C_BOOL:
370  {
371  // We do sign extension for any source type
372  // that is signed, independently of the
373  // destination type.
374  // E.g., ((short)(ulong)(short)-1)==-1
375  bool sign_extension=
376  src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM;
377 
378  for(std::size_t i=0; i<dest_width; i++)
379  {
380  if(i<src_width)
381  dest.push_back(src[i]);
382  else if(sign_extension)
383  dest.push_back(src[src_width-1]); // sign extension
384  else
385  dest.push_back(const_literal(false));
386  }
387 
388  return false;
389  }
390  // verilog_unsignedbv to signed/unsigned/enum
392  {
393  for(std::size_t i=0; i<dest_width; i++)
394  {
395  std::size_t src_index=i*2; // we take every second bit
396 
397  if(src_index<src_width)
398  dest.push_back(src[src_index]);
399  else // always zero-extend
400  dest.push_back(const_literal(false));
401  }
402 
403  return false;
404  }
405  break;
406 
407  case bvtypet::IS_VERILOG_SIGNED: // verilog_signedbv to signed/unsigned/enum
408  {
409  for(std::size_t i=0; i<dest_width; i++)
410  {
411  std::size_t src_index=i*2; // we take every second bit
412 
413  if(src_index<src_width)
414  dest.push_back(src[src_index]);
415  else // always sign-extend
416  dest.push_back(src.back());
417  }
418 
419  return false;
420  }
421  break;
422 
423  case bvtypet::IS_BV:
424  INVARIANT(
425  src_width == dest_width,
426  "source bitvector width shall equal the destination bitvector width");
427  dest = src;
428  return false;
429 
430  case bvtypet::IS_RANGE:
432  case bvtypet::IS_UNKNOWN:
433  if(src_type.id() == ID_bool)
434  {
435  // bool to integer
436 
437  INVARIANT(
438  src_width == 1, "bitvector of type boolean shall have width one");
439 
440  for(std::size_t i = 0; i < dest_width; i++)
441  {
442  if(i == 0)
443  dest.push_back(src[0]);
444  else
445  dest.push_back(const_literal(false));
446  }
447 
448  return false;
449  }
450  }
451  break;
452 
454  if(src_bvtype==bvtypet::IS_UNSIGNED ||
455  src_bvtype==bvtypet::IS_C_BOOL ||
456  src_type.id()==ID_bool)
457  {
458  for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
459  {
460  if(j<src_width)
461  dest.push_back(src[j]);
462  else
463  dest.push_back(const_literal(false));
464 
465  dest.push_back(const_literal(false));
466  }
467 
468  return false;
469  }
470  else if(src_bvtype==bvtypet::IS_SIGNED)
471  {
472  for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
473  {
474  if(j<src_width)
475  dest.push_back(src[j]);
476  else
477  dest.push_back(src.back());
478 
479  dest.push_back(const_literal(false));
480  }
481 
482  return false;
483  }
484  else if(src_bvtype==bvtypet::IS_VERILOG_UNSIGNED)
485  {
486  // verilog_unsignedbv to verilog_unsignedbv
487  dest=src;
488 
489  if(dest_width<src_width)
490  dest.resize(dest_width);
491  else
492  {
493  dest=src;
494  while(dest.size()<dest_width)
495  {
496  dest.push_back(const_literal(false));
497  dest.push_back(const_literal(false));
498  }
499  }
500  return false;
501  }
502  break;
503 
504  case bvtypet::IS_BV:
505  INVARIANT(
506  src_width == dest_width,
507  "source bitvector width shall equal the destination bitvector width");
508  dest=src;
509  return false;
510 
511  case bvtypet::IS_C_BOOL:
512  dest.resize(dest_width, const_literal(false));
513 
514  if(src_bvtype==bvtypet::IS_FLOAT)
515  {
516  float_utilst float_utils(prop, to_floatbv_type(src_type));
517  dest[0]=!float_utils.is_zero(src);
518  }
519  else if(src_bvtype==bvtypet::IS_C_BOOL)
520  dest[0]=src[0];
521  else
522  dest[0]=!bv_utils.is_zero(src);
523 
524  return false;
525 
527  case bvtypet::IS_UNKNOWN:
529  if(dest_type.id()==ID_array)
530  {
531  if(src_width==dest_width)
532  {
533  dest=src;
534  return false;
535  }
536  }
537  else if(ns.follow(dest_type).id() == ID_struct)
538  {
539  const struct_typet &dest_struct = to_struct_type(ns.follow(dest_type));
540 
541  if(ns.follow(src_type).id() == ID_struct)
542  {
543  // we do subsets
544 
545  dest.resize(dest_width, const_literal(false));
546 
547  const struct_typet &op_struct = to_struct_type(ns.follow(src_type));
548 
549  const struct_typet::componentst &dest_comp=
550  dest_struct.components();
551 
552  const struct_typet::componentst &op_comp=
553  op_struct.components();
554 
555  // build offset maps
556  const offset_mapt op_offsets = build_offset_map(op_struct);
557  const offset_mapt dest_offsets = build_offset_map(dest_struct);
558 
559  // build name map
560  typedef std::map<irep_idt, std::size_t> op_mapt;
561  op_mapt op_map;
562 
563  for(std::size_t i=0; i<op_comp.size(); i++)
564  op_map[op_comp[i].get_name()]=i;
565 
566  // now gather required fields
567  for(std::size_t i=0;
568  i<dest_comp.size();
569  i++)
570  {
571  std::size_t offset=dest_offsets[i];
572  std::size_t comp_width=boolbv_width(dest_comp[i].type());
573  if(comp_width==0)
574  continue;
575 
576  op_mapt::const_iterator it=
577  op_map.find(dest_comp[i].get_name());
578 
579  if(it==op_map.end())
580  {
581  // not found
582 
583  // filling with free variables
584  for(std::size_t j=0; j<comp_width; j++)
585  dest[offset+j]=prop.new_variable();
586  }
587  else
588  {
589  // found
590  if(dest_comp[i].type()!=dest_comp[it->second].type())
591  {
592  // filling with free variables
593  for(std::size_t j=0; j<comp_width; j++)
594  dest[offset+j]=prop.new_variable();
595  }
596  else
597  {
598  std::size_t op_offset=op_offsets[it->second];
599  for(std::size_t j=0; j<comp_width; j++)
600  dest[offset+j]=src[op_offset+j];
601  }
602  }
603  }
604 
605  return false;
606  }
607  }
608  }
609 
610  return true;
611 }
612 
615 {
616  if(expr.op().type().id() == ID_range)
617  {
618  mp_integer from = string2integer(expr.op().type().get_string(ID_from));
619  mp_integer to = string2integer(expr.op().type().get_string(ID_to));
620 
621  if(from==1 && to==1)
622  return const_literal(true);
623  else if(from==0 && to==0)
624  return const_literal(false);
625  }
626 
627  const bvt &bv = convert_bv(expr.op());
628 
629  if(!bv.empty())
630  return prop.lor(bv);
631 
632  return SUB::convert_rest(expr);
633 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
boolbvt::convert_bv_typecast
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
Definition: boolbv_typecast.cpp:20
ieee_floatt
Definition: ieee_float.h:120
bvtypet::IS_SIGNED
@ IS_SIGNED
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
boolbvt::type_conversion
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
Definition: boolbv_typecast.cpp:33
c_bit_field_replacement_type.h
float_utilst
Definition: float_utils.h:18
typet
The type of an expression, extends irept.
Definition: type.h:29
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bvtypet::IS_FIXED
@ IS_FIXED
bvtypet::IS_C_BIT_FIELD
@ IS_C_BIT_FIELD
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
boolbv_type.h
get_bvtype
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
propt::lor
virtual literalt lor(literalt a, literalt b)=0
bvtypet::IS_VERILOG_SIGNED
@ IS_VERILOG_SIGNED
bvtypet::IS_RANGE
@ IS_RANGE
bv_utilst::incrementer
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:573
bvtypet::IS_UNSIGNED
@ IS_UNSIGNED
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:203
propt::land
virtual literalt land(literalt a, literalt b)=0
Forall_literals
#define Forall_literals(it, bv)
Definition: literal.h:207
bvtypet::IS_BV
@ IS_BV
float_utilst::from_signed_integer
bvt from_signed_integer(const bvt &)
Definition: float_utils.cpp:32
ieee_float_spect
Definition: ieee_float.h:26
bvtypet
bvtypet
Definition: boolbv_type.h:17
bvtypet::IS_VERILOG_UNSIGNED
@ IS_VERILOG_UNSIGNED
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
bvtypet::IS_FLOAT
@ IS_FLOAT
bv_utilst::add
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
float_utilst::is_zero
literalt is_zero(const bvt &)
Definition: float_utils.cpp:652
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1362
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
bvtypet::IS_C_BOOL
@ IS_C_BOOL
range_typet::get_from
mp_integer get_from() const
Definition: std_types.cpp:156
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
std_types.h
Pre-defined types.
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1471
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
irept::id
const irep_idt & id() const
Definition: irep.h:418
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
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:119
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv_solver.cpp:349
to_range_type
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:1726
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:431
bvtypet::IS_C_ENUM
@ IS_C_ENUM
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
fixedbv_typet::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: std_types.h:1324
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
literalt
Definition: literal.h:26
c_bit_field_replacement_type
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
Definition: c_bit_field_replacement_type.cpp:13
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
boolbv.h
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
boolbvt::convert_typecast
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
Definition: boolbv_typecast.cpp:614
bv_utilst::is_zero
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
boolbvt::offset_mapt
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:261
boolbvt::build_offset_map
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:660
float_utilst::spec
ieee_float_spect spec
Definition: float_utils.h:88
float_utilst::from_unsigned_integer
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:50
bvtypet::IS_UNKNOWN
@ IS_UNKNOWN
validation_modet::INVARIANT
@ INVARIANT
bv_utilst::zero_extension
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:184
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131