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_expr.h>
12 #include <util/std_types.h>
13 
14 void functionst::record(const function_application_exprt &function_application)
15 {
16  function_map[function_application.function()].applications.insert(
17  function_application);
18 }
19 
21 {
22  for(const auto &function : function_map)
23  add_function_constraints(function.second);
24 }
25 
27  const exprt::operandst &o1,
28  const exprt::operandst &o2)
29 {
30  PRECONDITION(o1.size() == o2.size());
31 
32  exprt::operandst conjuncts;
33  conjuncts.reserve(o1.size());
34 
35  for(std::size_t i = 0; i < o1.size(); i++)
36  {
37  exprt lhs = o1[i];
38  exprt rhs = typecast_exprt::conditional_cast(o2[i], o1[i].type());
39  conjuncts.push_back(equal_exprt(lhs, rhs));
40  }
41 
42  return conjunction(conjuncts);
43 }
44 
46 {
47  // Do Ackermann's function reduction.
48  // This is quadratic, slow, and needs to be modernized.
49 
50  for(std::set<function_application_exprt>::const_iterator it1 =
51  info.applications.begin();
52  it1 != info.applications.end();
53  it1++)
54  {
55  for(std::set<function_application_exprt>::const_iterator it2 =
56  info.applications.begin();
57  it2 != it1;
58  it2++)
59  {
60  exprt arguments_equal_expr =
61  arguments_equal(it1->arguments(), it2->arguments());
62 
63  implies_exprt implication(arguments_equal_expr, equal_exprt(*it1, *it2));
64 
65  decision_procedure.set_to_true(implication);
66  }
67  }
68 }
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
conjunction
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:51
functionst::function_map
function_mapt function_map
Definition: functions.h:52
exprt
Base class for all expressions.
Definition: expr.h:53
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Definition: decision_procedure.cpp:23
functionst::arguments_equal
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
Definition: functions.cpp:26
functions.h
Uninterpreted Functions.
equal_exprt
Equality.
Definition: std_expr.h:1190
functionst::function_infot::applications
applicationst applications
Definition: functions.h:48
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
functionst::record
void record(const function_application_exprt &function_application)
Definition: functions.cpp:14
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
std_types.h
Pre-defined types.
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
functionst::decision_procedure
decision_proceduret & decision_procedure
Definition: functions.h:42
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
functionst::add_function_constraints
virtual void add_function_constraints()
Definition: functions.cpp:20
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:211
functionst::function_infot
Definition: functions.h:47
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
std_expr.h
API to expression classes.