Repository: sympy/sympy

Issue:
boolalg.py:is_cnf fails when it should pass
- If i create a simple conjunction of two literals, which by definition is in conjunctive normal form, the boolalg.py:is_cnf function incorrectly returns false.
- Additionally, if I create I an expression in disjunctive normal form, and then call boolalg.py:to_cnf on it. It is correctly put in conjunctive normal form, but boolalg.py:is_cnf still returns false.

Below is sample code that demonstrates both of these issues. 

``` Python
from sympy import S
from sympy.logic import boolalg
from sympy import srepr

literal1 = S("X>2")
literal2 = S("X<4")
literal3 = S("Y>-5")

# Conjunction by itself, which should be in CNF form
conjunction_clause = boolalg.And(literal1, literal2)

# Disjunction of a conjunction and literal, should be in DNF
dnf_exp = boolalg.Or(literal3, conjunction_clause)

print(srepr(conjunction_clause))
print(srepr(dnf_exp))

# Expression already in CNF, but is_cnf fails
simple_is_cnf_test = boolalg.is_cnf(conjunction_clause)
print("simple_is_cnf_test", simple_is_cnf_test)

# Expression in DNF
# Expression correctly put in CNF
print("DNF Expression, turned to CNF: \n\t", boolalg.to_cnf(dnf_exp))
dnf_to_cnf_test = boolalg.is_cnf(boolalg.to_cnf(dnf_exp))

assert((simple_is_cnf_test or dnf_to_cnf_test),
                "2 expression in CNF, but is_cnf returns false.")
```


Discussion:

Patch:
diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py
index dd734cedaf..03b0c8283d 100644
--- a/sympy/logic/boolalg.py
+++ b/sympy/logic/boolalg.py
@@ -1691,12 +1691,14 @@ def to_nnf(expr, simplify=True):
     return expr.to_nnf(simplify)
 
 
-def to_cnf(expr, simplify=False):
+def to_cnf(expr, simplify=False, force=False):
     """
-    Convert a propositional logical sentence s to conjunctive normal form.
-    That is, of the form ((A | ~B | ...) & (B | C | ...) & ...)
-    If simplify is True, the expr is evaluated to its simplest CNF form  using
-    the Quine-McCluskey algorithm.
+    Convert a propositional logical sentence s to conjunctive normal
+    form: ((A | ~B | ...) & (B | C | ...) & ...).
+    If simplify is True, the expr is evaluated to its simplest CNF
+    form using the Quine-McCluskey algorithm; this may take a long
+    time if there are more than 8 variables and requires that the
+    ``force`` flag be set to True (default is False).
 
     Examples
     ========
@@ -1714,7 +1716,12 @@ def to_cnf(expr, simplify=False):
         return expr
 
     if simplify:
-        return simplify_logic(expr, 'cnf', True)
+        if not force and len(_find_predicates(expr)) > 8:
+            raise ValueError(filldedent('''
+            To simplify a logical expression with more
+            than 8 variables may take a long time and requires
+            the use of `force=True`.'''))
+        return simplify_logic(expr, 'cnf', True, force=force)
 
     # Don't convert unless we have to
     if is_cnf(expr):
@@ -1726,12 +1733,14 @@ def to_cnf(expr, simplify=False):
     return res
 
 
-def to_dnf(expr, simplify=False):
+def to_dnf(expr, simplify=False, force=False):
     """
-    Convert a propositional logical sentence s to disjunctive normal form.
-    That is, of the form ((A & ~B & ...) | (B & C & ...) | ...)
+    Convert a propositional logical sentence s to disjunctive normal
+    form: ((A & ~B & ...) | (B & C & ...) | ...).
     If simplify is True, the expr is evaluated to its simplest DNF form using
-    the Quine-McCluskey algorithm.
+    the Quine-McCluskey algorithm; this may take a long
+    time if there are more than 8 variables and requires that the
+    ``force`` flag be set to True (default is False).
 
     Examples
     ========
@@ -1749,7 +1758,12 @@ def to_dnf(expr, simplify=False):
         return expr
 
     if simplify:
-        return simplify_logic(expr, 'dnf', True)
+        if not force and len(_find_predicates(expr)) > 8:
+            raise ValueError(filldedent('''
+            To simplify a logical expression with more
+            than 8 variables may take a long time and requires
+            the use of `force=True`.'''))
+        return simplify_logic(expr, 'dnf', True, force=force)
 
     # Don't convert unless we have to
     if is_dnf(expr):
@@ -1910,22 +1924,14 @@ def _is_form(expr, function1, function2):
     """
     expr = sympify(expr)
 
-    def is_a_literal(lit):
-        if isinstance(lit, Not) \
-                and lit.args[0].is_Atom:
-            return True
-        elif lit.is_Atom:
-            return True
-        return False
-
     vals = function1.make_args(expr) if isinstance(expr, function1) else [expr]
     for lit in vals:
         if isinstance(lit, function2):
             vals2 = function2.make_args(lit) if isinstance(lit, function2) else [lit]
             for l in vals2:
-                if is_a_literal(l) is False:
+                if is_literal(l) is False:
                     return False
-        elif is_a_literal(lit) is False:
+        elif is_literal(lit) is False:
             return False
 
     return True
@@ -1977,9 +1983,13 @@ def is_literal(expr):
 
     """
     if isinstance(expr, Not):
