From 8b04896b2ba4b61c8076f0712567d423b9695864 Mon Sep 17 00:00:00 2001 From: Amily Wu Date: Wed, 18 Mar 2026 19:27:41 +0000 Subject: [PATCH] Add optional emit reset to exportSMT --- mlir/include/mlir-c/Target/ExportSMTLIB.h | 8 +++--- .../include/mlir/Target/SMTLIB/ExportSMTLIB.h | 2 ++ mlir/lib/Bindings/Python/DialectSMT.cpp | 17 ++++++------ mlir/lib/CAPI/Target/ExportSMTLIB.cpp | 26 +++++++++---------- mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp | 3 ++- mlir/test/CAPI/smt.c | 11 +++++--- 6 files changed, 37 insertions(+), 30 deletions(-) diff --git a/mlir/include/mlir-c/Target/ExportSMTLIB.h b/mlir/include/mlir-c/Target/ExportSMTLIB.h index 59beda54d289b..f6a52940e0ab6 100644 --- a/mlir/include/mlir-c/Target/ExportSMTLIB.h +++ b/mlir/include/mlir-c/Target/ExportSMTLIB.h @@ -21,13 +21,13 @@ extern "C" { /// Emits SMTLIB for the specified module using the provided callback and user /// data -MLIR_CAPI_EXPORTED MlirLogicalResult -mlirTranslateModuleToSMTLIB(MlirModule, MlirStringCallback, void *userData, - bool inlineSingleUseValues, bool indentLetBody); +MLIR_CAPI_EXPORTED MlirLogicalResult mlirTranslateModuleToSMTLIB( + MlirModule, MlirStringCallback, void *userData, bool inlineSingleUseValues, + bool indentLetBody, bool emitReset); MLIR_CAPI_EXPORTED MlirLogicalResult mlirTranslateOperationToSMTLIB( MlirOperation, MlirStringCallback, void *userData, - bool inlineSingleUseValues, bool indentLetBody); + bool inlineSingleUseValues, bool indentLetBody, bool emitReset); #ifdef __cplusplus } diff --git a/mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h b/mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h index 6415b97167cf7..f612252fcf8fd 100644 --- a/mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h +++ b/mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h @@ -27,6 +27,8 @@ struct SMTEmissionOptions { bool inlineSingleUseValues = false; // Increase indentation for each 'let' expression body. bool indentLetBody = false; + // Emit a '(reset)' command at the end of each solver scope. + bool emitReset = true; }; /// Run the ExportSMTLIB pass. diff --git a/mlir/lib/Bindings/Python/DialectSMT.cpp b/mlir/lib/Bindings/Python/DialectSMT.cpp index 963076a6c672e..3e7fc4fbffe44 100644 --- a/mlir/lib/Bindings/Python/DialectSMT.cpp +++ b/mlir/lib/Bindings/Python/DialectSMT.cpp @@ -91,12 +91,12 @@ static void populateDialectSMTSubmodule(nanobind::module_ &m) { IntType::bind(m); auto exportSMTLIB = [](MlirOperation module, bool inlineSingleUseValues, - bool indentLetBody) { + bool indentLetBody, bool emitReset) { CollectDiagnosticsToStringScope scope(mlirOperationGetContext(module)); PyPrintAccumulator printAccum; MlirLogicalResult result = mlirTranslateOperationToSMTLIB( module, printAccum.getCallback(), printAccum.getUserData(), - inlineSingleUseValues, indentLetBody); + inlineSingleUseValues, indentLetBody, emitReset); if (mlirLogicalResultIsSuccess(result)) return printAccum.join(); throw nb::value_error( @@ -107,20 +107,21 @@ static void populateDialectSMTSubmodule(nanobind::module_ &m) { m.def( "export_smtlib", [&exportSMTLIB](const PyOperation &module, bool inlineSingleUseValues, - bool indentLetBody) { - return exportSMTLIB(module, inlineSingleUseValues, indentLetBody); + bool indentLetBody, bool emitReset) { + return exportSMTLIB(module, inlineSingleUseValues, indentLetBody, + emitReset); }, "module"_a, "inline_single_use_values"_a = false, - "indent_let_body"_a = false); + "indent_let_body"_a = false, "emit_reset"_a = true); m.def( "export_smtlib", [&exportSMTLIB](PyModule &module, bool inlineSingleUseValues, - bool indentLetBody) { + bool indentLetBody, bool emitReset) { return exportSMTLIB(mlirModuleGetOperation(module.get()), - inlineSingleUseValues, indentLetBody); + inlineSingleUseValues, indentLetBody, emitReset); }, "module"_a, "inline_single_use_values"_a = false, - "indent_let_body"_a = false); + "indent_let_body"_a = false, "emit_reset"_a = true); } } // namespace smt } // namespace MLIR_BINDINGS_PYTHON_DOMAIN diff --git a/mlir/lib/CAPI/Target/ExportSMTLIB.cpp b/mlir/lib/CAPI/Target/ExportSMTLIB.cpp index 4326f967281e1..be17143ec9c4a 100644 --- a/mlir/lib/CAPI/Target/ExportSMTLIB.cpp +++ b/mlir/lib/CAPI/Target/ExportSMTLIB.cpp @@ -19,24 +19,22 @@ using namespace mlir; -MlirLogicalResult mlirTranslateOperationToSMTLIB(MlirOperation module, - MlirStringCallback callback, - void *userData, - bool inlineSingleUseValues, - bool indentLetBody) { +MlirLogicalResult mlirTranslateOperationToSMTLIB( + MlirOperation module, MlirStringCallback callback, void *userData, + bool inlineSingleUseValues, bool indentLetBody, bool emitReset) { mlir::detail::CallbackOstream stream(callback, userData); smt::SMTEmissionOptions options; options.inlineSingleUseValues = inlineSingleUseValues; options.indentLetBody = indentLetBody; - return wrap(smt::exportSMTLIB(unwrap(module), stream)); + options.emitReset = emitReset; + return wrap(smt::exportSMTLIB(unwrap(module), stream, options)); } -MlirLogicalResult mlirTranslateModuleToSMTLIB(MlirModule module, - MlirStringCallback callback, - void *userData, - bool inlineSingleUseValues, - bool indentLetBody) { - return mlirTranslateOperationToSMTLIB(mlirModuleGetOperation(module), - callback, userData, - inlineSingleUseValues, indentLetBody); +MlirLogicalResult +mlirTranslateModuleToSMTLIB(MlirModule module, MlirStringCallback callback, + void *userData, bool inlineSingleUseValues, + bool indentLetBody, bool emitReset) { + return mlirTranslateOperationToSMTLIB( + mlirModuleGetOperation(module), callback, userData, inlineSingleUseValues, + indentLetBody, emitReset); } diff --git a/mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp b/mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp index e6d8e34ea7372..189f766c444b0 100644 --- a/mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp +++ b/mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp @@ -674,7 +674,8 @@ static LogicalResult emit(SolverOp solver, const SMTEmissionOptions &options, if (result.wasInterrupted()) return failure(); - stream << "(reset)\n"; + if (options.emitReset) + stream << "(reset)\n"; return success(); } diff --git a/mlir/test/CAPI/smt.c b/mlir/test/CAPI/smt.c index 95a9b55e3209b..a621147c91b61 100644 --- a/mlir/test/CAPI/smt.c +++ b/mlir/test/CAPI/smt.c @@ -34,13 +34,18 @@ void testExportSMTLIB(MlirContext ctx) { MlirModule module = mlirModuleCreateParse(ctx, mlirStringRefCreateFromCString(testSMT)); - MlirLogicalResult result = - mlirTranslateModuleToSMTLIB(module, dumpCallback, NULL, false, false); - (void)result; + MlirLogicalResult result = mlirTranslateModuleToSMTLIB( + module, dumpCallback, NULL, false, false, true); assert(mlirLogicalResultIsSuccess(result)); // CHECK: ; solver scope 0 // CHECK-NEXT: (reset) + + result = mlirTranslateModuleToSMTLIB(module, dumpCallback, NULL, false, false, + false); + assert(mlirLogicalResultIsSuccess(result)); + + // CHECK-NOT: (reset) mlirModuleDestroy(module); }