z3_mcp
If you are the rightful owner of z3_mcp and would like to certify it and/or have it hosted online, please leave a comment on the right or send an email to henry@mcphub.com.
A Python implementation of abstractions over the Z3 Theorem Prover capabilities using functional programming principles, exposed through a Model Context Protocol (MCP) server.
This project demonstrates how to use the Z3 Theorem Prover with a functional programming approach to solve complex constraint satisfaction problems and analyze relationships between entities. It leverages the `returns` library for functional programming abstractions and exposes its capabilities through an MCP server. The project is structured to include core implementations for solving constraint satisfaction problems and analyzing relationships, data models for constraints and relationships, and an MCP server to expose these capabilities. The technical stack includes the Z3 Solver, Returns library for functional programming, Pydantic for data validation, and FastMCP for the Model Context Protocol.
Features
- Constraint Satisfaction Problems: Solve complex problems with variables and constraints.
- Relationship Analysis: Analyze and infer relationships between entities.
- Functional Programming: Uses pure functions, immutable data structures, and monadic error handling.
- MCP Server: Exposes Z3 capabilities through a standardized interface.
Tools
solve_constraint_problem
Solves a constraint satisfaction problem with a full Problem model.
analyze_relationships
Analyzes relationships between entities with a full RelationshipQuery model.
simple_constraint_solver
A simpler interface for solving constraint problems without requiring the full Problem model.
simple_relationship_analyzer
A simpler interface for analyzing relationships without requiring the full RelationshipQuery model.
