smt_shim.h

Go to the documentation of this file.

#ifndef ILANG_TARGET_SMT_SMT_SHIM_H__
#define ILANG_TARGET_SMT_SMT_SHIM_H__

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

namespace ilang {

template <class Generator> class SmtShim {
public:
  SmtShim(Generator& gen) : gen_(gen) {}

private:
  Generator& gen_;
  typedef decltype(gen_.GetShimExpr(nullptr, "")) ShimExprType;

public:
  inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix = "") {
    return gen_.GetShimExpr(expr, suffix);
  }
  inline auto GetShimFunc(const FuncPtr& func) {
    return gen_.GetShimFunc(func);
  }
  inline auto BoolAnd(const ShimExprType& a, const ShimExprType& b) {
    return gen_.BoolAnd(a, b);
  }
  inline auto Equal(const ShimExprType& a, const ShimExprType& b) {
    return gen_.Equal(a, b);
  }
  inline Generator& get() const { return gen_; }

}; // class SmtShim

} // namespace ilang

#endif // ILANG_TARGET_SMT_SMT_SHIM_H__