Add set_ast_print_mode() to Python, C#, and TypeScript bindings (#8166)

* Initial plan

* Add set_ast_print_mode to Python and PrintMode getter to C#

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add setPrintMode to TypeScript Context API

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/api/dotnet/Context.cs

@@ -3395,7 +3395,12 @@ namespace Microsoft.Z3
         /// <seealso cref="Sort.ToString()"/>
         public Z3_ast_print_mode PrintMode
         {
-            set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
+            get { return m_print_mode; }
+            set 
+            { 
+                Native.Z3_set_ast_print_mode(nCtx, (uint)value);
+                m_print_mode = value;
+            }
         }
         #endregion
 
@@ -4943,6 +4948,7 @@ namespace Microsoft.Z3
         internal Native.Z3_error_handler m_n_err_handler = null;
         internal static Object creation_lock = new Object();
         internal IntPtr nCtx { get { return m_ctx; } }
+        private Z3_ast_print_mode m_print_mode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
 
         internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
         {

src/api/js/src/high-level/high-level.ts

@@ -382,6 +382,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       check(Z3.interrupt(contextPtr));
     }
 
+    function setPrintMode(mode: Z3_ast_print_mode): void {
+      Z3.set_ast_print_mode(contextPtr, mode);
+    }
+
     function isModel(obj: unknown): obj is Model<Name> {
       const r = obj instanceof ModelImpl;
       r && _assertContext(obj);
@@ -4487,6 +4491,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       // Functions //
       ///////////////
       interrupt,
+      setPrintMode,
       isModel,
       isAst,
       isSort,

src/api/js/src/high-level/types.ts

@@ -1,6 +1,7 @@
 import {
   Z3_ast,
   Z3_ast_map,
+  Z3_ast_print_mode,
   Z3_ast_vector,
   Z3_context,
   Z3_constructor,
@@ -181,6 +182,18 @@ export interface Context<Name extends string = 'main'> {
   /** @category Functions */
   interrupt(): void;
 
+  /**
+   * Set the pretty printing mode for ASTs.
+   * 
+   * @param mode - The print mode to use:
+   *   - Z3_PRINT_SMTLIB_FULL (0): Print AST nodes in SMTLIB verbose format.
+   *   - Z3_PRINT_LOW_LEVEL (1): Print AST nodes using a low-level format.
+   *   - Z3_PRINT_SMTLIB2_COMPLIANT (2): Print AST nodes in SMTLIB 2.x compliant format.
+   * 
+   * @category Functions
+   */
+  setPrintMode(mode: Z3_ast_print_mode): void;
+
   /** @category Functions */
   isModel(obj: unknown): obj is Model<Name>;
 

src/api/python/z3/z3.py

@@ -240,6 +240,26 @@ class Context:
     def param_descrs(self):
         """Return the global parameter description set."""
         return ParamDescrsRef(Z3_get_global_param_descrs(self.ref()), self)
+
+    def set_ast_print_mode(self, mode):
+        """Set the pretty printing mode for ASTs.
+
+        The following modes are available:
+        - Z3_PRINT_SMTLIB_FULL (0): Print AST nodes in SMTLIB verbose format.
+        - Z3_PRINT_LOW_LEVEL (1): Print AST nodes using a low-level format.
+        - Z3_PRINT_SMTLIB2_COMPLIANT (2): Print AST nodes in SMTLIB 2.x compliant format.
+
+        Example:
+        >>> c = Context()
+        >>> c.set_ast_print_mode(Z3_PRINT_LOW_LEVEL)
+        >>> x = Int('x', c)
+        >>> print(x)
+        (Int 0)
+        >>> c.set_ast_print_mode(Z3_PRINT_SMTLIB2_COMPLIANT)
+        >>> print(x)
+        x
+        """
+        Z3_set_ast_print_mode(self.ref(), mode)
         
 
 # Global Z3 context