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
 
 
 def plot_circuit(component):
@@ -201,3 +201,63 @@ def plot_parameter_history(parameters: List[Parameter], parameter_history: List[
             ]
         )
         plt.show()
+
+
+def print_statements(statements: StatementDictionary):
+    """
+    Print a list of statements in nice readable format.
+    """
+    print("-----------------------------------\n")
+    for z3_stmt in (statements.cost_functions or []) + (statements.parameter_constraints or []):
+        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)
+        if z3_stmt.validation is not None:
+            if z3_stmt.type == "COST_FUNCTION":
+                print(f"Satisfiable: {z3_stmt.validation.satisfiable}")
+                print(z3_stmt.validation.message)
+            else:
+                print(f"Satisfiable: {z3_stmt.validation.satisfiable}")
+                print(f"Holds: {z3_stmt.validation.holds} ({z3_stmt.validation.message})")
+        print("\n-----------------------------------\n")
+    for struct_stmt in (statements.structure_constraints or []):
+        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)
+        if struct_stmt.validation is not None:
+            print(f"Satisfiable: {struct_stmt.validation.satisfiable}")
+            print(f"Holds: {struct_stmt.validation.holds}")
+        print("\n-----------------------------------\n")
+    for unf_stmt in (statements.unformalizable_statements or []):
+        print("Type:", unf_stmt.type)
+        print("Statement:", unf_stmt.text)
+        print("Formalization: UNFORMALIZABLE")
+        print("\n-----------------------------------\n")