import sys
sys.path.append(".")
from utils.sym_solve import sym_solver

# (define-fun inequality_not_satisfied ((x Int)) Bool (not (> (+ (* 5 (pow x 2)) (* 19 x) 16) 20)))

statement = """
; Declare the ratio r
(declare-fun r () Real)

; The coordinates of the octahedron vertices connected to P1
(declare-const Px1 Real)
(declare-const Py1 Real)
(declare-const Pz1 Real)

; The coordinates of the octahedron vertices connected to P1'
(declare-const Px1' Real)
(declare-const Py1' Real)
(declare-const Pz1' Real)

; The ratio r is the same for all vertices on the edges starting from P1
(assert (= Px1 r))
(assert (= Py1 r))
(assert (= Pz1 r))

; The ratio r is the same for all vertices on the edges starting from P1' (which is at (1,1,1))
(assert (= Px1' (- 1 r)))
(assert (= Py1' (- 1 r)))
(assert (= Pz1' (- 1 r)))

; The side length of the octahedron is the distance between two adjacent vertices, which can be calculated
; by the distance formula between (Px1, Py1, 0) and (0, Py1, Pz1)
(declare-fun side_length () Real)
(assert (= side_length (sqrt (+ (expt (- Px1 0) 2) (expt (- Py1 Py1) 2) (expt (- 0 Pz1) 2)))))

; The area of the triangle ATU formed by the intersection of the horizontal plane and the cube's edges is 13.5
; This gives us an equation relating r and the area of the triangle
(assert (= (* 0.5 (* r r)) 13.5))

; We want to minimize r such that the area is still 13.5
(minimize r)

(check-sat)
(get-value (r))
(get-value (side_length))
"""


s = sym_solver()
try:
  s.compile(statement)  
except Exception as e:
  raise e
  print(e)
try:
  res = s.sympy_solve()
except Exception as e:
  # raise e
  print(e)
try:
  res = s.scipy_optim()
except Exception as e:
  raise e
  print(e)
print(res)