cprover
guard_bdd.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Guard Data Structure
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "guard_bdd.h"
13 
14 #include <algorithm>
15 #include <ostream>
16 #include <set>
17 
18 #include <solvers/bdd/bdd.h>
19 #include <solvers/prop/bdd_expr.h>
20 #include <util/expr_util.h>
21 #include <util/invariant.h>
22 #include <util/make_unique.h>
23 #include <util/namespace.h>
24 #include <util/simplify_utils.h>
25 #include <util/std_expr.h>
26 #include <util/symbol_table.h>
27 
29  : manager(manager), bdd(manager.from_expr(e))
30 {
31 }
32 
34 {
35  PRECONDITION(&manager == &other.manager);
36  bdd = other.bdd;
37  return *this;
38 }
39 
41 {
42  PRECONDITION(&manager == &other.manager);
43  std::swap(bdd, other.bdd);
44  return *this;
45 }
46 
48 {
49  if(is_true())
50  {
51  // do nothing
52  return expr;
53  }
54  else
55  {
56  if(expr.is_false())
57  {
58  return boolean_negate(as_expr());
59  }
60  else
61  {
62  return implies_exprt{as_expr(), expr};
63  }
64  }
65 }
66 
68 {
69  bdd = bdd.bdd_and(guard.bdd);
70  return *this;
71 }
72 
74 {
75  bdd = bdd.bdd_and(manager.from_expr(expr));
76  return *this;
77 }
78 
80 {
81  g1.bdd = g1.bdd.constrain(g2.bdd.bdd_or(g1.bdd));
82  return g1;
83 }
84 
86 {
87  g1.bdd = g1.bdd.bdd_or(g2.bdd);
88  return g1;
89 }
90 
92 {
93  return manager.as_expr(bdd);
94 }
bdd_exprt::from_expr
bddt from_expr(const exprt &expr)
Definition: bdd_expr.cpp:88
bddt::bdd
BDD bdd
Definition: bdd_cudd.h:128
bddt::bdd_or
bddt bdd_or(const bddt &other) const
Definition: bdd_cudd.h:100
guard_bddt::is_true
bool is_true() const
Definition: guard_bdd.h:47
guard_bddt::append
guard_bddt & append(const guard_bddt &guard)
Definition: guard_bdd.cpp:67
invariant.h
guard_bddt::bdd
bddt bdd
Definition: guard_bdd.h:77
bdd.h
Choice between the different interface to BDD libraries.
exprt
Base class for all expressions.
Definition: expr.h:53
guard_bddt
Definition: guard_bdd.h:25
namespace.h
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
bdd_exprt
Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...
Definition: bdd_expr.h:34
guard_bddt::add
guard_bddt & add(const exprt &expr)
Definition: guard_bdd.cpp:73
make_unique.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
guard_bddt::guard_bddt
guard_bddt(const exprt &e, bdd_exprt &manager)
Definition: guard_bdd.cpp:28
bdd_exprt::as_expr
exprt as_expr(const bddt &root) const
Definition: bdd_expr.cpp:172
guard_bddt::guard_expr
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
Definition: guard_bdd.cpp:47
bdd_expr.h
Conversion between exprt and miniBDD.
expr_util.h
Deprecated expression utility functions.
operator|=
guard_bddt & operator|=(guard_bddt &g1, const guard_bddt &g2)
Definition: guard_bdd.cpp:85
bddt::bdd_and
bddt bdd_and(const bddt &other) const
Definition: bdd_cudd.h:105
guard_bddt::operator=
guard_bddt & operator=(const guard_bddt &other)
Definition: guard_bdd.cpp:33
guard_bddt::manager
bdd_exprt & manager
Definition: guard_bdd.h:76
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
symbol_table.h
Author: Diffblue Ltd.
guard_bdd.h
Guard Data Structure Implementation using BDDs.
simplify_utils.h
std_expr.h
API to expression classes.
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
bddt::constrain
bddt constrain(const bddt &other)
Definition: bdd_cudd.h:120
guard_bddt::as_expr
exprt as_expr() const
Definition: guard_bdd.cpp:91
operator-=
guard_bddt & operator-=(guard_bddt &g1, const guard_bddt &g2)
Definition: guard_bdd.cpp:79