Coverage for /usr/lib/python3/dist-packages/sympy/core/facts.py: 40%

1r"""This is rule-based deduction system for SymPy

3The whole thing is split into two parts

5 - rules compilation and preparation of tables

6 - runtime inference

8For rule-based inference engines, the classical work is RETE algorithm [1],

9[2] Although we are not implementing it in full (or even significantly)

10it's still worth a read to understand the underlying ideas.

12In short, every rule in a system of rules is one of two forms:

14 - atom -> ... (alpha rule)

15 - And(atom1, atom2, ...) -> ... (beta rule)

18The major complexity is in efficient beta-rules processing and usually for an

19expert system a lot of effort goes into code that operates on beta-rules.

22Here we take minimalistic approach to get something usable first.

24 - (preparation) of alpha- and beta- networks, everything except

25 - (runtime) FactRules.deduce_all_facts

27 _____________________________________

28 ( Kirr: I've never thought that doing )

29 ( logic stuff is that difficult... )

30 -------------------------------------

31 o ^__^

32 o (oo)\_______

33 (__)\ )\/\

34 ||----w |

35 || ||

38Some references on the topic

39----------------------------

41[1] https://en.wikipedia.org/wiki/Rete_algorithm

42[2] http://reports-archive.adm.cs.cmu.edu/anon/1995/CMU-CS-95-113.pdf

44https://en.wikipedia.org/wiki/Propositional_formula

45https://en.wikipedia.org/wiki/Inference_rule

46https://en.wikipedia.org/wiki/List_of_rules_of_inference

47"""

49from collections import defaultdict

50from typing import Iterator

52from .logic import Logic, And, Or, Not

55def _base_fact(atom):

56 """Return the literal fact of an atom.

58 Effectively, this merely strips the Not around a fact.

59 """

60 if isinstance(atom, Not):

61 return atom.arg

62 else:

63 return atom

66def _as_pair(atom):

67 if isinstance(atom, Not):

68 return (atom.arg, False)

69 else:

70 return (atom, True)

72# XXX this prepares forward-chaining rules for alpha-network

75def transitive_closure(implications):

76 """

77 Computes the transitive closure of a list of implications

79 Uses Warshall's algorithm, as described at

80 http://www.cs.hope.edu/~cusack/Notes/Notes/DiscreteMath/Warshall.pdf.

81 """

82 full_implications = set(implications)

83 literals = set().union(*map(set, full_implications))

85 for k in literals:

86 for i in literals:

87 if (i, k) in full_implications:

88 for j in literals:

89 if (k, j) in full_implications:

90 full_implications.add((i, j))

92 return full_implications

95def deduce_alpha_implications(implications):

96 """deduce all implications

98 Description by example

99 ----------------------

100

101 given set of logic rules:

102

103 a -> b

104 b -> c

105

106 we deduce all possible rules:

107

108 a -> b, c

109 b -> c

110

111

112 implications: [] of (a,b)

113 return: {} of a -> set([b, c, ...])

114 """

115 implications = implications + [(Not(j), Not(i)) for (i, j) in implications]

116 res = defaultdict(set)

117 full_implications = transitive_closure(implications)

118 for a, b in full_implications:

119 if a == b:

120 continue # skip a->a cyclic input

121

122 res[a].add(b)

123

124 # Clean up tautologies and check consistency

125 for a, impl in res.items():

126 impl.discard(a)

127 na = Not(a)

128 if na in impl:

129 raise ValueError(

130 'implications are inconsistent: %s -> %s %s' % (a, na, impl))

131

132 return res

133

134

135def apply_beta_to_alpha_route(alpha_implications, beta_rules):

136 """apply additional beta-rules (And conditions) to already-built

137 alpha implication tables

138

139 TODO: write about

140

141 - static extension of alpha-chains

142 - attaching refs to beta-nodes to alpha chains

143

144

145 e.g.

146

147 alpha_implications:

148

149 a -> [b, !c, d]

150 b -> [d]

151 ...

154 beta_rules:

156 &(b,d) -> e

159 then we'll extend a's rule to the following

160

161 a -> [b, !c, d, e]

162 """

