30 throw "equality got different types";
39 if(type.
id()==ID_bool)
40 throw "equalityt got boolean equality";
50 std::pair<unsigned, unsigned> u;
53 std::pair<elementst::iterator, bool>
result=
54 elements.insert(std::pair<exprt, unsigned>(e1, elements.size()));
56 u.first=
result.first->second;
59 elements_rev[u.first]=e1;
63 std::pair<elementst::iterator, bool>
result=
64 elements.insert(elementst::value_type(e2, elements.size()));
66 u.second=
result.first->second;
69 elements_rev[u.second]=e2;
75 equalitiest::const_iterator
result=equalities.find(u);
77 if(
result==equalities.end())
82 equalities.insert(equalitiest::value_type(u, l));
93 for(typemapt::const_iterator it=
typemap.begin();
100 std::size_t no_elements=typestruct.
elements.size();
105 for(std::size_t i=no_elements; i!=0; bits++)
110 std::vector<bvt> eq_bvs;
112 eq_bvs.resize(no_elements);
114 for(std::size_t i=0; i<no_elements; i++)
116 eq_bvs[i].resize(bits);
117 for(std::size_t j=0; j<bits; j++)
125 for(equalitiest::const_iterator
130 const bvt &bv1=eq_bvs[it->first.first];
131 const bvt &bv2=eq_bvs[it->first.second];
The type of an expression.
std::map< unsigned, exprt > elements_revt
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
const irep_idt & id() const
virtual literalt new_variable()=0
virtual literalt equality2(const exprt &e1, const exprt &e2)
virtual void add_equality_constraints()
virtual void set_frozen(literalt)
std::unordered_map< const exprt, unsigned, irep_hash > elementst
virtual literalt equality(const exprt &e1, const exprt &e2)
literalt const_literal(bool value)
mstreamt & result() const
Base class for all expressions.
std::map< std::pair< unsigned, unsigned >, literalt > equalitiest
elements_revt elements_rev
std::vector< literalt > bvt