z3smt-mcp

# Z3/SMT MCP Server An MCP (Model Context Protocol) server that exposes Z3/SMT solver capabilities for constraint solving, logical reasoning, and satisfiability checking. ## Features - **Direct Z3 Python code execution** - Run arbitrary Z3 Python code - **SMT-LIB 2.0 support** - Parse and solve SMT-LIB format problems - **Constraint checking** - Check satisfiability of constraint lists - **Theorem proving** - Prove theorems by showing unsatisfiability of negation - **Expression simplification** - Simplify Z3 expressions - **Logic program solving** - Parse and solve structured logic programs (Logic-LLM format) - **Session management** - Incremental solving with push/pop support ## Installation ```bash # Using pip pip install z3smt-mcp # Or install from source git clone https://github.com/z3smt-mcp/z3smt-mcp cd z3smt-mcp pip install -e . ``` ### Requirements - Python >= 3.10 - z3-solver >= 4.12.0 - mcp >= 1.0.0 ## Usage ### Running the Server ```bash # Run directly z3smt-mcp # Or via Python python -m z3smt_mcp.server ``` ### Claude Desktop Configuration Add to your Claude Desktop config (`claude_desktop_config.json`): ```json { "mcpServers": { "z3smt": { "command": "z3smt-mcp" } } } ``` Or if installed from source: ```json { "mcpServers": { "z3smt": { "command": "python", "args": ["-m", "z3smt_mcp.server"] } } } ``` ## Available Tools ### `solve` Execute Z3 Python code directly. All Z3 imports are pre-loaded. ```python # Example: Solve a system of linear equations x = Int('x') y = Int('y') solver = Solver() solver.add(x + y == 10) solver.add(x - y == 4) if solver.check() == sat: print(solver.model()) # Output: [y = 3, x = 7] ``` ### `solve_smtlib` Solve problems in SMT-LIB 2.0 format. ```smt2 (declare-const x Int) (declare-const y Int) (assert (= (+ x y) 10)) (assert (= (- x y) 4)) (check-sat) (get-model) ``` ### `check_sat` Check satisfiability of a list of constraints with automatic variable de…