Expose PARAMETER_INTERNAL and PARAMETER_ZSTRING in case API users acc…

…ess these #7522
Z3Prover · Jan 22, 2025 · bd566f1 · bd566f1
1 parent ef275ab
commit bd566f1
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 20 deletions.
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
@@ -500,25 +500,25 @@ extern "C" {
             return Z3_PARAMETER_INT;
         }
         parameter const& p = to_func_decl(d)->get_parameters()[idx];
-        if (p.is_int()) {
-            return Z3_PARAMETER_INT;
-        }
-        if (p.is_double()) {
-            return Z3_PARAMETER_DOUBLE;
-        }
-        if (p.is_symbol()) {
-            return Z3_PARAMETER_SYMBOL;
-        }
-        if (p.is_rational()) {
-            return Z3_PARAMETER_RATIONAL;
-        }
-        if (p.is_ast() && is_sort(p.get_ast())) {
-            return Z3_PARAMETER_SORT;
-        }
-        if (p.is_ast() && is_expr(p.get_ast())) {
-            return Z3_PARAMETER_AST;
-        }
-        SASSERT(p.is_ast() && is_func_decl(p.get_ast()));
+        if (p.is_int()) 
+            return Z3_PARAMETER_INT;        
+        if (p.is_double()) 
+            return Z3_PARAMETER_DOUBLE;        
+        if (p.is_symbol()) 
+            return Z3_PARAMETER_SYMBOL;        
+        if (p.is_rational()) 
+            return Z3_PARAMETER_RATIONAL;        
+        if (p.is_ast() && is_sort(p.get_ast())) 
+            return Z3_PARAMETER_SORT;        
+        if (p.is_ast() && is_expr(p.get_ast())) 
+            return Z3_PARAMETER_AST;   
+        if (p.is_ast() && is_func_decl(p.get_ast()))
+            return Z3_PARAMETER_FUNC_DECL;
+        if (p.is_zstring())
+            return Z3_PARAMETER_ZSTRING;
+        if (p.is_external())
+            return Z3_PARAMETER_INTERNAL;
+        throw default_exception("an attempt was made to access an unknown parameter kind");
         return Z3_PARAMETER_FUNC_DECL;
         Z3_CATCH_RETURN(Z3_PARAMETER_INT);
     }

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
@@ -834,6 +834,10 @@ def params(self):
                 result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx)
             elif k == Z3_PARAMETER_FUNC_DECL:
                 result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx)
+            elif k == Z3_PARAMETER_INTERNAL:
+                result[i] = "internal parameter"
+            elif k == Z3_PARAMETER_ZSTRING:
+                result[i] = "internal string"
             else:
                 assert(False)
         return result

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
@@ -119,6 +119,8 @@ typedef enum
    - Z3_PARAMETER_SORT is used for sort parameters.
    - Z3_PARAMETER_AST is used for expression parameters.
    - Z3_PARAMETER_FUNC_DECL is used for function declaration parameters.
+   - Z3_PARAMETER_INTERNAL is used for parameters that are private to Z3. They cannot be accessed.
+   - Z3_PARAMETER_ZSTRING is used for string parameters. 
 */
 typedef enum
 {
@@ -128,7 +130,9 @@ typedef enum
     Z3_PARAMETER_SYMBOL,
     Z3_PARAMETER_SORT,
     Z3_PARAMETER_AST,
-    Z3_PARAMETER_FUNC_DECL
+    Z3_PARAMETER_FUNC_DECL,
+    Z3_PARAMETER_INTERNAL,
+    Z3_PARAMETER_ZSTRING
 } Z3_parameter_kind;
 
 /**