Print statements

Author: donato-ax

src/axiomatic/pic_helpers.py

@@ -3,7 +3,7 @@
 from ipywidgets import interactive, IntSlider  # type: ignore
 from typing import List, Optional
 
-from . import Parameter
+from . import Parameter, StatementDictionary, StatementValidationDictionary
 
 
 def plot_circuit(component):
@@ -80,8 +80,8 @@ def plot_single_spectrum(
     """
     Plot a single spectrum with vertical and horizontal lines.
     """
-    hlines = hlines or []
-    vlines = vlines or []
+    hlines = hlines
+    vlines = vlines
 
     plt.clf()
     plt.figure(figsize=(10, 5))
@@ -142,8 +142,8 @@ def plot_interactive_spectra(
 
     slider_index = slider_index or list(range(len(spectra[0])))
     spectrum_labels = spectrum_labels or [f"Spectrum {i}" for i in range(len(spectra))]
-    vlines = vlines or []
-    hlines = hlines or []
+    vlines = vlines
+    hlines = hlines
 
     # Function to update the plot
     def plot_array(index=0):
@@ -201,3 +201,92 @@ def plot_parameter_history(parameters: List[Parameter], parameter_history: List[
             ]
         )
         plt.show()
+
+
+def print_statements(statements: StatementDictionary, validation: StatementValidationDictionary | None = None):
+    """
+    Print a list of statements in nice readable format.
+    """
+    statements = StatementDictionary(
+        cost_functions=statements.cost_functions or [],
+        parameter_constraints=statements.parameter_constraints or [],
+        structure_constraints=statements.structure_constraints or [],
+        unformalizable_statements=statements.unformalizable_statements or [],
+    )
+
+    validation = StatementValidationDictionary(
+        cost_functions=(validation.cost_functions if validation is not None else None) or [None]*len(statements.cost_functions),
+        parameter_constraints=(validation.parameter_constraints if validation is not None else None) or [None]*len(statements.parameter_constraints),
+        structure_constraints=(validation.structure_constraints if validation is not None else None) or [None]*len(statements.structure_constraints),
+        unformalizable_statements=(validation.unformalizable_statements if validation is not None else None) or [None]*len(statements.unformalizable_statements)
+    )
+
+    if len(validation.cost_functions) != len(statements.cost_functions):
+        raise ValueError("Number of cost functions and validations do not match.")
+    if len(validation.parameter_constraints) != len(statements.parameter_constraints):
+        raise ValueError("Number of parameter constraints and validations do not match.")
+    if len(validation.structure_constraints) != len(statements.structure_constraints):
+        raise ValueError("Number of structure constraints and validations do not match.")
+    if len(validation.unformalizable_statements) != len(statements.unformalizable_statements):
+        raise ValueError("Number of unformalizable statements and validations do not match.")
+
+    print("-----------------------------------\n")
+    for z3_stmt, z3_val in zip((statements.cost_functions) + (statements.parameter_constraints), (validation.cost_functions) + (validation.parameter_constraints)):
+        print("Type:", z3_stmt.type)
+        print("Statement:", z3_stmt.text)
+        print("Formalization:", end=" ")
+        if z3_stmt.formalization is None:
+            print("UNFORMALIZED")
+        else:
+            code = z3_stmt.formalization.code
+            if z3_stmt.formalization.mapping is not None:
+                for var_name, computation in z3_stmt.formalization.mapping.items():
+                    if computation is not None:
+                        args_str = ", ".join(
+                            [
+                                f"{argname}="
+                                + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
+                                for argname, argvalue in computation.arguments.items()
+                            ]
+                        )
+                        code = code.replace(var_name, f"{computation.name}({args_str})")
+            print(code)
+        val = z3_stmt.validation or z3_val
+        if val is not None:
+            if z3_stmt.type == "COST_FUNCTION":
+                print(f"Satisfiable: {val.satisfiable}")
+                print(val.message)
+            else:
+                print(f"Satisfiable: {val.satisfiable}")
+                print(f"Holds: {val.holds} ({val.message})")
+        print("\n-----------------------------------\n")
+    for struct_stmt, struct_val in zip(statements.structure_constraints, validation.structure_constraints):
+        print("Type:", struct_stmt.type)
+        print("Statement:", struct_stmt.text)
+        print("Formalization:", end=" ")
+        if struct_stmt.formalization is None:
+            print("UNFORMALIZED")
+        else:
+            func_constr = struct_stmt.formalization
+            args_str = ", ".join(
+                [
+                    f"{argname}=" + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
+                    for argname, argvalue in func_constr.arguments.items()
+                ]
+            )
+            func_str = f"{func_constr.function_name}({args_str}) == {func_constr.expected_result}"
+            print(func_str)
+        val = struct_stmt.validation or struct_val
+        if val is not None:
+            print(f"Satisfiable: {val.satisfiable}")
+            print(f"Holds: {val.holds}")
+        print("\n-----------------------------------\n")
+    for unf_stmt, unf_val in zip(statements.unformalizable_statements, validation.unformalizable_statements):
+        print("Type:", unf_stmt.type)
+        print("Statement:", unf_stmt.text)
+        print("Formalization: UNFORMALIZABLE")
+        val = unf_stmt.validation or unf_val
+        if val is not None:
+            print(f"Satisfiable: {val.satisfiable}")
+            print(f"Holds: {val.holds}")
+        print("\n-----------------------------------\n")