[MLIR][Python] Add optional emit reset to exportSMTLIB - #187366
Merged
Conversation
Member
|
@llvm/pr-subscribers-mlir Author: RattataKing (RattataKing) ChangesPreviously, the MLIR's python binding Full diff: https://github.com/llvm/llvm-project/pull/187366.diff 6 Files Affected:
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);
}
|
makslevental
approved these changes
Mar 18, 2026
makslevental
left a comment
makslevental
left a comment
Contributor
There was a problem hiding this comment.
LGTM - just curious in what case wouldn't you want this (reset) at the end?
11 tasks
kuhar
approved these changes
Mar 18, 2026
kuhar
left a comment
kuhar
left a comment
Member
There was a problem hiding this comment.
Makes sense, our use case in IREE doesn’t need these resets
Contributor
Author
We want to enable something like: smt_module = iree_codegen.convert_constraints_op_to_smt_op(constraints_op)
smtlib = smt.export_smtlib(smt_module, emit_reset=False)
solver = z3.Solver()
solver.from_string(smtlib) # Construct the solver without needing to strip `(reset)` |
RattataKing
added a commit
to iree-org/iree
that referenced
this pull request
Mar 30, 2026
Pass `emitReset` parameter to mlir smtlib export api, see upstream PR: llvm/llvm-project#187366
kimm240
pushed a commit
to kimm240/iree
that referenced
this pull request
May 8, 2026
Pass `emitReset` parameter to mlir smtlib export api, see upstream PR: llvm/llvm-project#187366
RattataKing
added a commit
to RattataKing/iree
that referenced
this pull request
May 27, 2026
Pass `emitReset` parameter to mlir smtlib export api, see upstream PR: llvm/llvm-project#187366
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Previously, the MLIR's python binding
smt.export_smtlib(...)always emit(reset)to the end of smtlib string as a solver terminator.This PR added an option to suppress this trailing, as downstream users like python z3 module don't need it.