import sys
sys.path.append(".")
from utils.complify import mutate
from utils.solve import solve 
import time
import utils.gpt as gpt

statement = """
(declare-fun x () Real)
(declare-fun y () Real)

; Rewrite the given equation
(assert (= (- (pow y 4) (* 4 (pow x 4))) (- 1 (* 2 (pow y 2)))))

; Define possible conic sections
(define-fun is_circle () Bool (= (+ (pow x 2) (pow y 2)) 1))
(define-fun is_ellipse () Bool (and (< (+ (pow x 2) (pow y 2)) 1) (> (+ (pow x 2) (pow y 2)) 0)))
(define-fun is_hyperbola () Bool (< (- (pow y 2) (pow x 2)) 1))
(define-fun is_parabola () Bool (and (not (= (+ (pow x 2) (pow y 2)) 1)) (not (< (+ (pow x 2) (pow y 2)) 1)) (not (> (+ (pow x 2) (pow y 2)) 1))))

; Define the possible combinations of conic sections
(define-fun circle_circle () Bool (and is_circle is_circle))
(define-fun circle_ellipse () Bool (and is_circle is_ellipse))
(define-fun circle_hyperbola () Bool (and is_circle is_hyperbola))
(define-fun circle_parabola () Bool (and is_circle is_parabola))

(define-fun ellipse_circle () Bool (and is_ellipse is_circle))
(define-fun ellipse_ellipse () Bool (and is_ellipse is_ellipse))
(define-fun ellipse_hyperbola () Bool (and is_ellipse is_hyperbola))
(define-fun ellipse_parabola () Bool (and is_ellipse is_parabola))

(define-fun hyperbola_circle () Bool (and is_hyperbola is_circle))
(define-fun hyperbola_ellipse () Bool (and is_hyperbola is_ellipse))
(define-fun hyperbola_hyperbola () Bool (and is_hyperbola is_hyperbola))
(define-fun hyperbola_parabola () Bool (and is_hyperbola is_parabola))

(define-fun parabola_circle () Bool (and is_parabola is_circle))
(define-fun parabola_ellipse () Bool (and is_parabola is_ellipse))
(define-fun parabola_hyperbola () Bool (and is_parabola is_hyperbola))
(define-fun parabola_parabola () Bool (and is_parabola is_parabola))

; Check which of the combinations is true
(assert (or circle_circle circle_ellipse circle_hyperbola circle_parabola
            ellipse_circle ellipse_ellipse ellipse_hyperbola ellipse_parabola
            hyperbola_circle hyperbola_ellipse hyperbola_hyperbola hyperbola_parabola
            parabola_circle parabola_ellipse parabola_hyperbola parabola_parabola))
(check-sat)
(get-value (circle_circle circle_ellipse circle_hyperbola circle_parabola
            ellipse_circle ellipse_ellipse ellipse_hyperbola ellipse_parabola
            hyperbola_circle hyperbola_ellipse hyperbola_hyperbola hyperbola_parabola
            parabola_circle parabola_ellipse parabola_hyperbola parabola_parabola))
"""

if __name__ == "__main__":
    t0 = time.time()
    print(statement)
    ok, solution = solve(statement, verbose=True)
    print(ok, solution)
    new_statement = mutate(statement, tactic='mcmc', rm_aux=True, \
                                                allow_real=False, simplify=True, rename=False)
    print(new_statement)
    ok, solution = solve(new_statement)
    t1 = time.time()
    print(t1-t0, solution)
        
    # client = gpt_utils.set_api_key(1)
    # prompt = f"Translate the math problem formulated with SMT-LIB back to a natural language problem. Please ensure the problem to be a math word problem. {statement}"
    # natural_problem = gpt_utils.gpt4_response(client, prompt, [], top_p=0.9)
    # print(natural_problem)

    # client = gpt_utils.set_api_key(1)
    # prompt = f"Solve the following math word problem. Let us think step by step. {natural_problem}"
    # solution = gpt_utils.gpt4_response(client, prompt, [], top_p=0.9)
    # print(solution)