Skip to content

Commit

Permalink
Adding SAT xor differential-linear model
Browse files Browse the repository at this point in the history
  • Loading branch information
@juaninf
juaninf committed Feb 18, 2025
1 parent 2fc61a3 commit 937cb53
Show file tree
Hide file tree
Showing 2 changed files with 49 additions and 253 deletions.
8 changes: 4 additions & 4 deletions claasp/cipher_modules/models/sat/sat_models/sat_differential_linear_model.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -247,10 +247,10 @@ def build_xor_differential_linear_model(
if vari.startswith('cipher_output'):
print(vari)

minimize_vars = [f'cipher_output_7_24_{i}_o' for i in range(512)]
n_vars, v_const = self._sequential_counter(minimize_vars, 3, "dummy_id_unknown")
self._variables_list.extend(n_vars)
self._model_constraints.extend(v_const)
# minimize_vars = [f'cipher_output_7_24_{i}_o' for i in range(512)]
# n_vars, v_const = self._sequential_counter(minimize_vars, 3, "dummy_id_unknown")
# self._variables_list.extend(n_vars)
# self._model_constraints.extend(v_const)

self._get_connecting_constraints()

Expand Down
294 changes: 45 additions & 249 deletions claasp/cipher_modules/models/sat/utils/utils.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1118,259 +1118,55 @@ def get_cnf_semi_deterministic_window_2(
p0, q0, r0
):
return [
f'{p0} {B_t0} -{A_t2} -{C_t1} {A_t0} {C_t0}',
f'{p0} {B_t0} -{A_t2} {B_v1} -{C_v1} {A_t0} {C_t0}',
f'{p0} {B_t0} -{A_t2} {B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} -{A_t2} {B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{A_t2} -{B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{A_t2} -{B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{A_t2} -{C_v1} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} -{C_t3} {B_v3} -{C_t1} {A_v3} {A_t3} {B_t3} {A_t0} {C_t0}',
f'{p0} {B_t0} -{C_t3} {B_v3} {B_v1} {A_v3} -{C_v1} {A_t3} {B_t3} {A_t0} {C_t0}',
f'{p0} {B_t0} -{C_t3} {B_v3} {A_v3} {B_v0} -{C_v1} {A_t3} {B_t3} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} -{C_t3} {B_v3} {A_v3} {B_v0} -{C_v1} {A_t3} {B_t3} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{C_t3} {B_v3} {A_v3} -{B_v0} -{C_v1} {A_t3} {B_t3} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{C_t3} {B_v3} {A_v3} -{B_v0} -{C_v1} {A_t3} {B_t3} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{C_t3} {B_v3} {A_v3} -{C_v1} {A_t3} {B_t3} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} {C_t2} -{C_t1} {A_t0} {C_t0}',
f'{p0} {B_t0} {C_t2} {B_v1} -{C_v1} {A_t0} {C_t0}',
f'{p0} {B_t0} {C_t2} {B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} {C_t2} {B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} {C_t2} -{B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} {C_t2} -{B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} {C_t2} -{C_v1} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} -{B_t1} {A_t0} {C_t0}',
f'{p0} {B_t0} -{A_v2} -{C_t1} {A_t0} {C_t0}',
f'{p0} {B_t0} -{A_v2} {B_v1} -{C_v1} {A_t0} {C_t0}',
f'{p0} {B_t0} -{A_v2} {B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} -{A_v2} {B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{A_v2} -{B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{A_v2} -{B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{A_v2} -{C_v1} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} {C_t1} {B_v1} -{C_v1} {A_t0} {C_t0}',
f'{p0} {B_t0} {C_t1} {B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} {C_t1} {B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} {C_t1} -{B_v0} -{C_v1} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} {C_t1} -{B_v0} -{C_v1} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} {C_t1} -{C_v1} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} -{C_t1} -{B_v1} {A_t0} {C_t0}',
f'{p0} {B_t0} -{C_t1} {B_v0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{C_t1} {B_v0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{C_t1} -{B_v0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} -{C_t1} -{B_v0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{C_t1} -{B_v2} {A_t0} {C_t0}',
f'{p0} {B_t0} -{C_t1} {r0} {A_t0} {C_t0}',
f'{p0} {B_t0} -{C_t1} {A_t0} {C_t0} -{A_v1}',
f'{p0} {B_t0} -{C_t1} {A_t0} {C_t0} -{B_t2}',
f'{p0} {B_t0} -{C_t1} {A_t0} {C_t0} {q0}',
f'{p0} {B_t0} {B_v1} {B_v0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v1} {B_v0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} {B_v1} -{B_v0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} {B_v1} -{B_v0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v1} -{C_v1} -{B_v2} {A_t0} {C_t0}',
f'{p0} {B_t0} {B_v1} -{C_v1} {r0} {A_t0} {C_t0}',
f'{p0} {B_t0} {B_v1} -{C_v1} {A_t0} {C_t0} -{B_t2}',
f'{p0} {B_t0} {B_v1} -{C_v1} {A_t0} {C_t0} {q0}',
f'{p0} {B_t0} {B_v1} {A_t0} {C_t0} -{A_v1}',
f'{p0} {B_t0} -{B_v1} {B_v0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v1} {B_v0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v1} -{B_v0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v1} -{B_v0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v1} {C_v1} {A_t0} {C_t0}',
f'{p0} {B_t0} -{B_v1} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} {B_v0} {C_v1} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v0} {C_v1} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} -{B_v2} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} -{B_v2} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} {r0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} {r0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} {A_t0} {C_t0} -{B_t2} {C_v0} {A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} {A_t0} {C_t0} -{B_t2} -{C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} {A_t0} {C_t0} {q0} {C_v0} {A_v0}',
f'{p0} {B_t0} {B_v0} -{C_v1} {A_t0} {C_t0} {q0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v0} {A_t0} {C_t0} {A_v1} {C_v0} -{A_v0}',
f'{p0} {B_t0} {B_v0} {A_t0} {C_t0} {A_v1} -{C_v0} {A_v0}',
f'{p0} {B_t0} {B_v0} {A_t0} {C_t0} -{A_v1} {C_v0} {A_v0}',
f'{p0} {B_t0} {B_v0} {A_t0} {C_t0} -{A_v1} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} {C_v1} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v0} {C_v1} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} -{B_v2} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} -{B_v2} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} {r0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} {r0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} {A_t0} {C_t0} -{B_t2} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} {A_t0} {C_t0} -{B_t2} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} {A_t0} {C_t0} {q0} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} -{C_v1} {A_t0} {C_t0} {q0} -{C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v0} {A_t0} {C_t0} {A_v1} {C_v0} {A_v0}',
f'{p0} {B_t0} -{B_v0} {A_t0} {C_t0} {A_v1} -{C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} {A_t0} {C_t0} -{A_v1} {C_v0} -{A_v0}',
f'{p0} {B_t0} -{B_v0} {A_t0} {C_t0} -{A_v1} -{C_v0} {A_v0}',
f'{p0} {B_t0} {C_v1} {A_t0} {C_t0} -{A_v1}',
f'{p0} {B_t0} -{C_v1} -{B_v2} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} -{C_v1} {r0} {A_t0} {C_t0} {A_v1}',
f'{p0} {B_t0} -{C_v1} {A_t0} {C_t0} {A_v1} -{B_t2}',
f'{p0} {B_t0} -{C_v1} {A_t0} {C_t0} {A_v1} {q0}',
f'{p0} {B_t0} {A_t0} {C_t0} -{A_t1}',
f'{p0} -{A_t2} -{r0}',
f'{p0} -{C_t3} {B_v3} {A_v3} -{r0} {A_t3} {B_t3}',
f'{p0} {C_t2} -{r0}',
f'{p0} -{B_t1} -{r0}',
f'{p0} -{A_v2} -{r0}',
f'{p0} {C_t1} -{r0}',
f'{p0} -{B_v1} -{r0}',
f'{p0} {B_v0} -{r0} {C_v0} -{A_v0}',
f'{p0} {B_v0} -{r0} -{C_v0} {A_v0}',
f'{p0} -{B_v0} -{r0} {C_v0} {A_v0}',
f'{p0} -{B_v0} -{r0} -{C_v0} -{A_v0}',
f'{p0} -{B_v2} -{r0}',
f'{p0} -{r0} -{A_v1}',
f'{p0} -{r0} -{B_t2}',
f'{p0} -{r0} {q0}',
f'{p0} -{r0} -{A_t1}',
f'-{p0} -{B_t0}',
f'-{p0} {A_t2} -{C_t2} {B_t1} {A_v2} -{C_t1} {B_v1} {B_v2} {A_v1} {B_t2} {A_t1}',
f'-{p0} {A_t2} -{C_t2} {B_t1} {A_v2} {B_v1} {C_v1} {B_v2} {A_v1} {B_t2} {A_t1}',
f'-{p0} {A_t2} -{C_t2} {A_v2} {B_v2} {r0} {B_t2}',
f'-{p0} {B_t1} {C_t1} {B_v1} {C_v1} {A_v1} {A_t1}',
f'-{p0} {B_t1} {C_t1} -{B_v1} -{C_v1} -{A_v1} {A_t1}',
f'-{p0} {B_t1} -{C_t1} {B_v1} {B_v0} {A_v1} {C_v0} {A_t1} -{A_v0}',
f'-{p0} {B_t1} -{C_t1} {B_v1} {B_v0} {A_v1} -{C_v0} {A_t1} {A_v0}',
f'-{p0} {B_t1} -{C_t1} {B_v1} -{B_v0} {A_v1} {C_v0} {A_t1} {A_v0}',
f'-{p0} {B_t1} -{C_t1} {B_v1} -{B_v0} {A_v1} -{C_v0} {A_t1} -{A_v0}',
f'-{p0} {B_t1} -{C_t1} {B_v1} -{r0} {A_v1} {A_t1}',
f'-{p0} {B_t1} {B_v1} {B_v0} {C_v1} {A_v1} {C_v0} {A_t1} -{A_v0}',
f'-{p0} {B_t1} {B_v1} {B_v0} {C_v1} {A_v1} -{C_v0} {A_t1} {A_v0}',
f'-{p0} {B_t1} {B_v1} -{B_v0} {C_v1} {A_v1} {C_v0} {A_t1} {A_v0}',
f'-{p0} {B_t1} {B_v1} -{B_v0} {C_v1} {A_v1} -{C_v0} {A_t1} -{A_v0}',
f'-{p0} {B_t1} {B_v1} {C_v1} -{r0} {A_v1} {A_t1}',
f'-{p0} -{B_t1} {r0}',
f'-{p0} {C_t1} {r0}',
f'-{p0} -{B_v1} {r0}',
f'-{p0} {B_v0} {r0} {C_v0} -{A_v0}',
f'-{p0} {B_v0} {r0} -{C_v0} {A_v0}',
f'-{p0} -{B_v0} {r0} {C_v0} {A_v0}',
f'-{p0} -{B_v0} {r0} -{C_v0} -{A_v0}',
f'-{p0} {r0} -{A_v1}',
f'-{p0} {r0} -{A_t1}',
f'-{p0} -{A_t0}',
f'-{p0} -{C_t0}',
f'-{p0} -{q0}',
f'{B_t0} {A_t2} -{C_t3} -{C_t2} {B_t1} {B_v3} {A_v2} -{C_t1} {B_v1} {A_v3} {B_v2} {A_t3} {B_t3} {A_t0} {C_t0} {A_v1} {B_t2} {A_t1}',
f'{B_t0} {A_t2} -{C_t2} {B_t1} {A_v2} -{C_t1} {B_v1} {B_v2} {A_t0} {C_t0} {A_v1} {B_t2} {q0} {A_t1}',
f'{B_t0} {A_t2} -{C_t2} {A_v2} -{C_t1} {B_v2} {r0} {A_t0} {C_t0} {B_t2}',
f'{B_t0} {A_t2} -{C_t2} {A_v2} {B_v1} -{C_v1} {B_v2} {r0} {A_t0} {C_t0} {B_t2}',
f'{B_t0} {A_t2} -{C_t2} {A_v2} {B_v0} -{C_v1} {B_v2} {r0} {A_t0} {C_t0} {B_t2} {C_v0} {A_v0}',
f'{B_t0} {A_t2} -{C_t2} {A_v2} {B_v0} -{C_v1} {B_v2} {r0} {A_t0} {C_t0} {B_t2} -{C_v0} -{A_v0}',
f'{B_t0} {A_t2} -{C_t2} {A_v2} -{B_v0} -{C_v1} {B_v2} {r0} {A_t0} {C_t0} {B_t2} {C_v0} -{A_v0}',
f'{B_t0} {A_t2} -{C_t2} {A_v2} -{B_v0} -{C_v1} {B_v2} {r0} {A_t0} {C_t0} {B_t2} -{C_v0} {A_v0}',
f'{B_t0} {A_t2} -{C_t2} {A_v2} -{C_v1} {B_v2} {r0} {A_t0} {C_t0} {A_v1} {B_t2}',
f'{B_t0} {B_t1} -{C_t1} {B_v1} {B_v0} {A_t0} {C_t0} {A_v1} {C_v0} {A_t1} -{A_v0}',
f'{B_t0} {B_t1} -{C_t1} {B_v1} {B_v0} {A_t0} {C_t0} {A_v1} -{C_v0} {A_t1} {A_v0}',
f'{B_t0} {B_t1} -{C_t1} {B_v1} -{B_v0} {A_t0} {C_t0} {A_v1} {C_v0} {A_t1} {A_v0}',
f'{B_t0} {B_t1} -{C_t1} {B_v1} -{B_v0} {A_t0} {C_t0} {A_v1} -{C_v0} {A_t1} -{A_v0}',
f'{B_t0} {B_t1} {B_v1} {B_v0} {C_v1} {A_t0} {C_t0} {A_v1} {C_v0} {A_t1} -{A_v0}',
f'{B_t0} {B_t1} {B_v1} {B_v0} {C_v1} {A_t0} {C_t0} {A_v1} -{C_v0} {A_t1} {A_v0}',
f'{B_t0} {B_t1} {B_v1} -{B_v0} {C_v1} {A_t0} {C_t0} {A_v1} {C_v0} {A_t1} {A_v0}',
f'{B_t0} {B_t1} {B_v1} -{B_v0} {C_v1} {A_t0} {C_t0} {A_v1} -{C_v0} {A_t1} -{A_v0}',
f'{B_t0} -{B_t1} {r0} {A_t0} {C_t0}',
f'{B_t0} {C_t1} {B_v1} -{C_v1} {r0} {A_t0} {C_t0}',
f'{B_t0} {C_t1} {B_v0} -{C_v1} {r0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{B_t0} {C_t1} {B_v0} -{C_v1} {r0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{B_t0} {C_t1} -{B_v0} -{C_v1} {r0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{B_t0} {C_t1} -{B_v0} -{C_v1} {r0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{B_t0} {C_t1} -{C_v1} {r0} {A_t0} {C_t0} {A_v1}',
f'{B_t0} -{C_t1} -{B_v1} {r0} {A_t0} {C_t0}',
f'{B_t0} -{C_t1} {B_v0} {r0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{B_t0} -{C_t1} {B_v0} {r0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{B_t0} -{C_t1} -{B_v0} {r0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{B_t0} -{C_t1} -{B_v0} {r0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{B_t0} -{C_t1} {r0} {A_t0} {C_t0} -{A_v1}',
f'{B_t0} {B_v1} {B_v0} {r0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{B_t0} {B_v1} {B_v0} {r0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{B_t0} {B_v1} -{B_v0} {r0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{B_t0} {B_v1} -{B_v0} {r0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{B_t0} {B_v1} {r0} {A_t0} {C_t0} -{A_v1}',
f'{B_t0} -{B_v1} {B_v0} {r0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{B_t0} -{B_v1} {B_v0} {r0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{B_t0} -{B_v1} -{B_v0} {r0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{B_t0} -{B_v1} -{B_v0} {r0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{B_t0} -{B_v1} {C_v1} {r0} {A_t0} {C_t0}',
f'{B_t0} -{B_v1} {r0} {A_t0} {C_t0} {A_v1}',
f'{B_t0} {B_v0} {C_v1} {r0} {A_t0} {C_t0} {C_v0} -{A_v0}',
f'{B_t0} {B_v0} {C_v1} {r0} {A_t0} {C_t0} -{C_v0} {A_v0}',
f'{B_t0} {B_v0} {r0} {A_t0} {C_t0} {A_v1} {C_v0} -{A_v0}',
f'{B_t0} {B_v0} {r0} {A_t0} {C_t0} {A_v1} -{C_v0} {A_v0}',
f'{B_t0} {B_v0} {r0} {A_t0} {C_t0} -{A_v1} {C_v0} {A_v0}',
f'{B_t0} {B_v0} {r0} {A_t0} {C_t0} -{A_v1} -{C_v0} -{A_v0}',
f'{B_t0} -{B_v0} {C_v1} {r0} {A_t0} {C_t0} {C_v0} {A_v0}',
f'{B_t0} -{B_v0} {C_v1} {r0} {A_t0} {C_t0} -{C_v0} -{A_v0}',
f'{B_t0} -{B_v0} {r0} {A_t0} {C_t0} {A_v1} {C_v0} {A_v0}',
f'{B_t0} -{B_v0} {r0} {A_t0} {C_t0} {A_v1} -{C_v0} -{A_v0}',
f'{B_t0} -{B_v0} {r0} {A_t0} {C_t0} -{A_v1} {C_v0} -{A_v0}',
f'{B_t0} -{B_v0} {r0} {A_t0} {C_t0} -{A_v1} -{C_v0} {A_v0}',
f'{B_t0} {C_v1} {r0} {A_t0} {C_t0} -{A_v1}',
f'{B_t0} {r0} {A_t0} {C_t0} -{A_t1}',
f'-{B_t0} {B_t1} {C_t1} {B_v1} {C_v1} {A_v1} {A_t1}',
f'-{B_t0} {B_t1} {C_t1} -{B_v1} -{C_v1} -{A_v1} {A_t1}',
f'-{B_t0} -{r0}',
f'-{B_t0} -{q0}',
f'-{A_t2} {B_t1} -{C_t1} {B_v1} -{r0} {A_v1} {A_t1}',
f'-{A_t2} {B_t1} {B_v1} {C_v1} -{r0} {A_v1} {A_t1}',
f'{A_t3} {A_v3} {B_t3} {B_v3} -{C_t3} -{q0}',
f'-{A_t1} -{q0}',
f'{A_t2} {A_v2} {B_t2} {B_v2} -{C_t2} -{p0} {r0}',
f'{A_t1} {A_v0} -{A_v1} {B_t1} {B_v0} -{B_v1} {C_t1} {C_v0} -{C_v1}',
f'{A_t1} -{A_v0} -{A_v1} {B_t1} -{B_v0} -{B_v1} {C_t1} {C_v0} -{C_v1}',
f'{A_t1} -{A_v0} -{A_v1} {B_t1} {B_v0} -{B_v1} {C_t1} -{C_v0} -{C_v1}',
f'{A_t1} {A_v0} -{A_v1} {B_t1} -{B_v0} -{B_v1} {C_t1} -{C_v0} -{C_v1}',
f'-{A_t2} -{q0}',
f'-{C_t3} {B_t1} {B_v3} -{C_t1} {B_v1} {A_v3} -{r0} {A_t3} {B_t3} {A_v1} {A_t1}',
f'-{C_t3} {B_t1} {B_v3} {B_v1} {A_v3} {C_v1} -{r0} {A_t3} {B_t3} {A_v1} {A_t1}',
f'-{C_t3} {B_v3} {A_v3} {A_t3} {B_t3} -{q0}',
f'{C_t2} {B_t1} -{C_t1} {B_v1} -{r0} {A_v1} {A_t1}',
f'{C_t2} {B_t1} {B_v1} {C_v1} -{r0} {A_v1} {A_t1}',
f'{C_t2} -{q0}',
f'{B_t1} -{A_v2} -{C_t1} {B_v1} -{r0} {A_v1} {A_t1}',
f'{B_t1} -{A_v2} {B_v1} {C_v1} -{r0} {A_v1} {A_t1}',
f'{B_t1} {C_t1} {B_v1} {B_v0} {C_v1} {A_v1} {C_v0} {A_t1} -{A_v0}',
f'{B_t1} {C_t1} {B_v1} {B_v0} {C_v1} {A_v1} -{C_v0} {A_t1} {A_v0}',
f'{B_t1} {C_t1} {B_v1} -{B_v0} {C_v1} {A_v1} {C_v0} {A_t1} {A_v0}',
f'{B_t1} {C_t1} {B_v1} -{B_v0} {C_v1} {A_v1} -{C_v0} {A_t1} -{A_v0}',
f'{B_t1} {C_t1} {B_v1} {C_v1} -{r0} {A_v1} {A_t1}',
f'{B_t1} {C_t1} {B_v1} {C_v1} -{A_t0} {A_v1} {A_t1}',
f'{B_t1} {C_t1} {B_v1} {C_v1} -{C_t0} {A_v1} {A_t1}',
f'{B_t1} {C_t1} -{B_v1} {B_v0} -{C_v1} -{A_v1} {C_v0} {A_t1} {A_v0}',
f'{B_t1} {C_t1} -{B_v1} {B_v0} -{C_v1} -{A_v1} -{C_v0} {A_t1} -{A_v0}',
f'{B_t1} {C_t1} -{B_v1} -{B_v0} -{C_v1} -{A_v1} {C_v0} {A_t1} -{A_v0}',
f'{B_t1} {C_t1} -{B_v1} -{B_v0} -{C_v1} -{A_v1} -{C_v0} {A_t1} {A_v0}',
f'{B_t1} {C_t1} -{B_v1} -{C_v1} -{r0} -{A_v1} {A_t1}',
f'{B_t1} {C_t1} -{B_v1} -{C_v1} -{A_t0} -{A_v1} {A_t1}',
f'{B_t1} {C_t1} -{B_v1} -{C_v1} -{C_t0} -{A_v1} {A_t1}',
f'{B_t1} -{C_t1} {B_v1} {B_v0} -{r0} {A_v1} {C_v0} {A_t1} -{A_v0}',
f'{B_t1} -{C_t1} {B_v1} {B_v0} -{r0} {A_v1} -{C_v0} {A_t1} {A_v0}',
f'{B_t1} -{C_t1} {B_v1} -{B_v0} -{r0} {A_v1} {C_v0} {A_t1} {A_v0}',
f'{B_t1} -{C_t1} {B_v1} -{B_v0} -{r0} {A_v1} -{C_v0} {A_t1} -{A_v0}',
f'{B_t1} -{C_t1} {B_v1} -{B_v2} -{r0} {A_v1} {A_t1}',
f'{B_t1} -{C_t1} {B_v1} -{r0} {A_v1} -{B_t2} {A_t1}',
f'{B_t1} -{C_t1} {B_v1} -{r0} {A_v1} {q0} {A_t1}',
f'{B_t1} {B_v1} {B_v0} {C_v1} -{r0} {A_v1} {C_v0} {A_t1} -{A_v0}',
f'{B_t1} {B_v1} {B_v0} {C_v1} -{r0} {A_v1} -{C_v0} {A_t1} {A_v0}',
f'{B_t1} {B_v1} -{B_v0} {C_v1} -{r0} {A_v1} {C_v0} {A_t1} {A_v0}',
f'{B_t1} {B_v1} -{B_v0} {C_v1} -{r0} {A_v1} -{C_v0} {A_t1} -{A_v0}',
f'{B_t1} {B_v1} {C_v1} -{B_v2} -{r0} {A_v1} {A_t1}',
f'{B_t1} {B_v1} {C_v1} -{r0} {A_v1} -{B_t2} {A_t1}',
f'{B_t1} {B_v1} {C_v1} -{r0} {A_v1} {q0} {A_t1}',
f'-{B_t1} -{q0}',
f'-{A_v1} -{q0}',
f'-{A_v2} -{q0}',
f'{C_t1} -{q0}',
f'-{B_t1} -{q0}',
f'{A_t1} -{A_v1} {B_t1} -{B_v1} {C_t1} -{C_v1} -{r0}',
f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} -{C_t1} {C_v0}',
f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} -{C_t1} {C_v0}',
f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} -{C_t1} -{C_v0}',
f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} -{C_t1} -{C_v0}',
f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} {C_v0} {C_v1}',
f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} {C_v0} {C_v1}',
f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} -{C_v0} {C_v1}',
f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} -{C_v0} {C_v1}',
f'-{B_t2} -{q0}',
f'{A_t1} {A_v1} {B_t1} {B_v1} -{C_t1} {q0} -{r0}',
f'-{A_v1} -{p0} {r0}',
f'{A_t1} {A_v1} {B_t1} {B_v1} {C_v1} {q0} -{r0}',
f'{A_t0} {B_t0} {B_v1} {C_t0} -{C_v1} {p0} {r0}',
f'-{B_v1} -{q0}',
f'{B_v0} -{q0} {C_v0} -{A_v0}',
f'{B_v0} -{q0} -{C_v0} {A_v0}',
f'-{B_v0} -{q0} {C_v0} {A_v0}',
f'-{B_v0} -{q0} -{C_v0} -{A_v0}',
f'-{B_v2} -{q0}',
f'{r0} -{q0}',
f'-{r0} -{A_t0}',
f'-{r0} -{C_t0}',
f'-{A_t0} -{q0}',
f'-{C_t0} -{q0}',
f'-{A_v1} -{q0}',
f'-{B_t2} -{q0}',
f'-{q0} -{A_t1}'
f'{A_t0} -{A_v1} {B_t0} {C_t0} {C_v1} {r0}',
f'{C_t1} -{p0} {r0}',
f'{A_t0} {A_v1} {B_t0} -{B_v1} {C_t0} {r0}',
f'{C_t2} -{q0}',
f'{A_t0} -{A_t1} {B_t0} {C_t0} {r0}',
f'-{A_t0} -{r0}',
f'-{B_t0} -{r0}',
f'{A_t0} {B_t0} -{B_t1} {C_t0} {r0}',
f'-{C_t0} -{r0}',
f'-{p0} -{q0}',
f'{A_t0} {B_t0} {C_t0} -{C_t1} {p0} {q0}',
f'{C_t1} {p0} -{r0}',
f'-{q0} {r0}',
f'{A_t1} -{A_v1} {B_t1} -{B_v1} -{C_t0} {C_t1} -{C_v1}',
f'{A_t1} -{A_v1} -{B_t0} {B_t1} -{B_v1} {C_t1} -{C_v1}',
f'-{A_t0} {A_t1} -{A_v1} {B_t1} -{B_v1} {C_t1} -{C_v1}',
f'{A_t1} {A_v1} {B_t1} {B_v1} -{C_t0} {C_t1} {C_v1}',
f'{A_t1} {A_v1} -{B_t0} {B_t1} {B_v1} {C_t1} {C_v1}',
f'-{A_t0} {A_t1} {A_v1} {B_t1} {B_v1} {C_t1} {C_v1}',
f'-{C_t0} -{p0}',
f'-{B_t0} -{p0}',
f'-{A_t0} -{p0}',
]


Expand Down

0 comments on commit 937cb53

Please sign in to comment.