From 741cb5c3b552a438190b41b9878df194c31b3261 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Apr 2025 10:00:04 -0700 Subject: [PATCH] minimal z3 MCP server --- src/api/mcp/z3mcp.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 src/api/mcp/z3mcp.py diff --git a/src/api/mcp/z3mcp.py b/src/api/mcp/z3mcp.py new file mode 100644 index 000000000..107b297ea --- /dev/null +++ b/src/api/mcp/z3mcp.py @@ -0,0 +1,16 @@ +# z3mcp.py +from mcp.server.fastmcp import FastMCP +from z3 import * + +# Create an MCP server +mcp = FastMCP("Z3 Solver") + + +# Evaluate SMT commands +@mcp.tool() +def eval(command : str) -> str: + """Evaluate an SMTLIB2 Command using Z3""" + return Z3_eval_smtlib2_string(main_ctx().ctx, command) + +if __name__ == "__main__": + mcp.run()