cprover
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_types.h>
12 #include <util/std_expr.h>
13 
15  const function_application_exprt &function_application)
16 {
17  function_map[function_application.function()].applications.
18  insert(function_application);
19 }
20 
22 {
23  for(function_mapt::const_iterator it=
24  function_map.begin();
25  it!=function_map.end();
26  it++)
27  add_function_constraints(it->second);
28 }
29 
31  const exprt::operandst &o2)
32 {
33  PRECONDITION(o1.size() == o2.size());
34 
35  if(o1.empty())
36  return true_exprt();
37 
38  and_exprt and_expr;
39  and_exprt::operandst &conjuncts=and_expr.operands();
40  conjuncts.resize(o1.size());
41 
42  for(std::size_t i=0; i<o1.size(); i++)
43  {
44  exprt lhs=o1[i];
45  exprt rhs = typecast_exprt::conditional_cast(o2[i], o1[i].type());
46  conjuncts[i]=equal_exprt(lhs, rhs);
47  }
48 
49  return std::move(and_expr);
50 }
51 
53 {
54  // Do Ackermann's function reduction.
55  // This is quadratic, slow, and needs to be modernized.
56 
57  for(std::set<function_application_exprt>::const_iterator
58  it1=info.applications.begin();
59  it1!=info.applications.end();
60  it1++)
61  {
62  for(std::set<function_application_exprt>::const_iterator
63  it2=info.applications.begin();
64  it2!=it1;
65  it2++)
66  {
67  exprt arguments_equal_expr=
68  arguments_equal(it1->arguments(), it2->arguments());
69 
70  implies_exprt implication(arguments_equal_expr,
71  equal_exprt(*it1, *it2));
72 
73  prop_conv.set_to_true(implication);
74  }
75  }
76 }
Application of (mathematical) function.
Definition: std_expr.h:4481
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
Definition: functions.cpp:30
function_mapt function_map
Definition: functions.h:50
Boolean implication.
Definition: std_expr.h:2485
Equality.
Definition: std_expr.h:1484
The Boolean constant true.
Definition: std_expr.h:4443
prop_convt & prop_conv
Definition: functions.h:40
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbol_exprt & function()
Definition: std_expr.h:4496
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
std::vector< exprt > operandst
Definition: expr.h:57
virtual void add_function_constraints()
Definition: functions.cpp:21
Pre-defined types.
void record(const function_application_exprt &function_application)
Definition: functions.cpp:14
Uninterpreted Functions.
Base class for all expressions.
Definition: expr.h:54
void set_to_true(const exprt &expr)
applicationst applications
Definition: functions.h:46
operandst & operands()
Definition: expr.h:78