Z3 MCP

🚀 Z3 Theorem Prover and Functional Programming Project

This project is a Python-based implementation that demonstrates how to use the Z3 theorem prover to solve complex constraint satisfaction problems and analyze the relationships between entities. Additionally, it exposes these functionalities through the MCP (Machine-Readable Configuration) server interface.

✨ Features

• Complex Constraint Handling: Capable of solving constraint satisfaction problems involving multiple variables and conditions.
• Relationship Analysis: Supports the reasoning and verification of relationships between entities.
• Functional Programming Style: Adopts functional programming principles such as immutable data structures, result types, and Maybe types to ensure code simplicity and maintainability.
• MCP Server Interface: Provides a standardized machine-readable configuration interface for easy integration with external systems.

📦 Project Structure

z3_project/
├── README.md          # Project documentation
├── LICENSE           # License file
├── setup.py          # Project installation script
├── requirements.txt  # Dependency management file
├── src/
│   ├── __init__.py    # Package initialization file
│   ├── solver.py      # Constraint solver implementation
│   ├── relations.py   # Relationship reasoning module
│   └── server.py      # MCP server implementation

🔧 Technical Details

• Z3: An efficient theorem proving tool developed by Microsoft.
• Pydantic: A library for data validation and settings construction.
• Returns: A functional programming extension library that supports the handling of result types and Maybe types.
• FastMCP: A lightweight machine-readable configuration server framework.

📦 Installation

1. Clone the project repository:

   git clone https://github.com/yourusername/z3_project.git
   cd z3_project
   

2. Install dependencies:

   pip install -r requirements.txt
   

3. Optional: Install development tools:

   pip install pre-commit
   

💻 Usage Examples

Basic Usage

• Constraint Solving Example:

  from src.solver import solve_constraints
  variables = ['x', 'y']
  constraints = ["x + y == 10", "x <= 5"]
  solution = solve_constraints(variables, constraints)
  print(solution)  # Output the possible solution set
  

• Relationship Reasoning Example:

  from src.relations import infer_relations
  relations_data = [
      ("Bob", "Hanna", "sibling"),
      ("Bob", "Charlie", "sibling")
  ]
  inferred = infer_relations(relations_data)
  print(inferred)  # Output the inferred relationships
  

Advanced Usage

Start the MCP Server

uvicorn src.server:app --reload

MCP Server Configuration

Simple Constraint Solving Interface

Request Format:

{
  "variables": [
    {"name": "x", "type": "integer"},
    {"name": "y", "type": "integer"}
  ],
  "constraints": ["x + y == 10"],
  "description": "Find values of x and y that satisfy the conditions"
}

Simple Relationship Reasoning Interface

Request Format:

{
  "relationships": [
    {"person1": "Bob", "person2": "Hanna", "relation": "sibling"},
    {"person1": "Bob", "person2": "Charlie", "relation": "sibling"}
  ],
  "query": "sibling(Hanna, Charlie)"
}

📚 Functional Programming Methods

This project demonstrates various functional programming techniques:

• Immutable Data Structures: Achieve data immutability through Pydantic models.
• Result Types: Use returns.result.Result to handle errors and avoid throwing exceptions.
• Maybe Types: Adopt returns.maybe.Maybe to handle optional values.
• Do Notation: Combine generator expressions and Result.do() to implement operation sequences.
• Pattern Matching: Utilize Python's match-case structure to improve code readability.

Example Code

expr = (
    RelationshipResult(...)
    for entities in create_entities()
    if entities
)

📄 License

This project is licensed under the MIT License, allowing free use, modification, and distribution.

💪 Contribution Guidelines

Contributions are welcome! Please read CONTRIBUTING.md first to learn how to participate in the development.