graph.py

# Copyright 2023 DeepMind Technologies Limited
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#    http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
# ==============================================================================

"""Implements the graph representation of the proof state."""

# pylint: disable=g-multiple-import
from __future__ import annotations

from collections import defaultdict  # pylint: disable=g-importing-member
from typing import Callable, Generator, Optional, Type, Union

from absl import logging
import ar
import geometry as gm
from geometry import Angle, Direction, Length, Ratio
from geometry import Circle, Line, Point, Segment
from geometry import Measure, Value
import graph_utils as utils
import numericals as nm
import problem
from problem import Dependency, EmptyDependency


np = nm.np


FREE = [
    'free',
    'segment',
    'r_triangle',
    'risos',
    'triangle',
    'triangle12',
    'ieq_triangle',
    'eq_quadrangle',
    'eq_trapezoid',
    'eqdia_quadrangle',
    'quadrangle',
    'r_trapezoid',
    'rectangle',
    'isquare',
    'trapezoid',
    'pentagon',
    'iso_triangle',
]

INTERSECT = [
    'angle_bisector',
    'angle_mirror',
    'eqdistance',
    'lc_tangent',
    'on_aline',
    'on_bline',
    'on_circle',
    'on_line',
    'on_pline',
    'on_tline',
    'on_dia',
    's_angle',
    'on_opline',
    'eqangle3',
]


# pylint: disable=protected-access
# pylint: disable=unused-argument


class DepCheckFailError(Exception):
  pass


class PointTooCloseError(Exception):
  pass


class PointTooFarError(Exception):
  pass


