From f0e51dd4bc2544b4ad683f7ea28c4b5cc95b8ec8 Mon Sep 17 00:00:00 2001 From: alexcere <48130030+alexcere@users.noreply.github.com> Date: Fri, 10 Jan 2025 14:24:12 +0100 Subject: [PATCH] #18 Distinguish whether a variable is already in memory --- src/greedy/greedy_new_version.py | 17 ++-- .../greedy_permutation_files/swap_s2_s17.json | 78 +++++++++++++++++++ .../greedy_permutation_files/swap_s6_s17.json | 78 +++++++++++++++++++ tests/test_greedy_permutation.py | 17 +++- 4 files changed, 184 insertions(+), 6 deletions(-) create mode 100644 tests/greedy_permutation_files/swap_s2_s17.json create mode 100644 tests/greedy_permutation_files/swap_s6_s17.json diff --git a/src/greedy/greedy_new_version.py b/src/greedy/greedy_new_version.py index e10724ab..b65d5181 100644 --- a/src/greedy/greedy_new_version.py +++ b/src/greedy/greedy_new_version.py @@ -128,7 +128,7 @@ def __init__(self, initial_stack: List[var_id_T], dependency_graph: nx.DiGraph, self.n_computed: Counter = Counter(initial_stack) # Stack variables that have been moved to the memory due to accessing deeper elements - self.vars_in_memory: List[var_id_T] = [] + self.vars_in_memory: Set[var_id_T] = set() # Debug mode: store all the ops applied and the stacks before and after if self.debug_mode: @@ -362,7 +362,7 @@ def store_in_memory(self): Stores the topmost value in memory. Its behaviour is similar to POP """ stack_var = self.stack.pop(0) - self.vars_in_memory.append(stack_var) + self.vars_in_memory.add(stack_var) # Var copies: we add one because the stack var is totally removed from the encoding self.stack_var_copies_needed[stack_var] += 1 @@ -1215,12 +1215,19 @@ def move_vars_to_memory(self, current_position: cstack_pos_T, cstate: SymbolicSt # There are two options: if the memory contains the corresponding element, then we store an extra element # to be able to load it from memory + element_in_position = self._final_stack[cstate.idx_wrt_fstack(current_position)] stored_in_memory = self._final_stack[cstate.idx_wrt_fstack(current_position)] in cstate.vars_in_memory - while (current_position > STACK_DEPTH and stored_in_memory) or current_position >= STACK_DEPTH: - self.debug_logger.debug_message(f"Current_position: {current_position}") + + while current_position > STACK_DEPTH or (current_position == STACK_DEPTH and stored_in_memory): + topmost_element = cstate.top_stack() + + # The elements we are storing could be the one we will have to swap + if topmost_element == element_in_position: + stored_in_memory = True + move_vars_ops.extend(cstate.store_in_memory()) current_position -= 1 - self.debug_logger.debug_message(f"Afterwards: {current_position}") + return move_vars_ops def print_traces(self, cstate: SymbolicState) -> None: diff --git a/tests/greedy_permutation_files/swap_s2_s17.json b/tests/greedy_permutation_files/swap_s2_s17.json new file mode 100644 index 00000000..eef754cc --- /dev/null +++ b/tests/greedy_permutation_files/swap_s2_s17.json @@ -0,0 +1,78 @@ +{ + "name": "swap_element17", + "init_progr_len": 1, + "max_progr_len": 1, + "max_sk_sz": 18, + "vars": [ + "s(0)", + "s(1)", + "s(10)", + "s(11)", + "s(12)", + "s(13)", + "s(14)", + "s(15)", + "s(16)", + "s(17)", + "s(2)", + "s(3)", + "s(4)", + "s(5)", + "s(6)", + "s(7)", + "s(8)", + "s(9)" + ], + "src_ws": [ + "s(0)", + "s(1)", + "s(2)", + "s(3)", + "s(4)", + "s(5)", + "s(6)", + "s(7)", + "s(8)", + "s(9)", + "s(10)", + "s(11)", + "s(12)", + "s(13)", + "s(14)", + "s(15)", + "s(16)", + "s(17)" + ], + "tgt_ws": [ + "s(0)", + "s(1)", + "s(17)", + "s(3)", + "s(4)", + "s(5)", + "s(6)", + "s(7)", + "s(8)", + "s(9)", + "s(10)", + "s(11)", + "s(12)", + "s(13)", + "s(14)", + "s(15)", + "s(16)", + "s(2)" + ], + "user_instrs": [], + "current_cost": 3, + "storage_dependences": [], + "memory_dependences": [], + "dependencies": [], + "is_revert": false, + "rules_applied": false, + "rules": [], + "original_instrs": "SWAP16", + "min_length_instrs": 0, + "min_length_bounds": 0, + "min_length": 0 +} \ No newline at end of file diff --git a/tests/greedy_permutation_files/swap_s6_s17.json b/tests/greedy_permutation_files/swap_s6_s17.json new file mode 100644 index 00000000..b0970e48 --- /dev/null +++ b/tests/greedy_permutation_files/swap_s6_s17.json @@ -0,0 +1,78 @@ +{ + "name": "swap_element17", + "init_progr_len": 1, + "max_progr_len": 1, + "max_sk_sz": 18, + "vars": [ + "s(0)", + "s(1)", + "s(10)", + "s(11)", + "s(12)", + "s(13)", + "s(14)", + "s(15)", + "s(16)", + "s(17)", + "s(2)", + "s(3)", + "s(4)", + "s(5)", + "s(6)", + "s(7)", + "s(8)", + "s(9)" + ], + "src_ws": [ + "s(0)", + "s(1)", + "s(2)", + "s(3)", + "s(4)", + "s(5)", + "s(6)", + "s(7)", + "s(8)", + "s(9)", + "s(10)", + "s(11)", + "s(12)", + "s(13)", + "s(14)", + "s(15)", + "s(16)", + "s(17)" + ], + "tgt_ws": [ + "s(0)", + "s(1)", + "s(2)", + "s(3)", + "s(4)", + "s(5)", + "s(17)", + "s(7)", + "s(8)", + "s(9)", + "s(10)", + "s(11)", + "s(12)", + "s(13)", + "s(14)", + "s(15)", + "s(16)", + "s(6)" + ], + "user_instrs": [], + "current_cost": 3, + "storage_dependences": [], + "memory_dependences": [], + "dependencies": [], + "is_revert": false, + "rules_applied": false, + "rules": [], + "original_instrs": "SWAP16", + "min_length_instrs": 0, + "min_length_bounds": 0, + "min_length": 0 +} \ No newline at end of file diff --git a/tests/test_greedy_permutation.py b/tests/test_greedy_permutation.py index c29bdbda..a8924dc0 100644 --- a/tests/test_greedy_permutation.py +++ b/tests/test_greedy_permutation.py @@ -12,5 +12,20 @@ class TestGreedyPermutation: def test_swap_element17(self): sfs, seq, outcome = greedy_from_file("greedy_permutation_files/swap_element17.json") + assert check_execution_from_ids(sfs, seq), "Incorrect solution for SWAP17 tests" + desired_ids = ['SET(s(0))', 'SET(s(1))', 'GET(s(0))', 'SWAP16', 'GET(s(1))', 'SWAP1'] + assert desired_ids == seq, "Not reaching desired solution in SWAP17 test" + + def test_swap_s2_s17(self): + sfs, seq, outcome = greedy_from_file("greedy_permutation_files/swap_s2_s17.json") + print("LEN", len(seq)) + assert check_execution_from_ids(sfs, seq), "Incorrect solution for swap(s2, s17) test" + desired_ids = ['SET(s(0))', 'SWAP16', 'SWAP1', 'SWAP16', 'GET(s(0))'] + assert desired_ids == seq, "Not reaching desired solution in swap(s2, s17) test" + + def test_swap_s6_s17(self): + sfs, seq, outcome = greedy_from_file("greedy_permutation_files/swap_s6_s17.json") print("LEN", len(seq)) - assert check_execution_from_ids(sfs, seq), "Failing SWAP17 tests" + assert check_execution_from_ids(sfs, seq), "Incorrect solution for swap(s6, s17) test" + desired_ids = ['SET(s(0))', 'SWAP16', 'SWAP5', 'SWAP16', 'GET(s(0))'] + assert desired_ids == seq, "Not reaching desired solution in swap(s2, s17) test"