def test_conjuncts():
    A, B, C = symbols('ABC')
    assert set(conjuncts(A & B & C)) == set([A, B, C])
    assert set(conjuncts((A | B) & C)) == set([A | B, C])
    assert conjuncts(A) == [A]
    assert conjuncts(True) == [True]
    assert conjuncts(False) == [False]

def test_conjuncts():
    A, B, C = map(Boolean, symbols('ABC'))
    assert conjuncts(A & B & C) == set([A, B, C])
    assert conjuncts((A | B) & C) == set([A | B, C])
    assert conjuncts(A) == set([A])
    assert conjuncts(True) == set([True])
    assert conjuncts(False) == set([False])

 def process_conds(cond):
     """
     Turn ``cond`` into a strip (a, b), and auxiliary conditions.
     """
     a = -oo
     b = oo
     aux = True
     conds = conjuncts(to_cnf(cond))
     t = Dummy('t', real=True)
     for c in conds:
         a_ = oo
         b_ = -oo
         aux_ = []
         for d in disjuncts(c):
             d_ = d.replace(re, lambda x: x.as_real_imag()[0]).subs(re(s), t)
             if not d.is_Relational or (d.rel_op != '<' and d.rel_op != '<=') \
                or d_.has(s) or not d_.has(t):
                 aux_ += [d]
                 continue
             soln = _solve_inequality(d_, t)
             if not soln.is_Relational or \
                (soln.rel_op != '<' and soln.rel_op != '<='):
                 aux_ += [d]
                 continue
             if soln.lhs == t:
                 b_ = Max(soln.rhs, b_)
             else:
                 a_ = Min(soln.lhs, a_)
         if a_ != oo and a_ != b:
             a = Max(a_, a)
         elif b_ != -oo and b_ != a:
             b = Min(b_, b)
         else:
             aux = And(aux, Or(*aux_))
     return a, b, aux

    def ask(self, query):
        """Checks if the query is true given the set of clauses.

        Examples
        ========

        >>> from sympy.logic.inference import PropKB
        >>> from sympy.abc import x, y
        >>> l = PropKB()
        >>> l.tell(x & ~y)
        >>> l.ask(x)
        True
        >>> l.ask(y)
        False
        """
        if len(self.clauses) == 0:
            return False
        from sympy.logic.algorithms.dpll import dpll

        query_conjuncts = self.clauses[:]
        query_conjuncts.extend(conjuncts(to_cnf(query)))
        s = set()
        for q in query_conjuncts:
            s = s.union(q.atoms(C.Symbol))
        return bool(dpll(query_conjuncts, list(s), {}))

def dpll_satisfiable(expr):
    """
    Check satisfiability of a propositional sentence.
    It returns a model rather than True when it succeeds

    >>> from sympy.abc import A, B
    >>> from sympy.logic.algorithms.dpll import dpll_satisfiable
    >>> dpll_satisfiable(A & ~B)
    {A: True, B: False}
    >>> dpll_satisfiable(A & ~A)
    False

    """
    clauses = conjuncts(to_cnf(expr))
    if False in clauses:
        return False
    symbols = sorted(_find_predicates(expr), key=default_sort_key)
    symbols_int_repr = set(range(1, len(symbols) + 1))
    clauses_int_repr = to_int_repr(clauses, symbols)
    result = dpll_int_repr(clauses_int_repr, symbols_int_repr, {})
    if not result:
        return result
    output = {}
    for key in result:
        output.update({symbols[key - 1]: result[key]})
    return output

