Go to the documentation of this file.
10 #ifndef CPROVER_SOLVERS_FLATTENING_EQUALITY_H
11 #define CPROVER_SOLVERS_FLATTENING_EQUALITY_H
37 typedef std::unordered_map<const exprt, unsigned, irep_hash>
elementst;
48 typedef std::unordered_map<const typet, typestructt, irep_hash>
typemapt;
57 #endif // CPROVER_SOLVERS_FLATTENING_EQUALITY_H
std::unordered_map< const typet, typestructt, irep_hash > typemapt
Base class for all expressions.
std::map< unsigned, exprt > elements_revt
void post_process() override
virtual literalt equality2(const exprt &e1, const exprt &e2)
virtual void add_equality_constraints()
std::unordered_map< const exprt, unsigned, irep_hash > elementst
equalityt(propt &_prop, message_handlert &message_handler)
elements_revt elements_rev
virtual void post_process()
std::map< std::pair< unsigned, unsigned >, literalt > equalitiest
virtual literalt equality(const exprt &e1, const exprt &e2)