English Français العربية

io.github.daedalus/mcp-z3-prover

السجل الرسمي أخرى

MCP server exposing Z3 solver API

الشيفرة المصدرية التوثيق

ماذا يمكنك أن تفعل مع io.github.daedalus/mcp-z3-prover؟

  • 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

التثبيت

أضف هذا إلى إعدادات MCP في عميلك (Claude Desktop: claude_desktop_config.json، وCursor: ‏.cursor/mcp.json، ويستخدم VS Code وغيره الصيغة نفسها «mcpServers»).

PYPI package mcp-z3-prover
Claude Code 
claude mcp add mcp-z3-prover -- uvx mcp-z3-prover==0.1.0
إعداد JSON (Claude Desktop وCursor وVS Code) 
{
    "mcpServers": {
        "mcp-z3-prover": {
            "command": "uvx",
            "args": [
                "mcp-z3-prover==0.1.0"
            ]
        }
    }
}

التوثيق

مأخوذ من ملف README للمشروع على GitHub ويُحدَّث أسبوعيًا. تفتح الروابط على GitHub.

المحتويات
  1. mcp-z3-prover
  2. Install
  3. Usage
  4. MCP Tools
  5. Example
  6. Development
  7. MCP Registration

mcp-z3-prover

MCP server exposing Z3 solver API

Install

pip install mcp-z3-prover

Usage

from mcp_z3_prover import mcp

# Run the server
mcp.run()

Or from command line:

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

# Create variables
create_int_var("x")
create_int_var("y")

# Add constraints
add_constraint("int:x + int:y == 10")
add_constraint("int:x > 0")
add_constraint("int:y > 0")

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}

# Get specific values
x_val = get_model_value("int:x")
Integer Factorization Example
# Factor n = 4295229443 where n = p * q with q <= sqrt(n)
create_int_var("p")
create_int_var("q")

# Add constraints
add_constraint("int:p * int:q == 4295229443")
add_constraint("4295229443 > int:p")
add_constraint("4295229443 > int:q")
add_constraint("int:q <= 65537")  # sqrt(4295229443) ≈ 65537
add_constraint("int:q > 1")
add_constraint("int:p > 1")
add_constraint("int:q % 2 != 0")  # q is odd
add_constraint("int:p % 2 != 0")  # p is odd

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}
# Verification: 65537 * 65539 = 4295229443

Development

git clone https://github.com/daedalus/mcp-z3-prover.git
cd mcp-z3-prover
pip install -e ".[test]"

# run tests
pytest

# format
ruff format src/ tests/

# lint
ruff check src/ tests/

# type check
mypy src/

MCP Registration

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

الأسئلة الشائعة

ما هو io.github.daedalus/mcp-z3-prover؟

MCP server exposing Z3 solver API

كيف أثبّت io.github.daedalus/mcp-z3-prover؟

يعمل على جهازك. في Claude Code: claude mcp add mcp-z3-prover -- uvx mcp-z3-prover==0.1.0. وفي العملاء الآخرين، الصق إعداد JSON من هذه الصفحة في إعدادات MCP الخاصة بهم.

هل يحتاج io.github.daedalus/mcp-z3-prover إلى مفتاح API؟

لا يذكر إدراجه في السجل أي مفتاح أو سر إلزامي. قد تتطلب بعض الميزات حسابًا لدى الخدمة التي يتصل بها.

هل io.github.daedalus/mcp-z3-prover مفتوح المصدر؟

نعم. شيفرته متاحة على GitHub بترخيص MIT.

من يصون io.github.daedalus/mcp-z3-prover؟

ينشره daedalus. يدرجه AI.tn لكنه لا يصونه ولا يوصي به.

من سجل MCP الرسمي. الإدراج ليس توصية: راجع شيفرة الخادم وصلاحياته قبل منحه الوصول إلى بياناتك.