diff --git a/.flake8 b/.flake8 index c321e71..826d9f3 100644 --- a/.flake8 +++ b/.flake8 @@ -1,5 +1,5 @@ [flake8] -ignore = E203, E266, E501, W503 +ignore = E203, E266, E501, W503, C901 max-line-length = 80 max-complexity = 18 select = B,C,E,F,W,T4,B9 diff --git a/pylogic/propositional.py b/pylogic/propositional.py index 1aaf67c..e66b5b7 100644 --- a/pylogic/propositional.py +++ b/pylogic/propositional.py @@ -381,7 +381,8 @@ def parse(self, clause: Clause) -> Set[CnfClause]: return cnf_clauses -def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool: # noqa: C901 +# noqa: C901 +def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000, threshold=10000) -> bool: parser = CnfParser() alpha_cnf = parser.parse(to_cnf(~alpha)) @@ -435,7 +436,7 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool: # noqa: interesting_clauses.add(clause) added_knowledge = True - if not added_knowledge: + if not added_knowledge or len(interesting_clauses.clauses) >= threshold: return False it += 1 diff --git a/tests/test_propositional.py b/tests/test_propositional.py index e86c2f5..35e418a 100644 --- a/tests/test_propositional.py +++ b/tests/test_propositional.py @@ -120,3 +120,24 @@ def test_previous_bug_1(): kb.add(list(r4)) kb.add(list(r2)) assert pl_resolution(kb, alpha) is False + + +def test_debug(): + parser = CnfParser() + result = to_cnf( + Variable("B13", True) + >> (Variable("P12", True) | Variable("P03", True) | Variable("P32", True)) + ) + r4 = parser.parse(result) + + result = to_cnf( + Variable("P12", True) & Variable("P03", True) & Variable("B13", True) + ) + r2 = parser.parse(result) + + alpha = ~Variable("P32", True) + + kb = PropLogicKB() + kb.add(list(r4)) + kb.add(list(r2)) + assert pl_resolution(kb, alpha) is False