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):
@@ -201,3 +201,85 @@ 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.
+    """
+    validation = validation or StatementValidationDictionary(
+        cost_functions=[None]*len(statements.cost_functions),
+        parameter_constraints=[None]*len(statements.parameter_constraints),
+        structure_constraints=[None]*len(statements.structure_constraints),
+        unformalizable_statements=[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 or []) + (statements.parameter_constraints or []), (validation.cost_functions or []) + (validation.parameter_constraints or []), strict=True):
+        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 or [], validation.structure_constraints or [], strict=True):
+        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 or [], validation.unformalizable_statements or [], strict=True):
+        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")