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

fix #7085

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-16 10:18:46 -08:00
parent 4ff352fcac
commit afba43a5a7
1 changed files with 16 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/api/python/z3/z3printer.py
View file

@ -252,11 +252,11 @@ def _is_html_left_assoc(k):
def _is_add(k):
return k == Z3_OP_ADD or k == Z3_OP_BADD
return k == Z3_OP_ADD or k == Z3_OP_BADD or k == Z3_OP_FPA_ADD
def _is_sub(k):
return k == Z3_OP_SUB or k == Z3_OP_BSUB
return k == Z3_OP_SUB or k == Z3_OP_BSUB or k == Z3_OP_FPA_SUB
if sys.version_info.major < 3:
@ -890,9 +890,21 @@ class Formatter:
if self.is_infix(k) and n >= 3:
rm = a.arg(0)
if z3.is_fprm_value(rm) and z3.get_default_rounding_mode(a.ctx).eq(rm):
arg1 = to_format(self.pp_expr(a.arg(1), d + 1, xs))
arg2 = to_format(self.pp_expr(a.arg(2), d + 1, xs))
p = self.get_precedence(k)
r = []
x = a.arg(1)
y = a.arg(2)
arg1 = to_format(self.pp_expr(x, d + 1, xs))
arg2 = to_format(self.pp_expr(y, d + 1, xs))
if z3.is_app(x):
child_k = x.decl().kind()
if child_k != k and self.is_infix(child_k) and self.get_precedence(child_k) > p:
arg1 = self.add_paren(arg1)
if z3.is_app(y):
child_k = y.decl().kind()
if child_k != k and self.is_infix(child_k) and self.get_precedence(child_k) > p:
arg2 = self.add_paren(arg2)
r.append(arg1)
r.append(to_format(" "))
r.append(to_format(op))