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 }
static exprt make_or(exprt a, exprt b)
Disjunction of two expressions.
Definition: bdd_expr.cpp:94
Conversion between exprt and miniBDD.
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
exprt as_expr(const bddt &root) const
Definition: bdd_expr.cpp:171
bddt from_expr_rec(const exprt &expr)
Definition: bdd_expr.cpp:18
bdd_managert bdd_mgr
Definition: bdd_expr.h:40
expr_mapt expr_map
Definition: bdd_expr.h:44
bddt from_expr(const exprt &expr)
Definition: bdd_expr.cpp:87
bddt bdd_false()
Definition: bdd_cudd.h:150
bddt bdd_true()
Definition: bdd_cudd.h:145
bdd_nodet bdd_node(const bddt &bdd) const
Definition: bdd_cudd.h:160
bddt bdd_variable(bdd_nodet::indext index)
Definition: bdd_cudd.h:155
Low level access to the structure of the BDD, read-only.
Definition: bdd_cudd.h:28
Logical operations on BDDs.
Definition: bdd_cudd.h:78
bddt bdd_xor(const bddt &other) const
Definition: bdd_cudd.h:110
static bddt bdd_ite(const bddt &i, const bddt &t, const bddt &e)
Definition: bdd_cudd.h:115
bddt bdd_or(const bddt &other) const
Definition: bdd_cudd.h:100
bddt bdd_not() const
Definition: bdd_cudd.h:95
bddt bdd_and(const bddt &other) const
Definition: bdd_cudd.h:105
exprt & op1()
Definition: expr.h:102
exprt & lhs()
Definition: std_expr.h:580
exprt & op0()
Definition: expr.h:99
exprt & rhs()
Definition: std_expr.h:590
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
The Boolean constant false.
Definition: std_expr.h:2865
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Boolean implication.
Definition: std_expr.h:2037
const irep_idt & id() const
Definition: irep.h:396
The NIL expression.
Definition: std_expr.h:2874
Boolean negation.
Definition: std_expr.h:2181
Boolean OR.
Definition: std_expr.h:2082
The Boolean constant true.
Definition: std_expr.h:2856
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:35
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:291
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
Deprecated expression utility functions.
static int8_t r
Definition: irep_hash.h:60
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062