cprover
functions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Uninterpreted Functions
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
13 #define CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
14 
15 #include <set>
16 
17 #include <util/std_expr.h>
18 
19 #include <solvers/prop/prop_conv.h>
20 
22 {
23 public:
24  explicit functionst(prop_convt &_prop_conv):
25  prop_conv(_prop_conv) { }
26 
27  virtual ~functionst()
28  {
29  }
30 
31  void record(
32  const function_application_exprt &function_application);
33 
34  virtual void post_process()
35  {
37  }
38 
39 protected:
41 
42  typedef std::set<function_application_exprt> applicationst;
43 
45  {
46  applicationst applications;
47  };
48 
49  typedef std::map<exprt, function_infot> function_mapt;
50  function_mapt function_map;
51 
52  virtual void add_function_constraints();
53  virtual void add_function_constraints(const function_infot &info);
54 
56  const exprt::operandst &o2);
57 };
58 
59 #endif // CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
application of (mathematical) function
Definition: std_expr.h:3785
virtual ~functionst()
Definition: functions.h:27
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
Definition: functions.cpp:32
functionst(prop_convt &_prop_conv)
Definition: functions.h:24
function_mapt function_map
Definition: functions.h:50
std::set< function_application_exprt > applicationst
Definition: functions.h:42
prop_convt & prop_conv
Definition: functions.h:40
API to expression classes.
std::vector< exprt > operandst
Definition: expr.h:49
virtual void add_function_constraints()
Definition: functions.cpp:23
void record(const function_application_exprt &function_application)
Definition: functions.cpp:16
Base class for all expressions.
Definition: expr.h:46
applicationst applications
Definition: functions.h:46
std::map< exprt, function_infot > function_mapt
Definition: functions.h:49
virtual void post_process()
Definition: functions.h:34