163 x_impl = {}

164 for x in alpha_implications.keys():

165 x_impl[x] = (set(alpha_implications[x]), [])

166 for bcond, bimpl in beta_rules:

167 for bk in bcond.args:

168 if bk in x_impl:

169 continue

170 x_impl[bk] = (set(), [])

171

172 # static extensions to alpha rules:

173 # A: x -> a,b B: &(a,b) -> c ==> A: x -> a,b,c

174 seen_static_extension = True

175 while seen_static_extension:

176 seen_static_extension = False

177

178 for bcond, bimpl in beta_rules:

179 if not isinstance(bcond, And):

180 raise TypeError("Cond is not And")

181 bargs = set(bcond.args)

182 for x, (ximpls, bb) in x_impl.items():

183 x_all = ximpls | {x}

184 # A: ... -> a B: &(...) -> a is non-informative

185 if bimpl not in x_all and bargs.issubset(x_all):

186 ximpls.add(bimpl)

187

188 # we introduced new implication - now we have to restore

189 # completeness of the whole set.

190 bimpl_impl = x_impl.get(bimpl)

191 if bimpl_impl is not None:

192 ximpls |= bimpl_impl[0]

193 seen_static_extension = True

194

195 # attach beta-nodes which can be possibly triggered by an alpha-chain

196 for bidx, (bcond, bimpl) in enumerate(beta_rules):

197 bargs = set(bcond.args)

198 for x, (ximpls, bb) in x_impl.items():

199 x_all = ximpls | {x}

200 # A: ... -> a B: &(...) -> a (non-informative)

201 if bimpl in x_all:

202 continue

203 # A: x -> a... B: &(!a,...) -> ... (will never trigger)

204 # A: x -> a... B: &(...) -> !a (will never trigger)

205 if any(Not(xi) in bargs or Not(xi) == bimpl for xi in x_all):

206 continue

207

208 if bargs & x_all:

209 bb.append(bidx)

210

211 return x_impl

212

213

214def rules_2prereq(rules):

215 """build prerequisites table from rules

216

217 Description by example

218 ----------------------

219

220 given set of logic rules:

221

222 a -> b, c

223 b -> c

224

225 we build prerequisites (from what points something can be deduced):

226

227 b <- a

228 c <- a, b

229

230 rules: {} of a -> [b, c, ...]

231 return: {} of c <- [a, b, ...]

232

233 Note however, that this prerequisites may be *not* enough to prove a

234 fact. An example is 'a -> b' rule, where prereq(a) is b, and prereq(b)

235 is a. That's because a=T -> b=T, and b=F -> a=F, but a=F -> b=?

236 """

237 prereq = defaultdict(set)

238 for (a, _), impl in rules.items():

239 if isinstance(a, Not):

240 a = a.args[0]

241 for (i, _) in impl:

242 if isinstance(i, Not):

243 i = i.args[0]

244 prereq[i].add(a)

245 return prereq

246

247################

248# RULES PROVER #

249################

250

251

252class TautologyDetected(Exception):

253 """(internal) Prover uses it for reporting detected tautology"""

254 pass

255

256

257class Prover:

258 """ai - prover of logic rules

259

260 given a set of initial rules, Prover tries to prove all possible rules

261 which follow from given premises.

262

263 As a result proved_rules are always either in one of two forms: alpha or

264 beta:

265

266 Alpha rules

267 -----------

268

269 This are rules of the form::

270

271 a -> b & c & d & ...

272

273

274 Beta rules

275 ----------

276

277 This are rules of the form::

278

279 &(a,b,...) -> c & d & ...

280

281

282 i.e. beta rules are join conditions that say that something follows when

283 *several* facts are true at the same time.

284 """

