@@ -9,9 +9,11 @@ def test_expr():
99 assert (expr_handle_infix_ops ('P & Q ==> R & ~S' )
1010 == "P & Q |'==>'| R & ~S" )
1111
12+
1213def test_extend ():
1314 assert extend ({x : 1 }, y , 2 ) == {x : 1 , y : 2 }
1415
16+
1517def test_PropKB ():
1618 kb = PropKB ()
1719 assert count (kb .ask (expr ) for expr in [A , C , D , E , Q ]) is 0
@@ -33,44 +35,44 @@ def test_KB_wumpus():
3335 # TODO: Let's just use P11, P12, ... = symbols('P11, P12, ...')
3436 P = {}
3537 B = {}
36- P [1 ,1 ] = Symbol ("P[1,1]" )
37- P [1 ,2 ] = Symbol ("P[1,2]" )
38- P [2 ,1 ] = Symbol ("P[2,1]" )
39- P [2 ,2 ] = Symbol ("P[2,2]" )
40- P [3 ,1 ] = Symbol ("P[3,1]" )
41- B [1 ,1 ] = Symbol ("B[1,1]" )
42- B [2 ,1 ] = Symbol ("B[2,1]" )
43-
44- kb_wumpus .tell (~ P [1 ,1 ])
45- kb_wumpus .tell (B [1 ,1 ] | '<=>' | ((P [1 ,2 ] | P [2 ,1 ])))
46- kb_wumpus .tell (B [2 ,1 ] | '<=>' | ((P [1 ,1 ] | P [2 ,2 ] | P [3 ,1 ])))
47- kb_wumpus .tell (~ B [1 ,1 ])
48- kb_wumpus .tell (B [2 ,1 ])
38+ P [1 , 1 ] = Symbol ("P[1,1]" )
39+ P [1 , 2 ] = Symbol ("P[1,2]" )
40+ P [2 , 1 ] = Symbol ("P[2,1]" )
41+ P [2 , 2 ] = Symbol ("P[2,2]" )
42+ P [3 , 1 ] = Symbol ("P[3,1]" )
43+ B [1 , 1 ] = Symbol ("B[1,1]" )
44+ B [2 , 1 ] = Symbol ("B[2,1]" )
45+
46+ kb_wumpus .tell (~ P [1 , 1 ])
47+ kb_wumpus .tell (B [1 , 1 ] | '<=>' | ((P [1 , 2 ] | P [2 , 1 ])))
48+ kb_wumpus .tell (B [2 , 1 ] | '<=>' | ((P [1 , 1 ] | P [2 , 2 ] | P [3 , 1 ])))
49+ kb_wumpus .tell (~ B [1 , 1 ])
50+ kb_wumpus .tell (B [2 , 1 ])
4951
5052 # Statement: There is no pit in [1,1].
51- assert kb_wumpus .ask (~ P [1 ,1 ]) == {}
53+ assert kb_wumpus .ask (~ P [1 , 1 ]) == {}
5254
5355 # Statement: There is no pit in [1,2].
54- assert kb_wumpus .ask (~ P [1 ,2 ]) == {}
56+ assert kb_wumpus .ask (~ P [1 , 2 ]) == {}
5557
5658 # Statement: There is a pit in [2,2].
57- assert kb_wumpus .ask (P [2 ,2 ]) == False
59+ assert kb_wumpus .ask (P [2 , 2 ]) == False
5860
5961 # Statement: There is a pit in [3,1].
60- assert kb_wumpus .ask (P [3 ,1 ]) == False
62+ assert kb_wumpus .ask (P [3 , 1 ]) == False
6163
6264 # Statement: Neither [1,2] nor [2,1] contains a pit.
63- assert kb_wumpus .ask (~ P [1 ,2 ] & ~ P [2 ,1 ]) == {}
65+ assert kb_wumpus .ask (~ P [1 , 2 ] & ~ P [2 , 1 ]) == {}
6466
6567 # Statement: There is a pit in either [2,2] or [3,1].
66- assert kb_wumpus .ask (P [2 ,2 ] | P [3 ,1 ]) == {}
68+ assert kb_wumpus .ask (P [2 , 2 ] | P [3 , 1 ]) == {}
6769
6870
6971def test_definite_clause ():
70- assert is_definite_clause (expr ('A & B & C & D ==> E' ))
71- assert is_definite_clause (expr ('Farmer(Mac)' ))
72+ assert is_definite_clause (expr ('A & B & C & D ==> E' ))
73+ assert is_definite_clause (expr ('Farmer(Mac)' ))
7274 assert not is_definite_clause (expr ('~Farmer(Mac)' ))
73- assert is_definite_clause (expr ('(Farmer(f) & Rabbit(r)) ==> Hates(f, r)' ))
75+ assert is_definite_clause (expr ('(Farmer(f) & Rabbit(r)) ==> Hates(f, r)' ))
7476 assert not is_definite_clause (expr ('(Farmer(f) & ~Rabbit(r)) ==> Hates(f, r)' ))
7577 assert not is_definite_clause (expr ('(Farmer(f) | Rabbit(r)) ==> Hates(f, r)' ))
7678
@@ -79,12 +81,13 @@ def test_pl_true():
7981 assert pl_true (P , {}) is None
8082 assert pl_true (P , {P : False }) is False
8183 assert pl_true (P | Q , {P : True }) is True
82- assert pl_true ((A | B ) & ( C | D ), {A : False , B : True , D : True }) is True
83- assert pl_true ((A & B ) & ( C | D ), {A : False , B : True , D : True }) is False
84- assert pl_true ((A & B ) | ( A & C ), {A : False , B : True , C : True }) is False
85- assert pl_true ((A | B ) & ( C | D ), {A : True , D : False }) is None
84+ assert pl_true ((A | B ) & ( C | D ), {A : False , B : True , D : True }) is True
85+ assert pl_true ((A & B ) & ( C | D ), {A : False , B : True , D : True }) is False
86+ assert pl_true ((A & B ) | ( A & C ), {A : False , B : True , C : True }) is False
87+ assert pl_true ((A | B ) & ( C | D ), {A : True , D : False }) is None
8688 assert pl_true (P | P , {}) is None
8789
90+
8891def test_tt_true ():
8992 assert tt_true (P | ~ P )
9093 assert tt_true ('~~P <=> P' )
@@ -103,48 +106,56 @@ def test_tt_true():
103106 assert tt_true ('(A & (B | C)) <=> ((A & B) | (A & C))' )
104107 assert tt_true ('(A | (B & C)) <=> ((A | B) & (A | C))' )
105108
109+
106110def test_dpll ():
107111 assert (dpll_satisfiable (A & ~ B & C & (A | ~ D ) & (~ E | ~ D ) & (C | ~ D ) & (~ A | ~ F ) & (E | ~ F )
108112 & (~ D | ~ F ) & (B | ~ C | D ) & (A | ~ E | F ) & (~ A | E | D ))
109113 == {B : False , C : True , A : True , F : False , D : True , E : False })
110- assert dpll_satisfiable (A & ~ B ) == {A : True , B : False }
111- assert dpll_satisfiable (P & ~ P ) == False
114+ assert dpll_satisfiable (A & ~ B ) == {A : True , B : False }
115+ assert dpll_satisfiable (P & ~ P ) == False
112116
113117
114118def test_unify ():
115119 assert unify (x , x , {}) == {}
116120 assert unify (x , 3 , {}) == {x : 3 }
117121
122+
118123def test_pl_fc_entails ():
119124 assert pl_fc_entails (horn_clauses_KB , expr ('Q' ))
120125 assert not pl_fc_entails (horn_clauses_KB , expr ('SomethingSilly' ))
121126
127+
122128def test_tt_entails ():
123129 assert tt_entails (P & Q , Q )
124130 assert not tt_entails (P | Q , Q )
125131 assert tt_entails (A & (B | C ) & E & F & ~ (P | Q ), A & E & F & ~ P & ~ Q )
126132
133+
127134def test_eliminate_implications ():
128135 assert repr (eliminate_implications ('A ==> (~B <== C)' )) == '((~B | ~C) | ~A)'
129136 assert repr (eliminate_implications (A ^ B )) == '((A & ~B) | (~A & B))'
130137 assert repr (eliminate_implications (A & B | C & ~ D )) == '((A & B) | (C & ~D))'
131138
139+
132140def test_dissociate ():
133141 assert dissociate ('&' , [A & B ]) == [A , B ]
134142 assert dissociate ('|' , [A , B , C & D , P | Q ]) == [A , B , C & D , P , Q ]
135143 assert dissociate ('&' , [A , B , C & D , P | Q ]) == [A , B , C , D , P | Q ]
136144
145+
137146def test_associate ():
138147 assert (repr (associate ('&' , [(A & B ), (B | C ), (B & C )]))
139148 == '(A & B & (B | C) & B & C)' )
140149 assert (repr (associate ('|' , [A | (B | (C | (A & B )))]))
141150 == '(A | B | C | (A & B))' )
142151
152+
143153def test_move_not_inwards ():
144154 assert repr (move_not_inwards (~ (A | B ))) == '(~A & ~B)'
145155 assert repr (move_not_inwards (~ (A & B ))) == '(~A | ~B)'
146156 assert repr (move_not_inwards (~ (~ (A | ~ B ) | ~ ~ C ))) == '((A | ~B) & ~C)'
147157
158+
148159def test_to_cnf ():
149160 assert (repr (to_cnf (wumpus_world_inference & ~ expr ('~P12' ))) ==
150161 "((~P12 | B11) & (~P21 | B11) & (P12 | P21 | ~B11) & ~B11 & P12)" )
@@ -154,36 +165,40 @@ def test_to_cnf():
154165 assert repr (to_cnf ("A & (B | (D & E))" )) == '(A & (D | B) & (E | B))'
155166 assert repr (to_cnf ("A | (B | (C | (D & E)))" )) == '((D | A | B | C) & (E | A | B | C))'
156167
168+
157169def test_standardize_variables ():
158170 e = expr ('F(a, b, c) & G(c, A, 23)' )
159171 assert len (variables (standardize_variables (e ))) == 3
160172 #assert variables(e).intersection(variables(standardize_variables(e))) == {}
161173 assert is_variable (standardize_variables (expr ('x' )))
162174
175+
163176def test_fol_bc_ask ():
164177 def test_ask (query , kb = None ):
165178 q = expr (query )
166179 test_variables = variables (q )
167180 answers = fol_bc_ask (kb or test_kb , q )
168181 return sorted (
169182 [dict ((x , v ) for x , v in list (a .items ()) if x in test_variables )
170- for a in answers ], key = repr )
183+ for a in answers ], key = repr )
171184 assert repr (test_ask ('Farmer(x)' )) == '[{x: Mac}]'
172185 assert repr (test_ask ('Human(x)' )) == '[{x: Mac}, {x: MrsMac}]'
173186 assert repr (test_ask ('Rabbit(x)' )) == '[{x: MrsRabbit}, {x: Pete}]'
174187 assert repr (test_ask ('Criminal(x)' , crime_kb )) == '[{x: West}]'
175188
189+
176190def test_d ():
177- assert d (x * x - x , x ) == 2 * x - 1
191+ assert d (x * x - x , x ) == 2 * x - 1
192+
178193
179194def test_WalkSAT ():
180- def check_SAT (clauses , single_solution = {}):
195+ def check_SAT (clauses , single_solution = {}):
181196 # Make sure the solution is correct if it is returned by WalkSat
182197 # Sometimes WalkSat may run out of flips before finding a solution
183198 soln = WalkSAT (clauses )
184199 if soln :
185200 assert all (pl_true (x , soln ) for x in clauses )
186- if single_solution : #Cross check the solution if only one exists
201+ if single_solution : # Cross check the solution if only one exists
187202 assert all (pl_true (x , single_solution ) for x in clauses )
188203 assert soln == single_solution
189204 # Test WalkSat for problems with solution
@@ -195,18 +210,19 @@ def check_SAT(clauses, single_solution = {}):
195210 assert WalkSAT ([A | B , ~ A , ~ (B | C ), C | D , P | Q ], 0.5 , 100 ) is None
196211 assert WalkSAT ([A | B , B & C , C | D , D & A , P , ~ P ], 0.5 , 100 ) is None
197212
213+
198214def test_SAT_plan ():
199- transition = {'A' :{'Left' : 'A' , 'Right' : 'B' },
200- 'B' :{'Left' : 'A' , 'Right' : 'C' },
201- 'C' :{'Left' : 'B' , 'Right' : 'C' }}
215+ transition = {'A' : {'Left' : 'A' , 'Right' : 'B' },
216+ 'B' : {'Left' : 'A' , 'Right' : 'C' },
217+ 'C' : {'Left' : 'B' , 'Right' : 'C' }}
202218 assert SAT_plan ('A' , transition , 'C' , 2 ) is None
203219 assert SAT_plan ('A' , transition , 'B' , 3 ) == ['Right' ]
204220 assert SAT_plan ('C' , transition , 'A' , 3 ) == ['Left' , 'Left' ]
205221
206- transition = {(0 , 0 ):{'Right' : (0 , 1 ), 'Down' : (1 , 0 )},
207- (0 , 1 ):{'Left' : (1 , 0 ), 'Down' : (1 , 1 )},
208- (1 , 0 ):{'Right' : (1 , 0 ), 'Up' : (1 , 0 ), 'Left' : (1 , 0 ), 'Down' : (1 , 0 )},
209- (1 , 1 ):{'Left' : (1 , 0 ), 'Up' : (0 , 1 )}}
222+ transition = {(0 , 0 ): {'Right' : (0 , 1 ), 'Down' : (1 , 0 )},
223+ (0 , 1 ): {'Left' : (1 , 0 ), 'Down' : (1 , 1 )},
224+ (1 , 0 ): {'Right' : (1 , 0 ), 'Up' : (1 , 0 ), 'Left' : (1 , 0 ), 'Down' : (1 , 0 )},
225+ (1 , 1 ): {'Left' : (1 , 0 ), 'Up' : (0 , 1 )}}
210226 assert SAT_plan ((0 , 0 ), transition , (1 , 1 ), 4 ) == ['Right' , 'Down' ]
211227
212228
0 commit comments