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 <cassert>
12 
13 #include <util/std_types.h>
14 #include <util/std_expr.h>
15 
17  const function_application_exprt &function_application)
18 {
19  function_map[function_application.function()].applications.
20  insert(function_application);
21 }
22 
24 {
25  for(function_mapt::const_iterator it=
26  function_map.begin();
27  it!=function_map.end();
28  it++)
29  add_function_constraints(it->second);
30 }
31 
33  const exprt::operandst &o2)
34 {
35  assert(o1.size()==o2.size());
36 
37  if(o1.empty())
38  return true_exprt();
39 
40  and_exprt and_expr;
41  and_exprt::operandst &conjuncts=and_expr.operands();
42  conjuncts.resize(o1.size());
43 
44  for(std::size_t i=0; i<o1.size(); i++)
45  {
46  exprt lhs=o1[i];
47  exprt rhs=o2[i];
48 
49  if(lhs.type()!=rhs.type())
50  rhs.make_typecast(lhs.type());
51 
52  conjuncts[i]=equal_exprt(lhs, rhs);
53  }
54 
55  return and_expr;
56 }
57 
59 {
60  // Do Ackermann's function reduction.
61  // This is quadratic, slow, and needs to be modernized.
62 
63  for(std::set<function_application_exprt>::const_iterator
64  it1=info.applications.begin();
65  it1!=info.applications.end();
66  it1++)
67  {
68  for(std::set<function_application_exprt>::const_iterator
69  it2=info.applications.begin();
70  it2!=it1;
71  it2++)
72  {
73  exprt arguments_equal_expr=
74  arguments_equal(it1->arguments(), it2->arguments());
75 
76  implies_exprt implication(arguments_equal_expr,
77  equal_exprt(*it1, *it2));
78 
79  prop_conv.set_to_true(implication);
80  }
81  }
82 }
application of (mathematical) function
Definition: std_expr.h:4531
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
Definition: functions.cpp:32
typet & type()
Definition: expr.h:56
function_mapt function_map
Definition: functions.h:50
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
The boolean constant true.
Definition: std_expr.h:4488
prop_convt & prop_conv
Definition: functions.h:40
boolean AND
Definition: std_expr.h:2255
API to expression classes.
symbol_exprt & function()
Definition: std_expr.h:4552
std::vector< exprt > operandst
Definition: expr.h:45
virtual void add_function_constraints()
Definition: functions.cpp:23
API to type classes.
void record(const function_application_exprt &function_application)
Definition: functions.cpp:16
Uninterpreted Functions.
Base class for all expressions.
Definition: expr.h:42
void set_to_true(const exprt &expr)
applicationst applications
Definition: functions.h:46
operandst & operands()
Definition: expr.h:66
void make_typecast(const typet &_type)
Definition: expr.cpp:84