-        return not isinstance(expr.args[0], BooleanFunction)
-    else:
-        return not isinstance(expr, BooleanFunction)
+        return is_literal(expr.args[0])
+    elif expr in (True, False) or expr.is_Atom:
+        return True
+    elif not isinstance(expr, BooleanFunction) and all(
+            a.is_Atom for a in expr.args):
+        return True
+    return False
 
 
 def to_int_repr(clauses, symbols):
@@ -2756,11 +2766,12 @@ def simplify_logic(expr, form=None, deep=True, force=False):
         non-boolean functions contained within the input.
 
     force : boolean (default False)
-        As the simplifications require exponential time in the number of
-        variables, there is by default a limit on expressions with 8 variables.
-        When the expression has more than 8 variables only symbolical
-        simplification (controlled by ``deep``) is made. By setting force to ``True``, this limit
-        is removed. Be aware that this can lead to very long simplification times.
+        As the simplifications require exponential time in the number
+        of variables, there is by default a limit on expressions with
+        8 variables. When the expression has more than 8 variables
+        only symbolical simplification (controlled by ``deep``) is
+        made. By setting force to ``True``, this limit is removed. Be
+        aware that this can lead to very long simplification times.
 
     Examples
     ========
@@ -2782,6 +2793,16 @@ def simplify_logic(expr, form=None, deep=True, force=False):
     if form not in (None, 'cnf', 'dnf'):
         raise ValueError("form can be cnf or dnf only")
     expr = sympify(expr)
+    # check for quick exit: right form and all args are
+    # literal and do not involve Not
+    isc = is_cnf(expr)
+    isd = is_dnf(expr)
+    form_ok = (
+        isc and form == 'cnf' or
+        isd and form == 'dnf')
+    if form_ok and all(is_literal(a)
+            for a in expr.args):
+        return expr
     if deep:
         variables = _find_predicates(expr)
         from sympy.simplify.simplify import simplify
diff --git a/sympy/parsing/c/c_parser.py b/sympy/parsing/c/c_parser.py
index 61f68533fc..83be9058ac 100644
--- a/sympy/parsing/c/c_parser.py
+++ b/sympy/parsing/c/c_parser.py
@@ -80,7 +80,7 @@ class CCodeConverter(BaseParser):
         converts them to SymPy Expressions.
         """
 
-        def __init__(self):
+        def __init__(self, name):
             """Initializes the code converter"""
             super(CCodeConverter, self).__init__()
             self._py_nodes = []
@@ -650,7 +650,7 @@ def parse_c(source):
         List of Python expression strings
 
     """
-    converter = CCodeConverter()
+    converter = CCodeConverter('output')
     if os.path.exists(source):
         src = converter.parse(source, flags = [])
     else:


Test patch:
diff --git a/sympy/logic/tests/test_boolalg.py b/sympy/logic/tests/test_boolalg.py
index 493aa17e86..277564c8ac 100644
--- a/sympy/logic/tests/test_boolalg.py
+++ b/sympy/logic/tests/test_boolalg.py
@@ -528,6 +528,24 @@ def test_to_cnf():
         And(Or(Not(B), A), Or(Not(C), A), Or(B, C, Not(A)))
     assert to_cnf(A + 1) == A + 1
 
+
+def test_issue_18904():
+    x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15 = symbols('x1:16')
+    eq = (( x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9 )  |
+        ( x1 & x2 & x3 & x4 & x5 & x6 & x7 & x10 & x9 )  |
+        ( x1 & x11 & x3 & x12 & x5 & x13 & x14 & x15 & x9 ))
+    assert is_cnf(to_cnf(eq))
+    raises(ValueError, lambda: to_cnf(eq, simplify=True))
+    for f, t in zip((And, Or), (to_cnf, to_dnf)):
+        eq = f(x1, x2, x3, x4, x5, x6, x7, x8, x9)
+        raises(ValueError, lambda: to_cnf(eq, simplify=True))
+        assert t(eq, simplify=True, force=True) == eq
+
+
+def test_issue_9949():
+    assert is_cnf(to_cnf((b > -5) | (a > 2) & (a < 4)))
+
+
 def test_to_CNF():
     assert CNF.CNF_to_cnf(CNF.to_CNF(~(B | C))) == to_cnf(~(B | C))
     assert CNF.CNF_to_cnf(CNF.to_CNF((A & B) | C)) == to_cnf((A & B) | C)
@@ -665,6 +683,8 @@ def test_is_literal():
     assert is_literal(Not(Q.zero(A))) is True
     assert is_literal(Or(A, B)) is False
     assert is_literal(And(Q.zero(A), Q.zero(B))) is False
+    assert is_literal(x < 3)
+    assert not is_literal(x + y < 3)
 
 
 def test_operators():