RiSE4fun samples for Z3Py

solve

x, y = Reals('x y') solve(x**2 + y**2 < 1, 2*x + y > 1, show=True)

simple

# Declare three Real variables x, y, z = Reals('x y z') # Solve linear problem solve(x >= 1, y >= 1, z >= 1, x == y + z, x + y <= 4)

strategy

x = Real('x') # Create a solver using simplify and nlsat tactics s = Then('simplify', 'nlsat').solver() s.add(x**2 == 2) print s.check() print s.model() # Increase number of decimal places set_option(precision=50) print s.model()

nonlinear

x, y, z = Reals('x y z') solve(x**2 + y**2 < 1, x*y > 1, show=True) solve(x**2 + y**2 < 1, x*y > 0.4, show=True) solve(x**2 + y**2 < 1, x*y > 0.4, x < 0, show=True) solve(x**5 - x - y == 0, Or(y == 1, y == -1), show=True)

geometry

x1, x2, x3, x4 = Reals('x1 x2 x3 x4') u1, u2, u3 = Reals('u1 u2 u3') antecedent = And( x2 - u3 == 0, u3*(x1 - u1) - x2*u2 == 0, x4*x1 - x3*u3 == 0, x4*(u2 - u1) - u3*(x3 - u1) == 0, ) claim1 = x1**2 - 2*x1*x3 - 2*x4*x2 + x2**2 == 0 prove(Implies(antecedent, claim1)) # Strengthening antencedent antecedent = And(antecedent, u1 != 0, u3 != 0) prove(Implies(antecedent, claim1)) claim2 = 2*x3*u1 - 2*x3*u2 - 2*x4*u3 - u1**2 + u2**2 + u3**2 == 0 prove(Implies(antecedent, claim2))