Mapping Matcher

Implements theorem matching functions for the Deductive Database (DD).

class MappingMatcher(theorem_mapper)

Bases: RuleMatcher

match_theorem(rule, proof)

Match all dependencies created by the given rule given the existing dependency graph.

Return type:: set[Assumption | NumericalCheck | RuleApplication | ARDeduction | CircleMerge | LineMerge | DirectConsequence | Reflexivity]

class TheoremMapper

Bases: ABC

abstractmethod mappings(rule, points, proof)

Find valid mappings for the given rule using the given points.

Return type:: Generator[dict[NewType(VarName, str), NewType(PredicateArgument, str)], None, None]

class CCMapper

Bases: TheoremMapper

mappings(rule, points, proof)

Find valid mappings for the given rule using the given points.

Return type:: Generator[dict[NewType(VarName, str), NewType(PredicateArgument, str)], None, None]

class FilterMapper

Bases: TheoremMapper

mappings(rule, points, proof)

Find valid mappings for the given rule using the given points.

Return type:: Generator[dict[NewType(VarName, str), NewType(PredicateArgument, str)], None, None]

predictates_by_type_name_from_hypergraph(hyper_graph)

Return type:: dict[PredicateType, list[Circumcenter | Cong | Coll | NColl | Cyclic | ConstantAngle | ACompute | LCompute | ConstantLength | ConstantRatio | EqAngle | Diff | RCompute | ObtuseAngle | MidPoint | EqRatio | Perp | NPerp | Para | NPara | SameClock | SameSide | NSameSide | PythagoreanPremises | PythagoreanConclusions | SquaredConstantLength | SquaredConstantRatio | SimtriClock | SimtriReflect | ContriClock | ContriReflect | AngleEquation | LengthEquation]]

iterate_mapping_with_complementary_assignments(mapping, remaining_variables_in_theorem, points)

Yields mappings with additional variable assignments.

For a given initial mapping of variables to points, yields either: 1. Just the input mapping if there are no remaining unmapped variables 2. New mappings that combine the input mapping with all possible assignments of the remaining unmapped variables to points

Parameters:: mapping (dict[NewType(VarName, str), NewType(PredicateArgument, str)]) – Initial dict mapping theorem variables to point names
Yields:: Iterator mapping all theorem variables to point names
Return type:: Generator[dict[NewType(VarName, str), NewType(PredicateArgument, str)], None, None]

class PartialMapping(vars_to_assign, predicates, lookup_dict=None, valid_arg_permutations=None, partial_assignment=None, permutation_idxs_compatible_with_partial_assignment=None)

Bases: object

lookup_dict: dict[NewType(VarName, str), dict[NewType(PredicateArgument, str), set[int]]]

valid_arg_permutations: list[Union[PerpStatement, ParaStatement, EqangleStatement, EqratioStatement, CongStatement, MidptStatement, CollStatement, CircleStatement, TriangleStatement, CyclicStatement]]

mapping_hash: str

predicate_name: str

predicates: list[Union[PerpStatement, ParaStatement, EqangleStatement, EqratioStatement, CongStatement, MidptStatement, CollStatement, CircleStatement, TriangleStatement, CyclicStatement]]

vars_to_assign: tuple[NewType(VarName, str), ...]

partial_assignment: dict[NewType(VarName, str), NewType(PredicateArgument, str)]

permutation_idxs_compatible_with_partial_assignment: set[int]

with_assignment(var, point)

Return type:: PartialMapping | None

iterate_mappings(partial_mappings, remaining_variables, remaining_points, current_assignment=None, conclusions_yielded=None, allow_point_repetition=False)

Return type:: Iterator[dict[NewType(VarName, str), NewType(PredicateArgument, str)]]