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 
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;
44 
45  typedef std::unordered_map<exprt, mini_bddt, irep_hash> expr_mapt;
47  typedef std::map<unsigned, exprt> node_mapt;
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
static int8_t r
Definition: irep_hash.h:59
std::unordered_map< exprt, mini_bddt, irep_hash > expr_mapt
Definition: bdd_expr.h:45
expr_mapt expr_map
Definition: bdd_expr.h:46
mini_bdd_mgrt bdd_mgr
Definition: bdd_expr.h:42
TO_BE_DOCUMENTED.
Definition: namespace.h:74
mini_bddt from_expr_rec(const exprt &expr)
Definition: bdd_expr.cpp:20
TO_BE_DOCUMENTED.
Definition: bdd_expr.h:32
exprt as_expr() const
Definition: bdd_expr.cpp:140
const namespacet & ns
Definition: bdd_expr.h:41
mini_bddt root
Definition: bdd_expr.h:43
void from_expr(const exprt &expr)
Definition: bdd_expr.cpp:99
std::map< unsigned, exprt > node_mapt
Definition: bdd_expr.h:47
Base class for all expressions.
Definition: expr.h:42
A minimalistic BDD library, following Bryant&#39;s original paper and Andersen&#39;s lecture notes...
bdd_exprt(const namespacet &_ns)
Definition: bdd_expr.h:35
node_mapt node_map
Definition: bdd_expr.h:48