def dpll_satisfiable(expr):
    """
    Check satisfiability of a propositional sentence.
    It returns a model rather than True when it succeeds

    Examples
    ========

    >>> from sympy.abc import A, B
    >>> from sympy.logic.algorithms.dpll2 import dpll_satisfiable
    >>> dpll_satisfiable(A & ~B)
    {A: True, B: False}
    >>> dpll_satisfiable(A & ~A)
    False

    """
    clauses = conjuncts(to_cnf(expr))
    if False in clauses:
        return False
    symbols = sorted(_find_predicates(expr), key=default_sort_key)
    symbols_int_repr = range(1, len(symbols) + 1)
    clauses_int_repr = to_int_repr(clauses, symbols)

    solver = SATSolver(clauses_int_repr, symbols_int_repr, set())
    result = solver._find_model()

    if not result:
        return result
    # Uncomment to confirm the solution is valid (hitting set for the clauses)
    #else:
        #for cls in clauses_int_repr:
            #assert solver.var_settings.intersection(cls)

    return dict((symbols[abs(lit) - 1], lit > 0) for lit in solver.var_settings)

 def Symbol(expr, assumptions):
     """Objects are expected to be commutative unless otherwise stated"""
     if assumptions is True: return True
     for assump in conjuncts(assumptions):
         if assump.expr == expr and assump.key == 'commutative':
             return assump.value
     return True

def get_gene_association_list(ga):
    gene_association = ga.replace('and', '&').replace('or', '|').replace('OR', '|')
    if not gene_association:
        return ""
    try:
        res = to_cnf(gene_association, False)
        gene_association = [[str(it) for it in disjuncts(cjs)] for cjs in conjuncts(res)]
        result = '''<table class="p_table" border="0" width="100%%">
						<tr class="centre"><th colspan="%d" class="centre">Gene association</th></tr>
						<tr>''' % (2 * len(gene_association) - 1)
        first = True
        for genes in gene_association:
            if first:
                first = False
            else:
                result += '<td class="centre"><i>and</i></td>'
            result += '<td><table border="0">'
            if len(genes) > 1:
                result += "<tr><td class='centre'><i>(or)</i></td></tr>"
            for gene in genes:
                result += "<tr><td class='main'><a href=\'http://www.ncbi.nlm.nih.gov/gene/?term=%s[sym]\' target=\'_blank\'>%s</a></td></tr>" % (
                    gene, gene)
            result += '</table></td>'
        result += '</tr></table>'
        return result
    except:
        return ""

 def Symbol(expr, assumptions):
     """Objects are expected to be commutative unless otherwise stated"""
     assumps = conjuncts(assumptions)
     if Q.commutative(expr) in assumps:
         return True
     elif ~Q.commutative(expr) in assumps:
         return False
     return True

 def MatrixSymbol(expr, assumptions):
     if not expr.is_square:
         return False
     # TODO: implement sathandlers system for the matrices.
     # Now it duplicates the general fact: Implies(Q.diagonal, Q.symmetric).
     if ask(Q.diagonal(expr), assumptions):
         return True
     if Q.symmetric(expr) in conjuncts(assumptions):
         return True

 def ask(self, query):
     """TODO: examples"""
     if len(self.clauses) == 0: return False
     query_conjuncts = self.clauses[:]
     query_conjuncts.extend(conjuncts(to_cnf(query)))
     s = set()
     for q in query_conjuncts:
         s = s.union(q.atoms(Symbol))
     return bool(dpll(query_conjuncts, list(s), {}))

 def ask(self, query):
     """TODO: examples"""
     if len(self.clauses) == 0: return False
     from sympy.logic.algorithms.dpll import dpll
     query_conjuncts = self.clauses[:]
     query_conjuncts.extend(conjuncts(to_cnf(query)))
     s = set()
     for q in query_conjuncts:
         s = s.union(q.atoms(C.Symbol))
     return bool(dpll(query_conjuncts, list(s), {}))

