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

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

Classes
		builtins.object Numeral   class Numeral(builtins.object)     Numeral(num, ctx=None)   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) Initialize self.  See help(type(self)) for accurate signature. __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) Return 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) Return 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 Data descriptors defined here: __dict__ dictionary for instance variables (if defined) __weakref__ list of weak references to the object (if defined) Data and other attributes defined here: __hash__ = None

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_errno(...) sizeof(...) sizeof(C type) -> integer sizeof(C instance) -> integer Return the size in bytes of a C instance

Data
		DEFAULT_MODE = 0 Iterable = typing.Iterable 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_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_CHAR_CONST = 1594 Z3_OP_CHAR_FROM_BV = 1598 Z3_OP_CHAR_IS_DIGIT = 1599 Z3_OP_CHAR_LE = 1595 Z3_OP_CHAR_TO_BV = 1597 Z3_OP_CHAR_TO_INT = 1596 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 = 1570 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 = 1587 Z3_OP_RE_CONCAT = 1580 Z3_OP_RE_DERIVATIVE = 1593 Z3_OP_RE_DIFF = 1583 Z3_OP_RE_EMPTY_SET = 1588 Z3_OP_RE_FULL_CHAR_SET = 1590 Z3_OP_RE_FULL_SET = 1589 Z3_OP_RE_INTERSECT = 1584 Z3_OP_RE_LOOP = 1585 Z3_OP_RE_OF_PRED = 1591 Z3_OP_RE_OPTION = 1579 Z3_OP_RE_PLUS = 1577 Z3_OP_RE_POWER = 1586 Z3_OP_RE_RANGE = 1582 Z3_OP_RE_REVERSE = 1592 Z3_OP_RE_STAR = 1578 Z3_OP_RE_UNION = 1581 Z3_OP_ROTATE_LEFT = 1067 Z3_OP_ROTATE_RIGHT = 1068 Z3_OP_SBV_TO_STR = 1572 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_INDEX = 1565 Z3_OP_SEQ_IN_RE = 1568 Z3_OP_SEQ_LAST_INDEX = 1566 Z3_OP_SEQ_LENGTH = 1564 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 = 1576 Z3_OP_STRING_LT = 1575 Z3_OP_STR_FROM_CODE = 1574 Z3_OP_STR_TO_CODE = 1573 Z3_OP_STR_TO_INT = 1569 Z3_OP_SUB = 519 Z3_OP_TO_INT = 527 Z3_OP_TO_REAL = 526 Z3_OP_TRUE = 256 Z3_OP_UBV_TO_STR = 1571 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_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', '/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', '/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/default/bin:/home/vsts/.local/b...:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin' memmove = <CFunctionType object> memset = <CFunctionType object> pydll = <ctypes.LibraryLoader object> pythonapi = <PyDLL 'None', handle 7f287e6662e0> sat = sat unknown = unknown unsat = unsat v = 'PYTHONPATH'