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