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