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

duplicating private member from z3 to avoid build regressions under some environments

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-09-30 07:21:39 -07:00
parent f00d5b89e0
commit 279621c1d7
1 changed files with 13 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10,6 +10,10 @@ from .z3consts import *
from .z3core import * from .z3core import *
from ctypes import * from ctypes import *
def _z3_assert(cond, msg):
if not cond:
raise Z3Exception(msg)
############################## ##############################
# #
# Configuration # Configuration
@ -580,14 +584,14 @@ class Formatter:
return to_format(a.as_string()) return to_format(a.as_string())
def pp_fprm_value(self, a): def pp_fprm_value(self, a):
z3._z3_assert(z3.is_fprm_value(a), 'expected FPRMNumRef') _z3_assert(z3.is_fprm_value(a), 'expected FPRMNumRef')
if self.fpa_pretty and (a.decl().kind() in _z3_op_to_fpa_pretty_str): 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())) return to_format(_z3_op_to_fpa_pretty_str.get(a.decl().kind()))
else: else:
return to_format(_z3_op_to_fpa_normal_str.get(a.decl().kind())) return to_format(_z3_op_to_fpa_normal_str.get(a.decl().kind()))
def pp_fp_value(self, a): def pp_fp_value(self, a):
z3._z3_assert(isinstance(a, z3.FPNumRef), 'type mismatch') _z3_assert(isinstance(a, z3.FPNumRef), 'type mismatch')
if not self.fpa_pretty: if not self.fpa_pretty:
r = [] r = []
if (a.isNaN()): if (a.isNaN()):
@ -612,7 +616,7 @@ class Formatter:
else: else:
return to_format('+zero') return to_format('+zero')
else: else:
z3._z3_assert(z3.is_fp_value(a), 'expecting FP num ast') _z3_assert(z3.is_fp_value(a), 'expecting FP num ast')
r = [] r = []
sgn = c_int(0) sgn = c_int(0)
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
@ -642,7 +646,7 @@ class Formatter:
else: else:
return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_PLUS_ZERO]) return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_PLUS_ZERO])
else: else:
z3._z3_assert(z3.is_fp_value(a), 'expecting FP num ast') _z3_assert(z3.is_fp_value(a), 'expecting FP num ast')
r = [] r = []
sgn = (ctypes.c_int)(0) sgn = (ctypes.c_int)(0)
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
@ -659,7 +663,7 @@ class Formatter:
def pp_fp(self, a, d, xs): def pp_fp(self, a, d, xs):
z3._z3_assert(isinstance(a, z3.FPRef), "type mismatch") _z3_assert(isinstance(a, z3.FPRef), "type mismatch")
k = a.decl().kind() k = a.decl().kind()
op = '?' op = '?'
if (self.fpa_pretty and k in _z3_op_to_fpa_pretty_str): if (self.fpa_pretty and k in _z3_op_to_fpa_pretty_str):
@ -1164,12 +1168,12 @@ def set_pp_option(k, v):
return True return True
val = getattr(_PP, k, None) val = getattr(_PP, k, None)
if val != None: if val != None:
z3._z3_assert(type(v) == type(val), "Invalid pretty print option value") _z3_assert(type(v) == type(val), "Invalid pretty print option value")
setattr(_PP, k, v) setattr(_PP, k, v)
return True return True
val = getattr(_Formatter, k, None) val = getattr(_Formatter, k, None)
if val != None: if val != None:
z3._z3_assert(type(v) == type(val), "Invalid pretty print option value") _z3_assert(type(v) == type(val), "Invalid pretty print option value")
setattr(_Formatter, k, v) setattr(_Formatter, k, v)
return True return True
return False return False
@ -1219,13 +1223,13 @@ def pp(a):
print(a) print(a)
def print_matrix(m): def print_matrix(m):
z3._z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected") _z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected")
if not in_html_mode(): if not in_html_mode():
print(obj_to_string(m)) print(obj_to_string(m))
else: else:
print('<table cellpadding="2", cellspacing="0", border="1">') print('<table cellpadding="2", cellspacing="0", border="1">')
for r in m: for r in m:
z3._z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected") _z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected")
print('<tr>') print('<tr>')
for c in r: for c in r:
print('<td>%s</td>' % c) print('<td>%s</td>' % c)