def test_zero_pow():
    assert satask(Q.zero(x**y), Q.zero(x) & Q.positive(y)) is True
    assert satask(Q.zero(x**y), Q.nonzero(x) & Q.zero(y)) is False

    assert satask(Q.zero(x), Q.zero(x**y)) is True

    assert satask(Q.zero(x**y), Q.zero(x)) is None

def test_prime():
    assert satask(Q.prime(5)) is True
    assert satask(Q.prime(6)) is False
    assert satask(Q.prime(-5)) is False

    assert satask(Q.prime(x*y), Q.integer(x) & Q.integer(y)) is None
    assert satask(Q.prime(x*y), Q.prime(x) & Q.prime(y)) is False

def test_real():
    assert satask(Q.real(x*y), Q.real(x) & Q.real(y)) is True
    assert satask(Q.real(x + y), Q.real(x) & Q.real(y)) is True
    assert satask(Q.real(x*y*z), Q.real(x) & Q.real(y) & Q.real(z)) is True
    assert satask(Q.real(x*y*z), Q.real(x) & Q.real(y)) is None
    assert satask(Q.real(x*y*z), Q.real(x) & Q.real(y) & Q.imaginary(z)) is False
    assert satask(Q.real(x + y + z), Q.real(x) & Q.real(y) & Q.real(z)) is True
    assert satask(Q.real(x + y + z), Q.real(x) & Q.real(y)) is None

def test_imaginary():
    assert satask(Q.imaginary(2*I)) is True
    assert satask(Q.imaginary(x*y), Q.imaginary(x)) is None
    assert satask(Q.imaginary(x*y), Q.imaginary(x) & Q.real(y)) is True
    assert satask(Q.imaginary(x), Q.real(x)) is False
    assert satask(Q.imaginary(1)) is False
    assert satask(Q.imaginary(x*y), Q.real(x) & Q.real(y)) is False
    assert satask(Q.imaginary(x + y), Q.real(x) & Q.real(y)) is False

def test_zero():
    """
    Everything in this test doesn't work with the ask handlers, and most
    things would be very difficult or impossible to make work under that
    model.

    """
    assert satask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) is True
    assert satask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) is True

    assert satask(Implies(Q.zero(x), Q.zero(x*y))) is True

    # This one in particular requires computing the fixed-point of the
    # relevant facts, because going from Q.nonzero(x*y) -> ~Q.zero(x*y) and
    # Q.zero(x*y) -> Equivalent(Q.zero(x*y), Q.zero(x) | Q.zero(y)) takes two
    # steps.
    assert satask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)) is False

    assert satask(Q.zero(x), Q.zero(x**2)) is True

def test_abs():
    assert satask(Q.nonnegative(abs(x))) is True
    assert satask(Q.positive(abs(x)), ~Q.zero(x)) is True
    assert satask(Q.zero(x), ~Q.zero(abs(x))) is False
    assert satask(Q.zero(x), Q.zero(abs(x))) is True
    assert satask(Q.nonzero(x), ~Q.zero(abs(x))) is None # x could be complex
    assert satask(Q.zero(abs(x)), Q.zero(x)) is True

def test_pos_neg():
    assert satask(~Q.positive(x), Q.negative(x)) is True
    assert satask(~Q.negative(x), Q.positive(x)) is True
    assert satask(Q.positive(x + y), Q.positive(x) & Q.positive(y)) is True
    assert satask(Q.negative(x + y), Q.negative(x) & Q.negative(y)) is True
    assert satask(Q.positive(x + y), Q.negative(x) & Q.negative(y)) is False
    assert satask(Q.negative(x + y), Q.positive(x) & Q.positive(y)) is False

def test_zero_positive():
    assert satask(Q.zero(x + y), Q.positive(x) & Q.positive(y)) is False
    assert satask(Q.positive(x) & Q.positive(y), Q.zero(x + y)) is False
    assert satask(Q.nonzero(x + y), Q.positive(x) & Q.positive(y)) is True
    assert satask(Q.positive(x) & Q.positive(y), Q.nonzero(x + y)) is None

    # This one requires several levels of forward chaining
    assert satask(Q.zero(x*(x + y)), Q.positive(x) & Q.positive(y)) is False

    assert satask(Q.positive(pi*x*y + 1), Q.positive(x) & Q.positive(y)) is True
    assert satask(Q.positive(pi*x*y - 5), Q.positive(x) & Q.positive(y)) is None

