cprover
equality.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_FLATTENING_EQUALITY_H
11 #define CPROVER_SOLVERS_FLATTENING_EQUALITY_H
12 
13 #include <map>
14 
15 #include <util/expr.h>
16 
18 
20 {
21 public:
22  equalityt(propt &_prop, message_handlert &message_handler)
23  : prop_conv_solvert(_prop, message_handler)
24  {
25  }
26 
27  virtual literalt equality(const exprt &e1, const exprt &e2);
28 
29  void post_process() override
30  {
33  typemap.clear(); // if called incrementally, don't do it twice
34  }
35 
36 protected:
37  typedef std::unordered_map<const exprt, unsigned, irep_hash> elementst;
38  typedef std::map<std::pair<unsigned, unsigned>, literalt> equalitiest;
39  typedef std::map<unsigned, exprt> elements_revt;
40 
41  struct typestructt
42  {
46  };
47 
48  typedef std::unordered_map<const typet, typestructt, irep_hash> typemapt;
49 
51 
52  virtual literalt equality2(const exprt &e1, const exprt &e2);
53  virtual void add_equality_constraints();
54  virtual void add_equality_constraints(const typestructt &typestruct);
55 };
56 
57 #endif // CPROVER_SOLVERS_FLATTENING_EQUALITY_H
equalityt::typestructt
Definition: equality.h:42
equalityt::typemapt
std::unordered_map< const typet, typestructt, irep_hash > typemapt
Definition: equality.h:48
equalityt::typestructt::equalities
equalitiest equalities
Definition: equality.h:45
exprt
Base class for all expressions.
Definition: expr.h:53
equalityt::elements_revt
std::map< unsigned, exprt > elements_revt
Definition: equality.h:39
equalityt::post_process
void post_process() override
Definition: equality.h:29
expr.h
equalityt::equality2
virtual literalt equality2(const exprt &e1, const exprt &e2)
Definition: equality.cpp:25
prop_conv_solver.h
equalityt::add_equality_constraints
virtual void add_equality_constraints()
Definition: equality.cpp:89
equalityt::elementst
std::unordered_map< const exprt, unsigned, irep_hash > elementst
Definition: equality.h:37
equalityt::equalityt
equalityt(propt &_prop, message_handlert &message_handler)
Definition: equality.h:22
equalityt::typestructt::elements_rev
elements_revt elements_rev
Definition: equality.h:44
prop_conv_solvert::post_process
virtual void post_process()
Definition: prop_conv_solver.cpp:474
message_handlert
Definition: message.h:28
equalityt
Definition: equality.h:20
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
equalityt::typestructt::elements
elementst elements
Definition: equality.h:43
equalityt::equalitiest
std::map< std::pair< unsigned, unsigned >, literalt > equalitiest
Definition: equality.h:38
literalt
Definition: literal.h:26
prop_conv_solvert
Definition: prop_conv_solver.h:31
equalityt::typemap
typemapt typemap
Definition: equality.h:50
equalityt::equality
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17