CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
bdd_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Conversion between exprt and miniBDD
4
5Author: 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/narrow.h>
17#include <util/std_expr.h>
18
20{
22
23 if(expr.is_constant())
24 return expr.is_false() ? bdd_mgr.bdd_false() : bdd_mgr.bdd_true();
25 else if(expr.id()==ID_not)
26 return from_expr_rec(to_not_expr(expr).op()).bdd_not();
27 else if(expr.id()==ID_and ||
28 expr.id()==ID_or ||
29 expr.id()==ID_xor)
30 {
32 expr.operands().size() >= 2,
33 "logical and, or, and xor expressions have at least two operands");
35
38
39 return expr.id() == ID_and
40 ? lhs.bdd_and(rhs)
41 : (expr.id() == ID_or ? lhs.bdd_or(rhs) : lhs.bdd_xor(rhs));
42 }
43 else if(expr.id()==ID_implies)
44 {
46
48 bddt rhs = from_expr_rec(imp_expr.rhs());
49
50 return n_lhs.bdd_or(rhs);
51 }
52 else if(expr.id() == ID_equal && to_equal_expr(expr).lhs().is_boolean())
53 {
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
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()
167 }
168 return insert_result.first->second;
169}
170
171exprt 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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:19
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
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3199
The trinary if-then-else operator.
Definition std_expr.h:2497
Boolean implication.
Definition std_expr.h:2225
const irep_idt & id() const
Definition irep.h:388
The NIL expression.
Definition std_expr.h:3208
Boolean negation.
Definition std_expr.h:2454
Boolean OR.
Definition std_expr.h:2270
The Boolean constant true.
Definition std_expr.h:3190
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:38
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
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:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2479
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2250
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407