from __future__ import division  # This makes Python interpret / as float division.
from classes import *
from heuristic import *
from addition_module import *
from multiplication_module import *
from function_module import *
from random import randint
from math import floor, ceil
import timeit
start = timeit.default_timer()

            
# Runs the heuristic procedure on an initialized Heuristic_data object.
# If split_cases is true, will look at all unsigned variables and split on them being > or < 0.    
def run_heuristic_on_heuristic_data(H, split_cases):
    while H.changed:
        try:
            H.changed = False
            learn_add_comparisons(H)
            learn_mul_comparisons(H)
            learn_func_comparisons(H)
        except Contradiction:
            print "Contradiction found!"
            return True
        except KeyboardInterrupt:
            print "Stopped."
            quit()
            
    if split_cases:
        if H.verbose:
            print 'We\'ve run out of new information. Let\'s try splitting cases.'
        unsigned_vars = [t for t in range(H.num_terms) if H.weak_sign(t) == 0]
        if unsigned_vars:
            if H.verbose:
                print 'We don\'t know sign information for:'
                for t in unsigned_vars:
                    print ' ', IVar(t), '=', H.terms[t]
                
        else:
            if H.verbose:
                print 'Signs of all variables are known; nothing to split on.'
                
        for v in unsigned_vars:
            if H.verbose:
                print 'Assuming', IVar(v), '>= 0. That is,', H.terms[v], '>= 0.'
            Hposv = H.duplicate()
            contr = False
            try:
                Hposv.learn_zero_comparison(v, GE, HYP)
            except Contradiction:
                contr = True
            if contr or run_heuristic_on_heuristic_data(Hposv, False):  # v>=0 is a contradiction. learn v<0
                if H.verbose:
                    print 'From the case split, we learned', H.terms[v], '< 0'
                H.learn_zero_comparison(v, LT, HYP)
                return run_heuristic_on_heuristic_data(H, True)
            
            # otherwise, no contradiction from v>=0. try v<=0
            if H.verbose:
                print 'Assuming', H.terms[v], '<= 0'
            Hnegv = H.duplicate()
            contr = False
            try:
                Hnegv.learn_zero_comparison(v, LE, HYP)
            except Contradiction:
                contr = True
            if contr or run_heuristic_on_heuristic_data(Hnegv, False):  # v<=0 is a contradiction. learn v>0
                if H.verbose:
                    print 'From the case split, we learned', H.terms[v], '> 0'
                H.learn_zero_comparison(v, GT, HYP)
                return run_heuristic_on_heuristic_data(H, True)
            
            # otherwise, v could be pos or neg. try splitting on the next case.
    
    return False

# Takes a list of (uncanonized) Zero_comparisons and runs the heuristic.
# If split_cases is true, it will try assuming variables of unknown sign are pos or neg
# if it doesn't find a contradiction before.
# Will not chain case splits.
def run_heuristic_on_hypotheses(hyps, func_data=[], split_cases=True):
    hypotheses = [canonize_zero_comparison(h) for h in hyps]
    # print "Canonized hypotheses:"
    # for h in hypotheses:
    #     print h
    # print

    try:
        H = Heuristic_data(hypotheses, func_data, verbose=False)
    except Contradiction:
        print "Contradiction found!"
        return True
    H.changed = True
    
    if run_heuristic_on_heuristic_data(H, split_cases):
        return True
        
    print "Nothing more learned. No contradiction has been found."
    return False

###############################################################################
#
# HARD-CODED TESTS
#
###############################################################################
         
def test_heuristic():

    print
    print("From these hypotheses:")
    print
    print("  0 < x < y")
    print("  0 < u < v")
    print("  0 < w + z < r - 1") 
    print
    print("It follows that:")
    print
    print("  u + (1 + x)^2 (2 w + 2 z + 3) < 2 v + (1 + y)^2 (2 r + 1)")
    print
    print("This test proves this by showing that the hypotheses together")
    print("with the negation of the conclusion are inconsistent")
    print

    r = Var("r")
    u = Var("u")
    v = Var("v")
    w = Var("w")
    x = Var("x")
    y = Var("y")
    z = Var("z")

    # hypotheses
    gt_zero_hyps = [
        x,
        Add_term([(1, y), (-1, x)]),
        u,
        Add_term([(1, v), (-1, u)]),
        Add_term([(1, w), (1, z)]),
        Add_term([(1, r), (-1, one), (-1, w), (-1, z)])]
    ge_zero_hyps = [
        Add_term([(1, u),
                  (1, Mul_term([(Add_term([(1, one), (1, x)]), 2),
                                (Add_term([(2, w), (2, z), (3, one)]), 1)])),
                  (-2, v),
                  (-1, Mul_term([(Add_term([(1, one), (1, y)]), 2),
                                (Add_term([(2, r), (1, one)]), 1)]))])]

    hypotheses = ([Zero_comparison(t, GT) for t in gt_zero_hyps] + 
                  [Zero_comparison(t, GE) for t in ge_zero_hyps])

    run_heuristic_on_hypotheses(hypotheses)