def test_old_assump():
    assert satask(Q.positive(1)) is True
    assert satask(Q.positive(-1)) is False
    assert satask(Q.positive(0)) is False
    assert satask(Q.positive(I)) is False
    assert satask(Q.positive(pi)) is True

    assert satask(Q.negative(1)) is False
    assert satask(Q.negative(-1)) is True
    assert satask(Q.negative(0)) is False
    assert satask(Q.negative(I)) is False
    assert satask(Q.negative(pi)) is False

    assert satask(Q.zero(1)) is False
    assert satask(Q.zero(-1)) is False
    assert satask(Q.zero(0)) is True
    assert satask(Q.zero(I)) is False
    assert satask(Q.zero(pi)) is False

    assert satask(Q.nonzero(1)) is True
    assert satask(Q.nonzero(-1)) is True
    assert satask(Q.nonzero(0)) is False
    assert satask(Q.nonzero(I)) is False
    assert satask(Q.nonzero(pi)) is True

    assert satask(Q.nonpositive(1)) is False
    assert satask(Q.nonpositive(-1)) is True
    assert satask(Q.nonpositive(0)) is True
    assert satask(Q.nonpositive(I)) is False
    assert satask(Q.nonpositive(pi)) is False

    assert satask(Q.nonnegative(1)) is True
    assert satask(Q.nonnegative(-1)) is False
    assert satask(Q.nonnegative(0)) is True
    assert satask(Q.nonnegative(I)) is False
    assert satask(Q.nonnegative(pi)) is True

def test_invertible():
    A = MatrixSymbol('A', 5, 5)
    B = MatrixSymbol('B', 5, 5)
    assert satask(Q.invertible(A*B), Q.invertible(A) & Q.invertible(B)) is True
    assert satask(Q.invertible(A), Q.invertible(A*B))
    assert satask(Q.invertible(A) & Q.invertible(B), Q.invertible(A*B))

def test_integer():
    assert satask(Q.integer(1)) is True
    assert satask(Q.integer(Rational(1, 2))) is False

    assert satask(Q.integer(x + y), Q.integer(x) & Q.integer(y)) is True
    assert satask(Q.integer(x + y), Q.integer(x)) is None

    assert satask(Q.integer(x + y), Q.integer(x) & ~Q.integer(y)) is False
    assert satask(Q.integer(x + y + z), Q.integer(x) & Q.integer(y) &
        ~Q.integer(z)) is False
    assert satask(Q.integer(x + y + z), Q.integer(x) & ~Q.integer(y) &
        ~Q.integer(z)) is None
    assert satask(Q.integer(x + y + z), Q.integer(x) & ~Q.integer(y)) is None
    assert satask(Q.integer(x + y), Q.integer(x) & Q.irrational(y)) is False

    assert satask(Q.integer(x*y), Q.integer(x) & Q.integer(y)) is True
    assert satask(Q.integer(x*y), Q.integer(x)) is None

    assert satask(Q.integer(x*y), Q.integer(x) & ~Q.integer(y)) is None
    assert satask(Q.integer(x*y), Q.integer(x) & ~Q.rational(y)) is False
    assert satask(Q.integer(x*y*z), Q.integer(x) & Q.integer(y) &
        ~Q.rational(z)) is False
    assert satask(Q.integer(x*y*z), Q.integer(x) & ~Q.rational(y) &
        ~Q.rational(z)) is None
    assert satask(Q.integer(x*y*z), Q.integer(x) & ~Q.rational(y)) is None
    assert satask(Q.integer(x*y), Q.integer(x) & Q.irrational(y)) is False

def test_odd():
    assert satask(Q.odd(2)) is False
    assert satask(Q.odd(3)) is True

    assert satask(Q.odd(x*y), Q.even(x) & Q.odd(y)) is False
    assert satask(Q.odd(x*y), Q.even(x) & Q.integer(y)) is False
    assert satask(Q.odd(x*y), Q.even(x) & Q.even(y)) is False
    assert satask(Q.odd(x*y), Q.odd(x) & Q.odd(y)) is True
    assert satask(Q.odd(x*y), Q.even(x)) is None
    assert satask(Q.odd(x*y), Q.odd(x) & Q.integer(y)) is None
    assert satask(Q.odd(x*y), Q.odd(x) & Q.odd(y)) is True

    assert satask(Q.odd(abs(x)), Q.even(x)) is False
    assert satask(Q.odd(abs(x)), Q.odd(x)) is True
    assert satask(Q.odd(x), Q.odd(abs(x))) is None # x could be complex

