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 class namespacet;
27 
30 class bdd_exprt
31 {
32 public:
33  explicit bdd_exprt(const namespacet &_ns):ns(_ns) { }
34 
35  void from_expr(const exprt &expr);
36  exprt as_expr() const;
37 
38 protected:
39  const namespacet &ns;
42 
43  typedef std::unordered_map<exprt, mini_bddt, irep_hash> expr_mapt;
44  expr_mapt expr_map;
45  typedef std::map<unsigned, exprt> node_mapt;
46  node_mapt node_map;
47 
48  mini_bddt from_expr_rec(const exprt &expr);
49  exprt as_expr(const mini_bddt &r) const;
50 };
51 
52 #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:43
expr_mapt expr_map
Definition: bdd_expr.h:44
mini_bdd_mgrt bdd_mgr
Definition: bdd_expr.h:40
TO_BE_DOCUMENTED.
Definition: namespace.h:62
mini_bddt from_expr_rec(const exprt &expr)
Definition: bdd_expr.cpp:19
TO_BE_DOCUMENTED.
Definition: bdd_expr.h:30
exprt as_expr() const
Definition: bdd_expr.cpp:138
const namespacet & ns
Definition: bdd_expr.h:39
mini_bddt root
Definition: bdd_expr.h:41
void from_expr(const exprt &expr)
Definition: bdd_expr.cpp:97
std::map< unsigned, exprt > node_mapt
Definition: bdd_expr.h:45
Base class for all expressions.
Definition: expr.h:46
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:33
node_mapt node_map
Definition: bdd_expr.h:46