Coverage for /usr/lib/python3/dist-packages/sympy/logic/inference.py: 20%

1"""Inference in propositional logic""" 

2 

3from sympy.logic.boolalg import And, Not, conjuncts, to_cnf, BooleanFunction 

4from sympy.core.sorting import ordered 

5from sympy.core.sympify import sympify 

6from sympy.external.importtools import import_module 

7 

8 

9def literal_symbol(literal): 

10 """ 

11 The symbol in this literal (without the negation). 

12 

13 Examples 

14 ======== 

15 

16 >>> from sympy.abc import A 

17 >>> from sympy.logic.inference import literal_symbol 

18 >>> literal_symbol(A) 

19 A 

20 >>> literal_symbol(~A) 

21 A 

22 

23 """ 

24 

25 if literal is True or literal is False: 

26 return literal 

27 try: 

28 if literal.is_Symbol: 

29 return literal 

30 if literal.is_Not: 

31 return literal_symbol(literal.args[0]) 

32 else: 

33 raise ValueError 

34 except (AttributeError, ValueError): 

35 raise ValueError("Argument must be a boolean literal.") 

36 

37 

38def satisfiable(expr, algorithm=None, all_models=False, minimal=False): 

39 """ 

40 Check satisfiability of a propositional sentence. 

41 Returns a model when it succeeds. 

42 Returns {true: true} for trivially true expressions. 

43 

44 On setting all_models to True, if given expr is satisfiable then 

45 returns a generator of models. However, if expr is unsatisfiable 

46 then returns a generator containing the single element False. 

47 

48 Examples 

49 ======== 

50 

51 >>> from sympy.abc import A, B 

52 >>> from sympy.logic.inference import satisfiable 

53 >>> satisfiable(A & ~B) 

54 {A: True, B: False} 

55 >>> satisfiable(A & ~A) 

56 False 

57 >>> satisfiable(True) 

58 {True: True} 

59 >>> next(satisfiable(A & ~A, all_models=True)) 

60 False 

61 >>> models = satisfiable((A >> B) & B, all_models=True) 

62 >>> next(models) 

63 {A: False, B: True} 

64 >>> next(models) 

65 {A: True, B: True} 

66 >>> def use_models(models): 

67 ... for model in models: 

68 ... if model: 

69 ... # Do something with the model. 

70 ... print(model) 

71 ... else: 

72 ... # Given expr is unsatisfiable. 

73 ... print("UNSAT") 

74 >>> use_models(satisfiable(A >> ~A, all_models=True)) 

75 {A: False} 

76 >>> use_models(satisfiable(A ^ A, all_models=True)) 

77 UNSAT 

78 

79 """ 

80 if algorithm is None or algorithm == "pycosat": 

81 pycosat = import_module('pycosat') 

82 if pycosat is not None: 

83 algorithm = "pycosat" 

84 else: 

85 if algorithm == "pycosat": 

86 raise ImportError("pycosat module is not present") 

87 # Silently fall back to dpll2 if pycosat 

88 # is not installed 

89 algorithm = "dpll2" 

90 

91 if algorithm=="minisat22": 

92 pysat = import_module('pysat') 

93 if pysat is None: 

94 algorithm = "dpll2" 

95 

96 if algorithm == "dpll": 

97 from sympy.logic.algorithms.dpll import dpll_satisfiable 

98 return dpll_satisfiable(expr) 

99 elif algorithm == "dpll2": 

100 from sympy.logic.algorithms.dpll2 import dpll_satisfiable 

101 return dpll_satisfiable(expr, all_models) 

102 elif algorithm == "pycosat": 

103 from sympy.logic.algorithms.pycosat_wrapper import pycosat_satisfiable 

104 return pycosat_satisfiable(expr, all_models) 

105 elif algorithm == "minisat22": 

106 from sympy.logic.algorithms.minisat22_wrapper import minisat22_satisfiable 

107 return minisat22_satisfiable(expr, all_models, minimal) 

108 raise NotImplementedError 

109 

110 

111def valid(expr): 

112 """ 

113 Check validity of a propositional sentence. 

114 A valid propositional sentence is True under every assignment. 

115 

116 Examples 

117 ======== 

118 

119 >>> from sympy.abc import A, B 

120 >>> from sympy.logic.inference import valid 

121 >>> valid(A | ~A) 

122 True 

123 >>> valid(A | B) 

124 False 

125 

126 References 

127 ========== 

128 

129 .. [1] https://en.wikipedia.org/wiki/Validity 

130 

131 """ 

132 return not satisfiable(Not(expr)) 

133 

134 

135def pl_true(expr, model=None, deep=False): 

