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/format_expr.h>
16 #include <util/invariant.h>
17 #include <util/std_expr.h>
18 
19 #include <sstream>
20 
22 {
23  PRECONDITION(expr.type().id() == ID_bool);
24 
25  if(expr.is_constant())
26  return expr.is_false() ? bdd_mgr.False() : bdd_mgr.True();
27  else if(expr.id()==ID_not)
28  return !from_expr_rec(to_not_expr(expr).op());
29  else if(expr.id()==ID_and ||
30  expr.id()==ID_or ||
31  expr.id()==ID_xor)
32  {
34  expr.operands().size() >= 2,
35  "logical and, or, and xor expressions have at least two operands");
36  exprt bin_expr=make_binary(expr);
37 
38  mini_bddt op0=from_expr_rec(bin_expr.op0());
39  mini_bddt op1=from_expr_rec(bin_expr.op1());
40 
41  return expr.id()==ID_and ? (op0&op1) :
42  (expr.id()==ID_or ? (op0|op1) : (op0^op1));
43  }
44  else if(expr.id()==ID_implies)
45  {
46  const implies_exprt &imp_expr=to_implies_expr(expr);
47 
48  mini_bddt n_op0=!from_expr_rec(imp_expr.op0());
49  mini_bddt op1=from_expr_rec(imp_expr.op1());
50 
51  return n_op0|op1;
52  }
53  else if(expr.id()==ID_equal &&
54  expr.operands().size()==2 &&
55  expr.op0().type().id()==ID_bool)
56  {
57  const equal_exprt &eq_expr=to_equal_expr(expr);
58 
59  mini_bddt op0=from_expr_rec(eq_expr.op0());
60  mini_bddt op1=from_expr_rec(eq_expr.op1());
61 
62  return op0==op1;
63  }
64  else if(expr.id()==ID_if)
65  {
66  const if_exprt &if_expr=to_if_expr(expr);
67 
68  mini_bddt cond=from_expr_rec(if_expr.cond());
69  mini_bddt t_case=from_expr_rec(if_expr.true_case());
70  mini_bddt f_case=from_expr_rec(if_expr.false_case());
71 
72  return ((!cond)|t_case)&(cond|f_case);
73  }
74  else
75  {
76  std::pair<expr_mapt::iterator, bool> entry=
77  expr_map.insert(std::make_pair(expr, mini_bddt()));
78 
79  if(entry.second)
80  {
81  std::ostringstream s;
82  s << format(expr);
83  entry.first->second=bdd_mgr.Var(s.str());
84 
85  node_map.insert(std::make_pair(entry.first->second.var(),
86  expr));
87  }
88 
89  return entry.first->second;
90  }
91 }
92 
93 void bdd_exprt::from_expr(const exprt &expr)
94 {
95  root=from_expr_rec(expr);
96 }
97 
99 {
100  if(r.is_constant())
101  {
102  if(r.is_true())
103  return true_exprt();
104  else
105  return false_exprt();
106  }
107 
108  node_mapt::const_iterator entry=node_map.find(r.var());
109  CHECK_RETURN(entry != node_map.end());
110  const exprt &n_expr=entry->second;
111 
112  if(r.low().is_false())
113  {
114  if(r.high().is_true())
115  return n_expr;
116  else
117  return and_exprt(n_expr, as_expr(r.high()));
118  }
119  else if(r.high().is_false())
120  {
121  if(r.low().is_true())
122  return not_exprt(n_expr);
123  else
124  return and_exprt(not_exprt(n_expr), as_expr(r.low()));
125  }
126  else if(r.low().is_true())
127  return or_exprt(not_exprt(n_expr), as_expr(r.high()));
128  else if(r.high().is_true())
129  return or_exprt(n_expr, as_expr(r.low()));
130  else
131  return if_exprt(n_expr, as_expr(r.high()), as_expr(r.low()));
132 }
133 
135 {
136  if(!root.is_initialized())
137  return nil_exprt();
138 
139  return as_expr(root);
140 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
Boolean negation.
Definition: std_expr.h:3308
exprt & true_case()
Definition: std_expr.h:3455
static int8_t r
Definition: irep_hash.h:59
Boolean OR.
Definition: std_expr.h:2531
exprt & op0()
Definition: expr.h:84
const exprt & op() const
Definition: std_expr.h:371
Deprecated expression utility functions.
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
const mini_bddt & False() const
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
typet & type()
Return the type of the expression.
Definition: expr.h:68
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Boolean implication.
Definition: std_expr.h:2485
Equality.
Definition: std_expr.h:1484
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2505
Conversion between exprt and miniBDD.
const irep_idt & id() const
Definition: irep.h:259
expr_mapt expr_map
Definition: bdd_expr.h:46
The Boolean constant true.
Definition: std_expr.h:4443
bool is_initialized() const
Definition: miniBDD.h:58
The NIL expression.
Definition: std_expr.h:4461
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
exprt & op1()
Definition: expr.h:87
mini_bdd_mgrt bdd_mgr
Definition: bdd_expr.h:42
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
mini_bddt from_expr_rec(const exprt &expr)
Definition: bdd_expr.cpp:21
exprt & false_case()
Definition: std_expr.h:3465
exprt as_expr() const
Definition: bdd_expr.cpp:134
The Boolean constant false.
Definition: std_expr.h:4452
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
mini_bddt root
Definition: bdd_expr.h:43
void from_expr(const exprt &expr)
Definition: bdd_expr.cpp:93
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1519
mini_bddt Var(const std::string &label)
Definition: miniBDD.cpp:40
const mini_bddt & True() const
Base class for all expressions.
Definition: expr.h:54
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3328
node_mapt node_map
Definition: bdd_expr.h:48
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:36
static format_containert< T > format(const T &o)
Definition: format.h:35