z3.z3printer		index
/home/vsts/work/1/s/build/python/z3/z3printer.py

############################################
# Copyright (c) 2012 Microsoft Corporation
#
# Z3 Python interface
#
# Author: Leonardo de Moura (leonardo)
############################################

 
Modules
       
atexit
builtins
contextlib
ctypes
importlib.resources
io
os
sys
z3.z3

 
Classes
       
builtins.Exception(builtins.BaseException)
StopPPException
builtins.object
FormatObject
IndentFormatObject
LineBreakFormatObject
NAryFormatObject
ChoiceFormatObject
ComposeFormatObject
StringFormatObject
Formatter
HTMLFormatter
PP

 
class ChoiceFormatObject(NAryFormatObject)
    ChoiceFormatObject(fs)
 

 
 
Method resolution order:
ChoiceFormatObject
NAryFormatObject
FormatObject
builtins.object
Methods defined here:
as_tuple(self)
flat(self)
is_choice(sef)
space_upto_nl(self)
Methods inherited from NAryFormatObject:
__init__(self, fs)
Initialize self.  See help(type(self)) for accurate signature.
children(self)
Methods inherited from FormatObject:
is_compose(self)
is_indent(self)
is_linebreak(self)
is_nil(self)
is_string(self)
Data descriptors inherited from FormatObject:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class ComposeFormatObject(NAryFormatObject)
    ComposeFormatObject(fs)
 

 
 
Method resolution order:
ComposeFormatObject
NAryFormatObject
FormatObject
builtins.object
Methods defined here:
as_tuple(self)
flat(self)
is_compose(sef)
space_upto_nl(self)
Methods inherited from NAryFormatObject:
__init__(self, fs)
Initialize self.  See help(type(self)) for accurate signature.
children(self)
Methods inherited from FormatObject:
is_choice(self)
is_indent(self)
is_linebreak(self)
is_nil(self)
is_string(self)
Data descriptors inherited from FormatObject:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class FormatObject(builtins.object)
     Methods defined here:
as_tuple(self)
children(self)
flat(self)
is_choice(self)
is_compose(self)
is_indent(self)
is_linebreak(self)
is_nil(self)
is_string(self)
space_upto_nl(self)
Data descriptors defined here:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class Formatter(builtins.object)
     Methods defined here:
__call__(self, a)
Call self as a function.
__init__(self)
Initialize self.  See help(type(self)) for accurate signature.
add_paren(self, a)
get_precedence(self, a)
infix_args(self, a, d, xs)
infix_args_core(self, a, d, xs, r)
is_assoc(self, k)
is_infix(self, a)
is_infix_compact(self, a)
is_infix_unary(self, a)
is_left_assoc(self, k)
is_unary(self, a)
main(self, a)
pp_K(self, a, d, xs)
pp_algebraic(self, a)
pp_app(self, a, d, xs)
pp_arrow(self)
pp_atleast(self, a, d, f, xs)
pp_atmost(self, a, d, f, xs)
pp_bv(self, a)
pp_char(self, a)
pp_const(self, a)
pp_decl(self, f)
pp_distinct(self, a, d, xs)
pp_ellipses(self)
pp_expr(self, a, d, xs)
pp_extract(self, a, d, xs)
pp_fd(self, a)
pp_fdecl(self, f, a, d, xs)
pp_fp(self, a, d, xs)
pp_fp_value(self, a)
pp_fprm_value(self, a)
pp_func_entry(self, e)
pp_func_interp(self, f)
pp_infix(self, a, d, xs)
pp_int(self, a)
pp_is(self, a, d, xs)
pp_list(self, a)
pp_loop(self, a, d, xs)
pp_map(self, a, d, xs)
pp_model(self, m)
pp_name(self, a)
pp_neq(self)
pp_pattern(self, a, d, xs)
pp_pbcmp(self, a, d, f, xs)
pp_power(self, a, d, xs)
pp_power_arg(self, arg, d, xs)
pp_prefix(self, a, d, xs)
pp_quantifier(self, a, d, xs)
pp_rational(self, a)
pp_select(self, a, d, xs)
pp_seq(self, a, d, xs)
pp_seq_core(self, f, a, d, xs)
pp_seq_seq(self, a, d, xs)
pp_set(self, id, a)
pp_sort(self, s)
pp_string(self, a)
pp_unary(self, a, d, xs)
pp_unary_param(self, a, d, xs)
pp_unknown(self)
pp_var(self, a, d, xs)
Data descriptors defined here:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class HTMLFormatter(Formatter)
    
