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

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

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 get_errno(...) 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 subresultants(p, q, x) Return the non-constant subresultants of 'p' and 'q' with respect to the "variable" 'x'.   'p', 'q' and 'x' are Z3 expressions where 'p' and 'q' are arithmetic terms. Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable. Example: f(a) is a considered to be a variable b in the polynomial   f(a)*f(a) + 2*f(a) + 1   >>> x, y = Reals('x y') >>> subresultants(2*x + y, 3*x - 2*y + 2, x) [-7*y + 4] >>> r = subresultants(3*y*x**2 + y**3 + 1, 2*x**3 + y + 3, x) >>> r[0] 4*y**9 + 12*y**6 + 27*y**5 + 162*y**4 + 255*y**3 + 4 >>> r[1] -6*y**4 + -6*y

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_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> sat = sat unknown = unknown unsat = unsat v = 'PYTHONPATH'