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 
16 #include <solvers/prop/bdd_expr.h>
17 #include <util/expr_util.h>
18 #include <util/invariant.h>
19 #include <util/std_expr.h>
20 
22  : manager(manager), bdd(manager.from_expr(e))
23 {
24 }
25 
27 {
28  PRECONDITION(&manager == &other.manager);
29  bdd = other.bdd;
30  return *this;
31 }
32 
34 {
35  PRECONDITION(&manager == &other.manager);
36  std::swap(bdd, other.bdd);
37  return *this;
38 }
39 
41 {
42  if(is_true())
43  {
44  // do nothing
45  return expr;
46  }
47  else
48  {
49  if(expr.is_false())
50  {
51  return boolean_negate(as_expr());
52  }
53  else
54  {
55  return implies_exprt{as_expr(), expr};
56  }
57  }
58 }
59 
61 {
62  bdd = bdd.bdd_and(guard.bdd);
63  return *this;
64 }
65 
67 {
68  bdd = bdd.bdd_and(manager.from_expr(expr));
69  return *this;
70 }
71 
73 {
74  g1.bdd = g1.bdd.constrain(g2.bdd.bdd_or(g1.bdd));
75  return g1;
76 }
77 
79 {
80  g1.bdd = g1.bdd.bdd_or(g2.bdd);
81  return g1;
82 }
83 
85 {
86  return manager.as_expr(bdd);
87 }
Conversion between exprt and miniBDD.
Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...
Definition: bdd_expr.h:34
exprt as_expr(const bddt &root) const
Definition: bdd_expr.cpp:171
bddt from_expr(const exprt &expr)
Definition: bdd_expr.cpp:87
bddt constrain(const bddt &other)
Definition: bdd_cudd.h:120
bddt bdd_or(const bddt &other) const
Definition: bdd_cudd.h:100
bddt bdd_and(const bddt &other) const
Definition: bdd_cudd.h:105
BDD bdd
Definition: bdd_cudd.h:128
Base class for all expressions.
Definition: expr.h:54
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_true() const
Definition: guard_bdd.h:44
exprt as_expr() const
Definition: guard_bdd.cpp:84
guard_bddt & add(const exprt &expr)
Definition: guard_bdd.cpp:66
guard_bddt(const exprt &e, bdd_exprt &manager)
Definition: guard_bdd.cpp:21
guard_bddt & append(const guard_bddt &guard)
Definition: guard_bdd.cpp:60
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:40
bddt bdd
Definition: guard_bdd.h:74
bdd_exprt & manager
Definition: guard_bdd.h:73
guard_bddt & operator=(const guard_bddt &other)
Definition: guard_bdd.cpp:26
Boolean implication.
Definition: std_expr.h:2037
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
Deprecated expression utility functions.
guard_bddt & operator|=(guard_bddt &g1, const guard_bddt &g2)
Definition: guard_bdd.cpp:78
guard_bddt & operator-=(guard_bddt &g1, const guard_bddt &g2)
Definition: guard_bdd.cpp:72
Guard Data Structure Implementation using BDDs.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.