CBMC
functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "functions.h"
10 
11 #include <util/std_expr.h>
12 
14 
15 void functionst::record(const function_application_exprt &function_application)
16 {
17  function_map[function_application.function()].applications.insert(
18  function_application);
19 }
20 
22 {
23  for(const auto &function : function_map)
24  add_function_constraints(function.second);
25 }
26 
28  const exprt::operandst &o1,
29  const exprt::operandst &o2)
30 {
31  PRECONDITION(o1.size() == o2.size());
32 
33  exprt::operandst conjuncts;
34  conjuncts.reserve(o1.size());
35 
36  for(std::size_t i = 0; i < o1.size(); i++)
37  {
38  exprt lhs = o1[i];
39  exprt rhs = typecast_exprt::conditional_cast(o2[i], o1[i].type());
40  conjuncts.push_back(equal_exprt(lhs, rhs));
41  }
42 
43  return conjunction(conjuncts);
44 }
45 
47 {
48  // Do Ackermann's function reduction.
49  // This is quadratic, slow, and needs to be modernized.
50 
51  for(std::set<function_application_exprt>::const_iterator it1 =
52  info.applications.begin();
53  it1 != info.applications.end();
54  it1++)
55  {
56  for(std::set<function_application_exprt>::const_iterator it2 =
57  info.applications.begin();
58  it2 != it1;
59  it2++)
60  {
61  exprt arguments_equal_expr =
62  arguments_equal(it1->arguments(), it2->arguments());
63 
64  implies_exprt implication(arguments_equal_expr, equal_exprt(*it1, *it2));
65 
67  }
68  }
69 }
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
Equality.
Definition: std_expr.h:1366
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
Application of (mathematical) function.
function_mapt function_map
Definition: functions.h:52
virtual void add_function_constraints()
Definition: functions.cpp:21
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
Definition: functions.cpp:27
void record(const function_application_exprt &function_application)
Definition: functions.cpp:15
decision_proceduret & decision_procedure
Definition: functions.h:42
Boolean implication.
Definition: std_expr.h:2188
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
Decision Procedure Interface.
Uninterpreted Functions.
static exprt implication(exprt lhs, exprt rhs)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:83
API to expression classes.
applicationst applications
Definition: functions.h:48