smt_sort.h

Go to the documentation of this file.

#ifndef SOLVERS_SMT_SMT_SORT_H_
#define SOLVERS_SMT_SMT_SORT_H_
 
#include <irep2/irep2_type.h>

enum smt_sort_kind
{
  SMT_SORT_INT,
  SMT_SORT_REAL,
  SMT_SORT_BV,
  SMT_SORT_FIXEDBV,
  SMT_SORT_ARRAY,
  SMT_SORT_BOOL,
  SMT_SORT_STRUCT,
  SMT_SORT_BVFP,
  SMT_SORT_FPBV,
  SMT_SORT_BVFP_RM,
  SMT_SORT_FPBV_RM,
};

 
class smt_sort;
typedef const smt_sort *smt_sortt;
 
class smt_sort
{
public:
  smt_sort_kind id;
 
  smt_sort(smt_sort_kind i)
    : id(i), data_width(0), secondary_width(0), range_sort(nullptr)
  {
    assert(id != SMT_SORT_ARRAY);
  }
 
  smt_sort(smt_sort_kind i, const type2tc &type)
    : id(i),
      data_width(0),
      secondary_width(0),
      range_sort(nullptr),
      tupletype(type)
  {
    assert(i == SMT_SORT_STRUCT);
  }
 
  smt_sort(smt_sort_kind i, std::size_t width)
    : id(i), data_width(width), secondary_width(0), range_sort(nullptr)
  {
    assert(id >= SMT_SORT_BV || id <= SMT_SORT_FIXEDBV);
  }
 
  smt_sort(smt_sort_kind i, std::size_t width, std::size_t sigwidth)
    : id(i), data_width(width), secondary_width(sigwidth), range_sort(nullptr)
  {
    assert(id == SMT_SORT_BVFP || id == SMT_SORT_FPBV);
  }
 
  smt_sort(smt_sort_kind i, std::size_t dom_width, smt_sortt range_sort)
    : id(i), data_width(dom_width), secondary_width(0), range_sort(range_sort)
  {
    assert(id == SMT_SORT_ARRAY);
  }
 
  smt_sort(
    smt_sort_kind i,
    const type2tc &type,
    std::size_t dom_width,
    smt_sortt range_sort)
    : id(i),
      data_width(dom_width),
      secondary_width(0),
      range_sort(range_sort),
      tupletype(type)
  {
    assert(i == SMT_SORT_ARRAY);
  }
 
  size_t get_data_width() const
  {
    if (id == SMT_SORT_ARRAY)
      return data_width * range_sort->data_width;
    return data_width;
  }
 
  size_t get_domain_width() const
  {
    assert(id == SMT_SORT_ARRAY);
    return data_width;
  }
 
  smt_sortt get_range_sort() const
  {
    assert(id == SMT_SORT_ARRAY);
    assert(range_sort != nullptr);
    return range_sort;
  }
 
  size_t get_significand_width() const
  {
    assert(id == SMT_SORT_BVFP || id == SMT_SORT_FPBV);
    return secondary_width;
  }
 
  size_t get_exponent_width() const
  {
    assert(id == SMT_SORT_BVFP || id == SMT_SORT_FPBV);
    std::size_t exp_top = get_data_width() - 2;
    std::size_t exp_bot = get_significand_width() - 2;
    return (exp_top - exp_bot);
  }
 
  const type2tc &get_tuple_type() const
  {
    assert(!is_nil_type(tupletype));
    return tupletype;
  }
 
  virtual ~smt_sort() = default;
 
private:
  size_t data_width;

  size_t secondary_width;

  smt_sortt range_sort;

  const type2tc tupletype;
};
 
template <typename solver_sort>
class solver_smt_sort : public smt_sort
{
public:
  solver_smt_sort(smt_sort_kind i, solver_sort _s) : smt_sort(i), s(_s)
  {
  }
 
  solver_smt_sort(smt_sort_kind i, solver_sort _s, const type2tc &_tupletype)
    : smt_sort(i, _tupletype), s(_s)
  {
  }
 
  solver_smt_sort(smt_sort_kind i, solver_sort _s, unsigned int w)
    : smt_sort(i, w), s(_s)
  {
  }
 
  solver_smt_sort(
    smt_sort_kind i,
    solver_sort _s,
    unsigned int w,
    unsigned int sw)
    : smt_sort(i, w, sw), s(_s)
  {
  }
 
  solver_smt_sort(
    smt_sort_kind i,
    solver_sort _s,
    std::size_t dw,
    const smt_sort *_rangesort)
    : smt_sort(i, dw, _rangesort), s(_s)
  {
  }
 
  solver_smt_sort(
    smt_sort_kind i,
    solver_sort _s,
    const type2tc &type,
    std::size_t width,
    smt_sortt range_sort)
    : smt_sort(i, type, width, range_sort), s(_s)
  {
  }
 
  ~solver_smt_sort() override = default;
 
  solver_sort s;
};
 
#ifdef NDEBUG
#  define dynamic_cast static_cast
#endif
template <typename T>
const solver_smt_sort<T> *to_solver_smt_sort(smt_sortt s)
{
  const solver_smt_sort<T> *r = dynamic_cast<const solver_smt_sort<T> *>(s);
  assert(r);
  return r;
}
#ifdef dynamic_cast
#  undef dynamic_cast
#endif
 
#endif /* SOLVERS_SMT_SMT_SORT_H_ */