stronger abstraction

src/tea3/tea3model.py

@@ -7,7 +7,7 @@ from tea3.pretty_print import pretty_print, pretty_print_vec
 
 
 class Tea3Model:
-    def __init__(self, max_abstract=40960):
+    def __init__(self):
         self.F = GF(2)
         self.step_count = 0
 
@@ -15,7 +15,7 @@ class Tea3Model:
             [f"x{i}{j}" for i in range(5) for j in range(8)] +
             [f"r{i}{j}" for i in range(5) for j in range(8)] +
             [f"R{i}{j}" for i in range(8) for j in range(8)] +
-            [f"g{n}"    for n in range(max_abstract)]
+            ["g"]
         )
 
         name_string = ",".join(names)
@@ -26,17 +26,7 @@ class Tea3Model:
         self.r_bits = [list(self.v[40 + i*8 : 40 + (i+1)*8]) for i in range(5)]
         self.R_bits = [list(self.v[80 + i*8 : 80 + (i+1)*8]) for i in range(8)]
 
-        self._g_pool  = list(self.v[80 + 64:])
+        self.g = self.v[-1]
-        self._g_index = 0
-        self.abstractions = {}
-
-    def _alloc(self, step, i, j, xr_key):
-        if self._g_index >= len(self._g_pool):
-            raise RuntimeError("Abstract variable pool exhausted — increase max_abstract.")
-        var = self._g_pool[self._g_index]
-        self.abstractions[(step, i, j, xr_key)] = (var, self._g_index)
-        self._g_index += 1
-        return var
 
     def _abstract_R(self):
         s    = self.step_count
@@ -57,28 +47,19 @@ class Tea3Model:
                         continue
 
                     xr_vars = [v for v in term_vars if str(v)[0] in ('x', 'r')]
-                    Rf_vars = [v for v in term_vars if str(v)[0] in ('R', 'f', 'g')]  # 'g' added
+                    Rf_vars = [v for v in term_vars if str(v)[0] in ('R', 'f', 'g')]
 
                     xr_mono = reduce(mul, (self.S(v) for v in xr_vars), one)
-                    Rf_mono = reduce(mul, (self.S(v) for v in Rf_vars), one)
                     xr_key  = frozenset(str(v) for v in xr_vars)
 
                     if not Rf_vars:
                         pure_xr += xr_mono
                     else:
-                        if xr_key not in groups:
+                        groups[xr_key] = xr_mono
-                            groups[xr_key] = {'xr_mono': xr_mono, 'Rf_sum': zero}
-                        groups[xr_key]['Rf_sum'] += Rf_mono
 
                 result = pure_xr + const
-
+                for xr_key, xr_mono in groups.items():
-                for xr_key, bucket in groups.items():
+                    result += xr_mono * self.g
-                    Rf_sum  = bucket['Rf_sum']
-                    xr_mono = bucket['xr_mono']
-                    if Rf_sum == zero:
-                        continue
-                    g = self._alloc(s, i, j, xr_key)
-                    result += xr_mono * g
 
                 self.R_bits[i][j] = result