def test_rational_irrational():
    assert satask(Q.irrational(2)) is False
    assert satask(Q.rational(2)) is True
    assert satask(Q.irrational(pi)) is True
    assert satask(Q.rational(pi)) is False
    assert satask(Q.irrational(I)) is False
    assert satask(Q.rational(I)) is False

    assert satask(Q.irrational(x*y*z), Q.irrational(x) & Q.irrational(y) &
        Q.rational(z)) is None
    assert satask(Q.irrational(x*y*z), Q.irrational(x) & Q.rational(y) &
        Q.rational(z)) is True
    assert satask(Q.irrational(pi*x*y), Q.rational(x) & Q.rational(y)) is True

    assert satask(Q.irrational(x + y + z), Q.irrational(x) & Q.irrational(y) &
        Q.rational(z)) is None
    assert satask(Q.irrational(x + y + z), Q.irrational(x) & Q.rational(y) &
        Q.rational(z)) is True
    assert satask(Q.irrational(pi + x + y), Q.rational(x) & Q.rational(y)) is True

    assert satask(Q.irrational(x*y*z), Q.rational(x) & Q.rational(y) &
        Q.rational(z)) is False
    assert satask(Q.rational(x*y*z), Q.rational(x) & Q.rational(y) &
        Q.rational(z)) is True

    assert satask(Q.irrational(x + y + z), Q.rational(x) & Q.rational(y) &
        Q.rational(z)) is False
    assert satask(Q.rational(x + y + z), Q.rational(x) & Q.rational(y) &
        Q.rational(z)) is True

def test_satask():
    # No relevant facts
    assert satask(Q.real(x), Q.real(x)) is True
    assert satask(Q.real(x), ~Q.real(x)) is False
    assert satask(Q.real(x)) is None

    assert satask(Q.real(x), Q.positive(x)) is True
    assert satask(Q.positive(x), Q.real(x)) is None
    assert satask(Q.real(x), ~Q.positive(x)) is None
    assert satask(Q.positive(x), ~Q.real(x)) is False

    raises(ValueError, lambda: satask(Q.real(x), Q.real(x) & ~Q.real(x)))

    with assuming(Q.positive(x)):
        assert satask(Q.real(x)) is True
        assert satask(~Q.positive(x)) is False
        raises(ValueError, lambda: satask(Q.real(x), ~Q.positive(x)))

    assert satask(Q.zero(x), Q.nonzero(x)) is False
    assert satask(Q.positive(x), Q.zero(x)) is False
    assert satask(Q.real(x), Q.zero(x)) is True
    assert satask(Q.zero(x), Q.zero(x*y)) is None
    assert satask(Q.zero(x*y), Q.zero(x))

def ask(proposition, assumptions=True, context=global_assumptions):
    """
    Method for inferring properties about objects.

    **Syntax**

        * ask(proposition)

        * ask(proposition, assumptions)

            where ``proposition`` is any boolean expression

    Examples
    ========

    >>> from sympy import ask, Q, pi
    >>> from sympy.abc import x, y
    >>> ask(Q.rational(pi))
    False
    >>> ask(Q.even(x*y), Q.even(x) & Q.integer(y))
    True
    >>> ask(Q.prime(x*y), Q.integer(x) &  Q.integer(y))
    False

    **Remarks**
        Relations in assumptions are not implemented (yet), so the following
        will not give a meaningful result.

        >>> ask(Q.positive(x), Q.is_true(x > 0)) # doctest: +SKIP

        It is however a work in progress.

    """
    from sympy.assumptions.satask import satask

    if not isinstance(proposition, (BooleanFunction, AppliedPredicate, bool, BooleanAtom)):
        raise TypeError("proposition must be a valid logical expression")

    if not isinstance(assumptions, (BooleanFunction, AppliedPredicate, bool, BooleanAtom)):
        raise TypeError("assumptions must be a valid logical expression")

    if isinstance(proposition, AppliedPredicate):
        key, expr = proposition.func, sympify(proposition.arg)
    else:
        key, expr = Q.is_true, sympify(proposition)

    assumptions = And(assumptions, And(*context))
    assumptions = to_cnf(assumptions)

    local_facts = _extract_facts(assumptions, expr)

    known_facts_cnf = get_known_facts_cnf()
    known_facts_dict = get_known_facts_dict()

    if local_facts and satisfiable(And(local_facts, known_facts_cnf)) is False:
        raise ValueError("inconsistent assumptions %s" % assumptions)

    # direct resolution method, no logic
    res = key(expr)._eval_ask(assumptions)
    if res is not None:
        return bool(res)

    if local_facts is None:
        return satask(proposition, assumptions=assumptions, context=context)


    # See if there's a straight-forward conclusion we can make for the inference
    if local_facts.is_Atom:
        if key in known_facts_dict[local_facts]:
            return True
        if Not(key) in known_facts_dict[local_facts]:
            return False
    elif (local_facts.func is And and
            all(k in known_facts_dict for k in local_facts.args)):
        for assum in local_facts.args:
            if assum.is_Atom:
                if key in known_facts_dict[assum]:
                    return True
                if Not(key) in known_facts_dict[assum]:
                    return False
            elif assum.func is Not and assum.args[0].is_Atom:
                if key in known_facts_dict[assum]:
                    return False
                if Not(key) in known_facts_dict[assum]:
                    return True
    elif (isinstance(key, Predicate) and
            local_facts.func is Not and local_facts.args[0].is_Atom):
        if local_facts.args[0] in known_facts_dict[key]:
            return False

    # Failing all else, we do a full logical inference
    res = ask_full_inference(key, local_facts, known_facts_cnf)
    if res is None:
        return satask(proposition, assumptions=assumptions, context=context)
    return res

