Mcp Z3 Prover

Wraps the Z3 theorem prover so you can solve constraint satisfaction and optimization problems through MCP tools. Create Boolean, integer, and real variables, add constraints in a straightforward string syntax, then call solve or optimize to get satisfying assignments. The factorization example shows the flavor: define two integer variables p and q, constrain their product to equal a target number, add bounds and parity checks, and let Z3 find the factors. Useful when you need symbolic math solving, SMT queries, or constraint-based search without writing Python scripts directly. Each solver session maintains state across calls until you reset it.