z3smt-mcp 0.1.0

MCP server for Z3/SMT solver - enables constraint solving and logical reasoning

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

# 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

# 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):

{
  "mcpServers": {
    "z3smt": {
      "command": "z3smt-mcp"
    }
  }
}

Or if installed from source:

{
  "mcpServers": {
    "z3smt": {
      "command": "python",
      "args": ["-m", "z3smt_mcp.server"]
    }
  }
}

Available Tools

solve

Execute Z3 Python code directly. All Z3 imports are pre-loaded.

# 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.

(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 detection.

{
  "constraints": ["x + y == 10", "x > 0", "y > 0", "x < y"]
}

prove

Prove a theorem by showing its negation is unsatisfiable.

{
  "theorem": "Implies(And(x > 0, y > 0), x + y > 0)",
  "variables": {"x": "int", "y": "int"}
}

simplify

Simplify a Z3 expression.

{
  "expression": "And(x > 0, Or(x > 0, y > 0))"
}

solve_logic_program

Solve structured logic programs in Logic-LLM format.

# Declarations
Color = EnumSort([red, green, blue])
assign = Function(Object -> Color)

# Constraints
assign(obj1) != assign(obj2)
Distinct([c:Color], assign(c))

Session Management Tools

• session_add_variable - Add a variable to the session
• session_add_constraint - Add a constraint to the session
• session_check - Check satisfiability and get model
• session_push - Push a new context (for backtracking)
• session_pop - Pop context (backtrack)
• session_reset - Clear the session
• list_sessions - List all active sessions

Examples

Solving Sudoku

# Create a 9x9 grid of integer variables
X = [[Int(f"x_{i}_{j}") for j in range(9)] for i in range(9)]

solver = Solver()

# Each cell contains a value in 1-9
for i in range(9):
    for j in range(9):
        solver.add(And(X[i][j] >= 1, X[i][j] <= 9))

# Each row has distinct values
for i in range(9):
    solver.add(Distinct(X[i]))

# Each column has distinct values
for j in range(9):
    solver.add(Distinct([X[i][j] for i in range(9)]))

# Each 3x3 box has distinct values
for box_i in range(3):
    for box_j in range(3):
        box = [X[3*box_i + i][3*box_j + j]
               for i in range(3) for j in range(3)]
        solver.add(Distinct(box))

# Add known values (example)
solver.add(X[0][0] == 5)
solver.add(X[0][1] == 3)
# ... more constraints

if solver.check() == sat:
    m = solver.model()
    for i in range(9):
        print([m[X[i][j]] for j in range(9)])

Bit-Vector Arithmetic

# Solve for x where x * 3 == 21 in 8-bit arithmetic
x = BitVec('x', 8)
solver = Solver()
solver.add(x * 3 == 21)
if solver.check() == sat:
    print(solver.model())

Array Theory

# Find an array where a[0] + a[1] == 10
a = Array('a', IntSort(), IntSort())
solver = Solver()
solver.add(a[0] + a[1] == 10)
solver.add(a[0] > 0)
solver.add(a[1] > 0)
if solver.check() == sat:
    print(solver.model())

Credits

• Z3 solver implementation adapted from Logic-LLM
• MCP interface inspired by clingo-mcp
• Z3 Theorem Prover by Microsoft Research

License

MIT License