func.h

Go to the documentation of this file.

#ifndef ILANG_ILA_AST_FUNC_H__
#define ILANG_ILA_AST_FUNC_H__

#include <memory>
#include <string>
#include <vector>

#include <z3++.h>

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

namespace ilang {

// Forward declaration.
class Expr;

class Func : public Ast {
public:
  typedef std::shared_ptr<Func> FuncPtr;

  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  Func(const std::string& name, const SortPtr out,
       const std::vector<SortPtr>& args);

  ~Func();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  const SortPtr out() const { return out_; }
  size_t arg_num() const { return args_.size(); }
  const SortPtr arg(const int& i) const { return args_.at(i); }

  // ------------------------- METHODS -------------------------------------- //
  static FuncPtr New(const std::string& name,
                     const SortPtr out = Sort::MakeBoolSort());
  static FuncPtr New(const std::string& name, const SortPtr out,
                     const SortPtr arg0);
  static FuncPtr New(const std::string& name, const SortPtr out,
                     const SortPtr arg0, const SortPtr arg1);
  static FuncPtr New(const std::string& name, const SortPtr out,
                     const std::vector<SortPtr>& args);

  bool CheckSort(const std::vector<std::shared_ptr<Expr>>& args) const;

  z3::func_decl GetZ3FuncDecl(z3::context& ctx) const;

  std::ostream& Print(std::ostream& out) const;

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

private:
  // ------------------------- MEMBERS -------------------------------------- //
  SortPtr out_;
  std::vector<SortPtr> args_;

  // ------------------------- HELPERS -------------------------------------- //
}; // class Func

typedef Func::FuncPtr FuncPtr;

class FuncHash {
public:
  size_t operator()(const FuncPtr& func) const { return func->name().id(); }
}; // class FuncHash

} // namespace ilang

#endif // ILANG_ILA_AST_FUNC_H__