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