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 
17 #include <solvers/prop/prop_conv.h>
18 
20 {
21 public:
23  const namespacet &_ns,
24  propt &_prop):prop_conv_solvert(_ns, _prop) { }
25 
26  virtual literalt equality(const exprt &e1, const exprt &e2);
27 
28  void post_process() override
29  {
32  typemap.clear(); // if called incrementally, don't do it twice
33  }
34 
35 protected:
36  typedef std::unordered_map<const exprt, unsigned, irep_hash> elementst;
37  typedef std::map<std::pair<unsigned, unsigned>, literalt> equalitiest;
38  typedef std::map<unsigned, exprt> elements_revt;
39 
40  struct typestructt
41  {
45  };
46 
47  typedef std::unordered_map<const typet, typestructt, irep_hash> typemapt;
48 
50 
51  virtual literalt equality2(const exprt &e1, const exprt &e2);
52  virtual void add_equality_constraints();
53  virtual void add_equality_constraints(const typestructt &typestruct);
54 };
55 
56 #endif // CPROVER_SOLVERS_FLATTENING_EQUALITY_H
std::map< unsigned, exprt > elements_revt
Definition: equality.h:38
equalityt(const namespacet &_ns, propt &_prop)
Definition: equality.h:22
virtual void post_process()
Definition: prop_conv.cpp:461
std::unordered_map< const typet, typestructt, irep_hash > typemapt
Definition: equality.h:47
virtual literalt equality2(const exprt &e1, const exprt &e2)
Definition: equality.cpp:25
TO_BE_DOCUMENTED.
Definition: namespace.h:74
virtual void add_equality_constraints()
Definition: equality.cpp:91
elementst elements
Definition: equality.h:42
std::unordered_map< const exprt, unsigned, irep_hash > elementst
Definition: equality.h:36
void post_process() override
Definition: equality.h:28
TO_BE_DOCUMENTED.
Definition: prop.h:24
equalitiest equalities
Definition: equality.h:44
typemapt typemap
Definition: equality.h:49
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
TO_BE_DOCUMENTED.
Definition: prop_conv.h:70
Base class for all expressions.
Definition: expr.h:42
std::map< std::pair< unsigned, unsigned >, literalt > equalitiest
Definition: equality.h:37
elements_revt elements_rev
Definition: equality.h:43