def _mellin_transform(f, x, s_, integrator=_default_integrator, simplify=True):
    """ Backend function to compute mellin transforms. """
    from sympy import re, Max, Min
    # We use a fresh dummy, because assumptions on s might drop conditions on
    # convergence of the integral.
    s = _dummy('s', 'mellin-transform', f)
    F = integrator(x**(s-1) * f, x)

    if not F.has(Integral):
        return _simplify(F.subs(s, s_), simplify), (-oo, oo), True

    if not F.is_Piecewise:
        raise IntegralTransformError('Mellin', f, 'could not compute integral')

    F, cond = F.args[0]
    if F.has(Integral):
        raise IntegralTransformError('Mellin', f, 'integral in unexpected form')

    a = -oo
    b = oo
    aux = True
    conds = conjuncts(to_cnf(cond))
    t = Dummy('t', real=True)
    for c in conds:
        a_ = oo
        b_ = -oo
        aux_ = []
        for d in disjuncts(c):
            d_ = d.replace(re, lambda x: x.as_real_imag()[0]).subs(re(s), t)
            if not d.is_Relational or (d.rel_op != '<' and d.rel_op != '<=') \
               or d_.has(s) or not d_.has(t):
                aux_ += [d]
                continue
            soln = _solve_inequality(d_, t)
            if not soln.is_Relational or \
               (soln.rel_op != '<' and soln.rel_op != '<='):
                aux_ += [d]
                continue
            if soln.lhs == t:
                b_ = Max(soln.rhs, b_)
            else:
                a_ = Min(soln.lhs, a_)
        if a_ != oo and a_ != b:
            a = Max(a_, a)
        elif b_ != -oo and b_ != a:
            b = Min(b_, b)
        else:
            aux = And(aux, Or(*aux_))

    if aux is False:
        raise IntegralTransformError('Mellin', f, 'no convergence found')

    return _simplify(F.subs(s, s_), simplify), (a, b), aux

def _laplace_transform(f, t, s, simplify=True):
    """ The backend function for laplace transforms. """
    from sympy import (re, Max, exp, pi, Abs, Min, periodic_argument as arg,
                       cos, Wild, symbols)
    F = integrate(exp(-s*t) * f, (t, 0, oo))

    if not F.has(Integral):
        return _simplify(F, simplify), -oo, True

    if not F.is_Piecewise:
        raise IntegralTransformError('Laplace', f, 'could not compute integral')

    F, cond = F.args[0]
    if F.has(Integral):
        raise IntegralTransformError('Laplace', f, 'integral in unexpected form')

    a = -oo
    aux = True
    conds = conjuncts(to_cnf(cond))
    u = Dummy('u', real=True)
    p, q, w1, w2, w3 = symbols('p q w1 w2 w3', cls=Wild, exclude=[s])
    for c in conds:
        a_ = oo
        aux_ = []
        for d in disjuncts(c):
            m = d.match(abs(arg((s + w3)**p*q, w1)) < w2)
            if m:
                if m[q] > 0 and m[w2]/m[p] == pi/2:
                    d = re(s + m[w3]) > 0
            m = d.match(0 < cos(abs(arg(s, q)))*abs(s) - p)
            if m:
                d = re(s) > m[p]
            d_ = d.replace(re, lambda x: x.expand().as_real_imag()[0]).subs(re(s), t)
            if not d.is_Relational or (d.rel_op != '<' and d.rel_op != '<=') \
               or d_.has(s) or not d_.has(t):
                aux_ += [d]
                continue
            soln = _solve_inequality(d_, t)
            if not soln.is_Relational or \
               (soln.rel_op != '<' and soln.rel_op != '<='):
                aux_ += [d]
                continue
            if soln.lhs == t:
                raise IntegralTransformError('Laplace', f,
                                     'convergence not in half-plane?')
            else:
                a_ = Min(soln.lhs, a_)
        if a_ != oo:
            a = Max(a_, a)
        else:
            aux = And(aux, Or(*aux_))

    return _simplify(F, simplify), a, aux

def dpll_satisfiable(expr):
    """Check satisfiability of a propositional sentence.
    It returns a model rather than True when it succeeds
    >>> from sympy import symbols
    >>> A, B = symbols('AB')
    >>> dpll_satisfiable(A & ~B)
    {A: True, B: False}
    >>> dpll_satisfiable(A & ~A)
    False
    """
    clauses = conjuncts(to_cnf(expr))
    symbols = list(expr.atoms(Symbol))
    return dpll(clauses, symbols, {})

