Merge 65bab36 into 71fbdab

include/ilang/ila-mngr/u_unroller.h

@@ -4,26 +4,28 @@
 #ifndef ILANG_ILA_MNGR_U_UNROLLER_H__
 #define ILANG_ILA_MNGR_U_UNROLLER_H__
 
-#include <set>
+#include <map>
 #include <vector>
 
-#include "z3++.h"
+#include <z3++.h>
+
 #include <ilang/ila/instr_lvl_abs.h>
-#include <ilang/ila/z3_expr_adapter.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 
 /// \namespace ilang
 namespace ilang {
 
 /// \brief Base class for unrolling ILA execution in different settings.
 class Unroller {
-public:
+protected:
   /// Type alias for z3::expr.
   typedef z3::expr ZExpr;
   /// Type for containing a set of z3::expr.
   typedef z3::expr_vector ZExprVec;
   /// Type alias for a set of ExprPtr.
   typedef ExprPtrVec IExprVec;
 
+public:
   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
   /// Default constructor
   Unroller(z3::context& ctx, const std::string& suffix);
@@ -144,7 +146,7 @@ class Unroller {
                    const std::string& suffix);
 
   /// Clear the z3::epxr container.
-  inline void Clear(ZExprVec& z3_vec);
+  void Clear(ZExprVec& z3_vec);
 
   /// Generate and append the z3::expr for the set of Expr w.r.t. the suffix.
   void IExprToZExpr(const IExprVec& i_expr_src, const std::string& suffix,

include/ilang/ila-mngr/v_eq_check_legacy_bmc.h

@@ -6,9 +6,10 @@
 
 #include <map>
 
-#include "z3++.h"
+#include <z3++.h>
+
 #include <ilang/ila/instr_lvl_abs.h>
-#include <ilang/ila/z3_expr_adapter.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 #include <ilang/util/container.h>
 
 /// \namespace ilang

include/ilang/ila/transition.h

@@ -6,7 +6,6 @@
 
 #include <ilang/ila/expr_fuse.h>
 #include <ilang/ila/instr.h>
-#include <ilang/ila/z3_expr_adapter.h>
 #include <ilang/util/container.h>
 
 /// \namespace ilang

include/ilang/mcm/inter_ila_unroller.h

@@ -10,10 +10,10 @@
 #include <stack>
 #include <vector>
 
-#include "ilang/ila/instr_lvl_abs.h"
-#include "ilang/ila/z3_expr_adapter.h"
-#include "ilang/mcm/memory_model.h"
-#include "z3++.h"
+#include <z3++.h>
+
+#include <ilang/ila/instr_lvl_abs.h>
+#include <ilang/mcm/memory_model.h>
 
 /// \namespace ilang
 namespace ilang {

include/ilang/mcm/memory_model.h

@@ -4,8 +4,9 @@
 #ifndef ILANG_MCM_MEMORY_MODEL_H__
 #define ILANG_MCM_MEMORY_MODEL_H__
 
-#include "ilang/mcm/ast_helper.h"
-#include "ilang/mcm/axiom_helper.h"
+#include <ilang/mcm/ast_helper.h>
+#include <ilang/mcm/axiom_helper.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 
 /// \namespace ilang
 namespace ilang {

include/ilang/target-smt/smt_shim.h

@@ -0,0 +1,37 @@
+/// \file
+/// Header for the class SmtShim.
+
+#ifndef ILANG_TARGET_SMT_SMT_SHIM_H__
+#define ILANG_TARGET_SMT_SMT_SHIM_H__
+
+#include <ilang/ila/expr_fuse.h>
+
+/// \namespace ilang
+namespace ilang {
+
+/// \brief A templated class for wrapping z3 and smt-switch to provide a unified
+/// interface for different application, e.g., unroller.
+template <class Generator> class SmtShim {
+public:
+  /// Constructor.
+  SmtShim(Generator& gen) : gen_(gen) {}
+
+private:
+  /// Reference to the underlying SMT formula generator.
+  Generator& gen_;
+
+public:
+  /// Unified interface to get expression.
+  inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix = "") {
+    return gen_.GetShimExpr(expr, suffix);
+  }
+  /// Unified interface to get function declaration.
+  inline auto GetShimFunc(const FuncPtr& func) {
+    return gen_.GetShimFunc(func);
+  }
+
+}; // class SmtShim
+
+} // namespace ilang
+
+#endif // ILANG_TARGET_SMT_SMT_SHIM_H__

include/ilang/ila-mngr/u_smt_switch.h → include/ilang/target-smt/smt_switch_itf.h

@@ -4,8 +4,6 @@
 #ifndef ILANG_ILA_MNGR_U_SMT_SWITCH_H__
 #define ILANG_ILA_MNGR_U_SMT_SWITCH_H__
 
-#include <ilang/config.h>
-
 #ifdef SMTSWITCH_INTERFACE
 
 #include <string>
@@ -27,21 +25,31 @@ class SmtSwitchItf {
   /// Default destructor.
   ~SmtSwitchItf();
 
-  /// Type for cacheing the generated expressions.
-  typedef std::unordered_map<const ExprPtr, smt::Term, ExprHash> ExprTermMap;
-  /// Type for cacheing the generated functions.
-  typedef std::unordered_map<const FuncPtr, smt::Term, FuncHash> FuncTermMap;
-
   // ------------------------- METHODS -------------------------------------- //
   /// Get the SMT Term of the AST node.
-  smt::Term GetSmtTerm(const ExprPtr expr, const std::string& suffix = "");
+  smt::Term GetSmtTerm(const ExprPtr& expr, const std::string& suffix = "");
   /// Reset the solver and the interface.
   void Reset();
 
-  /// Function object for getting SMT Term.
-  void operator()(const ExprPtr expr);
+  /// Check if Term is generated.
+  bool pre(const ExprPtr& expr);
+  /// Generate Term if not already.
+  void post(const ExprPtr& expr);
+
+  // ------------------------- SHIM INTERFACE ------------------------------- //
+  /// Unified SmtShim interface to get smt::Term.
+  inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix) {
+    return GetSmtTerm(expr, suffix);
+  }
+  /// Unified SmtShim interface to get smt::Func.
+  inline auto GetShimFunc(const FuncPtr& func) { return Func2Term(func); }
 
 private:
+  /// Type for cacheing the generated expressions.
+  typedef std::unordered_map<const ExprPtr, smt::Term, ExprHash> ExprTermMap;
+  /// Type for cacheing the generated functions.
+  typedef std::unordered_map<const FuncPtr, smt::Term, FuncHash> FuncTermMap;
+
   // ------------------------- MEMBERS -------------------------------------- //
   /// The underlying SMT solver.
   smt::SmtSolver& solver_;
@@ -54,15 +62,17 @@ class SmtSwitchItf {
 
   // ------------------------- HELPERS -------------------------------------- //
   /// Insert the SMT Term of the given node into the map.
-  void PopulateExprMap(const ExprPtr expr);
+  void PopulateExprMap(const ExprPtr& expr);
   /// Make Term of expr variable.
-  smt::Term ExprVar2Term(const ExprPtr expr);
+  smt::Term ExprVar2Term(const ExprPtr& expr);
   /// Make Term of expr constant.
-  smt::Term ExprConst2Term(const ExprPtr expr);
+  smt::Term ExprConst2Term(const ExprPtr& expr);
   /// Make Term of expr operator.
-  smt::Term ExprOp2Term(const ExprPtr expr, const smt::TermVec& arg_terms);
+  smt::Term ExprOp2Term(const ExprPtr& expr, const smt::TermVec& arg_terms);
+  /// Make Term of func.
+  smt::Term Func2Term(const FuncPtr& func);
   /// Make smt::Sort of ilang::SortPtr.
-  smt::Sort IlaSort2SmtSort(const SortPtr s);
+  smt::Sort IlaSort2SmtSort(const SortPtr& s);
 
 }; // class SmtSwitchItf
 

include/ilang/ila/z3_expr_adapter.h → include/ilang/target-smt/z3_expr_adapter.h

@@ -1,12 +1,13 @@
 /// \file
 /// Header for the class Z3ExprAdapter
 
-#ifndef ILANG_ILA_Z3_EXPR_ADAPTER_H__
-#define ILANG_ILA_Z3_EXPR_ADAPTER_H__
+#ifndef ILANG_TARGET_SMT_Z3_EXPR_ADAPTER_H__
+#define ILANG_TARGET_SMT_Z3_EXPR_ADAPTER_H__
 
 #include <unordered_map>
 
-#include "z3++.h"
+#include <z3++.h>
+
 #include <ilang/ila/expr_fuse.h>
 
 /// \namespace ilang
@@ -24,17 +25,27 @@ class Z3ExprAdapter {
   /// ~Default destructor.
   ~Z3ExprAdapter();
 
-  /// Type for caching the generated expressions.
-  typedef std::unordered_map<const ExprPtr, z3::expr, Z3AdapterHash> ExprMap;
-
   // ------------------------- METHODS -------------------------------------- //
   /// Get the z3 expression of the AST node.
-  z3::expr GetExpr(const ExprPtr expr, const std::string& suffix = "");
+  z3::expr GetExpr(const ExprPtr& expr, const std::string& suffix = "");
 
   /// Function object for getting z3 expression.
-  void operator()(const ExprPtr expr);
+  void operator()(const ExprPtr& expr);
+
+  // ------------------------- SHIM INTERFACE ------------------------------- //
+  /// Unified SmtShim interface to get z3::expr.
+  inline auto GetShimExpr(const ExprPtr& expr, const std::string& suffix) {
+    return GetExpr(expr, suffix);
+  }
+  /// Unified SmtShim interface to get z3::func_decl.
+  inline auto GetShimFunc(const FuncPtr& func) {
+    return func->GetZ3FuncDecl(ctx_);
+  }
 
 private:
+  /// Type for caching the generated expressions.
+  typedef std::unordered_map<const ExprPtr, z3::expr, Z3AdapterHash> ExprMap;
+
   // ------------------------- MEMBERS -------------------------------------- //
   /// The underlying z3 context.
   z3::context& ctx_;
@@ -45,10 +56,10 @@ class Z3ExprAdapter {
 
   // ------------------------- HELPERS -------------------------------------- //
   /// Insert the z3 expression of the given node into the map.
-  void PopulateExprMap(const ExprPtr expr);
+  void PopulateExprMap(const ExprPtr& expr);
 
 }; // class Z3ExprAdapter
 
 } // namespace ilang
 
-#endif // ILANG_ILA_Z3_EXPR_ADAPTER_H__
+#endif // ILANG_TARGET_SMT_Z3_EXPR_ADAPTER_H__

src/CMakeLists.txt

@@ -13,6 +13,7 @@ add_subdirectory(ila-mngr)
 add_subdirectory(mcm)
 add_subdirectory(target-json)
 add_subdirectory(target-sc)
+add_subdirectory(target-smt)
 add_subdirectory(util)
 add_subdirectory(verilog-in)
 add_subdirectory(verilog-out)
@@ -59,6 +60,9 @@ target_include_directories(${ILANG_LIB_NAME}
 
 # check if c++17 filesystem is available
 CHECK_INCLUDE_FILE_CXX(filesystem FS_INCLUDE)
+if(${FS_INCLUDE})
+  target_compile_definitions(${ILANG_LIB_NAME} PRIVATE FS_INCLUDE)
+endif()
 
 # ---------------------------------------------------------------------------- #
 # LINK LIBRARIES
@@ -200,7 +204,7 @@ if(${ILANG_BUILD_SWITCH})
 
   find_package(smtswitch REQUIRED)
   target_link_libraries(${ILANG_LIB_NAME} PUBLIC smt-switch::smt-switch)
-  set(SMTSWITCH_INTERFACE TRUE)
+  target_compile_definitions(${ILANG_LIB_NAME} PUBLIC SMTSWITCH_INTERFACE)
 
   if(${SMTSWITCH_BTOR_FOUND})
     target_link_libraries(${ILANG_LIB_NAME} PUBLIC smt-switch::smt-switch-btor)
@@ -218,8 +222,6 @@ if(${ILANG_BUILD_SWITCH})
     target_link_libraries(${ILANG_LIB_NAME} PUBLIC smt-switch::smt-switch-yices2)
   endif()
 
-else()
-  set(SMTSWITCH_INTERFACE FALSE)
 endif()
 
 ##

src/config.h.in

@@ -24,7 +24,7 @@
 
 #cmakedefine SMTSWITCH_YICES2_FOUND
 
-#cmakedefine FS_INCLUDE
+// #cmakedefine FS_INCLUDE
 
 #endif // CONFIG_CMAKE_DEFINE_H__
 

src/ila-mngr/CMakeLists.txt

@@ -12,7 +12,6 @@ target_sources(${ILANG_LIB_NAME} PRIVATE
   ${CMAKE_CURRENT_SOURCE_DIR}/u_abs_knob.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_expr.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/u_rewrite_ila.cc
-  ${CMAKE_CURRENT_SOURCE_DIR}/u_smt_switch.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/u_unroller.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/v_eq_check_crr.cc

src/ila-mngr/p_simplify_semantic.cc

@@ -3,7 +3,7 @@
 
 #include <ilang/ila-mngr/pass.h>
 
-#include <ilang/ila/z3_expr_adapter.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 #include <ilang/util/log.h>
 
 namespace ilang {

src/ila-mngr/u_unroller.cc

@@ -13,7 +13,7 @@ namespace ilang {
 
 using namespace ExprFuse;
 
-typedef Unroller::ZExpr ZExpr;
+typedef z3::expr ZExpr;
 
 /******************************************************************************/
 // Unroller

src/ila/CMakeLists.txt

@@ -19,6 +19,4 @@ target_sources(${ILANG_LIB_NAME} PRIVATE
   ${CMAKE_CURRENT_SOURCE_DIR}/symbol.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/transition.cc
   ${CMAKE_CURRENT_SOURCE_DIR}/validate_model.cc
-  ${CMAKE_CURRENT_SOURCE_DIR}/z3_expr_adapter.cc
 )
-

src/ila/validate_model.cc

@@ -3,9 +3,10 @@
 
 #include <ilang/ila/validate_model.h>
 
-#include "z3++.h"
+#include <z3++.h>
+
 #include <ilang/ila/ast_fuse.h>
-#include <ilang/ila/z3_expr_adapter.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 #include <ilang/util/log.h>
 
 namespace ilang {

src/ilang++.cc

@@ -6,12 +6,12 @@
 #include <ilang/config.h>
 #include <ilang/ila-mngr/pass.h>
 #include <ilang/ila-mngr/u_abs_knob.h>
-#include <ilang/ila-mngr/u_smt_switch.h>
 #include <ilang/ila-mngr/u_unroller.h>
 #include <ilang/ila/instr_lvl_abs.h>
 #include <ilang/target-itsy/interface.h>
 #include <ilang/target-json/interface.h>
 #include <ilang/target-sc/ilator.h>
+#include <ilang/target-smt/smt_switch_itf.h>
 #include <ilang/util/log.h>
 #include <ilang/verilog-out/verilog_gen.h>
 

src/target-sc/ilator.cc

@@ -1,6 +1,8 @@
 /// \file
 /// Implementation of the class Ilator.
 
+#include <ilang/target-sc/ilator.h>
+
 #include <fstream>
 
 #include <fmt/format.h>
@@ -11,12 +13,10 @@
 #include <ilang/ila-mngr/u_abs_knob.h>
 #include <ilang/ila/ast_fuse.h>
 #include <ilang/ila/expr_fuse.h>
-#include <ilang/ila/z3_expr_adapter.h>
+#include <ilang/target-smt/z3_expr_adapter.h>
 #include <ilang/util/fs.h>
 #include <ilang/util/log.h>
 
-#include <ilang/target-sc/ilator.h>
-
 /// \namespace ilang
 namespace ilang {