<commit_before>"""For more tests on satisfiability, see test_dimacs"""

from sympy import symbols
from sympy.logic.boolalg import Equivalent
from sympy.logic.inference import pl_true, satisfiable, find_pure_symbol, \
        find_unit_clause
from sympy.logic.kb import PropKB
from sympy.logic.algorithms.dpll import dpll, dpll_satisfiable

def test_find_pure_symbol():
    A, B, C = symbols('ABC')
    assert find_pure_symbol([A, B, C], [ A | ~B, ~B | ~C, C | A]) == (A, True)
    assert find_pure_symbol([A, B, C], [~A |  B,  B | ~C, C | A]) == (B, True)
    assert find_pure_symbol([A, B, C], [~A | ~B, ~B | ~C, C | A]) == (B, False)

def test_unit_clause():
    A, B, C = symbols('ABC')
    assert find_unit_clause([A | B | C, B | ~C, A | ~B], {A:True}) == (B, False)

def test_dpll():
    """This is also tested in test_dimacs"""
    A, B, C = symbols('ABC')
    assert dpll([A | B], [A, B], {A: True, B: True}) == {A: True, B: True}

def test_dpll_satisfiable():
    A, B, C = symbols('ABC')
    assert dpll_satisfiable( A & ~A )     == False
    assert dpll_satisfiable( A & ~B )     == {A: True, B: False}
    assert dpll_satisfiable( A & B & C  ) == {A: True, B: True, C: True}
    assert dpll_satisfiable( A | B )      in ({A: True}, {B: True})
    assert dpll_satisfiable( (A | B) & (A >> B)) == {B: True}
    assert dpll_satisfiable(Equivalent(A, B) & A) == {A: True, B: True}
    assert dpll_satisfiable(Equivalent(A, B) & ~A) == {A: False, B: 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_pl_true():
    A, B, C = symbols('ABC')
    assert pl_true( A & B, {A : True, B : True}) == True
    assert pl_true( A | B, {A : True}) == True<commit_msg>Extend test coverage in sympy.logic.tests.test_inference<commit_after>"""For more tests on satisfiability, see test_dimacs"""

from sympy import symbols
from sympy.logic.boolalg import Equivalent
from sympy.logic.inference import pl_true, satisfiable, find_pure_symbol, \
        find_unit_clause
from sympy.logic.kb import PropKB
from sympy.logic.algorithms.dpll import dpll, dpll_satisfiable

def test_find_pure_symbol():
    A, B, C = symbols('ABC')
    assert find_pure_symbol([A], [A]) == (A, True)
    assert find_pure_symbol([A, B, C], [ A | ~B, ~B | ~C, C | A]) == (A, True)
    assert find_pure_symbol([A, B, C], [~A |  B,  B | ~C, C | A]) == (B, True)
    assert find_pure_symbol([A, B, C], [~A | ~B, ~B | ~C, C | A]) == (B, False)
    assert find_pure_symbol([A, B, C], [~A | B, ~B | ~C, C | A]) == (None, None)

def test_unit_clause():
    A, B, C = symbols('ABC')
    assert find_unit_clause([A], {}) == (A, True)
    assert find_unit_clause([A | B], {A: True}) == (B, True)
    assert find_unit_clause([A | B], {B: True}) == (A, True)
    assert find_unit_clause([A | B | C, B | ~C, A | ~B], {A:True}) == (B, False)
    assert find_unit_clause([A | B | C, B | ~C, A | B], {A:True})  == (B, True)
    assert find_unit_clause([A | B | C, B | ~C, A ], {}) == (A, True)

def test_dpll():
    """This is also tested in test_dimacs"""
    A, B, C = symbols('ABC')
    assert dpll([A | B], [A, B], {A: True, B: True}) == {A: True, B: True}

def test_dpll_satisfiable():
    A, B, C = symbols('ABC')
    assert dpll_satisfiable( A & ~A )     == False
    assert dpll_satisfiable( A & ~B )     == {A: True, B: False}
    assert dpll_satisfiable( A & B & C  ) == {A: True, B: True, C: True}
    assert dpll_satisfiable( A | B )      in ({A: True}, {B: True})
    assert dpll_satisfiable( (A | B) & (A >> B)) == {B: True}
    assert dpll_satisfiable(Equivalent(A, B) & A) == {A: True, B: True}
    assert dpll_satisfiable(Equivalent(A, B) & ~A) == {A: False, B: 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_pl_true():
    A, B, C = symbols('ABC')
    assert pl_true( A & B, {A : True, B : True}) == True
    assert pl_true( A | B, {A : True}) == True
{'fraction_non_alphanumeric': 0.18453683442742524, 'fraction_numerical': 0.0004862630683199611, 'mean_word_length': 3.376595744680851, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '803386', 'n_tokens_mistral': 1680, 'n_tokens_neox': 1614, 'n_words': 502}