Method resolution order:
HTMLFormatter
Formatter
builtins.object
Methods defined here:
__init__(self)
Initialize self.  See help(type(self)) for accurate signature.
get_precedence(self, a)
is_assoc(self, k)
is_infix(self, a)
is_left_assoc(self, k)
is_unary(self, a)
pp_arrow(self)
pp_name(self, a)
pp_neq(self)
pp_power(self, a, d, xs)
pp_quantifier(self, a, d, xs)
pp_unknown(self)
pp_var(self, a, d, xs)
Methods inherited from Formatter:
__call__(self, a)
Call self as a function.
add_paren(self, a)
infix_args(self, a, d, xs)
infix_args_core(self, a, d, xs, r)
is_infix_compact(self, a)
is_infix_unary(self, a)
main(self, a)
pp_K(self, a, d, xs)
pp_algebraic(self, a)
pp_app(self, a, d, xs)
pp_atleast(self, a, d, f, xs)
pp_atmost(self, a, d, f, xs)
pp_bv(self, a)
pp_char(self, a)
pp_const(self, a)
pp_decl(self, f)
pp_distinct(self, a, d, xs)
pp_ellipses(self)
pp_expr(self, a, d, xs)
pp_extract(self, a, d, xs)
pp_fd(self, a)
pp_fdecl(self, f, a, d, xs)
pp_fp(self, a, d, xs)
pp_fp_value(self, a)
pp_fprm_value(self, a)
pp_func_entry(self, e)
pp_func_interp(self, f)
pp_infix(self, a, d, xs)
pp_int(self, a)
pp_is(self, a, d, xs)
pp_list(self, a)
pp_loop(self, a, d, xs)
pp_map(self, a, d, xs)
pp_model(self, m)
pp_pattern(self, a, d, xs)
pp_pbcmp(self, a, d, f, xs)
pp_power_arg(self, arg, d, xs)
pp_prefix(self, a, d, xs)
pp_rational(self, a)
pp_select(self, a, d, xs)
pp_seq(self, a, d, xs)
pp_seq_core(self, f, a, d, xs)
pp_seq_seq(self, a, d, xs)
pp_set(self, id, a)
pp_sort(self, s)
pp_string(self, a)
pp_unary(self, a, d, xs)
pp_unary_param(self, a, d, xs)
Data descriptors inherited from Formatter:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class IndentFormatObject(FormatObject)
    IndentFormatObject(indent, child)
 

 
 
Method resolution order:
IndentFormatObject
FormatObject
builtins.object
Methods defined here:
__init__(self, indent, child)
Initialize self.  See help(type(self)) for accurate signature.
as_tuple(self)
children(self)
flat(self)
is_indent(self)
space_upto_nl(self)
Methods inherited from FormatObject:
is_choice(self)
is_compose(self)
is_linebreak(self)
is_nil(self)
is_string(self)
Data descriptors inherited from FormatObject:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class LineBreakFormatObject(FormatObject)
    
Method resolution order:
LineBreakFormatObject
FormatObject
builtins.object
Methods defined here:
__init__(self)
Initialize self.  See help(type(self)) for accurate signature.
as_tuple(self)
flat(self)
is_linebreak(self)
space_upto_nl(self)
Methods inherited from FormatObject:
children(self)
is_choice(self)
is_compose(self)
is_indent(self)
is_nil(self)
is_string(self)
Data descriptors inherited from FormatObject:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class NAryFormatObject(FormatObject)
    NAryFormatObject(fs)
 

 
 
Method resolution order:
NAryFormatObject
FormatObject
builtins.object
Methods defined here:
__init__(self, fs)
Initialize self.  See help(type(self)) for accurate signature.
children(self)
Methods inherited from FormatObject:
as_tuple(self)
flat(self)
is_choice(self)
is_compose(self)
is_indent(self)
is_linebreak(self)
is_nil(self)
is_string(self)
space_upto_nl(self)
Data descriptors inherited from FormatObject:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class PP(builtins.object)
     Methods defined here:
