mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Expose PARAMETER_INTERNAL and PARAMETER_ZSTRING in case API users access these #7522

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-22 11:46:03 -08:00
parent ef275ab1a0
commit bd566f16b1
3 changed files with 28 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/api/api_ast.cpp
View file

@ -500,25 +500,25 @@ extern "C" {
return Z3_PARAMETER_INT; return Z3_PARAMETER_INT;
} }
parameter const& p = to_func_decl(d)->get_parameters()[idx]; parameter const& p = to_func_decl(d)->get_parameters()[idx];
if (p.is_int()) { if (p.is_int())
return Z3_PARAMETER_INT; return Z3_PARAMETER_INT;
} if (p.is_double())
if (p.is_double()) { return Z3_PARAMETER_DOUBLE;
return Z3_PARAMETER_DOUBLE; if (p.is_symbol())
} return Z3_PARAMETER_SYMBOL;
if (p.is_symbol()) { if (p.is_rational())
return Z3_PARAMETER_SYMBOL; return Z3_PARAMETER_RATIONAL;
} if (p.is_ast() && is_sort(p.get_ast()))
if (p.is_rational()) { return Z3_PARAMETER_SORT;
return Z3_PARAMETER_RATIONAL; if (p.is_ast() && is_expr(p.get_ast()))
} return Z3_PARAMETER_AST;
if (p.is_ast() && is_sort(p.get_ast())) { if (p.is_ast() && is_func_decl(p.get_ast()))
return Z3_PARAMETER_SORT; return Z3_PARAMETER_FUNC_DECL;
} if (p.is_zstring())
if (p.is_ast() && is_expr(p.get_ast())) { return Z3_PARAMETER_ZSTRING;
return Z3_PARAMETER_AST; if (p.is_external())
} return Z3_PARAMETER_INTERNAL;
SASSERT(p.is_ast() && is_func_decl(p.get_ast())); throw default_exception("an attempt was made to access an unknown parameter kind");
return Z3_PARAMETER_FUNC_DECL; return Z3_PARAMETER_FUNC_DECL;
Z3_CATCH_RETURN(Z3_PARAMETER_INT); Z3_CATCH_RETURN(Z3_PARAMETER_INT);
} }

4
src/api/python/z3/z3.py
View file

@ -834,6 +834,10 @@ class FuncDeclRef(AstRef):
result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx) result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx)
elif k == Z3_PARAMETER_FUNC_DECL: elif k == Z3_PARAMETER_FUNC_DECL:
result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx) 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: else:
assert(False) assert(False)
return result return result

6
src/api/z3_api.h
View file

@ -119,6 +119,8 @@ typedef enum
- Z3_PARAMETER_SORT is used for sort parameters. - Z3_PARAMETER_SORT is used for sort parameters.
- Z3_PARAMETER_AST is used for expression parameters. - Z3_PARAMETER_AST is used for expression parameters.
- Z3_PARAMETER_FUNC_DECL is used for function declaration 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 typedef enum
{ {
@ -128,7 +130,9 @@ typedef enum
Z3_PARAMETER_SYMBOL, Z3_PARAMETER_SYMBOL,
Z3_PARAMETER_SORT, Z3_PARAMETER_SORT,
Z3_PARAMETER_AST, Z3_PARAMETER_AST,
Z3_PARAMETER_FUNC_DECL Z3_PARAMETER_FUNC_DECL,
Z3_PARAMETER_INTERNAL,
Z3_PARAMETER_ZSTRING
} Z3_parameter_kind; } Z3_parameter_kind;
/** /**