Merge branch '56-templatecreator-hierarchy' into 56.2-testing

sxpat/stats.py

@@ -287,10 +287,11 @@ class Grid:
     def __init__(self, spec_obj: TemplateSpecs):
         self.__exact_name: str = spec_obj.exact_benchmark
         self.__approximate_name: str = spec_obj.benchmark_name
-        self.__lpp: int = spec_obj.max_lpp
         if spec_obj.shared:
+            self.__lpp: int = spec_obj.max_its
             self.__ppo: int = spec_obj.max_pit
         else:
+            self.__lpp: int = spec_obj.max_lpp
             self.__ppo: int = spec_obj.max_ppo
         self.__et: int = spec_obj.et
 
@@ -354,12 +355,11 @@ def __init__(self, spec_obj: TemplateSpecs):
         self.__template_name = spec_obj.template_name
         self.__exact_name: str = spec_obj.exact_benchmark
         self.__approximate_name: str = spec_obj.benchmark_name
-        self.__lpp: int = spec_obj.max_lpp
-
-        self.__pit: int = spec_obj.max_pit
         if spec_obj.shared:
+            self.__lpp: int = spec_obj.max_its
             self.__ppo: int = spec_obj.max_pit
         else:
+            self.__lpp: int = spec_obj.max_lpp
             self.__ppo: int = spec_obj.max_ppo
         self.__et: int = spec_obj.et
         self.__shared: bool = spec_obj.shared
@@ -404,10 +404,6 @@ def tool_name(self):
     def template_name(self):
         return self.__template_name
 
-    @property
-    def pit(self):
-        return self.__pit
-
     @property
     def shared(self):
         return self.__shared
@@ -558,7 +554,7 @@ def get_grid_name(self):
 
         # let's divide our nomenclature into X parts: head (common), technique_specific, tail (common)
 
-        head = f'grid_{self.exact_name}_{self.lpp}X{self.pit if self.specs.shared else self.ppo}_et{self.et}_'
+        head = f'grid_{self.exact_name}_{self.lpp}X{self.ppo}_et{self.et}_'
 
         technique_specific = f'{self.tool_name}_{self.specs.et_partitioning if self.tool_name == sxpatconfig.SUBXPAT_V2 else ""}_'
         technique_specific += f'enc{self.specs.encoding}_'

sxpat/synthesis.py

