bdd_expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Conversion between exprt and miniBDD
 
Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk
 
\*******************************************************************/

 
#ifndef CPROVER_SOLVERS_PROP_BDD_EXPR_H
#define CPROVER_SOLVERS_PROP_BDD_EXPR_H

 
#include <util/expr.h>
 
#include <solvers/bdd/bdd.h> // IWYU pragma: keep
 
#include <unordered_map>

class bdd_exprt
{
public:
  bddt from_expr(const exprt &expr);
  exprt as_expr(const bddt &root) const;
 
protected:
  bdd_managert bdd_mgr;
 
  typedef std::unordered_map<exprt, bddt, irep_hash> expr_mapt;
 
  expr_mapt expr_map;

  std::vector<exprt> node_map;
 
  bddt from_expr_rec(const exprt &expr);
  exprt as_expr(
    const bdd_nodet &r,
    std::unordered_map<bdd_nodet::idt, exprt> &cache) const;
};
 
#endif // CPROVER_SOLVERS_PROP_BDD_EXPR_H