class Graph:
  """Graph data structure representing proof state."""

  def __init__(self):
    self.type2nodes = {
        Point: [],
        Line: [],
        Segment: [],
        Circle: [],
        Direction: [],
        Length: [],
        Angle: [],
        Ratio: [],
        Measure: [],
        Value: [],
    }
    self._name2point = {}
    self._name2node = {}

    self.rconst = {}  # contains all constant ratios
    self.aconst = {}  # contains all constant angles.

    self.halfpi, _ = self.get_or_create_const_ang(1, 2)
    self.vhalfpi = self.halfpi.val

    self.atable = ar.AngleTable()
    self.dtable = ar.DistanceTable()
    self.rtable = ar.RatioTable()

    # to quick access deps.
    self.cache = {}

    self._pair2line = {}
    self._triplet2circle = {}

  def copy(self) -> Graph:
    """Make a copy of self."""
    p, definitions = self.build_def

    p = p.copy()
    for clause in p.clauses:
      clause.nums = []
      for pname in clause.points:
        clause.nums.append(self._name2node[pname].num)

    g, _ = Graph.build_problem(p, definitions, verbose=False, init_copy=False)

    g.build_clauses = list(getattr(self, 'build_clauses', []))
    return g

  def _create_const_ang(self, n: int, d: int) -> None:
    n, d = ar.simplify(n, d)
    ang = self.aconst[(n, d)] = self.new_node(Angle, f'{n}pi/{d}')
    ang.set_directions(None, None)
    self.connect_val(ang, deps=None)

  def _create_const_rat(self, n: int, d: int) -> None:
    n, d = ar.simplify(n, d)
    rat = self.rconst[(n, d)] = self.new_node(Ratio, f'{n}/{d}')
    rat.set_lengths(None, None)
    self.connect_val(rat, deps=None)

  def get_or_create_const_ang(self, n: int, d: int) -> None:
    n, d = ar.simplify(n, d)
    if (n, d) not in self.aconst:
      self._create_const_ang(n, d)
    ang1 = self.aconst[(n, d)]

    n, d = ar.simplify(d - n, d)
    if (n, d) not in self.aconst:
      self._create_const_ang(n, d)
    ang2 = self.aconst[(n, d)]
    return ang1, ang2

  def get_or_create_const_rat(self, n: int, d: int) -> None:
    n, d = ar.simplify(n, d)
    if (n, d) not in self.rconst:
      self._create_const_rat(n, d)
    rat1 = self.rconst[(n, d)]

    if (d, n) not in self.rconst:
      self._create_const_rat(d, n)  # pylint: disable=arguments-out-of-order
    rat2 = self.rconst[(d, n)]
    return rat1, rat2

  def add_algebra(self, dep: Dependency, level: int) -> None:
    """Add new algebraic predicates."""
    _ = level
    if dep.name not in [
        'para',
        'perp',
        'eqangle',
        'eqratio',
        'aconst',
        'rconst',
        'cong',
    ]:
      return

    name, args = dep.name, dep.args

    if name == 'para':
      ab, cd = dep.algebra
      self.atable.add_para(ab, cd, dep)

    if name == 'perp':
      ab, cd = dep.algebra
      self.atable.add_const_angle(ab, cd, 90, dep)

    if name == 'eqangle':
      ab, cd, mn, pq = dep.algebra
      if (ab, cd) == (pq, mn):
        self.atable.add_const_angle(ab, cd, 90, dep)
      else:
        self.atable.add_eqangle(ab, cd, mn, pq, dep)

    if name == 'eqratio':
      ab, cd, mn, pq = dep.algebra
      if (ab, cd) == (pq, mn):
        self.rtable.add_eq(ab, cd, dep)
      else:
        self.rtable.add_eqratio(ab, cd, mn, pq, dep)

    if name == 'aconst':
      bx, ab, y = dep.algebra
      self.atable.add_const_angle(bx, ab, y, dep)

    if name == 'rconst':
      l1, l2, m, n = dep.algebra
      self.rtable.add_const_ratio(l1, l2, m, n, dep)

    if name == 'cong':
      a, b, c, d = args
      ab, _ = self.get_line_thru_pair_why(a, b)
      cd, _ = self.get_line_thru_pair_why(c, d)
      self.dtable.add_cong(ab, cd, a, b, c, d, dep)

      ab, cd = dep.algebra
      self.rtable.add_eq(ab, cd, dep)

  def add_eqrat_const(
      self, args: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add new algebraic predicates of type eqratio-constant."""
    a, b, c, d, num, den = args
    nd, dn = self.get_or_create_const_rat(num, den)

    if num == den:
      return self.add_cong([a, b, c, d], deps)

    ab = self._get_or_create_segment(a, b, deps=None)
    cd = self._get_or_create_segment(c, d, deps=None)

    self.connect_val(ab, deps=None)
    self.connect_val(cd, deps=None)

    if ab.val == cd.val:
      raise ValueError(f'{ab.name} and {cd.name} cannot be equal')

    args = [a, b, c, d, nd]
    i = 0
    for x, y, xy in [(a, b, ab), (c, d, cd)]:
      i += 1
      x_, y_ = list(xy._val._obj.points)
      if {x, y} == {x_, y_}:
        continue
      if deps:
        deps = deps.extend(self, 'rconst', list(args), 'cong', [x, y, x_, y_])
      args[2 * i - 2] = x_
      args[2 * i - 1] = y_

    ab_cd, cd_ab, why = self._get_or_create_ratio(ab, cd, deps=None)
    if why:
      dep0 = deps.populate('rconst', [a, b, c, d, nd])
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why

    lab, lcd = ab_cd._l
    a, b = list(lab._obj.points)
    c, d = list(lcd._obj.points)

    add = []
    if not self.is_equal(ab_cd, nd):
      args = [a, b, c, d, nd]
      dep1 = deps.populate('rconst', args)
      dep1.algebra = ab._val, cd._val, num, den
      self.make_equal(nd, ab_cd, deps=dep1)
      self.cache_dep('rconst', [a, b, c, d, nd], dep1)
      add += [dep1]

    if not self.is_equal(cd_ab, dn):
      args = [c, d, a, b, dn]
      dep2 = deps.populate('rconst', args)
      dep2.algebra = cd._val, ab._val, num, den
      self.make_equal(dn, cd_ab, deps=dep2)
      self.cache_dep('rconst', [c, d, a, b, dn], dep2)
      add += [dep2]

    return add

  def do_algebra(self, name: str, args: list[Point]) -> list[Dependency]:
    """Derive (but not add) new algebraic predicates."""
    if name == 'para':
      a, b, dep = args
      if gm.is_equiv(a, b):
        return []
      (x, y), (m, n) = a._obj.points, b._obj.points
      return self.add_para([x, y, m, n], dep)

    if name == 'aconst':
      a, b, n, d, dep = args
      ab, ba, why = self.get_or_create_angle_d(a, b, deps=None)
      nd, dn = self.get_or_create_const_ang(n, d)

      (x, y), (m, n) = a._obj.points, b._obj.points

      if why:
        dep0 = dep.populate('aconst', [x, y, m, n, nd])
        dep = EmptyDependency(level=dep.level, rule_name=None)
        dep.why = [dep0] + why

      a, b = ab._d
      (x, y), (m, n) = a._obj.points, b._obj.points

      added = []
      if not self.is_equal(ab, nd):
        if nd == self.halfpi:
          added += self.add_perp([x, y, m, n], dep)
        # else:
        name = 'aconst'
        args = [x, y, m, n, nd]
        dep1 = dep.populate(name, args)
        self.cache_dep(name, args, dep1)
        self.make_equal(nd, ab, deps=dep1)
        added += [dep1]

      if not self.is_equal(ba, dn):
        if dn == self.halfpi:
          added += self.add_perp([m, n, x, y], dep)
        name = 'aconst'
        args = [m, n, x, y, dn]
        dep2 = dep.populate(name, args)
        self.cache_dep(name, args, dep2)
        self.make_equal(dn, ba, deps=dep2)
        added += [dep2]
      return added

    if name == 'rconst':
      a, b, c, d, num, den, dep = args
      return self.add_eqrat_const([a, b, c, d, num, den], dep)

    if name == 'eqangle':
      d1, d2, d3, d4, dep = args
      a, b = d1._obj.points
      c, d = d2._obj.points
      e, f = d3._obj.points
      g, h = d4._obj.points

      return self.add_eqangle([a, b, c, d, e, f, g, h], dep)

    if name == 'eqratio':
      d1, d2, d3, d4, dep = args
      a, b = d1._obj.points
      c, d = d2._obj.points
      e, f = d3._obj.points
      g, h = d4._obj.points

      return self.add_eqratio([a, b, c, d, e, f, g, h], dep)

    if name in ['cong', 'cong2']:
      a, b, c, d, dep = args
      if not (a != b and c != d and (a != c or b != d)):
        return []
      return self.add_cong([a, b, c, d], dep)

    return []

  def derive_algebra(
      self, level: int, verbose: bool = False
  ) -> tuple[
      dict[str, list[tuple[Point, ...]]], dict[str, [tuple[Point, ...]]]
  ]:
    """Derive new algebraic predicates."""
    derives = {}
    ang_derives = self.derive_angle_algebra(level, verbose=verbose)
    dist_derives = self.derive_distance_algebra(level, verbose=verbose)
    rat_derives = self.derive_ratio_algebra(level, verbose=verbose)

    derives.update(ang_derives)
    derives.update(dist_derives)
    derives.update(rat_derives)

    # Separate eqangle and eqratio derivations
    # As they are too numerous => slow down DD+AR.
    # & reserve them only for last effort.
    eqs = {'eqangle': derives.pop('eqangle'), 'eqratio': derives.pop('eqratio')}
    return derives, eqs

  def derive_ratio_algebra(
      self, level: int, verbose: bool = False
  ) -> dict[str, list[tuple[Point, ...]]]:
    """Derive new eqratio predicates."""
    added = {'cong2': [], 'eqratio': []}

    for x in self.rtable.get_all_eqs_and_why():
      x, why = x[:-1], x[-1]
      dep = EmptyDependency(level=level, rule_name='a01')
      dep.why = why

      if len(x) == 2:
        a, b = x
        if gm.is_equiv(a, b):
          continue

        (m, n), (p, q) = a._obj.points, b._obj.points
        added['cong2'].append((m, n, p, q, dep))

      if len(x) == 4:
        a, b, c, d = x
        added['eqratio'].append((a, b, c, d, dep))

    return added

  def derive_angle_algebra(
      self, level: int, verbose: bool = False
  ) -> dict[str, list[tuple[Point, ...]]]:
    """Derive new eqangles predicates."""
    added = {'eqangle': [], 'aconst': [], 'para': []}

    for x in self.atable.get_all_eqs_and_why():
      x, why = x[:-1], x[-1]
      dep = EmptyDependency(level=level, rule_name='a02')
      dep.why = why

      if len(x) == 2:
        a, b = x
        if gm.is_equiv(a, b):
          continue

        (e, f), (p, q) = a._obj.points, b._obj.points
        if not nm.check('para', [e, f, p, q]):
          continue

        added['para'].append((a, b, dep))

      if len(x) == 3:
        a, b, (n, d) = x

        (e, f), (p, q) = a._obj.points, b._obj.points
        if not nm.check('aconst', [e, f, p, q, n, d]):
          continue

        added['aconst'].append((a, b, n, d, dep))

      if len(x) == 4:
        a, b, c, d = x
        added['eqangle'].append((a, b, c, d, dep))

    return added

  def derive_distance_algebra(
      self, level: int, verbose: bool = False
  ) -> dict[str, list[tuple[Point, ...]]]:
    """Derive new cong predicates."""
    added = {'inci': [], 'cong': [], 'rconst': []}
    for x in self.dtable.get_all_eqs_and_why():
      x, why = x[:-1], x[-1]
      dep = EmptyDependency(level=level, rule_name='a00')
      dep.why = why

      if len(x) == 2:
        a, b = x
        if a == b:
          continue

        dep.name = f'inci {a.name} {b.name}'
        added['inci'].append((x, dep))

      if len(x) == 4:
        a, b, c, d = x
        if not (a != b and c != d and (a != c or b != d)):
          continue
        added['cong'].append((a, b, c, d, dep))

      if len(x) == 6:
        a, b, c, d, num, den = x
        if not (a != b and c != d and (a != c or b != d)):
          continue
        added['rconst'].append((a, b, c, d, num, den, dep))

    return added

  @classmethod
  def build_problem(
      cls,
      pr: problem.Problem,
      definitions: dict[str, problem.Definition],
      verbose: bool = True,
      init_copy: bool = True,
  ) -> tuple[Graph, list[Dependency]]:
    """Build a problem into a gr.Graph object."""
    check = False
    g = None
    added = None
    if verbose:
      logging.info(pr.url)
      logging.info(pr.txt())
    while not check:
      try:
        g = Graph()
        added = []
        plevel = 0
        for clause in pr.clauses:
          adds, plevel = g.add_clause(
              clause, plevel, definitions, verbose=verbose
          )
          added += adds
        g.plevel = plevel

      except (nm.InvalidLineIntersectError, nm.InvalidQuadSolveError):
        continue
      except DepCheckFailError:
        continue
      except (PointTooCloseError, PointTooFarError):
        continue

      if not pr.goal:
        break

      args = list(map(lambda x: g.get(x, lambda: int(x)), pr.goal.args))
      check = nm.check(pr.goal.name, args)

    g.url = pr.url
    g.build_def = (pr, definitions)
    for add in added:
      g.add_algebra(add, level=0)

    return g, added

  def all_points(self) -> list[Point]:
    """Return all nodes of type Point."""
    return list(self.type2nodes[Point])

  def all_nodes(self) -> list[gm.Node]:
    """Return all nodes."""
    return list(self._name2node.values())

  def add_points(self, pnames: list[str]) -> list[Point]:
    """Add new points with given names in list pnames."""
    result = [self.new_node(Point, name) for name in pnames]
    self._name2point.update(zip(pnames, result))
    return result

  def names2nodes(self, pnames: list[str]) -> list[gm.Node]:
    return [self._name2node[name] for name in pnames]

  def names2points(
      self, pnames: list[str], create_new_point: bool = False
  ) -> list[Point]:
    """Return Point objects given names."""
    result = []
    for name in pnames:
      if name not in self._name2node and not create_new_point:
        raise ValueError(f'Cannot find point {name} in graph')
      elif name in self._name2node:
        obj = self._name2node[name]
      else:
        obj = self.new_node(Point, name)
      result.append(obj)

    return result

  def names2points_or_int(self, pnames: list[str]) -> list[Point]:
    """Return Point objects given names."""
    result = []
    for name in pnames:
      if name.isdigit():
        result += [int(name)]
      elif 'pi/' in name:
        n, d = name.split('pi/')
        ang, _ = self.get_or_create_const_ang(int(n), int(d))
        result += [ang]
      elif '/' in name:
        n, d = name.split('/')
        rat, _ = self.get_or_create_const_rat(int(n), int(d))
        result += [rat]
      else:
        result += [self._name2point[name]]

    return result

  def get(self, pointname: str, default_fn: Callable[str, Point]) -> Point:
    if pointname in self._name2point:
      return self._name2point[pointname]
    if pointname in self._name2node:
      return self._name2node[pointname]
    return default_fn()

  def new_node(self, oftype: Type[gm.Node], name: str = '') -> gm.Node:
    node = oftype(name, self)

    self.type2nodes[oftype].append(node)
    self._name2node[name] = node

    if isinstance(node, Point):
      self._name2point[name] = node

    return node

  def merge(self, nodes: list[gm.Node], deps: Dependency) -> gm.Node:
    """Merge all nodes."""
    if len(nodes) < 2:
      return

    node0, *nodes1 = nodes
    all_nodes = self.type2nodes[type(node0)]

    # find node0 that exists in all_nodes to be the rep
    # and merge all other nodes into node0
    for node in nodes:
      if node in all_nodes:
        node0 = node
        nodes1 = [n for n in nodes if n != node0]
        break
    return self.merge_into(node0, nodes1, deps)

  def merge_into(
      self, node0: gm.Node, nodes1: list[gm.Node], deps: Dependency
  ) -> gm.Node:
    """Merge nodes1 into a single node0."""
    node0.merge(nodes1, deps)
    for n in nodes1:
      if n.rep() != n:
        self.remove([n])

    nodes = [node0] + nodes1
    if any([node._val for node in nodes]):
      for node in nodes:
        self.connect_val(node, deps=None)

      vals1 = [n._val for n in nodes1]
      node0._val.merge(vals1, deps)

      for v in vals1:
        if v.rep() != v:
          self.remove([v])

    return node0

  def remove(self, nodes: list[gm.Node]) -> None:
    """Remove nodes out of self because they are merged."""
    if not nodes:
      return

    for node in nodes:
      all_nodes = self.type2nodes[type(nodes[0])]

      if node in all_nodes:
        all_nodes.remove(node)

      if node.name in self._name2node.values():
        self._name2node.pop(node.name)

  def connect(self, a: gm.Node, b: gm.Node, deps: Dependency) -> None:
    a.connect_to(b, deps)
    b.connect_to(a, deps)

  def connect_val(self, node: gm.Node, deps: Dependency) -> gm.Node:
    """Connect a node into its value (equality) node."""
    if node._val:
      return node._val
    name = None
    if isinstance(node, Line):
      name = 'd(' + node.name + ')'
    if isinstance(node, Angle):
      name = 'm(' + node.name + ')'
    if isinstance(node, Segment):
      name = 'l(' + node.name + ')'
    if isinstance(node, Ratio):
      name = 'r(' + node.name + ')'
    v = self.new_node(gm.val_type(node), name)
    self.connect(node, v, deps=deps)
    return v

  def is_equal(self, x: gm.Node, y: gm.Node, level: int = None) -> bool:
    return gm.is_equal(x, y, level)

  def add_piece(
      self, name: str, args: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add a new predicate."""
    if name in ['coll', 'collx']:
      return self.add_coll(args, deps)
    elif name == 'para':
      return self.add_para(args, deps)
    elif name == 'perp':
      return self.add_perp(args, deps)
    elif name == 'midp':
      return self.add_midp(args, deps)
    elif name == 'cong':
      return self.add_cong(args, deps)
    elif name == 'circle':
      return self.add_circle(args, deps)
    elif name == 'cyclic':
      return self.add_cyclic(args, deps)
    elif name in ['eqangle', 'eqangle6']:
      return self.add_eqangle(args, deps)
    elif name in ['eqratio', 'eqratio6']:
      return self.add_eqratio(args, deps)
    # numerical!
    elif name == 's_angle':
      return self.add_s_angle(args, deps)
    elif name == 'aconst':
      a, b, c, d, ang = args

      if isinstance(ang, str):
        name = ang
      else:
        name = ang.name

      num, den = name.split('pi/')
      num, den = int(num), int(den)
      return self.add_aconst([a, b, c, d, num, den], deps)
    elif name == 's_angle':
      b, x, a, b, ang = (  # pylint: disable=redeclared-assigned-name,unused-variable
          args
      )

      if isinstance(ang, str):
        name = ang
      else:
        name = ang.name

      n, d = name.split('pi/')
      ang = int(n) * 180 / int(d)
      return self.add_s_angle([a, b, x, ang], deps)
    elif name == 'rconst':
      a, b, c, d, rat = args

      if isinstance(rat, str):
        name = rat
      else:
        name = rat.name

      num, den = name.split('/')
      num, den = int(num), int(den)
      return self.add_eqrat_const([a, b, c, d, num, den], deps)

    # composite pieces:
    elif name == 'cong2':
      return self.add_cong2(args, deps)
    elif name == 'eqratio3':
      return self.add_eqratio3(args, deps)
    elif name == 'eqratio4':
      return self.add_eqratio4(args, deps)
    elif name == 'simtri':
      return self.add_simtri(args, deps)
    elif name == 'contri':
      return self.add_contri(args, deps)
    elif name == 'simtri2':
      return self.add_simtri2(args, deps)
    elif name == 'contri2':
      return self.add_contri2(args, deps)
    elif name == 'simtri*':
      return self.add_simtri_check(args, deps)
    elif name == 'contri*':
      return self.add_contri_check(args, deps)
    elif name in ['acompute', 'rcompute']:
      dep = deps.populate(name, args)
      self.cache_dep(name, args, dep)
      return [dep]
    elif name in ['fixl', 'fixc', 'fixb', 'fixt', 'fixp']:
      dep = deps.populate(name, args)
      self.cache_dep(name, args, dep)
      return [dep]
    elif name in ['ind']:
      return []
    raise ValueError(f'Not recognize {name}')

  def check(self, name: str, args: list[Point]) -> bool:
    """Symbolically check if a predicate is True."""
    if name == 'ncoll':
      return self.check_ncoll(args)
    if name == 'npara':
      return self.check_npara(args)
    if name == 'nperp':
      return self.check_nperp(args)
    if name == 'midp':
      return self.check_midp(args)
    if name == 'cong':
      return self.check_cong(args)
    if name == 'perp':
      return self.check_perp(args)
    if name == 'para':
      return self.check_para(args)
    if name == 'coll':
      return self.check_coll(args)
    if name == 'cyclic':
      return self.check_cyclic(args)
    if name == 'circle':
      return self.check_circle(args)
    if name == 'aconst':
      return self.check_aconst(args)
    if name == 'rconst':
      return self.check_rconst(args)
    if name == 'acompute':
      return self.check_acompute(args)
    if name == 'rcompute':
      return self.check_rcompute(args)
    if name in ['eqangle', 'eqangle6']:
      if len(args) == 5:
        return self.check_aconst(args)
      return self.check_eqangle(args)
    if name in ['eqratio', 'eqratio6']:
      if len(args) == 5:
        return self.check_rconst(args)
      return self.check_eqratio(args)
    if name in ['simtri', 'simtri2', 'simtri*']:
      return self.check_simtri(args)
    if name in ['contri', 'contri2', 'contri*']:
      return self.check_contri(args)
    if name == 'sameside':
      return self.check_sameside(args)
    if name in 'diff':
      a, b = args
      return not a.num.close(b.num)
    if name in ['fixl', 'fixc', 'fixb', 'fixt', 'fixp']:
      return self.in_cache(name, args)
    if name in ['ind']:
      return True
    raise ValueError(f'Not recognize {name}')

  def get_lines_thru_all(self, *points: list[gm.Point]) -> list[Line]:
    line2count = defaultdict(lambda: 0)
    points = set(points)
    for p in points:
      for l in p.neighbors(Line):
        line2count[l] += 1
    return [l for l, count in line2count.items() if count == len(points)]

  def _get_line(self, a: Point, b: Point) -> Optional[Line]:
    linesa = a.neighbors(Line)
    for l in b.neighbors(Line):
      if l in linesa:
        return l
    return None

  def _get_line_all(self, a: Point, b: Point) -> Generator[Line, None, None]:
    linesa = a.neighbors(Line, do_rep=False)
    linesb = b.neighbors(Line, do_rep=False)
    for l in linesb:
      if l in linesa:
        yield l

  def _get_lines(self, *points: list[Point]) -> list[Line]:
    """Return all lines that connect to >= 2 points."""
    line2count = defaultdict(lambda: 0)
    for p in points:
      for l in p.neighbors(Line):
        line2count[l] += 1
    return [l for l, count in line2count.items() if count >= 2]

  def get_circle_thru_triplet(self, p1: Point, p2: Point, p3: Point) -> Circle:
    p1, p2, p3 = sorted([p1, p2, p3], key=lambda x: x.name)
    if (p1, p2, p3) in self._triplet2circle:
      return self._triplet2circle[(p1, p2, p3)]
    return self.get_new_circle_thru_triplet(p1, p2, p3)

  def get_new_circle_thru_triplet(
      self, p1: Point, p2: Point, p3: Point
  ) -> Circle:
    """Get a new Circle that goes thru three given Points."""
    p1, p2, p3 = sorted([p1, p2, p3], key=lambda x: x.name)
    name = p1.name.lower() + p2.name.lower() + p3.name.lower()
    circle = self.new_node(Circle, f'({name})')
    circle.num = nm.Circle(p1=p1.num, p2=p2.num, p3=p3.num)
    circle.points = p1, p2, p3

    self.connect(p1, circle, deps=None)
    self.connect(p2, circle, deps=None)
    self.connect(p3, circle, deps=None)
    self._triplet2circle[(p1, p2, p3)] = circle
    return circle

  def get_line_thru_pair(self, p1: Point, p2: Point) -> Line:
    if (p1, p2) in self._pair2line:
      return self._pair2line[(p1, p2)]
    if (p2, p1) in self._pair2line:
      return self._pair2line[(p2, p1)]
    return self.get_new_line_thru_pair(p1, p2)

  def get_new_line_thru_pair(self, p1: Point, p2: Point) -> Line:
    if p1.name.lower() > p2.name.lower():
      p1, p2 = p2, p1
    name = p1.name.lower() + p2.name.lower()
    line = self.new_node(Line, name)
    line.num = nm.Line(p1.num, p2.num)
    line.points = p1, p2

    self.connect(p1, line, deps=None)
    self.connect(p2, line, deps=None)
    self._pair2line[(p1, p2)] = line
    return line

  def get_line_thru_pair_why(
      self, p1: Point, p2: Point
  ) -> tuple[Line, list[Dependency]]:
    """Get one line thru two given points and the corresponding dependency list."""
    if p1.name.lower() > p2.name.lower():
      p1, p2 = p2, p1
    if (p1, p2) in self._pair2line:
      return self._pair2line[(p1, p2)].rep_and_why()

    l, why = gm.line_of_and_why([p1, p2])
    if l is None:
      l = self.get_new_line_thru_pair(p1, p2)
      why = []
    return l, why

  def coll_dep(self, points: list[Point], p: Point) -> list[Dependency]:
    """Return the dep(.why) explaining why p is coll with points."""
    for p1, p2 in utils.comb2(points):
      if self.check_coll([p1, p2, p]):
        dep = Dependency('coll', [p1, p2, p], None, None)
        return dep.why_me_or_cache(self, None)

  def add_coll(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add a predicate that `points` are collinear."""
    points = list(set(points))
    og_points = list(points)

    all_lines = []
    for p1, p2 in utils.comb2(points):
      all_lines.append(self.get_line_thru_pair(p1, p2))
    points = sum([l.neighbors(Point) for l in all_lines], [])
    points = list(set(points))

    existed = set()
    new = set()
    for p1, p2 in utils.comb2(points):
      if p1.name > p2.name:
        p1, p2 = p2, p1
      if (p1, p2) in self._pair2line:
        line = self._pair2line[(p1, p2)]
        existed.add(line)
      else:
        line = self.get_new_line_thru_pair(p1, p2)
        new.add(line)

    existed = sorted(existed, key=lambda l: l.name)
    new = sorted(new, key=lambda l: l.name)

    existed, new = list(existed), list(new)
    if not existed:
      line0, *lines = new
    else:
      line0, lines = existed[0], existed[1:] + new

    add = []
    line0, why0 = line0.rep_and_why()
    a, b = line0.points
    for line in lines:
      c, d = line.points
      args = list({a, b, c, d})
      if len(args) < 3:
        continue

      whys = []
      for x in args:
        if x not in og_points:
          whys.append(self.coll_dep(og_points, x))

      abcd_deps = deps
      if whys + why0:
        dep0 = deps.populate('coll', og_points)
        abcd_deps = EmptyDependency(level=deps.level, rule_name=None)
        abcd_deps.why = [dep0] + whys

      is_coll = self.check_coll(args)
      dep = abcd_deps.populate('coll', args)
      self.cache_dep('coll', args, dep)
      self.merge_into(line0, [line], dep)

      if not is_coll:
        add += [dep]

    return add

  def check_coll(self, points: list[Point]) -> bool:
    points = list(set(points))
    if len(points) < 3:
      return True
    line2count = defaultdict(lambda: 0)
    for p in points:
      for l in p.neighbors(Line):
        line2count[l] += 1
    return any([count == len(points) for _, count in line2count.items()])

  def why_coll(self, args: tuple[Line, list[Point]]) -> list[Dependency]:
    line, points = args
    return line.why_coll(points)

  def check_ncoll(self, points: list[Point]) -> bool:
    if self.check_coll(points):
      return False
    return not nm.check_coll([p.num for p in points])

  def check_sameside(self, points: list[Point]) -> bool:
    return nm.check_sameside([p.num for p in points])

  def make_equal(self, x: gm.Node, y: gm.Node, deps: Dependency) -> None:
    """Make that two nodes x and y are equal, i.e. merge their value node."""
    if x.val is None:
      x, y = y, x

    self.connect_val(x, deps=None)
    self.connect_val(y, deps=None)
    vx = x._val
    vy = y._val

    if vx == vy:
      return

    merges = [vx, vy]

    if (
        isinstance(x, Angle)
        and x not in self.aconst.values()
        and y not in self.aconst.values()
        and x.directions == y.directions[::-1]
        and x.directions[0] != x.directions[1]
    ):
      merges = [self.vhalfpi, vx, vy]

    self.merge(merges, deps)

  def merge_vals(self, vx: gm.Node, vy: gm.Node, deps: Dependency) -> None:
    if vx == vy:
      return
    merges = [vx, vy]
    self.merge(merges, deps)

  def why_equal(self, x: gm.Node, y: gm.Node, level: int) -> list[Dependency]:
    return gm.why_equal(x, y, level)

  def _why_coll4(
      self,
      a: Point,
      b: Point,
      ab: Line,
      c: Point,
      d: Point,
      cd: Line,
      level: int,
  ) -> list[Dependency]:
    return self._why_coll2(a, b, ab, level) + self._why_coll2(c, d, cd, level)

  def _why_coll8(
      self,
      a: Point,
      b: Point,
      ab: Line,
      c: Point,
      d: Point,
      cd: Line,
      m: Point,
      n: Point,
      mn: Line,
      p: Point,
      q: Point,
      pq: Line,
      level: int,
  ) -> list[Dependency]:
    """Dependency list of why 8 points are collinear."""
    why8 = self._why_coll4(a, b, ab, c, d, cd, level)
    why8 += self._why_coll4(m, n, mn, p, q, pq, level)
    return why8

  def add_para(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add a new predicate that 4 points (2 lines) are parallel."""
    a, b, c, d = points
    ab, why1 = self.get_line_thru_pair_why(a, b)
    cd, why2 = self.get_line_thru_pair_why(c, d)

    is_equal = self.is_equal(ab, cd)

    (a, b), (c, d) = ab.points, cd.points

    dep0 = deps.populate('para', points)
    deps = EmptyDependency(level=deps.level, rule_name=None)

    deps = deps.populate('para', [a, b, c, d])
    deps.why = [dep0] + why1 + why2

    self.make_equal(ab, cd, deps)
    deps.algebra = ab._val, cd._val

    self.cache_dep('para', [a, b, c, d], deps)
    if not is_equal:
      return [deps]
    return []

  def why_para(self, args: list[Point]) -> list[Dependency]:
    ab, cd, lvl = args
    return self.why_equal(ab, cd, lvl)

  def check_para_or_coll(self, points: list[Point]) -> bool:
    return self.check_para(points) or self.check_coll(points)

  def check_para(self, points: list[Point]) -> bool:
    a, b, c, d = points
    if (a == b) or (c == d):
      return False
    ab = self._get_line(a, b)
    cd = self._get_line(c, d)
    if not ab or not cd:
      return False

    return self.is_equal(ab, cd)

  def check_npara(self, points: list[Point]) -> bool:
    if self.check_para(points):
      return False
    return not nm.check_para([p.num for p in points])

  def _get_angle(
      self, d1: Direction, d2: Direction
  ) -> tuple[Angle, Optional[Angle]]:
    for a in self.type2nodes[Angle]:
      if a.directions == (d1, d2):
        return a, a.opposite
    return None, None

  def get_first_angle(
      self, l1: Line, l2: Line
  ) -> tuple[Angle, list[Dependency]]:
    """Get a first angle between line l1 and line l2."""
    d1, d2 = l1._val, l2._val

    d1s = d1.all_reps()
    d2s = d2.all_reps()

    found = d1.first_angle(d2s)
    if found is None:
      found = d2.first_angle(d1s)
      if found is None:
        return None, []
      ang, x2, x1 = found
      found = ang.opposite, x1, x2

    ang, x1, x2 = found
    return ang, d1.deps_upto(x1) + d2.deps_upto(x2)

  def _get_or_create_angle(
      self, l1: Line, l2: Line, deps: Dependency
  ) -> tuple[Angle, Angle, list[Dependency]]:
    return self.get_or_create_angle_d(l1._val, l2._val, deps)

  def get_or_create_angle_d(
      self, d1: Direction, d2: Direction, deps: Dependency
  ) -> tuple[Angle, Angle, list[Dependency]]:
    """Get or create an angle between two Direction d1 and d2."""
    for a in self.type2nodes[Angle]:
      if a.directions == (d1.rep(), d2.rep()):  # directions = _d.rep()
        d1_, d2_ = a._d
        why1 = d1.why_equal([d1_], None) + d1_.why_rep()
        why2 = d2.why_equal([d2_], None) + d2_.why_rep()
        return a, a.opposite, why1 + why2

    d1, why1 = d1.rep_and_why()
    d2, why2 = d2.rep_and_why()
    a12 = self.new_node(Angle, f'{d1.name}-{d2.name}')
    a21 = self.new_node(Angle, f'{d2.name}-{d1.name}')
    self.connect(d1, a12, deps)
    self.connect(d2, a21, deps)
    self.connect(a12, a21, deps)
    a12.set_directions(d1, d2)
    a21.set_directions(d2, d1)
    a12.opposite = a21
    a21.opposite = a12
    return a12, a21, why1 + why2

  def _add_para_or_coll(
      self,
      a: Point,
      b: Point,
      c: Point,
      d: Point,
      x: Point,
      y: Point,
      m: Point,
      n: Point,
      deps: EmptyDependency,
  ) -> list[Dependency]:
    """Add a new parallel or collinear predicate."""
    extends = [('perp', [x, y, m, n])]
    if {a, b} == {x, y}:
      pass
    elif self.check_para([a, b, x, y]):
      extends.append(('para', [a, b, x, y]))
    elif self.check_coll([a, b, x, y]):
      extends.append(('coll', set(list([a, b, x, y]))))
    else:
      return None

    if m in [c, d] or n in [c, d] or c in [m, n] or d in [m, n]:
      pass
    elif self.check_coll([c, d, m]):
      extends.append(('coll', [c, d, m]))
    elif self.check_coll([c, d, n]):
      extends.append(('coll', [c, d, n]))
    elif self.check_coll([c, m, n]):
      extends.append(('coll', [c, m, n]))
    elif self.check_coll([d, m, n]):
      extends.append(('coll', [d, m, n]))
    else:
      deps = deps.extend_many(self, 'perp', [a, b, c, d], extends)
      return self.add_para([c, d, m, n], deps)

    deps = deps.extend_many(self, 'perp', [a, b, c, d], extends)
    return self.add_coll(list(set([c, d, m, n])), deps)

  def maybe_make_para_from_perp(
      self, points: list[Point], deps: EmptyDependency
  ) -> Optional[list[Dependency]]:
    """Maybe add a new parallel predicate from perp predicate."""
    a, b, c, d = points
    halfpi = self.aconst[(1, 2)]
    for ang in halfpi.val.neighbors(Angle):
      if ang == halfpi:
        continue
      d1, d2 = ang.directions
      x, y = d1._obj.points
      m, n = d2._obj.points

      for args in [
          (a, b, c, d, x, y, m, n),
          (a, b, c, d, m, n, x, y),
          (c, d, a, b, x, y, m, n),
          (c, d, a, b, m, n, x, y),
      ]:
        args = args + (deps,)
        add = self._add_para_or_coll(*args)
        if add:
          return add

    return None

  def add_perp(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add a new perpendicular predicate from 4 points (2 lines)."""
    add = self.maybe_make_para_from_perp(points, deps)
    if add is not None:
      return add

    a, b, c, d = points
    ab, why1 = self.get_line_thru_pair_why(a, b)
    cd, why2 = self.get_line_thru_pair_why(c, d)

    (a, b), (c, d) = ab.points, cd.points

    if why1 + why2:
      dep0 = deps.populate('perp', points)
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why1 + why2

    self.connect_val(ab, deps=None)
    self.connect_val(cd, deps=None)

    if ab.val == cd.val:
      raise ValueError(f'{ab.name} and {cd.name} Cannot be perp.')

    args = [a, b, c, d]
    i = 0
    for x, y, xy in [(a, b, ab), (c, d, cd)]:
      i += 1
      x_, y_ = xy._val._obj.points
      if {x, y} == {x_, y_}:
        continue
      if deps:
        deps = deps.extend(self, 'perp', list(args), 'para', [x, y, x_, y_])
      args[2 * i - 2] = x_
      args[2 * i - 1] = y_

    a12, a21, why = self._get_or_create_angle(ab, cd, deps=None)

    if why:
      dep0 = deps.populate('perp', [a, b, c, d])
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why

    dab, dcd = a12._d
    a, b = dab._obj.points
    c, d = dcd._obj.points

    is_equal = self.is_equal(a12, a21)
    deps = deps.populate('perp', [a, b, c, d])
    deps.algebra = [dab, dcd]
    self.make_equal(a12, a21, deps=deps)

    self.cache_dep('perp', [a, b, c, d], deps)
    self.cache_dep('eqangle', [a, b, c, d, c, d, a, b], deps)

    if not is_equal:
      return [deps]
    return []

  def why_perp(
      self, args: list[Union[Point, list[Dependency]]]
  ) -> list[Dependency]:
    a, b, deps = args
    return deps + self.why_equal(a, b, None)

  def check_perpl(self, ab: Line, cd: Line) -> bool:
    if ab.val is None or cd.val is None:
      return False
    if ab.val == cd.val:
      return False
    a12, a21 = self._get_angle(ab.val, cd.val)
    if a12 is None or a21 is None:
      return False
    return self.is_equal(a12, a21)

  def check_perp(self, points: list[Point]) -> bool:
    a, b, c, d = points
    ab = self._get_line(a, b)
    cd = self._get_line(c, d)
    if not ab or not cd:
      return False
    return self.check_perpl(ab, cd)

  def check_nperp(self, points: list[Point]) -> bool:
    if self.check_perp(points):
      return False
    return not nm.check_perp([p.num for p in points])

  def _get_segment(self, p1: Point, p2: Point) -> Optional[Segment]:
    for s in self.type2nodes[Segment]:
      if s.points == {p1, p2}:
        return s
    return None

  def _get_or_create_segment(
      self, p1: Point, p2: Point, deps: Dependency
  ) -> Segment:
    """Get or create a Segment object between two Points p1 and p2."""
    if p1 == p2:
      raise ValueError(f'Creating same 0-length segment {p1.name}')

    for s in self.type2nodes[Segment]:
      if s.points == {p1, p2}:
        return s

    if p1.name > p2.name:
      p1, p2 = p2, p1
    s = self.new_node(Segment, name=f'{p1.name.upper()}{p2.name.upper()}')
    self.connect(p1, s, deps=deps)
    self.connect(p2, s, deps=deps)
    s.points = {p1, p2}
    return s

  def add_cong(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add that two segments (4 points) are congruent."""
    a, b, c, d = points
    ab = self._get_or_create_segment(a, b, deps=None)
    cd = self._get_or_create_segment(c, d, deps=None)

    is_equal = self.is_equal(ab, cd)

    dep = deps.populate('cong', [a, b, c, d])
    self.make_equal(ab, cd, deps=dep)
    dep.algebra = ab._val, cd._val

    self.cache_dep('cong', [a, b, c, d], dep)

    result = []

    if not is_equal:
      result += [dep]

    if a not in [c, d] and b not in [c, d]:
      return result

    if b in [c, d]:
      a, b = b, a
    if a == d:
      c, d = d, c  # pylint: disable=unused-variable

    result += self._maybe_add_cyclic_from_cong(a, b, d, dep)
    return result

  def _maybe_add_cyclic_from_cong(
      self, a: Point, b: Point, c: Point, cong_ab_ac: Dependency
  ) -> list[Dependency]:
    """Maybe add a new cyclic predicate from given congruent segments."""
    ab = self._get_or_create_segment(a, b, deps=None)

    # all eq segs with one end being a.
    segs = [s for s in ab.val.neighbors(Segment) if a in s.points]

    # all points on circle (a, b)
    points = []
    for s in segs:
      x, y = list(s.points)
      points.append(x if y == a else y)

    # for sure both b and c are in points
    points = [p for p in points if p not in [b, c]]

    if len(points) < 2:
      return []

    x, y = points[:2]

    if self.check_cyclic([b, c, x, y]):
      return []

    ax = self._get_or_create_segment(a, x, deps=None)
    ay = self._get_or_create_segment(a, y, deps=None)
    why = ab._val.why_equal([ax._val, ay._val], level=None)
    why += [cong_ab_ac]

    deps = EmptyDependency(cong_ab_ac.level, '')
    deps.why = why

    return self.add_cyclic([b, c, x, y], deps)

  def check_cong(self, points: list[Point]) -> bool:
    a, b, c, d = points
    if {a, b} == {c, d}:
      return True

    ab = self._get_segment(a, b)
    cd = self._get_segment(c, d)
    if ab is None or cd is None:
      return False
    return self.is_equal(ab, cd)

  def why_cong(self, args: tuple[Segment, Segment]) -> list[Dependency]:
    ab, cd = args
    return self.why_equal(ab, cd, None)

  def add_midp(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    m, a, b = points
    add = self.add_coll(points, deps=deps)
    add += self.add_cong([m, a, m, b], deps)
    return add

  def why_midp(
      self, args: tuple[Line, list[Point], Segment, Segment]
  ) -> list[Dependency]:
    line, points, ma, mb = args
    return self.why_coll([line, points]) + self.why_cong([ma, mb])

  def check_midp(self, points: list[Point]) -> bool:
    if not self.check_coll(points):
      return False
    m, a, b = points
    return self.check_cong([m, a, m, b])

  def add_circle(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    o, a, b, c = points
    add = self.add_cong([o, a, o, b], deps=deps)
    add += self.add_cong([o, a, o, c], deps=deps)
    return add

  def why_circle(
      self, args: tuple[Segment, Segment, Segment]
  ) -> list[Dependency]:
    oa, ob, oc = args
    return self.why_equal(oa, ob, None) and self.why_equal(oa, oc, None)

  def check_circle(self, points: list[Point]) -> bool:
    o, a, b, c = points
    return self.check_cong([o, a, o, b]) and self.check_cong([o, a, o, c])

  def get_circles_thru_all(self, *points: list[Point]) -> list[Circle]:
    circle2count = defaultdict(lambda: 0)
    points = set(points)
    for p in points:
      for c in p.neighbors(Circle):
        circle2count[c] += 1
    return [c for c, count in circle2count.items() if count == len(points)]

  def _get_circles(self, *points: list[Point]) -> list[Circle]:
    circle2count = defaultdict(lambda: 0)
    for p in points:
      for c in p.neighbors(Circle):
        circle2count[c] += 1
    return [c for c, count in circle2count.items() if count >= 3]

  def cyclic_dep(self, points: list[Point], p: Point) -> list[Dependency]:
    for p1, p2, p3 in utils.comb3(points):
      if self.check_cyclic([p1, p2, p3, p]):
        dep = Dependency('cyclic', [p1, p2, p3, p], None, None)
        return dep.why_me_or_cache(self, None)

  def add_cyclic(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add a new cyclic predicate that 4 points are concyclic."""
    points = list(set(points))
    og_points = list(points)

    all_circles = []
    for p1, p2, p3 in utils.comb3(points):
      all_circles.append(self.get_circle_thru_triplet(p1, p2, p3))
    points = sum([c.neighbors(Point) for c in all_circles], [])
    points = list(set(points))

    existed = set()
    new = set()
    for p1, p2, p3 in utils.comb3(points):
      p1, p2, p3 = sorted([p1, p2, p3], key=lambda x: x.name)

      if (p1, p2, p3) in self._triplet2circle:
        circle = self._triplet2circle[(p1, p2, p3)]
        existed.add(circle)
      else:
        circle = self.get_new_circle_thru_triplet(p1, p2, p3)
        new.add(circle)

    existed = sorted(existed, key=lambda l: l.name)
    new = sorted(new, key=lambda l: l.name)

    existed, new = list(existed), list(new)
    if not existed:
      circle0, *circles = new
    else:
      circle0, circles = existed[0], existed[1:] + new

    add = []
    circle0, why0 = circle0.rep_and_why()
    a, b, c = circle0.points
    for circle in circles:
      d, e, f = circle.points
      args = list({a, b, c, d, e, f})
      if len(args) < 4:
        continue
      whys = []
      for x in [a, b, c, d, e, f]:
        if x not in og_points:
          whys.append(self.cyclic_dep(og_points, x))
      abcdef_deps = deps
      if whys + why0:
        dep0 = deps.populate('cyclic', og_points)
        abcdef_deps = EmptyDependency(level=deps.level, rule_name=None)
        abcdef_deps.why = [dep0] + whys

      is_cyclic = self.check_cyclic(args)

      dep = abcdef_deps.populate('cyclic', args)
      self.cache_dep('cyclic', args, dep)
      self.merge_into(circle0, [circle], dep)
      if not is_cyclic:
        add += [dep]

    return add

  def check_cyclic(self, points: list[Point]) -> bool:
    points = list(set(points))
    if len(points) < 4:
      return True
    circle2count = defaultdict(lambda: 0)
    for p in points:
      for c in p.neighbors(Circle):
        circle2count[c] += 1
    return any([count == len(points) for _, count in circle2count.items()])

  def make_equal_pairs(
      self,
      a: Point,
      b: Point,
      c: Point,
      d: Point,
      m: Point,
      n: Point,
      p: Point,
      q: Point,
      ab: Line,
      cd: Line,
      mn: Line,
      pq: Line,
      deps: EmptyDependency,
  ) -> list[Dependency]:
    """Add ab/cd = mn/pq in case either two of (ab,cd,mn,pq) are equal."""
    depname = 'eqratio' if isinstance(ab, Segment) else 'eqangle'
    eqname = 'cong' if isinstance(ab, Segment) else 'para'

    is_equal = self.is_equal(mn, pq)

    if ab != cd:
      dep0 = deps.populate(depname, [a, b, c, d, m, n, p, q])
      deps = EmptyDependency(level=deps.level, rule_name=None)

      dep = Dependency(eqname, [a, b, c, d], None, deps.level)
      deps.why = [dep0, dep.why_me_or_cache(self, None)]

    elif eqname == 'para':  # ab == cd.
      colls = [a, b, c, d]
      if len(set(colls)) > 2:
        dep0 = deps.populate(depname, [a, b, c, d, m, n, p, q])
        deps = EmptyDependency(level=deps.level, rule_name=None)

        dep = Dependency('collx', colls, None, deps.level)
        deps.why = [dep0, dep.why_me_or_cache(self, None)]

    deps = deps.populate(eqname, [m, n, p, q])
    self.make_equal(mn, pq, deps=deps)

    deps.algebra = mn._val, pq._val
    self.cache_dep(eqname, [m, n, p, q], deps)

    if is_equal:
      return []
    return [deps]

  def maybe_make_equal_pairs(
      self,
      a: Point,
      b: Point,
      c: Point,
      d: Point,
      m: Point,
      n: Point,
      p: Point,
      q: Point,
      ab: Line,
      cd: Line,
      mn: Line,
      pq: Line,
      deps: EmptyDependency,
  ) -> Optional[list[Dependency]]:
    """Add ab/cd = mn/pq in case maybe either two of (ab,cd,mn,pq) are equal."""
    level = deps.level
    if self.is_equal(ab, cd, level):
      return self.make_equal_pairs(a, b, c, d, m, n, p, q, ab, cd, mn, pq, deps)
    elif self.is_equal(mn, pq, level):
      return self.make_equal_pairs(  # pylint: disable=arguments-out-of-order
          m,
          n,
          p,
          q,
          a,
          b,
          c,
          d,
          mn,
          pq,
          ab,
          cd,
          deps,
      )
    elif self.is_equal(ab, mn, level):
      return self.make_equal_pairs(  # pylint: disable=arguments-out-of-order
          a,
          b,
          m,
          n,
          c,
          d,
          p,
          q,
          ab,
          mn,
          cd,
          pq,
          deps,
      )
    elif self.is_equal(cd, pq, level):
      return self.make_equal_pairs(  # pylint: disable=arguments-out-of-order
          c,
          d,
          p,
          q,
          a,
          b,
          m,
          n,
          cd,
          pq,
          ab,
          mn,
          deps,
      )
    else:
      return None

  def _add_eqangle(
      self,
      a: Point,
      b: Point,
      c: Point,
      d: Point,
      m: Point,
      n: Point,
      p: Point,
      q: Point,
      ab: Line,
      cd: Line,
      mn: Line,
      pq: Line,
      deps: EmptyDependency,
  ) -> list[Dependency]:
    """Add eqangle core."""
    if deps:
      deps = deps.copy()

    args = [a, b, c, d, m, n, p, q]
    i = 0
    for x, y, xy in [(a, b, ab), (c, d, cd), (m, n, mn), (p, q, pq)]:
      i += 1
      x_, y_ = xy._val._obj.points
      if {x, y} == {x_, y_}:
        continue
      if deps:
        deps = deps.extend(self, 'eqangle', list(args), 'para', [x, y, x_, y_])

        args[2 * i - 2] = x_
        args[2 * i - 1] = y_

    add = []
    ab_cd, cd_ab, why1 = self._get_or_create_angle(ab, cd, deps=None)
    mn_pq, pq_mn, why2 = self._get_or_create_angle(mn, pq, deps=None)

    why = why1 + why2
    if why:
      dep0 = deps.populate('eqangle', args)
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why

    dab, dcd = ab_cd._d
    dmn, dpq = mn_pq._d

    a, b = dab._obj.points
    c, d = dcd._obj.points
    m, n = dmn._obj.points
    p, q = dpq._obj.points

    is_eq1 = self.is_equal(ab_cd, mn_pq)
    deps1 = None
    if deps:
      deps1 = deps.populate('eqangle', [a, b, c, d, m, n, p, q])
      deps1.algebra = [dab, dcd, dmn, dpq]
    if not is_eq1:
      add += [deps1]
    self.cache_dep('eqangle', [a, b, c, d, m, n, p, q], deps1)
    self.make_equal(ab_cd, mn_pq, deps=deps1)

    is_eq2 = self.is_equal(cd_ab, pq_mn)
    deps2 = None
    if deps:
      deps2 = deps.populate('eqangle', [c, d, a, b, p, q, m, n])
      deps2.algebra = [dcd, dab, dpq, dmn]
    if not is_eq2:
      add += [deps2]
    self.cache_dep('eqangle', [c, d, a, b, p, q, m, n], deps2)
    self.make_equal(cd_ab, pq_mn, deps=deps2)

    return add

  def add_eqangle(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add eqangle made by 8 points in `points`."""
    if deps:
      deps = deps.copy()
    a, b, c, d, m, n, p, q = points
    ab, why1 = self.get_line_thru_pair_why(a, b)
    cd, why2 = self.get_line_thru_pair_why(c, d)
    mn, why3 = self.get_line_thru_pair_why(m, n)
    pq, why4 = self.get_line_thru_pair_why(p, q)

    a, b = ab.points
    c, d = cd.points
    m, n = mn.points
    p, q = pq.points

    if deps and why1 + why2 + why3 + why4:
      dep0 = deps.populate('eqangle', points)
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why1 + why2 + why3 + why4

    add = self.maybe_make_equal_pairs(
        a, b, c, d, m, n, p, q, ab, cd, mn, pq, deps
    )

    if add is not None:
      return add

    self.connect_val(ab, deps=None)
    self.connect_val(cd, deps=None)
    self.connect_val(mn, deps=None)
    self.connect_val(pq, deps=None)

    add = []
    if (
        ab.val != cd.val
        and mn.val != pq.val
        and (ab.val != mn.val or cd.val != pq.val)
    ):
      add += self._add_eqangle(a, b, c, d, m, n, p, q, ab, cd, mn, pq, deps)

    if (
        ab.val != mn.val
        and cd.val != pq.val
        and (ab.val != cd.val or mn.val != pq.val)
    ):
      add += self._add_eqangle(  # pylint: disable=arguments-out-of-order
          a,
          b,
          m,
          n,
          c,
          d,
          p,
          q,
          ab,
          mn,
          cd,
          pq,
          deps,
      )

    return add

  def add_aconst(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add that an angle is equal to some constant."""
    a, b, c, d, num, den = points
    nd, dn = self.get_or_create_const_ang(num, den)

    if nd == self.halfpi:
      return self.add_perp([a, b, c, d], deps)

    ab, why1 = self.get_line_thru_pair_why(a, b)
    cd, why2 = self.get_line_thru_pair_why(c, d)

    (a, b), (c, d) = ab.points, cd.points
    if why1 + why2:
      args = points[:-2] + [nd]
      dep0 = deps.populate('aconst', args)
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why1 + why2

    self.connect_val(ab, deps=None)
    self.connect_val(cd, deps=None)

    if ab.val == cd.val:
      raise ValueError(f'{ab.name} - {cd.name} cannot be {nd.name}')

    args = [a, b, c, d, nd]
    i = 0
    for x, y, xy in [(a, b, ab), (c, d, cd)]:
      i += 1
      x_, y_ = xy._val._obj.points
      if {x, y} == {x_, y_}:
        continue
      if deps:
        deps = deps.extend(self, 'aconst', list(args), 'para', [x, y, x_, y_])
      args[2 * i - 2] = x_
      args[2 * i - 1] = y_

    ab_cd, cd_ab, why = self._get_or_create_angle(ab, cd, deps=None)
    if why:
      dep0 = deps.populate('aconst', [a, b, c, d, nd])
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why

    dab, dcd = ab_cd._d
    a, b = dab._obj.points
    c, d = dcd._obj.points

    ang = int(num) * 180 / int(den)
    add = []
    if not self.is_equal(ab_cd, nd):
      deps1 = deps.populate('aconst', [a, b, c, d, nd])
      deps1.algebra = dab, dcd, ang % 180
      self.make_equal(ab_cd, nd, deps=deps1)
      self.cache_dep('aconst', [a, b, c, d, nd], deps1)
      add += [deps1]

    if not self.is_equal(cd_ab, dn):
      deps2 = deps.populate('aconst', [c, d, a, b, dn])
      deps2.algebra = dcd, dab, 180 - ang % 180
      self.make_equal(cd_ab, dn, deps=deps2)
      self.cache_dep('aconst', [c, d, a, b, dn], deps2)
      add += [deps2]
    return add

  def add_s_angle(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add that an angle abx is equal to constant y."""
    a, b, x, y = points

    n, d = ar.simplify(y % 180, 180)
    nd, dn = self.get_or_create_const_ang(n, d)

    if nd == self.halfpi:
      return self.add_perp([a, b, b, x], deps)

    ab, why1 = self.get_line_thru_pair_why(a, b)
    bx, why2 = self.get_line_thru_pair_why(b, x)

    self.connect_val(ab, deps=None)
    self.connect_val(bx, deps=None)
    add = []

    if ab.val == bx.val:
      return add

    deps.why += why1 + why2

    for p, q, pq in [(a, b, ab), (b, x, bx)]:
      p_, q_ = pq.val._obj.points
      if {p, q} == {p_, q_}:
        continue
      dep = Dependency('para', [p, q, p_, q_], None, deps.level)
      deps.why += [dep.why_me_or_cache(self, None)]

    xba, abx, why = self._get_or_create_angle(bx, ab, deps=None)
    if why:
      dep0 = deps.populate('aconst', [b, x, a, b, nd])
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why

    dab, dbx = abx._d
    a, b = dab._obj.points
    c, x = dbx._obj.points

    if not self.is_equal(xba, nd):
      deps1 = deps.populate('aconst', [c, x, a, b, nd])
      deps1.algebra = dbx, dab, y % 180

      self.make_equal(xba, nd, deps=deps1)
      self.cache_dep('aconst', [c, x, a, b, nd], deps1)
      add += [deps1]

    if not self.is_equal(abx, dn):
      deps2 = deps.populate('aconst', [a, b, c, x, dn])
      deps2.algebra = dab, dbx, 180 - (y % 180)

      self.make_equal(abx, dn, deps=deps2)
      self.cache_dep('s_angle', [a, b, c, x, dn], deps2)
      add += [deps2]
    return add

  def check_aconst(self, points: list[Point], verbose: bool = False) -> bool:
    """Check if the angle is equal to a certain constant."""
    a, b, c, d, nd = points
    _ = verbose
    if isinstance(nd, str):
      name = nd
    else:
      name = nd.name
    num, den = name.split('pi/')
    ang, _ = self.get_or_create_const_ang(int(num), int(den))

    ab = self._get_line(a, b)
    cd = self._get_line(c, d)
    if not ab or not cd:
      return False

    if not (ab.val and cd.val):
      return False

    for ang1, _, _ in gm.all_angles(ab._val, cd._val):
      if self.is_equal(ang1, ang):
        return True
    return False

  def check_acompute(self, points: list[Point]) -> bool:
    """Check if an angle has a constant value."""
    a, b, c, d = points
    ab = self._get_line(a, b)
    cd = self._get_line(c, d)
    if not ab or not cd:
      return False

    if not (ab.val and cd.val):
      return False

    for ang0 in self.aconst.values():
      for ang in ang0.val.neighbors(Angle):
        d1, d2 = ang.directions
        if ab.val == d1 and cd.val == d2:
          return True
    return False

  def check_eqangle(self, points: list[Point]) -> bool:
    """Check if two angles are equal."""
    a, b, c, d, m, n, p, q = points

    if {a, b} == {c, d} and {m, n} == {p, q}:
      return True
    if {a, b} == {m, n} and {c, d} == {p, q}:
      return True

    if (a == b) or (c == d) or (m == n) or (p == q):
      return False
    ab = self._get_line(a, b)
    cd = self._get_line(c, d)
    mn = self._get_line(m, n)
    pq = self._get_line(p, q)

    if {a, b} == {c, d} and mn and pq and self.is_equal(mn, pq):
      return True
    if {a, b} == {m, n} and cd and pq and self.is_equal(cd, pq):
      return True
    if {p, q} == {m, n} and ab and cd and self.is_equal(ab, cd):
      return True
    if {p, q} == {c, d} and ab and mn and self.is_equal(ab, mn):
      return True

    if not ab or not cd or not mn or not pq:
      return False

    if self.is_equal(ab, cd) and self.is_equal(mn, pq):
      return True
    if self.is_equal(ab, mn) and self.is_equal(cd, pq):
      return True

    if not (ab.val and cd.val and mn.val and pq.val):
      return False

    if (ab.val, cd.val) == (mn.val, pq.val) or (ab.val, mn.val) == (
        cd.val,
        pq.val,
    ):
      return True

    for ang1, _, _ in gm.all_angles(ab._val, cd._val):
      for ang2, _, _ in gm.all_angles(mn._val, pq._val):
        if self.is_equal(ang1, ang2):
          return True

    if self.check_perp([a, b, m, n]) and self.check_perp([c, d, p, q]):
      return True
    if self.check_perp([a, b, p, q]) and self.check_perp([c, d, m, n]):
      return True

    return False

  def _get_ratio(self, l1: Length, l2: Length) -> tuple[Ratio, Ratio]:
    for r in self.type2nodes[Ratio]:
      if r.lengths == (l1, l2):
        return r, r.opposite
    return None, None

  def _get_or_create_ratio(
      self, s1: Segment, s2: Segment, deps: Dependency
  ) -> tuple[Ratio, Ratio, list[Dependency]]:
    return self._get_or_create_ratio_l(s1._val, s2._val, deps)

  def _get_or_create_ratio_l(
      self, l1: Length, l2: Length, deps: Dependency
  ) -> tuple[Ratio, Ratio, list[Dependency]]:
    """Get or create a new Ratio from two Lenghts l1 and l2."""
    for r in self.type2nodes[Ratio]:
      if r.lengths == (l1.rep(), l2.rep()):
        l1_, l2_ = r._l
        why1 = l1.why_equal([l1_], None) + l1_.why_rep()
        why2 = l2.why_equal([l2_], None) + l2_.why_rep()
        return r, r.opposite, why1 + why2

    l1, why1 = l1.rep_and_why()
    l2, why2 = l2.rep_and_why()
    r12 = self.new_node(Ratio, f'{l1.name}/{l2.name}')
    r21 = self.new_node(Ratio, f'{l2.name}/{l1.name}')
    self.connect(l1, r12, deps)
    self.connect(l2, r21, deps)
    self.connect(r12, r21, deps)
    r12.set_lengths(l1, l2)
    r21.set_lengths(l2, l1)
    r12.opposite = r21
    r21.opposite = r12
    return r12, r21, why1 + why2

  def add_cong2(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    m, n, a, b = points
    add = []
    add += self.add_cong([m, a, n, a], deps)
    add += self.add_cong([m, b, n, b], deps)
    return add

  def add_eqratio3(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add three eqratios through a list of 6 points (due to parallel lines)."""
    a, b, c, d, m, n = points
    #   a -- b
    #  m  --  n
    # c   --   d
    add = []
    add += self.add_eqratio([m, a, m, c, n, b, n, d], deps)
    add += self.add_eqratio([a, m, a, c, b, n, b, d], deps)
    add += self.add_eqratio([c, m, c, a, d, n, d, b], deps)
    if m == n:
      add += self.add_eqratio([m, a, m, c, a, b, c, d], deps)
    return add

  def add_eqratio4(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    o, a, b, c, d = points
    #   o
    #  a b
    # c   d
    add = self.add_eqratio3([a, b, c, d, o, o], deps)
    add += self.add_eqratio([o, a, o, c, a, b, c, d], deps)
    return add

  def _add_eqratio(
      self,
      a: Point,
      b: Point,
      c: Point,
      d: Point,
      m: Point,
      n: Point,
      p: Point,
      q: Point,
      ab: Segment,
      cd: Segment,
      mn: Segment,
      pq: Segment,
      deps: EmptyDependency,
  ) -> list[Dependency]:
    """Add a new eqratio from 8 points (core)."""
    if deps:
      deps = deps.copy()

    args = [a, b, c, d, m, n, p, q]
    i = 0
    for x, y, xy in [(a, b, ab), (c, d, cd), (m, n, mn), (p, q, pq)]:
      if {x, y} == set(xy.points):
        continue
      x_, y_ = list(xy.points)
      if deps:
        deps = deps.extend(self, 'eqratio', list(args), 'cong', [x, y, x_, y_])
      args[2 * i - 2] = x_
      args[2 * i - 1] = y_

    add = []
    ab_cd, cd_ab, why1 = self._get_or_create_ratio(ab, cd, deps=None)
    mn_pq, pq_mn, why2 = self._get_or_create_ratio(mn, pq, deps=None)

    why = why1 + why2
    if why:
      dep0 = deps.populate('eqratio', args)
      deps = EmptyDependency(level=deps.level, rule_name=None)
      deps.why = [dep0] + why

    lab, lcd = ab_cd._l
    lmn, lpq = mn_pq._l

    a, b = lab._obj.points
    c, d = lcd._obj.points
    m, n = lmn._obj.points
    p, q = lpq._obj.points

    is_eq1 = self.is_equal(ab_cd, mn_pq)
    deps1 = None
    if deps:
      deps1 = deps.populate('eqratio', [a, b, c, d, m, n, p, q])
      deps1.algebra = [ab._val, cd._val, mn._val, pq._val]
    if not is_eq1:
      add += [deps1]
    self.cache_dep('eqratio', [a, b, c, d, m, n, p, q], deps1)
    self.make_equal(ab_cd, mn_pq, deps=deps1)

    is_eq2 = self.is_equal(cd_ab, pq_mn)
    deps2 = None
    if deps:
      deps2 = deps.populate('eqratio', [c, d, a, b, p, q, m, n])
      deps2.algebra = [cd._val, ab._val, pq._val, mn._val]
    if not is_eq2:
      add += [deps2]
    self.cache_dep('eqratio', [c, d, a, b, p, q, m, n], deps2)
    self.make_equal(cd_ab, pq_mn, deps=deps2)
    return add

  def add_eqratio(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add a new eqratio from 8 points."""
    if deps:
      deps = deps.copy()
    a, b, c, d, m, n, p, q = points
    ab = self._get_or_create_segment(a, b, deps=None)
    cd = self._get_or_create_segment(c, d, deps=None)
    mn = self._get_or_create_segment(m, n, deps=None)
    pq = self._get_or_create_segment(p, q, deps=None)

    add = self.maybe_make_equal_pairs(
        a, b, c, d, m, n, p, q, ab, cd, mn, pq, deps
    )

    if add is not None:
      return add

    self.connect_val(ab, deps=None)
    self.connect_val(cd, deps=None)
    self.connect_val(mn, deps=None)
    self.connect_val(pq, deps=None)

    add = []
    if (
        ab.val != cd.val
        and mn.val != pq.val
        and (ab.val != mn.val or cd.val != pq.val)
    ):
      add += self._add_eqratio(a, b, c, d, m, n, p, q, ab, cd, mn, pq, deps)

    if (
        ab.val != mn.val
        and cd.val != pq.val
        and (ab.val != cd.val or mn.val != pq.val)
    ):
      add += self._add_eqratio(  # pylint: disable=arguments-out-of-order
          a,
          b,
          m,
          n,
          c,
          d,
          p,
          q,
          ab,
          mn,
          cd,
          pq,
          deps,
      )
    return add

  def check_rconst(self, points: list[Point], verbose: bool = False) -> bool:
    """Check whether a ratio is equal to some given constant."""
    _ = verbose
    a, b, c, d, nd = points
    if isinstance(nd, str):
      name = nd
    else:
      name = nd.name
    num, den = name.split('/')
    rat, _ = self.get_or_create_const_rat(int(num), int(den))

    ab = self._get_segment(a, b)
    cd = self._get_segment(c, d)

    if not ab or not cd:
      return False

    if not (ab.val and cd.val):
      return False

    for rat1, _, _ in gm.all_ratios(ab._val, cd._val):
      if self.is_equal(rat1, rat):
        return True
    return False

  def check_rcompute(self, points: list[Point]) -> bool:
    """Check whether a ratio is equal to some constant."""
    a, b, c, d = points
    ab = self._get_segment(a, b)
    cd = self._get_segment(c, d)

    if not ab or not cd:
      return False

    if not (ab.val and cd.val):
      return False

    for rat0 in self.rconst.values():
      for rat in rat0.val.neighbors(Ratio):
        l1, l2 = rat.lengths
        if ab.val == l1 and cd.val == l2:
          return True
    return False

  def check_eqratio(self, points: list[Point]) -> bool:
    """Check if 8 points make an eqratio predicate."""
    a, b, c, d, m, n, p, q = points

    if {a, b} == {c, d} and {m, n} == {p, q}:
      return True
    if {a, b} == {m, n} and {c, d} == {p, q}:
      return True

    ab = self._get_segment(a, b)
    cd = self._get_segment(c, d)
    mn = self._get_segment(m, n)
    pq = self._get_segment(p, q)

    if {a, b} == {c, d} and mn and pq and self.is_equal(mn, pq):
      return True
    if {a, b} == {m, n} and cd and pq and self.is_equal(cd, pq):
      return True
    if {p, q} == {m, n} and ab and cd and self.is_equal(ab, cd):
      return True
    if {p, q} == {c, d} and ab and mn and self.is_equal(ab, mn):
      return True

    if not ab or not cd or not mn or not pq:
      return False

    if self.is_equal(ab, cd) and self.is_equal(mn, pq):
      return True
    if self.is_equal(ab, mn) and self.is_equal(cd, pq):
      return True

    if not (ab.val and cd.val and mn.val and pq.val):
      return False

    if (ab.val, cd.val) == (mn.val, pq.val) or (ab.val, mn.val) == (
        cd.val,
        pq.val,
    ):
      return True

    for rat1, _, _ in gm.all_ratios(ab._val, cd._val):
      for rat2, _, _ in gm.all_ratios(mn._val, pq._val):
        if self.is_equal(rat1, rat2):
          return True
    return False

  def add_simtri_check(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    if nm.same_clock(*[p.num for p in points]):
      return self.add_simtri(points, deps)
    return self.add_simtri2(points, deps)

  def add_contri_check(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    if nm.same_clock(*[p.num for p in points]):
      return self.add_contri(points, deps)
    return self.add_contri2(points, deps)

  def enum_sides(
      self, points: list[Point]
  ) -> Generator[list[Point], None, None]:
    a, b, c, x, y, z = points
    yield [a, b, x, y]
    yield [b, c, y, z]
    yield [c, a, z, x]

  def enum_triangle(
      self, points: list[Point]
  ) -> Generator[list[Point], None, None]:
    a, b, c, x, y, z = points
    yield [a, b, a, c, x, y, x, z]
    yield [b, a, b, c, y, x, y, z]
    yield [c, a, c, b, z, x, z, y]

  def enum_triangle2(
      self, points: list[Point]
  ) -> Generator[list[Point], None, None]:
    a, b, c, x, y, z = points
    yield [a, b, a, c, x, z, x, y]
    yield [b, a, b, c, y, z, y, x]
    yield [c, a, c, b, z, y, z, x]

  def add_simtri(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add two similar triangles."""
    add = []
    hashs = [d.hashed() for d in deps.why]

    for args in self.enum_triangle(points):
      if problem.hashed('eqangle6', args) in hashs:
        continue
      add += self.add_eqangle(args, deps=deps)

    for args in self.enum_triangle(points):
      if problem.hashed('eqratio6', args) in hashs:
        continue
      add += self.add_eqratio(args, deps=deps)

    return add

  def check_simtri(self, points: list[Point]) -> bool:
    a, b, c, x, y, z = points
    return self.check_eqangle([a, b, a, c, x, y, x, z]) and self.check_eqangle(
        [b, a, b, c, y, x, y, z]
    )

  def add_simtri2(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add two similar reflected triangles."""
    add = []
    hashs = [d.hashed() for d in deps.why]
    for args in self.enum_triangle2(points):
      if problem.hashed('eqangle6', args) in hashs:
        continue
      add += self.add_eqangle(args, deps=deps)

    for args in self.enum_triangle(points):
      if problem.hashed('eqratio6', args) in hashs:
        continue
      add += self.add_eqratio(args, deps=deps)

    return add

  def add_contri(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add two congruent triangles."""
    add = []
    hashs = [d.hashed() for d in deps.why]
    for args in self.enum_triangle(points):
      if problem.hashed('eqangle6', args) in hashs:
        continue
      add += self.add_eqangle(args, deps=deps)

    for args in self.enum_sides(points):
      if problem.hashed('cong', args) in hashs:
        continue
      add += self.add_cong(args, deps=deps)
    return add

  def check_contri(self, points: list[Point]) -> bool:
    a, b, c, x, y, z = points
    return (
        self.check_cong([a, b, x, y])
        and self.check_cong([b, c, y, z])
        and self.check_cong([c, a, z, x])
    )

  def add_contri2(
      self, points: list[Point], deps: EmptyDependency
  ) -> list[Dependency]:
    """Add two congruent reflected triangles."""
    add = []
    hashs = [d.hashed() for d in deps.why]
    for args in self.enum_triangle2(points):
      if problem.hashed('eqangle6', args) in hashs:
        continue
      add += self.add_eqangle(args, deps=deps)

    for args in self.enum_sides(points):
      if problem.hashed('cong', args) in hashs:
        continue
      add += self.add_cong(args, deps=deps)

    return add

  def in_cache(self, name: str, args: list[Point]) -> bool:
    return problem.hashed(name, args) in self.cache

  def cache_dep(
      self, name: str, args: list[Point], premises: list[Dependency]
  ) -> None:
    hashed = problem.hashed(name, args)
    if hashed in self.cache:
      return
    self.cache[hashed] = premises

  def all_same_line(
      self, a: Point, b: Point
  ) -> Generator[tuple[Point, Point], None, None]:
    ab = self._get_line(a, b)
    if ab is None:
      return
    for p1, p2 in utils.comb2(ab.neighbors(Point)):
      if {p1, p2} != {a, b}:
        yield p1, p2

  def all_same_angle(
      self, a: Point, b: Point, c: Point, d: Point
  ) -> Generator[tuple[Point, Point, Point, Point], None, None]:
    for x, y in self.all_same_line(a, b):
      for m, n in self.all_same_line(c, d):
        yield x, y, m, n

  def additionally_draw(self, name: str, args: list[Point]) -> None:
    """Draw some extra line/circles for illustration purpose."""

    if name in ['circle']:
      center, point = args[:2]
      circle = self.new_node(Circle, f'({center.name},{point.name})')
      circle.num = nm.Circle(center.num, p1=point.num)
      circle.points = center, point

    if name in ['on_circle', 'tangent']:
      center, point = args[-2:]
      circle = self.new_node(Circle, f'({center.name},{point.name})')
      circle.num = nm.Circle(center.num, p1=point.num)
      circle.points = center, point

    if name in ['incenter', 'excenter', 'incenter2', 'excenter2']:
      d, a, b, c = [x for x in args[-4:]]
      a, b, c = sorted([a, b, c], key=lambda x: x.name.lower())
      circle = self.new_node(Circle, f'({d.name},h.{a.name}{b.name})')
      p = d.num.foot(nm.Line(a.num, b.num))
      circle.num = nm.Circle(d.num, p1=p)
      circle.points = d, a, b, c

    if name in ['cc_tangent']:
      o, a, w, b = args[-4:]
      c1 = self.new_node(Circle, f'({o.name},{a.name})')
      c1.num = nm.Circle(o.num, p1=a.num)
      c1.points = o, a

      c2 = self.new_node(Circle, f'({w.name},{b.name})')
      c2.num = nm.Circle(w.num, p1=b.num)
      c2.points = w, b

    if name in ['ninepoints']:
      a, b, c = args[-3:]
      a, b, c = sorted([a, b, c], key=lambda x: x.name.lower())
      circle = self.new_node(Circle, f'(,m.{a.name}{b.name}{c.name})')
      p1 = (b.num + c.num) * 0.5
      p2 = (c.num + a.num) * 0.5
      p3 = (a.num + b.num) * 0.5
      circle.num = nm.Circle(p1=p1, p2=p2, p3=p3)
      circle.points = (None, None, a, b, c)

    if name in ['2l1c']:
      a, b, c, o = args[:4]
      a, b, c = sorted([a, b, c], key=lambda x: x.name.lower())
      circle = self.new_node(Circle, f'({o.name},{a.name}{b.name}{c.name})')
      circle.num = nm.Circle(p1=a.num, p2=b.num, p3=c.num)
      circle.points = (a, b, c)

  def add_clause(
      self,
      clause: problem.Clause,
      plevel: int,
      definitions: dict[str, problem.Definition],
      verbose: int = False,
  ) -> tuple[list[Dependency], int]:
    """Add a new clause of construction, e.g. a new excenter."""
    existing_points = self.all_points()
    new_points = [Point(name) for name in clause.points]

    new_points_dep_points = set()
    new_points_dep = []

    # Step 1: check for all deps.
    for c in clause.constructions:
      cdef = definitions[c.name]

      if len(cdef.construction.args) != len(c.args):
        if len(cdef.construction.args) - len(c.args) == len(clause.points):
          c.args = clause.points + c.args
        else:
          correct_form = ' '.join(cdef.points + ['=', c.name] + cdef.args)
          raise ValueError('Argument mismatch. ' + correct_form)

      mapping = dict(zip(cdef.construction.args, c.args))
      c_name = 'midp' if c.name == 'midpoint' else c.name
      deps = EmptyDependency(level=0, rule_name=problem.CONSTRUCTION_RULE)
      deps.construction = Dependency(c_name, c.args, rule_name=None, level=0)

      for d in cdef.deps.constructions:
        args = self.names2points([mapping[a] for a in d.args])
        new_points_dep_points.update(args)
        if not self.check(d.name, args):
          raise DepCheckFailError(
              d.name + ' ' + ' '.join([x.name for x in args])
          )
        deps.why += [
            Dependency(
                d.name, args, rule_name=problem.CONSTRUCTION_RULE, level=0
            )
        ]

      new_points_dep += [deps]

    # Step 2: draw.
    def range_fn() -> (
        list[Union[nm.Point, nm.Line, nm.Circle, nm.HalfLine, nm.HoleCircle]]
    ):
      to_be_intersected = []
      for c in clause.constructions:
        cdef = definitions[c.name]
        mapping = dict(zip(cdef.construction.args, c.args))
        for n in cdef.numerics:
          args = [mapping[a] for a in n.args]
          args = list(map(lambda x: self.get(x, lambda: int(x)), args))
          to_be_intersected += nm.sketch(n.name, args)

      return to_be_intersected

    is_total_free = (
        len(clause.constructions) == 1 and clause.constructions[0].name in FREE
    )
    is_semi_free = (
        len(clause.constructions) == 1
        and clause.constructions[0].name in INTERSECT
    )

    existing_points = [p.num for p in existing_points]

    def draw_fn() -> list[nm.Point]:
      to_be_intersected = range_fn()
      return nm.reduce(to_be_intersected, existing_points)

    rely_on = set()
    for c in clause.constructions:
      cdef = definitions[c.name]
      mapping = dict(zip(cdef.construction.args, c.args))
      for n in cdef.numerics:
        args = [mapping[a] for a in n.args]
        args = list(map(lambda x: self.get(x, lambda: int(x)), args))
        rely_on.update([a for a in args if isinstance(a, Point)])

    for p in rely_on:
      p.change.update(new_points)

    nums = draw_fn()
    for p, num, num0 in zip(new_points, nums, clause.nums):
      p.co_change = new_points
      if isinstance(num0, nm.Point):
        num = num0
      elif isinstance(num0, (tuple, list)):
        x, y = num0
        num = nm.Point(x, y)

      p.num = num

    # check two things.
    if nm.check_too_close(nums, existing_points):
      raise PointTooCloseError()
    if nm.check_too_far(nums, existing_points):
      raise PointTooFarError()

    # Commit: now that all conditions are passed.
    # add these points to current graph.
    for p in new_points:
      self._name2point[p.name] = p
      self._name2node[p.name] = p
      self.type2nodes[Point].append(p)

    for p in new_points:
      p.why = sum([d.why for d in new_points_dep], [])  # to generate txt logs.
      p.group = new_points
      p.dep_points = new_points_dep_points
      p.dep_points.update(new_points)
      p.plevel = plevel

    # movement dependency:
    rely_dict_0 = defaultdict(lambda: [])

    for c in clause.constructions:
      cdef = definitions[c.name]
      mapping = dict(zip(cdef.construction.args, c.args))
      for p, ps in cdef.rely.items():
        p = mapping[p]
        ps = [mapping[x] for x in ps]
        rely_dict_0[p].append(ps)

    rely_dict = {}
    for p, pss in rely_dict_0.items():
      ps = sum(pss, [])
      if len(pss) > 1:
        ps = [x for x in ps if x != p]

      p = self._name2point[p]
      ps = self.names2nodes(ps)
      rely_dict[p] = ps

    for p in new_points:
      p.rely_on = set(rely_dict.get(p, []))
      for x in p.rely_on:
        if not hasattr(x, 'base_rely_on'):
          x.base_rely_on = set()
      p.base_rely_on = set.union(*[x.base_rely_on for x in p.rely_on] + [set()])
      if is_total_free or is_semi_free:
        p.rely_on.add(p)
        p.base_rely_on.add(p)

    plevel_done = set()
    added = []
    basics = []
    # Step 3: build the basics.
    for c, deps in zip(clause.constructions, new_points_dep):
      cdef = definitions[c.name]
      mapping = dict(zip(cdef.construction.args, c.args))

      # not necessary for proofing, but for visualization.
      c_args = list(map(lambda x: self.get(x, lambda: int(x)), c.args))
      self.additionally_draw(c.name, c_args)

      for points, bs in cdef.basics:
        if points:
          points = self.names2nodes([mapping[p] for p in points])
          points = [p for p in points if p not in plevel_done]
          for p in points:
            p.plevel = plevel
          plevel_done.update(points)
          plevel += 1
        else:
          continue

        for b in bs:
          if b.name != 'rconst':
            args = [mapping[a] for a in b.args]
          else:
            num, den = map(int, b.args[-2:])
            rat, _ = self.get_or_create_const_rat(num, den)
            args = [mapping[a] for a in b.args[:-2]] + [rat.name]

          args = list(map(lambda x: self.get(x, lambda: int(x)), args))

          adds = self.add_piece(name=b.name, args=args, deps=deps)
          basics.append((b.name, args, deps))
          if adds:
            added += adds
            for add in adds:
              self.cache_dep(add.name, add.args, add)

    assert len(plevel_done) == len(new_points)
    for p in new_points:
      p.basics = basics

    return added, plevel

  def all_eqangle_same_lines(self) -> Generator[tuple[Point, ...], None, None]:
    for l1, l2 in utils.perm2(self.type2nodes[Line]):
      for a, b, c, d, e, f, g, h in utils.all_8points(l1, l2, l1, l2):
        if (a, b, c, d) != (e, f, g, h):
          yield a, b, c, d, e, f, g, h

  def all_eqangles_distinct_linepairss(
      self,
  ) -> Generator[tuple[Line, ...], None, None]:
    """No eqangles betcause para-para, or para-corresponding, or same."""

    for measure in self.type2nodes[Measure]:
      angs = measure.neighbors(Angle)
      line_pairss = []
      for ang in angs:
        d1, d2 = ang.directions
        if d1 is None or d2 is None:
          continue
        l1s = d1.neighbors(Line)
        l2s = d2.neighbors(Line)
        # Any pair in this is para-para.
        para_para = list(utils.cross(l1s, l2s))
        line_pairss.append(para_para)

      for pairs1, pairs2 in utils.comb2(line_pairss):
        for pair1, pair2 in utils.cross(pairs1, pairs2):
          (l1, l2), (l3, l4) = pair1, pair2
          yield l1, l2, l3, l4

  def all_eqangles_8points(self) -> Generator[tuple[Point, ...], None, None]:
    """List all sets of 8 points that make two equal angles."""
    # Case 1: (l1-l2) = (l3-l4), including because l1//l3, l2//l4 (para-para)
    angss = []
    for measure in self.type2nodes[Measure]:
      angs = measure.neighbors(Angle)
      angss.append(angs)

    # include the angs that do not have any measure.
    angss.extend([[ang] for ang in self.type2nodes[Angle] if ang.val is None])

    line_pairss = []
    for angs in angss:
      line_pairs = set()
      for ang in angs:
        d1, d2 = ang.directions
        if d1 is None or d2 is None:
          continue
        l1s = d1.neighbors(Line)
        l2s = d2.neighbors(Line)
        line_pairs.update(set(utils.cross(l1s, l2s)))
      line_pairss.append(line_pairs)

    # include (d1, d2) in which d1 does not have any angles.
    noang_ds = [d for d in self.type2nodes[Direction] if not d.neighbors(Angle)]

    for d1 in noang_ds:
      for d2 in self.type2nodes[Direction]:
        if d1 == d2:
          continue
        l1s = d1.neighbors(Line)
        l2s = d2.neighbors(Line)
        if len(l1s) < 2 and len(l2s) < 2:
          continue
        line_pairss.append(set(utils.cross(l1s, l2s)))
        line_pairss.append(set(utils.cross(l2s, l1s)))

    # Case 2: d1 // d2 => (d1-d3) = (d2-d3)
    # include lines that does not have any direction.
    nodir_ls = [l for l in self.type2nodes[Line] if l.val is None]

    for line in nodir_ls:
      for d in self.type2nodes[Direction]:
        l1s = d.neighbors(Line)
        if len(l1s) < 2:
          continue
        l2s = [line]
        line_pairss.append(set(utils.cross(l1s, l2s)))
        line_pairss.append(set(utils.cross(l2s, l1s)))

    record = set()
    for line_pairs in line_pairss:
      for pair1, pair2 in utils.perm2(list(line_pairs)):
        (l1, l2), (l3, l4) = pair1, pair2
        if l1 == l2 or l3 == l4:
          continue
        if (l1, l2) == (l3, l4):
          continue
        if (l1, l2, l3, l4) in record:
          continue
        record.add((l1, l2, l3, l4))
        for a, b, c, d, e, f, g, h in utils.all_8points(l1, l2, l3, l4):
          yield (a, b, c, d, e, f, g, h)

    for a, b, c, d, e, f, g, h in self.all_eqangle_same_lines():
      yield a, b, c, d, e, f, g, h

  def all_eqangles_6points(self) -> Generator[tuple[Point, ...], None, None]:
    """List all sets of 6 points that make two equal angles."""
    record = set()
    for a, b, c, d, e, f, g, h in self.all_eqangles_8points():
      if (
          a not in (c, d)
          and b not in (c, d)
          or e not in (g, h)
          and f not in (g, h)
      ):
        continue

      if b in (c, d):
        a, b = b, a  # now a in c, d
      if f in (g, h):
        e, f = f, e  # now e in g, h
      if a == d:
        c, d = d, c  # now a == c
      if e == h:
        g, h = h, g  # now e == g
      if (a, b, c, d, e, f, g, h) in record:
        continue
      record.add((a, b, c, d, e, f, g, h))
      yield a, b, c, d, e, f, g, h  # where a==c, e==g

  def all_paras(self) -> Generator[tuple[Point, ...], None, None]:
    for d in self.type2nodes[Direction]:
      for l1, l2 in utils.perm2(d.neighbors(Line)):
        for a, b, c, d in utils.all_4points(l1, l2):
          yield a, b, c, d

  def all_perps(self) -> Generator[tuple[Point, ...], None, None]:
    for ang in self.vhalfpi.neighbors(Angle):
      d1, d2 = ang.directions
      if d1 is None or d2 is None:
        continue
      if d1 == d2:
        continue
      for l1, l2 in utils.cross(d1.neighbors(Line), d2.neighbors(Line)):
        for a, b, c, d in utils.all_4points(l1, l2):
          yield a, b, c, d

  def all_congs(self) -> Generator[tuple[Point, ...], None, None]:
    for l in self.type2nodes[Length]:
      for s1, s2 in utils.perm2(l.neighbors(Segment)):
        (a, b), (c, d) = s1.points, s2.points
        for x, y in [(a, b), (b, a)]:
          for m, n in [(c, d), (d, c)]:
            yield x, y, m, n

  def all_eqratios_8points(self) -> Generator[tuple[Point, ...], None, None]:
    """List all sets of 8 points that make two equal ratios."""
    ratss = []
    for value in self.type2nodes[Value]:
      rats = value.neighbors(Ratio)
      ratss.append(rats)

    # include the rats that do not have any val.
    ratss.extend([[rat] for rat in self.type2nodes[Ratio] if rat.val is None])

    seg_pairss = []
    for rats in ratss:
      seg_pairs = set()
      for rat in rats:
        l1, l2 = rat.lengths
        if l1 is None or l2 is None:
          continue
        s1s = l1.neighbors(Segment)
        s2s = l2.neighbors(Segment)
        seg_pairs.update(utils.cross(s1s, s2s))
      seg_pairss.append(seg_pairs)

    # include (l1, l2) in which l1 does not have any ratio.
    norat_ls = [l for l in self.type2nodes[Length] if not l.neighbors(Ratio)]

    for l1 in norat_ls:
      for l2 in self.type2nodes[Length]:
        if l1 == l2:
          continue
        s1s = l1.neighbors(Segment)
        s2s = l2.neighbors(Segment)
        if len(s1s) < 2 and len(s2s) < 2:
          continue
        seg_pairss.append(set(utils.cross(s1s, s2s)))
        seg_pairss.append(set(utils.cross(s2s, s1s)))

    # include Seg that does not have any Length.
    nolen_ss = [s for s in self.type2nodes[Segment] if s.val is None]

    for seg in nolen_ss:
      for l in self.type2nodes[Length]:
        s1s = l.neighbors(Segment)
        if len(s1s) == 1:
          continue
        s2s = [seg]
        seg_pairss.append(set(utils.cross(s1s, s2s)))
        seg_pairss.append(set(utils.cross(s2s, s1s)))

    record = set()
    for seg_pairs in seg_pairss:
      for pair1, pair2 in utils.perm2(list(seg_pairs)):
        (s1, s2), (s3, s4) = pair1, pair2
        if s1 == s2 or s3 == s4:
          continue
        if (s1, s2) == (s3, s4):
          continue
        if (s1, s2, s3, s4) in record:
          continue
        record.add((s1, s2, s3, s4))
        a, b = s1.points
        c, d = s2.points
        e, f = s3.points
        g, h = s4.points

        for x, y in [(a, b), (b, a)]:
          for z, t in [(c, d), (d, c)]:
            for m, n in [(e, f), (f, e)]:
              for p, q in [(g, h), (h, g)]:
                yield (x, y, z, t, m, n, p, q)

    segss = []
    # finally the list of ratios that is equal to 1.0
    for length in self.type2nodes[Length]:
      segs = length.neighbors(Segment)
      segss.append(segs)

    segs_pair = list(utils.perm2(list(segss)))
    segs_pair += list(zip(segss, segss))
    for segs1, segs2 in segs_pair:
      for s1, s2 in utils.perm2(list(segs1)):
        for s3, s4 in utils.perm2(list(segs2)):
          if (s1, s2) == (s3, s4) or (s1, s3) == (s2, s4):
            continue
          if (s1, s2, s3, s4) in record:
            continue
          record.add((s1, s2, s3, s4))
          a, b = s1.points
          c, d = s2.points
          e, f = s3.points
          g, h = s4.points

          for x, y in [(a, b), (b, a)]:
            for z, t in [(c, d), (d, c)]:
              for m, n in [(e, f), (f, e)]:
                for p, q in [(g, h), (h, g)]:
                  yield (x, y, z, t, m, n, p, q)

  def all_eqratios_6points(self) -> Generator[tuple[Point, ...], None, None]:
    """List all sets of 6 points that make two equal angles."""
    record = set()
    for a, b, c, d, e, f, g, h in self.all_eqratios_8points():
      if (
          a not in (c, d)
          and b not in (c, d)
          or e not in (g, h)
          and f not in (g, h)
      ):
        continue
      if b in (c, d):
        a, b = b, a
      if f in (g, h):
        e, f = f, e
      if a == d:
        c, d = d, c
      if e == h:
        g, h = h, g
      if (a, b, c, d, e, f, g, h) in record:
        continue
      record.add((a, b, c, d, e, f, g, h))
      yield a, b, c, d, e, f, g, h  # now a==c, e==g

  def all_cyclics(self) -> Generator[tuple[Point, ...], None, None]:
    for c in self.type2nodes[Circle]:
      for x, y, z, t in utils.perm4(c.neighbors(Point)):
        yield x, y, z, t

  def all_colls(self) -> Generator[tuple[Point, ...], None, None]:
    for l in self.type2nodes[Line]:
      for x, y, z in utils.perm3(l.neighbors(Point)):
        yield x, y, z

  def all_midps(self) -> Generator[tuple[Point, ...], None, None]:
    for l in self.type2nodes[Line]:
      for a, b, c in utils.perm3(l.neighbors(Point)):
        if self.check_cong([a, b, a, c]):
          yield a, b, c

  def all_circles(self) -> Generator[tuple[Point, ...], None, None]:
    for l in self.type2nodes[Length]:
      p2p = defaultdict(list)
      for s in l.neighbors(Segment):
        a, b = s.points
        p2p[a].append(b)
        p2p[b].append(a)
      for p, ps in p2p.items():
        if len(ps) >= 3:
          for a, b, c in utils.perm3(ps):
            yield p, a, b, c

  def two_points_on_direction(self, d: Direction) -> tuple[Point, Point]:
    l = d.neighbors(Line)[0]
    p1, p2 = l.neighbors(Point)[:2]
    return p1, p2

  def two_points_of_length(self, l: Length) -> tuple[Point, Point]:
    s = l.neighbors(Segment)[0]
    p1, p2 = s.points
    return p1, p2


def create_consts_str(g: Graph, s: str) -> Union[Ratio, Angle]:
  if 'pi/' in s:
    n, d = s.split('pi/')
    n, d = int(n), int(d)
    p0, _ = g.get_or_create_const_ang(n, d)
  else:
    n, d = s.split('/')
    n, d = int(n), int(d)
    p0, _ = g.get_or_create_const_rat(n, d)
  return p0


def create_consts(g: Graph, p: gm.Node) -> Union[Ratio, Angle]:
  if isinstance(p, Angle):
    n, d = p.name.split('pi/')
    n, d = int(n), int(d)
    p0, _ = g.get_or_create_const_ang(n, d)
  if isinstance(p, Ratio):
    n, d = p.name.split('/')
    n, d = int(n), int(d)
    p0, _ = g.get_or_create_const_rat(n, d)
  return p0  # pylint: disable=undefined-variable