boolbv_quantifier.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/simplify_expr.h>
 
#include "boolbv.h"
 
static bool expr_eq(const exprt &expr1, const exprt &expr2)
{
  return skip_typecast(expr1) == skip_typecast(expr2);
}
 
static std::optional<constant_exprt>
get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
{
  if(quantifier_expr.id()==ID_or)
  {
    for(auto &x : quantifier_expr.operands())
    {
      if(x.id()!=ID_not)
        continue;
      exprt y = to_not_expr(x).op();
      if(y.id()!=ID_ge)
        continue;
      const auto &y_binary = to_binary_relation_expr(y);
      if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
      {
        return to_constant_expr(y_binary.rhs());
      }
    }
 
    if(var_expr.type().id() == ID_unsignedbv)
      return from_integer(0, var_expr.type());
  }
  else if(quantifier_expr.id() == ID_and)
  {
    // The minimum variable can be of the form `var_expr >= constant`, or
    // it can be of the form `var_expr == constant` (e.g. in the case where
    // the interval that bounds the variable is a singleton interval (set
    // with only one element)).
    for(auto &x : quantifier_expr.operands())
    {
      if(x.id() != ID_ge && x.id() != ID_equal)
        continue;
      const auto &x_binary = to_binary_relation_expr(x);
      if(expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().is_constant())
      {
        return to_constant_expr(x_binary.rhs());
      }
    }
 
    if(var_expr.type().id() == ID_unsignedbv)
      return from_integer(0, var_expr.type());
  }
 
  return {};
}
 
static std::optional<constant_exprt>
get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
{
  if(quantifier_expr.id()==ID_or)
  {
    for(auto &x : quantifier_expr.operands())
    {
      if(x.id()!=ID_ge)
        continue;
      const auto &x_binary = to_binary_relation_expr(x);
      if(expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().is_constant())
      {
        const constant_exprt &over_expr = to_constant_expr(x_binary.rhs());
 
        mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
 
        over_i-=1;
        return from_integer(over_i, x_binary.rhs().type());
      }
    }
  }
  else
  {
    // There are two potential forms we could come across here. The first one
    // is `!(var_expr >= constant)` - identified by the first if branch - and
    // the second is `var_expr == constant` - identified by the second else-if
    // branch. The second form could be met if previous simplification has
    // identified a singleton interval - see simplify_boolean_expr.cpp.
    for(auto &x : quantifier_expr.operands())
    {
      if(x.id() == ID_not)
      {
        exprt y = to_not_expr(x).op();
        if(y.id() != ID_ge)
          continue;
        const auto &y_binary = to_binary_relation_expr(y);
        if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
        {
          const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
          mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
          over_i -= 1;
          return from_integer(over_i, y_binary.rhs().type());
        }
      }
      else if(x.id() == ID_equal)
      {
        const auto &y_binary = to_binary_relation_expr(x);
        if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
        {
          return to_constant_expr(y_binary.rhs());
        }
      }
      else
      {
        // If you need special handling for a particular expression type (say,
        // after changes to the simplifier) you need to make sure that you add
        // an `else if` branch above, otherwise the expression will get skipped
        // and the constraints will not propagate correctly.
        continue;
      }
    }
  }
 
  return {};
}
 
