Execute Z3 Python code to solve SMT constraints.

The code can use any Z3 Python API functions. Common imports (Solver, Int, Real, Bool, And, Or, Not, etc.) are pre-loaded.

Example:

x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x + y == 10)
solver.add(x - y == 4)
if solver.check() == sat:
    print(solver.model())

Solve an SMT problem in SMT-LIB 2.0 format.

Example:

(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (- x y) 4))
(check-sat)
(get-model)

Check satisfiability of a list of constraints.

Provide constraints as Z3 Python expressions. Variables will be auto-declared based on usage.

Example constraints:

• "x + y == 10"

• "x > 0"

• "And(x < 100, y < 100)"

Attempt to prove a theorem by showing its negation is unsatisfiable.

Provide the theorem as a Z3 expression. If the negation is unsatisfiable, the theorem is proven.

Example: prove "ForAll([x], x + 0 == x)" for integer x

Simplify a Z3 expression.

Returns the simplified form of the given expression.

Example: simplify "And(x > 0, x > 0)" -> "x > 0"

Solve a structured logic program (Logic-LLM format).

The program should have sections:

Declarations

• EnumSort, IntSort, Function declarations

Constraints

• Logical constraints

Example:

# Declarations
Color = EnumSort([red, green, blue])
assign = Function(Object -> Color)

# Constraints
assign(obj1) != assign(obj2)

Add a variable to the current solver session.

Supported types: int, real, bool, bitvec (with bits parameter)

Add a constraint to the current solver session.

The constraint should be a valid Z3 expression using previously declared variables.

Check satisfiability of current session constraints and get the model if satisfiable.

Push a new context onto the solver stack (for backtracking).

Pop a context from the solver stack (backtrack).

Reset the current solver session, clearing all variables and constraints.

List all active solver sessions.