10 #ifndef CPROVER_SOLVERS_FLATTENING_EQUALITY_H 11 #define CPROVER_SOLVERS_FLATTENING_EQUALITY_H 36 typedef std::unordered_map<const exprt, unsigned, irep_hash>
elementst;
47 typedef std::unordered_map<const typet, typestructt, irep_hash>
typemapt;
56 #endif // CPROVER_SOLVERS_FLATTENING_EQUALITY_H std::map< unsigned, exprt > elements_revt
equalityt(const namespacet &_ns, propt &_prop)
virtual void post_process()
std::unordered_map< const typet, typestructt, irep_hash > typemapt
virtual literalt equality2(const exprt &e1, const exprt &e2)
virtual void add_equality_constraints()
std::unordered_map< const exprt, unsigned, irep_hash > elementst
void post_process() override
virtual literalt equality(const exprt &e1, const exprt &e2)
Base class for all expressions.
std::map< std::pair< unsigned, unsigned >, literalt > equalitiest
elements_revt elements_rev