Arithmetic Theory

Int = IntSort()
x = Int('x')
y = Int('y')

Real = RealSort()
a = Real('a')
b = Real('b')

from z3 import *

x = Int('x')
s = Solver()
s.add(x == 42)
print(s.check())  # sat
print(s.model())  # [x = 42]

from z3 import *

x = Real('x')
s = Solver()
s.add(x == RealVal("3/2"))
s.add(x == Q(3, 2))  # Alternative syntax
print(s.check())  # sat

x, y, z = Ints('x y z')
solve(x + y == 10, x > 5)
# [y = 4, x = 6]

x, y = Ints('x y')
solve(x - y == 3, x < 10, y > 0)
# [y = 1, x = 4]

x, y = Ints('x y')
solve(x * y == 12, x > 1, y > 1, x < y)
# [x = 2, y = 6]

x = Real('x')
y = Real('y')
solve(x / y == 2, y == 3)
# [x = 6, y = 3]

a = Int('a')
b = Int('b')
solve(a / b == 2, b == 3, a >= 6, a <= 7)
# Integer division: [a = 6, b = 3]

x = Int('x')
solve(x % 5 == 2, x >= 0, x < 20)
# [x = 2] (could also be 7, 12, 17)

# Remainder operation
solve(x - (x / 5) * 5 == 2)

x = Real('x')
solve(x ** 2 == 16, x > 0)
# [x = 4]

x = Int('x')
solve(-x == 5)
# [x = -5]

x = Int('x')
solve(abs(x) == 5, x < 0)
# [x = -5]

x, y = Ints('x y')
solve(x < y, x + y == 10, x >= 0)
# [x = 4, y = 6]

solve(x <= y, x + y == 10, x >= 5)
# [x = 5, y = 5]

x, y = Ints('x y')
solve(x > y, x + y == 10)
# [y = 4, x = 6]

solve(x >= y, x + y == 10)
# [x = 5, y = 5]

x = Int('x')
y = Real('y')
solve(ToReal(x) == y, x == 5)
# [x = 5, y = 5]

x = Real('x')
y = Int('y')
solve(ToInt(x) == y, x == RealVal("5.7"))
# [x = 5.7, y = 5]  # Truncates toward zero

x = Real('x')
solve(IsInt(x), x > 2.5, x < 4.5)
# [x = 3]

from z3 import *

x = Int('x')
# Create a divisibility constraint: 3 divides x
s = Solver()
k = Int('k')
s.add(x == 3 * k)
s.add(x > 10, x < 20)
print(s.check())
print(s.model())
# [k = 4, x = 12]

from z3 import *

x = Real('x')
solve(x * x == 2, x > 0)
# Z3 can represent sqrt(2) exactly

from z3 import *

val = RealVal("22/7")
s = Solver()
x = Real('x')
y = Real('y')
s.add(x == 22, y == 7)
print(s.check())
# Numerator is 22, denominator is 7

from z3 import *

# Solve a system of linear equations
x, y, z = Reals('x y z')

s = Solver()
s.add(2*x + 3*y - z == 8)
s.add(x - y + 2*z == 5)
s.add(3*x + 2*y + z == 11)

if s.check() == sat:
    m = s.model()
    print(f"x = {m[x]}")
    print(f"y = {m[y]}")
    print(f"z = {m[z]}")
    # x = 1, y = 2, z = 2

# Non-linear constraint
a, b = Reals('a b')
solve(a**2 + b**2 == 25, a > 0, b > 0, a == b)
# [a = 5/√2, b = 5/√2]

# Integer constraint with modulo
n = Int('n')
solve(n % 7 == 3, n > 50, n < 60)
# [n = 52]