[xlscc] Reuse z3 IR translators.

Reusing z3 IR translators allows previous conversions to be reused, which provides significant savings as this translation is expensive.

PiperOrigin-RevId: 678390950

Author: grebe

xls/contrib/xlscc/BUILD

@@ -120,6 +120,7 @@ cc_library(
         ":xlscc_logging",
         "//xls/common:math_util",
         "//xls/common:stopwatch",
+        "//xls/common/status:ret_check",
         "//xls/common/status:status_macros",
         "//xls/interpreter:ir_interpreter",
         "//xls/ir",
@@ -137,6 +138,7 @@ cc_library(
         "//xls/solvers:z3_ir_translator",
         "//xls/solvers:z3_utils",
         "@com_google_absl//absl/base",
+        "@com_google_absl//absl/base:core_headers",
         "@com_google_absl//absl/container:btree",
         "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/container:flat_hash_set",

xls/contrib/xlscc/translate_loops.cc

@@ -163,12 +163,8 @@ absl::Status Translator::GenerateIR_UnrolledLoop(bool always_first_iter,
                                                  const clang::Stmt* body,
                                                  clang::ASTContext& ctx,
                                                  const xls::SourceInfo& loc) {
-  XLS_ASSIGN_OR_RETURN(
-      std::unique_ptr<xls::solvers::z3::IrTranslator> z3_translator_parent,
-      xls::solvers::z3::IrTranslator::CreateAndTranslate(
-          /*source=*/nullptr,
-          /*allow_unsupported=*/false));
-
+  XLS_ASSIGN_OR_RETURN(xls::solvers::z3::IrTranslator * z3_translator_parent,
+                       GetZ3Translator(context().fb->function()));
   Z3_solver solver =
       xls::solvers::z3::CreateSolver(z3_translator_parent->ctx(), 1);
 

xls/contrib/xlscc/translator.cc

@@ -68,6 +68,7 @@
 #include "llvm/include/llvm/ADT/FloatingPointMode.h"
 #include "llvm/include/llvm/ADT/StringRef.h"
 #include "llvm/include/llvm/Support/raw_ostream.h"
+#include "xls/common/status/ret_check.h"
 #include "xls/common/status/status_macros.h"
 #include "xls/contrib/xlscc/cc_parser.h"
 #include "xls/contrib/xlscc/xlscc_logging.h"
@@ -5395,12 +5396,9 @@ absl::StatusOr<bool> Translator::BitMustBe(bool assert_value, xls::BValue& bval,
 
   XLS_RETURN_IF_ERROR(ShortCircuitBVal(bval, loc));
 
-  XLS_ASSIGN_OR_RETURN(
-      std::unique_ptr<xls::solvers::z3::IrTranslator> z3_translator,
-      xls::solvers::z3::IrTranslator::CreateAndTranslate(
-          /*ctx=*/ctx,
-          /*source=*/bval.node(),
-          /*allow_unsupported=*/false));
+  XLS_ASSIGN_OR_RETURN(xls::solvers::z3::IrTranslator * z3_translator,
+                       GetZ3Translator(bval.builder()->function()));
+  XLS_RETURN_IF_ERROR(bval.node()->Accept(z3_translator));
 
   absl::Span<xls::Node*> positive_assumptions, negative_assumptions;
   xls::Node* assumptions[] = {bval.node()};
@@ -6116,4 +6114,19 @@ absl::StatusOr<Pragma> Translator::FindPragmaForLoc(
   return parser_->FindPragmaForLoc(ploc, ignore_label);
 }
 
+absl::StatusOr<xls::solvers::z3::IrTranslator*> Translator::GetZ3Translator(
+    xls::FunctionBase* func) {
+  XLS_RET_CHECK(!func->IsBlock());
+  auto [iter, inserted] = z3_translators_.insert({func, nullptr});
+  if (inserted) {
+    XLS_ASSIGN_OR_RETURN(
+        iter->second,
+        xls::solvers::z3::IrTranslator::CreateAndTranslate(
+            // Don't preemptively convert everything as this is expensive and we
+            // might get away with converting less.
+            /*function_base=*/nullptr, /*allow_unsupported=*/false));
+  }
+  return iter->second.get();
+}
+
 }  // namespace xlscc

xls/contrib/xlscc/translator.h

@@ -29,6 +29,7 @@
 #include <utility>
 #include <vector>
 
+#include "absl/base/attributes.h"
 #include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
@@ -2249,6 +2250,13 @@ class Translator {
   }
   clang::PresumedLoc GetPresumedLoc(const clang::Stmt& stmt);
   clang::PresumedLoc GetPresumedLoc(const clang::Decl& decl);
+
+  absl::StatusOr<xls::solvers::z3::IrTranslator*> GetZ3Translator(
+      xls::FunctionBase* func) ABSL_ATTRIBUTE_LIFETIME_BOUND;
+
+  absl::flat_hash_map<xls::FunctionBase*,
+                      std::unique_ptr<xls::solvers::z3::IrTranslator>>
+      z3_translators_;
 };
 
 }  // namespace xlscc