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

statement = """
(declare-fun brad_pumpkin () Real)
(declare-fun jessica_pumpkin () Real)
(declare-fun betty_pumpkin () Real)
(declare-fun difference () Real)
(assert (= brad_pumpkin 54))
(assert (= jessica_pumpkin (/ brad_pumpkin 2)))
(assert (= betty_pumpkin (* jessica_pumpkin 4)))
(assert (= difference (- (max brad_pumpkin (max jessica_pumpkin betty_pumpkin)) (min brad_pumpkin (min jessica_pumpkin betty_pumpkin)))))
(check-sat)
(get-value (difference))
"""

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