from io import StringIO
import z3
from z3 import z3rcf

import sys
sys.path.insert(0, '/home/argustest/pysmt')
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 p () Real)
(declare-fun x () Real)


(assert (> p 0))
(assert (< p 15))
(assert (<= p x))
(assert (<= x 15))

(define-fun f () Real 
    (+ (abs (- x p)) 
       (abs (- x 15)) 
       (abs (- x (+ p 15)))))

(assert (not (>= f 15)))

(check-sat)

(get-model)
"""

if __name__ == "__main__":
    # s = z3.Solver()
    # s.from_string(statement)
    # print(s.check())
    # m = s.model()
    # print(m)
    # # # 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)
    # print(s.sexpr())
    # print(m.decls())
    # print(z3.is_arith(m[m[0]]), m[m[0]], m[m[0]].is_real(), type(m[m[0]]))

    # res = solve(statement, verbose=True)
    # print(res)
    # print(pysmt_solver(statement, solver_name='cvc5'))
    print(pysmt_solver(statement, solver_name='z3'))
    # print(pysmt_solver(statement, solver_name='cvc4'))
    # print(pysmt_solver(statement, solver_name='msat'))
    smt_parser = SmtLibParser()
    script = smt_parser.get_script(StringIO(statement))  
    print(script)  
    buf_out = StringIO()
    # script.serialize(buf_out, comment=True, daggify=False)
    # statement = buf_out.getvalue()
    # print(buf_out.getvalue()) 
    # res = solve(statement, verbose=True)
    # 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)


