#18 Distinguish whether a variable is already in memory

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:

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
+}

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
+}

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"