def ask_full_inference(proposition, assumptions):
    """
    Method for inferring properties about objects.

    """
    if not satisfiable(And(known_facts_cnf, assumptions, proposition)):
        return False
    if not satisfiable(And(known_facts_cnf, assumptions, Not(proposition))):
        return True
    return None

def test_satisfiable_non_symbols():
    x, y = symbols('x y')
    assumptions = Q.zero(x*y)
    facts = Implies(Q.zero(x*y), Q.zero(x) | Q.zero(y))
    query = ~Q.zero(x) & ~Q.zero(y)
    refutations = [
        {Q.zero(x): True, Q.zero(x*y): True},
        {Q.zero(y): True, Q.zero(x*y): True},
        {Q.zero(x): True, Q.zero(y): True, Q.zero(x*y): True},
        {Q.zero(x): True, Q.zero(y): False, Q.zero(x*y): True},
        {Q.zero(x): False, Q.zero(y): True, Q.zero(x*y): True}]
    assert not satisfiable(And(assumptions, facts, query), algorithm='dpll')
    assert satisfiable(And(assumptions, facts, ~query), algorithm='dpll') in refutations
    assert not satisfiable(And(assumptions, facts, query), algorithm='dpll2')
    assert satisfiable(And(assumptions, facts, ~query), algorithm='dpll2') in refutations

def test_satisfiable_all_models():
    from sympy.abc import A, B
    assert next(satisfiable(False, all_models=True)) is False
    assert list(satisfiable((A >> ~A) & A , all_models=True)) == [False]
    assert list(satisfiable(True, all_models=True)) == [{true: true}]

    models = [{A: True, B: False}, {A: False, B: True}]
    result = satisfiable(A ^ B, all_models=True)
    models.remove(next(result))
    models.remove(next(result))
    raises(StopIteration, lambda: next(result))
    assert not models

    assert list(satisfiable(Equivalent(A, B), all_models=True)) == \
    [{A: False, B: False}, {A: True, B: True}]

    models = [{A: False, B: False}, {A: False, B: True}, {A: True, B: True}]
    for model in satisfiable(A >> B, all_models=True):
        models.remove(model)
    assert not models

    # This is a santiy test to check that only the required number
    # of solutions are generated. The expr below has 2**100 - 1 models
    # which would time out the test if all are generated at once.
    from sympy import numbered_symbols
    from sympy.logic.boolalg import Or
    sym = numbered_symbols()
    X = [next(sym) for i in range(100)]
    result = satisfiable(Or(*X), all_models=True)
    for i in range(10):
        assert next(result)

def satask(proposition, assumptions=True, context=global_assumptions, use_known_facts=True, iterations=oo):
    relevant_facts = get_all_relevant_facts(
        proposition, assumptions, context, use_known_facts=use_known_facts, iterations=iterations
    )

    can_be_true = satisfiable(And(proposition, assumptions, relevant_facts, *context))
    can_be_false = satisfiable(And(~proposition, assumptions, relevant_facts, *context))

    if can_be_true and can_be_false:
        return None

    if can_be_true and not can_be_false:
        return True

    if not can_be_true and can_be_false:
        return False

    if not can_be_true and not can_be_false:
        # TODO: Run additional checks to see which combination of the
        # assumptions, global_assumptions, and relevant_facts are
        # inconsistent.
        raise ValueError("Inconsistent assumptions")

    def equals(self, other):
        """
        Returns if the given formulas have the same truth table.
        For two formulas to be equal they must have the same literals.

        Examples
        ========

        >>> from sympy.abc import A, B, C
        >>> from sympy.logic.boolalg import And, Or, Not
        >>> (A >> B).equals(~B >> ~A)
        True
        >>> Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C)))
        False
        >>> Not(And(A, Not(A))).equals(Or(B, Not(B)))
        False
        """

        from sympy.logic.inference import satisfiable
        return self.atoms() == other.atoms() and \
                not satisfiable(Not(Equivalent(self, other)))

    def equals(self, other):
        """
        Returns if the given formulas have the same truth table.
        For two formulas to be equal they must have the same literals.

        Examples
        ========

        >>> from sympy.abc import A, B, C
        >>> from sympy.logic.boolalg import And, Or, Not
        >>> (A >> B).equals(~B >> ~A)
        True
        >>> Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C)))
        False
        >>> Not(And(A, Not(A))).equals(Or(B, Not(B)))
        False
        """
        from sympy.logic.inference import satisfiable
        from sympy.core.relational import Relational

        if self.has(Relational) or other.has(Relational):
            raise NotImplementedError('handling of relationals')
        return self.atoms() == other.atoms() and \
                not satisfiable(Not(Equivalent(self, other)))

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.

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

    if not isinstance(assumptions, (BooleanFunction, AppliedPredicate, bool)):
        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))
    local_facts = _extract_facts(assumptions, expr)

    if local_facts is not None 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 res

    if assumptions is True:
        return

    if local_facts in (None, True):
        return

    # 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
    return ask_full_inference(key, local_facts, known_facts_cnf)

