From 1b68d3c8ed4983a89b1f9609e412b56b1d30f17b Mon Sep 17 00:00:00 2001 From: Francesco Date: Fri, 26 Jul 2024 13:48:57 +0200 Subject: [PATCH] #49: Fixed problem with labeling (passing wrong graph and overwriting them); Fixed definition of approximate output constraints in template manager (defined get_preds_approx) --- sxpat/template_manager/template_manager.py | 3 +- sxpat/xplore.py | 36 ++++++++-------------- 2 files changed, 15 insertions(+), 24 deletions(-) diff --git a/sxpat/template_manager/template_manager.py b/sxpat/template_manager/template_manager.py index 4d6c2d492..5d66ce859 100644 --- a/sxpat/template_manager/template_manager.py +++ b/sxpat/template_manager/template_manager.py @@ -360,6 +360,7 @@ def _update_builder(self, builder: Builder) -> None: # exact_wires_constraints def get_preds(name: str) -> Collection[str]: return tuple(self._exact_graph.graph.predecessors(name)) + def get_preds_approx(name: str) -> Collection[str]: return tuple(self._current_graph.graph.predecessors(name)) def get_func(name: str) -> str: return self._exact_graph.graph.nodes[name][sxpat_cfg.LABEL] lines = [] for gate_i, gate_name in self.exact_gates.items(): @@ -401,7 +402,7 @@ def get_func(name: str) -> str: return self._exact_graph.graph.nodes[name][sxpat # approximate_output_constraints lines = [] for output_name in self.outputs.values(): - output_preds = get_preds(output_name) + output_preds = get_preds_approx(output_name) assert len(output_preds) == 1, 'an output must have exactly one predecessor' pred = self._use_approx_var(output_preds[0]) diff --git a/sxpat/xplore.py b/sxpat/xplore.py index a31d85300..353c281eb 100644 --- a/sxpat/xplore.py +++ b/sxpat/xplore.py @@ -59,7 +59,6 @@ def explore_grid(specs_obj: TemplateSpecs): i = 0 prev_actual_error = 0 prev_given_error = 0 - max_unsat_reached = False while (obtained_wce_exact < available_error): i += 1 @@ -78,22 +77,16 @@ def explore_grid(specs_obj: TemplateSpecs): else: raise NotImplementedError('invalid status') + if et > available_error or et < 0: + break + pprint.info1(f'iteration {i} with et {et}, available error {available_error}' if (specs_obj.subxpat or specs_obj.subxpat_v2) else f'Only one iteration with et {et}') - # Fix the infinite loop - if max_unsat_reached: - break - # for all candidates for candidate in current_population: - # guard - if pre_iter_unsats[candidate] == specs_obj.total_number_of_cells_per_iter and not specs_obj.keep_unsat_candidate: - pprint.info1(f'Number of UNSATs reached!') - max_unsat_reached = True - continue - + pprint.info1(f'candidate {candidate}') if candidate.endswith('.v'): specs_obj.benchmark_name = candidate[:-2] @@ -109,10 +102,10 @@ def explore_grid(specs_obj: TemplateSpecs): # label graph if specs_obj.max_sensitivity > 0 or specs_obj.mode >= 3: - et_coefficient = 8 + et_coefficient = 1 t_start = time.time() - label_graph(exact_graph, current_graph, + label_graph(current_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 @@ -207,11 +200,11 @@ 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, available_error) - obtained_wce_prev = erroreval_verification_wce(specs_obj.exact_benchmark, approximate_benchmark, available_error) + obtained_wce_exact = erroreval_verification_wce(exact_file_name, approximate_benchmark, et) + obtained_wce_prev = erroreval_verification_wce(specs_obj.exact_benchmark, approximate_benchmark, et) prev_actual_error = obtained_wce_prev - if obtained_wce_exact > available_error: + if obtained_wce_exact > et: stats_obj.store_grid() return stats_obj # raise Exception(color.error('ErrorEval Verification: FAILED!')) @@ -229,10 +222,6 @@ def explore_grid(specs_obj: TemplateSpecs): stats_obj.grid.cells[lpp][ppo].store_model_info(this_model_info) pprint.success(f'ErrorEval PASS! with total wce = {obtained_wce_exact}') - benchmark_name = specs_obj.benchmark_name - - # todo:check: this seems to be working, lets make sure - specs_obj.exact_benchmark = approximate_benchmark specs_obj.benchmark_name = approximate_benchmark synth_obj.set_path(z3logpath.OUTPUT_PATH['ver'], list(cur_model_results.keys())[0]) @@ -243,7 +232,7 @@ def explore_grid(specs_obj: TemplateSpecs): synth_obj.estimate_delay(exact_file_path)] print_current_model(cur_model_results, normalize=False, exact_stats=exact_stats) - store_current_model(cur_model_results, exact_stats=exact_stats, benchmark_name=benchmark_name, et=specs_obj.et, + store_current_model(cur_model_results, exact_stats=exact_stats, benchmark_name=specs_obj.benchmark_name, et=specs_obj.et, encoding=specs_obj.encoding, subgraph_extraction_time=subgraph_extraction_time, labeling_time=labeling_time) for key in cur_model_results.keys(): @@ -264,6 +253,7 @@ def explore_grid(specs_obj: TemplateSpecs): # SAT found, stop grid exploration break + prev_actual_error = 0 if exists_an_area_zero(current_population): break @@ -466,10 +456,10 @@ def display_the_tree(this_dict: Dict) -> None: # pass -def label_graph(exact_graph: AnnotatedGraph, current_graph: AnnotatedGraph, +def label_graph(current_graph: AnnotatedGraph, min_labeling: bool = False, partial: bool = False, et: int = -1, parallel: bool = False): - labels, _ = labeling_explicit(exact_graph.name, current_graph.name, + labels, _ = labeling_explicit(current_graph.name, current_graph.name, constant_value=0, min_labeling=min_labeling, partial=partial, et=et, parallel=parallel)