def test_heuristic_2():

    print
    print("From these hypotheses:")
    print
    print("  (x^2-8)/(x^2+3x-1) < 0")
    print("  0 < x < 1")
    print
    print("There should be no contradiction. Both are true at x=.5")
    print
    print

    x = Var("x")

    # hypotheses
    # x^2-8
    a = Add_term([Add_pair(1, Mul_term([Mul_pair(x, 2)])), Add_pair(-8, one)])
    
    # x^2+3x-1
    b = Add_term([Add_pair(1, Mul_term([Mul_pair(x, 2)])), Add_pair(3, x), Add_pair(-1, one)])
    
    lt_zero_hyps = [
       Mul_term([Mul_pair(a, 1), Mul_pair(b, -1)])
       ]
    gt_zero_hyps = [
        x,
        Add_term([Add_pair(1, one), Add_pair(-1, x)])
        ]


    hypotheses = ([Zero_comparison(t, LT) for t in lt_zero_hyps]
                   + [Zero_comparison(t, GT) for t in gt_zero_hyps])

    run_heuristic_on_hypotheses(hypotheses, split_cases=False)
        
def test_heuristic_3():

    print
    print("From these hypotheses:")
    print
    print("  -x^2 > -10")
    print("  x > 5")
    print
    print("There should be a contradiction.")
    print
    print

    x = Var("x")

    # hypotheses
    # -x^2>-10
    a = Add_term([Add_pair(-1, Mul_term([Mul_pair(x, 2)])), Add_pair(10, one)])
    
    # x>5
    b = Add_term([Add_pair(1, x), Add_pair(-5, one)])
    lt_zero_hyps = [
       
       ]
    gt_zero_hyps = [
        a, b
        ]


    hypotheses = ([Zero_comparison(t, LT) for t in lt_zero_hyps]
                   + [Zero_comparison(t, GT) for t in gt_zero_hyps])

    run_heuristic_on_hypotheses(hypotheses)
    
def test_heuristic_4():

    print
    print("From these hypotheses:")
    print
    print("  x < 0")
    print("  x - y < 0")
    print("  x + y >= 5")
    print
    print("There should be no contradiction. All are true at x=-1, y=10.")
    print
    print

    x = Var("x")
    y = Var("y")

    
    lt_zero_hyps = [
       x, Add_term([Add_pair(1, x), Add_pair(-1, y)])
       ]

    hypotheses = ([Zero_comparison(t, LT) for t in lt_zero_hyps]
                   + [Zero_comparison(Add_term([Add_pair(1, x), Add_pair(1, y), Add_pair(-5, one)]), GE)])

    run_heuristic_on_hypotheses(hypotheses)
    
def test_heuristic_on_functions():
    # we know x < y => exp(x) < exp(y)
    # Assume x < y, exp(x) > exp(y).
    
    x = Var("x")
    y = Var("y")
    hypotheses = [Zero_comparison(Add_term([Add_pair(1, x), Add_pair(-1, y)]), LT), Zero_comparison(Add_term([Add_pair(1, Func_term('exp', [y])), Add_pair(-1, Func_term('exp', [x]))]), LT)]
    co = Function_conclusion((lambda H, a, b:Func_term("exp", [a])), (lambda H, a, b:Func_term("exp", [b])), GT)
    fr = Function_restriction('exp', lambda H, a, b:a.gt_rel(b, H), co)
    

    co2 = Function_conclusion(lambda H, a:Func_term("exp", [a]), lambda H, a:0, GT)
    fr2 = Function_restriction('exp2', lambda H, a:True, co2)
    # fr2 = Function_restriction('exp',free_vars2,[h2],co2)
    
    run_heuristic_on_hypotheses(hypotheses, [fr2])

def test_heuristic_on_functions2():
    # we know x < y => exp(x) < exp(y)
    # Assume x < y, exp(x) > exp(y).
    
    x = Var("x")
    y = Var("y")
    hypotheses = [Zero_comparison(Add_term([Add_pair(1, x), Add_pair(-1, y)]), LT), Zero_comparison(Add_term([Add_pair(1, Func_term('exp', [y])), Add_pair(-1, Func_term('exp', [x]))]), LE),
                  Zero_comparison(Add_term([Add_pair(1, Func_term('exp', [y])), Add_pair(-1, Func_term('exp', [x]))]), GE)]
    co = Function_conclusion((lambda H, a, b:Func_term("exp", [a])), (lambda H, a, b:Func_term("exp", [b])), GT)
    fr = Function_restriction('exp', lambda H, a, b:a.neq_rel(b, H), co)
    

    co2 = Function_conclusion(lambda H, a:Func_term("exp", [a]), lambda H, a:0, GT)
    fr2 = Function_restriction('exp2', lambda H, a:True, co2)
    # fr2 = Function_restriction('exp',free_vars2,[h2],co2)
    
    run_heuristic_on_hypotheses(hypotheses, [fr])

###################################################
#
#  INPUT CODE
#
####################################################

digit = '1234567890'
alpha = 'abcdefghijklmnopqrstuvwxyz_'
alphanum = alpha + digit
comp = '><='