def ask(expr, key, assumptions=True, context=global_assumptions, disable_preprocessing=False):
    """
    Method for inferring properties about objects.

    **Syntax**

        * ask(expression, key)

        * ask(expression, key, assumptions)

            where expression is any SymPy expression

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

    **Remarks**
        Relations in assumptions are not implemented (yet), so the following
        will not give a meaningful result.
        >> ask(x, positive=True, Assume(x>0))
        It is however a work in progress and should be available before
        the official release

    """
    expr = sympify(expr)
    if type(key) is not Predicate:
        key = getattr(Q, str(key))
    assumptions = And(assumptions, And(*context))

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

    if assumptions is True:
        return

    if not expr.is_Atom:
        return

    assumptions = eliminate_assume(assumptions, expr)
    if assumptions is None or assumptions is True:
        return

    # See if there's a straight-forward conclusion we can make for the inference
    if not disable_preprocessing:
        if assumptions.is_Atom:
            if key in known_facts_dict[assumptions]:
                return True
            if Not(key) in known_facts_dict[assumptions]:
                return False
        elif assumptions.func is And:
            for assum in assumptions.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 assumptions.func is Not and assumptions.args[0].is_Atom:
            if assumptions.args[0] in known_facts_dict[key]:
                return False

    # Failing all else, we do a full logical inference
    # If it's not consistent with the assumptions, then it can't be true
    if not satisfiable(And(known_facts_cnf, assumptions, key)):
        return False

    # If the negation is unsatisfiable, it is entailed
    if not satisfiable(And(known_facts_cnf, assumptions, Not(key))):
        return True

    # Otherwise, we don't have enough information to conclude one way or the other
    return None

def test_satisfiable():
    A, B, C = symbols('A,B,C')
    assert satisfiable(A & (A >> B) & ~B) is False

 def eval(variable, expr):
     if satisfiable(expr) == False:
         return false
     return Exist(variable, expr, evaluate=False)

def test_satisfiable_1():
    """We prove expr entails alpha proving expr & ~B is unsatisfiable"""
    A, B, C = symbols('ABC')
    assert satisfiable(A & (A >> B) & ~B) == False

def test_satisfiable_bool():
    from sympy.core.singleton import S
    assert satisfiable(true) == {true: true}
    assert satisfiable(S.true) == {true: true}
    assert satisfiable(false) is False
    assert satisfiable(S.false) is False

def test_satisfiable_bool():
    assert satisfiable(True) == {}
    assert satisfiable(False) == False

def test_satisfiable():
    A, B, C = symbols("A,B,C")
    assert satisfiable(A & (A >> B) & ~B) == False

    if (i == "AND") or (i == "&&") or (i == "and") or (i == "∧"):
        tokenized_input.append("&")
        continue
        # or
    if (i == "OR") or (i == "||") or (i == "or") or (i == "∨"):
        tokenized_input.append("|")
        continue
        # not
    if (i == "NOT") or (i == "not") or (i == "!") or (i == "¬"):
        tokenized_input.append("~")
        continue

        # XOR
    if (i == "XOR") or (i == "xor") or (i == "^"):
        tokenized_input.append("^")
        continue

    tokenized_input.append(i)

print("Tokenized: " + str(tokenized_input))

string = " ".join(tokenized_input)

print("string: " + string)


sym = sympify(str(string), convert_xor=False)
sat = satisfiable(sym, all_models=True)
for x in sat:  # print all possibilities
    print(x)