#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

@@ -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])

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)