cprover
simplify_utils.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 "simplify_utils.h"
10 #include "as_const.h"
11 
12 #include <algorithm>
13 
18 {
19  bool do_sort=false;
20 
21  forall_expr(it, operands)
22  {
23  exprt::operandst::const_iterator next_it=it;
24  next_it++;
25 
26  if(next_it!=operands.end() && *next_it < *it)
27  {
28  do_sort=true;
29  break;
30  }
31  }
32 
33  if(!do_sort)
34  return true;
35 
36  std::sort(operands.begin(), operands.end());
37 
38  return false;
39 }
40 
42 // The entries
43 // { ID_plus, ID_floatbv },
44 // { ID_mult, ID_floatbv },
45 // { ID_plus, ID_pointer },
46 // are deliberately missing, as FP-addition and multiplication
47 // aren't associative. Addition to pointers isn't really
48 // associative.
49 
50 struct saj_tablet
51 {
52  const irep_idt id;
53  const irep_idt type_ids[10];
54 } const saj_table[]=
55 {
56  { ID_plus, {ID_integer ,
57  ID_natural ,
58  ID_real ,
59  ID_complex ,
60  ID_rational ,
61  ID_unsignedbv ,
62  ID_signedbv ,
63  ID_fixedbv ,
64  irep_idt() }},
65  { ID_mult, {ID_integer ,
66  ID_natural ,
67  ID_real ,
68  ID_complex ,
69  ID_rational ,
70  ID_unsignedbv ,
71  ID_signedbv ,
72  ID_fixedbv ,
73  irep_idt() }},
74  { ID_and, {ID_bool ,
75  irep_idt() }},
76  { ID_or, {ID_bool ,
77  irep_idt() }},
78  { ID_xor, {ID_bool ,
79  irep_idt() }},
80  { ID_bitand, {ID_unsignedbv ,
81  ID_signedbv ,
82  ID_floatbv ,
83  ID_fixedbv ,
84  irep_idt() }},
85  { ID_bitor, {ID_unsignedbv ,
86  ID_signedbv ,
87  ID_floatbv ,
88  ID_fixedbv ,
89  irep_idt() }},
90  { ID_bitxor, {ID_unsignedbv ,
91  ID_signedbv ,
92  ID_floatbv ,
93  ID_fixedbv ,
94  irep_idt() }},
95  { irep_idt(), { irep_idt() }}
96 };
97 
98 static bool sort_and_join(
99  const struct saj_tablet &saj_entry,
100  const irep_idt &type_id)
101 {
102  for(unsigned i=0; !saj_entry.type_ids[i].empty(); i++)
103  if(type_id==saj_entry.type_ids[i])
104  return true;
105 
106  return false;
107 }
108 
109 static const struct saj_tablet &sort_and_join(
110  const irep_idt &id,
111  const irep_idt &type_id)
112 {
113  unsigned i=0;
114 
115  for( ; !saj_table[i].id.empty(); i++)
116  if(id==saj_table[i].id &&
117  sort_and_join(saj_table[i], type_id))
118  return saj_table[i];
119 
120  return saj_table[i];
121 }
122 
123 bool sort_and_join(exprt &expr)
124 {
125  bool no_change = true;
126 
127  if(!expr.has_operands())
128  return true;
129 
130  const struct saj_tablet &saj_entry =
131  sort_and_join(expr.id(), as_const(expr).type().id());
132  if(saj_entry.id.empty())
133  return true;
134 
135  // check operand types
136 
137  forall_operands(it, expr)
138  if(!sort_and_join(saj_entry, it->type().id()))
139  return true;
140 
141  // join expressions
142 
143  exprt::operandst new_ops;
144  new_ops.reserve(expr.operands().size());
145 
146  forall_operands(it, expr)
147  {
148  if(it->id()==expr.id())
149  {
150  new_ops.reserve(new_ops.capacity()+it->operands().size()-1);
151 
152  forall_operands(it2, *it)
153  new_ops.push_back(*it2);
154 
155  no_change = false;
156  }
157  else
158  new_ops.push_back(*it);
159  }
160 
161  // sort it
162 
163  no_change = sort_operands(new_ops) && no_change;
164  expr.operands().swap(new_ops);
165 
166  return no_change;
167 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
saj_tablet::id
const irep_idt id
Definition: simplify_utils.cpp:52
saj_tablet
produce canonical ordering for associative and commutative binary operators
Definition: simplify_utils.cpp:51
exprt
Base class for all expressions.
Definition: expr.h:53
irep_idt
dstringt irep_idt
Definition: irep.h:32
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
saj_tablet::type_ids
const irep_idt type_ids[10]
Definition: simplify_utils.cpp:53
saj_table
struct saj_tablet saj_table[]
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
sort_and_join
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
Definition: simplify_utils.cpp:98
exprt::operands
operandst & operands()
Definition: expr.h:95
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:29
simplify_utils.h
as_const.h
sort_operands
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
Definition: simplify_utils.cpp:17