def dpll_satisfiable(expr):
    """Check satisfiability of a propositional sentence.
    It returns a model rather than True when it succeeds
    >>> from sympy import symbols
    >>> A, B = symbols('AB')
    >>> dpll_satisfiable(A & ~B)
    {A: True, B: False}
    >>> dpll_satisfiable(A & ~A)
    False

    References: Implemented as described in http://aima.cs.berkeley.edu/
    """
    clauses = conjuncts(to_cnf(expr))
    symbols = list(expr.atoms(Symbol))
    return dpll(clauses, symbols, {})

 def process_conds(conds):
     """ Turn ``conds`` into a strip and auxiliary conditions. """
     a = -oo
     aux = True
     conds = conjuncts(to_cnf(conds))
     u = Dummy('u', real=True)
     p, q, w1, w2, w3, w4, w5 = symbols('p q w1 w2 w3 w4 w5', cls=Wild, exclude=[s])
     for c in conds:
         a_ = oo
         aux_ = []
         for d in disjuncts(c):
             m = d.match(abs(arg((s + w3)**p*q, w1)) < w2)
             if not m:
                 m = d.match(abs(arg((s + w3)**p*q, w1)) <= w2)
             if not m:
                 m = d.match(abs(arg((polar_lift(s + w3))**p*q, w1)) < w2)
             if not m:
                 m = d.match(abs(arg((polar_lift(s + w3))**p*q, w1)) <= w2)
             if m:
                 if m[q] > 0 and m[w2]/m[p] == pi/2:
                     d = re(s + m[w3]) > 0
             m = d.match(0 < cos(abs(arg(s**w1*w5, q))*w2)*abs(s**w3)**w4 - p)
             if not m:
                 m = d.match(0 < cos(abs(arg(polar_lift(s)**w1*w5, q))*w2)*abs(s**w3)**w4 - p)
             if m and all(m[wild] > 0 for wild in [w1, w2, w3, w4, w5]):
                 d = re(s) > m[p]
             d_ = d.replace(re, lambda x: x.expand().as_real_imag()[0]).subs(re(s), t)
             if not d.is_Relational or \
                d.rel_op not in ('>', '>=', '<', '<=') \
                or d_.has(s) or not d_.has(t):
                 aux_ += [d]
                 continue
             soln = _solve_inequality(d_, t)
             if not soln.is_Relational or \
                soln.rel_op not in ('>', '>=', '<', '<='):
                 aux_ += [d]
                 continue
             if soln.lts == t:
                 raise IntegralTransformError('Laplace', f,
                                      'convergence not in half-plane?')
             else:
                 a_ = Min(soln.lts, a_)
         if a_ != oo:
             a = Max(a_, a)
         else:
             aux = And(aux, Or(*aux_))
     return a, aux

    def Symbol(expr, assumptions):
        """
        Handles Symbol.

        Example:

        >>> from sympy import Symbol, Assume, Q
        >>> from sympy.assumptions.handlers.calculus import AskBoundedHandler
        >>> from sympy.abc import x
        >>> a = AskBoundedHandler()
        >>> a.Symbol(x, Assume(x, Q.positive))
        False
        >>> a.Symbol(x, Assume(x, Q.bounded))
        True

        """
        if Assume(expr, 'bounded') in conjuncts(assumptions):
            return True
        return False

    def Symbol(expr, assumptions):
        """
        Handles Symbol.

        Examples:

        >>> from sympy import Symbol, Q
        >>> from sympy.assumptions.handlers.calculus import AskBoundedHandler
        >>> from sympy.abc import x
        >>> a = AskBoundedHandler()
        >>> a.Symbol(x, Q.positive(x)) == None
        True
        >>> a.Symbol(x, Q.bounded(x))
        True

        """
        if Q.bounded(expr) in conjuncts(assumptions):
            return True
        return None

    def tell(self, sentence):
        """Add the sentence's clauses to the KB

        Examples
        ========
        >>> from sympy.logic.inference import PropKB
        >>> from sympy.abc import x, y, z
        >>> l = PropKB()
        >>> l.clauses
        []

        >>> l.tell(x | y)
        >>> l.clauses
        [Or(x, y)]

        >>> l.tell(y & z)
        >>> l.clauses
        [Or(x, y), y, z]
        """
        for c in conjuncts(to_cnf(sentence)):
            if not c in self.clauses: self.clauses.append(c)