Before30

.gitignore

@@ -22,3 +22,5 @@ share/python-wheels/
 .installed.cfg
 *.egg
 MANIFEST
+ag_ckpt_vocab/
+meliad_lib/

CACHEDIR.TAG

@@ -0,0 +1,4 @@
+Signature: 8a477f597d28d172789f06886806bc55
+# This file is a cache directory tag created by Python virtualenv.
+# For information about cache directory tags, see:
+#   https://bford.info/cachedir/

alphageometry.py

@@ -29,7 +29,6 @@
 import pretty as pt
 import problem as pr
 
-
 _GIN_SEARCH_PATHS = flags.DEFINE_list(
     'gin_search_paths',
     ['third_party/py/meliad/transformer/configs'],
@@ -174,6 +173,20 @@ def write_solution(g: gh.Graph, p: pr.Problem, out_file: str) -> None:
       'r38': '(Similar Triangles)',
       'r39': '(Similar Triangles)',
       'r40': '(Congruent Triangles)',
+      'r43': '(Menelaus)',
+      'r44': '(Menelaus)',
+      'r45': '(Ceva)',
+      'r46': '(Ceva)',
+      'r47': '(Circle Power)',
+      'r48': '(Circle Power)',
+      'r49': '(Circle Power)',
+      'r50': '(Circle Power)',
+      'r51': '(Radical Axis)',
+      'r52': '(Pascal)',
+      'r53': '(Pascal)',
+      'r54': '(Pascal)',
+      'r55': '(Pascal)',
+      'r56': '(Pascal)',
       'a00': '(Distance chase)',
       'a01': '(Ratio chase)',
       'a02': '(Angle chase)',
@@ -189,6 +202,7 @@ def write_solution(g: gh.Graph, p: pr.Problem, out_file: str) -> None:
 
   solution += '==========================\n'
   logging.info(solution)
+  print(solution)
   if out_file:
     with open(out_file, 'w') as f:
       f.write(solution)
@@ -380,7 +394,8 @@ def try_translate_constrained_to_construct(string: str, g: gh.Graph) -> str:
   """
   if string[-1] != ';':
     return 'ERROR: must end with ;'
-
+  if ':' not in string:
+    return 'ERROR: must contain :'
   head, prem_str = string.split(' : ')
   point = head.strip()
 
@@ -571,7 +586,7 @@ def run_alphageometry(
 
         # Update the constructive statement of the problem with the aux point:
         candidate_pstring = insert_aux_to_premise(pstring, translation)
-
+        print(candidate_pstring)
         logging.info('Solving: "%s"', candidate_pstring)
         p_new = pr.Problem.from_txt(candidate_pstring)
 
@@ -604,7 +619,6 @@ def run_alphageometry(
 def main(_):
   global DEFINITIONS
   global RULES
-
   # definitions of terms used in our domain-specific language.
   DEFINITIONS = pr.Definition.from_txt_file(_DEFS_FILE.value, to_dict=True)
   # load inference rules used in DD.
@@ -649,3 +663,4 @@ def main(_):
 
 if __name__ == '__main__':
   app.run(main)
+

ar.py

@@ -17,7 +17,7 @@
 
 from collections import defaultdict  # pylint: disable=g-importing-member
 from fractions import Fraction as frac  # pylint: disable=g-importing-member
-from typing import Any, Generator
+from typing import Any, Generator, Union
 
 import geometry as gm
 import numpy as np
@@ -219,9 +219,16 @@ def update_groups(
   Returns:
     groups1, links, history: result of the update.
   """
+  print("len1",len(groups1))
+  print("len2",len(groups2))
+  cnt = 0
+  lenall = len(groups2)
   history = []
   links = []
   for g2 in groups2:
+    cnt += 1
+    if cnt % 1000 == 0:
+      print(f'{cnt}/{lenall}')
     joins = [None] * len(groups1)  # mark which one in groups1 is merged
     merged_g1 = set()  # merge them into this.
     old = None  # any elem in g2 that belong to any set in groups1 (old)
@@ -265,8 +272,7 @@ def update_groups(
       new_groups1 += [set(new)]
 
     groups1 = new_groups1
-    history.append(groups1)
-
+    #history.append(groups1)
   return groups1, links, history
 
 
@@ -363,7 +369,7 @@ def register(self, vc: list[tuple[str, float]], dep: pr.Dependency) -> None:
   def register2(
       self, a: str, b: str, m: float, n: float, dep: pr.Dependency
   ) -> None:
-    self.register([(a, m), (b, -n)], dep)
+    self.register([(a, n), (b, -m)], dep)
 
   def register3(self, a: str, b: str, f: float, dep: pr.Dependency) -> None:
     self.register([(a, 1), (b, -1), (self.const, -f)], dep)
@@ -373,6 +379,11 @@ def register4(
   ) -> None:
     self.register([(a, 1), (b, -1), (c, -1), (d, 1)], dep)
 
+  def register5(
+      self, a: str, b: str, c: str, dep: pr.Dependency
+  ) -> None:
+    self.register([(a, 1), (b, -1), (c, -1)], dep)
+
   def why(self, e: dict[str, float]) -> list[Any]:
     """AR traceback == MILP."""
     if not self.do_why:
@@ -401,7 +412,7 @@ def why(self, e: dict[str, float]) -> list[Any]:
     deps = []
     for i, dep in enumerate(self.deps):
       if x[2 * i] > 1e-12 or x[2 * i + 1] > 1e-12:
-        if dep not in deps:
+        if dep is not None and dep not in deps:
           deps.append(dep)
     return deps
 
@@ -426,7 +437,7 @@ def add_eq2(
       self, a: str, b: str, m: float, n: float, dep: pr.Dependency
   ) -> None:
     # a/b = m/n
-    if not self.add_expr([(a, m), (b, -n)]):
+    if not self.add_expr([(a, n), (b, -m)]):
       return []
     self.register2(a, b, m, n, dep)
 
@@ -455,10 +466,32 @@ def add_eq4(self, a: str, b: str, c: str, d: str, dep: pr.Dependency) -> None:
         self.groups, [{(a, b), (c, d)}, {(b, a), (d, c)}]
     )
 
+
+  def add_eq5(self, a: str, b: str, c: str, dep: pr.Dependency) -> None:
+    # a = b + c
+    self.eqs.add((a, b, c))
+    self.eqs.add((a, c, b))
+
+    expr = list(minus({a: 1, b: -1}, {c: 1}).items())
+
+    if not self.add_expr(expr):
+      return []
+
+    self.register5(a, b, c, dep)
+
   def pairs(self) -> Generator[list[tuple[str, str]], None, None]:
     for v1, v2 in perm2(list(self.v2e.keys())):  # pylint: disable=g-builtin-op
       if v1 == self.const or v2 == self.const:
         continue
+      # v1s = [v1]
+      # v2s = [v2]
+      # if '*' in v1:
+      #   v1s = v1.split('*')
+      # if '*' in v2:
+      #   v2s = v2.split('*')
+      # vs = [v for v in v1s if v in v2s]
+      # if vs != []:
+      #   continue
       yield v1, v2
 
   def modulo(self, e: dict[str, float]) -> dict[str, float]:
@@ -503,23 +536,44 @@ def get_all_eqs_and_why(
           value = simplify(frac.numerator, frac.denominator)
           yield v1, v2, value, self.why(why_dict)
         continue
-
+      
       groups.append(vv)
 
     if not return_quads:
       return
 
     self.groups, links, _ = update_groups(self.groups, groups)
+    lenall = len(links)
+    cnt = 0
     for (v1, v2), (v3, v4) in links:
+      cnt += 1
+      if cnt % 1000 == 0:
+        print(f'{cnt}/{lenall}')
       if self.check_record_eq(v1, v2, v3, v4):
         continue
+      # v1s = [v1]
+      # v2s = [v2]
+      # v3s = [v3]
+      # v4s = [v4]
+      # if '*' in v1:
+      #   v1s = v1.split('*')
+      # if '*' in v2:
+      #   v2s = v2.split('*')
+      # if '*' in v3:
+      #   v3s = v3.split('*')
+      # if '*' in v3:
+      #   v4s = v4.split('*')
+      # v14 = v1s + v4s
+      # v23 = v2s + v3s
+      # vs = [v for v in v14 if v in v23]
       e12 = minus(self.v2e[v1], self.v2e[v2])
       e34 = minus(self.v2e[v3], self.v2e[v4])
 
       why_dict = minus(  # why (v1-v2)-(v3-v4)=e12-e34?
           minus({v1: 1, v2: -1}, {v3: 1, v4: -1}), minus(e12, e34)
       )
       self.record_eq(v1, v2, v3, v4)
+      #if vs == []:
       yield v1, v2, v3, v4, self.why(why_dict)
 
 
@@ -543,6 +597,7 @@ def get_all_eqs_and_why(
     for out in super().get_all_eqs_and_why(return_quads):
       if len(out) == 3:
         x, y, why = out
+        #print('out2', x, y)
         x, y = self.map2obj([x, y])
         yield x, y, why
       if len(out) == 4:
@@ -551,6 +606,7 @@ def get_all_eqs_and_why(
         yield x, y, f, why
       if len(out) == 5:
         a, b, x, y, why = out
+        #print('out4', a, b, x, y)
         a, b, x, y = self.map2obj([a, b, x, y])
         yield a, b, x, y, why
 
@@ -575,19 +631,32 @@ def add_const_ratio(
 
   def add_eqratio(
       self,
-      l1: gm.Length,
-      l2: gm.Length,
-      l3: gm.Length,
-      l4: gm.Length,
+      l1: Union[gm.Length, gm.Length_Pro],
+      l2: Union[gm.Length, gm.Length_Pro],
+      l3: Union[gm.Length, gm.Length_Pro],
+      l4: Union[gm.Length, gm.Length_Pro],
       dep: pr.Dependency,
   ) -> None:
     l1, l2, l3, l4 = self.get_name([l1, l2, l3, l4])
-    return self.add_eq4(l1, l2, l3, l4, dep)
+    return super().add_eq4(l1, l2, l3, l4, dep)
+
+  def add_length_pro(
+      self,
+      lp: gm.Length_Pro,
+      l1: gm.Length,
+      l2: gm.Length,
+      dep=None,
+  ) -> None:
+    if lp.name in self.v2obj:
+      return
+    lp, l1, l2 = self.get_name([lp, l1, l2])
+    return super().add_eq5(lp, l1, l2, dep)
 
   def get_all_eqs_and_why(self) -> Generator[Any, None, None]:
     return super().get_all_eqs_and_why(True)
 
 
+
 class AngleTable(GeometricTable):
   """Coefficient matrix A for slope(direction)."""
 

bin/activate

@@ -0,0 +1,87 @@
+# This file must be used with "source bin/activate" *from bash*
+# you cannot run it directly
+
+
+if [ "${BASH_SOURCE-}" = "$0" ]; then
+    echo "You must source this script: \$ source $0" >&2
+    exit 33
+fi
+
+deactivate () {
+    unset -f pydoc >/dev/null 2>&1 || true
+
+    # reset old environment variables
+    # ! [ -z ${VAR+_} ] returns true if VAR is declared at all
+    if ! [ -z "${_OLD_VIRTUAL_PATH:+_}" ] ; then
+        PATH="$_OLD_VIRTUAL_PATH"
+        export PATH
+        unset _OLD_VIRTUAL_PATH
+    fi
+    if ! [ -z "${_OLD_VIRTUAL_PYTHONHOME+_}" ] ; then
+        PYTHONHOME="$_OLD_VIRTUAL_PYTHONHOME"
+        export PYTHONHOME
+        unset _OLD_VIRTUAL_PYTHONHOME
+    fi
+
+    # The hash command must be called to get it to forget past
+    # commands. Without forgetting past commands the $PATH changes
+    # we made may not be respected
+    hash -r 2>/dev/null
+
+    if ! [ -z "${_OLD_VIRTUAL_PS1+_}" ] ; then
+        PS1="$_OLD_VIRTUAL_PS1"
+        export PS1
+        unset _OLD_VIRTUAL_PS1
+    fi
+
+    unset VIRTUAL_ENV
+    unset VIRTUAL_ENV_PROMPT
+    if [ ! "${1-}" = "nondestructive" ] ; then
+    # Self destruct!
+        unset -f deactivate
+    fi
+}
+
+# unset irrelevant variables
+deactivate nondestructive
+
+VIRTUAL_ENV=/home/featurize/work/alphageometry
+if ([ "$OSTYPE" = "cygwin" ] || [ "$OSTYPE" = "msys" ]) && $(command -v cygpath &> /dev/null) ; then
+    VIRTUAL_ENV=$(cygpath -u "$VIRTUAL_ENV")
+fi
+export VIRTUAL_ENV
+
+_OLD_VIRTUAL_PATH="$PATH"
+PATH="$VIRTUAL_ENV/"bin":$PATH"
+export PATH
+
+if [ "x"'' != x ] ; then
+    VIRTUAL_ENV_PROMPT=''
+else
+    VIRTUAL_ENV_PROMPT=$(basename "$VIRTUAL_ENV")
+fi
+export VIRTUAL_ENV_PROMPT
+
+# unset PYTHONHOME if set
+if ! [ -z "${PYTHONHOME+_}" ] ; then
+    _OLD_VIRTUAL_PYTHONHOME="$PYTHONHOME"
+    unset PYTHONHOME
+fi
+
+if [ -z "${VIRTUAL_ENV_DISABLE_PROMPT-}" ] ; then
+    _OLD_VIRTUAL_PS1="${PS1-}"
+    PS1="(${VIRTUAL_ENV_PROMPT}) ${PS1-}"
+    export PS1
+fi
+
+# Make sure to unalias pydoc if it's already there
+alias pydoc 2>/dev/null >/dev/null && unalias pydoc || true
+
+pydoc () {
+    python -m pydoc "$@"
+}
+
+# The hash command must be called to get it to forget past
+# commands. Without forgetting past commands the $PATH changes
+# we made may not be respected
+hash -r 2>/dev/null || true