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/std_expr.h>
15 #include <util/expr_util.h>
16 #include <util/format_expr.h>
17 
18 #include <sstream>
19 
21 {
22  assert(expr.type().id()==ID_bool);
23 
24  if(expr.is_constant())
25  return expr.is_false() ? bdd_mgr.False() : bdd_mgr.True();
26  else if(expr.id()==ID_not)
27  return !from_expr_rec(to_not_expr(expr).op());
28  else if(expr.id()==ID_and ||
29  expr.id()==ID_or ||
30  expr.id()==ID_xor)
31  {
32  assert(expr.operands().size()>=2);
33  exprt bin_expr=make_binary(expr);
34 
35  mini_bddt op0=from_expr_rec(bin_expr.op0());
36  mini_bddt op1=from_expr_rec(bin_expr.op1());
37 
38  return expr.id()==ID_and ? (op0&op1) :
39  (expr.id()==ID_or ? (op0|op1) : (op0^op1));
40  }
41  else if(expr.id()==ID_implies)
42  {
43  const implies_exprt &imp_expr=to_implies_expr(expr);
44 
45  mini_bddt n_op0=!from_expr_rec(imp_expr.op0());
46  mini_bddt op1=from_expr_rec(imp_expr.op1());
47 
48  return n_op0|op1;
49  }
50  else if(expr.id()==ID_equal &&
51  expr.operands().size()==2 &&
52  expr.op0().type().id()==ID_bool)
53  {
54  const equal_exprt &eq_expr=to_equal_expr(expr);
55 
56  mini_bddt op0=from_expr_rec(eq_expr.op0());
57  mini_bddt op1=from_expr_rec(eq_expr.op1());
58 
59  return op0==op1;
60  }
61  else if(expr.id()==ID_iff)
62  {
63  assert(expr.operands().size()==2);
64 
65  mini_bddt op0=from_expr_rec(expr.op0());
66  mini_bddt op1=from_expr_rec(expr.op1());
67 
68  return op0==op1;
69  }
70  else if(expr.id()==ID_if)
71  {
72  const if_exprt &if_expr=to_if_expr(expr);
73 
74  mini_bddt cond=from_expr_rec(if_expr.cond());
75  mini_bddt t_case=from_expr_rec(if_expr.true_case());
76  mini_bddt f_case=from_expr_rec(if_expr.false_case());
77 
78  return ((!cond)|t_case)&(cond|f_case);
79  }
80  else
81  {
82  std::pair<expr_mapt::iterator, bool> entry=
83  expr_map.insert(std::make_pair(expr, mini_bddt()));
84 
85  if(entry.second)
86  {
87  std::ostringstream s;
88  s << format(expr);
89  entry.first->second=bdd_mgr.Var(s.str());
90 
91  node_map.insert(std::make_pair(entry.first->second.var(),
92  expr));
93  }
94 
95  return entry.first->second;
96  }
97 }
98 
99 void bdd_exprt::from_expr(const exprt &expr)
100 {
101  root=from_expr_rec(expr);
102 }
103 
105 {
106  if(r.is_constant())
107  {
108  if(r.is_true())
109  return true_exprt();
110  else
111  return false_exprt();
112  }
113 
114  node_mapt::const_iterator entry=node_map.find(r.var());
115  assert(entry!=node_map.end());
116  const exprt &n_expr=entry->second;
117 
118  if(r.low().is_false())
119  {
120  if(r.high().is_true())
121  return n_expr;
122  else
123  return and_exprt(n_expr, as_expr(r.high()));
124  }
125  else if(r.high().is_false())
126  {
127  if(r.low().is_true())
128  return not_exprt(n_expr);
129  else
130  return and_exprt(not_exprt(n_expr), as_expr(r.low()));
131  }
132  else if(r.low().is_true())
133  return or_exprt(not_exprt(n_expr), as_expr(r.high()));
134  else if(r.high().is_true())
135  return or_exprt(n_expr, as_expr(r.low()));
136  else
137  return if_exprt(n_expr, as_expr(r.high()), as_expr(r.low()));
138 }
139 
141 {
142  if(!root.is_initialized())
143  return nil_exprt();
144 
145  return as_expr(root);
146 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
Boolean negation.
Definition: std_expr.h:3230
exprt & true_case()
Definition: std_expr.h:3395
static int8_t r
Definition: irep_hash.h:59
boolean OR
Definition: std_expr.h:2391
exprt & op0()
Definition: expr.h:72
const exprt & op() const
Definition: std_expr.h:340
Deprecated expression utility functions.
bool is_false() const
Definition: expr.cpp:131
const mini_bddt & False() const
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
typet & type()
Definition: expr.h:56
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
Definition: std_expr.h:2362
Conversion between exprt and miniBDD.
const irep_idt & id() const
Definition: irep.h:189
expr_mapt expr_map
Definition: bdd_expr.h:46
The boolean constant true.
Definition: std_expr.h:4488
bool is_initialized() const
Definition: miniBDD.h:58
The NIL expression.
Definition: std_expr.h:4510
boolean AND
Definition: std_expr.h:2255
API to expression classes.
exprt & op1()
Definition: expr.h:75
mini_bdd_mgrt bdd_mgr
Definition: bdd_expr.h:42
mini_bddt from_expr_rec(const exprt &expr)
Definition: bdd_expr.cpp:20
exprt & false_case()
Definition: std_expr.h:3405
exprt as_expr() const
Definition: bdd_expr.cpp:140
The boolean constant false.
Definition: std_expr.h:4499
bool is_constant() const
Definition: expr.cpp:119
mini_bddt root
Definition: bdd_expr.h:43
void from_expr(const exprt &expr)
Definition: bdd_expr.cpp:99
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1377
mini_bddt Var(const std::string &label)
Definition: miniBDD.cpp:40
const mini_bddt & True() const
Base class for all expressions.
Definition: expr.h:42
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:3254
node_mapt node_map
Definition: bdd_expr.h:48
operandst & operands()
Definition: expr.h:66
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:22
static format_containert< T > format(const T &o)
Definition: format.h:35