Deduction rule.
| 372 | |
| 373 | |
| 374 | class Theorem: |
| 375 | """Deduction rule.""" |
| 376 | |
| 377 | @classmethod |
| 378 | def from_txt_file(cls, fname: str, to_dict: bool = False) -> Theorem: |
| 379 | with open(fname, 'r') as f: |
| 380 | theorems = f.read() |
| 381 | return cls.from_string(theorems, to_dict) |
| 382 | |
| 383 | @classmethod |
| 384 | def from_string(cls, string: str, to_dict: bool = False) -> Theorem: |
| 385 | """Load deduction rule from a str object.""" |
| 386 | theorems = string.split('\n') |
| 387 | theorems = [l for l in theorems if l and not l.startswith('#')] |
| 388 | theorems = [cls.from_txt(l) for l in theorems] |
| 389 | |
| 390 | for i, th in enumerate(theorems): |
| 391 | th.rule_name = 'r{:02}'.format(i) |
| 392 | |
| 393 | if to_dict: |
| 394 | result = {} |
| 395 | for t in theorems: |
| 396 | if t.name in result: |
| 397 | t.name += '_' |
| 398 | result[t.rule_name] = t |
| 399 | |
| 400 | return result |
| 401 | |
| 402 | return theorems |
| 403 | |
| 404 | @classmethod |
| 405 | def from_txt(cls, data: str) -> Theorem: |
| 406 | premises, conclusion = data.split(' => ') |
| 407 | premises = premises.split(', ') |
| 408 | conclusion = conclusion.split(', ') |
| 409 | return Theorem( |
| 410 | premise=[Construction.from_txt(p) for p in premises], |
| 411 | conclusion=[Construction.from_txt(c) for c in conclusion], |
| 412 | ) |
| 413 | |
| 414 | def __init__( |
| 415 | self, premise: list[Construction], conclusion: list[Construction] |
| 416 | ): |
| 417 | if len(conclusion) != 1: |
| 418 | raise ValueError('Cannot have more than one conclusion') |
| 419 | self.name = '_'.join([p.name for p in premise + conclusion]) |
| 420 | self.premise = premise |
| 421 | self.conclusion = conclusion |
| 422 | self.is_arg_reduce = False |
| 423 | |
| 424 | assert len(self.conclusion) == 1 |
| 425 | con = self.conclusion[0] |
| 426 | |
| 427 | if con.name in [ |
| 428 | 'eqratio3', |
| 429 | 'midp', |
| 430 | 'contri', |
| 431 | 'simtri', |