285

286 def __init__(self):

287 self.proved_rules = []

288 self._rules_seen = set()

289

290 def split_alpha_beta(self):

291 """split proved rules into alpha and beta chains"""

292 rules_alpha = [] # a -> b

293 rules_beta = [] # &(...) -> b

294 for a, b in self.proved_rules:

295 if isinstance(a, And):

296 rules_beta.append((a, b))

297 else:

298 rules_alpha.append((a, b))

299 return rules_alpha, rules_beta

300

301 @property

302 def rules_alpha(self):

303 return self.split_alpha_beta()[0]

304

305 @property

306 def rules_beta(self):

307 return self.split_alpha_beta()[1]

308

309 def process_rule(self, a, b):

310 """process a -> b rule""" # TODO write more?

311 if (not a) or isinstance(b, bool):

312 return

313 if isinstance(a, bool):

314 return

315 if (a, b) in self._rules_seen:

316 return

317 else:

318 self._rules_seen.add((a, b))

319

320 # this is the core of processing

321 try:

322 self._process_rule(a, b)

323 except TautologyDetected:

324 pass

325

326 def _process_rule(self, a, b):

327 # right part first

328

329 # a -> b & c --> a -> b ; a -> c

330 # (?) FIXME this is only correct when b & c != null !

331

332 if isinstance(b, And):

333 sorted_bargs = sorted(b.args, key=str)

334 for barg in sorted_bargs:

335 self.process_rule(a, barg)

336

337 # a -> b | c --> !b & !c -> !a

338 # --> a & !b -> c

339 # --> a & !c -> b

340 elif isinstance(b, Or):

341 sorted_bargs = sorted(b.args, key=str)

342 # detect tautology first

343 if not isinstance(a, Logic): # Atom

344 # tautology: a -> a|c|...

345 if a in sorted_bargs:

346 raise TautologyDetected(a, b, 'a -> a|c|...')

347 self.process_rule(And(*[Not(barg) for barg in b.args]), Not(a))

348

349 for bidx in range(len(sorted_bargs)):

350 barg = sorted_bargs[bidx]

351 brest = sorted_bargs[:bidx] + sorted_bargs[bidx + 1:]

352 self.process_rule(And(a, Not(barg)), Or(*brest))

353

354 # left part

355

356 # a & b -> c --> IRREDUCIBLE CASE -- WE STORE IT AS IS

357 # (this will be the basis of beta-network)

358 elif isinstance(a, And):

359 sorted_aargs = sorted(a.args, key=str)

360 if b in sorted_aargs:

361 raise TautologyDetected(a, b, 'a & b -> a')

362 self.proved_rules.append((a, b))

363 # XXX NOTE at present we ignore !c -> !a | !b

364

365 elif isinstance(a, Or):

366 sorted_aargs = sorted(a.args, key=str)

367 if b in sorted_aargs:

368 raise TautologyDetected(a, b, 'a | b -> a')

369 for aarg in sorted_aargs:

370 self.process_rule(aarg, b)

371

372 else:

373 # both `a` and `b` are atoms

374 self.proved_rules.append((a, b)) # a -> b

375 self.proved_rules.append((Not(b), Not(a))) # !b -> !a

376

377########################################

378

379

380class FactRules:

381 """Rules that describe how to deduce facts in logic space

382

383 When defined, these rules allow implications to quickly be determined

384 for a set of facts. For this precomputed deduction tables are used.

385 see `deduce_all_facts` (forward-chaining)

386

387 Also it is possible to gather prerequisites for a fact, which is tried

388 to be proven. (backward-chaining)

389

390

391 Definition Syntax

392 -----------------

393

394 a -> b -- a=T -> b=T (and automatically b=F -> a=F)

395 a -> !b -- a=T -> b=F

396 a == b -- a -> b & b -> a

397 a -> b & c -- a=T -> b=T & c=T

398 # TODO b | c

399

400

401 Internals

402 ---------

403

404 .full_implications[k, v]: all the implications of fact k=v

405 .beta_triggers[k, v]: beta rules that might be triggered when k=v

406 .prereq -- {} k <- [] of k's prerequisites

407

408 .defined_facts -- set of defined fact names

409 """

