#60: added --top_grid option

.gitignore

@@ -31,5 +31,4 @@ Laura/
 .DS_Store
 
 #> Lollo testing
-Lollo/
-*.sh
+Lollo/

main.py

@@ -28,7 +28,7 @@ def main():
                                   sub_error_function=args.sub_error_function,
                                   et=args.et, et_partitioning=args.et_partitioning,
                                   partitioning_percentage=args.partitioning_percentage, iterations=args.iterations,
-                                  grid=args.grid, imax=args.imax, omax=args.omax, sensitivity=args.sensitivity,
+                                  grid=args.grid, top_grid=args.top_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,
@@ -55,18 +55,18 @@ def main():
                                   full_error_function=args.full_error_function, sub_error_function=args.sub_error_function,
                                   et=args.et, et_partitioning=args.et_partitioning,
                                   partitioning_percentage=args.partitioning_percentage, iterations=args.iterations,
-                                  grid=args.grid, imax=args.imax, omax=args.omax, sensitivity=args.sensitivity,
+                                  grid=args.grid, top_grid=args.top_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, encoding=args.encoding,
                                   partial_labeling=args.partial_labeling, num_subgraphs=args.num_subgraphs)
 
-        if specs_obj.grid:
+        if specs_obj.grid or specs_obj.top_grid:
             stats_obj = explore_grid(specs_obj)
 
         else:
             # todo:question: What should happen here?
-            raise NotImplementedError('WIP: for now --grid must be passed')
+            raise NotImplementedError('WIP: for now --grid or --top_grid must be passed')
 
 
 def clean_all():

sxpat/arguments.py

@@ -98,6 +98,7 @@ def __init__(self, tmp_args: argparse):
         self.__population: int = tmp_args.population
         self.__num_models: int = tmp_args.num_models
         self.__min_labeling: bool = tmp_args.min_labeling
+        self.__top_grid: bool = tmp_args.top_grid
         self.__shared: bool = tmp_args.shared
         self.__products_in_total: int = tmp_args.pit
         self.__parallel: bool = tmp_args.parallel
@@ -129,6 +130,10 @@ def shared(self):
     def min_labeling(self):
         return self.__min_labeling
 
+    @property
+    def top_grid(self):
+        return self.__top_grid
+
     @property
     def num_models(self):
         return self.__num_models
@@ -323,6 +328,10 @@ def parse(cls) -> Arguments:
                                action="store_true",
                                default=False)
 
+        my_parser.add_argument('--top_grid',
+                               action="store_true",
+                               default=False)                     
+
         my_parser.add_argument('--multiple',
                                action="store_true",
                                default=False)
@@ -461,6 +470,7 @@ def __repr__(self):
                f'{self.population = }\n' \
                f'{self.num_models = }\n'\
                f'{self.min_labeling = }\n' \
+               f'{self.top_grid = }\n' \
                f'{self.shared = }\n' \
                f'{self.parallel = }\n' \
                f'{self.full_error_function = }\n' \

sxpat/config/config.py

@@ -21,6 +21,7 @@
 PARTITIONING_PERCENTAGE = 'partitioning_percentage'
 ITERATIONS = 'iterations'
 GRID = 'grid'
+TOP_GRID = 'top_grid'
 EXACT = 'exact'
 IMAX = 'imax'
 OMAX = 'omax'

sxpat/templateSpecs.py

@@ -18,6 +18,7 @@ def __init__(self, **kwargs):
 
         self.__iterations = kwargs[ITERATIONS] if self.subxpat else 1
         self.__grid = kwargs[GRID]
+        self.__top_grid = kwargs[TOP_GRID]
         self.__imax = kwargs[IMAX]
         self.__omax = kwargs[OMAX]
         self.__max_sensitivity = kwargs[SENSITIVITY]
@@ -147,6 +148,10 @@ def iterations(self, this_iteration: int):
     @property
     def grid(self):
         return self.__grid
+
+    @property
+    def top_grid(self):
+        return self.__top_grid
 
     @property
     def imax(self):