@@ -33,8 +33,8 @@ def __init__(self, template_specs: TemplateSpecs, graph_obj: AnnotatedGraph = No
         self.__shared: bool = template_specs.shared
 
         self.__iterations = template_specs.iterations
-        self.__literal_per_product = template_specs.lpp
-        self.__product_per_output = template_specs.ppo
+        self.__literals_per_product = template_specs.lpp
+        self.__products_per_output = template_specs.ppo
         self.__error_threshold = template_specs.et
         self.__graph: AnnotatedGraph = graph_obj
         self.__magraph: Optional[MaGraph] = magraph
@@ -43,7 +43,7 @@ def __init__(self, template_specs: TemplateSpecs, graph_obj: AnnotatedGraph = No
         self.__num_models: int = template_specs.num_of_models
 
         if self.shared:
-            self.__products_in_total: int = template_specs.products_in_total
+            self.__products_in_total: int = template_specs.pit
         else:
             self.__products_in_total: float = float('inf')
 
@@ -120,19 +120,19 @@ def json_model(self):
 
     @property
     def literals_per_product(self):
-        return self.__literal_per_product
+        return self.__literals_per_product
 
     @property
     def lpp(self):
-        return self.__literal_per_product
+        return self.__literals_per_product
 
     @property
     def products_per_output(self):
-        return self.__product_per_output
+        return self.__products_per_output
 
     @property
     def ppo(self):
-        return self.__product_per_output
+        return self.__products_per_output
 
     @property
     def template_name(self):

sxpat/template_manager/template.py

@@ -28,6 +28,7 @@ def z3_abs_diff(a, b):
 
 # Parameters variables declaration
 {{{{params_declaration}}}}
+params_list = {{{{params_list}}}}
 
 # wires functions declaration for exact circuit
 {{{{exact_wires_declaration}}}}
@@ -209,9 +210,7 @@ def key_function(parameter_constraint):
 		'attempts_times': [list(map(lambda tup: [*tup], attempts_times))]
 	}
 	if result == sat:
-		data_object['model'] = dict(map(lambda item: (str(item[0]), is_true(item[1])),
-			sorted(parameters_constraints,
-			key=key_function)))
+		data_object['model'] = {str(p): is_true(m[p]) for p in params_list}
 	found_data.append(data_object)
 	if result != sat:
 		break

sxpat/template_manager/template_manager.py

@@ -1,34 +1,22 @@
 from __future__ import annotations
-from abc import abstractmethod
+from typing import Callable, Collection, Dict, Iterable, Sequence, Tuple
 import dataclasses as dc
+
+from abc import abstractmethod
+
 import functools
 import itertools
+
 import json
-import pathlib
 import re
 import subprocess
-from typing import Any, Callable, Collection, Dict, Iterable, Iterator, Mapping, Sequence, Tuple, Union
 
 from sxpat.annotatedGraph import AnnotatedGraph
 import sxpat.config.config as sxpat_cfg
 import sxpat.config.paths as sxpat_paths
 from sxpat.templateSpecs import TemplateSpecs
 from .encoding import Encoding
-
-
-NOTHING = object()
-
-
-def mapping_inv(mapping: Mapping, value: Any, default: Any = NOTHING) -> Any:
-    key = next((k for (k, v) in mapping.items() if v == value), default)
-    if key is NOTHING:
-        raise ValueError('The value does not match with any pair in the mapping.')
-    return key
-
-
-def pairwise_iter(iterable: Iterable) -> Iterator:
-    """iterate pair-wise (AB, BC, CD, ...)"""
-    return zip(iterable, itertools.islice(iterable, 1, None))
+from utils.collections import mapping_inv, pairwise_iter
 
 
 @dc.dataclass
@@ -38,13 +26,6 @@ class Result:
 
 
 class TemplateManager:
-    def __init__(self, exact_graph: AnnotatedGraph, current_graph: AnnotatedGraph,
-                 specs: TemplateSpecs, encoding: Encoding) -> None:
-        self._exact_graph = exact_graph
-        self._current_graph = current_graph
-        self._specs = specs
-        self._encoding = encoding
-
     @staticmethod
     def factory(specs: TemplateSpecs,
                 exact_graph: AnnotatedGraph,
@@ -59,15 +40,39 @@ def factory(specs: TemplateSpecs,
 
         # select and return TemplateManager object
         return {
-            False: SOPManager,
-            True: SOPSManager,
-        }[specs.shared](
+            (False, 1): SOPManager,
+            (False, 2): SOPManager,
+            (True, 1): SOPSManager,
+            (True, 2): SOPSManager,
+            (False, 3): SOP_QBF_Manager,
+        }[specs.shared, specs.encoding](
             exact_graph,
             current_graph,
             specs,
             encoding
         )
 
+    def __init__(self, exact_graph: AnnotatedGraph,
+                 current_graph: AnnotatedGraph,
+                 specs: TemplateSpecs,
+                 encoding: Encoding,
+                 ) -> None:
+        self._exact_graph = exact_graph
+        self._current_graph = current_graph
+        self._specs = specs
+        self._encoding = encoding
+
+    def run(self) -> Sequence[Result]:
+        raise NotImplementedError(f'{self.__class__.__name__}.run(...) is abstract.')
+
+
+class SOP_QBF_Manager(TemplateManager):
+    def run(self) -> Sequence[Result]:
+        # todo:lorenzo: here
+        pass
+
+
+class Z3TemplateManager(TemplateManager):
     def generate_script(self) -> None:
         # initialize builder object
         builder = Builder.from_file('./sxpat/template_manager/template.py')
@@ -92,10 +97,6 @@ def run_script(self) -> None:
             stderr=subprocess.PIPE
         )
 
-        print(process.stdout)
-        print('==================================================================')
-        print(process.stderr)
-        print('==================================================================')
         if process.returncode != 0:
             raise RuntimeError(f'ERROR!!! Cannot run file {self.script_path}')
 
@@ -440,22 +441,23 @@ def _update_builder(self, builder: Builder) -> None:
         # apply superclass updates
         super()._update_builder(builder)
 
-        # params_declaration
-        builder.update(params_declaration='\n'.join(itertools.chain(
+        # params_declaration and params_list
+        params = list(itertools.chain(
             (
-                self._gen_declare_gate(self._output_parameter(output_i))
+                self._output_parameter(output_i)
                 for output_i in self.subgraph_outputs.keys()
             ),
             itertools.chain.from_iterable(
-                (
-                    self._gen_declare_gate((pars := self._input_parameters(output_i, product_i, input_i))[0]),
-                    self._gen_declare_gate(pars[1])
-                )
+                self._input_parameters(output_i, product_i, input_i)
                 for output_i in self.subgraph_outputs.keys()
                 for product_i in range(self._specs.ppo)
                 for input_i in self.subgraph_inputs.keys()
             ),
-        )))
+        ))
+        builder.update(
+            params_declaration='\n'.join(self._gen_declare_gate(p) for p in params),
+            params_list=f'[{", ".join(params)}]'
+        )
 
         # approximate_wires_constraints
         def get_preds(name: str) -> Collection[str]:
@@ -582,26 +584,27 @@ def _update_builder(self, builder: Builder) -> None:
         # apply superclass updates
         super()._update_builder(builder)
 
-        # params_declaration
-        builder.update(params_declaration='\n'.join(itertools.chain(
+        # params_declaration and params_list
+        params = list(itertools.chain(
             (  # p_o#
-                self._gen_declare_gate(self._output_parameter(output_i))
+                self._output_parameter(output_i)
                 for output_i in self.subgraph_outputs.keys()
             ),
             itertools.chain.from_iterable(  # p_pr#_i#
-                (
-                    self._gen_declare_gate((pars := self._input_parameters(None, product_i, input_i))[0]),
-                    self._gen_declare_gate(pars[1])
-                )
+                self._input_parameters(None, product_i, input_i)
                 for product_i in range(self._specs.pit)
                 for input_i in self.subgraph_inputs.keys()
             ),
             (  # p_pr#_o#
-                self._gen_declare_gate(self._product_parameter(output_i, product_i))
+                self._product_parameter(output_i, product_i)
                 for output_i in self.subgraph_outputs.keys()
                 for product_i in range(self._specs.pit)
             ),
-        )))
+        ))
+        builder.update(
+            params_declaration='\n'.join(self._gen_declare_gate(p) for p in params),
+            params_list=f'[{", ".join(params)}]'
+        )
 
         # approximate_wires_constraints
         def get_preds(name: str) -> Collection[str]: return sorted(self._current_graph.graph.predecessors(name), key=lambda n: int(re.search(r'\d+', n).group()))

sxpat/utils/collections.py

@@ -0,0 +1,21 @@
+from typing import Iterator, Mapping, Sequence, Tuple, TypeVar
+
+import itertools
+
+
+NOTHING = object()
+K = TypeVar('K')
+V = TypeVar('V')
+T = TypeVar('T')
+
+
+def mapping_inv(mapping: Mapping[K, V], value: V, default: K = NOTHING) -> K:
+    key = next((k for (k, v) in mapping.items() if v == value), default)
+    if key is NOTHING:
+        raise ValueError('The value does not match with any pair in the mapping.')
+    return key
+
+
+def pairwise_iter(sequence: Sequence[T]) -> Iterator[Tuple[T, T]]:
+    """iterate pair-wise (AB, BC, CD, ...)"""
+    return zip(sequence, itertools.islice(sequence, 1, None))

sxpat/xplore.py

@@ -270,7 +270,9 @@ def explore_grid(specs_obj: TemplateSpecs):
                         prev_actual_error = obtained_wce_prev
 
                         if obtained_wce_exact > available_error:
-                            raise Exception(color.error('ErrorEval Verification: FAILED!'))
+                            stats_obj.store_grid()
+                            return stats_obj
+                            # raise Exception(color.error('ErrorEval Verification: FAILED!'))
 
                     this_model_info = Model(id=0, status=cur_status.upper(), cell=(lpp, ppo), et=obtained_wce_exact, iteration=i,
                                             area=cur_model_results[synth_obj.ver_out_name][0],