cprover
qdimacs_core.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
9 #include "qdimacs_core.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/bitvector_expr.h>
13 #include <util/std_expr.h>
14 
16 {
17  if(expr.id()==ID_and)
18  {
19  typedef std::map<exprt, std::set<exprt> > used_bits_mapt;
20  used_bits_mapt used_bits_map;
21 
22  forall_operands(it, expr)
23  {
24  if(it->id() == ID_extractbit)
25  {
26  const auto &extractbit_expr = to_extractbit_expr(*it);
27  if(extractbit_expr.op1().is_constant())
28  used_bits_map[extractbit_expr.src()].insert(extractbit_expr.index());
29  }
30  else if(it->id() == ID_not && to_not_expr(*it).op().id() == ID_extractbit)
31  {
32  const auto &extractbit_expr = to_extractbit_expr(to_not_expr(*it).op());
33  if(extractbit_expr.op1().is_constant())
34  used_bits_map[extractbit_expr.src()].insert(extractbit_expr.index());
35  }
36  }
37 
38  // clang-format off
39  // this is unmaintained code, don't try to reformat it
40  for(used_bits_mapt::const_iterator it=used_bits_map.begin();
41  it!=used_bits_map.end();
42  it++)
43  {
44  #if 0
45  unsigned width;
46  boolbv_get_width(it->first.type(), width);
47 
48  std::string value_string;
49  value_string.resize(width, '0');
50 
51  if(it->second.size()==width) // all bits extracted from this one!
52  {
53  const irep_idt &ident=it->first.get(ID_identifier);
54  const exprt::operandst &old_operands=expr.operands();
55  exprt::operandst new_operands;
56 
57  for(exprt::operandst::const_iterator oit=old_operands.begin();
58  oit!=old_operands.end();
59  oit++)
60  {
61  if(oit->id()==ID_extractbit &&
62  oit->op1().is_constant())
63  {
64  if(oit->op0().get(ID_identifier)==ident)
65  {
66  const exprt &val_expr=oit->op1();
67  const std::size_t value = numeric_cast_v<std::size_t>(val_expr);
68  value_string[value]='1';
69 
70  #if 0
71  std::cout << "[" << value << "]=1\n";
72  #endif
73 
74  continue;
75  }
76  }
77  else if(oit->id()==ID_not &&
78  oit->op0().id()==ID_extractbit &&
79  oit->op0().op1().is_constant())
80  {
81  if(oit->op0().op0().get(ID_identifier)==ident)
82  {
83  // just kick it; the bit in value_string is 0 anyways
84  continue;
85  }
86  }
87 
88  new_operands.push_back(*oit);
89  }
90 
91  const constant_exprt new_value(value_string, it->first.type());
92  new_operands.push_back(equality_exprt(it->first, new_value));
93 
94  #if 0
95  std::cout << "FINAL: " << value_string << '\n';
96  #endif
97 
98  expr.operands()=new_operands;
99  }
100  #endif
101  }
102  // clang-format on
103  }
104 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:411
arith_tools.h
exprt
Base class for all expressions.
Definition: expr.h:54
qdimacs_core.h
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
exprt::op1
exprt & op1()
Definition: expr.h:106
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2066
qdimacs_coret::simplify_extractbits
void simplify_extractbits(exprt &expr) const
Definition: qdimacs_core.cpp:15
exprt::operands
operandst & operands()
Definition: expr.h:96
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
std_expr.h
API to expression classes.
bitvector_expr.h
API to expression classes for bitvectors.