mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
FPA Python API cosmetics
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
052baaabe4
commit
079204d1aa
|
@ -7749,7 +7749,7 @@ class FPRMRef(ExprRef):
|
|||
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
|
||||
|
||||
|
||||
def RoundNearestTiesToEven (ctx=None):
|
||||
def RoundNearestTiesToEven(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
|
||||
|
||||
|
@ -7757,7 +7757,7 @@ def RNE (ctx=None):
|
|||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
|
||||
|
||||
def RoundNearestTiesToAway (ctx=None):
|
||||
def RoundNearestTiesToAway(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
|
||||
|
||||
|
@ -7765,27 +7765,27 @@ def RNA (ctx=None):
|
|||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
|
||||
|
||||
def RoundTowardPositive (ctx=None):
|
||||
def RoundTowardPositive(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
|
||||
|
||||
def RTP (ctx=None):
|
||||
def RTP(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
|
||||
|
||||
def RoundTowardNegative (ctx=None):
|
||||
def RoundTowardNegative(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
|
||||
|
||||
def RTN (ctx=None):
|
||||
def RTN(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
|
||||
|
||||
def RoundTowardZero (ctx=None):
|
||||
def RoundTowardZero(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
|
||||
|
||||
def RTZ (ctx=None):
|
||||
def RTZ(ctx=None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
|
||||
|
||||
|
|
|
@ -64,9 +64,9 @@ _z3_precedence = {
|
|||
|
||||
# FPA operators
|
||||
_z3_op_to_fpa_normal_str = {
|
||||
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RNE()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RNA()',
|
||||
Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RTP()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RTN()',
|
||||
Z3_OP_FPA_RM_TOWARD_ZERO : 'RTZ()',
|
||||
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RoundNearestTiesToEven()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RoundNearestTiesToAway()',
|
||||
Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RoundTowardPositive()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RoundTowardNegative()',
|
||||
Z3_OP_FPA_RM_TOWARD_ZERO : 'RoundTowardZero()',
|
||||
Z3_OP_FPA_PLUS_INF : '+oo', Z3_OP_FPA_MINUS_INF : '-oo',
|
||||
Z3_OP_FPA_NAN : 'NaN', Z3_OP_FPA_PLUS_ZERO : 'PZero', Z3_OP_FPA_MINUS_ZERO : 'NZero',
|
||||
Z3_OP_FPA_ADD : 'fpAdd', Z3_OP_FPA_SUB : 'fpSub', Z3_OP_FPA_NEG : 'fpNeg', Z3_OP_FPA_MUL : 'fpMul',
|
||||
|
@ -580,7 +580,7 @@ class Formatter:
|
|||
if self.fpa_pretty and a.decl().kind() in _z3_op_to_fpa_pretty_str:
|
||||
return to_format(_z3_op_to_fpa_pretty_str.get(a.decl().kind()))
|
||||
else:
|
||||
return to_format(a.as_string())
|
||||
return to_format(_z3_op_to_fpa_normal_str.get(a.decl().kind()))
|
||||
|
||||
def pp_fp_value(self, a):
|
||||
z3._z3_assert(isinstance(a, z3.FPNumRef), 'type mismatch')
|
||||
|
|
Loading…
Reference in a new issue