From f21bde0e08d8576aff2881653abeb690524a9741 Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Thu, 27 Jun 2024 04:42:59 +0200 Subject: [PATCH] Use FunctionalTools::Scope instead of replaceCharacters --- backends/functional/smtlib.cc | 26 +++++++------------------- 1 file changed, 7 insertions(+), 19 deletions(-) diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib.cc index 7f1ca0a61b6..afddbd83440 100644 --- a/backends/functional/smtlib.cc +++ b/backends/functional/smtlib.cc @@ -23,11 +23,14 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +const char illegal_characters[] = "$\\"; +const char *reserved_keywords[] = {}; + struct SmtScope { pool used_names; dict name_map; - - SmtScope() {} + FunctionalTools::Scope scope; + SmtScope() : scope(illegal_characters, reserved_keywords) {} void reserve(const std::string &name) { used_names.insert(name); } @@ -184,21 +187,6 @@ struct SmtModule { SmtModule(const std::string &module_name, FunctionalIR ir) : name(module_name), ir(std::move(ir)) {} - std::string replaceCharacters(const std::string &input) - { - std::string result = input; - std::replace(result.begin(), result.end(), '$', '_'); // Replace $ with _ - - // Since \ is an escape character, we use a loop to replace it - size_t pos = 0; - while ((pos = result.find('\\', pos)) != std::string::npos) { - result.replace(pos, 1, "_"); - pos += 1; // Move past the replaced character - } - - return result; - } - void write(std::ostream &out) { SmtWriter writer(out); @@ -237,7 +225,7 @@ struct SmtModule { if (ir.inputs().count(node.name()) > 0) continue; - std::string node_name = replaceCharacters(scope[node.name()]); + std::string node_name = scope[node.name()]; std::string node_expr = node.visit(visitor); writer.print(" (let ( (%s %s))", node_name.c_str(), node_expr.c_str()); @@ -247,7 +235,7 @@ struct SmtModule { for (const auto &output : ir.outputs()) { std::string output_name = scope[output.first]; const std::string output_assignment = ir.get_output_node(output.first).name().c_str(); - writer.print(" (%s %s)", output_name.c_str(), replaceCharacters(output_assignment).substr(1).c_str()); + writer.print(" (%s %s)", output_name.c_str(), output_assignment.substr(1).c_str()); } writer.print(" )"); writer.print(" (mk_outputs");