Merge branch 'main' into 49-exploiting-constant-outputs-in-sat-formul…

…ation

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, num_subgraphs=args.num_subgraphs)
         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, num_subgraphs=args.num_subgraphs)
 
         if specs_obj.grid:
             stats_obj = explore_grid(specs_obj)
@@ -69,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'],

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

sxpat/arguments.py

@@ -104,6 +104,10 @@ 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
+        self.__num_subgraphs: int = tmp_args.num_subgraphs
+
+
 
     @property
     def parallel(self):
@@ -229,6 +233,14 @@ def sub_error_function(self):
     def et_partitioning(self):
         return self.__et_partitioning
 
+    @property
+    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',
@@ -401,9 +413,18 @@ def parse(cls) -> Arguments:
 
         #
         my_parser.add_argument('--et-partitioning',
-                               choices=['asc', 'desc'],
+                               choices=['asc', 'desc', 'smart_asc', 'smart_desc'],
                                default='asc')
 
+        my_parser.add_argument('--partial-labeling',
+                               action="store_true",
+                               default=False)
+
+        my_parser.add_argument('-num-subgraphs',
+                               type=int,
+                               default=1,
+                               help='the-number-of-attempts-for-subgraph-extractions')
+
         tmp_args = my_parser.parse_args()
 
         return Arguments(tmp_args)
@@ -437,4 +458,6 @@ 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.num_subgraphs = }\n' \
                f'{self.clean = }'

sxpat/config/config.py

@@ -35,6 +35,8 @@
 FULL_ERROR_FUNCTION = 'full_error_function'
 SUB_ERROR_FUNCTION = 'sub_error_function'
 ET_PARTITIONING = 'et_partitioning'
+PARTIAL_LABELING = 'partial_labeling'
+NUM_SUBGRAPHS = 'num_subgraphs'
 
 # shared
 SHARED = 'shared'

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: int, 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, 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()
@@ -72,33 +73,33 @@ 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=parallel)
     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=parallel)
 
     if constant_value == 0:
-        labels_false = z3py_obj.label_circuit(False)
-
-        # cleanup (folder z3/)
-        z3_folder, _ = OUTPUT_PATH['z3']
-        all_files = [f for f in os.listdir(z3_folder)]
-        for dir in all_files:
-            if os.path.isdir(f'{z3_folder}/{dir}') and re.search('labeling', dir):
-                shutil.rmtree(f'{z3_folder}/{dir}')
+        labels_false = z3py_obj.label_circuit(False, partial=partial, et=et)
 
         # 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 os.path.isdir(f'{report_folder}/{dir}') and re.search('labeling', dir):
+            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 re.search('labeling', dir) and os.path.isdir(f'{z3_folder}/{dir}'):
+                shutil.rmtree(f'{z3_folder}/{dir}')
+
         return labels_false, labels_false
 
     elif constant_value == 1:
-        labels_true = z3py_obj.label_circuit(True)
-
-        # cleanup (folder z3/)
+        labels_true = z3py_obj.label_circuit(True, partial=partial, et=et)
         folder, _ = OUTPUT_PATH['z3']
         all_files = [f for f in os.listdir(folder)]
         for dir in all_files:
@@ -108,10 +109,8 @@ def labeling_explicit(exact_benchmark_name: str, approximate_benchmark: str, con
         return labels_true, labels_true
 
     else:
-        labels_false = z3py_obj.label_circuit(False)
-        labels_true = z3py_obj.label_circuit(True)
-
-        # cleanup (folder z3/)
+        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)]
         for dir in all_files:

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):
@@ -593,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):
@@ -615,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)

sxpat/templateCreator.py

@@ -268,18 +268,23 @@ 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):
-        labels, _ = labeling_explicit(self.exact_benchmark, self.benchmark_name, 1, min_labeling)
+    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, parallel=parallel)
 
         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):
+    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:
@@ -1462,9 +1467,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:

sxpat/templateSpecs.py

@@ -36,6 +36,16 @@ 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]
+        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
 
     @property
     def keep_unsat_candidate(self):
@@ -217,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' \
@@ -247,4 +261,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'

sxpat/verification.py

@@ -93,3 +93,49 @@ 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)
+                        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