Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
import pytest
from logic import *
def test_expr():
assert repr(expr('P <=> Q(1)')) == '(P <=> Q(1))'
assert repr(expr('P & Q | ~R(x, F(x))')) == '((P & Q) | ~R(x, F(x)))'
def test_PropKB():
kb = PropKB()
assert count(kb.ask(expr) for expr in [A, B, C, P, Q]) is 0
kb.tell(A & B)
assert kb.ask(A) == kb.ask(B) == {}
kb.tell(B >> C)
assert kb.ask(C) == {}
kb.retract(B)
assert kb.ask(B) is False
assert kb.ask(C) is False
def test_pl_true():
assert pl_true(P, {}) is None
assert pl_true(P, {P: False}) is False
assert pl_true(P | Q, {P: True}) is True
assert pl_true((A|B)&(C|D), {A: False, B: True, D: True}) is True
assert pl_true((A&B)&(C|D), {A: False, B: True, D: True}) is False
assert pl_true((A&B)|(A&C), {A: False, B: True, C: True}) is False
assert pl_true((A|B)&(C|D), {A: True, D: False}) is None
assert pl_true(P | P, {}) is None
def test_tt_true():
assert tt_true(P | ~P)
assert tt_true('~~P <=> P')
assert not tt_true('(P | ~Q)&(~P | Q)')
assert not tt_true(P & ~P)
assert not tt_true(P & Q)
assert tt_true('(P | ~Q)|(~P | Q)')
assert tt_true('(A & B) ==> (A | B)')
assert tt_true('((A & B) & C) <=> (A & (B & C))')
assert tt_true('((A | B) | C) <=> (A | (B | C))')
assert tt_true('(A >> B) <=> (~B >> ~A)')
assert tt_true('(A >> B) <=> (~A | B)')
assert tt_true('(A <=> B) <=> ((A >> B) & (B >> A))')
assert tt_true('~(A & B) <=> (~A | ~B)')
assert tt_true('~(A | B) <=> (~A & ~B)')
assert tt_true('(A & (B | C)) <=> ((A & B) | (A & C))')
assert tt_true('(A | (B & C)) <=> ((A | B) & (A | C))')
def test_dpll():
assert dpll_satisfiable(A & ~B & C & (A | ~D) & (~E | ~D) & (C | ~D) & (~A | ~F) & (E | ~F) & (~D | ~F) & (B | ~C | D) & (A | ~E | F) & (~A | E | D)) == {B: False, C: True, A: True, F: False, D: True, E: False} #noqa
def test_unify():
assert unify(x, x, {}) == {}
assert unify(x, 3, {}) == {x: 3}
def test_to_cnf():
#assert to_cnf(Fig[7, 13] & ~expr('~P12')) BUG - FAILING THIS TEST DUE TO AN ERROR
assert repr(to_cnf((P&Q) | (~P & ~Q))) == '((~P | P) & (~Q | P) & (~P | Q) & (~Q | Q))'
pass
def test_pl_fc_entails():
assert pl_fc_entails(Fig[7,15], expr('Q'))
assert not pl_fc_entails(Fig[7,15], expr('SomethingSilly'))