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

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

 
Modules
       
codecs
copy
ctypes
io
math
os
pkg_resources
sys
z3.z3
z3.z3core

 
Classes
       
Numeral

 
class Numeral
    A Z3 numeral can be used to perform computations over arbitrary
precision integers, rationals and real algebraic numbers.
It also automatically converts python numeric values.
 
>>> Numeral(2)
2
>>> Numeral("3/2") + 1
5/2
>>> Numeral(Sqrt(2))
1.4142135623?
>>> Numeral(Sqrt(2)) + 2
3.4142135623?
>>> Numeral(Sqrt(2)) + Numeral(Sqrt(3))
3.1462643699?
 
Z3 numerals can be used to perform computations with
values in a Z3 model.
 
>>> s = Solver()
>>> x = Real('x')
>>> s.add(x*x == 2)
>>> s.add(x > 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[x]
1.4142135623?
>>> m[x] + 1
1.4142135623? + 1
 
The previous result is a Z3 expression.
 
>>> (m[x] + 1).sexpr()
'(+ (root-obj (+ (^ x 2) (- 2)) 2) 1.0)'
 
>>> Numeral(m[x]) + 1
2.4142135623?
>>> Numeral(m[x]).is_pos()
True
>>> Numeral(m[x])**2
2
 
We can also isolate the roots of polynomials.
 
>>> x0, x1, x2 = RealVarVector(3)
>>> r0 = isolate_roots(x0**5 - x0 - 1)
>>> r0
[1.1673039782?]
 
In the following example, we are isolating the roots
of a univariate polynomial (on x1) obtained after substituting
x0 -> r0[0]
 
>>> r1 = isolate_roots(x1**2 - x0 + 1, [ r0[0] ])
>>> r1
[-0.4090280898?, 0.4090280898?]
 
Similarly, in the next example we isolate the roots of
a univariate polynomial (on x2) obtained after substituting
x0 -> r0[0] and x1 -> r1[0]
 
>>> isolate_roots(x1*x2 + x0, [ r0[0], r1[0] ])
[2.8538479564?]
 
  Methods defined here:
__add__(self, other)
Return the numeral `self + other`.
 
>>> Numeral(2) + 3
5
>>> Numeral(2) + Numeral(4)
6
>>> Numeral("2/3") + 1
5/3
__del__(self)
__div__(self, other)
Return the numeral `self / other`.
>>> Numeral(2) / 3
2/3
>>> Numeral(2).root(2) / 3
0.4714045207?
>>> Numeral(Sqrt(2)) / Numeral(Sqrt(3))
0.8164965809?
__eq__(self, other)
Return True if `self == other`.
 
>>> Numeral(Sqrt(2)) == 2
False
>>> Numeral(Sqrt(3)) == Numeral(Sqrt(2))
False
>>> Numeral(Sqrt(2)) == Numeral(Sqrt(2))
True
__ge__(self, other)
Return True if `self >= other`.
 
>>> Numeral(Sqrt(2)) >= 2
False
>>> Numeral(Sqrt(3)) >= Numeral(Sqrt(2))
True
>>> Numeral(Sqrt(2)) >= Numeral(Sqrt(2))
True
__gt__(self, other)
Return True if `self > other`.
 
>>> Numeral(Sqrt(2)) > 2
False
>>> Numeral(Sqrt(3)) > Numeral(Sqrt(2))
True
>>> Numeral(Sqrt(2)) > Numeral(Sqrt(2))
False
__init__(self, num, ctx=None)
__le__(self, other)
Return True if `self <= other`.
 
>>> Numeral(Sqrt(2)) <= 2
True
>>> Numeral(Sqrt(3)) <= Numeral(Sqrt(2))
False
>>> Numeral(Sqrt(2)) <= Numeral(Sqrt(2))
True
__lt__(self, other)
Return True if `self < other`.
 
>>> Numeral(Sqrt(2)) < 2
True
>>> Numeral(Sqrt(3)) < Numeral(Sqrt(2))
False
>>> Numeral(Sqrt(2)) < Numeral(Sqrt(2))
False
__mul__(self, other)
Return the numeral `self * other`.
>>> Numeral(2) * 3
6
__ne__(self, other)
Return True if `self != other`.
 
>>> Numeral(Sqrt(2)) != 2
True
>>> Numeral(Sqrt(3)) != Numeral(Sqrt(2))
True
>>> Numeral(Sqrt(2)) != Numeral(Sqrt(2))
False
__pow__(self, k)
Return the numeral `self^k`.
 
>>> sqrt3 = Numeral(3).root(2)
>>> sqrt3
1.7320508075?
>>> sqrt3**2
3
__radd__(self, other)
Return the numeral `other + self`.
 
>>> 3 + Numeral(2)
5
__rdiv__(self, other)
Return the numeral `other / self`.
>>> 3 / Numeral(2)
3/2
>>> 3 / Numeral(2).root(2)
2.1213203435?
__repr__(self)
__rge__(self, other)
Return True if `other >= self`.
 
>>> 2 >= Numeral(Sqrt(2))
True
__rgt__(self, other)
Return True if `other > self`.
 
>>> 2 > Numeral(Sqrt(2))
True
__rle__(self, other)
Return True if `other <= self`.
 
>>> 2 <= Numeral(Sqrt(2))
False
__rlt__(self, other)
Return True if `other < self`.
 
>>> 2 < Numeral(Sqrt(2))
False
__rmul__(self, other)
Return the numeral `other * mul`.
>>> 3 * Numeral(2)
6
__rsub__(self, other)
Return the numeral `other - self`.
 
>>> 3 - Numeral(2)
1
__rtruediv__(self, other)
__str__(self)
__sub__(self, other)
Return the numeral `self - other`.
 
>>> Numeral(2) - 3
-1
__truediv__(self, other)
approx(self, precision=10)
Return a numeral that approximates the numeral `self`.
The result `r` is such that |r - self| <= 1/10^precision
 
If `self` is rational, then the result is `self`.
 
>>> x = Numeral(2).root(2)
>>> x.approx(20)
6838717160008073720548335/4835703278458516698824704
>>> x.approx(5)
2965821/2097152
>>> Numeral(2).approx(10)
2
as_ast(self)
as_fraction(self)
Return a numeral (that is a rational) as a Python Fraction.
>>> Numeral("1/5").as_fraction()
Fraction(1, 5)
as_long(self)
Return a numeral (that is an integer) as a Python long.
ctx_ref(self)
denominator(self)
Return the denominator if `self` is rational.
 
>>> Numeral("2/3").denominator()
3
is_integer(self)
Return True if the numeral is integer.
 
>>> Numeral(2).is_integer()
True
>>> (Numeral(Sqrt(2)) * Numeral(Sqrt(2))).is_integer()
True
>>> Numeral(Sqrt(2)).is_integer()
False
>>> Numeral("2/3").is_integer()
False
is_irrational(self)
Return True if the numeral is irrational.
 
>>> Numeral(2).is_irrational()
False
>>> Numeral("2/3").is_irrational()
False
>>> Numeral(Sqrt(2)).is_irrational()
True
is_neg(self)
Return True if the numeral is negative.
 
>>> Numeral(2).is_neg()
False
>>> Numeral(-3).is_neg()
True
>>> Numeral(0).is_neg()
False
is_pos(self)
Return True if the numeral is positive.
 
>>> Numeral(2).is_pos()
True
>>> Numeral(-3).is_pos()
False
>>> Numeral(0).is_pos()
False
is_rational(self)
Return True if the numeral is rational.
 
>>> Numeral(2).is_rational()
True
>>> Numeral("2/3").is_rational()
True
>>> Numeral(Sqrt(2)).is_rational()
False
is_zero(self)
Return True if the numeral is zero.
 
>>> Numeral(2).is_zero()
False
>>> Numeral(-3).is_zero()
False
>>> Numeral(0).is_zero()
True
>>> sqrt2 = Numeral(2).root(2)
>>> sqrt2.is_zero()
False
>>> (sqrt2 - sqrt2).is_zero()
True
lower(self, precision=10)
Return a lower bound that approximates the numeral `self`.
The result `r` is such that self - r <= 1/10^precision
 
If `self` is rational, then the result is `self`.
 
>>> x = Numeral(2).root(2)
>>> x.lower(20)
1709679290002018430137083/1208925819614629174706176
>>> Numeral("2/3").lower(10)
2/3
numerator(self)
Return the numerator if `self` is rational.
 
>>> Numeral("2/3").numerator()
2
power(self, k)
Return the numeral `self^k`.
 
>>> sqrt3 = Numeral(3).root(2)
>>> sqrt3
1.7320508075?
>>> sqrt3.power(2)
3
root(self, k)
Return the numeral `self^(1/k)`.
 
>>> sqrt2 = Numeral(2).root(2)
>>> sqrt2
1.4142135623?
>>> sqrt2 * sqrt2
2
>>> sqrt2 * 2 + 1
3.8284271247?
>>> (sqrt2 * 2 + 1).sexpr()
'(root-obj (+ (^ x 2) (* (- 2) x) (- 7)) 2)'
sexpr(self)
sign(self)
Return the sign of the numeral.
 
>>> Numeral(2).sign()
1
>>> Numeral(-3).sign()
-1
>>> Numeral(0).sign()
0
upper(self, precision=10)
Return a upper bound that approximates the numeral `self`.
The result `r` is such that r - self <= 1/10^precision
 
If `self` is rational, then the result is `self`.
 
>>> x = Numeral(2).root(2)
>>> x.upper(20)
6838717160008073720548335/4835703278458516698824704
>>> x.upper(5)
2965821/2097152
>>> Numeral(2).upper(10)
2

 
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
eval_sign_at(p, vs)
Evaluate the sign of the polynomial `p` at `vs`.  `p` is a Z3
Expression containing arithmetic operators: +, -, *, ^k where k is
an integer; and free variables x that is_var(x) is True. Moreover,
all variables must be real.
 
The result is 1 if the polynomial is positive at the given point,
-1 if negative, and 0 if zero.
 
>>> x0, x1, x2 = RealVarVector(3)
>>> eval_sign_at(x0**2 + x1*x2 + 1, (Numeral(0), Numeral(1), Numeral(2)))
1
>>> eval_sign_at(x0**2 - 2, [ Numeral(Sqrt(2)) ])
0
>>> eval_sign_at((x0 + x1)*(x0 + x2), (Numeral(0), Numeral(Sqrt(2)), Numeral(Sqrt(3))))
1
get_errno(...)
isolate_roots(p, vs=[])
Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
roots of the univariate polynomial p(vs[0], ..., vs[len(vs)-1], x_n).
 
Remarks:
* p is a Z3 expression that contains only arithmetic terms and free variables.
* forall i in [0, n) vs is a numeral.
 
The result is a list of numerals
 
>>> x0 = RealVar(0)
>>> isolate_roots(x0**5 - x0 - 1)
[1.1673039782?]
>>> x1 = RealVar(1)
>>> isolate_roots(x0**2 - x1**4 - 1, [ Numeral(Sqrt(3)) ])
[-1.1892071150?, 1.1892071150?]
>>> x2 = RealVar(2)
>>> isolate_roots(x2**2 + x0 - x1, [ Numeral(Sqrt(3)), Numeral(Sqrt(2)) ])
[]
pointer(...)
resize(...)
Resize the memory buffer of a ctypes instance
set_conversion_mode(...)
set_conversion_mode(encoding, errors) -> (previous-encoding, previous-errors)
 
Set the encoding and error handling ctypes uses when converting
between unicode and strings.  Returns the previous values.
set_errno(...)
sizeof(...)
sizeof(C type) -> integer
sizeof(C instance) -> integer
Return the size in bytes of a C instance

 
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_DATATYPE_SORT = 6
Z3_DEBUG = True
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_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_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 = 1567
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_REM = 524
Z3_OP_REPEAT = 1060
Z3_OP_RE_COMPLEMENT = 1580
Z3_OP_RE_CONCAT = 1573
Z3_OP_RE_EMPTY_SET = 1578
Z3_OP_RE_FULL_SET = 1579
Z3_OP_RE_INTERSECT = 1577
Z3_OP_RE_LOOP = 1576
Z3_OP_RE_OPTION = 1572
Z3_OP_RE_PLUS = 1570
Z3_OP_RE_RANGE = 1575
Z3_OP_RE_STAR = 1571
Z3_OP_RE_UNION = 1574
Z3_OP_ROTATE_LEFT = 1067
Z3_OP_ROTATE_RIGHT = 1068
Z3_OP_SELECT = 769
Z3_OP_SEQ_AT = 1559
Z3_OP_SEQ_CONCAT = 1553
Z3_OP_SEQ_CONTAINS = 1556
Z3_OP_SEQ_EMPTY = 1552
Z3_OP_SEQ_EXTRACT = 1557
Z3_OP_SEQ_INDEX = 1562
Z3_OP_SEQ_IN_RE = 1565
Z3_OP_SEQ_LAST_INDEX = 1563
Z3_OP_SEQ_LENGTH = 1561
Z3_OP_SEQ_NTH = 1560
Z3_OP_SEQ_PREFIX = 1554
Z3_OP_SEQ_REPLACE = 1558
Z3_OP_SEQ_SUFFIX = 1555
Z3_OP_SEQ_TO_RE = 1564
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 = 1569
Z3_OP_STRING_LT = 1568
Z3_OP_STR_TO_INT = 1566
Z3_OP_SUB = 519
Z3_OP_TO_INT = 527
Z3_OP_TO_REAL = 526
Z3_OP_TRUE = 256
Z3_OP_UGEQ = 1043
Z3_OP_UGT = 1047
Z3_OP_ULEQ = 1041
Z3_OP_ULT = 1045
Z3_OP_UMINUS = 520
Z3_OP_UNINTERPRETED = 45101
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_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/system/bin', '/home/linuxbrew/.linuxbrew/bin', '/home/linuxbrew/.linuxbrew/sbin', '/home/vsts/.local/bin', '/opt/pipx_bin', '/usr/share/rust/.cargo/bin', '/home/vsts/.config/composer/vendor/bin', '/usr/local/.ghcup/bin', '/home/vsts/.dotnet/tools', '/snap/bin', '/usr/local/sbin', '/usr/local/bin', '/usr/sbin', '/usr/bin', '/sbin', '/bin', '/usr/games', '/usr/local/games', '/snap/bin']
lp = '/home/vsts/.opam/system/bin:/home/linuxbrew/.lin...:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin'
memmove = <CFunctionType object>
memset = <CFunctionType object>
pydll = <ctypes.LibraryLoader object>
pythonapi = <PyDLL 'None', handle 7f0c212f5170 at 7f0c1f47a9d0>
sat = sat
unknown = unknown
unsat = unsat
v = 'PYTHONPATH'