Add constraint solver

[aolofsson]

Example:

https://github.com/Z3Prover/z3

from z3 import *
import random

# Declare variables
x = Int('x')
y = Int('y')
powers = [1 << i for i in range(0, 9)]  # 1 to 256

# Create a solver instance
s = Solver()

# Add constraints
s.add(x + y == 12)
s.add(x > 0)       # positive
s.add(x % 2 == 0)  # even
s.add(y > x) # comparison
s.add(Or([y == p for p in powers])) # power of 2 (one of many solutions, wanted to stay with int)

# find all solutions
solutions = []
print(f"Finding Solution:")
while s.check() == sat:
    m = s.model()
    x_val = m[x].as_long()
    y_val = m[y].as_long()
    solutions.append((x_val, y_val))
    print(f"x = {x_val}, y = {y_val}")

    # Add blocking clause to exclude current solution
    s.add(Or(x != x_val, y != y_val))

print(f"\nTotal solutions: {len(solutions)}")

# randomize execution
print(f"\nRandomized Order:")
random.shuffle(solutions)
for x_val, y_val in solutions:
    print(f"x = {x_val}, y = {y_val}")

[aolofsson]