sort.h

Go to the documentation of this file.

#ifndef ILANG_ILA_AST_SORT_H__
#define ILANG_ILA_AST_SORT_H__

#include <memory>
#include <ostream>

#include <z3++.h>

#include <ilang/ila/ast/ast.h>

namespace ilang {

enum AstUidSort { kBool = 1, kBv, kMem };

class Sort : public Ast {
public:
  typedef std::shared_ptr<Sort> SortPtr;

  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  Sort();
  virtual ~Sort();

  // ------------------------- HELPERS -------------------------------------- //
  static SortPtr MakeBoolSort();
  static SortPtr MakeBvSort(const int& bit_width);
  static SortPtr MakeMemSort(const int& addr_width, const int& data_width);

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  virtual AstUidSort uid() const = 0;
  virtual bool is_bool() const { return false; }
  virtual bool is_bv(const int& width = 0) const { return false; }
  virtual bool is_mem() const { return false; }

  virtual int bit_width() const;
  virtual int addr_width() const;
  virtual int data_width() const;

  // ------------------------- METHODS -------------------------------------- //
  virtual z3::sort GetZ3Sort(z3::context& ctx) const = 0;
  virtual z3::expr GetZ3Expr(z3::context& ctx,
                             const std::string& name) const = 0;

  virtual bool Equal(const SortPtr rhs) const = 0;
  friend bool operator==(const SortPtr lhs, const SortPtr rhs) {
    return lhs->Equal(rhs);
  }

  virtual std::ostream& Print(std::ostream& out) const = 0;
  friend std::ostream& operator<<(std::ostream& out, const SortPtr s) {
    return s->Print(out);
  }

}; // class Sort

typedef Sort::SortPtr SortPtr;

class SortBool : public Sort {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  SortBool();
  ~SortBool();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  AstUidSort uid() const { return AstUidSort::kBool; }
  bool is_bool() const { return true; }

  // ------------------------- METHODS -------------------------------------- //
  z3::sort GetZ3Sort(z3::context& ctx) const;
  z3::expr GetZ3Expr(z3::context& ctx, const std::string& name) const;
  bool Equal(const SortPtr rhs) const;
  std::ostream& Print(std::ostream& out) const;
}; // class SortBool

class SortBv : public Sort {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  SortBv(const int& width);
  ~SortBv();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  AstUidSort uid() const { return AstUidSort::kBv; }
  bool is_bv(const int& width) const {
    return (width == 0) ? true : (width == bit_width_);
  }

  // ------------------------- METHODS -------------------------------------- //
  int bit_width() const { return bit_width_; }
  z3::sort GetZ3Sort(z3::context& ctx) const;
  z3::expr GetZ3Expr(z3::context& ctx, const std::string& name) const;
  bool Equal(const SortPtr rhs) const;
  std::ostream& Print(std::ostream& out) const;

private:
  int bit_width_;
}; // class SortBv

class SortMem : public Sort {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  SortMem(const int& addr_w, const int& data_w);
  ~SortMem();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  AstUidSort uid() const { return AstUidSort::kMem; }
  bool is_mem() const { return true; }

  // ------------------------- METHODS -------------------------------------- //
  int addr_width() const { return addr_width_; }
  int data_width() const { return data_width_; }
  z3::sort GetZ3Sort(z3::context& ctx) const;
  z3::expr GetZ3Expr(z3::context& ctx, const std::string& name) const;
  bool Equal(const SortPtr rhs) const;
  std::ostream& Print(std::ostream& out) const;

private:
  int addr_width_;
  int data_width_;
}; // class SortMem

} // namespace ilang

#endif // ILANG_ILA_AST_SORT_H__