mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

minimal z3 MCP server

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-18 10:00:04 -07:00
parent f63c9e366f
commit 741cb5c3b5
1 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/mcp/z3mcp.py Normal file
View file

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