mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity

remove non-working ts mcp server, settle with python variant

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-18 10:10:12 -07:00
parent 741cb5c3b5
commit ed5dd26bb7
2 changed files with 4 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/mcp/z3mcp.py
View file

@ -9,7 +9,10 @@ mcp = FastMCP("Z3 Solver")
# Evaluate SMT commands # Evaluate SMT commands
@mcp.tool() @mcp.tool()
def eval(command : str) -> str: def eval(command : str) -> str:
"""Evaluate an SMTLIB2 Command using Z3""" """Evaluate an SMTLIB2 Command using Z3
Whenever you are faced with a problem that can be formulated as SMTLIB2 constraints
always use this function to solve the problem.
"""
return Z3_eval_smtlib2_string(main_ctx().ctx, command) return Z3_eval_smtlib2_string(main_ctx().ctx, command)
if __name__ == "__main__": if __name__ == "__main__":

62
src/api/mcp/z3mcp.ts
View file

@ -1,62 +0,0 @@
import { McpServer } from "@modelcontextprotocol/sdk/server/mcp.js";
import { StdioServerTransport } from "@modelcontextprotocol/sdk/server/stdio.js";
async function importZ3() {
try {
const z3 = await import("z3-solver");
return await z3.init();
} catch (e) {
console.error("Failed to import z3-solver:", e?.message);
return undefined;
}
}
async function Z3Run(input) {
const z3p = await importZ3();
if (!z3p) {
return "Z3 not available. Make sure to install the https://www.npmjs.com/package/z3-solver package.";
}
const { Z3 } = z3p;
const cfg = Z3.mk_config();
const ctx = Z3.mk_context(cfg);
Z3.del_config(cfg);
const timeout = 10000;
Z3.global_param_set("timeout", String(timeout));
let output = "";
let error = "";
const timeStart = Date.now();
try {
output = (await Z3.eval_smtlib2_string(ctx, input)) ?? "";
} catch (e) {
error = e.message ?? "Error message is empty";
} finally {
Z3.del_context(ctx);
}
if (/unknown/.test(output)) {
const timeEnd = Date.now();
if (timeEnd - timeStart >= timeout) {
output = output + "\nZ3 timeout\n";
}
}
if (!error) return output;
else return `error: ${error}\n\n${output || ""}`;
}
const server = new McpServer({
name: "z3",
version: "1.0.0"
});
server.tool(
"eval",
{ command: { type: "string", description: "smtlib2 command" } },
async ({ command }) => {
const result = await Z3Run(command);
return { content: [{ type: "text", text: result }] };
}
);
const transport = new StdioServerTransport();
await server.connect(transport);