410

411 def __init__(self, rules):

412 """Compile rules into internal lookup tables"""

413

414 if isinstance(rules, str):

415 rules = rules.splitlines()

416

417 # --- parse and process rules ---

418 P = Prover()

419

420 for rule in rules:

421 # XXX `a` is hardcoded to be always atom

422 a, op, b = rule.split(None, 2)

423

424 a = Logic.fromstring(a)

425 b = Logic.fromstring(b)

426

427 if op == '->':

428 P.process_rule(a, b)

429 elif op == '==':

430 P.process_rule(a, b)

431 P.process_rule(b, a)

432 else:

433 raise ValueError('unknown op %r' % op)

434

435 # --- build deduction networks ---

436 self.beta_rules = []

437 for bcond, bimpl in P.rules_beta:

438 self.beta_rules.append(

439 ({_as_pair(a) for a in bcond.args}, _as_pair(bimpl)))

440

441 # deduce alpha implications

442 impl_a = deduce_alpha_implications(P.rules_alpha)

443

444 # now:

445 # - apply beta rules to alpha chains (static extension), and

446 # - further associate beta rules to alpha chain (for inference

447 # at runtime)

448 impl_ab = apply_beta_to_alpha_route(impl_a, P.rules_beta)

449

450 # extract defined fact names

451 self.defined_facts = {_base_fact(k) for k in impl_ab.keys()}

452

453 # build rels (forward chains)

454 full_implications = defaultdict(set)

455 beta_triggers = defaultdict(set)

456 for k, (impl, betaidxs) in impl_ab.items():

457 full_implications[_as_pair(k)] = {_as_pair(i) for i in impl}

458 beta_triggers[_as_pair(k)] = betaidxs

459

460 self.full_implications = full_implications

461 self.beta_triggers = beta_triggers

462

463 # build prereq (backward chains)

464 prereq = defaultdict(set)

465 rel_prereq = rules_2prereq(full_implications)

466 for k, pitems in rel_prereq.items():

467 prereq[k] |= pitems

468 self.prereq = prereq

469

470 def _to_python(self) -> str:

471 """ Generate a string with plain python representation of the instance """

472 return '\n'.join(self.print_rules())

473

474 @classmethod

475 def _from_python(cls, data : dict):

476 """ Generate an instance from the plain python representation """

477 self = cls('')

478 for key in ['full_implications', 'beta_triggers', 'prereq']:

479 d=defaultdict(set)

480 d.update(data[key])

481 setattr(self, key, d)

482 self.beta_rules = data['beta_rules']

483 self.defined_facts = set(data['defined_facts'])

484

485 return self

486

487 def _defined_facts_lines(self):

488 yield 'defined_facts = ['

489 for fact in sorted(self.defined_facts):

490 yield f' {fact!r},'

491 yield '] # defined_facts'

492

493 def _full_implications_lines(self):

494 yield 'full_implications = dict( ['

495 for fact in sorted(self.defined_facts):

496 for value in (True, False):

497 yield f' # Implications of {fact} = {value}:'

498 yield f' (({fact!r}, {value!r}), set( ('

499 implications = self.full_implications[(fact, value)]

500 for implied in sorted(implications):

501 yield f' {implied!r},'

502 yield ' ) ),'

503 yield ' ),'

504 yield ' ] ) # full_implications'

505

506 def _prereq_lines(self):

507 yield 'prereq = {'

508 yield ''

509 for fact in sorted(self.prereq):

510 yield f' # facts that could determine the value of {fact}'

511 yield f' {fact!r}: {{'

512 for pfact in sorted(self.prereq[fact]):

