cprover
bdd_expr.h
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
#ifndef CPROVER_SOLVERS_PROP_BDD_EXPR_H
13
#define CPROVER_SOLVERS_PROP_BDD_EXPR_H
14
22
#include <
util/expr.h
>
23
24
#include <
solvers/miniBDD/miniBDD.h
>
25
26
#include <unordered_map>
27
28
class
namespacet
;
29
32
class
bdd_exprt
33
{
34
public
:
35
explicit
bdd_exprt
(
const
namespacet
&_ns):
ns
(_ns) { }
36
37
void
from_expr
(
const
exprt
&expr);
38
exprt
as_expr
()
const
;
39
40
protected
:
41
const
namespacet
&
ns
;
42
mini_bdd_mgrt
bdd_mgr
;
43
mini_bddt
root
;
44
45
typedef
std::unordered_map<exprt, mini_bddt, irep_hash>
expr_mapt
;
46
expr_mapt
expr_map
;
47
typedef
std::map<unsigned, exprt>
node_mapt
;
48
node_mapt
node_map
;
49
50
mini_bddt
from_expr_rec
(
const
exprt
&expr);
51
exprt
as_expr
(
const
mini_bddt
&
r
)
const
;
52
};
53
54
#endif // CPROVER_SOLVERS_PROP_BDD_EXPR_H
bdd_exprt::as_expr
exprt as_expr() const
Definition:
bdd_expr.cpp:134
bdd_exprt::expr_map
expr_mapt expr_map
Definition:
bdd_expr.h:46
bdd_exprt::node_map
node_mapt node_map
Definition:
bdd_expr.h:48
miniBDD.h
Small BDD implementation.
exprt
Base class for all expressions.
Definition:
expr.h:54
bdd_exprt
TO_BE_DOCUMENTED.
Definition:
bdd_expr.h:32
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
bdd_exprt::from_expr
void from_expr(const exprt &expr)
Definition:
bdd_expr.cpp:93
mini_bdd_mgrt
Definition:
miniBDD.h:81
bdd_exprt::expr_mapt
std::unordered_map< exprt, mini_bddt, irep_hash > expr_mapt
Definition:
bdd_expr.h:45
bdd_exprt::bdd_exprt
bdd_exprt(const namespacet &_ns)
Definition:
bdd_expr.h:35
mini_bddt
Definition:
miniBDD.h:31
bdd_exprt::node_mapt
std::map< unsigned, exprt > node_mapt
Definition:
bdd_expr.h:47
bdd_exprt::from_expr_rec
mini_bddt from_expr_rec(const exprt &expr)
Definition:
bdd_expr.cpp:21
r
static int8_t r
Definition:
irep_hash.h:59
bdd_exprt::ns
const namespacet & ns
Definition:
bdd_expr.h:41
bdd_exprt::root
mini_bddt root
Definition:
bdd_expr.h:43
bdd_exprt::bdd_mgr
mini_bdd_mgrt bdd_mgr
Definition:
bdd_expr.h:42
solvers
prop
bdd_expr.h
Generated by
1.8.17