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

# Run directly
z3smt-mcp

# Or via Python
python -m z3smt_mcp.server

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

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

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

(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (- x y) 4))
(check-sat)
(get-model)

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

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

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

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

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

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

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

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