cprover
Loading...
Searching...
No Matches
guard_bdd.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Guard Data Structure
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
11
12#include "guard_bdd.h"
13
14#include <algorithm>
15
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{
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
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
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.