18 lines
228 B
Python
18 lines
228 B
Python
#!/usr/bin/env python3
|
|
|
|
from z3 import *
|
|
|
|
x = Real('x')
|
|
y = Real('y')
|
|
|
|
eq1 = x + y == 5
|
|
eq2 = x - y == 3
|
|
|
|
s = Solver()
|
|
s.add(eq1, eq2)
|
|
|
|
if s.check() == sat:
|
|
print("Solution:", s.model())
|
|
else:
|
|
print("No solution found")
|