1############################################ 2# Copyright (c) 2012 Microsoft Corporation 3# 4# Z3 Python interface 5# 6# Author: Leonardo de Moura (leonardo) 7############################################ 8import sys 9import io 10 11# We want to import submodule z3 here, but there's no way 12# to do that that works correctly on both Python 2 and 3. 13if sys.version_info.major < 3: 14 # In Python 2: an implicit-relative import of submodule z3. 15 # In Python 3: an undesirable import of global package z3. 16 import z3 17else: 18 # In Python 2: an illegal circular import. 19 # In Python 3: an explicit-relative import of submodule z3. 20 from . import z3 21 22from .z3consts import * 23from .z3core import * 24from ctypes import * 25 26 27def _z3_assert(cond, msg): 28 if not cond: 29 raise Z3Exception(msg) 30 31############################## 32# 33# Configuration 34# 35############################## 36 37 38# Z3 operator names to Z3Py 39_z3_op_to_str = { 40 Z3_OP_TRUE: "True", 41 Z3_OP_FALSE: "False", 42 Z3_OP_EQ: "==", 43 Z3_OP_DISTINCT: "Distinct", 44 Z3_OP_ITE: "If", 45 Z3_OP_AND: "And", 46 Z3_OP_OR: "Or", 47 Z3_OP_IFF: "==", 48 Z3_OP_XOR: "Xor", 49 Z3_OP_NOT: "Not", 50 Z3_OP_IMPLIES: "Implies", 51 52 Z3_OP_IDIV: "/", 53 Z3_OP_MOD: "%", 54 Z3_OP_TO_REAL: "ToReal", 55 Z3_OP_TO_INT: "ToInt", 56 Z3_OP_POWER: "**", 57 Z3_OP_IS_INT: "IsInt", 58 Z3_OP_BADD: "+", 59 Z3_OP_BSUB: "-", 60 Z3_OP_BMUL: "*", 61 Z3_OP_BOR: "|", 62 Z3_OP_BAND: "&", 63 Z3_OP_BNOT: "~", 64 Z3_OP_BXOR: "^", 65 Z3_OP_BNEG: "-", 66 Z3_OP_BUDIV: "UDiv", 67 Z3_OP_BSDIV: "/", 68 Z3_OP_BSMOD: "%", 69 Z3_OP_BSREM: "SRem", 70 Z3_OP_BUREM: "URem", 71 72 Z3_OP_EXT_ROTATE_LEFT: "RotateLeft", 73 Z3_OP_EXT_ROTATE_RIGHT: "RotateRight", 74 75 Z3_OP_SLEQ: "<=", 76 Z3_OP_SLT: "<", 77 Z3_OP_SGEQ: ">=", 78 Z3_OP_SGT: ">", 79 80 Z3_OP_ULEQ: "ULE", 81 Z3_OP_ULT: "ULT", 82 Z3_OP_UGEQ: "UGE", 83 Z3_OP_UGT: "UGT", 84 Z3_OP_SIGN_EXT: "SignExt", 85 Z3_OP_ZERO_EXT: "ZeroExt", 86 87 Z3_OP_REPEAT: "RepeatBitVec", 88 Z3_OP_BASHR: ">>", 89 Z3_OP_BSHL: "<<", 90 Z3_OP_BLSHR: "LShR", 91 92 Z3_OP_CONCAT: "Concat", 93 Z3_OP_EXTRACT: "Extract", 94 Z3_OP_BV2INT: "BV2Int", 95 Z3_OP_ARRAY_MAP: "Map", 96 Z3_OP_SELECT: "Select", 97 Z3_OP_STORE: "Store", 98 Z3_OP_CONST_ARRAY: "K", 99 Z3_OP_ARRAY_EXT: "Ext", 100 101 Z3_OP_PB_AT_MOST: "AtMost", 102 Z3_OP_PB_LE: "PbLe", 103 Z3_OP_PB_GE: "PbGe", 104 Z3_OP_PB_EQ: "PbEq", 105 106 Z3_OP_SEQ_CONCAT: "Concat", 107 Z3_OP_SEQ_PREFIX: "PrefixOf", 108 Z3_OP_SEQ_SUFFIX: "SuffixOf", 109 Z3_OP_SEQ_UNIT: "Unit", 110 Z3_OP_SEQ_CONTAINS: "Contains", 111 Z3_OP_SEQ_REPLACE: "Replace", 112 Z3_OP_SEQ_AT: "At", 113 Z3_OP_SEQ_NTH: "Nth", 114 Z3_OP_SEQ_INDEX: "IndexOf", 115 Z3_OP_SEQ_LAST_INDEX: "LastIndexOf", 116 Z3_OP_SEQ_LENGTH: "Length", 117 Z3_OP_STR_TO_INT: "StrToInt", 118 Z3_OP_INT_TO_STR: "IntToStr", 119 120 Z3_OP_SEQ_IN_RE: "InRe", 121 Z3_OP_SEQ_TO_RE: "Re", 122 Z3_OP_RE_PLUS: "Plus", 123 Z3_OP_RE_STAR: "Star", 124 Z3_OP_RE_OPTION: "Option", 125 Z3_OP_RE_UNION: "Union", 126 Z3_OP_RE_RANGE: "Range", 127 Z3_OP_RE_INTERSECT: "Intersect", 128 Z3_OP_RE_COMPLEMENT: "Complement", 129 130 Z3_OP_FPA_IS_NAN: "fpIsNaN", 131 Z3_OP_FPA_IS_INF: "fpIsInf", 132 Z3_OP_FPA_IS_ZERO: "fpIsZero", 133 Z3_OP_FPA_IS_NORMAL: "fpIsNormal", 134 Z3_OP_FPA_IS_SUBNORMAL: "fpIsSubnormal", 135 Z3_OP_FPA_IS_NEGATIVE: "fpIsNegative", 136 Z3_OP_FPA_IS_POSITIVE: "fpIsPositive", 137} 138 139# List of infix operators 140_z3_infix = [ 141 Z3_OP_EQ, Z3_OP_IFF, Z3_OP_ADD, Z3_OP_SUB, Z3_OP_MUL, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_POWER, 142 Z3_OP_LE, Z3_OP_LT, Z3_OP_GE, Z3_OP_GT, Z3_OP_BADD, Z3_OP_BSUB, Z3_OP_BMUL, 143 Z3_OP_BSDIV, Z3_OP_BSMOD, Z3_OP_BOR, Z3_OP_BAND, 144 Z3_OP_BXOR, Z3_OP_BSDIV, Z3_OP_SLEQ, Z3_OP_SLT, Z3_OP_SGEQ, Z3_OP_SGT, Z3_OP_BASHR, Z3_OP_BSHL, 145] 146 147_z3_unary = [Z3_OP_UMINUS, Z3_OP_BNOT, Z3_OP_BNEG] 148 149# Precedence 150_z3_precedence = { 151 Z3_OP_POWER: 0, 152 Z3_OP_UMINUS: 1, Z3_OP_BNEG: 1, Z3_OP_BNOT: 1, 153 Z3_OP_MUL: 2, Z3_OP_DIV: 2, Z3_OP_IDIV: 2, Z3_OP_MOD: 2, Z3_OP_BMUL: 2, Z3_OP_BSDIV: 2, Z3_OP_BSMOD: 2, 154 Z3_OP_ADD: 3, Z3_OP_SUB: 3, Z3_OP_BADD: 3, Z3_OP_BSUB: 3, 155 Z3_OP_BASHR: 4, Z3_OP_BSHL: 4, 156 Z3_OP_BAND: 5, 157 Z3_OP_BXOR: 6, 158 Z3_OP_BOR: 7, 159 Z3_OP_LE: 8, Z3_OP_LT: 8, Z3_OP_GE: 8, Z3_OP_GT: 8, Z3_OP_EQ: 8, Z3_OP_SLEQ: 8, 160 Z3_OP_SLT: 8, Z3_OP_SGEQ: 8, Z3_OP_SGT: 8, Z3_OP_IFF: 8, 161 162 Z3_OP_FPA_NEG: 1, 163 Z3_OP_FPA_MUL: 2, Z3_OP_FPA_DIV: 2, Z3_OP_FPA_REM: 2, Z3_OP_FPA_FMA: 2, 164 Z3_OP_FPA_ADD: 3, Z3_OP_FPA_SUB: 3, 165 Z3_OP_FPA_LE: 8, Z3_OP_FPA_LT: 8, Z3_OP_FPA_GE: 8, Z3_OP_FPA_GT: 8, Z3_OP_FPA_EQ: 8, 166} 167 168# FPA operators 169_z3_op_to_fpa_normal_str = { 170 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven()", 171 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway()", 172 Z3_OP_FPA_RM_TOWARD_POSITIVE: "RoundTowardPositive()", 173 Z3_OP_FPA_RM_TOWARD_NEGATIVE: "RoundTowardNegative()", 174 Z3_OP_FPA_RM_TOWARD_ZERO: "RoundTowardZero()", 175 Z3_OP_FPA_PLUS_INF: "fpPlusInfinity", 176 Z3_OP_FPA_MINUS_INF: "fpMinusInfinity", 177 Z3_OP_FPA_NAN: "fpNaN", 178 Z3_OP_FPA_PLUS_ZERO: "fpPZero", 179 Z3_OP_FPA_MINUS_ZERO: "fpNZero", 180 Z3_OP_FPA_ADD: "fpAdd", 181 Z3_OP_FPA_SUB: "fpSub", 182 Z3_OP_FPA_NEG: "fpNeg", 183 Z3_OP_FPA_MUL: "fpMul", 184 Z3_OP_FPA_DIV: "fpDiv", 185 Z3_OP_FPA_REM: "fpRem", 186 Z3_OP_FPA_ABS: "fpAbs", 187 Z3_OP_FPA_MIN: "fpMin", 188 Z3_OP_FPA_MAX: "fpMax", 189 Z3_OP_FPA_FMA: "fpFMA", 190 Z3_OP_FPA_SQRT: "fpSqrt", 191 Z3_OP_FPA_ROUND_TO_INTEGRAL: "fpRoundToIntegral", 192 193 Z3_OP_FPA_EQ: "fpEQ", 194 Z3_OP_FPA_LT: "fpLT", 195 Z3_OP_FPA_GT: "fpGT", 196 Z3_OP_FPA_LE: "fpLEQ", 197 Z3_OP_FPA_GE: "fpGEQ", 198 199 Z3_OP_FPA_FP: "fpFP", 200 Z3_OP_FPA_TO_FP: "fpToFP", 201 Z3_OP_FPA_TO_FP_UNSIGNED: "fpToFPUnsigned", 202 Z3_OP_FPA_TO_UBV: "fpToUBV", 203 Z3_OP_FPA_TO_SBV: "fpToSBV", 204 Z3_OP_FPA_TO_REAL: "fpToReal", 205 Z3_OP_FPA_TO_IEEE_BV: "fpToIEEEBV", 206} 207 208_z3_op_to_fpa_pretty_str = { 209 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: "RNE()", Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: "RNA()", 210 Z3_OP_FPA_RM_TOWARD_POSITIVE: "RTP()", Z3_OP_FPA_RM_TOWARD_NEGATIVE: "RTN()", 211 Z3_OP_FPA_RM_TOWARD_ZERO: "RTZ()", 212 Z3_OP_FPA_PLUS_INF: "+oo", Z3_OP_FPA_MINUS_INF: "-oo", 213 Z3_OP_FPA_NAN: "NaN", Z3_OP_FPA_PLUS_ZERO: "+0.0", Z3_OP_FPA_MINUS_ZERO: "-0.0", 214 215 Z3_OP_FPA_ADD: "+", Z3_OP_FPA_SUB: "-", Z3_OP_FPA_MUL: "*", Z3_OP_FPA_DIV: "/", 216 Z3_OP_FPA_REM: "%", Z3_OP_FPA_NEG: "-", 217 218 Z3_OP_FPA_EQ: "fpEQ", Z3_OP_FPA_LT: "<", Z3_OP_FPA_GT: ">", Z3_OP_FPA_LE: "<=", Z3_OP_FPA_GE: ">=" 219} 220 221_z3_fpa_infix = [ 222 Z3_OP_FPA_ADD, Z3_OP_FPA_SUB, Z3_OP_FPA_MUL, Z3_OP_FPA_DIV, Z3_OP_FPA_REM, 223 Z3_OP_FPA_LT, Z3_OP_FPA_GT, Z3_OP_FPA_LE, Z3_OP_FPA_GE 224] 225 226 227_ASSOC_OPS = frozenset({ 228 Z3_OP_BOR, 229 Z3_OP_BXOR, 230 Z3_OP_BAND, 231 Z3_OP_ADD, 232 Z3_OP_BADD, 233 Z3_OP_MUL, 234 Z3_OP_BMUL, 235}) 236 237 238def _is_assoc(k): 239 return k in _ASSOC_OPS 240 241 242def _is_left_assoc(k): 243 return _is_assoc(k) or k == Z3_OP_SUB or k == Z3_OP_BSUB 244 245 246def _is_html_assoc(k): 247 return k == Z3_OP_AND or k == Z3_OP_OR or k == Z3_OP_IFF or _is_assoc(k) 248 249 250def _is_html_left_assoc(k): 251 return _is_html_assoc(k) or k == Z3_OP_SUB or k == Z3_OP_BSUB 252 253 254def _is_add(k): 255 return k == Z3_OP_ADD or k == Z3_OP_BADD 256 257 258def _is_sub(k): 259 return k == Z3_OP_SUB or k == Z3_OP_BSUB 260 261 262if sys.version_info.major < 3: 263 import codecs 264 265 def u(x): 266 return codecs.unicode_escape_decode(x)[0] 267else: 268 def u(x): 269 return x 270 271_z3_infix_compact = [Z3_OP_MUL, Z3_OP_BMUL, Z3_OP_POWER, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_BSDIV, Z3_OP_BSMOD] 272 273_ellipses = "..." 274 275_html_ellipses = "…" 276# Overwrite some of the operators for HTML 277_z3_pre_html_op_to_str = {Z3_OP_EQ: "=", Z3_OP_IFF: "=", Z3_OP_NOT: "¬", 278 Z3_OP_AND: "∧", Z3_OP_OR: "∨", Z3_OP_IMPLIES: "⇒", 279 Z3_OP_LT: "<", Z3_OP_GT: ">", Z3_OP_LE: "≤", Z3_OP_GE: "≥", 280 Z3_OP_MUL: "·", 281 Z3_OP_SLEQ: "≤", Z3_OP_SLT: "<", Z3_OP_SGEQ: "≥", Z3_OP_SGT: ">", 282 Z3_OP_ULEQ: "≤<sub>u</sub>", Z3_OP_ULT: "<<sub>u</sub>", 283 Z3_OP_UGEQ: "≥<sub>u</sub>", Z3_OP_UGT: "><sub>u</sub>", 284 Z3_OP_BMUL: "·", 285 Z3_OP_BUDIV: "/<sub>u</sub>", Z3_OP_BUREM: "%<sub>u</sub>", 286 Z3_OP_BASHR: ">>", Z3_OP_BSHL: "<<", 287 Z3_OP_BLSHR: ">><sub>u</sub>" 288 } 289 290# Extra operators that are infix/unary for HTML 291_z3_html_infix = [Z3_OP_AND, Z3_OP_OR, Z3_OP_IMPLIES, 292 Z3_OP_ULEQ, Z3_OP_ULT, Z3_OP_UGEQ, Z3_OP_UGT, Z3_OP_BUDIV, Z3_OP_BUREM, Z3_OP_BLSHR 293 ] 294 295_z3_html_unary = [Z3_OP_NOT] 296 297# Extra Precedence for HTML 298_z3_pre_html_precedence = {Z3_OP_BUDIV: 2, Z3_OP_BUREM: 2, 299 Z3_OP_BLSHR: 4, 300 Z3_OP_ULEQ: 8, Z3_OP_ULT: 8, 301 Z3_OP_UGEQ: 8, Z3_OP_UGT: 8, 302 Z3_OP_ULEQ: 8, Z3_OP_ULT: 8, 303 Z3_OP_UGEQ: 8, Z3_OP_UGT: 8, 304 Z3_OP_NOT: 1, 305 Z3_OP_AND: 10, 306 Z3_OP_OR: 11, 307 Z3_OP_IMPLIES: 12} 308 309############################## 310# 311# End of Configuration 312# 313############################## 314 315 316def _support_pp(a): 317 return isinstance(a, z3.Z3PPObject) or isinstance(a, list) or isinstance(a, tuple) 318 319 320_infix_map = {} 321_unary_map = {} 322_infix_compact_map = {} 323 324for _k in _z3_infix: 325 _infix_map[_k] = True 326for _k in _z3_unary: 327 _unary_map[_k] = True 328 329for _k in _z3_infix_compact: 330 _infix_compact_map[_k] = True 331 332 333def _is_infix(k): 334 global _infix_map 335 return _infix_map.get(k, False) 336 337 338def _is_infix_compact(k): 339 global _infix_compact_map 340 return _infix_compact_map.get(k, False) 341 342 343def _is_unary(k): 344 global _unary_map 345 return _unary_map.get(k, False) 346 347 348def _op_name(a): 349 if isinstance(a, z3.FuncDeclRef): 350 f = a 351 else: 352 f = a.decl() 353 k = f.kind() 354 n = _z3_op_to_str.get(k, None) 355 if n is None: 356 return f.name() 357 else: 358 return n 359 360 361def _get_precedence(k): 362 global _z3_precedence 363 return _z3_precedence.get(k, 100000) 364 365 366_z3_html_op_to_str = {} 367for _k in _z3_op_to_str: 368 _v = _z3_op_to_str[_k] 369 _z3_html_op_to_str[_k] = _v 370for _k in _z3_pre_html_op_to_str: 371 _v = _z3_pre_html_op_to_str[_k] 372 _z3_html_op_to_str[_k] = _v 373 374_z3_html_precedence = {} 375for _k in _z3_precedence: 376 _v = _z3_precedence[_k] 377 _z3_html_precedence[_k] = _v 378for _k in _z3_pre_html_precedence: 379 _v = _z3_pre_html_precedence[_k] 380 _z3_html_precedence[_k] = _v 381 382_html_infix_map = {} 383_html_unary_map = {} 384for _k in _z3_infix: 385 _html_infix_map[_k] = True 386for _k in _z3_html_infix: 387 _html_infix_map[_k] = True 388for _k in _z3_unary: 389 _html_unary_map[_k] = True 390for _k in _z3_html_unary: 391 _html_unary_map[_k] = True 392 393 394def _is_html_infix(k): 395 global _html_infix_map 396 return _html_infix_map.get(k, False) 397 398 399def _is_html_unary(k): 400 global _html_unary_map 401 return _html_unary_map.get(k, False) 402 403 404def _html_op_name(a): 405 global _z3_html_op_to_str 406 if isinstance(a, z3.FuncDeclRef): 407 f = a 408 else: 409 f = a.decl() 410 k = f.kind() 411 n = _z3_html_op_to_str.get(k, None) 412 if n is None: 413 sym = Z3_get_decl_name(f.ctx_ref(), f.ast) 414 if Z3_get_symbol_kind(f.ctx_ref(), sym) == Z3_INT_SYMBOL: 415 return "ζ<sub>%s</sub>" % Z3_get_symbol_int(f.ctx_ref(), sym) 416 else: 417 # Sanitize the string 418 return f.name() 419 else: 420 return n 421 422 423def _get_html_precedence(k): 424 global _z3_html_predence 425 return _z3_html_precedence.get(k, 100000) 426 427 428class FormatObject: 429 def is_compose(self): 430 return False 431 432 def is_choice(self): 433 return False 434 435 def is_indent(self): 436 return False 437 438 def is_string(self): 439 return False 440 441 def is_linebreak(self): 442 return False 443 444 def is_nil(self): 445 return True 446 447 def children(self): 448 return [] 449 450 def as_tuple(self): 451 return None 452 453 def space_upto_nl(self): 454 return (0, False) 455 456 def flat(self): 457 return self 458 459 460class NAryFormatObject(FormatObject): 461 def __init__(self, fs): 462 assert all([isinstance(a, FormatObject) for a in fs]) 463 self.children = fs 464 465 def children(self): 466 return self.children 467 468 469class ComposeFormatObject(NAryFormatObject): 470 def is_compose(sef): 471 return True 472 473 def as_tuple(self): 474 return ("compose", [a.as_tuple() for a in self.children]) 475 476 def space_upto_nl(self): 477 r = 0 478 for child in self.children: 479 s, nl = child.space_upto_nl() 480 r = r + s 481 if nl: 482 return (r, True) 483 return (r, False) 484 485 def flat(self): 486 return compose([a.flat() for a in self.children]) 487 488 489class ChoiceFormatObject(NAryFormatObject): 490 def is_choice(sef): 491 return True 492 493 def as_tuple(self): 494 return ("choice", [a.as_tuple() for a in self.children]) 495 496 def space_upto_nl(self): 497 return self.children[0].space_upto_nl() 498 499 def flat(self): 500 return self.children[0].flat() 501 502 503class IndentFormatObject(FormatObject): 504 def __init__(self, indent, child): 505 assert isinstance(child, FormatObject) 506 self.indent = indent 507 self.child = child 508 509 def children(self): 510 return [self.child] 511 512 def as_tuple(self): 513 return ("indent", self.indent, self.child.as_tuple()) 514 515 def space_upto_nl(self): 516 return self.child.space_upto_nl() 517 518 def flat(self): 519 return indent(self.indent, self.child.flat()) 520 521 def is_indent(self): 522 return True 523 524 525class LineBreakFormatObject(FormatObject): 526 def __init__(self): 527 self.space = " " 528 529 def is_linebreak(self): 530 return True 531 532 def as_tuple(self): 533 return "<line-break>" 534 535 def space_upto_nl(self): 536 return (0, True) 537 538 def flat(self): 539 return to_format(self.space) 540 541 542class StringFormatObject(FormatObject): 543 def __init__(self, string): 544 assert isinstance(string, str) 545 self.string = string 546 547 def is_string(self): 548 return True 549 550 def as_tuple(self): 551 return self.string 552 553 def space_upto_nl(self): 554 return (getattr(self, "size", len(self.string)), False) 555 556 557def fits(f, space_left): 558 s, nl = f.space_upto_nl() 559 return s <= space_left 560 561 562def to_format(arg, size=None): 563 if isinstance(arg, FormatObject): 564 return arg 565 else: 566 r = StringFormatObject(str(arg)) 567 if size is not None: 568 r.size = size 569 return r 570 571 572def compose(*args): 573 if len(args) == 1 and (isinstance(args[0], list) or isinstance(args[0], tuple)): 574 args = args[0] 575 return ComposeFormatObject(args) 576 577 578def indent(i, arg): 579 return IndentFormatObject(i, arg) 580 581 582def group(arg): 583 return ChoiceFormatObject([arg.flat(), arg]) 584 585 586def line_break(): 587 return LineBreakFormatObject() 588 589 590def _len(a): 591 if isinstance(a, StringFormatObject): 592 return getattr(a, "size", len(a.string)) 593 else: 594 return len(a) 595 596 597def seq(args, sep=",", space=True): 598 nl = line_break() 599 if not space: 600 nl.space = "" 601 r = [] 602 r.append(args[0]) 603 num = len(args) 604 for i in range(num - 1): 605 r.append(to_format(sep)) 606 r.append(nl) 607 r.append(args[i + 1]) 608 return compose(r) 609 610 611def seq1(header, args, lp="(", rp=")"): 612 return group(compose(to_format(header), 613 to_format(lp), 614 indent(len(lp) + _len(header), 615 seq(args)), 616 to_format(rp))) 617 618 619def seq2(header, args, i=4, lp="(", rp=")"): 620 if len(args) == 0: 621 return compose(to_format(header), to_format(lp), to_format(rp)) 622 else: 623 return group(compose(indent(len(lp), compose(to_format(lp), to_format(header))), 624 indent(i, compose(seq(args), to_format(rp))))) 625 626 627def seq3(args, lp="(", rp=")"): 628 if len(args) == 0: 629 return compose(to_format(lp), to_format(rp)) 630 else: 631 return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp)))) 632 633 634class StopPPException(Exception): 635 def __str__(self): 636 return "pp-interrupted" 637 638 639class PP: 640 def __init__(self): 641 self.max_lines = 200 642 self.max_width = 60 643 self.bounded = False 644 self.max_indent = 40 645 646 def pp_string(self, f, indent): 647 if not self.bounded or self.pos <= self.max_width: 648 sz = _len(f) 649 if self.bounded and self.pos + sz > self.max_width: 650 self.out.write(u(_ellipses)) 651 else: 652 self.pos = self.pos + sz 653 self.ribbon_pos = self.ribbon_pos + sz 654 self.out.write(u(f.string)) 655 656 def pp_compose(self, f, indent): 657 for c in f.children: 658 self.pp(c, indent) 659 660 def pp_choice(self, f, indent): 661 space_left = self.max_width - self.pos 662 if space_left > 0 and fits(f.children[0], space_left): 663 self.pp(f.children[0], indent) 664 else: 665 self.pp(f.children[1], indent) 666 667 def pp_line_break(self, f, indent): 668 self.pos = indent 669 self.ribbon_pos = 0 670 self.line = self.line + 1 671 if self.line < self.max_lines: 672 self.out.write(u("\n")) 673 for i in range(indent): 674 self.out.write(u(" ")) 675 else: 676 self.out.write(u("\n...")) 677 raise StopPPException() 678 679 def pp(self, f, indent): 680 if isinstance(f, str): 681 self.pp_string(f, indent) 682 elif f.is_string(): 683 self.pp_string(f, indent) 684 elif f.is_indent(): 685 self.pp(f.child, min(indent + f.indent, self.max_indent)) 686 elif f.is_compose(): 687 self.pp_compose(f, indent) 688 elif f.is_choice(): 689 self.pp_choice(f, indent) 690 elif f.is_linebreak(): 691 self.pp_line_break(f, indent) 692 else: 693 return 694 695 def __call__(self, out, f): 696 try: 697 self.pos = 0 698 self.ribbon_pos = 0 699 self.line = 0 700 self.out = out 701 self.pp(f, 0) 702 except StopPPException: 703 return 704 705 706class Formatter: 707 def __init__(self): 708 global _ellipses 709 self.max_depth = 20 710 self.max_args = 128 711 self.rational_to_decimal = False 712 self.precision = 10 713 self.ellipses = to_format(_ellipses) 714 self.max_visited = 10000 715 self.fpa_pretty = True 716 717 def pp_ellipses(self): 718 return self.ellipses 719 720 def pp_arrow(self): 721 return " ->" 722 723 def pp_unknown(self): 724 return "<unknown>" 725 726 def pp_name(self, a): 727 return to_format(_op_name(a)) 728 729 def is_infix(self, a): 730 return _is_infix(a) 731 732 def is_unary(self, a): 733 return _is_unary(a) 734 735 def get_precedence(self, a): 736 return _get_precedence(a) 737 738 def is_infix_compact(self, a): 739 return _is_infix_compact(a) 740 741 def is_infix_unary(self, a): 742 return self.is_infix(a) or self.is_unary(a) 743 744 def add_paren(self, a): 745 return compose(to_format("("), indent(1, a), to_format(")")) 746 747 def pp_sort(self, s): 748 if isinstance(s, z3.ArraySortRef): 749 return seq1("Array", (self.pp_sort(s.domain()), self.pp_sort(s.range()))) 750 elif isinstance(s, z3.BitVecSortRef): 751 return seq1("BitVec", (to_format(s.size()), )) 752 elif isinstance(s, z3.FPSortRef): 753 return seq1("FPSort", (to_format(s.ebits()), to_format(s.sbits()))) 754 elif isinstance(s, z3.ReSortRef): 755 return seq1("ReSort", (self.pp_sort(s.basis()), )) 756 elif isinstance(s, z3.SeqSortRef): 757 if s.is_string(): 758 return to_format("String") 759 return seq1("Seq", (self.pp_sort(s.basis()), )) 760 elif isinstance(s, z3.CharSortRef): 761 return to_format("Char") 762 else: 763 return to_format(s.name()) 764 765 def pp_const(self, a): 766 k = a.decl().kind() 767 if k == Z3_OP_RE_EMPTY_SET: 768 return self.pp_set("Empty", a) 769 elif k == Z3_OP_SEQ_EMPTY: 770 return self.pp_set("Empty", a) 771 elif k == Z3_OP_RE_FULL_SET: 772 return self.pp_set("Full", a) 773 return self.pp_name(a) 774 775 def pp_int(self, a): 776 return to_format(a.as_string()) 777 778 def pp_rational(self, a): 779 if not self.rational_to_decimal: 780 return to_format(a.as_string()) 781 else: 782 return to_format(a.as_decimal(self.precision)) 783 784 def pp_algebraic(self, a): 785 return to_format(a.as_decimal(self.precision)) 786 787 def pp_string(self, a): 788 return to_format("\"" + a.as_string() + "\"") 789 790 def pp_bv(self, a): 791 return to_format(a.as_string()) 792 793 def pp_fd(self, a): 794 return to_format(a.as_string()) 795 796 def pp_fprm_value(self, a): 797 _z3_assert(z3.is_fprm_value(a), "expected FPRMNumRef") 798 if self.fpa_pretty and (a.decl().kind() in _z3_op_to_fpa_pretty_str): 799 return to_format(_z3_op_to_fpa_pretty_str.get(a.decl().kind())) 800 else: 801 return to_format(_z3_op_to_fpa_normal_str.get(a.decl().kind())) 802 803 def pp_fp_value(self, a): 804 _z3_assert(isinstance(a, z3.FPNumRef), "type mismatch") 805 if not self.fpa_pretty: 806 r = [] 807 if (a.isNaN()): 808 r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_NAN])) 809 r.append(to_format("(")) 810 r.append(to_format(a.sort())) 811 r.append(to_format(")")) 812 return compose(r) 813 elif (a.isInf()): 814 if (a.isNegative()): 815 r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_MINUS_INF])) 816 else: 817 r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_PLUS_INF])) 818 r.append(to_format("(")) 819 r.append(to_format(a.sort())) 820 r.append(to_format(")")) 821 return compose(r) 822 823 elif (a.isZero()): 824 if (a.isNegative()): 825 return to_format("-zero") 826 else: 827 return to_format("+zero") 828 else: 829 _z3_assert(z3.is_fp_value(a), "expecting FP num ast") 830 r = [] 831 sgn = c_int(0) 832 sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) 833 exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False) 834 sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast) 835 r.append(to_format("FPVal(")) 836 if sgnb and sgn.value != 0: 837 r.append(to_format("-")) 838 r.append(to_format(sig)) 839 r.append(to_format("*(2**")) 840 r.append(to_format(exp)) 841 r.append(to_format(", ")) 842 r.append(to_format(a.sort())) 843 r.append(to_format("))")) 844 return compose(r) 845 else: 846 if (a.isNaN()): 847 return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_NAN]) 848 elif (a.isInf()): 849 if (a.isNegative()): 850 return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_MINUS_INF]) 851 else: 852 return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_PLUS_INF]) 853 elif (a.isZero()): 854 if (a.isNegative()): 855 return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_MINUS_ZERO]) 856 else: 857 return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_PLUS_ZERO]) 858 else: 859 _z3_assert(z3.is_fp_value(a), "expecting FP num ast") 860 r = [] 861 sgn = (ctypes.c_int)(0) 862 sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) 863 exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False) 864 sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast) 865 if sgnb and sgn.value != 0: 866 r.append(to_format("-")) 867 r.append(to_format(sig)) 868 if (exp != "0"): 869 r.append(to_format("*(2**")) 870 r.append(to_format(exp)) 871 r.append(to_format(")")) 872 return compose(r) 873 874 def pp_fp(self, a, d, xs): 875 _z3_assert(isinstance(a, z3.FPRef), "type mismatch") 876 k = a.decl().kind() 877 op = "?" 878 if (self.fpa_pretty and k in _z3_op_to_fpa_pretty_str): 879 op = _z3_op_to_fpa_pretty_str[k] 880 elif k in _z3_op_to_fpa_normal_str: 881 op = _z3_op_to_fpa_normal_str[k] 882 elif k in _z3_op_to_str: 883 op = _z3_op_to_str[k] 884 885 n = a.num_args() 886 887 if self.fpa_pretty: 888 if self.is_infix(k) and n >= 3: 889 rm = a.arg(0) 890 if z3.is_fprm_value(rm) and z3.get_default_rounding_mode(a.ctx).eq(rm): 891 arg1 = to_format(self.pp_expr(a.arg(1), d + 1, xs)) 892 arg2 = to_format(self.pp_expr(a.arg(2), d + 1, xs)) 893 r = [] 894 r.append(arg1) 895 r.append(to_format(" ")) 896 r.append(to_format(op)) 897 r.append(to_format(" ")) 898 r.append(arg2) 899 return compose(r) 900 elif k == Z3_OP_FPA_NEG: 901 return compose([to_format("-"), to_format(self.pp_expr(a.arg(0), d + 1, xs))]) 902 903 if k in _z3_op_to_fpa_normal_str: 904 op = _z3_op_to_fpa_normal_str[k] 905 906 r = [] 907 r.append(to_format(op)) 908 if not z3.is_const(a): 909 r.append(to_format("(")) 910 first = True 911 for c in a.children(): 912 if first: 913 first = False 914 else: 915 r.append(to_format(", ")) 916 r.append(self.pp_expr(c, d + 1, xs)) 917 r.append(to_format(")")) 918 return compose(r) 919 else: 920 return to_format(a.as_string()) 921 922 def pp_prefix(self, a, d, xs): 923 r = [] 924 sz = 0 925 for child in a.children(): 926 r.append(self.pp_expr(child, d + 1, xs)) 927 sz = sz + 1 928 if sz > self.max_args: 929 r.append(self.pp_ellipses()) 930 break 931 return seq1(self.pp_name(a), r) 932 933 def is_assoc(self, k): 934 return _is_assoc(k) 935 936 def is_left_assoc(self, k): 937 return _is_left_assoc(k) 938 939 def infix_args_core(self, a, d, xs, r): 940 sz = len(r) 941 k = a.decl().kind() 942 p = self.get_precedence(k) 943 first = True 944 for child in a.children(): 945 child_pp = self.pp_expr(child, d + 1, xs) 946 child_k = None 947 if z3.is_app(child): 948 child_k = child.decl().kind() 949 if k == child_k and (self.is_assoc(k) or (first and self.is_left_assoc(k))): 950 self.infix_args_core(child, d, xs, r) 951 sz = len(r) 952 if sz > self.max_args: 953 return 954 elif self.is_infix_unary(child_k): 955 child_p = self.get_precedence(child_k) 956 if p > child_p or (_is_add(k) and _is_sub(child_k)) or (_is_sub(k) and first and _is_add(child_k)): 957 r.append(child_pp) 958 else: 959 r.append(self.add_paren(child_pp)) 960 sz = sz + 1 961 elif z3.is_quantifier(child): 962 r.append(self.add_paren(child_pp)) 963 else: 964 r.append(child_pp) 965 sz = sz + 1 966 if sz > self.max_args: 967 r.append(self.pp_ellipses()) 968 return 969 first = False 970 971 def infix_args(self, a, d, xs): 972 r = [] 973 self.infix_args_core(a, d, xs, r) 974 return r 975 976 def pp_infix(self, a, d, xs): 977 k = a.decl().kind() 978 if self.is_infix_compact(k): 979 op = self.pp_name(a) 980 return group(seq(self.infix_args(a, d, xs), op, False)) 981 else: 982 op = self.pp_name(a) 983 sz = _len(op) 984 op.string = " " + op.string 985 op.size = sz + 1 986 return group(seq(self.infix_args(a, d, xs), op)) 987 988 def pp_unary(self, a, d, xs): 989 k = a.decl().kind() 990 p = self.get_precedence(k) 991 child = a.children()[0] 992 child_k = None 993 if z3.is_app(child): 994 child_k = child.decl().kind() 995 child_pp = self.pp_expr(child, d + 1, xs) 996 if k != child_k and self.is_infix_unary(child_k): 997 child_p = self.get_precedence(child_k) 998 if p <= child_p: 999 child_pp = self.add_paren(child_pp) 1000 if z3.is_quantifier(child): 1001 child_pp = self.add_paren(child_pp) 1002 name = self.pp_name(a) 1003 return compose(to_format(name), indent(_len(name), child_pp)) 1004 1005 def pp_power_arg(self, arg, d, xs): 1006 r = self.pp_expr(arg, d + 1, xs) 1007 k = None 1008 if z3.is_app(arg): 1009 k = arg.decl().kind() 1010 if self.is_infix_unary(k) or (z3.is_rational_value(arg) and arg.denominator_as_long() != 1): 1011 return self.add_paren(r) 1012 else: 1013 return r 1014 1015 def pp_power(self, a, d, xs): 1016 arg1_pp = self.pp_power_arg(a.arg(0), d + 1, xs) 1017 arg2_pp = self.pp_power_arg(a.arg(1), d + 1, xs) 1018 return group(seq((arg1_pp, arg2_pp), "**", False)) 1019 1020 def pp_neq(self): 1021 return to_format("!=") 1022 1023 def pp_distinct(self, a, d, xs): 1024 if a.num_args() == 2: 1025 op = self.pp_neq() 1026 sz = _len(op) 1027 op.string = " " + op.string 1028 op.size = sz + 1 1029 return group(seq(self.infix_args(a, d, xs), op)) 1030 else: 1031 return self.pp_prefix(a, d, xs) 1032 1033 def pp_select(self, a, d, xs): 1034 if a.num_args() != 2: 1035 return self.pp_prefix(a, d, xs) 1036 else: 1037 arg1_pp = self.pp_expr(a.arg(0), d + 1, xs) 1038 arg2_pp = self.pp_expr(a.arg(1), d + 1, xs) 1039 return compose(arg1_pp, indent(2, compose(to_format("["), arg2_pp, to_format("]")))) 1040 1041 def pp_unary_param(self, a, d, xs): 1042 p = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) 1043 arg = self.pp_expr(a.arg(0), d + 1, xs) 1044 return seq1(self.pp_name(a), [to_format(p), arg]) 1045 1046 def pp_extract(self, a, d, xs): 1047 high = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) 1048 low = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1) 1049 arg = self.pp_expr(a.arg(0), d + 1, xs) 1050 return seq1(self.pp_name(a), [to_format(high), to_format(low), arg]) 1051 1052 def pp_loop(self, a, d, xs): 1053 low = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) 1054 arg = self.pp_expr(a.arg(0), d + 1, xs) 1055 if Z3_get_decl_num_parameters(a.ctx_ref(), a.decl().ast) > 1: 1056 high = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1) 1057 return seq1("Loop", [arg, to_format(low), to_format(high)]) 1058 return seq1("Loop", [arg, to_format(low)]) 1059 1060 def pp_set(self, id, a): 1061 return seq1(id, [self.pp_sort(a.sort())]) 1062 1063 def pp_pattern(self, a, d, xs): 1064 if a.num_args() == 1: 1065 return self.pp_expr(a.arg(0), d, xs) 1066 else: 1067 return seq1("MultiPattern", [self.pp_expr(arg, d + 1, xs) for arg in a.children()]) 1068 1069 def pp_is(self, a, d, xs): 1070 f = a.params()[0] 1071 return self.pp_fdecl(f, a, d, xs) 1072 1073 def pp_map(self, a, d, xs): 1074 f = z3.get_map_func(a) 1075 return self.pp_fdecl(f, a, d, xs) 1076 1077 def pp_fdecl(self, f, a, d, xs): 1078 r = [] 1079 sz = 0 1080 r.append(to_format(f.name())) 1081 for child in a.children(): 1082 r.append(self.pp_expr(child, d + 1, xs)) 1083 sz = sz + 1 1084 if sz > self.max_args: 1085 r.append(self.pp_ellipses()) 1086 break 1087 return seq1(self.pp_name(a), r) 1088 1089 def pp_K(self, a, d, xs): 1090 return seq1(self.pp_name(a), [self.pp_sort(a.domain()), self.pp_expr(a.arg(0), d + 1, xs)]) 1091 1092 def pp_atmost(self, a, d, f, xs): 1093 k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) 1094 return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)]) 1095 1096 def pp_pbcmp(self, a, d, f, xs): 1097 chs = a.children() 1098 rchs = range(len(chs)) 1099 k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) 1100 ks = [Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, i + 1) for i in rchs] 1101 ls = [seq3([self.pp_expr(chs[i], d + 1, xs), to_format(ks[i])]) for i in rchs] 1102 return seq1(self.pp_name(a), [seq3(ls), to_format(k)]) 1103 1104 def pp_app(self, a, d, xs): 1105 if z3.is_int_value(a): 1106 return self.pp_int(a) 1107 elif z3.is_rational_value(a): 1108 return self.pp_rational(a) 1109 elif z3.is_algebraic_value(a): 1110 return self.pp_algebraic(a) 1111 elif z3.is_bv_value(a): 1112 return self.pp_bv(a) 1113 elif z3.is_finite_domain_value(a): 1114 return self.pp_fd(a) 1115 elif z3.is_fprm_value(a): 1116 return self.pp_fprm_value(a) 1117 elif z3.is_fp_value(a): 1118 return self.pp_fp_value(a) 1119 elif z3.is_fp(a): 1120 return self.pp_fp(a, d, xs) 1121 elif z3.is_string_value(a): 1122 return self.pp_string(a) 1123 elif z3.is_const(a): 1124 return self.pp_const(a) 1125 else: 1126 f = a.decl() 1127 k = f.kind() 1128 if k == Z3_OP_POWER: 1129 return self.pp_power(a, d, xs) 1130 elif k == Z3_OP_DISTINCT: 1131 return self.pp_distinct(a, d, xs) 1132 elif k == Z3_OP_SELECT: 1133 return self.pp_select(a, d, xs) 1134 elif k == Z3_OP_SIGN_EXT or k == Z3_OP_ZERO_EXT or k == Z3_OP_REPEAT: 1135 return self.pp_unary_param(a, d, xs) 1136 elif k == Z3_OP_EXTRACT: 1137 return self.pp_extract(a, d, xs) 1138 elif k == Z3_OP_RE_LOOP: 1139 return self.pp_loop(a, d, xs) 1140 elif k == Z3_OP_DT_IS: 1141 return self.pp_is(a, d, xs) 1142 elif k == Z3_OP_ARRAY_MAP: 1143 return self.pp_map(a, d, xs) 1144 elif k == Z3_OP_CONST_ARRAY: 1145 return self.pp_K(a, d, xs) 1146 elif k == Z3_OP_PB_AT_MOST: 1147 return self.pp_atmost(a, d, f, xs) 1148 elif k == Z3_OP_PB_LE: 1149 return self.pp_pbcmp(a, d, f, xs) 1150 elif k == Z3_OP_PB_GE: 1151 return self.pp_pbcmp(a, d, f, xs) 1152 elif k == Z3_OP_PB_EQ: 1153 return self.pp_pbcmp(a, d, f, xs) 1154 elif z3.is_pattern(a): 1155 return self.pp_pattern(a, d, xs) 1156 elif self.is_infix(k): 1157 return self.pp_infix(a, d, xs) 1158 elif self.is_unary(k): 1159 return self.pp_unary(a, d, xs) 1160 else: 1161 return self.pp_prefix(a, d, xs) 1162 1163 def pp_var(self, a, d, xs): 1164 idx = z3.get_var_index(a) 1165 sz = len(xs) 1166 if idx >= sz: 1167 return seq1("Var", (to_format(idx),)) 1168 else: 1169 return to_format(xs[sz - idx - 1]) 1170 1171 def pp_quantifier(self, a, d, xs): 1172 ys = [to_format(a.var_name(i)) for i in range(a.num_vars())] 1173 new_xs = xs + ys 1174 body_pp = self.pp_expr(a.body(), d + 1, new_xs) 1175 if len(ys) == 1: 1176 ys_pp = ys[0] 1177 else: 1178 ys_pp = seq3(ys, "[", "]") 1179 if a.is_forall(): 1180 header = "ForAll" 1181 elif a.is_exists(): 1182 header = "Exists" 1183 else: 1184 header = "Lambda" 1185 return seq1(header, (ys_pp, body_pp)) 1186 1187 def pp_expr(self, a, d, xs): 1188 self.visited = self.visited + 1 1189 if d > self.max_depth or self.visited > self.max_visited: 1190 return self.pp_ellipses() 1191 if z3.is_app(a): 1192 return self.pp_app(a, d, xs) 1193 elif z3.is_quantifier(a): 1194 return self.pp_quantifier(a, d, xs) 1195 elif z3.is_var(a): 1196 return self.pp_var(a, d, xs) 1197 else: 1198 return to_format(self.pp_unknown()) 1199 1200 def pp_decl(self, f): 1201 k = f.kind() 1202 if k == Z3_OP_DT_IS or k == Z3_OP_ARRAY_MAP: 1203 g = f.params()[0] 1204 r = [to_format(g.name())] 1205 return seq1(self.pp_name(f), r) 1206 return self.pp_name(f) 1207 1208 def pp_seq_core(self, f, a, d, xs): 1209 self.visited = self.visited + 1 1210 if d > self.max_depth or self.visited > self.max_visited: 1211 return self.pp_ellipses() 1212 r = [] 1213 sz = 0 1214 for elem in a: 1215 r.append(f(elem, d + 1, xs)) 1216 sz = sz + 1 1217 if sz > self.max_args: 1218 r.append(self.pp_ellipses()) 1219 break 1220 return seq3(r, "[", "]") 1221 1222 def pp_seq(self, a, d, xs): 1223 return self.pp_seq_core(self.pp_expr, a, d, xs) 1224 1225 def pp_seq_seq(self, a, d, xs): 1226 return self.pp_seq_core(self.pp_seq, a, d, xs) 1227 1228 def pp_model(self, m): 1229 r = [] 1230 sz = 0 1231 for d in m: 1232 i = m[d] 1233 if isinstance(i, z3.FuncInterp): 1234 i_pp = self.pp_func_interp(i) 1235 else: 1236 i_pp = self.pp_expr(i, 0, []) 1237 name = self.pp_name(d) 1238 r.append(compose(name, to_format(" = "), indent(_len(name) + 3, i_pp))) 1239 sz = sz + 1 1240 if sz > self.max_args: 1241 r.append(self.pp_ellipses()) 1242 break 1243 return seq3(r, "[", "]") 1244 1245 def pp_func_entry(self, e): 1246 num = e.num_args() 1247 if num > 1: 1248 args = [] 1249 for i in range(num): 1250 args.append(self.pp_expr(e.arg_value(i), 0, [])) 1251 args_pp = group(seq3(args)) 1252 else: 1253 args_pp = self.pp_expr(e.arg_value(0), 0, []) 1254 value_pp = self.pp_expr(e.value(), 0, []) 1255 return group(seq((args_pp, value_pp), self.pp_arrow())) 1256 1257 def pp_func_interp(self, f): 1258 r = [] 1259 sz = 0 1260 num = f.num_entries() 1261 for i in range(num): 1262 r.append(self.pp_func_entry(f.entry(i))) 1263 sz = sz + 1 1264 if sz > self.max_args: 1265 r.append(self.pp_ellipses()) 1266 break 1267 if sz <= self.max_args: 1268 else_val = f.else_value() 1269 if else_val is None: 1270 else_pp = to_format("#unspecified") 1271 else: 1272 else_pp = self.pp_expr(else_val, 0, []) 1273 r.append(group(seq((to_format("else"), else_pp), self.pp_arrow()))) 1274 return seq3(r, "[", "]") 1275 1276 def pp_list(self, a): 1277 r = [] 1278 sz = 0 1279 for elem in a: 1280 if _support_pp(elem): 1281 r.append(self.main(elem)) 1282 else: 1283 r.append(to_format(str(elem))) 1284 sz = sz + 1 1285 if sz > self.max_args: 1286 r.append(self.pp_ellipses()) 1287 break 1288 if isinstance(a, tuple): 1289 return seq3(r) 1290 else: 1291 return seq3(r, "[", "]") 1292 1293 def main(self, a): 1294 if z3.is_expr(a): 1295 return self.pp_expr(a, 0, []) 1296 elif z3.is_sort(a): 1297 return self.pp_sort(a) 1298 elif z3.is_func_decl(a): 1299 return self.pp_decl(a) 1300 elif isinstance(a, z3.Goal) or isinstance(a, z3.AstVector): 1301 return self.pp_seq(a, 0, []) 1302 elif isinstance(a, z3.Solver): 1303 return self.pp_seq(a.assertions(), 0, []) 1304 elif isinstance(a, z3.Fixedpoint): 1305 return a.sexpr() 1306 elif isinstance(a, z3.Optimize): 1307 return a.sexpr() 1308 elif isinstance(a, z3.ApplyResult): 1309 return self.pp_seq_seq(a, 0, []) 1310 elif isinstance(a, z3.ModelRef): 1311 return self.pp_model(a) 1312 elif isinstance(a, z3.FuncInterp): 1313 return self.pp_func_interp(a) 1314 elif isinstance(a, list) or isinstance(a, tuple): 1315 return self.pp_list(a) 1316 else: 1317 return to_format(self.pp_unknown()) 1318 1319 def __call__(self, a): 1320 self.visited = 0 1321 return self.main(a) 1322 1323 1324class HTMLFormatter(Formatter): 1325 def __init__(self): 1326 Formatter.__init__(self) 1327 global _html_ellipses 1328 self.ellipses = to_format(_html_ellipses) 1329 1330 def pp_arrow(self): 1331 return to_format(" →", 1) 1332 1333 def pp_unknown(self): 1334 return "<b>unknown</b>" 1335 1336 def pp_name(self, a): 1337 r = _html_op_name(a) 1338 if r[0] == "&" or r[0] == "/" or r[0] == "%": 1339 return to_format(r, 1) 1340 else: 1341 pos = r.find("__") 1342 if pos == -1 or pos == 0: 1343 return to_format(r) 1344 else: 1345 sz = len(r) 1346 if pos + 2 == sz: 1347 return to_format(r) 1348 else: 1349 return to_format("%s<sub>%s</sub>" % (r[0:pos], r[pos + 2:sz]), sz - 2) 1350 1351 def is_assoc(self, k): 1352 return _is_html_assoc(k) 1353 1354 def is_left_assoc(self, k): 1355 return _is_html_left_assoc(k) 1356 1357 def is_infix(self, a): 1358 return _is_html_infix(a) 1359 1360 def is_unary(self, a): 1361 return _is_html_unary(a) 1362 1363 def get_precedence(self, a): 1364 return _get_html_precedence(a) 1365 1366 def pp_neq(self): 1367 return to_format("≠") 1368 1369 def pp_power(self, a, d, xs): 1370 arg1_pp = self.pp_power_arg(a.arg(0), d + 1, xs) 1371 arg2_pp = self.pp_expr(a.arg(1), d + 1, xs) 1372 return compose(arg1_pp, to_format("<sup>", 1), arg2_pp, to_format("</sup>", 1)) 1373 1374 def pp_var(self, a, d, xs): 1375 idx = z3.get_var_index(a) 1376 sz = len(xs) 1377 if idx >= sz: 1378 # 957 is the greek letter nu 1379 return to_format("ν<sub>%s</sub>" % idx, 1) 1380 else: 1381 return to_format(xs[sz - idx - 1]) 1382 1383 def pp_quantifier(self, a, d, xs): 1384 ys = [to_format(a.var_name(i)) for i in range(a.num_vars())] 1385 new_xs = xs + ys 1386 body_pp = self.pp_expr(a.body(), d + 1, new_xs) 1387 ys_pp = group(seq(ys)) 1388 if a.is_forall(): 1389 header = "∀" 1390 else: 1391 header = "∃" 1392 return group(compose(to_format(header, 1), 1393 indent(1, compose(ys_pp, to_format(" :"), line_break(), body_pp)))) 1394 1395 1396_PP = PP() 1397_Formatter = Formatter() 1398 1399 1400def set_pp_option(k, v): 1401 if k == "html_mode": 1402 if v: 1403 set_html_mode(True) 1404 else: 1405 set_html_mode(False) 1406 return True 1407 if k == "fpa_pretty": 1408 if v: 1409 set_fpa_pretty(True) 1410 else: 1411 set_fpa_pretty(False) 1412 return True 1413 val = getattr(_PP, k, None) 1414 if val is not None: 1415 _z3_assert(isinstance(v, type(val)), "Invalid pretty print option value") 1416 setattr(_PP, k, v) 1417 return True 1418 val = getattr(_Formatter, k, None) 1419 if val is not None: 1420 _z3_assert(isinstance(v, type(val)), "Invalid pretty print option value") 1421 setattr(_Formatter, k, v) 1422 return True 1423 return False 1424 1425 1426def obj_to_string(a): 1427 out = io.StringIO() 1428 _PP(out, _Formatter(a)) 1429 return out.getvalue() 1430 1431 1432_html_out = None 1433 1434 1435def set_html_mode(flag=True): 1436 global _Formatter 1437 if flag: 1438 _Formatter = HTMLFormatter() 1439 else: 1440 _Formatter = Formatter() 1441 1442 1443def set_fpa_pretty(flag=True): 1444 global _Formatter 1445 global _z3_op_to_str 1446 _Formatter.fpa_pretty = flag 1447 if flag: 1448 for (_k, _v) in _z3_op_to_fpa_pretty_str.items(): 1449 _z3_op_to_str[_k] = _v 1450 for _k in _z3_fpa_infix: 1451 _infix_map[_k] = True 1452 else: 1453 for (_k, _v) in _z3_op_to_fpa_normal_str.items(): 1454 _z3_op_to_str[_k] = _v 1455 for _k in _z3_fpa_infix: 1456 _infix_map[_k] = False 1457 1458 1459set_fpa_pretty(True) 1460 1461 1462def get_fpa_pretty(): 1463 global Formatter 1464 return _Formatter.fpa_pretty 1465 1466 1467def in_html_mode(): 1468 return isinstance(_Formatter, HTMLFormatter) 1469 1470 1471def pp(a): 1472 if _support_pp(a): 1473 print(obj_to_string(a)) 1474 else: 1475 print(a) 1476 1477 1478def print_matrix(m): 1479 _z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected") 1480 if not in_html_mode(): 1481 print(obj_to_string(m)) 1482 else: 1483 print('<table cellpadding="2", cellspacing="0", border="1">') 1484 for r in m: 1485 _z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected") 1486 print("<tr>") 1487 for c in r: 1488 print("<td>%s</td>" % c) 1489 print("</tr>") 1490 print("</table>") 1491 1492 1493def insert_line_breaks(s, width): 1494 """Break s in lines of size width (approx)""" 1495 sz = len(s) 1496 if sz <= width: 1497 return s 1498 new_str = io.StringIO() 1499 w = 0 1500 for i in range(sz): 1501 if w > width and s[i] == " ": 1502 new_str.write(u("<br />")) 1503 w = 0 1504 else: 1505 new_str.write(u(s[i])) 1506 w = w + 1 1507 return new_str.getvalue() 1508