39 type.id() != ID_bool,
"method shall not be used to compare Boolean types");
48 std::pair<unsigned, unsigned> u;
51 std::pair<elementst::iterator, bool>
result=
52 elements.insert(std::pair<exprt, unsigned>(e1, elements.size()));
54 u.first=
result.first->second;
57 elements_rev[u.first]=e1;
61 std::pair<elementst::iterator, bool>
result=
62 elements.insert(elementst::value_type(e2, elements.size()));
64 u.second=
result.first->second;
67 elements_rev[u.second]=e2;
73 equalitiest::const_iterator
result=equalities.find(u);
75 if(
result==equalities.end())
80 equalities.insert(equalitiest::value_type(u, l));
91 for(typemapt::const_iterator it=
typemap.begin();
98 std::size_t no_elements=typestruct.
elements.size();
103 for(std::size_t i=no_elements; i!=0; bits++)
108 std::vector<bvt> eq_bvs;
110 eq_bvs.resize(no_elements);
112 for(std::size_t i=0; i<no_elements; i++)
114 eq_bvs[i].resize(bits);
115 for(std::size_t j=0; j<bits; j++)
123 for(equalitiest::const_iterator
128 const bvt &bv1=eq_bvs[it->first.first];
129 const bvt &bv2=eq_bvs[it->first.second];
The type of an expression, extends irept.
std::map< unsigned, exprt > elements_revt
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
typet & type()
Return the type of the expression.
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
virtual literalt new_variable()=0
virtual literalt equality2(const exprt &e1, const exprt &e2)
virtual void add_equality_constraints()
#define PRECONDITION(CONDITION)
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
std::vector< literalt > bvt