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