Create a Boolean variable with the given name.

Create an Integer variable with the given name.

Create a Real (floating-point) variable with the given name.

Create an integer constant with the given value.

Create a real constant with the given value.

Add a constraint to the solver.

Use variable references like 'bool:x', 'int:y', 'real:z' in expressions. Supports standard Z3 Python API syntax.

Solve the current problem and return the result.

Checks all added constraints for satisfiability and returns a model if the problem is SAT.

Get the value of a variable from the model after solving.

Solve with an optimization objective (maximize or minimize).

Finds the optimal value for the given objective function subject to all added constraints.

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']}