guard_expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Guard Data Structure
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#ifndef CPROVER_ANALYSES_GUARD_EXPR_H
#define CPROVER_ANALYSES_GUARD_EXPR_H
 
#include <util/std_expr.h>

struct guard_expr_managert
{
};
 
class guard_exprt
{
public:
  explicit guard_exprt(const exprt &e, guard_expr_managert &) : expr(e)
  {
  }
 
  guard_exprt &operator=(const guard_exprt &other)
  {
    expr = other.expr;
    return *this;
  }
 
  void add(const exprt &expr);
 
  void append(const guard_exprt &guard)
  {
    add(guard.as_expr());
  }
 
  exprt as_expr() const
  {
    return expr;
  }

  static constexpr bool is_always_simplified = false;

  exprt guard_expr(exprt expr) const;
 
  bool is_true() const
  {
    return expr == true;
  }
 
  bool is_false() const
  {
    return expr == false;
  }
 
  friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);
  friend guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2);

  bool disjunction_may_simplify(const guard_exprt &other_guard);
 
private:
  exprt expr;
};
 
#endif // CPROVER_ANALYSES_GUARD_EXPR_H