@@ -282,6 +287,7 @@ def __repr__(self):
                f'{self.partitioning_percentage = }\n' \
                f'{self.iterations = }\n' \
                f'{self.grid = }\n' \
+               f'{self.top_grid = }\n' \
                f'{self.imax = }\n' \
                f'{self.omax = }\n' \
                f'{self.max_sensitivity = }\n' \

sxpat/template_manager/template_manager.py

@@ -584,6 +584,8 @@ def run(self) -> Sequence[Result]:
         os.remove(path_to_output)
         # SOP_QBF_Manager.output = open(path_to_output,'a')
         if result.strip()[-1] == '1':
+            time_taken = result.split('\n')[4]
+            # print(time_taken)
             res_dict = dict()
             for x in result.split('\n')[3][2:-2].split():
                 # SOP_QBF_Manager.output.write(f'{x} = ' + ('and()' if x[0] == '+' else 'or()') + '\n')
@@ -594,6 +596,8 @@ def run(self) -> Sequence[Result]:
                     res_dict[f'p_o{x[3:]}'] = True if x[0] == '+' else False
             return [Result(sxpat_cfg.SAT,res_dict)]
         else:
+            time_taken = result.split('\n')[3]
+            # print(time_taken)
             return [Result(sxpat_cfg.UNSAT,dict())]
 
 

sxpat/xplore.py

@@ -209,11 +209,23 @@ def explore_grid(specs_obj: TemplateSpecs):
             # explore the grid
             pprint.info2(f'Grid ({specs_obj.grid_param_1} X {specs_obj.grid_param_2}) and et={specs_obj.et} exploration started...')
             dominant_cells = []
+            # for top_grid
+            skip = False
+            stop_at_ppo = specs_obj.max_ppo
             for lpp, ppo in CellIterator.factory(specs_obj):
                 if is_dominated((lpp, ppo), dominant_cells):
                     pprint.info1(f'Cell({lpp},{ppo}) at iteration {i} -> DOMINATED')
                     continue
 
+                # for top_grid
+                if specs_obj.top_grid and ppo > stop_at_ppo:
+                    break
+                if skip and lpp < specs_obj.max_lpp:
+                    pprint.info1(f'Skipping Cell({lpp},{ppo})')
+                    continue
+                else:
+                    skip = False
+
                 # > cell step settings
 
                 # update the context
@@ -239,7 +251,9 @@ def explore_grid(specs_obj: TemplateSpecs):
                                             subxpat_v1_time=execution_time)
                     stats_obj.grid.cells[lpp][ppo].store_model_info(this_model_info)
                     pre_iter_unsats[candidate] += 1
-
+                    # for top_grid
+                    if specs_obj.top_grid and lpp == specs_obj.max_lpp:
+                        skip = True
                     if cur_status == UNKNOWN:
                         # store cell as dominant (to skip dominated subgrid)
                         dominant_cells.append((lpp, ppo))
@@ -327,6 +341,10 @@ def explore_grid(specs_obj: TemplateSpecs):
                     for key in current_population.keys():
                         pre_iter_unsats[key] = 0
 
+                    # for top_grid
+                    if specs_obj.top_grid and lpp == specs_obj.max_lpp:
+                        stop_at_ppo = ppo
+                        continue
                     # SAT found, stop grid exploration
                     break
                 prev_actual_error = 0
@@ -390,8 +408,13 @@ def non_shared(specs: TemplateSpecs) -> Iterator[Tuple[int, int]]:
 
         # grid cells
         for ppo in range(1, max_ppo + 1):
-            for lpp in range(1, max_lpp + 1):
-                yield (lpp, ppo)
+            if specs.top_grid:
+                yield (max_lpp, ppo)
+                for lpp in range(1, max_lpp):
+                    yield (lpp,ppo)
+            else:
+                for lpp in range(1, max_lpp + 1):
+                    yield (lpp, ppo)
 
 
 def is_dominated(coords: Tuple[int, int], dominant_cells: Iterable[Tuple[int, int]]) -> bool: