Doomhowl-Interactive/llvm-project
0
0
Fork 0
Code Issues Pull Requests Actions 5 Packages Projects Releases Wiki Activity

[MLIR][Python] Add optional emit reset to exportSMTLIB (#187366)

Browse Source 
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.
This commit is contained in:
RattataKing
2026-03-18 16:10:07 -04:00
committed by GitHub
parent 360fab623d
commit 5a5c3176ef
6 changed files with 37 additions and 30 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
mlir/include/mlir-c/Target/ExportSMTLIB.h
View File

@@ -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
}

2
mlir/include/mlir/Target/SMTLIB/ExportSMTLIB.h
View File

@@ -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.

17
mlir/lib/Bindings/Python/DialectSMT.cpp
View File

@@ -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

26
mlir/lib/CAPI/Target/ExportSMTLIB.cpp
View File

@@ -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);
}

3
mlir/lib/Target/SMTLIB/ExportSMTLIB.cpp
View File

@@ -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();
}

11
mlir/test/CAPI/smt.c
View File

@@ -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);
}