static std::optional<exprt> eager_quantifier_instantiation(
  const quantifier_exprt &expr,
  const namespacet &ns)
{
  if(expr.variables().size() > 1)
  {
    // Qx,y.P(x,y) is the same as Qx.Qy.P(x,y)
    auto new_variables = expr.variables();
    new_variables.pop_back();
    auto new_expression = quantifier_exprt(
      expr.id(),
      expr.variables().back(),
      quantifier_exprt(expr.id(), new_variables, expr.where()));
    return eager_quantifier_instantiation(new_expression, ns);
  }
 
  const symbol_exprt &var_expr = expr.symbol();
 
  const exprt where_simplified = simplify_expr(expr.where(), ns);
 
  if(
    (where_simplified.is_true() || where_simplified.is_false()) &&
    (var_expr.type().id() == ID_integer ||
     var_expr.type().id() == ID_rational || var_expr.type().id() == ID_real ||
     var_expr.type().id() == ID_bool ||
     (can_cast_type<bitvector_typet>(var_expr.type()) &&
      to_bitvector_type(var_expr.type()).get_width() > 0)))
  {
    return where_simplified;
  }
 
  if(var_expr.is_boolean())
  {
    // Expand in full.
    // This grows worst-case exponentially in the quantifier nesting depth.
    if(expr.id() == ID_forall)
    {
      // ∀b.f(b) <===> f(0)∧f(1)
      return and_exprt(
        expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
    }
    else if(expr.id() == ID_exists)
    {
      // ∃b.f(b) <===> f(0)∨f(1)
      return or_exprt(
        expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
    }
    else
      UNREACHABLE;
  }
 
  const std::optional<constant_exprt> min_i =
    get_quantifier_var_min(var_expr, where_simplified);
  const std::optional<constant_exprt> max_i =
    get_quantifier_var_max(var_expr, where_simplified);
 
  if(!min_i.has_value() || !max_i.has_value())
    return {};
 
  mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
  mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
 
  if(lb > ub)
    return {};
 
  auto expr_simplified =
    quantifier_exprt(expr.id(), expr.variables(), where_simplified);
 
  std::vector<exprt> expr_insts;
  for(mp_integer i = lb; i <= ub; ++i)
  {
    exprt constraint_expr =
      expr_simplified.instantiate({from_integer(i, var_expr.type())});
    expr_insts.push_back(constraint_expr);
  }
 
  if(expr.id() == ID_forall)
  {
    // maintain the domain constraint if it isn't guaranteed
    // by the instantiations (for a disjunction the domain
    // constraint is implied by the instantiations)
    if(where_simplified.id() == ID_and)
    {
      expr_insts.push_back(binary_predicate_exprt(
        var_expr, ID_gt, from_integer(lb, var_expr.type())));
      expr_insts.push_back(binary_predicate_exprt(
        var_expr, ID_le, from_integer(ub, var_expr.type())));
    }
 
    return simplify_expr(conjunction(expr_insts), ns);
  }
  else if(expr.id() == ID_exists)
  {
    // maintain the domain constraint if it isn't trivially satisfied
    // by the instantiations (for a conjunction the instantiations are
    // stronger constraints)
    if(where_simplified.id() == ID_or)
    {
      expr_insts.push_back(binary_predicate_exprt(
        var_expr, ID_gt, from_integer(lb, var_expr.type())));
      expr_insts.push_back(binary_predicate_exprt(
        var_expr, ID_le, from_integer(ub, var_expr.type())));
    }
 
    return simplify_expr(disjunction(expr_insts), ns);
  }
 
  UNREACHABLE;
}
 
literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
{
  PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
 
  // We first worry about the scoping of the symbols bound by the quantifier.
  auto fresh_symbols = fresh_binding(src);
 
  // replace in where()
  auto where_replaced = src.instantiate(fresh_symbols);
 
  // produce new quantifier expression
  auto new_src =
    quantifier_exprt(src.id(), std::move(fresh_symbols), where_replaced);
 
  const auto res = eager_quantifier_instantiation(src, ns);
 
  if(res)
    return convert_bool(*res);
 
  // we failed to instantiate here, need to pass to post-processing
  quantifier_list.emplace_back(quantifiert(src, prop.new_variable()));
 
  return quantifier_list.back().l;
}
 
void boolbvt::finish_eager_conversion_quantifiers()
{
  if(quantifier_list.empty())
    return;
 
  // we do not yet have any elaborate post-processing
  for(const auto &q : quantifier_list)
    conversion_failed(q.expr);
}