expr.h

Go to the documentation of this file.

#ifndef ILANG_ILA_AST_EXPR_H__
#define ILANG_ILA_AST_EXPR_H__

#include <memory>
#include <ostream>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <vector>

#include <z3++.h>
#include <z3_api.h>

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

namespace ilang {

class Expr : public Ast, public std::enable_shared_from_this<Expr> {
public:
  typedef std::shared_ptr<Expr> ExprPtr;
  typedef std::vector<ExprPtr> ExprPtrVec;

protected:
  typedef std::vector<z3::expr> Z3ExprVec;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  Expr();
  Expr(const std::string& name);
  virtual ~Expr();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  inline const SortPtr sort() const { return sort_; }
  inline size_t arg_num() const { return args_.size(); }
  inline ExprPtr arg(const size_t& i) const { return args_.at(i); }
  inline size_t param_num() const { return params_.size(); }
  inline int param(const size_t& i) const { return params_.at(i); }

  void set_sort(const SortPtr sort);
  void set_args(const ExprPtrVec& args);
  void set_params(const std::vector<int> params);
  void replace_arg(const int& idx, const ExprPtr& arg);
  void replace_arg(const ExprPtr& a, const ExprPtr& b);

  bool is_expr() const { return true; }

  virtual bool is_const() const { return false; }
  virtual bool is_var() const { return false; }
  virtual bool is_op() const { return false; }

  inline bool is_bool() const { return sort_->is_bool(); }
  inline bool is_bv(const int& width = 0) const { return sort_->is_bv(width); }
  inline bool is_mem() const { return sort_->is_mem(); }

  // ------------------------- METHODS -------------------------------------- //
  virtual z3::expr GetZ3Expr(z3::context& z3_ctx, const Z3ExprVec& z3expr_vec,
                             const std::string& suffix = "") const = 0;

  virtual std::ostream& Print(std::ostream& out) const = 0;

  friend std::ostream& operator<<(std::ostream& out, const ExprPtr& expr) {
    return expr->Print(out);
  }

  template <class F> void DepthFirstVisit(F& func) {
    for (size_t i = 0; i != arg_num(); i++) {
      auto arg_i = this->arg(i);
      arg_i->DepthFirstVisit<F>(func);
    }
    func(shared_from_this());
  }

  template <class F> void DepthFirstVisitPrePost(F& func) {
    // pre check
    if (func.pre(shared_from_this())) { // break if return true
      return;
    }
    // traverse child
    for (size_t i = 0; i != arg_num(); i++) {
      auto arg_i = this->arg(i);
      arg_i->DepthFirstVisitPrePost<F>(func);
    }
    // post
    func.post(shared_from_this());
  }

private:
  // ------------------------- MEMBERS -------------------------------------- //
  SortPtr sort_;
  ExprPtrVec args_;
  std::vector<int> params_;

  // ------------------------- HELPERS -------------------------------------- //

}; // class Expr

typedef Expr::ExprPtr ExprPtr;
typedef Expr::ExprPtrVec ExprPtrVec;

class ExprHash {
public:
  size_t operator()(const ExprPtr& expr) const { return expr->name().id(); }
}; // class ExprHash

typedef std::unordered_map<const ExprPtr, const ExprPtr, ExprHash> ExprMap;
typedef std::unordered_set<ExprPtr, ExprHash> ExprSet;

} // namespace ilang

#endif // ILANG_ILA_AST_EXPR_H__