__call__(self, out, f)
Call self as a function.
__init__(self)
Initialize self.  See help(type(self)) for accurate signature.
pp(self, f, indent)
pp_choice(self, f, indent)
pp_compose(self, f, indent)
pp_line_break(self, f, indent)
pp_string(self, f, indent)
Data descriptors defined here:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
class StopPPException(builtins.Exception)
    
Method resolution order:
StopPPException
builtins.Exception
builtins.BaseException
builtins.object
Methods defined here:
__str__(self)
Return str(self).
Data descriptors defined here:
__weakref__
list of weak references to the object (if defined)
Methods inherited from builtins.Exception:
__init__(self, /, *args, **kwargs)
Initialize self.  See help(type(self)) for accurate signature.
Static methods inherited from builtins.Exception:
__new__(*args, **kwargs) from builtins.type
Create and return a new object.  See help(type) for accurate signature.
Methods inherited from builtins.BaseException:
__delattr__(self, name, /)
Implement delattr(self, name).
__getattribute__(self, name, /)
Return getattr(self, name).
__reduce__(...)
Helper for pickle.
__repr__(self, /)
Return repr(self).
__setattr__(self, name, value, /)
Implement setattr(self, name, value).
__setstate__(...)
with_traceback(...)
Exception.with_traceback(tb) --
set self.__traceback__ to tb and return self.
Data descriptors inherited from builtins.BaseException:
__cause__
exception cause
__context__
exception context
__dict__
__suppress_context__
__traceback__
args

 
class StringFormatObject(FormatObject)
    StringFormatObject(string)
 

 
 
Method resolution order:
StringFormatObject
FormatObject
builtins.object
Methods defined here:
__init__(self, string)
Initialize self.  See help(type(self)) for accurate signature.
as_tuple(self)
is_string(self)
space_upto_nl(self)
Methods inherited from FormatObject:
children(self)
flat(self)
is_choice(self)
is_compose(self)
is_indent(self)
is_linebreak(self)
is_nil(self)
Data descriptors inherited from FormatObject:
__dict__
dictionary for instance variables (if defined)
__weakref__
list of weak references to the object (if defined)

 
Functions
       
POINTER(...)
addressof(...)
addressof(C instance) -> integer
Return the address of the C instance internal buffer
alignment(...)
alignment(C type) -> integer
alignment(C instance) -> integer
Return the alignment requirements of a C instance
byref(...)
byref(C instance[, offset=0]) -> byref-object
Return a pointer lookalike to a C instance, only usable
as function argument
compose(*args)
fits(f, space_left)
get_errno(...)
get_fpa_pretty()
group(arg)
in_html_mode()
indent(i, arg)
insert_line_breaks(s, width)
Break s in lines of size width (approx)
line_break()
obj_to_string(a)
pointer(...)
pp(a)
print_matrix(m)
resize(...)
Resize the memory buffer of a ctypes instance
seq(args, sep=',', space=True)
seq1(header, args, lp='(', rp=')')
seq2(header, args, i=4, lp='(', rp=')')
seq3(args, lp='(', rp=')')
set_errno(...)
set_fpa_pretty(flag=True)
set_html_mode(flag=True)
set_pp_option(k, v)
sizeof(...)
sizeof(C type) -> integer
sizeof(C instance) -> integer
Return the size in bytes of a C instance
to_format(arg, size=None)
u(x)

 
Data
        DEFAULT_MODE = 0
