[issue879] (deterministically) randomize order in which invariant thr…

…eats are considered

src/translate/invariant_finder.py

@@ -3,6 +3,7 @@
 
 from collections import deque, defaultdict
 import itertools
+import random
 import time
 from typing import List
 
@@ -104,6 +105,11 @@ def enqueue_func(invariant):
             candidates.append(invariant)
             seen_candidates.add(invariant)
 
+    # we want to fix the random seed for the invariant synthesis but don't want
+    # to have this a more global impact. For this reason, we temporary store
+    # the state of the random generator.
+    random_state = random.getstate()
+    random.seed(314159)
     start_time = time.process_time()
     while candidates:
         candidate = candidates.popleft()
@@ -112,6 +118,7 @@ def enqueue_func(invariant):
             return
         if candidate.check_balance(balance_checker, enqueue_func):
             yield candidate
+    random.setstate(random_state)
 
 def useful_groups(invariants, initial_facts):
     predicate_to_invariants = defaultdict(list)

src/translate/invariants.py

@@ -1,5 +1,6 @@
 from collections import defaultdict
 import itertools
+from random import randrange
 
 import constraints
 import pddl
@@ -324,12 +325,25 @@ def check_balance(self, balance_checker, enqueue_func):
         # invariance analysis.
         for part in self.parts:
             actions_to_check.update(balance_checker.get_threats(part.predicate))
-        for action in actions_to_check.keys():
+
+        # For a better expected perfomance, we want to randomize the order in
+        # which actions are checked. Since candidates are often already
+        # discarded by an early check, we do not want to shuffle the order but
+        # instead always draw the next action randomly from those we did not
+        # yet consider.
+        actions = list(actions_to_check.keys())
+        unchecked = len(actions)
+        while unchecked:
+            pos = randrange(unchecked)
+            action = actions[pos]
             heavy_action = balance_checker.get_heavy_action(action)
             if self._operator_too_heavy(heavy_action):
                 return False
             if self._operator_unbalanced(action, enqueue_func):
                 return False
+            actions[pos], actions[unchecked - 1] = \
+                actions[unchecked - 1], actions[pos]
+            unchecked -= 1
         return True
 
     def _operator_too_heavy(self, h_action):