expr.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Expression Representation
 
Author: Daniel Kroening, kroening@kroening.com
        Joel Allred, joel.allred@diffblue.com
 
\*******************************************************************/
 
 
#include "arith_tools.h"
#include "bitvector_types.h"
#include "expr_iterator.h"
#include "expr_util.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "rational.h"
#include "rational_tools.h"
#include "std_expr.h"
 
#include <stack>
 
bool exprt::is_true() const
{
  return *this == true;
}
 
bool exprt::is_false() const
{
  return *this == false;
}
 
bool exprt::is_zero() const
{
  return *this == 0;
}
 
bool exprt::is_one() const
{
  return *this == 1;
}
 
const source_locationt &exprt::find_source_location() const
{
  const source_locationt &l=source_location();
 
  if(l.is_not_nil())
    return l;
 
  for(const auto &op : operands())
  {
    const source_locationt &op_l = op.find_source_location();
    if(op_l.is_not_nil())
      return op_l;
  }
 
  return source_locationt::nil();
}
 
template <typename T>
void visit_post_template(std::function<void(T &)> visitor, T *_expr)
{
  struct stack_entryt
  {
    T *e;
    bool operands_pushed;
    explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
    {
    }
  };
 
  std::stack<stack_entryt> stack;
 
  stack.emplace(_expr);
 
  while(!stack.empty())
  {
    auto &top = stack.top();
    if(top.operands_pushed)
    {
      visitor(*top.e);
      stack.pop();
    }
    else
    {
      // do modification of 'top' before pushing in case 'top' isn't stable
      top.operands_pushed = true;
      for(auto &op : top.e->operands())
        stack.emplace(&op);
    }
  }
}
 
void exprt::visit_post(std::function<void(exprt &)> visitor)
{
  visit_post_template(visitor, this);
}
 
void exprt::visit_post(std::function<void(const exprt &)> visitor) const
{
  visit_post_template(visitor, this);
}
 
template <typename T>
static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
{
  std::stack<T *> stack;
 
  stack.push(_expr);
 
  while(!stack.empty())
  {
    T &expr = *stack.top();
    stack.pop();
 
    visitor(expr);
 
    for(auto &op : expr.operands())
      stack.push(&op);
  }
}
 
void exprt::visit_pre(std::function<void(exprt &)> visitor)
{
  visit_pre_template(visitor, this);
}
 
void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
{
  visit_pre_template(visitor, this);
}
 
void exprt::visit(expr_visitort &visitor)
{
  visit_pre([&visitor](exprt &e) { visitor(e); });
}
 
void exprt::visit(const_expr_visitort &visitor) const
{
  visit_pre([&visitor](const exprt &e) { visitor(e); });
}
 
depth_iteratort exprt::depth_begin()
{ return depth_iteratort(*this); }
depth_iteratort exprt::depth_end()
{ return depth_iteratort(); }
const_depth_iteratort exprt::depth_begin() const
{ return const_depth_iteratort(*this); }
const_depth_iteratort exprt::depth_end() const
{ return const_depth_iteratort(); }
const_depth_iteratort exprt::depth_cbegin() const
{ return const_depth_iteratort(*this); }
const_depth_iteratort exprt::depth_cend() const
{ return const_depth_iteratort(); }
depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
{
  return depth_iteratort(*this, std::move(mutate_root));
}
 
const_unique_depth_iteratort exprt::unique_depth_begin() const
{ return const_unique_depth_iteratort(*this); }
const_unique_depth_iteratort exprt::unique_depth_end() const
{ return const_unique_depth_iteratort(); }
const_unique_depth_iteratort exprt::unique_depth_cbegin() const
{ return const_unique_depth_iteratort(*this); }
const_unique_depth_iteratort exprt::unique_depth_cend() const
{ return const_unique_depth_iteratort(); }