def test_pow_pos_neg():
    assert satask(Q.nonnegative(x**2), Q.positive(x)) is True
    assert satask(Q.nonpositive(x**2), Q.positive(x)) is False
    assert satask(Q.positive(x**2), Q.positive(x)) is True
    assert satask(Q.negative(x**2), Q.positive(x)) is False
    assert satask(Q.real(x**2), Q.positive(x)) is True

    assert satask(Q.nonnegative(x**2), Q.negative(x)) is True
    assert satask(Q.nonpositive(x**2), Q.negative(x)) is False
    assert satask(Q.positive(x**2), Q.negative(x)) is True
    assert satask(Q.negative(x**2), Q.negative(x)) is False
    assert satask(Q.real(x**2), Q.negative(x)) is True

    assert satask(Q.nonnegative(x**2), Q.nonnegative(x)) is True
    assert satask(Q.nonpositive(x**2), Q.nonnegative(x)) is None
    assert satask(Q.positive(x**2), Q.nonnegative(x)) is None
    assert satask(Q.negative(x**2), Q.nonnegative(x)) is False
    assert satask(Q.real(x**2), Q.nonnegative(x)) is True

    assert satask(Q.nonnegative(x**2), Q.nonpositive(x)) is True
    assert satask(Q.nonpositive(x**2), Q.nonpositive(x)) is None
    assert satask(Q.positive(x**2), Q.nonpositive(x)) is None
    assert satask(Q.negative(x**2), Q.nonpositive(x)) is False
    assert satask(Q.real(x**2), Q.nonpositive(x)) is True

    assert satask(Q.nonnegative(x**3), Q.positive(x)) is True
    assert satask(Q.nonpositive(x**3), Q.positive(x)) is False
    assert satask(Q.positive(x**3), Q.positive(x)) is True
    assert satask(Q.negative(x**3), Q.positive(x)) is False
    assert satask(Q.real(x**3), Q.positive(x)) is True

    assert satask(Q.nonnegative(x**3), Q.negative(x)) is False
    assert satask(Q.nonpositive(x**3), Q.negative(x)) is True
    assert satask(Q.positive(x**3), Q.negative(x)) is False
    assert satask(Q.negative(x**3), Q.negative(x)) is True
    assert satask(Q.real(x**3), Q.negative(x)) is True

    assert satask(Q.nonnegative(x**3), Q.nonnegative(x)) is True
    assert satask(Q.nonpositive(x**3), Q.nonnegative(x)) is None
    assert satask(Q.positive(x**3), Q.nonnegative(x)) is None
    assert satask(Q.negative(x**3), Q.nonnegative(x)) is False
    assert satask(Q.real(x**3), Q.nonnegative(x)) is True

    assert satask(Q.nonnegative(x**3), Q.nonpositive(x)) is None
    assert satask(Q.nonpositive(x**3), Q.nonpositive(x)) is True
    assert satask(Q.positive(x**3), Q.nonpositive(x)) is False
    assert satask(Q.negative(x**3), Q.nonpositive(x)) is None
    assert satask(Q.real(x**3), Q.nonpositive(x)) is True

    # If x is zero, x**negative is not real.
    assert satask(Q.nonnegative(x**-2), Q.nonpositive(x)) is None
    assert satask(Q.nonpositive(x**-2), Q.nonpositive(x)) is None
    assert satask(Q.positive(x**-2), Q.nonpositive(x)) is None
    assert satask(Q.negative(x**-2), Q.nonpositive(x)) is None
    assert satask(Q.real(x**-2), Q.nonpositive(x)) is None