[cmd] Implement & Refactor the conversion of previous frontier places to...

[cmd] Implement & Refactor the conversion of previous frontier places to numerical values => big perf gain

command_line/cadbiom_cmd/solution_search.py

@@ -130,6 +130,20 @@ def make_logical_formula(previous_frontier_places, start_prop):
     return add_start_prop('')
 
 
+def get_dimacs_start_properties(mcla, previous_frontier_places):
+    """Translate frontier places to their numerical values
+    thanks to the current unfolder.
+
+    It's much more efficient than using the ANTLR grammar to parse formulas
+    for each new query.
+    """
+    dimacs_start = list()
+    [dimacs_start.append(
+        [-mcla.unfolder.var_dimacs_code(place) for place in frontier_places]
+     )
+     for frontier_places in previous_frontier_places]
+
+
 def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_file,
           steps, final_prop, start_prop, inv_prop, all_macs, continue_run, limit):
     """
@@ -207,19 +221,15 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
         try:
             ## TODO: see docstring of read_mac_file
             previous_frontier_places = read_mac_file(mac_file)
-            current_start_prop = make_logical_formula(previous_frontier_places,
-                                                      start_prop)
             LOGGER.info("%s:: Reload previous frontier places: %s",
                         final_prop,
                         len(previous_frontier_places))
         except IOError:
             LOGGER.warning("%s:: mac file not found!", final_prop)
             previous_frontier_places = set()
-            current_start_prop = start_prop
     else:
         # New run
         previous_frontier_places = set()
-        current_start_prop = start_prop
 
 
     # Compute the number of previously computed frontier places
@@ -231,25 +241,30 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
                     final_prop)
         return
 
-
-    ## Find macs in an optimized way with find_macs() (see the docstring for more info)
-    LOGGER.info("%s:: Start property: %s", final_prop, current_start_prop)
+    ## Find macs in an optimized way with find_macs() (see the doc for more info)
+    LOGGER.info("%s:: Start property: %s", final_prop, start_prop)
     # with PyCallGraph(output=GraphvizOutput()):
     find_macs(mcla,
               mac_file, mac_step_file, mac_complete_file,
-              steps, final_prop, current_start_prop, inv_prop, limit, current_nb_sols)
+              steps, final_prop, start_prop, inv_prop, limit, current_nb_sols,
+              previous_frontier_places)
 
     return
-
-    ## Alternative and deprecated way
+    ############################################################################
+    ############################################################################
+    ## Alternative and deprecated less efficient way
     ## Find mac one by one with find_mac() (see the docstring for more info)
     while True:
+        # Compute the formula of the next start_property
+        current_start_prop = make_logical_formula(previous_frontier_places,
+                                                  start_prop)
         LOGGER.info("%s:: Start property: %s", final_prop, current_start_prop)
 
         ret = \
             find_mac(mcla,
                      mac_file, mac_step_file, mac_complete_file,
-                     steps, final_prop, current_start_prop, inv_prop)
+                     steps, final_prop, start_prop, inv_prop,
+                     previous_frontier_places)
 
         if not ret:
             # No new solution/not satisfiable
@@ -264,10 +279,6 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
                      final_prop,
                      previous_frontier_places)
 
-        # Compute the formula of the next start_property
-        current_start_prop = make_logical_formula(previous_frontier_places,
-                                                  start_prop)
-
         # If set to True (not default), search all macs with
         # less or equal the maxium of steps defined with the argument `steps`.
         # If all_macs == True: The limit is always the maximal number given
@@ -283,15 +294,13 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
                         final_prop)
             return
 
-        LOGGER.debug("%s:: Next start_prop formula: %s in %s steps",
-                     final_prop,
-                     current_start_prop,
-                     steps)
+        LOGGER.debug("%s:: Next solution will be in %s steps", final_prop, steps)
 
 
 def find_macs(mcla,
               mac_file, mac_step_file, mac_complete_file,
-              steps, final_prop, start_prop, inv_prop, limit, current_nb_sols):
+              steps, final_prop, start_prop, inv_prop, limit, current_nb_sols,
+              previous_frontier_places):
     """Search for many solutions, save timings, and save frontiers.
 
     For every new solution, the system is NOT reinitialized, and a satisfiability
@@ -307,12 +316,17 @@ def find_macs(mcla,
     :param limit: Limit the number of solutions.
     :param current_nb_sols: The current number of solutions already found.
         This number is used to limit the number of searched solutions.
+    :param previous_frontier_places: Set of frontier places tuples from previous
+        solutions. These tuples will be banned from the future solutions.
     :type limit: <int>
     :type current_nb_sols: <int>
+    :type previous_frontier_places: <set <tuple <str>>>
     :return: None
     """
     # Build query
     query = MCLSimpleQuery(start_prop, inv_prop, final_prop)
+    # Translate frontier places to their numerical values
+    query.dim_start = get_dimacs_start_properties(mcla, previous_frontier_places)
 
     # Iterate on solutions
     for i, frontier_sol in enumerate(mcla.mac_search(query, steps), current_nb_sols):
@@ -348,9 +362,9 @@ def find_macs(mcla,
 
 def find_mac(mcla,
              mac_file, mac_step_file, mac_complete_file,
-             steps, final_prop, start_prop, inv_prop):
+             steps, final_prop, start_prop, inv_prop, previous_frontier_places):
     """Search for 1 solution, save timings, save frontiers, and return it with
-    the current step.
+    the current step (deprecated, see find_macs()).
 
     For every new solution, the system is reinitialized, and a satisfiability
     test is made on a new query to evaluate the minimal number of steps for
@@ -361,11 +375,16 @@ def find_mac(mcla,
     the previous solutions for example) in text format is very expensive because
     realized by the grammar ANTLR.
 
+    :param previous_frontier_places: Set of frontier places tuples from previous
+        solutions. These tuples will be banned from the future solutions.
+    :type previous_frontier_places: <set <tuple <str>>>
     :return: A tuple of activated frontiers and the current step.
         None if there is no new Solution or if problem is not satisfiable.
     """
     # Build query
     query = MCLSimpleQuery(start_prop, inv_prop, final_prop)
+    # Translate frontier places to their numerical values
+    query.dim_start = get_dimacs_start_properties(mcla, previous_frontier_places)
 
     # Is the property reacheable ?
     reacheable = mcla.sq_is_satisfiable(query, steps)