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

statement = """
(declare-fun power () Real)
(declare-fun result () Real)

; Define the expression 
(assert (= result (/ (pow 5 (/ 1 3)) (pow 5 (/ 1 5)))))

; The expression equals 5 raised to some power
(assert (= result (pow 5 power)))

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

if __name__ == "__main__":
    # statement = simplify(statement, comment=False)
    # print(1, statement)
    # statement = simplify(statement, comment=True)
    # print(2, statement)
    ok, solution = solve(statement)
    print(solution)
    statement = refresh(statement, comment=True)
    print(statement)
    ok, solution = solve(statement)
    print(solution)
