from io import StringIO
import z3

from pysmt.smtlib.parser import SmtLibParser, SmtLibScript
from io import StringIO


from joblib import Parallel, delayed, parallel_config


import sys
sys.path.append(".")
from utils.solve import solve, pysmt_solver

statement = """
(declare-fun departure_time () Int)
(declare-fun walking_time () Int)
(declare-fun train_ride () Int)
(declare-fun arrival_time () Int)

(assert (= walking_time 10)) ; time in minutes
(assert (= train_ride 80)) ; time in minutes, 1hr 20min equals 80min
(assert (= arrival_time 900)) ; time in 24hr format, 0900 hours

; convert everything to the same unit (minutes) and calculate departure time
(assert (= departure_time (- arrival_time (+ (/ walking_time 60) (/ train_ride 60)))))

(check-sat)
(get-value (departure_time))
"""


from z3 import *
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
x = Int('x')
y = Int('y')
z = Int('z')
# $a(b+c) = 152$, $b(c+a) = 162$, and $c(a+b) = 170$, then find $abc.$
s = Solver()
s.add(a > 0)
s.add(b > 0)
s.add(c > 0)
s.add(x > 0)
s.add(a*(b+c) == 152-x)
s.add(b*(c+a) == 162+y)
s.add(c*(a+b) == 170*z)
s.add(d != 720)
s.add(d == a*b*c)
s.add(d <= 10000)
print(s.check())
print(s.model())



# if __name__ == "__main__":
#     # s = z3.Solver()
#     # s.from_string(statement)
#     # # t = z3.Tactic("ctx-solver-simplify")
#     # # # t = z3.Tactic("solve-eqs")
#     # # g = z3.Goal()
#     # # cons = z3.parse_smt2_string(statement)
#     # # print(z3.simplify(z3.And(cons[0], cons[2])))
#     # # g.add(cons[1:3])
#     # # print(g, t(g))
#     # print(s.sexpr())
#     # print(s.check())
#     # print(s.model())
#     # print(s)

#     res = solve(statement)
#     print(res)
#     smt_parser = SmtLibParser()
#     script = smt_parser.get_script(StringIO(statement))  
#     print(script)  
#     buf_out = StringIO()
#     script.serialize(buf_out, daggify=False)
#     print(buf_out.getvalue()) 
#     res = solve(statement)
#     print(res)


#     # try:
#     #     with Optimizer(name="z3") as opt:
#     #         logs = script.evaluate(opt) 
#     # except (PysmtInfinityError, PysmtUnboundedOptimizationError) as e:
#     #     print(e)
#     # s = sym_solver()
#     # ok, res = s.sympy_solve(statement)
#     # print(res)


