mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

add shortcut to retrieve kind of application

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-22 13:05:58 -07:00
parent 78d1139ba0
commit 8b657f27aa
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1400,7 +1400,7 @@ def is_app_of(a, k):
>>> is_app_of(n, Z3_OP_MUL) >>> is_app_of(n, Z3_OP_MUL)
False False
""" """
return is_app(a) and a.decl().kind() == k return is_app(a) and a.kind() == k
def If(a, b, c, ctx=None): def If(a, b, c, ctx=None):
@ -9454,7 +9454,7 @@ _ROUNDING_MODES = frozenset({
def set_default_rounding_mode(rm, ctx=None): def set_default_rounding_mode(rm, ctx=None):
global _dflt_rounding_mode global _dflt_rounding_mode
if is_fprm_value(rm): if is_fprm_value(rm):
_dflt_rounding_mode = rm.decl().kind() _dflt_rounding_mode = rm.kind()
else: else:
_z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode") _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode")
_dflt_rounding_mode = rm _dflt_rounding_mode = rm