smt_switch_itf.h

Go to the documentation of this file.

#ifndef ILANG_ILA_MNGR_U_SMT_SWITCH_H__
#define ILANG_ILA_MNGR_U_SMT_SWITCH_H__

#ifdef SMTSWITCH_INTERFACE

#include <string>
#include <unordered_map>

#include <smt-switch/smt.h>

#include <ilang/ila/ast_hub.h>

namespace ilang {

class SmtSwitchItf {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  SmtSwitchItf(smt::SmtSolver& solver);
  ~SmtSwitchItf();

  // ------------------------- METHODS -------------------------------------- //
  smt::Term GetSmtTerm(const ExprPtr& expr, const std::string& suffix = "");
  void Reset();
  inline smt::SmtSolver& solver() const { return solver_; }

  bool pre(const ExprPtr& expr);
  void post(const ExprPtr& expr);

  // ------------------------- SHIM INTERFACE ------------------------------- //
  inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix) {
    return GetSmtTerm(expr, suffix);
  }
  inline auto GetShimFunc(const FuncPtr& func) { return Func2Term(func); }
  inline auto BoolAnd(const smt::Term& a, const smt::Term& b) {
    return solver_->make_term(smt::PrimOp::And, a, b);
  }
  inline auto Equal(const smt::Term& a, const smt::Term& b) {
    return solver_->make_term(smt::PrimOp::Equal, a, b);
  }

private:
  typedef std::unordered_map<const ExprPtr, smt::Term, ExprHash> ExprTermMap;
  typedef std::unordered_map<const FuncPtr, smt::Term, FuncHash> FuncTermMap;

  // ------------------------- MEMBERS -------------------------------------- //
  smt::SmtSolver& solver_;
  ExprTermMap expr_map_;
  FuncTermMap func_map_;
  std::string suffix_ = "";

  // ------------------------- HELPERS -------------------------------------- //
  void PopulateExprMap(const ExprPtr& expr);
  smt::Term ExprVar2Term(const ExprPtr& expr);
  smt::Term ExprConst2Term(const ExprPtr& expr);
  smt::Term ExprOp2Term(const ExprPtr& expr, const smt::TermVec& arg_terms);
  smt::Term Func2Term(const FuncPtr& func);
  smt::Sort IlaSort2SmtSort(const SortPtr& s);

}; // class SmtSwitchItf

} // namespace ilang

#endif // SMTSWITCH_INTERFACE

#endif // ILANG_ILA_MNGR_U_SMT_SWITCH_H__