guard_bdd.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Guard Data Structure
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/

 
#ifndef CPROVER_ANALYSES_GUARD_BDD_H
#define CPROVER_ANALYSES_GUARD_BDD_H
 
#include <solvers/bdd/bdd.h> // IWYU pragma: keep
 
class bdd_exprt;
class exprt;
 
class guard_bddt
{
public:
  guard_bddt(const exprt &e, bdd_exprt &manager);
  guard_bddt(const guard_bddt &other) : manager(other.manager), bdd(other.bdd)
  {
  }
 
  guard_bddt &operator=(const guard_bddt &other);
  guard_bddt &operator=(guard_bddt &&other);
  guard_bddt &add(const exprt &expr);
  guard_bddt &append(const guard_bddt &guard);
  exprt as_expr() const;

  static constexpr bool is_always_simplified = true;

  exprt guard_expr(exprt expr) const;
 
  bool is_true() const
  {
    return bdd.is_true();
  }
 
  bool is_false() const
  {
    return bdd.is_false();
  }

  friend guard_bddt &operator-=(guard_bddt &g1, const guard_bddt &g2);
 
  friend guard_bddt &operator|=(guard_bddt &g1, const guard_bddt &g2);
 
  guard_bddt operator!() const
  {
    return guard_bddt(manager, bdd.bdd_not());
  }

  bool disjunction_may_simplify(const guard_bddt &other_guard)
  {
    return true;
  }
 
private:
  bdd_exprt &manager;
  bddt bdd;
 
  guard_bddt(bdd_exprt &manager, bddt bdd)
    : manager(manager), bdd(std::move(bdd))
  {
  }
};
 
#endif // CPROVER_ANALYSES_GUARD_BDD_H