z3_expr_adapter.h

Go to the documentation of this file.

#ifndef ILANG_TARGET_SMT_Z3_EXPR_ADAPTER_H__
#define ILANG_TARGET_SMT_Z3_EXPR_ADAPTER_H__

#include <unordered_map>

#include <z3++.h>

#include <ilang/ila/ast_hub.h>

namespace ilang {

typedef ExprHash Z3AdapterHash;

class Z3ExprAdapter {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  Z3ExprAdapter(z3::context& ctx);
  ~Z3ExprAdapter();

  // ------------------------- METHODS -------------------------------------- //
  z3::expr GetExpr(const ExprPtr& expr, const std::string& suffix = "");

  void operator()(const ExprPtr& expr);

  inline z3::context& context() const { return ctx_; }

  // ------------------------- SHIM INTERFACE ------------------------------- //
  inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix) {
    return GetExpr(expr, suffix);
  }
  inline auto GetShimFunc(const FuncPtr& func) {
    return func->GetZ3FuncDecl(ctx_);
  }
  inline auto BoolAnd(const z3::expr& a, const z3::expr& b) { return a && b; }
  inline auto Equal(const z3::expr& a, const z3::expr& b) { return a == b; }

private:
  typedef std::unordered_map<const ExprPtr, z3::expr, Z3AdapterHash> ExprMap;

  // ------------------------- MEMBERS -------------------------------------- //
  z3::context& ctx_;
  ExprMap expr_map_;
  std::string suffix_ = "";

  // ------------------------- HELPERS -------------------------------------- //
  void PopulateExprMap(const ExprPtr& expr);

}; // class Z3ExprAdapter

} // namespace ilang

#endif // ILANG_TARGET_SMT_Z3_EXPR_ADAPTER_H__