From a0d2356700712d26a4bf6cc5778c8628b2d7464e Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Mon, 25 Nov 2019 20:19:36 +0100
Subject: [PATCH] [cmd] Implement & Refactor the conversion of previous
frontier places to numerical values => big perf gain
---
command_line/cadbiom_cmd/solution_search.py | 63 ++++++++++++++-------
1 file changed, 41 insertions(+), 22 deletions(-)
diff --git a/command_line/cadbiom_cmd/solution_search.py b/command_line/cadbiom_cmd/solution_search.py
index 8a44852..71456bb 100644
--- a/command_line/cadbiom_cmd/solution_search.py
+++ b/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)
--
GitLab