io.github.daedalus/mcp-z3-prover

Create a Boolean variable with the given name. Args: name: The name of the boolean variable to create. Returns: The variable reference string in the format 'bool:<name>'. Raises: ValueError: If a variable with the given name already exists. Example: >>> create_bool_var("x") 'bool:x'

Create an Integer variable with the given name. Args: name: The name of the integer variable to create. Returns: The variable reference string in the format 'int:<name>'. Raises: ValueError: If a variable with the given name already exists. Example: >>> create_int_var("n") 'int:n'

Create a Real (floating-point) variable with the given name. Args: name: The name of the real variable to create. Returns: The variable reference string in the format 'real:<name>'. Raises: ValueError: If a variable with the given name already exists. Example: >>> create_real_var("x") 'real:x'

Create an integer constant with the given value. Args: value: The integer value for the constant. Returns: The constant reference string in the format 'int:<value>'. Example: >>> create_int_constant(42) 'int:42'

Create a real constant with the given value. Args: value: The real value for the constant. Returns: The constant reference string in the format 'real:<value>'. Example: >>> create_real_constant(3.14) 'real:3.14'

Add a constraint to the solver. Use variable references like 'bool:x', 'int:y', 'real:z' in expressions. Supports standard Z3 Python API syntax. Args: constraint: A Z3 constraint expression as a string. Returns: A dictionary with status and the constraint that was added. Raises: ValueError: If the constraint cannot be parsed. Example: >>> create_int_var("x") 'int:x' >>> create_int_var("y") 'int:y' >>> add_constraint("int:x + int:y > 10") {'status': 'success', 'constraint': 'int:x + int:y > 10'}

Solve the current problem and return the result. Checks all added constraints for satisfiability and returns a model if the problem is SAT. Args: timeout_ms: Timeout in milliseconds for the solver. Returns: A dictionary containing: - status: 'sat', 'unsat', or 'unknown' - model: (if sat) A dictionary of variable assignments - message: (if unsat/unknown) A description of the result Example: >>> create_int_var("x") 'int:x' >>> create_int_constant(5) 'int:5' >>> add_constraint("int:x > int:5") {'status': 'success', 'constraint': 'int:x > int:5'} >>> solve() {'status': 'sat', 'model': {'x': '6'}}

Get the value of a variable from the model after solving. Args: variable: The variable reference (e.g., 'int:x', 'bool:y'). Returns: The value of the variable as a string. Raises: RuntimeError: If solve() has not been called yet. ValueError: If the variable is not known. Example: >>> create_int_var("x") 'int:x' >>> add_constraint("int:x == 42") {'status': 'success', 'constraint': 'int:x == 42'} >>> solve() {'status': 'sat', 'model': {'x': '42'}} >>> get_model_value("int:x") '42'

Solve with an optimization objective (maximize or minimize). Finds the optimal value for the given objective function subject to all added constraints. Args: objective: The expression to optimize (e.g., 'int:x + int:y'). maximize: If True, maximize the objective; if False, minimize. timeout_ms: Timeout in milliseconds for the optimizer. Returns: A dictionary containing: - status: 'sat', 'unsat', or 'unknown' - optimal_value: (if sat) The optimal value of the objective - model: (if sat) A dictionary of variable assignments - message: (if unsat/unknown) A description of the result Example: >>> create_int_var("x") 'int:x' >>> create_int_var("y") 'int:y' >>> add_constraint("int:x + int:y == 10") {'status': 'success', 'constraint': 'int:x + int:y == 10'} >>> add_constraint("int:x >= 0") {'status': 'success', 'constraint': 'int:x >= 0'} >>> add_constraint("int:y >= 0") {'status': 'success', 'constraint': 'int:y >= 0'} >>> optimize("int:x - int:y", maximize=True) {'status': 'sat', 'optimal_value': '10', 'model': {'x': '10', 'y': '0'}}

Reset the solver state. Clears all variables, constants, constraints, and model data. Useful when starting a new problem. Returns: A dictionary with status and a success message. Example: >>> create_int_var("x") 'int:x' >>> add_constraint("int:x > 5") {'status': 'success', 'constraint': 'int:x > 5'} >>> reset_solver() {'status': 'success', 'message': 'Solver reset successfully'} >>> list_variables() {'variables': []}

List all created variables. Returns: A dictionary containing a list of all variable references. Example: >>> create_int_var("x") 'int:x' >>> create_bool_var("flag") 'bool:flag' >>> list_variables() {'variables': ['int:x', 'bool:flag']}