RTLD_GLOBAL = 256
RTLD_LOCAL = 0
Z3_APP_AST = 1
Z3_ARRAY_SORT = 5
Z3_BOOL_SORT = 1
Z3_BV_SORT = 4
Z3_CHAR_SORT = 13
Z3_DATATYPE_SORT = 6
Z3_DEC_REF_ERROR = 11
Z3_EXCEPTION = 12
Z3_FILE_ACCESS_ERROR = 8
Z3_FINITE_DOMAIN_SORT = 8
Z3_FLOATING_POINT_SORT = 9
Z3_FUNC_DECL_AST = 5
Z3_GOAL_OVER = 2
Z3_GOAL_PRECISE = 0
Z3_GOAL_UNDER = 1
Z3_GOAL_UNDER_OVER = 3
Z3_INTERNAL_FATAL = 9
Z3_INT_SORT = 2
Z3_INT_SYMBOL = 0
Z3_INVALID_ARG = 3
Z3_INVALID_PATTERN = 6
Z3_INVALID_USAGE = 10
Z3_IOB = 2
Z3_L_FALSE = -1
Z3_L_TRUE = 1
Z3_L_UNDEF = 0
Z3_MEMOUT_FAIL = 7
Z3_NO_PARSER = 5
Z3_NUMERAL_AST = 0
Z3_OK = 0
Z3_OP_ABS = 530
Z3_OP_ADD = 518
Z3_OP_AGNUM = 513
Z3_OP_AND = 261
Z3_OP_ANUM = 512
Z3_OP_ARRAY_DEFAULT = 772
Z3_OP_ARRAY_EXT = 779
Z3_OP_ARRAY_MAP = 771
Z3_OP_AS_ARRAY = 778
Z3_OP_BADD = 1028
Z3_OP_BAND = 1049
Z3_OP_BASHR = 1066
Z3_OP_BCOMP = 1063
Z3_OP_BIT0 = 1026
Z3_OP_BIT1 = 1025
Z3_OP_BIT2BOOL = 1071
Z3_OP_BLSHR = 1065
Z3_OP_BMUL = 1030
Z3_OP_BNAND = 1053
Z3_OP_BNEG = 1027
Z3_OP_BNOR = 1054
Z3_OP_BNOT = 1051
Z3_OP_BNUM = 1024
Z3_OP_BOR = 1050
Z3_OP_BREDAND = 1062
Z3_OP_BREDOR = 1061
Z3_OP_BSDIV = 1031
Z3_OP_BSDIV0 = 1036
Z3_OP_BSDIV_I = 1079
Z3_OP_BSHL = 1064
Z3_OP_BSMOD = 1035
Z3_OP_BSMOD0 = 1040
Z3_OP_BSMOD_I = 1083
Z3_OP_BSMUL_NO_OVFL = 1076
Z3_OP_BSMUL_NO_UDFL = 1078
Z3_OP_BSREM = 1033
Z3_OP_BSREM0 = 1038
Z3_OP_BSREM_I = 1081
Z3_OP_BSUB = 1029
Z3_OP_BUDIV = 1032
Z3_OP_BUDIV0 = 1037
Z3_OP_BUDIV_I = 1080
Z3_OP_BUMUL_NO_OVFL = 1077
Z3_OP_BUREM = 1034
Z3_OP_BUREM0 = 1039
Z3_OP_BUREM_I = 1082
Z3_OP_BV2INT = 1073
Z3_OP_BXNOR = 1055
Z3_OP_BXOR = 1052
Z3_OP_CARRY = 1074
Z3_OP_CHAR_CONST = 1598
Z3_OP_CHAR_FROM_BV = 1602
Z3_OP_CHAR_IS_DIGIT = 1603
Z3_OP_CHAR_LE = 1599
Z3_OP_CHAR_TO_BV = 1601
Z3_OP_CHAR_TO_INT = 1600
Z3_OP_CONCAT = 1056
Z3_OP_CONST_ARRAY = 770
Z3_OP_DISTINCT = 259
Z3_OP_DIV = 522
Z3_OP_DT_ACCESSOR = 2051
Z3_OP_DT_CONSTRUCTOR = 2048
Z3_OP_DT_IS = 2050
Z3_OP_DT_RECOGNISER = 2049
Z3_OP_DT_UPDATE_FIELD = 2052
Z3_OP_EQ = 258
Z3_OP_EXTRACT = 1059
Z3_OP_EXT_ROTATE_LEFT = 1069
Z3_OP_EXT_ROTATE_RIGHT = 1070
Z3_OP_FALSE = 257
Z3_OP_FD_CONSTANT = 1549
Z3_OP_FD_LT = 1550
Z3_OP_FPA_ABS = 45073
Z3_OP_FPA_ADD = 45067
Z3_OP_FPA_BV2RM = 45099
Z3_OP_FPA_BVWRAP = 45098
Z3_OP_FPA_DIV = 45071
Z3_OP_FPA_EQ = 45079
Z3_OP_FPA_FMA = 45076
Z3_OP_FPA_FP = 45091
Z3_OP_FPA_GE = 45083
Z3_OP_FPA_GT = 45081
Z3_OP_FPA_IS_INF = 45085
Z3_OP_FPA_IS_NAN = 45084
Z3_OP_FPA_IS_NEGATIVE = 45089
Z3_OP_FPA_IS_NORMAL = 45087
Z3_OP_FPA_IS_POSITIVE = 45090
Z3_OP_FPA_IS_SUBNORMAL = 45088
Z3_OP_FPA_IS_ZERO = 45086
Z3_OP_FPA_LE = 45082
Z3_OP_FPA_LT = 45080
Z3_OP_FPA_MAX = 45075
Z3_OP_FPA_MIN = 45074
Z3_OP_FPA_MINUS_INF = 45063
Z3_OP_FPA_MINUS_ZERO = 45066
Z3_OP_FPA_MUL = 45070
Z3_OP_FPA_NAN = 45064
Z3_OP_FPA_NEG = 45069
Z3_OP_FPA_NUM = 45061
Z3_OP_FPA_PLUS_INF = 45062
Z3_OP_FPA_PLUS_ZERO = 45065
Z3_OP_FPA_REM = 45072
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 45057
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 45056
Z3_OP_FPA_RM_TOWARD_NEGATIVE = 45059
Z3_OP_FPA_RM_TOWARD_POSITIVE = 45058
Z3_OP_FPA_RM_TOWARD_ZERO = 45060
Z3_OP_FPA_ROUND_TO_INTEGRAL = 45078
Z3_OP_FPA_SQRT = 45077
Z3_OP_FPA_SUB = 45068
Z3_OP_FPA_TO_FP = 45092
Z3_OP_FPA_TO_FP_UNSIGNED = 45093
Z3_OP_FPA_TO_IEEE_BV = 45097
Z3_OP_FPA_TO_REAL = 45096
Z3_OP_FPA_TO_SBV = 45095
Z3_OP_FPA_TO_UBV = 45094
Z3_OP_GE = 515
Z3_OP_GT = 517
Z3_OP_IDIV = 523
Z3_OP_IFF = 263
Z3_OP_IMPLIES = 266
Z3_OP_INT2BV = 1072
Z3_OP_INTERNAL = 45100
Z3_OP_INT_TO_STR = 1574
Z3_OP_IS_INT = 528
Z3_OP_ITE = 260
Z3_OP_LABEL = 1792
Z3_OP_LABEL_LIT = 1793
Z3_OP_LE = 514
Z3_OP_LT = 516
Z3_OP_MOD = 525
Z3_OP_MUL = 521
Z3_OP_NOT = 265
Z3_OP_OEQ = 267
Z3_OP_OR = 262
Z3_OP_PB_AT_LEAST = 2305
Z3_OP_PB_AT_MOST = 2304
Z3_OP_PB_EQ = 2308
Z3_OP_PB_GE = 2307
Z3_OP_PB_LE = 2306
Z3_OP_POWER = 529
Z3_OP_PR_AND_ELIM = 1293
Z3_OP_PR_APPLY_DEF = 1314
Z3_OP_PR_ASSERTED = 1282
Z3_OP_PR_ASSUMPTION_ADD = 1309
Z3_OP_PR_BIND = 1291
Z3_OP_PR_CLAUSE_TRAIL = 1312
Z3_OP_PR_COMMUTATIVITY = 1307
Z3_OP_PR_DEF_AXIOM = 1308
Z3_OP_PR_DEF_INTRO = 1313
Z3_OP_PR_DER = 1300
Z3_OP_PR_DISTRIBUTIVITY = 1292
Z3_OP_PR_ELIM_UNUSED_VARS = 1299
Z3_OP_PR_GOAL = 1283
Z3_OP_PR_HYPER_RESOLVE = 1321
Z3_OP_PR_HYPOTHESIS = 1302
Z3_OP_PR_IFF_FALSE = 1306
Z3_OP_PR_IFF_OEQ = 1315
Z3_OP_PR_IFF_TRUE = 1305
Z3_OP_PR_LEMMA = 1303
Z3_OP_PR_LEMMA_ADD = 1310
Z3_OP_PR_MODUS_PONENS = 1284
Z3_OP_PR_MODUS_PONENS_OEQ = 1319
Z3_OP_PR_MONOTONICITY = 1289
Z3_OP_PR_NNF_NEG = 1317
Z3_OP_PR_NNF_POS = 1316
Z3_OP_PR_NOT_OR_ELIM = 1294
Z3_OP_PR_PULL_QUANT = 1297
Z3_OP_PR_PUSH_QUANT = 1298
Z3_OP_PR_QUANT_INST = 1301
Z3_OP_PR_QUANT_INTRO = 1290
Z3_OP_PR_REDUNDANT_DEL = 1311
Z3_OP_PR_REFLEXIVITY = 1285
Z3_OP_PR_REWRITE = 1295
Z3_OP_PR_REWRITE_STAR = 1296
Z3_OP_PR_SKOLEMIZE = 1318
Z3_OP_PR_SYMMETRY = 1286
Z3_OP_PR_TH_LEMMA = 1320
Z3_OP_PR_TRANSITIVITY = 1287
Z3_OP_PR_TRANSITIVITY_STAR = 1288
Z3_OP_PR_TRUE = 1281
Z3_OP_PR_UNDEF = 1280
Z3_OP_PR_UNIT_RESOLUTION = 1304
Z3_OP_RA_CLONE = 1548
Z3_OP_RA_COMPLEMENT = 1546
Z3_OP_RA_EMPTY = 1537
Z3_OP_RA_FILTER = 1543
Z3_OP_RA_IS_EMPTY = 1538
Z3_OP_RA_JOIN = 1539
Z3_OP_RA_NEGATION_FILTER = 1544
Z3_OP_RA_PROJECT = 1542
Z3_OP_RA_RENAME = 1545
Z3_OP_RA_SELECT = 1547
Z3_OP_RA_STORE = 1536
Z3_OP_RA_UNION = 1540
Z3_OP_RA_WIDEN = 1541
Z3_OP_RECURSIVE = 45101
Z3_OP_REM = 524
Z3_OP_REPEAT = 1060
Z3_OP_RE_COMPLEMENT = 1591
Z3_OP_RE_CONCAT = 1584
Z3_OP_RE_DERIVATIVE = 1597
Z3_OP_RE_DIFF = 1587
Z3_OP_RE_EMPTY_SET = 1592
Z3_OP_RE_FULL_CHAR_SET = 1594
Z3_OP_RE_FULL_SET = 1593
Z3_OP_RE_INTERSECT = 1588
Z3_OP_RE_LOOP = 1589
Z3_OP_RE_OF_PRED = 1595
Z3_OP_RE_OPTION = 1583
Z3_OP_RE_PLUS = 1581
Z3_OP_RE_POWER = 1590
Z3_OP_RE_RANGE = 1586
Z3_OP_RE_REVERSE = 1596
Z3_OP_RE_STAR = 1582
Z3_OP_RE_UNION = 1585
Z3_OP_ROTATE_LEFT = 1067
Z3_OP_ROTATE_RIGHT = 1068
Z3_OP_SBV_TO_STR = 1576
Z3_OP_SELECT = 769
Z3_OP_SEQ_AT = 1562
Z3_OP_SEQ_CONCAT = 1553
Z3_OP_SEQ_CONTAINS = 1556
Z3_OP_SEQ_EMPTY = 1552
Z3_OP_SEQ_EXTRACT = 1557
Z3_OP_SEQ_FOLDL = 1571
Z3_OP_SEQ_FOLDLI = 1572
Z3_OP_SEQ_INDEX = 1565
Z3_OP_SEQ_IN_RE = 1568
Z3_OP_SEQ_LAST_INDEX = 1566
Z3_OP_SEQ_LENGTH = 1564
Z3_OP_SEQ_MAP = 1569
Z3_OP_SEQ_MAPI = 1570
Z3_OP_SEQ_NTH = 1563
Z3_OP_SEQ_PREFIX = 1554
Z3_OP_SEQ_REPLACE = 1558
Z3_OP_SEQ_REPLACE_ALL = 1561
Z3_OP_SEQ_REPLACE_RE = 1559
Z3_OP_SEQ_REPLACE_RE_ALL = 1560
Z3_OP_SEQ_SUFFIX = 1555
Z3_OP_SEQ_TO_RE = 1567
Z3_OP_SEQ_UNIT = 1551
Z3_OP_SET_CARD = 781
Z3_OP_SET_COMPLEMENT = 776
Z3_OP_SET_DIFFERENCE = 775
Z3_OP_SET_HAS_SIZE = 780
Z3_OP_SET_INTERSECT = 774
Z3_OP_SET_SUBSET = 777
Z3_OP_SET_UNION = 773
Z3_OP_SGEQ = 1044
Z3_OP_SGT = 1048
Z3_OP_SIGN_EXT = 1057
Z3_OP_SLEQ = 1042
Z3_OP_SLT = 1046
Z3_OP_SPECIAL_RELATION_LO = 40960
Z3_OP_SPECIAL_RELATION_PLO = 40962
Z3_OP_SPECIAL_RELATION_PO = 40961
Z3_OP_SPECIAL_RELATION_TC = 40964
Z3_OP_SPECIAL_RELATION_TO = 40963
Z3_OP_SPECIAL_RELATION_TRC = 40965
Z3_OP_STORE = 768
Z3_OP_STRING_LE = 1580
Z3_OP_STRING_LT = 1579
Z3_OP_STR_FROM_CODE = 1578
Z3_OP_STR_TO_CODE = 1577
Z3_OP_STR_TO_INT = 1573
Z3_OP_SUB = 519
Z3_OP_TO_INT = 527
Z3_OP_TO_REAL = 526
Z3_OP_TRUE = 256
Z3_OP_UBV_TO_STR = 1575
Z3_OP_UGEQ = 1043
Z3_OP_UGT = 1047
Z3_OP_ULEQ = 1041
Z3_OP_ULT = 1045
Z3_OP_UMINUS = 520
Z3_OP_UNINTERPRETED = 45102
Z3_OP_XOR = 264
Z3_OP_XOR3 = 1075
Z3_OP_ZERO_EXT = 1058
Z3_PARAMETER_AST = 5
Z3_PARAMETER_DOUBLE = 1
Z3_PARAMETER_FUNC_DECL = 6
Z3_PARAMETER_INT = 0
Z3_PARAMETER_RATIONAL = 2
Z3_PARAMETER_SORT = 4
Z3_PARAMETER_SYMBOL = 3
Z3_PARSER_ERROR = 4
Z3_PK_BOOL = 1
Z3_PK_DOUBLE = 2
Z3_PK_INVALID = 6
Z3_PK_OTHER = 5
Z3_PK_STRING = 4
Z3_PK_SYMBOL = 3
Z3_PK_UINT = 0
Z3_PRINT_LOW_LEVEL = 1
Z3_PRINT_SMTLIB2_COMPLIANT = 2
Z3_PRINT_SMTLIB_FULL = 0
Z3_QUANTIFIER_AST = 3
Z3_REAL_SORT = 3
Z3_RELATION_SORT = 7
Z3_RE_SORT = 12
Z3_ROUNDING_MODE_SORT = 10
Z3_SEQ_SORT = 11
Z3_SORT_AST = 4
Z3_SORT_ERROR = 1
Z3_STRING_SYMBOL = 1
Z3_TYPE_VAR = 14
Z3_UNINTERPRETED_SORT = 0
Z3_UNKNOWN_AST = 1000
Z3_UNKNOWN_SORT = 1000
Z3_VAR_AST = 2
cdll = <ctypes.LibraryLoader object>
d = '/home/vsts/work/1/s/build/libz3.so'
lds = ['/home/vsts/.opam/default/bin', '/snap/bin', '/home/vsts/.local/bin', '/opt/pipx_bin', '/home/vsts/.cargo/bin', '/home/vsts/.config/composer/vendor/bin', '/usr/local/.ghcup/bin', '/home/vsts/.dotnet/tools', '/usr/local/sbin', '/usr/local/bin', '/usr/sbin', '/usr/bin', '/sbin', '/bin', '/usr/games', '/usr/local/games', '/snap/bin']
lp = '/home/vsts/.opam/default/bin:/snap/bin:/home/vst...:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin'
memmove = <CFunctionType object>
memset = <CFunctionType object>
pydll = <ctypes.LibraryLoader object>
pythonapi = <PyDLL 'None', handle 7f198ae802e0>
v = 'PYTHONPATH'