guard_expr.cpp

/*******************************************************************\

Module: Symbolic Execution

Author: Daniel Kroening, kroening@kroening.com

\*******************************************************************/

/// \file
/// Symbolic Execution

#include "guard_expr.h"

#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/std_expr.h>

exprt guard_exprt::guard_expr(exprt expr) const
{
  if(is_true())
  {
    // do nothing
    return expr;
  }
  else
  {
    if(expr.is_constant() && to_constant_expr(expr).is_false())
    {
      return boolean_negate(as_expr());
    }
    else
    {
      return implies_exprt{as_expr(), expr};
    }
  }
}

void guard_exprt::add(const exprt &expr)
{
  PRECONDITION(expr.is_boolean());

  if(is_false() || (expr.is_constant() && to_constant_expr(expr).is_true()))
    return;
  else if(
    is_true() || (expr.is_constant() && to_constant_expr(expr).is_false()))
  {
    this->expr = expr;

    return;
  }
  else if(this->expr.id() != ID_and)
  {
    and_exprt a({this->expr});
    this->expr = a;
  }

  exprt::operandst &op = this->expr.operands();

  if(expr.id() == ID_and)
    op.insert(op.end(), expr.operands().begin(), expr.operands().end());
  else
    op.push_back(expr);
}

guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2)
{
  if(g1.expr.id() != ID_and)
  {
    if(g2.expr.id() != ID_and)
    {
      if(g1.expr == g2.expr)
        g1.expr = true_exprt{};
    }
    else
    {
      for(const auto &op : g2.expr.operands())
      {
        if(g1.expr == op)
        {
          g1.expr = true_exprt{};
          break;
        }
      }
    }

    return g1;
  }

  if(g2.expr.id() != ID_and)
  {
    exprt::operandst &op1 = g1.expr.operands();
    for(exprt::operandst::iterator it = op1.begin(); it != op1.end(); ++it)
    {
      if(g1.expr == g2.expr)
      {
        op1.erase(it);
        break;
      }
    }

    return g1;
  }

  exprt g2_sorted = g2.as_expr();

  exprt::operandst &op1 = g1.expr.operands();
  const exprt::operandst &op2 = g2_sorted.operands();

  exprt::operandst::iterator it1 = op1.begin();
  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
      ++it2)
  {
    if(it1 != op1.end() && *it1 == *it2)
      it1 = op1.erase(it1);
    else
      break;
  }

  g1.expr = conjunction(op1);

  return g1;
}

bool guard_exprt::disjunction_may_simplify(const guard_exprt &other_guard)
{
  if(is_true() || is_false() || other_guard.is_true() || other_guard.is_false())
    return true;
  if(expr.id() == ID_and && other_guard.expr.id() == ID_and)
    return true;
  if(other_guard.expr == boolean_negate(expr))
    return true;
  return false;
}

guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2)
{
  if(g2.is_false() || g1.is_true())
    return g1;
  if(g1.is_false() || g2.is_true())
  {
    g1.expr = g2.expr;
    return g1;
  }

  if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
  {
    exprt tmp(boolean_negate(g2.as_expr()));

    if(tmp == g1.as_expr())
      g1.expr = true_exprt();
    else
      g1.expr = or_exprt(g1.as_expr(), g2.as_expr());

    // TODO: make simplify more capable and apply here

    return g1;
  }

  // find common prefix
  exprt g2_sorted = g2.as_expr();

  exprt::operandst &op1 = g1.expr.operands();
  const exprt::operandst &op2 = g2_sorted.operands();

  exprt::operandst n_op1, n_op2;
  n_op1.reserve(op1.size());
  n_op2.reserve(op2.size());

  exprt::operandst::iterator it1 = op1.begin();
  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
      ++it2)
  {
    while(it1 != op1.end() && *it1 < *it2)
    {
      n_op1.push_back(*it1);
      it1 = op1.erase(it1);
    }
    if(it1 != op1.end() && *it1 == *it2)
      ++it1;
    else
      n_op2.push_back(*it2);
  }
  while(it1 != op1.end())
  {
    n_op1.push_back(*it1);
    it1 = op1.erase(it1);
  }

  if(n_op2.empty())
    return g1;

  // end of common prefix
  exprt and_expr1 = conjunction(n_op1);
  exprt and_expr2 = conjunction(n_op2);

  g1.expr = conjunction(op1);

  exprt tmp(boolean_negate(and_expr2));

  if(tmp != and_expr1)
  {
    if(
      (and_expr1.is_constant() && to_constant_expr(and_expr1).is_true()) ||
      (and_expr2.is_constant() && to_constant_expr(and_expr2).is_true()))
    {
    }
    else
      // TODO: make simplify more capable and apply here
      g1.add(or_exprt(and_expr1, and_expr2));
  }

  return g1;
}