Z3 Theorem Prover with Functional Programming

関数型プログラミングによるZ3定理証明器

関数型プログラミングの原則を用いてZ3定理証明器の機能を抽象化し、Model Context Protocol（MCP）サーバーを通じて公開するPython実装です。

概要

このプロジェクトでは、Z3定理証明器を関数型プログラミングのアプローチで使用し、複雑な制約充足問題を解決して、エンティティ間の関係を分析する方法を紹介します。関数型プログラミングの抽象化にはreturnsライブラリを活用し、MCP サーバーを通じてその機能を公開します。

機能

• 制約充足問題：変数と制約を含む複雑な問題を解決します
• 関係分析：エンティティ間の関係を分析し、推論します
• 関数型プログラミング：純粋関数、不変データ構造、モナドによるエラー処理を使用します
• MCP サーバー：標準化されたインターフェースを通じてZ3の機能を公開します

プロジェクト構成

z3_mcp/
├── core/                  # Core implementation
│   ├── solver.py          # Constraint satisfaction problem solving
│   └── relationships.py   # Relationship analysis
├── models/                # Data models
│   ├── constraints.py     # Models for constraint problems
│   └── relationships.py   # Models for relationship analysis
├── server/                # MCP server
│   └── main.py            # Server implementation
└── examples/              # Example usage
    └── main.py            # Demonstration of capabilities

技術スタック

• Z3 Solver：制約を解くためのMicrosoft製定理証明器
• Returns：モナド操作とエラー処理のための関数型プログラミングライブラリ
• Pydantic：データの検証とシリアライズ
• FastMCP：Model Context Protocolの実装

インストール

このプロジェクトでは依存関係の管理にuvを使用します。

# Clone the repository
git clone https://github.com/javergar/z3_mcp.git
cd z3_mcp

# Install dependencies
uv pip install -e .

# Install development dependencies (optional)
uv pip install -e ".[dev]"

使用方法

サンプルの実行

このプロジェクトには、Z3ソルバーの機能を紹介するサンプルがいくつか含まれています。

# Run the examples
python -m z3_poc.examples.main

サンプルには次のものがあります。

• N-クイーン問題
• 家族関係の推論
• 因果関係を伴う時間推論
• 文字算（SEND + MORE = MONEY）

MCP サーバーの実行

MCP サーバーを起動して、Model Context Protocolを通じてZ3の機能を公開します。

# Run the server
python -m z3_poc.server.main

Claude/ClineでMCP サーバーを設定する

VSCodeのCline拡張機能を通じてClaudeでZ3ソルバーのMCP サーバーを使用するには、settings.jsonファイルを設定する必要があります。

1. 設定：設定ファイルのmcpServersオブジェクトに次の内容を追加します。

"z3-solver": {
  "command": "uv",
  "args": [
    "--directory",
    "/path/to/your/z3_poc",
    "run",
    "z3_poc/server/main.py"
  ],
  "disabled": false,
  "autoApprove": [
    "simple_constraint_solver", 
    "simple_relationship_analyzer", 
    "solve_constraint_problem", 
    "analyze_relationships"
  ]
}

2. 設定オプション：

   • command：実行するコマンド（Python環境の管理にはuvを使用します）
   • args：プロジェクトへのパスとサーバースクリプトを含むコマンド引数
   • disabled：サーバーを有効にするにはfalseに設定します
   • autoApprove：明示的な承認なしで使用できるツールの一覧

3. 再起動：設定を更新した後、変更を反映するためにVSCodeまたはClaude Desktopアプリを再起動します。

設定すると、ClaudeはMCP サーバーを通じてZ3ソルバーの機能を利用できるようになります。

MCP ツール

サーバーは次のツールを提供します。

solve_constraint_problem

完全なProblemモデルを使用して、制約充足問題を解決します。

# Example input
{
  "problem": {
    "variables": [
      {"name": "x", "type": "integer"},
      {"name": "y", "type": "integer"}
    ],
    "constraints": [
      {"expression": "x + y == 10"},
      {"expression": "x >= 0"},
      {"expression": "y >= 0"}
    ],
    "description": "Find non-negative values for x and y that sum to 10"
  }
}

analyze_relationships

完全なRelationshipQueryモデルを使用して、エンティティ間の関係を分析します。

# Example input
{
  "query": {
    "relationships": [
      {"person1": "Alice", "person2": "Bob", "relation": "sibling"},
      {"person1": "Bob", "person2": "Charlie", "relation": "sibling"}
    ],
    "query": "sibling(Alice, Charlie)"
  }
}

simple_constraint_solver

完全なProblemモデルを必要としない、制約問題を解決するための簡易インターフェースです。

# Example input
{
  "variables": [
    {"name": "x", "type": "integer"},
    {"name": "y", "type": "integer"}
  ],
  "constraints": [
    "x + y == 10",
    "x <= 5",
    "y <= 5"
  ],
  "description": "Find values for x and y"
}

simple_relationship_analyzer

完全なRelationshipQueryモデルを必要としない、関係を分析するための簡易インターフェースです。

# Example input
{
  "relationships": [
    {"person1": "Bob", "person2": "Hanna", "relation": "sibling"},
    {"person1": "Bob", "person2": "Claudia", "relation": "sibling"}
  ],
  "query": "sibling(Hanna, Claudia)"
}

関数型プログラミングのアプローチ

このプロジェクトでは、関数型プログラミングの原則をいくつか紹介します。

1. 不変データ構造：不変のデータ表現にPydanticモデルを使用します
2. Result型：例外を使わずにエラーを処理するため、returns.result.Resultを使用します
3. Maybe型：null許容値を処理するため、returns.maybe.Maybeを使用します
4. Do記法：逐次処理にResult.do()を使ったジェネレーター式を使用します
5. パターンマッチング：異なる結果型を処理するため、Pythonのmatch-caseを使用します

analyze_relationshipsにおけるDo記法の例：

expr = (
    RelationshipResult(...)
    for entities in create_entities(query.relationships)
    for relations in create_relations(query.relationships)
    for _ in add_relationship_assertions(solver, query.relationships, entities, relations)
    for query_expr in parse_query(query.query, entities, relations)
    for (result, explanation, is_satisfiable) in evaluate_query(solver, query_expr)
)

return Result.do(expr)

コントリビューション

コントリビューションを歓迎します。お気軽にPull Requestを送信してください。

ライセンス

このプロジェクトはMITライセンスの下で公開されています。詳細についてはLICENSEファイルをご覧ください。