cprover
bdd_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Conversion between exprt and miniBDD
4 
5 Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #include "bdd_expr.h"
13 
14 #include <util/expr_util.h>
15 #include <util/invariant.h>
16 #include <util/std_expr.h>
17 
19 {
20  PRECONDITION(expr.type().id() == ID_bool);
21 
22  if(expr.is_constant())
23  return expr.is_false() ? bdd_mgr.bdd_false() : bdd_mgr.bdd_true();
24  else if(expr.id()==ID_not)
25  return from_expr_rec(to_not_expr(expr).op()).bdd_not();
26  else if(expr.id()==ID_and ||
27  expr.id()==ID_or ||
28  expr.id()==ID_xor)
29  {
31  expr.operands().size() >= 2,
32  "logical and, or, and xor expressions have at least two operands");
33  exprt bin_expr=make_binary(expr);
34 
35  bddt lhs = from_expr_rec(to_binary_expr(bin_expr).lhs());
36  bddt rhs = from_expr_rec(to_binary_expr(bin_expr).rhs());
37 
38  return expr.id() == ID_and
39  ? lhs.bdd_and(rhs)
40  : (expr.id() == ID_or ? lhs.bdd_or(rhs) : lhs.bdd_xor(rhs));
41  }
42  else if(expr.id()==ID_implies)
43  {
44  const implies_exprt &imp_expr=to_implies_expr(expr);
45 
46  bddt n_lhs = from_expr_rec(imp_expr.lhs()).bdd_not();
47  bddt rhs = from_expr_rec(imp_expr.rhs());
48 
49  return n_lhs.bdd_or(rhs);
50  }
51  else if(
52  expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool)
53  {
54  const equal_exprt &eq_expr=to_equal_expr(expr);
55 
56  bddt op0 = from_expr_rec(eq_expr.op0());
57  bddt op1 = from_expr_rec(eq_expr.op1());
58 
59  return op0.bdd_xor(op1).bdd_not();
60  }
61  else if(expr.id()==ID_if)
62  {
63  const if_exprt &if_expr=to_if_expr(expr);
64 
65  bddt cond = from_expr_rec(if_expr.cond());
66  bddt t_case = from_expr_rec(if_expr.true_case());
67  bddt f_case = from_expr_rec(if_expr.false_case());
68 
69  return bddt::bdd_ite(cond, t_case, f_case);
70  }
71  else
72  {
73  std::pair<expr_mapt::iterator, bool> entry =
74  expr_map.emplace(expr, bdd_mgr.bdd_true());
75 
76  if(entry.second)
77  {
78  node_map.push_back(expr);
79  const unsigned index = (unsigned)node_map.size() - 1;
80  entry.first->second = bdd_mgr.bdd_variable(index);
81  }
82 
83  return entry.first->second;
84  }
85 }
86 
88 {
89  return from_expr_rec(expr);
90 }
91 
94 static exprt make_or(exprt a, exprt b)
95 {
96  if(b.id() == ID_or)
97  {
98  b.add_to_operands(std::move(a));
99  return b;
100  }
101  return or_exprt{std::move(a), std::move(b)};
102 }
103 
108  const bdd_nodet &r,
109  std::unordered_map<bdd_nodet::idt, exprt> &cache) const
110 {
111  if(r.is_constant())
112  {
113  if(r.is_complement())
114  return false_exprt();
115  else
116  return true_exprt();
117  }
118 
119  auto index = narrow<std::size_t>(r.index());
120  INVARIANT(index < node_map.size(), "Index should be in node_map");
121  const exprt &n_expr = node_map[index];
122 
123  // Look-up cache for already computed value
124  auto insert_result = cache.emplace(r.id(), nil_exprt());
125  if(insert_result.second)
126  {
127  auto result_ignoring_complementation = [&]() -> exprt {
128  if(r.else_branch().is_constant())
129  {
130  if(r.then_branch().is_constant())
131  {
132  if(r.else_branch().is_complement()) // else is false
133  return n_expr;
134  return not_exprt(n_expr); // else is true
135  }
136  else
137  {
138  if(r.else_branch().is_complement()) // else is false
139  {
140  exprt then_case = as_expr(r.then_branch(), cache);
141  return make_and(n_expr, then_case);
142  }
143  exprt then_case = as_expr(r.then_branch(), cache);
144  return make_or(not_exprt(n_expr), then_case);
145  }
146  }
147  else if(r.then_branch().is_constant())
148  {
149  if(r.then_branch().is_complement()) // then is false
150  {
151  exprt else_case = as_expr(r.else_branch(), cache);
152  return make_and(not_exprt(n_expr), else_case);
153  }
154  exprt else_case = as_expr(r.else_branch(), cache);
155  return make_or(n_expr, else_case);
156  }
157 
158  exprt then_branch = as_expr(r.then_branch(), cache);
159  exprt else_branch = as_expr(r.else_branch(), cache);
160  return if_exprt(n_expr, then_branch, else_branch);
161  }();
162 
163  insert_result.first->second =
164  r.is_complement()
165  ? boolean_negate(std::move(result_ignoring_complementation))
166  : result_ignoring_complementation;
167  }
168  return insert_result.first->second;
169 }
170 
171 exprt bdd_exprt::as_expr(const bddt &root) const
172 {
173  std::unordered_map<bdd_nodet::idt, exprt> cache;
174  bdd_nodet node = bdd_mgr.bdd_node(root);
175  return as_expr(node, cache);
176 }
make_and
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:289
bdd_exprt::from_expr
bddt from_expr(const exprt &expr)
Definition: bdd_expr.cpp:87
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:590
bddt::bdd_or
bddt bdd_or(const bddt &other) const
Definition: bdd_cudd.h:100
bdd_exprt::expr_map
expr_mapt expr_map
Definition: bdd_expr.h:44
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
bdd_exprt::node_map
std::vector< exprt > node_map
Mapping from BDD variables to expressions: the expression at index i of node_map corresponds to the i...
Definition: bdd_expr.h:48
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
bddt::bdd_not
bddt bdd_not() const
Definition: bdd_cudd.h:95
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:580
bdd_nodet
Low level access to the structure of the BDD, read-only.
Definition: bdd_cudd.h:28
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:34
equal_exprt
Equality.
Definition: std_expr.h:1225
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
bdd_exprt::bdd_mgr
bdd_managert bdd_mgr
Definition: bdd_expr.h:40
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
or_exprt
Boolean OR.
Definition: std_expr.h:2028
bddt::bdd_ite
static bddt bdd_ite(const bddt &i, const bddt &t, const bddt &e)
Definition: bdd_cudd.h:115
bdd_managert::bdd_true
bddt bdd_true()
Definition: bdd_cudd.h:145
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
bdd_managert::bdd_node
bdd_nodet bdd_node(const bddt &bdd) const
Definition: bdd_cudd.h:160
bdd_managert::bdd_variable
bddt bdd_variable(bdd_nodet::indext index)
Definition: bdd_cudd.h:155
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:125
bdd_exprt::as_expr
exprt as_expr(const bddt &root) const
Definition: bdd_expr.cpp:171
irept::id
const irep_idt & id() const
Definition: irep.h:407
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
bdd_managert::bdd_false
bddt bdd_false()
Definition: bdd_cudd.h:150
bdd_expr.h
Conversion between exprt and miniBDD.
expr_util.h
Deprecated expression utility functions.
bdd_exprt::from_expr_rec
bddt from_expr_rec(const exprt &expr)
Definition: bdd_expr.cpp:18
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
bddt::bdd_and
bddt bdd_and(const bddt &other) const
Definition: bdd_cudd.h:105
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2008
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2189
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
implies_exprt
Boolean implication.
Definition: std_expr.h:1983
exprt::operands
operandst & operands()
Definition: expr.h:92
r
static int8_t r
Definition: irep_hash.h:60
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
bddt
Logical operations on BDDs.
Definition: bdd_cudd.h:78
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
binary_exprt::op1
exprt & op1()
Definition: expr.h:102
std_expr.h
API to expression classes.
bddt::bdd_xor
bddt bdd_xor(const bddt &other) const
Definition: bdd_cudd.h:110
make_or
static exprt make_or(exprt a, exprt b)
Disjunction of two expressions.
Definition: bdd_expr.cpp:94
binary_exprt::op0
exprt & op0()
Definition: expr.h:99
not_exprt
Boolean negation.
Definition: std_expr.h:2127