From ed5dd26bb7f08ea95a5e3dc9ecae6574db4b7b90 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 Apr 2025 10:10:12 -0700
Subject: [PATCH] remove non-working ts mcp server, settle with python variant

---
 src/api/mcp/z3mcp.py |  5 +++-
 src/api/mcp/z3mcp.ts | 62 --------------------------------------------
 2 files changed, 4 insertions(+), 63 deletions(-)
 delete mode 100644 src/api/mcp/z3mcp.ts

diff --git a/src/api/mcp/z3mcp.py b/src/api/mcp/z3mcp.py
index 107b297ea..b292ce1e9 100644
--- a/src/api/mcp/z3mcp.py
+++ b/src/api/mcp/z3mcp.py
@@ -9,7 +9,10 @@ mcp = FastMCP("Z3 Solver")
 # Evaluate SMT commands
 @mcp.tool()
 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)
 
 if __name__ == "__main__":
diff --git a/src/api/mcp/z3mcp.ts b/src/api/mcp/z3mcp.ts
deleted file mode 100644
index 1a063cf8c..000000000
--- a/src/api/mcp/z3mcp.ts
+++ /dev/null
@@ -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);