Mcp Z3 Prover

io.github.daedalus由 GitHub 帳號 daedalus 發布v0.1.0更新於 Oct 28, 2026

MCP server exposing Z3 solver API

已驗證STDIO僅桌面開發者工具AI 與機器學習

概覽

AI 產生的概覽

本機 MCP 伺服器，包裝 Z3 求解器，讓助理建立變數與限制式並進行求解或最佳化。

可以做什麼
  • 建立布林、整數與實數變數，以及整數或實數常數
  • 將限制式加入求解器並求解目前問題
  • 從結果模型中讀取變數值
  • 帶最佳化目標進行求解
  • 重設求解器狀態並列出已建立的變數
適用情境
適合讓助理判斷一組邏輯或算術限制式是否可滿足、找出滿足條件的賦值，或對目標進行最佳化，例如小規模因數分解或邏輯謎題類問題。
執行需求
以本機程序執行，需從 PyPI 安裝 mcp-z3-prover 套件（pip install mcp-z3-prover），並以 mcp-z3-prover 指令啟動；僅支援桌面環境。未宣告驗證、環境變數或標頭。
安裝前請注意
求解器在多次呼叫間保留狀態，限制式會持續累積，需重設才能清空；困難問題可能耗時較久或佔用大量 CPU。未顯示需要憑證、付費或將資料送往第三方。

安裝

在 SourceWeft 中

  1. 開啟 儀表板中的 Mcp Z3 Prover，將其新增到工作區。
  2. 為需要使用其工具的對話啟用該服務。

Desktop only，透過 STDIO。 STDIO 服務會啟動本機處理程序，因此需要 SourceWeft 桌面主機。

其他 MCP 客戶端

參照 儲存庫 中的啟動說明。

README

mcp-z3-prover

MCP server exposing Z3 solver API

[PyPI] [Python] [Ruff]

Install

bash
pip install mcp-z3-prover

Usage

python
from mcp_z3_prover import mcp
# Run the servermcp.run()

Or from command line:

bash
mcp-z3-prover

MCP Tools

The server exposes the following tools:

  • create_bool_var - Create a Boolean variable
  • create_int_var - Create an Integer variable
  • create_real_var - Create a Real variable
  • create_int_constant - Create an integer constant
  • create_real_constant - Create a real constant
  • add_constraint - Add a constraint to the solver
  • solve - Solve the current problem
  • get_model_value - Get value of a variable from the model
  • optimize - Solve with optimization objective
  • reset_solver - Reset the solver state
  • list_variables - List all created variables

Example

python
# Create variablescreate_int_var("x")create_int_var("y")
# Add constraintsadd_constraint("int:x + int:y == 10")add_constraint("int:x > 0")add_constraint("int:y > 0")
# Solveresult = solve()# Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}
# Get specific valuesx_val = get_model_value("int:x")

Integer Factorization Example

python
# Factor n = 4295229443 where n = p * q with q <= sqrt(n)create_int_var("p")create_int_var("q")
# Add constraintsadd_constraint("int:p * int:q == 4295229443")add_constraint("4295229443 > int:p")add_constraint("4295229443 > int:q")add_constraint("int:q <= 65537")  # sqrt(4295229443) ≈ 65537add_constraint("int:q > 1")add_constraint("int:p > 1")add_constraint("int:q % 2 != 0")  # q is oddadd_constraint("int:p % 2 != 0")  # p is odd
# Solveresult = solve()# Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}# Verification: 65537 * 65539 = 4295229443

Development

bash
git clone https://github.com/daedalus/mcp-z3-prover.gitcd mcp-z3-proverpip install -e ".[test]"
# run testspytest
# formatruff format src/ tests/
# lintruff check src/ tests/
# type checkmypy src/

MCP Registration

mcp-name: io.github.daedalus/mcp-z3-prover

來源：README.md，提交 12bcd34

工具

0
SourceWeft 尚未在沙箱中啟動過該軟體包，因此其工具未知。

版本歷史

1
  1. v0.1.0最新Sep 16, 2026

評分

已滿足適用檢查項的 50%

該評分衡量此收錄條目的完整程度，依據註冊中心條目、端點與公開來源計算得出。它不是對伺服器本身的評價，也不表示伺服器安全或目前可用：可連通性是帶日期的檢查結果，評分也不包含安裝量或使用者評價。

  • 近 30 天內可連通25 分

    請保持端點能夠回應 MCP 握手；SourceWeft 每 30 天探測一次。

  • 已宣告認證方式10 分

    請在註冊中心條目中宣告憑證請求標頭，或保持端點能夠回應探測，以便判定其認證方式。

  • 已列出工具15 分

    請讓伺服器在無憑證時回應 tools/list，或發布可在沙箱中無憑證啟動的軟體包。

  • 描述必需15 分
  • 圖示10 分
  • 文件15 分
  • 授權條款10 分