class Context:
    def __init__(self, *args, **kws)

# Use default context
x = Int('x')

# Create custom context
ctx = Context()
y = Int('y', ctx)

# Context with configuration
ctx2 = Context(timeout=5000)

ctx.interrupt()

descrs = ctx.param_descrs()

class Solver:
    def __init__(self, solver=None, ctx=None, logFile=None)

s = Solver()
x = Int('x')
s.add(x > 0, x < 10)

result = s.check()
if result == sat:
    print("Satisfiable")

if s.check() == sat:
    m = s.model()
    print(m)

s.push()
s.add(x > 5)
s.check()
s.pop()  # Restore previous state

s.reset()

s.assert_and_track(x > 0, 'positive')

if s.check() == unsat:
    core = s.unsat_core()
    print(core)

s.set('timeout', 5000)  # 5 second timeout
s.set('random_seed', 42)

s.check()
stats = s.statistics()
print(stats)

x = Int('x')

x, y, z = Ints('x y z')

a = Real('a')

a, b, c = Reals('a b c')

five = IntVal(5)

pi = RealVal("3.14159")
half = RealVal(1, 2)  # Fraction: 1/2

p = Bool('p')

p, q, r = Bools('p q r')

t = BoolVal(True)
f = BoolVal(False)

x = BitVec('x', 32)  # 32-bit bitvector

x, y, z = BitVecs('x y z', 32)

val = BitVecVal(42, 32)
hex_val = BitVecVal(0xFF, 8)

s = String('s')

hello = StringVal("hello")

x, y = Ints('x y')

# Arithmetic
z = x + y
z = x - y
z = x * y
z = x / y  # Integer division for Int
z = x % y  # Modulo
z = -x     # Negation

# Comparison
c = x > y
c = x >= y
c = x < y
c = x <= y
c = x == y
c = x != y

p, q = Bools('p q')

# Logical operators
r = And(p, q)
r = Or(p, q)
r = Not(p)
r = Implies(p, q)
r = Xor(p, q)

x, y = BitVecs('x y', 32)

# Arithmetic
z = x + y
z = x - y
z = x * y
z = x / y   # Unsigned division
z = x % y   # Unsigned modulo

# Bitwise
z = x & y   # AND
z = x | y   # OR
z = x ^ y   # XOR
z = ~x      # NOT
z = x << 2  # Left shift
z = x >> 2  # Logical right shift

# Comparison
c = ULT(x, y)  # Unsigned less than
c = UGT(x, y)  # Unsigned greater than

result = And(p, q, r)
result = And([p, q, r])  # Can also take a list

result = Or(p, q, r)

result = Not(p)

result = Implies(p, q)

result = Xor(p, q)

x = Int('x')
y = Int('y')
formula = ForAll([x], x + 0 == x)

x = Int('x')
formula = Exists([x], And(x > 0, x < 10))

A = Array('A', IntSort(), IntSort())

value = Select(A, 5)
value = A[5]  # Equivalent

A2 = Store(A, 5, 10)  # A2 is A with index 5 set to 10

s1 = String('s1')
s2 = String('s2')
result = Concat(s1, s2)

len_s = Length(s1)

sub = SubString(s1, 0, 5)

constraint = PrefixOf(StringVal("hello"), s1)

constraint = SuffixOf(StringVal(".txt"), s1)

constraint = Contains(s1, StringVal("world"))

x = Bool('x')
expr = And(x, Or(x, False))
simplified = simplify(expr)  # Returns: x

x, y = Ints('x y')
expr = x + y
new_expr = substitute(expr, (x, IntVal(5)))

x = Int('x')
solve(x > 0, x < 10)
# Prints a satisfying assignment

x = Int('x')
prove(x + 0 == x)  # Attempt to prove this is always true

int_sort = IntSort()

real_sort = RealSort()

bool_sort = BoolSort()

bv32_sort = BitVecSort(32)

string_sort = StringSort()

array_sort = ArraySort(IntSort(), IntSort())

Object = DeclareSort('Object')

# f: Int × Int → Int
f = Function('f', IntSort(), IntSort(), IntSort())

# Application
x, y = Ints('x y')
result = f(x, y)

fac = RecFunction('fac', IntSort(), IntSort())
x = Int('x')
RecAddDefinition(fac, [x], If(x == 0, 1, x * fac(x - 1)))

m = s.model()
val = m[x]

result = m.eval(x + y)

for d in m.decls():
    print(f"{d.name()} = {m[d]}")

major, minor, build, rev = get_version()

version = get_version_string()  # e.g., "4.12.2"

full_version = get_full_version()

set_param('timeout', 5000)
set_param('verbose', 2)

is_int(expr)       # Check if integer expression
is_real(expr)      # Check if real expression
is_bool(expr)      # Check if Boolean expression
is_bv(expr)        # Check if bitvector expression
is_string(expr)    # Check if string expression
is_array(expr)     # Check if array expression
is_const(expr)     # Check if constant
is_expr(expr)      # Check if expression
is_sort(s)         # Check if sort