From 5ba08d70b778e5a5377a49393149317258d7d17a Mon Sep 17 00:00:00 2001 From: Francesco Date: Thu, 25 Apr 2024 15:10:42 +0200 Subject: [PATCH 01/17] Added information on number of inputs and outputs for subgraph --- sxpat/stats.py | 12 ++++++++++++ sxpat/xplore.py | 8 ++++++++ 2 files changed, 20 insertions(+) diff --git a/sxpat/stats.py b/sxpat/stats.py index f3fb5bca2..edf594c31 100644 --- a/sxpat/stats.py +++ b/sxpat/stats.py @@ -53,6 +53,8 @@ def __init__(self, runtime: float = None, et: int = -1, labeling_time: float = -1, subgraph_extraction_time: float = -1, + subgraph_number_inputs: int = -1, + subgraph_number_outputs: int = -1, subxpat_phase1_time: float = -1, subxpat_phase2_time: float = -1): self.__cell = cell @@ -67,6 +69,8 @@ def __init__(self, runtime: float = None, self.__et = et self.__labeling_time = labeling_time self.__subgraph_extraction_time = subgraph_extraction_time + self.__subgraph_number_inputs = subgraph_number_inputs + self.__subgraph_number_outputs = subgraph_number_outputs self.__subxpat_phase1_time = subxpat_phase1_time self.__subxpat_phase2_time = subxpat_phase2_time self.__runtime = runtime @@ -86,6 +90,14 @@ def labeling_time(self): @property def subgraph_extraction_time(self): return self.__subgraph_extraction_time + + @property + def subgraph_number_inputs(self): + return self.__subgraph_number_inputs + + @property + def subgraph_number_outputs(self): + return self.__subgraph_number_outputs @property def subxpat_phase1_time(self): diff --git a/sxpat/xplore.py b/sxpat/xplore.py index fad6c9044..24383b11a 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -124,7 +124,11 @@ def explore_grid(specs_obj: TemplateSpecs): t_start = time.time() subgraph_is_available = template_obj.current_graph.extract_subgraph(specs_obj) subgraph_extraction_time = time.time() - t_start + subgraph_number_inputs = template_obj.current_graph.num_inputs + subgraph_number_outputs = template_obj.current_graph.num_outputs print(f'subgraph_extraction_time = {subgraph_extraction_time}') + print(f'subgraph_number_inputs = {subgraph_number_inputs}') + print(f'subgraph_number_outputs = {subgraph_number_outputs}') # todo:wip:marco: export subgraph folder = 'output/gv/subgraphs' @@ -190,6 +194,8 @@ def explore_grid(specs_obj: TemplateSpecs): this_model_info = Model(id=0, status=cur_status.upper(), cell=(lpp, ppo), et=et, iteration=i, labeling_time=labeling_time, subgraph_extraction_time=subgraph_extraction_time, + subgraph_number_inputs=subgraph_number_inputs, + subgraph_number_outputs=subgraph_number_outputs, subxpat_phase1_time=subxpat_phase1_time, subxpat_phase2_time=subxpat_phase2_time) stats_obj.grid.cells[lpp][ppo].store_model_info(this_model_info) @@ -235,6 +241,8 @@ def explore_grid(specs_obj: TemplateSpecs): delay=cur_model_results[synth_obj.ver_out_name][2], labeling_time=labeling_time, subgraph_extraction_time=subgraph_extraction_time, + subgraph_number_inputs=subgraph_number_inputs, + subgraph_number_outputs=subgraph_number_outputs, subxpat_phase1_time=subxpat_phase1_time, subxpat_phase2_time=subxpat_phase2_time) stats_obj.grid.cells[lpp][ppo].store_model_info(this_model) From 24e34a1844351d85f7a8fe0907f1910cac7b5c67 Mon Sep 17 00:00:00 2001 From: Francesco Date: Thu, 25 Apr 2024 16:33:24 +0200 Subject: [PATCH 02/17] Fixed saving of inputs and outputs of subgraph --- sxpat/xplore.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/sxpat/xplore.py b/sxpat/xplore.py index 24383b11a..7850274bd 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -124,8 +124,8 @@ def explore_grid(specs_obj: TemplateSpecs): t_start = time.time() subgraph_is_available = template_obj.current_graph.extract_subgraph(specs_obj) subgraph_extraction_time = time.time() - t_start - subgraph_number_inputs = template_obj.current_graph.num_inputs - subgraph_number_outputs = template_obj.current_graph.num_outputs + subgraph_number_inputs = template_obj.current_graph.subgraph_num_inputs + subgraph_number_outputs = template_obj.current_graph.subgraph_num_outputs print(f'subgraph_extraction_time = {subgraph_extraction_time}') print(f'subgraph_number_inputs = {subgraph_number_inputs}') print(f'subgraph_number_outputs = {subgraph_number_outputs}') From 59f21b4608e4bae042d2797214a2a982b57c2825 Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 26 Apr 2024 14:46:16 +0200 Subject: [PATCH 03/17] Added information to output file --- sxpat/stats.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/sxpat/stats.py b/sxpat/stats.py index edf594c31..60a6cfe76 100644 --- a/sxpat/stats.py +++ b/sxpat/stats.py @@ -605,7 +605,7 @@ def store_grid(self): # header = tuple(header) header = ('cell', 'iteration', 'model_id', 'status', 'runtime', 'area', 'delay', 'total_power', 'et', - 'labeling_time', 'subgraph_extraction', 'subxpat_phase1', 'subxpat_phase2') + 'labeling_time', 'subgraph_extraction', 'subgraph_inputs','subgraph_outputs', 'subxpat_phase1', 'subxpat_phase2') csvwriter.writerow(header) # iterate over cells (lppXppo) for ppo in range(self.ppo + 1): @@ -627,6 +627,8 @@ def store_grid(self): row.append(self.grid.cells[lpp][ppo].models[iteration][m_id].et) row.append(self.grid.cells[lpp][ppo].models[iteration][m_id].labeling_time) row.append(self.grid.cells[lpp][ppo].models[iteration][m_id].subgraph_extraction_time) + row.append(self.grid.cells[lpp][ppo].models[iteration][m_id].subgraph_number_inputs) + row.append(self.grid.cells[lpp][ppo].models[iteration][m_id].subgraph_number_outputs) row.append(self.grid.cells[lpp][ppo].models[iteration][m_id].subxpat_phase1_time) row.append(self.grid.cells[lpp][ppo].models[iteration][m_id].subxpat_phase2_time) row = tuple(row) From 2cd055b4671f89553323caef015496b3880ffe0a Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 10 May 2024 11:28:37 +0200 Subject: [PATCH 04/17] Added implementation of smart ascending and smart descending et partitioning --- sxpat/arguments.py | 2 +- sxpat/verification.py | 39 ++++++++++++++++++++++ sxpat/xplore.py | 76 +++++++++++++++++++++++++++++++++---------- 3 files changed, 98 insertions(+), 19 deletions(-) diff --git a/sxpat/arguments.py b/sxpat/arguments.py index 33a61bd44..88ef65dbc 100644 --- a/sxpat/arguments.py +++ b/sxpat/arguments.py @@ -401,7 +401,7 @@ def parse(cls) -> Arguments: # my_parser.add_argument('--et-partitioning', - choices=['asc', 'desc'], + choices=['asc', 'desc', 'smart_asc', 'smart_desc'], default='asc') tmp_args = my_parser.parse_args() diff --git a/sxpat/verification.py b/sxpat/verification.py index c5c2effad..be86e8f97 100644 --- a/sxpat/verification.py +++ b/sxpat/verification.py @@ -93,3 +93,42 @@ def erroreval_verification_explicit(exact_benchmark_name: str, approximate_bench 'w') as f: pass return False + +def erroreval_verification_wce(exact_benchmark_name: str, approximate_benchmark: str, et: int) -> int: + + # print(f'{approximate_benchmark = }') + verilog_obj_exact = Verilog(exact_benchmark_name) + verilog_obj_exact.export_circuit() + # + + verilog_obj_approx = Verilog(approximate_benchmark) + verilog_obj_approx.export_circuit() + # + convert_verilog_to_gv(exact_benchmark_name) + convert_verilog_to_gv(approximate_benchmark) + # + graph_obj_exact = Graph(exact_benchmark_name) + graph_obj_approx = Graph(approximate_benchmark) + # + graph_obj_exact.export_graph() + graph_obj_approx.export_graph() + + z3py_obj_qor = Z3solver(exact_benchmark_name, approximate_benchmark) + z3py_obj_qor.convert_gv_to_z3pyscript_maxerror_qor() + + z3py_obj_qor.export_z3pyscript() + z3py_obj_qor.run_z3pyscript_qor() + + # Compare the obtained WCE + folder, extension = z3logpath.OUTPUT_PATH['report'] + for csvfile in os.listdir(folder): + if csvfile.endswith(extension) and re.search(approximate_benchmark, csvfile): + report_file = f'{folder}/{csvfile}' + with open(report_file, 'r') as rf: + csvreader = csv.reader(rf) + for row in csvreader: + if row[0] == WCE: + obtained_wce = int(row[1]) + os.remove(report_file) + + return obtained_wce diff --git a/sxpat/xplore.py b/sxpat/xplore.py index fad6c9044..f1465ee78 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -17,7 +17,7 @@ from sxpat.config.config import * from sxpat.synthesis import Synthesis from sxpat.utils.filesystem import FS -from sxpat.verification import erroreval_verification_explicit +from sxpat.verification import erroreval_verification_explicit, erroreval_verification_wce from sxpat.stats import Stats, sxpatconfig, Model from z_marco.ma_graph import insert_subgraph, xpat_model_to_magraph, remove_subgraph @@ -54,6 +54,8 @@ def explore_grid(specs_obj: TemplateSpecs): # initial setup total_iterations = specs_obj.iterations exact_file_path = f"{INPUT_PATH['ver'][0]}/{specs_obj.exact_benchmark}.v" + exact_file_name = specs_obj.exact_benchmark + sum_wce_actual = 0 max_lpp = specs_obj.lpp max_ppo = specs_obj.pit if specs_obj.shared else specs_obj.ppo total_number_of_cells_per_iter = max_lpp * max_ppo + 1 @@ -75,20 +77,49 @@ def explore_grid(specs_obj: TemplateSpecs): total: Dict[Dict] = {} pre_iter_unsats: Dict = {specs_obj.benchmark_name: 0} - # define errors - if not specs_obj.subxpat_v2: - error_iterator = ((i+1, specs_obj.et) for i in range(total_iterations)) - elif specs_obj.et_partitioning == 'asc': - log2 = int(math.log2(specs_obj.et)) - error_iterator = ((i+1, 2**i) for i in range(log2)) - elif specs_obj.et_partitioning == 'desc': - log2 = int(math.log2(specs_obj.et)) - error_iterator = ((i+1, 2**(log2 - i - 1)) for i in range(log2)) - else: - raise NotImplementedError('invalid status') - - for i, et in error_iterator: - pprint.info1(f'iteration {i} with et {et}' + # # define errors + # if not specs_obj.subxpat_v2: + # error_iterator = ((i+1, specs_obj.et) for i in range(total_iterations)) + # elif specs_obj.et_partitioning == 'asc': + # log2 = int(math.log2(specs_obj.et)) + # error_iterator = ((i+1, 2**i) for i in range(log2)) + # elif specs_obj.et_partitioning == 'desc': + # log2 = int(math.log2(specs_obj.et)) + # error_iterator = ((i+1, 2**(log2 - i - 1)) for i in range(log2)) + # else: + # raise NotImplementedError('invalid status') + + available_error = specs_obj.et * 5 if not specs_obj.subxpat_v2 else specs_obj.et + total_error = available_error + actual_exact = 0 + i = 0 + prev_actual_error = 0 + prev_given_error = 0 + while(actual_exact <= available_error ): + # for i, et in error_iterator: + i += 1 + if not specs_obj.subxpat_v2: + et = specs_obj.et + elif specs_obj.et_partitioning == 'asc': + log2 = int(math.log2(specs_obj.et)) + et = 2**(i-1) + elif specs_obj.et_partitioning == 'desc': + log2 = int(math.log2(specs_obj.et)) + et = 2**(log2 - i - 2) + elif specs_obj.et_partitioning == 'smart_asc': + et = 1 if i == 1 else prev_given_error + (1 if prev_actual_error == 0 else 0) + if available_error < et*2: + et = available_error + prev_given_error = et + elif specs_obj.et_partitioning == 'smart_desc': + et = available_error if i == 1 else prev_given_error - (1 if prev_actual_error == 0 else 0) + if et > available_error: + et = available_error + prev_given_error = et + else: + raise NotImplementedError('invalid status') + + pprint.info1(f'iteration {i} with et {et}, available error {available_error}' if specs_obj.subxpat else f'Only one iteration with et {et}') @@ -136,6 +167,9 @@ def explore_grid(specs_obj: TemplateSpecs): # guard if not subgraph_is_available: pprint.warning(f'No subgraph available.') + prev_actual_error = 0 + if et == available_error: + available_error = 0 continue # run grid phase @@ -268,10 +302,16 @@ def explore_grid(specs_obj: TemplateSpecs): for candidate in cur_model_results: approximate_benchmark = candidate[:-2] + obtained_wce_exact = erroreval_verification_wce(exact_file_name, approximate_benchmark, template_obj.et) + actual_exact = obtained_wce_exact + obtained_wce_prev = erroreval_verification_wce(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et) + prev_actual_error = obtained_wce_prev + if not erroreval_verification_explicit(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et): raise Exception(color.error('ErrorEval Verification: FAILED!')) - - pprint.success('ErrorEval PASS! ') + + sum_wce_actual += obtained_wce_prev + pprint.success(f'ErrorEval PASS! with total wce = {obtained_wce_exact} and prev_wce = {obtained_wce_prev} with sum of prevs wce = {sum_wce_actual}') # todo:check: this seems to be working, lets make sure specs_obj.exact_benchmark = approximate_benchmark @@ -307,7 +347,7 @@ def explore_grid(specs_obj: TemplateSpecs): if exists_an_area_zero(current_population): break - + # available_error = total_error - obtained_wce_total display_the_tree(total) stats_obj.store_grid() From de5d2762d1f5fe3b5e0365702e1a46cf1fd49c7b Mon Sep 17 00:00:00 2001 From: MorellRAP Date: Mon, 13 May 2024 10:33:42 +0200 Subject: [PATCH 05/17] argument partial labeling added, z3log version 2.2.12, and partial labeling is integrated! --- main.py | 6 ++++-- requirements.txt | 2 +- sxpat/arguments.py | 12 ++++++++++++ sxpat/config/config.py | 1 + sxpat/labeling.py | 31 ++++++++++++++++--------------- sxpat/templateCreator.py | 7 +++++-- sxpat/templateSpecs.py | 7 +++++++ sxpat/xplore.py | 3 ++- 8 files changed, 48 insertions(+), 21 deletions(-) diff --git a/main.py b/main.py index 804cdb91e..35e896278 100644 --- a/main.py +++ b/main.py @@ -28,7 +28,8 @@ def main(): grid=args.grid, imax=args.imax, omax=args.omax, sensitivity=args.sensitivity, timeout=args.timeout, subgraph_size=args.subgraph_size, mode=args.mode, population=args.population, min_labeling=args.min_labeling, - shared=args.shared, products_in_total=args.pit, parallel=args.parallel) + shared=args.shared, products_in_total=args.pit, parallel=args.parallel, + partial_labeling=args.partial_labeling) stats_obj = Stats(specs_obj) stats_obj.gather_results() @@ -52,7 +53,8 @@ def main(): grid=args.grid, imax=args.imax, omax=args.omax, sensitivity=args.sensitivity, timeout=args.timeout, subgraph_size=args.subgraph_size, mode=args.mode, population=args.population, min_labeling=args.min_labeling, manual_nodes=args.manual_nodes, - shared=args.shared, products_in_total=args.pit, parallel=args.parallel) + shared=args.shared, products_in_total=args.pit, parallel=args.parallel, + partial_labeling=args.partial_labeling) if specs_obj.grid: stats_obj = explore_grid(specs_obj) diff --git a/requirements.txt b/requirements.txt index 6ab9a06b2..2f02ed621 100644 --- a/requirements.txt +++ b/requirements.txt @@ -26,4 +26,4 @@ tabulate==0.9.0 threadpoolctl==3.2.0 typing==3.7.4.3 z3-solver==4.11.2.0 -z3log==2.2.11 +z3log==2.2.12 diff --git a/sxpat/arguments.py b/sxpat/arguments.py index 88ef65dbc..34c7a258d 100644 --- a/sxpat/arguments.py +++ b/sxpat/arguments.py @@ -104,6 +104,9 @@ def __init__(self, tmp_args: argparse): self.__full_error_function: int = tmp_args.full_error_function self.__sub_error_function: int = tmp_args.sub_error_function self.__et_partitioning: int = tmp_args.et_partitioning + self.__partial_labeling: bool = tmp_args.partial_labeling + + @property def parallel(self): @@ -229,6 +232,10 @@ def sub_error_function(self): def et_partitioning(self): return self.__et_partitioning + @property + def partial_labeling(self): + return self.__partial_labeling + @classmethod def parse(cls) -> Arguments: my_parser = argparse.ArgumentParser(description='converts different formats to one another', @@ -404,6 +411,10 @@ def parse(cls) -> Arguments: choices=['asc', 'desc', 'smart_asc', 'smart_desc'], default='asc') + my_parser.add_argument('--partial-labeling', + action="store_true", + default=False) + tmp_args = my_parser.parse_args() return Arguments(tmp_args) @@ -437,4 +448,5 @@ def __repr__(self): f'{self.full_error_function = }\n' \ f'{self.sub_error_function = }\n' \ f'{self.et_partitioning = }\n' \ + f'{self.partial_labeling = }\n' \ f'{self.clean = }' diff --git a/sxpat/config/config.py b/sxpat/config/config.py index c9a6543db..4bdb143d3 100644 --- a/sxpat/config/config.py +++ b/sxpat/config/config.py @@ -35,6 +35,7 @@ FULL_ERROR_FUNCTION = 'full_error_function' SUB_ERROR_FUNCTION = 'sub_error_function' ET_PARTITIONING = 'et_partitioning' +PARTIAL_LABELING = 'partial_labeling' # shared SHARED = 'shared' diff --git a/sxpat/labeling.py b/sxpat/labeling.py index 4f4e14545..bd4829aea 100644 --- a/sxpat/labeling.py +++ b/sxpat/labeling.py @@ -52,7 +52,8 @@ def labeling(exact_benchmark_name: str, return labels -def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, constant_value: 0, min_labeling: bool) -> Dict: +def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, constant_value: 0, min_labeling: bool, + partial: bool = False, et: int = -1) -> Dict: # 1) create a clean verilog out of exact and approximate circuits verilog_obj_exact = Verilog(exact_benchmark_name) verilog_obj_exact.export_circuit() @@ -72,29 +73,29 @@ def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, con # convert gv to z3 expression if min_labeling: - z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, style='min') + z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, style='min', parallel=True) else: - z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE) + z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, parallel=True) if constant_value == 0: - labels_false = z3py_obj.label_circuit(False) + labels_false = z3py_obj.label_circuit(False, partial=partial, et=et) z3_folder, _ = OUTPUT_PATH['z3'] report_folder, _ = OUTPUT_PATH['report'] all_files = [f for f in os.listdir(z3_folder)] # print(f'{all_files = }') - for dir in all_files: - if os.path.isdir(f'{z3_folder}/{dir}') and re.search('labeling', dir): - shutil.rmtree(f'{z3_folder}/{dir}') - - all_files = [f for f in os.listdir(report_folder)] - for dir in all_files: - if os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir): - shutil.rmtree(f'{report_folder}/{dir}') + # for dir in all_files: + # if os.path.isdir(f'{z3_folder}/{dir}') and re.search('labeling', dir): + # shutil.rmtree(f'{z3_folder}/{dir}') + # + # all_files = [f for f in os.listdir(report_folder)] + # for dir in all_files: + # if os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir): + # shutil.rmtree(f'{report_folder}/{dir}') return labels_false, labels_false elif constant_value == 1: - labels_true = z3py_obj.label_circuit(True) + labels_true = z3py_obj.label_circuit(True, partial=partial, et=et) folder, _ = OUTPUT_PATH['z3'] all_files = [f for f in os.listdir(folder)] @@ -103,8 +104,8 @@ def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, con shutil.rmtree(f'{folder}/{dir}') return labels_true, labels_true else: - labels_false = z3py_obj.label_circuit(False) - labels_true = z3py_obj.label_circuit(True) + labels_false = z3py_obj.label_circuit(False, partial=partial, et=et) + labels_true = z3py_obj.label_circuit(True, partial=partial, et=et) folder, _ = OUTPUT_PATH['z3'] all_files = [f for f in os.listdir(folder)] diff --git a/sxpat/templateCreator.py b/sxpat/templateCreator.py index 3b263119a..dbc5f8941 100644 --- a/sxpat/templateCreator.py +++ b/sxpat/templateCreator.py @@ -268,13 +268,16 @@ def json_in_path(self): def json_in_path(self, this_json_path): self.__json_in_path = this_json_path - def label_graph(self, min_labeling: bool = False, parallel: bool = True): + def label_graph(self, min_labeling: bool = False, partial: bool = False, et: int = -1): # labels = labeling(self.exact_benchmark, self.benchmark_name, min_labeling, parallel) - labels, _ = labeling_explicit(self.exact_benchmark, self.benchmark_name, min_labeling, parallel) + labels, _ = labeling_explicit(self.exact_benchmark, self.benchmark_name, constant_value=0, min_labeling=min_labeling, + partial = partial, et = et) for n in self.current_graph.graph.nodes: if n in labels: self.current_graph.graph.nodes[n][WEIGHT] = int(labels[n]) + else: + self.current_graph.graph.nodes[n][WEIGHT] = int(-1) # TODO: Deprecated def label_graph_old(self, constant_value=2, min_labeling: bool = False): diff --git a/sxpat/templateSpecs.py b/sxpat/templateSpecs.py index 53af429bc..2b0462cf3 100644 --- a/sxpat/templateSpecs.py +++ b/sxpat/templateSpecs.py @@ -36,6 +36,12 @@ def __init__(self, **kwargs): self.et_partitioning: str = kwargs[ET_PARTITIONING] self.__keep_unsat_candidate: bool = self.__subxpat_v2 + self.__partial_labeling: bool = kwargs[PARTIAL_LABELING] + + + @property + def partial_labeling(self): + return self.__partial_labeling @property def keep_unsat_candidate(self): @@ -247,4 +253,5 @@ def __repr__(self): f'{self.full_error_function = }\n' \ f'{self.sub_error_function = }\n' \ f'{self.et_partitioning = }\n' \ + f'{self.partial_labeling = }\n' \ f'{self.keep_unsat_candidate = }\n' diff --git a/sxpat/xplore.py b/sxpat/xplore.py index f1465ee78..0766daa82 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -147,7 +147,8 @@ def explore_grid(specs_obj: TemplateSpecs): if specs_obj.max_sensitivity > 0 or specs_obj.mode >= 3: # label graph t_start = time.time() - template_obj.label_graph(min_labeling=specs_obj.min_labeling) + print(f'{et = }') + template_obj.label_graph(min_labeling=specs_obj.min_labeling, partial=specs_obj.partial_labeling, et=et) labeling_time = time.time() - t_start print(f'labeling_time = {labeling_time}') From 6d1ab9d70bca2aa925b9aec28e8c27cd7a39fecf Mon Sep 17 00:00:00 2001 From: MorellRAP Date: Tue, 14 May 2024 12:22:05 +0200 Subject: [PATCH 06/17] multiple subgraphs and penalty scoring added and tested! --- main.py | 6 +- sxpat/annotatedGraph.py | 345 ++++++++++++++++++++++++++++++++++++++++ sxpat/arguments.py | 11 ++ sxpat/config/config.py | 1 + sxpat/templateSpecs.py | 6 +- sxpat/xplore.py | 4 +- 6 files changed, 367 insertions(+), 6 deletions(-) diff --git a/main.py b/main.py index 35e896278..6f834ae9a 100644 --- a/main.py +++ b/main.py @@ -29,7 +29,7 @@ def main(): timeout=args.timeout, subgraph_size=args.subgraph_size, mode=args.mode, population=args.population, min_labeling=args.min_labeling, shared=args.shared, products_in_total=args.pit, parallel=args.parallel, - partial_labeling=args.partial_labeling) + partial_labeling=args.partial_labeling, num_subgraphs=args.num_subgraphs) stats_obj = Stats(specs_obj) stats_obj.gather_results() @@ -54,7 +54,7 @@ def main(): timeout=args.timeout, subgraph_size=args.subgraph_size, mode=args.mode, population=args.population, min_labeling=args.min_labeling, manual_nodes=args.manual_nodes, shared=args.shared, products_in_total=args.pit, parallel=args.parallel, - partial_labeling=args.partial_labeling) + partial_labeling=args.partial_labeling, num_subgraphs=args.num_subgraphs) if specs_obj.grid: stats_obj = explore_grid(specs_obj) @@ -71,7 +71,7 @@ def clean_all(): z3logpath.OUTPUT_PATH['z3'], z3logpath.OUTPUT_PATH['report'], z3logpath.OUTPUT_PATH['figure'], - z3logpath.LOG_PATH['yosys'], + # z3logpath.LOG_PATH['yosys'], z3logpath.TEST_PATH['tb'], sxpatpaths.OUTPUT_PATH['area'], sxpatpaths.OUTPUT_PATH['power'], diff --git a/sxpat/annotatedGraph.py b/sxpat/annotatedGraph.py index b5d7eea94..1dde46104 100644 --- a/sxpat/annotatedGraph.py +++ b/sxpat/annotatedGraph.py @@ -259,6 +259,15 @@ def extract_subgraph(self, specs_obj: TemplateSpecs): if self.subgraph.nodes[self.gate_dict[gate_idx]][SUBGRAPH] == 1: cnt_nodes += 1 + pprint.success(f" (#ofNodes={cnt_nodes})") + elif mode == 6: + pprint.info2(f"Partition with omax={specs_obj.omax} and soft feasibility constraints. Looking for largest partition") + self.subgraph = self.find_subgraph_feasible_soft(specs_obj) # Critian's subgraph extraction + cnt_nodes = 0 + for gate_idx in self.gate_dict: + if self.subgraph.nodes[self.gate_dict[gate_idx]][SUBGRAPH] == 1: + cnt_nodes += 1 + pprint.success(f" (#ofNodes={cnt_nodes})") else: raise Exception('invalid mode!') @@ -1693,6 +1702,342 @@ def find_subgraph_feasible_hard(self, specs_obj: TemplateSpecs): tmp_graph.nodes[self.gate_dict[gate_idx]][COLOR] = WHITE return tmp_graph + + def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): + """ + extracts a colored subgraph from the original non-partitioned graph object + :return: an annotated graph in which the extracted subgraph is colored + """ + omax = specs_obj.omax + feasibility_treshold = specs_obj.et + + + tmp_graph = self.graph.copy(as_view=False) + + input_literals = {} # literals associated to the input nodes + gate_literals = {} # literals associated to the gates in the circuit + output_literals = {} # literals associated to the output nodes + + # Data structures containing the edges + input_edges = {} # key = input node id, value = array of id. Contains id of gates in the circuit connected with the input node (childs) + gate_edges = {} # key = gate id, value = array of id. Contains the successors gate (childs) + output_edges = {} # key = output node id, value = array of id. Contains id of gates in the circuit connected with the output node (parents) + + # Optimizer + opt = Optimize() + + # Function to maximize + max_func = [] + + # List of all the partition edges + partition_input_edges = [] # list of all the input edges ([S'D_1 + S'D_2 + ..., ...]) + partition_output_edges = [] # list of all the output edges ([S_1D' + S_2D' + ..., ...]) + + # Generate all literals + for e in tmp_graph.edges: + if 'in' in e[0]: # Generate literal for each input node + in_id = int(e[0][2:]) + if in_id not in input_literals: + input_literals[in_id] = Bool("in_%s" % str(in_id)) + if 'g' in e[0]: # Generate literal for each gate in the circuit + g_id = int(e[0][1:]) + if g_id not in gate_literals and g_id not in self.constant_dict: # Not in constant_dict since we don't care about constants + gate_literals[g_id] = Bool("g_%s" % str(g_id)) + + if 'out' in e[1]: # Generate literal for each output node + out_id = int(e[1][3:]) + if out_id not in output_literals: + output_literals[out_id] = Bool("out_%s" % str(out_id)) + + # Generate structures holding edge information + for e in tmp_graph.edges: + if 'in' in e[0]: # Populate input_edges structure + in_id = int(e[0][2:]) + + if in_id not in input_edges: + input_edges[in_id] = [] + # input_edges[in_id].append(int(e[1][1:])) # this is a bug for a case where e = (in1, out1) + # Morteza added ============== + try: + input_edges[in_id].append(int(e[1][1:])) + except: + if re.search('g(\d+)', e[1]): + my_id = int(re.search('g(\d+)', e[1]).group(1)) + input_edges[in_id].append(my_id) + # ============================= + + if 'g' in e[0] and 'g' in e[1]: # Populate gate_edges structure + ns_id = int(e[0][1:]) + nd_id = int(e[1][1:]) + + if ns_id in self.constant_dict: + print("ERROR: Constants should only be connected to output nodes") + exit(0) + if ns_id not in gate_edges: + gate_edges[ns_id] = [] + # try: + gate_edges[ns_id].append(nd_id) + + if 'out' in e[1]: # Populate output_edges structure + out_id = int(e[1][3:]) + if out_id not in output_edges: + output_edges[out_id] = [] + # output_edges[out_id].append(int(e[0][1:])) + # Morteza added ============== + try: + output_edges[out_id].append(int(e[0][1:])) + except: + my_id = int(re.search('(\d+)', e[0]).group(1)) + output_edges[out_id].append(my_id) + + # ============================= + + + + + # Define input edges + for source in input_edges: + edge_in_holder = [] + edge_out_holder = [] + + for destination in input_edges[source]: + e_in = And(Not(input_literals[source]), gate_literals[destination]) + + edge_in_holder.append(e_in) + + partition_input_edges.append(Or(edge_in_holder)) + + # Define gate edges and data structures containing the edge weights + edge_w = {} + edge_constraint = {} + + for source in gate_edges: + edge_in_holder = [] + edge_out_holder = [] + + for destination in gate_edges[source]: + e_in = And(Not(gate_literals[source]), gate_literals[destination]) + e_out = And(gate_literals[source], Not(gate_literals[destination])) + + edge_in_holder.append(e_in) + edge_out_holder.append(e_out) + + partition_input_edges.append(Or(edge_in_holder)) + if source not in edge_w: + edge_w[source] = tmp_graph.nodes[self.gate_dict[source]][WEIGHT] + + if source not in edge_constraint: + edge_constraint[source] = Or(edge_out_holder) + partition_output_edges.append(Or(edge_out_holder)) + + # Define output edges + for output_id in output_edges: + predecessor = output_edges[output_id][ + 0] # Output nodes have only one predecessor (it could be a gate or it could be an input) + if predecessor not in gate_literals: # This handle cases where input and output are directly connected + continue + e_out = And(gate_literals[predecessor], Not(output_literals[output_id])) + if predecessor not in edge_w: + edge_w[predecessor] = tmp_graph.nodes[self.gate_dict[predecessor]][WEIGHT] + if predecessor not in edge_constraint: + edge_constraint[predecessor] = e_out + partition_output_edges.append(e_out) + + # Create graph of the cicuit without input and output nodes + G = nx.DiGraph() + # print(f'{tmp_graph.edges = }') + for e in tmp_graph.edges: + if 'g' in str(e[0]) and 'g' in str(e[1]): + source = int(e[0][1:]) + destination = int(e[1][1:]) + + G.add_edge(source, destination) + # Morteza added ===================== + for e in tmp_graph.edges: + if 'g' in str(e[0]): + source = int(e[0][1:]) + if source in self.constant_dict: + continue + G.add_node(source) + # =================================== + + # Generate structure with gate weights + # for n in self.graph.nodes: + # print(f'{self.graph.nodes[n][WEIGHT] = }, {n =}') + # print(f'{self.gate_dict = }') + gate_weight = {} + for gate_idx in G.nodes: + + if gate_idx not in gate_weight: + gate_weight[gate_idx] = tmp_graph.nodes[self.gate_dict[gate_idx]][WEIGHT] + # print("Gate", gate_idx, " value ", gate_weight[gate_idx]) + + descendants = {} + ancestors = {} + for n in G: + if n not in descendants: + descendants[n] = list(nx.descendants(G, n)) + if n not in ancestors: + ancestors[n] = list(nx.ancestors(G, n)) + + # Generate convexity constraints + for source in gate_edges: + for destination in gate_edges[source]: + if len(descendants[destination]) > 0: # Constraints on output edges + not_descendants = [Not(gate_literals[l]) for l in descendants[destination]] + not_descendants.append(Not(gate_literals[destination])) + descendat_condition = Implies(And(gate_literals[source], Not(gate_literals[destination])), + And(not_descendants)) + opt.add(descendat_condition) + if len(ancestors[source]) > 0: # Constraints on input edges + not_ancestors = [Not(gate_literals[l]) for l in ancestors[source]] + not_ancestors.append(Not(gate_literals[source])) + ancestor_condition = Implies(And(Not(gate_literals[source]), gate_literals[destination]), + And(not_ancestors)) + opt.add(ancestor_condition) + + # Set input nodes to False + for input_node_id in input_literals: + opt.add(input_literals[input_node_id] == False) + + # Set output nodes to False + for output_node_id in output_literals: + opt.add(output_literals[output_node_id] == False) + + # Add constraints on the number of output edges + opt.add(Sum(partition_output_edges) <= omax) + + feasibility_constraints = [] + for s in edge_w: + + if gate_weight[s] <= feasibility_treshold: + # print(s, "is feasible", gate_weight[s]) + feasibility_constraints.append(edge_constraint[s]) + + opt.add(Sum(feasibility_constraints) >= 1) + + # Generate function to maximize + for gate_id in gate_literals: + max_func.append(gate_literals[gate_id]) + # Add function to maximize to the solver + opt.maximize(Sum(max_func)) + # =========================== Skipping the nodes that are not labeled ================================ + skipped_nodes = [] + for node in self.graph.nodes: + if self.graph.nodes[node][WEIGHT] == -1: + if node.startswith('g'): + node_literal = f'{node[0:1]}_{node[1:]}' + elif node.startswith('in'): + node_literal = f'{node[0:2]}_{node[2:]}' + elif node.startswith('out'): + node_literal = f'{node[0:3]}_{node[3:]}' + else: + print(f'Node is neither input, output, nor gate') + raise + skipped_nodes.append(Bool(node_literal)) + skipped_nodes_constraints = [node_literal == False for node_literal in skipped_nodes] + opt.add(skipped_nodes_constraints) + + # ==================================================================================================== + + # =========================== Coming up with a penalty for each subgraph ============================= + penalty = Int('penalty') + output_individual_penalty = [] + penalty_coefficient = 1 + for s in edge_w: + output_individual_penalty.append(If(gate_weight[s] > feasibility_treshold, + penalty_coefficient * (gate_weight[s] - feasibility_treshold), + 0)) + opt.add(penalty == Sum(output_individual_penalty)) + opt.add_soft(Sum(output_individual_penalty) <= omax * feasibility_treshold, weight=1) + + # ======================================================== + + + + # ======================== Check for multiple subgraphs ======================================= + all_partitions = {} + count = specs_obj.num_subgraphs + while count > 0: + node_partition = [] + pprint.info1(f'Attempt {count}: ', end='') + c = opt.check() + if c == sat: + pprint.success(f"subgraph found -> SAT") + # print(opt.model()) + m = opt.model() + # print(f'{m = }') + for t in m.decls(): + if 'penalty' in str(t): + print(f'{t} = {m[t]}') + if 'g' not in str(t): # Look only the literals associate to the gates + continue + if is_true(m[t]): + gate_id = int(str(t)[2:]) + node_partition.append(gate_id) # Gates inside the partition + + + else: + pprint.warning("subgraph not found -> UNSAT") + count = 0 + # Check partition convexity + for i in range(len(node_partition) - 1): + for j in range(i + 1, len(node_partition)): + u = node_partition[i] + v = node_partition[j] + try: + path = nx.shortest_path(G, source=u, target=v) + all_nodes_in_partition = True + + # Check that all the nodes in the shortest path are in the partition + for n in path: + if n not in node_partition: + all_nodes_in_partition = False + + if not all_nodes_in_partition: + print("Partition is not convex") + exit(0) + + except nx.exception.NetworkXNoPath: + pass + + + + # ======================================================================== + if c == sat: + block_clause = [d() == True if m[d] else d() == False for d in m.decls() if 'g' in d.name()] + opt.add(Not(And(block_clause))) + current_penalty = m[penalty] + + all_partitions[count] = (current_penalty, node_partition) + count -= 1 + # ================================================================ + # =======================Pick the Subgraph with the lowest penalty ============================== + if all_partitions: + sorted_partitions = dict( + sorted( + all_partitions.items(), + key=lambda item: (item[1][0], -len(item[1][1])) + ) + ) + + + penalty, node_partition = next(iter(sorted_partitions.values())) + print(f'{penalty, node_partition}') + + # ================================================================ + + for gate_idx in self.gate_dict: + # print(f'{gate_idx = }') + if gate_idx in node_partition: + # print(f'{gate_idx} is in the node_partition') + tmp_graph.nodes[self.gate_dict[gate_idx]][SUBGRAPH] = 1 + tmp_graph.nodes[self.gate_dict[gate_idx]][COLOR] = RED + else: + tmp_graph.nodes[self.gate_dict[gate_idx]][SUBGRAPH] = 0 + tmp_graph.nodes[self.gate_dict[gate_idx]][COLOR] = WHITE + return tmp_graph + def entire_graph(self): tmp_graph = self.graph.copy() diff --git a/sxpat/arguments.py b/sxpat/arguments.py index 34c7a258d..11e9101d0 100644 --- a/sxpat/arguments.py +++ b/sxpat/arguments.py @@ -105,6 +105,7 @@ def __init__(self, tmp_args: argparse): self.__sub_error_function: int = tmp_args.sub_error_function self.__et_partitioning: int = tmp_args.et_partitioning self.__partial_labeling: bool = tmp_args.partial_labeling + self.__num_subgraphs: int = tmp_args.num_subgraphs @@ -236,6 +237,10 @@ def et_partitioning(self): def partial_labeling(self): return self.__partial_labeling + @property + def num_subgraphs(self): + return self.__num_subgraphs + @classmethod def parse(cls) -> Arguments: my_parser = argparse.ArgumentParser(description='converts different formats to one another', @@ -415,6 +420,11 @@ def parse(cls) -> Arguments: action="store_true", default=False) + my_parser.add_argument('-num-subgraphs', + type=int, + default=3, + help='the-number-of-attempts-for-subgraph-extractions') + tmp_args = my_parser.parse_args() return Arguments(tmp_args) @@ -449,4 +459,5 @@ def __repr__(self): f'{self.sub_error_function = }\n' \ f'{self.et_partitioning = }\n' \ f'{self.partial_labeling = }\n' \ + f'{self.num_subgraphs = }\n' \ f'{self.clean = }' diff --git a/sxpat/config/config.py b/sxpat/config/config.py index 4bdb143d3..36946f5a2 100644 --- a/sxpat/config/config.py +++ b/sxpat/config/config.py @@ -36,6 +36,7 @@ SUB_ERROR_FUNCTION = 'sub_error_function' ET_PARTITIONING = 'et_partitioning' PARTIAL_LABELING = 'partial_labeling' +NUM_SUBGRAPHS = 'num_subgraphs' # shared SHARED = 'shared' diff --git a/sxpat/templateSpecs.py b/sxpat/templateSpecs.py index 2b0462cf3..256bb4970 100644 --- a/sxpat/templateSpecs.py +++ b/sxpat/templateSpecs.py @@ -37,8 +37,10 @@ def __init__(self, **kwargs): self.__keep_unsat_candidate: bool = self.__subxpat_v2 self.__partial_labeling: bool = kwargs[PARTIAL_LABELING] - - + self.__num_subgraphs: int = kwargs[NUM_SUBGRAPHS] + @property + def num_subgraphs(self): + return self.__num_subgraphs @property def partial_labeling(self): return self.__partial_labeling diff --git a/sxpat/xplore.py b/sxpat/xplore.py index 0766daa82..6b0fe0a58 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -148,7 +148,7 @@ def explore_grid(specs_obj: TemplateSpecs): # label graph t_start = time.time() print(f'{et = }') - template_obj.label_graph(min_labeling=specs_obj.min_labeling, partial=specs_obj.partial_labeling, et=et) + template_obj.label_graph(min_labeling=specs_obj.min_labeling, partial=specs_obj.partial_labeling, et=2*et) labeling_time = time.time() - t_start print(f'labeling_time = {labeling_time}') @@ -158,6 +158,8 @@ def explore_grid(specs_obj: TemplateSpecs): subgraph_extraction_time = time.time() - t_start print(f'subgraph_extraction_time = {subgraph_extraction_time}') + + # todo:wip:marco: export subgraph folder = 'output/gv/subgraphs' graph_path = f'{folder}/{specs_obj.benchmark_name}_lpp{specs_obj.lpp}_ppo{specs_obj.ppo}_et{specs_obj.et}_mode{specs_obj.mode}_omax{specs_obj.omax}_serr{specs_obj.sub_error_function}.gv' From c88b5405c346a110be34720dd1569c1ee94e782c Mon Sep 17 00:00:00 2001 From: MorellRAP Date: Thu, 16 May 2024 15:12:03 +0200 Subject: [PATCH 07/17] penalty scoring debugged and made more accurate --- requirements.txt | 2 +- sxpat/annotatedGraph.py | 118 ++++++++++++++++++++++++++++++++++----- sxpat/labeling.py | 2 +- sxpat/templateCreator.py | 1 + sxpat/xplore.py | 3 +- 5 files changed, 109 insertions(+), 17 deletions(-) diff --git a/requirements.txt b/requirements.txt index 2f02ed621..5263f1c92 100644 --- a/requirements.txt +++ b/requirements.txt @@ -26,4 +26,4 @@ tabulate==0.9.0 threadpoolctl==3.2.0 typing==3.7.4.3 z3-solver==4.11.2.0 -z3log==2.2.12 +z3log==2.2.13 diff --git a/sxpat/annotatedGraph.py b/sxpat/annotatedGraph.py index 1dde46104..2cae2e128 100644 --- a/sxpat/annotatedGraph.py +++ b/sxpat/annotatedGraph.py @@ -504,6 +504,24 @@ def find_subgraph(self, specs_obj: TemplateSpecs): # Add function to maximize to the solver opt.maximize(Sum(max_func)) + # =========================== Skipping the nodes that are not labeled ================================ + skipped_nodes = [] + for node in self.graph.nodes: + if self.graph.nodes[node][WEIGHT] == -1: + if node.startswith('g'): + node_literal = f'{node[0:1]}_{node[1:]}' + elif node.startswith('in'): + node_literal = f'{node[0:2]}_{node[2:]}' + elif node.startswith('out'): + node_literal = f'{node[0:3]}_{node[3:]}' + else: + print(f'Node is neither input, output, nor gate') + raise + skipped_nodes.append(Bool(node_literal)) + skipped_nodes_constraints = [node_literal == False for node_literal in skipped_nodes] + opt.add(skipped_nodes_constraints) + # ==================================================================================================== + node_partition = [] if opt.check() == sat: pprint.success("subgraph found -> SAT ", end='') @@ -790,7 +808,23 @@ def find_subgraph_sensitivity(self, specs_obj: TemplateSpecs): # Add function to maximize to the solver opt.maximize(Sum(max_func)) - + # =========================== Skipping the nodes that are not labeled ================================ + skipped_nodes = [] + for node in self.graph.nodes: + if self.graph.nodes[node][WEIGHT] == -1: + if node.startswith('g'): + node_literal = f'{node[0:1]}_{node[1:]}' + elif node.startswith('in'): + node_literal = f'{node[0:2]}_{node[2:]}' + elif node.startswith('out'): + node_literal = f'{node[0:3]}_{node[3:]}' + else: + print(f'Node is neither input, output, nor gate') + raise + skipped_nodes.append(Bool(node_literal)) + skipped_nodes_constraints = [node_literal == False for node_literal in skipped_nodes] + opt.add(skipped_nodes_constraints) + # ==================================================================================================== node_partition = [] if opt.check() == sat: pprint.success("subgraph found -> SAT", end='') @@ -1077,6 +1111,24 @@ def find_subgraph_sensitivity_no_io_constraints(self, specs_obj: TemplateSpecs): # Add function to maximize to the solver opt.maximize(Sum(max_func)) + # =========================== Skipping the nodes that are not labeled ================================ + skipped_nodes = [] + for node in self.graph.nodes: + if self.graph.nodes[node][WEIGHT] == -1: + if node.startswith('g'): + node_literal = f'{node[0:1]}_{node[1:]}' + elif node.startswith('in'): + node_literal = f'{node[0:2]}_{node[2:]}' + elif node.startswith('out'): + node_literal = f'{node[0:3]}_{node[3:]}' + else: + print(f'Node is neither input, output, nor gate') + raise + skipped_nodes.append(Bool(node_literal)) + skipped_nodes_constraints = [node_literal == False for node_literal in skipped_nodes] + opt.add(skipped_nodes_constraints) + # ==================================================================================================== + node_partition = [] if opt.check() == sat: pprint.success("subgraph found -> SAT", end='') @@ -1359,7 +1411,23 @@ def find_subgraph_feasible(self, specs_obj: TemplateSpecs): # Add function to maximize to the solver opt.maximize(Sum(max_func)) - + # =========================== Skipping the nodes that are not labeled ================================ + skipped_nodes = [] + for node in self.graph.nodes: + if self.graph.nodes[node][WEIGHT] == -1: + if node.startswith('g'): + node_literal = f'{node[0:1]}_{node[1:]}' + elif node.startswith('in'): + node_literal = f'{node[0:2]}_{node[2:]}' + elif node.startswith('out'): + node_literal = f'{node[0:3]}_{node[3:]}' + else: + print(f'Node is neither input, output, nor gate') + raise + skipped_nodes.append(Bool(node_literal)) + skipped_nodes_constraints = [node_literal == False for node_literal in skipped_nodes] + opt.add(skipped_nodes_constraints) + # ==================================================================================================== node_partition = [] if opt.check() == sat: pprint.success("subgraph found -> SAT", end='') @@ -1643,6 +1711,24 @@ def find_subgraph_feasible_hard(self, specs_obj: TemplateSpecs): # Add function to maximize to the solver opt.maximize(Sum(max_func)) + # =========================== Skipping the nodes that are not labeled ================================ + skipped_nodes = [] + for node in self.graph.nodes: + if self.graph.nodes[node][WEIGHT] == -1: + if node.startswith('g'): + node_literal = f'{node[0:1]}_{node[1:]}' + elif node.startswith('in'): + node_literal = f'{node[0:2]}_{node[2:]}' + elif node.startswith('out'): + node_literal = f'{node[0:3]}_{node[3:]}' + else: + print(f'Node is neither input, output, nor gate') + raise + skipped_nodes.append(Bool(node_literal)) + skipped_nodes_constraints = [node_literal == False for node_literal in skipped_nodes] + opt.add(skipped_nodes_constraints) + # ==================================================================================================== + node_partition = [] if opt.check() == sat: pprint.success("subgraph found -> SAT", end='') @@ -1910,8 +1996,8 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): feasibility_constraints = [] for s in edge_w: - if gate_weight[s] <= feasibility_treshold: - # print(s, "is feasible", gate_weight[s]) + if gate_weight[s] <= feasibility_treshold and gate_weight[s] != -1: + print(s, "is feasible", gate_weight[s]) feasibility_constraints.append(edge_constraint[s]) opt.add(Sum(feasibility_constraints) >= 1) @@ -1920,7 +2006,9 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): for gate_id in gate_literals: max_func.append(gate_literals[gate_id]) # Add function to maximize to the solver + opt.maximize(Sum(max_func)) + # =========================== Skipping the nodes that are not labeled ================================ skipped_nodes = [] for node in self.graph.nodes: @@ -1942,19 +2030,20 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): # =========================== Coming up with a penalty for each subgraph ============================= penalty = Int('penalty') + output_individual_penalty = [] penalty_coefficient = 1 for s in edge_w: - output_individual_penalty.append(If(gate_weight[s] > feasibility_treshold, - penalty_coefficient * (gate_weight[s] - feasibility_treshold), - 0)) + if gate_weight[s] > feasibility_treshold: + output_individual_penalty.append(If(gate_literals[s], + penalty_coefficient * (gate_weight[s] - feasibility_treshold), + 0)) opt.add(penalty == Sum(output_individual_penalty)) - opt.add_soft(Sum(output_individual_penalty) <= omax * feasibility_treshold, weight=1) + opt.add_soft(Sum(output_individual_penalty) <= 2 * feasibility_treshold, weight=1) # ======================================================== - - + # opt.add(Sum(max_func) > 1) # ======================== Check for multiple subgraphs ======================================= all_partitions = {} count = specs_obj.num_subgraphs @@ -2007,8 +2096,8 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): if c == sat: block_clause = [d() == True if m[d] else d() == False for d in m.decls() if 'g' in d.name()] opt.add(Not(And(block_clause))) - current_penalty = m[penalty] - + current_penalty = m[penalty].as_long() + print(f'{current_penalty}, {node_partition}') all_partitions[count] = (current_penalty, node_partition) count -= 1 # ================================================================ @@ -2017,11 +2106,12 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): sorted_partitions = dict( sorted( all_partitions.items(), - key=lambda item: (item[1][0], -len(item[1][1])) + key=lambda item: (-len(item[1][1]), item[1][0]) ) ) - + for par in sorted_partitions: + print(f'{sorted_partitions[par] = }') penalty, node_partition = next(iter(sorted_partitions.values())) print(f'{penalty, node_partition}') diff --git a/sxpat/labeling.py b/sxpat/labeling.py index bd4829aea..20f6e1c2d 100644 --- a/sxpat/labeling.py +++ b/sxpat/labeling.py @@ -78,7 +78,7 @@ def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, con z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, parallel=True) if constant_value == 0: - + print(f'{et = }') labels_false = z3py_obj.label_circuit(False, partial=partial, et=et) z3_folder, _ = OUTPUT_PATH['z3'] report_folder, _ = OUTPUT_PATH['report'] diff --git a/sxpat/templateCreator.py b/sxpat/templateCreator.py index dbc5f8941..b99e21321 100644 --- a/sxpat/templateCreator.py +++ b/sxpat/templateCreator.py @@ -269,6 +269,7 @@ def json_in_path(self, this_json_path): self.__json_in_path = this_json_path def label_graph(self, min_labeling: bool = False, partial: bool = False, et: int = -1): + print(f'{et = } for partial labeling!') # labels = labeling(self.exact_benchmark, self.benchmark_name, min_labeling, parallel) labels, _ = labeling_explicit(self.exact_benchmark, self.benchmark_name, constant_value=0, min_labeling=min_labeling, partial = partial, et = et) diff --git a/sxpat/xplore.py b/sxpat/xplore.py index 6b0fe0a58..dbe28b386 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -148,7 +148,7 @@ def explore_grid(specs_obj: TemplateSpecs): # label graph t_start = time.time() print(f'{et = }') - template_obj.label_graph(min_labeling=specs_obj.min_labeling, partial=specs_obj.partial_labeling, et=2*et) + template_obj.label_graph(min_labeling=specs_obj.min_labeling, partial=specs_obj.partial_labeling, et=8*et) labeling_time = time.time() - t_start print(f'labeling_time = {labeling_time}') @@ -160,6 +160,7 @@ def explore_grid(specs_obj: TemplateSpecs): + # todo:wip:marco: export subgraph folder = 'output/gv/subgraphs' graph_path = f'{folder}/{specs_obj.benchmark_name}_lpp{specs_obj.lpp}_ppo{specs_obj.ppo}_et{specs_obj.et}_mode{specs_obj.mode}_omax{specs_obj.omax}_serr{specs_obj.sub_error_function}.gv' From 7969e4eb136695aea619ee2d0107ee14c014f4d6 Mon Sep 17 00:00:00 2001 From: MorellRAP Date: Fri, 17 May 2024 13:41:06 +0200 Subject: [PATCH 08/17] everything ready for the merge! --- sxpat/annotatedGraph.py | 1 - sxpat/xplore.py | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/sxpat/annotatedGraph.py b/sxpat/annotatedGraph.py index 2cae2e128..13adc303c 100644 --- a/sxpat/annotatedGraph.py +++ b/sxpat/annotatedGraph.py @@ -1992,7 +1992,6 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): # Add constraints on the number of output edges opt.add(Sum(partition_output_edges) <= omax) - feasibility_constraints = [] for s in edge_w: diff --git a/sxpat/xplore.py b/sxpat/xplore.py index dbe28b386..d208704eb 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -308,6 +308,7 @@ def explore_grid(specs_obj: TemplateSpecs): obtained_wce_exact = erroreval_verification_wce(exact_file_name, approximate_benchmark, template_obj.et) actual_exact = obtained_wce_exact + obtained_wce_prev = erroreval_verification_wce(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et) prev_actual_error = obtained_wce_prev From 722a9bbb2464c590c6ebbcd55a9fa2e8ca2770b6 Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 17 May 2024 13:45:54 +0200 Subject: [PATCH 09/17] Cleaned up smart partitoning conditions --- requirements.txt | 2 +- sxpat/xplore.py | 7 +++---- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/requirements.txt b/requirements.txt index 6ab9a06b2..5263f1c92 100644 --- a/requirements.txt +++ b/requirements.txt @@ -26,4 +26,4 @@ tabulate==0.9.0 threadpoolctl==3.2.0 typing==3.7.4.3 z3-solver==4.11.2.0 -z3log==2.2.11 +z3log==2.2.13 diff --git a/sxpat/xplore.py b/sxpat/xplore.py index f1465ee78..b58d70f1c 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -89,7 +89,7 @@ def explore_grid(specs_obj: TemplateSpecs): # else: # raise NotImplementedError('invalid status') - available_error = specs_obj.et * 5 if not specs_obj.subxpat_v2 else specs_obj.et + available_error = specs_obj.et total_error = available_error actual_exact = 0 i = 0 @@ -98,9 +98,7 @@ def explore_grid(specs_obj: TemplateSpecs): while(actual_exact <= available_error ): # for i, et in error_iterator: i += 1 - if not specs_obj.subxpat_v2: - et = specs_obj.et - elif specs_obj.et_partitioning == 'asc': + if specs_obj.et_partitioning == 'asc': log2 = int(math.log2(specs_obj.et)) et = 2**(i-1) elif specs_obj.et_partitioning == 'desc': @@ -183,6 +181,7 @@ def explore_grid(specs_obj: TemplateSpecs): print(f"p1_time = {subxpat_phase1_time:.6f}") if not success: + # TODO: Look into this in v2 pprint.warning(f'phase 1 failed with message: {message}') continue From 91c04c70778c882bf8a1c28b1166733044efeb7d Mon Sep 17 00:00:00 2001 From: MarcusTral Date: Fri, 17 May 2024 15:56:07 +0200 Subject: [PATCH 10/17] added requires_subgraph_extraction to specs, and updated usage --- sxpat/annotatedGraph.py | 10 +--------- sxpat/templateSpecs.py | 6 ++++++ 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/sxpat/annotatedGraph.py b/sxpat/annotatedGraph.py index 13adc303c..76135abfc 100644 --- a/sxpat/annotatedGraph.py +++ b/sxpat/annotatedGraph.py @@ -186,7 +186,7 @@ def extract_subgraph(self, specs_obj: TemplateSpecs): pprint.with_color(Fore.LIGHTYELLOW_EX)(f'No gates are found in the graph! Skipping the subgraph extraction') return False else: - if specs_obj.subxpat: + if specs_obj.requires_subgraph_extraction: mode = specs_obj.mode if mode == 1: pprint.info2(f"Partition with imax={specs_obj.imax} and omax={specs_obj.omax}. Looking for largest partition") @@ -1788,7 +1788,6 @@ def find_subgraph_feasible_hard(self, specs_obj: TemplateSpecs): tmp_graph.nodes[self.gate_dict[gate_idx]][COLOR] = WHITE return tmp_graph - def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): """ extracts a colored subgraph from the original non-partitioned graph object @@ -1797,7 +1796,6 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): omax = specs_obj.omax feasibility_treshold = specs_obj.et - tmp_graph = self.graph.copy(as_view=False) input_literals = {} # literals associated to the input nodes @@ -1878,9 +1876,6 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): # ============================= - - - # Define input edges for source in input_edges: edge_in_holder = [] @@ -2064,7 +2059,6 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): gate_id = int(str(t)[2:]) node_partition.append(gate_id) # Gates inside the partition - else: pprint.warning("subgraph not found -> UNSAT") count = 0 @@ -2089,8 +2083,6 @@ def find_subgraph_feasible_soft(self, specs_obj: TemplateSpecs): except nx.exception.NetworkXNoPath: pass - - # ======================================================================== if c == sat: block_clause = [d() == True if m[d] else d() == False for d in m.decls() if 'g' in d.name()] diff --git a/sxpat/templateSpecs.py b/sxpat/templateSpecs.py index 256bb4970..0bd6a9113 100644 --- a/sxpat/templateSpecs.py +++ b/sxpat/templateSpecs.py @@ -38,9 +38,11 @@ def __init__(self, **kwargs): self.__keep_unsat_candidate: bool = self.__subxpat_v2 self.__partial_labeling: bool = kwargs[PARTIAL_LABELING] self.__num_subgraphs: int = kwargs[NUM_SUBGRAPHS] + @property def num_subgraphs(self): return self.__num_subgraphs + @property def partial_labeling(self): return self.__partial_labeling @@ -225,6 +227,10 @@ def full_error_function(self): def sub_error_function(self): return self.__sub_error_function + @property + def requires_subgraph_extraction(self): + return self.__subxpat or self.__subxpat_v2 + def __repr__(self): return f'An object of Class TemplateSpecs:\n' \ f'{self.template_name = }\n' \ From 1cc02fbcd967af016c9fb7055c414de90ab5aed9 Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 17 May 2024 16:00:14 +0200 Subject: [PATCH 11/17] Finalized details of advanced et partitioning --- sxpat/xplore.py | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/sxpat/xplore.py b/sxpat/xplore.py index ae44662cd..dc21efb8a 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -95,8 +95,8 @@ def explore_grid(specs_obj: TemplateSpecs): i = 0 prev_actual_error = 0 prev_given_error = 0 - while(actual_exact <= available_error ): - # for i, et in error_iterator: + while (actual_exact <= available_error): + # for i, et in error_iterator: i += 1 if specs_obj.et_partitioning == 'asc': log2 = int(math.log2(specs_obj.et)) @@ -116,7 +116,7 @@ def explore_grid(specs_obj: TemplateSpecs): prev_given_error = et else: raise NotImplementedError('invalid status') - + pprint.info1(f'iteration {i} with et {et}, available error {available_error}' if specs_obj.subxpat else f'Only one iteration with et {et}') @@ -156,9 +156,6 @@ def explore_grid(specs_obj: TemplateSpecs): subgraph_extraction_time = time.time() - t_start print(f'subgraph_extraction_time = {subgraph_extraction_time}') - - - # todo:wip:marco: export subgraph folder = 'output/gv/subgraphs' graph_path = f'{folder}/{specs_obj.benchmark_name}_lpp{specs_obj.lpp}_ppo{specs_obj.ppo}_et{specs_obj.et}_mode{specs_obj.mode}_omax{specs_obj.omax}_serr{specs_obj.sub_error_function}.gv' @@ -166,7 +163,7 @@ def explore_grid(specs_obj: TemplateSpecs): template_obj.current_graph.export_annotated_graph(graph_path) print(f'subgraph exported at {graph_path}') - # guard + # guard if not subgraph_is_available: pprint.warning(f'No subgraph available.') prev_actual_error = 0 @@ -187,6 +184,9 @@ def explore_grid(specs_obj: TemplateSpecs): if not success: # TODO: Look into this in v2 pprint.warning(f'phase 1 failed with message: {message}') + prev_actual_error = 0 + if et == available_error: + available_error = 0 continue # explore the grid @@ -307,15 +307,18 @@ def explore_grid(specs_obj: TemplateSpecs): obtained_wce_exact = erroreval_verification_wce(exact_file_name, approximate_benchmark, template_obj.et) actual_exact = obtained_wce_exact - - obtained_wce_prev = erroreval_verification_wce(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et) - prev_actual_error = obtained_wce_prev + if specs_obj.subxpat_v2: + obtained_wce_prev = erroreval_verification_wce(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et) + prev_actual_error = obtained_wce_prev if not erroreval_verification_explicit(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et): raise Exception(color.error('ErrorEval Verification: FAILED!')) - - sum_wce_actual += obtained_wce_prev - pprint.success(f'ErrorEval PASS! with total wce = {obtained_wce_exact} and prev_wce = {obtained_wce_prev} with sum of prevs wce = {sum_wce_actual}') + + prev_string = '' + if specs_obj.subxpat_v2: + sum_wce_actual += obtained_wce_prev + prev_string = f' and prev_wce = {obtained_wce_prev} with sum of prevs wce = {sum_wce_actual}' + pprint.success(f'ErrorEval PASS! with total wce = {obtained_wce_exact}' + prev_string) # todo:check: this seems to be working, lets make sure specs_obj.exact_benchmark = approximate_benchmark From 2db39a926897f98da7e4fcf0aa66d8a458638ab5 Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 17 May 2024 16:04:58 +0200 Subject: [PATCH 12/17] Small printing fix --- sxpat/xplore.py | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) diff --git a/sxpat/xplore.py b/sxpat/xplore.py index dc21efb8a..447235441 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -77,20 +77,7 @@ def explore_grid(specs_obj: TemplateSpecs): total: Dict[Dict] = {} pre_iter_unsats: Dict = {specs_obj.benchmark_name: 0} - # # define errors - # if not specs_obj.subxpat_v2: - # error_iterator = ((i+1, specs_obj.et) for i in range(total_iterations)) - # elif specs_obj.et_partitioning == 'asc': - # log2 = int(math.log2(specs_obj.et)) - # error_iterator = ((i+1, 2**i) for i in range(log2)) - # elif specs_obj.et_partitioning == 'desc': - # log2 = int(math.log2(specs_obj.et)) - # error_iterator = ((i+1, 2**(log2 - i - 1)) for i in range(log2)) - # else: - # raise NotImplementedError('invalid status') - available_error = specs_obj.et - total_error = available_error actual_exact = 0 i = 0 prev_actual_error = 0 @@ -118,7 +105,7 @@ def explore_grid(specs_obj: TemplateSpecs): raise NotImplementedError('invalid status') pprint.info1(f'iteration {i} with et {et}, available error {available_error}' - if specs_obj.subxpat else + if (specs_obj.subxpat or specs_obj.subxpat_v2) else f'Only one iteration with et {et}') # for all candidates @@ -163,7 +150,7 @@ def explore_grid(specs_obj: TemplateSpecs): template_obj.current_graph.export_annotated_graph(graph_path) print(f'subgraph exported at {graph_path}') - # guard + # guard if not subgraph_is_available: pprint.warning(f'No subgraph available.') prev_actual_error = 0 From 22386cede85fe7e8eb61b7a215ae5f99420267c8 Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 17 May 2024 16:19:56 +0200 Subject: [PATCH 13/17] Changed mode number for partial labeling --- sxpat/annotatedGraph.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sxpat/annotatedGraph.py b/sxpat/annotatedGraph.py index 76135abfc..b1609373c 100644 --- a/sxpat/annotatedGraph.py +++ b/sxpat/annotatedGraph.py @@ -260,7 +260,7 @@ def extract_subgraph(self, specs_obj: TemplateSpecs): cnt_nodes += 1 pprint.success(f" (#ofNodes={cnt_nodes})") - elif mode == 6: + elif mode == 11: pprint.info2(f"Partition with omax={specs_obj.omax} and soft feasibility constraints. Looking for largest partition") self.subgraph = self.find_subgraph_feasible_soft(specs_obj) # Critian's subgraph extraction cnt_nodes = 0 From 25293c79c2d9c7c7e4458341427d98f028518004 Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 17 May 2024 16:55:41 +0200 Subject: [PATCH 14/17] Removed useless variable and comment, swapped to single erroreval_verification function --- sxpat/verification.py | 7 +++++++ sxpat/xplore.py | 8 +++----- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/sxpat/verification.py b/sxpat/verification.py index be86e8f97..5366222a5 100644 --- a/sxpat/verification.py +++ b/sxpat/verification.py @@ -130,5 +130,12 @@ def erroreval_verification_wce(exact_benchmark_name: str, approximate_benchmark: if row[0] == WCE: obtained_wce = int(row[1]) os.remove(report_file) + if obtained_wce > et: + print(Fore.RED + f'ERROR!!! The obtained WCE does not match the given error threshold!') + print(f'{obtained_wce = } > ET = {et}' + Style.RESET_ALL) + with open( + f'output/report/FAILED_{approximate_benchmark}.txt', + 'w') as f: + pass return obtained_wce diff --git a/sxpat/xplore.py b/sxpat/xplore.py index b5da4edd7..8a7c46aa2 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -78,11 +78,11 @@ def explore_grid(specs_obj: TemplateSpecs): pre_iter_unsats: Dict = {specs_obj.benchmark_name: 0} available_error = specs_obj.et - actual_exact = 0 + obtained_wce_exact = 0 i = 0 prev_actual_error = 0 prev_given_error = 0 - while (actual_exact <= available_error): + while (obtained_wce_exact <= available_error): # for i, et in error_iterator: i += 1 if specs_obj.et_partitioning == 'asc': @@ -301,12 +301,11 @@ def explore_grid(specs_obj: TemplateSpecs): approximate_benchmark = candidate[:-2] obtained_wce_exact = erroreval_verification_wce(exact_file_name, approximate_benchmark, template_obj.et) - actual_exact = obtained_wce_exact if specs_obj.subxpat_v2: obtained_wce_prev = erroreval_verification_wce(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et) prev_actual_error = obtained_wce_prev - if not erroreval_verification_explicit(specs_obj.exact_benchmark, approximate_benchmark, template_obj.et): + if obtained_wce_exact > template_obj.et: raise Exception(color.error('ErrorEval Verification: FAILED!')) prev_string = '' @@ -349,7 +348,6 @@ def explore_grid(specs_obj: TemplateSpecs): if exists_an_area_zero(current_population): break - # available_error = total_error - obtained_wce_total display_the_tree(total) stats_obj.store_grid() From 2b4db08ace4bf5a1eeef5195518f5447d5b65aa2 Mon Sep 17 00:00:00 2001 From: MorellRAP Date: Tue, 21 May 2024 11:36:56 +0200 Subject: [PATCH 15/17] cleaning up labeling reports --- sxpat/labeling.py | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/sxpat/labeling.py b/sxpat/labeling.py index 20f6e1c2d..ffeecd3e3 100644 --- a/sxpat/labeling.py +++ b/sxpat/labeling.py @@ -83,15 +83,15 @@ def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, con z3_folder, _ = OUTPUT_PATH['z3'] report_folder, _ = OUTPUT_PATH['report'] all_files = [f for f in os.listdir(z3_folder)] - # print(f'{all_files = }') - # for dir in all_files: - # if os.path.isdir(f'{z3_folder}/{dir}') and re.search('labeling', dir): - # shutil.rmtree(f'{z3_folder}/{dir}') - # - # all_files = [f for f in os.listdir(report_folder)] - # for dir in all_files: - # if os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir): - # shutil.rmtree(f'{report_folder}/{dir}') + print(f'{all_files = }') + for dir in all_files: + if os.path.isdir(f'{z3_folder}/{dir}') and re.search('labeling', dir): + shutil.rmtree(f'{z3_folder}/{dir}') + + all_files = [f for f in os.listdir(report_folder)] + for dir in all_files: + if os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir): + shutil.rmtree(f'{report_folder}/{dir}') return labels_false, labels_false elif constant_value == 1: From e670578dae91705b8f4355c7b8935d7c2b9944dd Mon Sep 17 00:00:00 2001 From: MorellRAP Date: Tue, 21 May 2024 11:41:41 +0200 Subject: [PATCH 16/17] labeling reports are cleaned! --- sxpat/labeling.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/sxpat/labeling.py b/sxpat/labeling.py index 0d45a64af..2e8597e15 100644 --- a/sxpat/labeling.py +++ b/sxpat/labeling.py @@ -78,19 +78,19 @@ def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, con z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, parallel=True) if constant_value == 0: - print(f'{et = }') + labels_false = z3py_obj.label_circuit(False, partial=partial, et=et) - z3_folder, _ = OUTPUT_PATH['z3'] + z3_folder, _ = OUTPUT_PATH['report'] all_files = [f for f in os.listdir(z3_folder)] - print(f'{all_files = }') + print(f'{all_files= }') for dir in all_files: if os.path.isdir(f'{z3_folder}/{dir}') and re.search('labeling', dir): shutil.rmtree(f'{z3_folder}/{dir}') - all_files = [f for f in os.listdir(report_folder)] - for dir in all_files: - if os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir): - shutil.rmtree(f'{report_folder}/{dir}') + # all_files = [f for f in os.listdir(report_folder)] + # for dir in all_files: + # if os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir): + # shutil.rmtree(f'{report_folder}/{dir}') return labels_false, labels_false From fbdd59fa040fadd193914c6e7047b74f28a1b145 Mon Sep 17 00:00:00 2001 From: MarcusTral Date: Tue, 21 May 2024 15:02:34 +0200 Subject: [PATCH 17/17] implemented changes from PR #50 --- sxpat/arguments.py | 2 +- sxpat/labeling.py | 26 +++++++++++++++----------- sxpat/templateCreator.py | 13 +++++++------ sxpat/xplore.py | 3 ++- 4 files changed, 25 insertions(+), 19 deletions(-) diff --git a/sxpat/arguments.py b/sxpat/arguments.py index ca6b95b0f..59c9b99aa 100644 --- a/sxpat/arguments.py +++ b/sxpat/arguments.py @@ -422,7 +422,7 @@ def parse(cls) -> Arguments: my_parser.add_argument('-num-subgraphs', type=int, - default=3, + default=1, help='the-number-of-attempts-for-subgraph-extractions') tmp_args = my_parser.parse_args() diff --git a/sxpat/labeling.py b/sxpat/labeling.py index 2e8597e15..59c4fa5d0 100644 --- a/sxpat/labeling.py +++ b/sxpat/labeling.py @@ -53,7 +53,7 @@ def labeling(exact_benchmark_name: str, def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, constant_value: 0, min_labeling: bool, - partial: bool = False, et: int = -1) -> Dict: + partial: bool = False, et: int = -1, parallel: bool = False) -> Dict: # 1) create a clean verilog out of exact and approximate circuits verilog_obj_exact = Verilog(exact_benchmark_name) verilog_obj_exact.export_circuit() @@ -73,25 +73,29 @@ def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, con # convert gv to z3 expression if min_labeling: - z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, style='min', parallel=True) + z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, style='min', parallel=parallel) else: - z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, parallel=True) + z3py_obj = Z3solver(exact_benchmark_name, approximate_benchmark, experiment=SINGLE, optimization=MAXIMIZE, parallel=parallel) if constant_value == 0: - labels_false = z3py_obj.label_circuit(False, partial=partial, et=et) - z3_folder, _ = OUTPUT_PATH['report'] + + # cleanup (folder report/) + report_folder, _ = OUTPUT_PATH['report'] + all_files = [f for f in os.listdir(report_folder)] + print(f'{all_files= }') + for dir in all_files: + if re.search('labeling', dir) and os.path.isdir(f'{report_folder}/{dir}'): + shutil.rmtree(f'{report_folder}/{dir}') + + # cleanup (folder z3/) + z3_folder, _ = OUTPUT_PATH['z3'] all_files = [f for f in os.listdir(z3_folder)] print(f'{all_files= }') for dir in all_files: - if os.path.isdir(f'{z3_folder}/{dir}') and re.search('labeling', dir): + if re.search('labeling', dir) and os.path.isdir(f'{z3_folder}/{dir}'): shutil.rmtree(f'{z3_folder}/{dir}') - # all_files = [f for f in os.listdir(report_folder)] - # for dir in all_files: - # if os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir): - # shutil.rmtree(f'{report_folder}/{dir}') - return labels_false, labels_false elif constant_value == 1: diff --git a/sxpat/templateCreator.py b/sxpat/templateCreator.py index b99e21321..053542335 100644 --- a/sxpat/templateCreator.py +++ b/sxpat/templateCreator.py @@ -268,11 +268,11 @@ def json_in_path(self): def json_in_path(self, this_json_path): self.__json_in_path = this_json_path - def label_graph(self, min_labeling: bool = False, partial: bool = False, et: int = -1): + def label_graph(self, min_labeling: bool = False, partial: bool = False, et: int = -1, parallel: bool = False): print(f'{et = } for partial labeling!') # labels = labeling(self.exact_benchmark, self.benchmark_name, min_labeling, parallel) labels, _ = labeling_explicit(self.exact_benchmark, self.benchmark_name, constant_value=0, min_labeling=min_labeling, - partial = partial, et = et) + partial=partial, et=et, parallel=parallel) for n in self.current_graph.graph.nodes: if n in labels: @@ -281,10 +281,10 @@ def label_graph(self, min_labeling: bool = False, partial: bool = False, et: in self.current_graph.graph.nodes[n][WEIGHT] = int(-1) # TODO: Deprecated - def label_graph_old(self, constant_value=2, min_labeling: bool = False): + def label_graph_old(self, constant_value=2, min_labeling: bool = False, parallel: bool = False): """ ~ DEPRECATED ~ """ print(Fore.BLUE + f'labeling...' + Style.RESET_ALL) - labels1, labels0 = labeling_explicit(self.exact_benchmark, self.benchmark_name, constant_value, min_labeling) + labels1, labels0 = labeling_explicit(self.exact_benchmark, self.benchmark_name, constant_value, min_labeling, parallel=parallel) for n in self.current_graph.graph.nodes: if n in labels0 and n in labels1: if constant_value == 0: @@ -1564,9 +1564,10 @@ def label_graph(self, min_labeling: bool = False, parallel: bool = True): self.current_graph.graph.nodes[n][WEIGHT] = int(labels[n]) # TODO: Deprecated - def label_graph_old(self, constant_value=2, min_labeling: bool = False): + def label_graph_old(self, constant_value=2, min_labeling: bool = False, parallel: bool = False): + print(Fore.BLUE + f'labeling...' + Style.RESET_ALL) - labels1, labels0 = labeling_explicit(self.exact_benchmark, self.benchmark_name, constant_value, min_labeling) + labels1, labels0 = labeling_explicit(self.exact_benchmark, self.benchmark_name, constant_value, min_labeling, parallel=parallel) for n in self.current_graph.graph.nodes: if n in labels0 and n in labels1: if constant_value == 0: diff --git a/sxpat/xplore.py b/sxpat/xplore.py index 8a7c46aa2..8e3f359aa 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -133,7 +133,8 @@ def explore_grid(specs_obj: TemplateSpecs): # label graph t_start = time.time() print(f'{et = }') - template_obj.label_graph(min_labeling=specs_obj.min_labeling, partial=specs_obj.partial_labeling, et=8*et) + et_coefficient = 8 + template_obj.label_graph(min_labeling=specs_obj.min_labeling, partial=specs_obj.partial_labeling, et=et*et_coefficient, parallel=specs_obj.parallel) labeling_time = time.time() - t_start print(f'labeling_time = {labeling_time}')