513 yield f' {pfact!r},'

514 yield ' },'

515 yield ''

516 yield '} # prereq'

517

518 def _beta_rules_lines(self):

519 reverse_implications = defaultdict(list)

520 for n, (pre, implied) in enumerate(self.beta_rules):

521 reverse_implications[implied].append((pre, n))

522

523 yield '# Note: the order of the beta rules is used in the beta_triggers'

524 yield 'beta_rules = ['

525 yield ''

526 m = 0

527 indices = {}

528 for implied in sorted(reverse_implications):

529 fact, value = implied

530 yield f' # Rules implying {fact} = {value}'

531 for pre, n in reverse_implications[implied]:

532 indices[n] = m

533 m += 1

534 setstr = ", ".join(map(str, sorted(pre)))

535 yield f' ({{{setstr}}},'

536 yield f' {implied!r}),'

537 yield ''

538 yield '] # beta_rules'

539

540 yield 'beta_triggers = {'

541 for query in sorted(self.beta_triggers):

542 fact, value = query

543 triggers = [indices[n] for n in self.beta_triggers[query]]

544 yield f' {query!r}: {triggers!r},'

545 yield '} # beta_triggers'

546

547 def print_rules(self) -> Iterator[str]:

548 """ Returns a generator with lines to represent the facts and rules """

549 yield from self._defined_facts_lines()

550 yield ''

551 yield ''

552 yield from self._full_implications_lines()

553 yield ''

554 yield ''

555 yield from self._prereq_lines()

556 yield ''

557 yield ''

558 yield from self._beta_rules_lines()

559 yield ''

560 yield ''

561 yield "generated_assumptions = {'defined_facts': defined_facts, 'full_implications': full_implications,"

562 yield " 'prereq': prereq, 'beta_rules': beta_rules, 'beta_triggers': beta_triggers}"

563

564

565class InconsistentAssumptions(ValueError):

566 def __str__(self):

567 kb, fact, value = self.args

568 return "%s, %s=%s" % (kb, fact, value)

569

570

571class FactKB(dict):

572 """

573 A simple propositional knowledge base relying on compiled inference rules.

574 """

575 def __str__(self):

576 return '{\n%s}' % ',\n'.join(

577 ["\t%s: %s" % i for i in sorted(self.items())])

578

579 def __init__(self, rules):

580 self.rules = rules

581

582 def _tell(self, k, v):

583 """Add fact k=v to the knowledge base.

584

585 Returns True if the KB has actually been updated, False otherwise.

586 """

587 if k in self and self[k] is not None:

588 if self[k] == v:

589 return False

590 else:

591 raise InconsistentAssumptions(self, k, v)

592 else:

593 self[k] = v

594 return True

595

596 # *********************************************

597 # * This is the workhorse, so keep it *fast*. *

598 # *********************************************

599 def deduce_all_facts(self, facts):

600 """

601 Update the KB with all the implications of a list of facts.

602

603 Facts can be specified as a dictionary or as a list of (key, value)

604 pairs.

605 """

606 # keep frequently used attributes locally, so we'll avoid extra

607 # attribute access overhead

608 full_implications = self.rules.full_implications

609 beta_triggers = self.rules.beta_triggers

610 beta_rules = self.rules.beta_rules

611

612 if isinstance(facts, dict):

613 facts = facts.items()

614

615 while facts:

616 beta_maytrigger = set()

617

618 # --- alpha chains ---

619 for k, v in facts:

620 if not self._tell(k, v) or v is None:

621 continue

622

623 # lookup routing tables

624 for key, value in full_implications[k, v]:

625 self._tell(key, value)

626

627 beta_maytrigger.update(beta_triggers[k, v])

628

629 # --- beta chains ---

630 facts = []

631 for bidx in beta_maytrigger:

632 bcond, bimpl = beta_rules[bidx]

633 if all(self.get(k) is v for k, v in bcond):

634 facts.append(bimpl)