136 """ 

137 Returns whether the given assignment is a model or not. 

138 

139 If the assignment does not specify the value for every proposition, 

140 this may return None to indicate 'not obvious'. 

141 

142 Parameters 

143 ========== 

144 

145 model : dict, optional, default: {} 

146 Mapping of symbols to boolean values to indicate assignment. 

147 deep: boolean, optional, default: False 

148 Gives the value of the expression under partial assignments 

149 correctly. May still return None to indicate 'not obvious'. 

150 

151 

152 Examples 

153 ======== 

154 

155 >>> from sympy.abc import A, B 

156 >>> from sympy.logic.inference import pl_true 

157 >>> pl_true( A & B, {A: True, B: True}) 

158 True 

159 >>> pl_true(A & B, {A: False}) 

160 False 

161 >>> pl_true(A & B, {A: True}) 

162 >>> pl_true(A & B, {A: True}, deep=True) 

163 >>> pl_true(A >> (B >> A)) 

164 >>> pl_true(A >> (B >> A), deep=True) 

165 True 

166 >>> pl_true(A & ~A) 

167 >>> pl_true(A & ~A, deep=True) 

168 False 

169 >>> pl_true(A & B & (~A | ~B), {A: True}) 

170 >>> pl_true(A & B & (~A | ~B), {A: True}, deep=True) 

171 False 

172 

173 """ 

174 

175 from sympy.core.symbol import Symbol 

176 

177 boolean = (True, False) 

178 

179 def _validate(expr): 

180 if isinstance(expr, Symbol) or expr in boolean: 

181 return True 

182 if not isinstance(expr, BooleanFunction): 

183 return False 

184 return all(_validate(arg) for arg in expr.args) 

185 

186 if expr in boolean: 

187 return expr 

188 expr = sympify(expr) 

189 if not _validate(expr): 

190 raise ValueError("%s is not a valid boolean expression" % expr) 

191 if not model: 

192 model = {} 

193 model = {k: v for k, v in model.items() if v in boolean} 

194 result = expr.subs(model) 

195 if result in boolean: 

196 return bool(result) 

197 if deep: 

198 model = {k: True for k in result.atoms()} 

199 if pl_true(result, model): 

200 if valid(result): 

201 return True 

202 else: 

203 if not satisfiable(result): 

204 return False 

205 return None 

206 

207 

208def entails(expr, formula_set=None): 

209 """ 

210 Check whether the given expr_set entail an expr. 

211 If formula_set is empty then it returns the validity of expr. 

212 

213 Examples 

214 ======== 

215 

216 >>> from sympy.abc import A, B, C 

217 >>> from sympy.logic.inference import entails 

218 >>> entails(A, [A >> B, B >> C]) 

219 False 

220 >>> entails(C, [A >> B, B >> C, A]) 

221 True 

222 >>> entails(A >> B) 

223 False 

224 >>> entails(A >> (B >> A)) 

225 True 

226 

227 References 

228 ========== 

229 

230 .. [1] https://en.wikipedia.org/wiki/Logical_consequence 

231 

232 """ 

233 if formula_set: 

234 formula_set = list(formula_set) 

235 else: 

236 formula_set = [] 

237 formula_set.append(Not(expr)) 

238 return not satisfiable(And(*formula_set)) 

239 

240 

241class KB: 

242 """Base class for all knowledge bases""" 

243 def __init__(self, sentence=None): 

244 self.clauses_ = set() 

245 if sentence: 

246 self.tell(sentence) 

247 

248 def tell(self, sentence): 

249 raise NotImplementedError 

250 

251 def ask(self, query): 

252 raise NotImplementedError 

253 

254 def retract(self, sentence): 

255 raise NotImplementedError 

256 

257 @property 

258 def clauses(self): 

259 return list(ordered(self.clauses_)) 

260 

261 

262class PropKB(KB): 

263 """A KB for Propositional Logic. Inefficient, with no indexing.""" 

264 

265 def tell(self, sentence): 

266 """Add the sentence's clauses to the KB 

267 

268 Examples 

269 ======== 

270 

271 >>> from sympy.logic.inference import PropKB 

272 >>> from sympy.abc import x, y 

273 >>> l = PropKB() 

274 >>> l.clauses 

275 [] 

276 

277 >>> l.tell(x | y) 

278 >>> l.clauses 

279 [x | y] 

280 

281 >>> l.tell(y) 

282 >>> l.clauses 

283 [y, x | y] 

284 

285 """ 

286 for c in conjuncts(to_cnf(sentence)): 

287 self.clauses_.add(c) 

288 

289 def ask(self, query): 

290 """Checks if the query is true given the set of clauses. 

291 

292 Examples 

293 ======== 

294 

295 >>> from sympy.logic.inference import PropKB 

296 >>> from sympy.abc import x, y 

297 >>> l = PropKB() 

298 >>> l.tell(x & ~y) 

299 >>> l.ask(x) 

300 True 

301 >>> l.ask(y) 

302 False 

303 

304 """ 

305 return entails(query, self.clauses_) 

306 

307 def retract(self, sentence): 

308 """Remove the sentence's clauses from the KB 

309 

310 Examples 

311 ======== 

312 

313 >>> from sympy.logic.inference import PropKB 

314 >>> from sympy.abc import x, y 

315 >>> l = PropKB() 

316 >>> l.clauses 

317 [] 

318 

319 >>> l.tell(x | y) 

320 >>> l.clauses 

321 [x | y] 

322 

323 >>> l.retract(x | y) 

324 >>> l.clauses 

325 [] 

326 

327 """ 

328 for c in conjuncts(to_cnf(sentence)): 

329 self.clauses_.discard(c)