cprover
equality.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 "equality.h"
10 
11 #ifdef DEBUG
12 #include <iostream>
13 #endif
14 
15 #include "bv_utils.h"
16 
17 literalt equalityt::equality(const exprt &e1, const exprt &e2)
18 {
19  if(e1<e2)
20  return equality2(e1, e2);
21  else
22  return equality2(e2, e1);
23 }
24 
26 {
27  const typet &type=e1.type();
28 
29  if(e2.type()!=e1.type())
30  throw "equality got different types";
31 
32  // check for syntactical equality
33 
34  if(e1==e2)
35  return const_literal(true);
36 
37  // check for boolean equality
38 
39  if(type.id()==ID_bool)
40  throw "equalityt got boolean equality";
41  // return lequal(convert(e1), convert(e2));
42 
43  // look it up
44 
45  typestructt &typestruct=typemap[type];
46  elementst &elements=typestruct.elements;
47  elements_revt &elements_rev=typestruct.elements_rev;
48  equalitiest &equalities=typestruct.equalities;
49 
50  std::pair<unsigned, unsigned> u;
51 
52  {
53  std::pair<elementst::iterator, bool> result=
54  elements.insert(std::pair<exprt, unsigned>(e1, elements.size()));
55 
56  u.first=result.first->second;
57 
58  if(result.second)
59  elements_rev[u.first]=e1;
60  }
61 
62  {
63  std::pair<elementst::iterator, bool> result=
64  elements.insert(elementst::value_type(e2, elements.size()));
65 
66  u.second=result.first->second;
67 
68  if(result.second)
69  elements_rev[u.second]=e2;
70  }
71 
72  literalt l;
73 
74  {
75  equalitiest::const_iterator result=equalities.find(u);
76 
77  if(result==equalities.end())
78  {
79  l=prop.new_variable();
80  if(freeze_all && !l.is_constant())
81  prop.set_frozen(l);
82  equalities.insert(equalitiest::value_type(u, l));
83  }
84  else
85  l=result->second;
86  }
87 
88  return l;
89 }
90 
92 {
93  for(typemapt::const_iterator it=typemap.begin();
94  it!=typemap.end(); it++)
95  add_equality_constraints(it->second);
96 }
97 
99 {
100  std::size_t no_elements=typestruct.elements.size();
101  std::size_t bits=0;
102 
103  // get number of necessary bits
104 
105  for(std::size_t i=no_elements; i!=0; bits++)
106  i=(i>>1);
107 
108  // generate bit vectors
109 
110  std::vector<bvt> eq_bvs;
111 
112  eq_bvs.resize(no_elements);
113 
114  for(std::size_t i=0; i<no_elements; i++)
115  {
116  eq_bvs[i].resize(bits);
117  for(std::size_t j=0; j<bits; j++)
118  eq_bvs[i][j]=prop.new_variable();
119  }
120 
121  // generate equality constraints
122 
123  bv_utilst bv_utils(prop);
124 
125  for(equalitiest::const_iterator
126  it=typestruct.equalities.begin();
127  it!=typestruct.equalities.end();
128  it++)
129  {
130  const bvt &bv1=eq_bvs[it->first.first];
131  const bvt &bv2=eq_bvs[it->first.second];
132 
133  prop.set_equal(bv_utils.equal(bv1, bv2), it->second);
134  }
135 }
The type of an expression.
Definition: type.h:20
mstreamt & result()
Definition: message.h:233
virtual void set_frozen(literalt a)
Definition: prop.h:109
std::map< unsigned, exprt > elements_revt
Definition: equality.h:38
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
typet & type()
Definition: expr.h:60
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:14
const irep_idt & id() const
Definition: irep.h:189
virtual literalt new_variable()=0
virtual literalt equality2(const exprt &e1, const exprt &e2)
Definition: equality.cpp:25
virtual void add_equality_constraints()
Definition: equality.cpp:91
elementst elements
Definition: equality.h:42
std::unordered_map< const exprt, unsigned, irep_hash > elementst
Definition: equality.h:36
equalitiest equalities
Definition: equality.h:44
typemapt typemap
Definition: equality.h:49
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
literalt const_literal(bool value)
Definition: literal.h:187
bool is_constant() const
Definition: literal.h:165
Base class for all expressions.
Definition: expr.h:46
std::map< std::pair< unsigned, unsigned >, literalt > equalitiest
Definition: equality.h:37
elements_revt elements_rev
Definition: equality.h:43
std::vector< literalt > bvt
Definition: literal.h:197