| @@ -0,0 +1,314 @@ | ||
| # Automatically generated file | ||
|
|
||
| # enum Z3_lbool | ||
| Z3_L_FALSE = -1 | ||
| Z3_L_UNDEF = 0 | ||
| Z3_L_TRUE = 1 | ||
|
|
||
| # enum Z3_symbol_kind | ||
| Z3_INT_SYMBOL = 0 | ||
| Z3_STRING_SYMBOL = 1 | ||
|
|
||
| # enum Z3_parameter_kind | ||
| Z3_PARAMETER_INT = 0 | ||
| Z3_PARAMETER_DOUBLE = 1 | ||
| Z3_PARAMETER_RATIONAL = 2 | ||
| Z3_PARAMETER_SYMBOL = 3 | ||
| Z3_PARAMETER_SORT = 4 | ||
| Z3_PARAMETER_AST = 5 | ||
| Z3_PARAMETER_FUNC_DECL = 6 | ||
|
|
||
| # enum Z3_sort_kind | ||
| Z3_UNINTERPRETED_SORT = 0 | ||
| Z3_BOOL_SORT = 1 | ||
| Z3_INT_SORT = 2 | ||
| Z3_REAL_SORT = 3 | ||
| Z3_BV_SORT = 4 | ||
| Z3_ARRAY_SORT = 5 | ||
| Z3_DATATYPE_SORT = 6 | ||
| Z3_RELATION_SORT = 7 | ||
| Z3_FINITE_DOMAIN_SORT = 8 | ||
| Z3_FLOATING_POINT_SORT = 9 | ||
| Z3_ROUNDING_MODE_SORT = 10 | ||
| Z3_SEQ_SORT = 11 | ||
| Z3_RE_SORT = 12 | ||
| Z3_UNKNOWN_SORT = 1000 | ||
|
|
||
| # enum Z3_ast_kind | ||
| Z3_NUMERAL_AST = 0 | ||
| Z3_APP_AST = 1 | ||
| Z3_VAR_AST = 2 | ||
| Z3_QUANTIFIER_AST = 3 | ||
| Z3_SORT_AST = 4 | ||
| Z3_FUNC_DECL_AST = 5 | ||
| Z3_UNKNOWN_AST = 1000 | ||
|
|
||
| # enum Z3_decl_kind | ||
| Z3_OP_TRUE = 256 | ||
| Z3_OP_FALSE = 257 | ||
| Z3_OP_EQ = 258 | ||
| Z3_OP_DISTINCT = 259 | ||
| Z3_OP_ITE = 260 | ||
| Z3_OP_AND = 261 | ||
| Z3_OP_OR = 262 | ||
| Z3_OP_IFF = 263 | ||
| Z3_OP_XOR = 264 | ||
| Z3_OP_NOT = 265 | ||
| Z3_OP_IMPLIES = 266 | ||
| Z3_OP_OEQ = 267 | ||
| Z3_OP_INTERP = 268 | ||
| Z3_OP_ANUM = 512 | ||
| Z3_OP_AGNUM = 513 | ||
| Z3_OP_LE = 514 | ||
| Z3_OP_GE = 515 | ||
| Z3_OP_LT = 516 | ||
| Z3_OP_GT = 517 | ||
| Z3_OP_ADD = 518 | ||
| Z3_OP_SUB = 519 | ||
| Z3_OP_UMINUS = 520 | ||
| Z3_OP_MUL = 521 | ||
| Z3_OP_DIV = 522 | ||
| Z3_OP_IDIV = 523 | ||
| Z3_OP_REM = 524 | ||
| Z3_OP_MOD = 525 | ||
| Z3_OP_TO_REAL = 526 | ||
| Z3_OP_TO_INT = 527 | ||
| Z3_OP_IS_INT = 528 | ||
| Z3_OP_POWER = 529 | ||
| Z3_OP_STORE = 768 | ||
| Z3_OP_SELECT = 769 | ||
| Z3_OP_CONST_ARRAY = 770 | ||
| Z3_OP_ARRAY_MAP = 771 | ||
| Z3_OP_ARRAY_DEFAULT = 772 | ||
| Z3_OP_SET_UNION = 773 | ||
| Z3_OP_SET_INTERSECT = 774 | ||
| Z3_OP_SET_DIFFERENCE = 775 | ||
| Z3_OP_SET_COMPLEMENT = 776 | ||
| Z3_OP_SET_SUBSET = 777 | ||
| Z3_OP_AS_ARRAY = 778 | ||
| Z3_OP_ARRAY_EXT = 779 | ||
| Z3_OP_BNUM = 1024 | ||
| Z3_OP_BIT1 = 1025 | ||
| Z3_OP_BIT0 = 1026 | ||
| Z3_OP_BNEG = 1027 | ||
| Z3_OP_BADD = 1028 | ||
| Z3_OP_BSUB = 1029 | ||
| Z3_OP_BMUL = 1030 | ||
| Z3_OP_BSDIV = 1031 | ||
| Z3_OP_BUDIV = 1032 | ||
| Z3_OP_BSREM = 1033 | ||
| Z3_OP_BUREM = 1034 | ||
| Z3_OP_BSMOD = 1035 | ||
| Z3_OP_BSDIV0 = 1036 | ||
| Z3_OP_BUDIV0 = 1037 | ||
| Z3_OP_BSREM0 = 1038 | ||
| Z3_OP_BUREM0 = 1039 | ||
| Z3_OP_BSMOD0 = 1040 | ||
| Z3_OP_ULEQ = 1041 | ||
| Z3_OP_SLEQ = 1042 | ||
| Z3_OP_UGEQ = 1043 | ||
| Z3_OP_SGEQ = 1044 | ||
| Z3_OP_ULT = 1045 | ||
| Z3_OP_SLT = 1046 | ||
| Z3_OP_UGT = 1047 | ||
| Z3_OP_SGT = 1048 | ||
| Z3_OP_BAND = 1049 | ||
| Z3_OP_BOR = 1050 | ||
| Z3_OP_BNOT = 1051 | ||
| Z3_OP_BXOR = 1052 | ||
| Z3_OP_BNAND = 1053 | ||
| Z3_OP_BNOR = 1054 | ||
| Z3_OP_BXNOR = 1055 | ||
| Z3_OP_CONCAT = 1056 | ||
| Z3_OP_SIGN_EXT = 1057 | ||
| Z3_OP_ZERO_EXT = 1058 | ||
| Z3_OP_EXTRACT = 1059 | ||
| Z3_OP_REPEAT = 1060 | ||
| Z3_OP_BREDOR = 1061 | ||
| Z3_OP_BREDAND = 1062 | ||
| Z3_OP_BCOMP = 1063 | ||
| Z3_OP_BSHL = 1064 | ||
| Z3_OP_BLSHR = 1065 | ||
| Z3_OP_BASHR = 1066 | ||
| Z3_OP_ROTATE_LEFT = 1067 | ||
| Z3_OP_ROTATE_RIGHT = 1068 | ||
| Z3_OP_EXT_ROTATE_LEFT = 1069 | ||
| Z3_OP_EXT_ROTATE_RIGHT = 1070 | ||
| Z3_OP_INT2BV = 1071 | ||
| Z3_OP_BV2INT = 1072 | ||
| Z3_OP_CARRY = 1073 | ||
| Z3_OP_XOR3 = 1074 | ||
| Z3_OP_BSMUL_NO_OVFL = 1075 | ||
| Z3_OP_BUMUL_NO_OVFL = 1076 | ||
| Z3_OP_BSMUL_NO_UDFL = 1077 | ||
| Z3_OP_BSDIV_I = 1078 | ||
| Z3_OP_BUDIV_I = 1079 | ||
| Z3_OP_BSREM_I = 1080 | ||
| Z3_OP_BUREM_I = 1081 | ||
| Z3_OP_BSMOD_I = 1082 | ||
| Z3_OP_PR_UNDEF = 1280 | ||
| Z3_OP_PR_TRUE = 1281 | ||
| Z3_OP_PR_ASSERTED = 1282 | ||
| Z3_OP_PR_GOAL = 1283 | ||
| Z3_OP_PR_MODUS_PONENS = 1284 | ||
| Z3_OP_PR_REFLEXIVITY = 1285 | ||
| Z3_OP_PR_SYMMETRY = 1286 | ||
| Z3_OP_PR_TRANSITIVITY = 1287 | ||
| Z3_OP_PR_TRANSITIVITY_STAR = 1288 | ||
| Z3_OP_PR_MONOTONICITY = 1289 | ||
| Z3_OP_PR_QUANT_INTRO = 1290 | ||
| Z3_OP_PR_DISTRIBUTIVITY = 1291 | ||
| Z3_OP_PR_AND_ELIM = 1292 | ||
| Z3_OP_PR_NOT_OR_ELIM = 1293 | ||
| Z3_OP_PR_REWRITE = 1294 | ||
| Z3_OP_PR_REWRITE_STAR = 1295 | ||
| Z3_OP_PR_PULL_QUANT = 1296 | ||
| Z3_OP_PR_PULL_QUANT_STAR = 1297 | ||
| Z3_OP_PR_PUSH_QUANT = 1298 | ||
| Z3_OP_PR_ELIM_UNUSED_VARS = 1299 | ||
| Z3_OP_PR_DER = 1300 | ||
| Z3_OP_PR_QUANT_INST = 1301 | ||
| Z3_OP_PR_HYPOTHESIS = 1302 | ||
| Z3_OP_PR_LEMMA = 1303 | ||
| Z3_OP_PR_UNIT_RESOLUTION = 1304 | ||
| Z3_OP_PR_IFF_TRUE = 1305 | ||
| Z3_OP_PR_IFF_FALSE = 1306 | ||
| Z3_OP_PR_COMMUTATIVITY = 1307 | ||
| Z3_OP_PR_DEF_AXIOM = 1308 | ||
| Z3_OP_PR_DEF_INTRO = 1309 | ||
| Z3_OP_PR_APPLY_DEF = 1310 | ||
| Z3_OP_PR_IFF_OEQ = 1311 | ||
| Z3_OP_PR_NNF_POS = 1312 | ||
| Z3_OP_PR_NNF_NEG = 1313 | ||
| Z3_OP_PR_NNF_STAR = 1314 | ||
| Z3_OP_PR_CNF_STAR = 1315 | ||
| Z3_OP_PR_SKOLEMIZE = 1316 | ||
| Z3_OP_PR_MODUS_PONENS_OEQ = 1317 | ||
| Z3_OP_PR_TH_LEMMA = 1318 | ||
| Z3_OP_PR_HYPER_RESOLVE = 1319 | ||
| Z3_OP_RA_STORE = 1536 | ||
| Z3_OP_RA_EMPTY = 1537 | ||
| Z3_OP_RA_IS_EMPTY = 1538 | ||
| Z3_OP_RA_JOIN = 1539 | ||
| Z3_OP_RA_UNION = 1540 | ||
| Z3_OP_RA_WIDEN = 1541 | ||
| Z3_OP_RA_PROJECT = 1542 | ||
| Z3_OP_RA_FILTER = 1543 | ||
| Z3_OP_RA_NEGATION_FILTER = 1544 | ||
| Z3_OP_RA_RENAME = 1545 | ||
| Z3_OP_RA_COMPLEMENT = 1546 | ||
| Z3_OP_RA_SELECT = 1547 | ||
| Z3_OP_RA_CLONE = 1548 | ||
| Z3_OP_FD_CONSTANT = 1549 | ||
| Z3_OP_FD_LT = 1550 | ||
| Z3_OP_SEQ_UNIT = 1551 | ||
| Z3_OP_SEQ_EMPTY = 1552 | ||
| Z3_OP_SEQ_CONCAT = 1553 | ||
| Z3_OP_SEQ_PREFIX = 1554 | ||
| Z3_OP_SEQ_SUFFIX = 1555 | ||
| Z3_OP_SEQ_CONTAINS = 1556 | ||
| Z3_OP_SEQ_EXTRACT = 1557 | ||
| Z3_OP_SEQ_REPLACE = 1558 | ||
| Z3_OP_SEQ_AT = 1559 | ||
| Z3_OP_SEQ_LENGTH = 1560 | ||
| Z3_OP_SEQ_INDEX = 1561 | ||
| Z3_OP_SEQ_TO_RE = 1562 | ||
| Z3_OP_SEQ_IN_RE = 1563 | ||
| Z3_OP_RE_PLUS = 1564 | ||
| Z3_OP_RE_STAR = 1565 | ||
| Z3_OP_RE_OPTION = 1566 | ||
| Z3_OP_RE_CONCAT = 1567 | ||
| Z3_OP_RE_UNION = 1568 | ||
| Z3_OP_LABEL = 1792 | ||
| Z3_OP_LABEL_LIT = 1793 | ||
| Z3_OP_DT_CONSTRUCTOR = 2048 | ||
| Z3_OP_DT_RECOGNISER = 2049 | ||
| Z3_OP_DT_ACCESSOR = 2050 | ||
| Z3_OP_DT_UPDATE_FIELD = 2051 | ||
| Z3_OP_PB_AT_MOST = 2304 | ||
| Z3_OP_PB_LE = 2305 | ||
| Z3_OP_PB_GE = 2306 | ||
| Z3_OP_PB_EQ = 2307 | ||
| Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 2308 | ||
| Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 2309 | ||
| Z3_OP_FPA_RM_TOWARD_POSITIVE = 2310 | ||
| Z3_OP_FPA_RM_TOWARD_NEGATIVE = 2311 | ||
| Z3_OP_FPA_RM_TOWARD_ZERO = 2312 | ||
| Z3_OP_FPA_NUM = 2313 | ||
| Z3_OP_FPA_PLUS_INF = 2314 | ||
| Z3_OP_FPA_MINUS_INF = 2315 | ||
| Z3_OP_FPA_NAN = 2316 | ||
| Z3_OP_FPA_PLUS_ZERO = 2317 | ||
| Z3_OP_FPA_MINUS_ZERO = 2318 | ||
| Z3_OP_FPA_ADD = 2319 | ||
| Z3_OP_FPA_SUB = 2320 | ||
| Z3_OP_FPA_NEG = 2321 | ||
| Z3_OP_FPA_MUL = 2322 | ||
| Z3_OP_FPA_DIV = 2323 | ||
| Z3_OP_FPA_REM = 2324 | ||
| Z3_OP_FPA_ABS = 2325 | ||
| Z3_OP_FPA_MIN = 2326 | ||
| Z3_OP_FPA_MAX = 2327 | ||
| Z3_OP_FPA_FMA = 2328 | ||
| Z3_OP_FPA_SQRT = 2329 | ||
| Z3_OP_FPA_ROUND_TO_INTEGRAL = 2330 | ||
| Z3_OP_FPA_EQ = 2331 | ||
| Z3_OP_FPA_LT = 2332 | ||
| Z3_OP_FPA_GT = 2333 | ||
| Z3_OP_FPA_LE = 2334 | ||
| Z3_OP_FPA_GE = 2335 | ||
| Z3_OP_FPA_IS_NAN = 2336 | ||
| Z3_OP_FPA_IS_INF = 2337 | ||
| Z3_OP_FPA_IS_ZERO = 2338 | ||
| Z3_OP_FPA_IS_NORMAL = 2339 | ||
| Z3_OP_FPA_IS_SUBNORMAL = 2340 | ||
| Z3_OP_FPA_IS_NEGATIVE = 2341 | ||
| Z3_OP_FPA_IS_POSITIVE = 2342 | ||
| Z3_OP_FPA_FP = 2343 | ||
| Z3_OP_FPA_TO_FP = 2344 | ||
| Z3_OP_FPA_TO_FP_UNSIGNED = 2345 | ||
| Z3_OP_FPA_TO_UBV = 2346 | ||
| Z3_OP_FPA_TO_SBV = 2347 | ||
| Z3_OP_FPA_TO_REAL = 2348 | ||
| Z3_OP_FPA_TO_IEEE_BV = 2349 | ||
| Z3_OP_FPA_MIN_I = 2350 | ||
| Z3_OP_FPA_MAX_I = 2351 | ||
| Z3_OP_INTERNAL = 2352 | ||
| Z3_OP_UNINTERPRETED = 2353 | ||
|
|
||
| # enum Z3_param_kind | ||
| Z3_PK_UINT = 0 | ||
| Z3_PK_BOOL = 1 | ||
| Z3_PK_DOUBLE = 2 | ||
| Z3_PK_SYMBOL = 3 | ||
| Z3_PK_STRING = 4 | ||
| Z3_PK_OTHER = 5 | ||
| Z3_PK_INVALID = 6 | ||
|
|
||
| # enum Z3_ast_print_mode | ||
| Z3_PRINT_SMTLIB_FULL = 0 | ||
| Z3_PRINT_LOW_LEVEL = 1 | ||
| Z3_PRINT_SMTLIB_COMPLIANT = 2 | ||
| Z3_PRINT_SMTLIB2_COMPLIANT = 3 | ||
|
|
||
| # enum Z3_error_code | ||
| Z3_OK = 0 | ||
| Z3_SORT_ERROR = 1 | ||
| Z3_IOB = 2 | ||
| Z3_INVALID_ARG = 3 | ||
| Z3_PARSER_ERROR = 4 | ||
| Z3_NO_PARSER = 5 | ||
| Z3_INVALID_PATTERN = 6 | ||
| Z3_MEMOUT_FAIL = 7 | ||
| Z3_FILE_ACCESS_ERROR = 8 | ||
| Z3_INTERNAL_FATAL = 9 | ||
| Z3_INVALID_USAGE = 10 | ||
| Z3_DEC_REF_ERROR = 11 | ||
| Z3_EXCEPTION = 12 | ||
|
|
||
| # enum Z3_goal_prec | ||
| Z3_GOAL_PRECISE = 0 | ||
| Z3_GOAL_UNDER = 1 | ||
| Z3_GOAL_OVER = 2 | ||
| Z3_GOAL_UNDER_OVER = 3 | ||
|
|
| @@ -0,0 +1,35 @@ | ||
| ############################################ | ||
| # Copyright (c) 2012 Microsoft Corporation | ||
| # | ||
| # Z3 Python interface for Z3 polynomials | ||
| # | ||
| # Author: Leonardo de Moura (leonardo) | ||
| ############################################ | ||
|
|
||
| from .z3 import * | ||
|
|
||
| def 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 | ||
| """ | ||
| return AstVector(Z3_polynomial_subresultants(p.ctx_ref(), p.as_ast(), q.as_ast(), x.as_ast()), p.ctx) | ||
|
|
||
| if __name__ == "__main__": | ||
| import doctest | ||
| if doctest.testmod().failed: | ||
| exit(1) |
| @@ -0,0 +1,163 @@ | ||
| ############################################ | ||
| # Copyright (c) 2013 Microsoft Corporation | ||
| # | ||
| # Z3 Python interface for Z3 Real Closed Fields | ||
| # that may contain | ||
| # - computable transcendentals | ||
| # - infinitesimals | ||
| # - algebraic extensions | ||
| # | ||
| # Author: Leonardo de Moura (leonardo) | ||
| ############################################ | ||
| from .z3 import * | ||
| from .z3core import * | ||
| from .z3printer import * | ||
| from fractions import Fraction | ||
|
|
||
| def _to_rcfnum(num, ctx=None): | ||
| if isinstance(num, RCFNum): | ||
| return num | ||
| else: | ||
| return RCFNum(num, ctx) | ||
|
|
||
| def Pi(ctx=None): | ||
| ctx = z3._get_ctx(ctx) | ||
| return RCFNum(Z3_rcf_mk_pi(ctx.ref()), ctx) | ||
|
|
||
| def E(ctx=None): | ||
| ctx = z3._get_ctx(ctx) | ||
| return RCFNum(Z3_rcf_mk_e(ctx.ref()), ctx) | ||
|
|
||
| def MkInfinitesimal(name="eps", ctx=None): | ||
| # Todo: remove parameter name. | ||
| # For now, we keep it for backward compatibility. | ||
| ctx = z3._get_ctx(ctx) | ||
| return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref()), ctx) | ||
|
|
||
| def MkRoots(p, ctx=None): | ||
| ctx = z3._get_ctx(ctx) | ||
| num = len(p) | ||
| _tmp = [] | ||
| _as = (RCFNumObj * num)() | ||
| _rs = (RCFNumObj * num)() | ||
| for i in range(num): | ||
| _a = _to_rcfnum(p[i], ctx) | ||
| _tmp.append(_a) # prevent GC | ||
| _as[i] = _a.num | ||
| nr = Z3_rcf_mk_roots(ctx.ref(), num, _as, _rs) | ||
| r = [] | ||
| for i in range(nr): | ||
| r.append(RCFNum(_rs[i], ctx)) | ||
| return r | ||
|
|
||
| class RCFNum: | ||
| def __init__(self, num, ctx=None): | ||
| # TODO: add support for converting AST numeral values into RCFNum | ||
| if isinstance(num, RCFNumObj): | ||
| self.num = num | ||
| self.ctx = z3._get_ctx(ctx) | ||
| else: | ||
| self.ctx = z3._get_ctx(ctx) | ||
| self.num = Z3_rcf_mk_rational(self.ctx_ref(), str(num)) | ||
|
|
||
| def __del__(self): | ||
| Z3_rcf_del(self.ctx_ref(), self.num) | ||
|
|
||
| def ctx_ref(self): | ||
| return self.ctx.ref() | ||
|
|
||
| def __repr__(self): | ||
| return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False, in_html_mode()) | ||
|
|
||
| def compact_str(self): | ||
| return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True, in_html_mode()) | ||
|
|
||
| def __add__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_add(self.ctx_ref(), self.num, v.num), self.ctx) | ||
|
|
||
| def __radd__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_add(self.ctx_ref(), v.num, self.num), self.ctx) | ||
|
|
||
| def __mul__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_mul(self.ctx_ref(), self.num, v.num), self.ctx) | ||
|
|
||
| def __rmul__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_mul(self.ctx_ref(), v.num, self.num), self.ctx) | ||
|
|
||
| def __sub__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_sub(self.ctx_ref(), self.num, v.num), self.ctx) | ||
|
|
||
| def __rsub__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_sub(self.ctx_ref(), v.num, self.num), self.ctx) | ||
|
|
||
| def __div__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_div(self.ctx_ref(), self.num, v.num), self.ctx) | ||
|
|
||
| def __rdiv__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return RCFNum(Z3_rcf_div(self.ctx_ref(), v.num, self.num), self.ctx) | ||
|
|
||
| def __neg__(self): | ||
| return self.__rsub__(0) | ||
|
|
||
| def power(self, k): | ||
| return RCFNum(Z3_rcf_power(self.ctx_ref(), self.num, k), self.ctx) | ||
|
|
||
| def __pow__(self, k): | ||
| return self.power(k) | ||
|
|
||
| def decimal(self, prec=5): | ||
| return Z3_rcf_num_to_decimal_string(self.ctx_ref(), self.num, prec) | ||
|
|
||
| def __lt__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_lt(self.ctx_ref(), self.num, v.num) | ||
|
|
||
| def __rlt__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_lt(self.ctx_ref(), v.num, self.num) | ||
|
|
||
| def __gt__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_gt(self.ctx_ref(), self.num, v.num) | ||
|
|
||
| def __rgt__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_gt(self.ctx_ref(), v.num, self.num) | ||
|
|
||
| def __le__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_le(self.ctx_ref(), self.num, v.num) | ||
|
|
||
| def __rle__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_le(self.ctx_ref(), v.num, self.num) | ||
|
|
||
| def __ge__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_ge(self.ctx_ref(), self.num, v.num) | ||
|
|
||
| def __rge__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_ge(self.ctx_ref(), v.num, self.num) | ||
|
|
||
| def __eq__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_eq(self.ctx_ref(), self.num, v.num) | ||
|
|
||
| def __ne__(self, other): | ||
| v = _to_rcfnum(other, self.ctx) | ||
| return Z3_rcf_neq(self.ctx_ref(), self.num, v.num) | ||
|
|
||
| def split(self): | ||
| n = (RCFNumObj * 1)() | ||
| d = (RCFNumObj * 1)() | ||
| Z3_rcf_get_numerator_denominator(self.ctx_ref(), self.num, n, d) | ||
| return (RCFNum(n[0], self.ctx), RCFNum(d[0], self.ctx)) |
| @@ -0,0 +1,123 @@ | ||
| ############################################ | ||
| # Copyright (c) 2012 Microsoft Corporation | ||
| # | ||
| # Z3 Python interface | ||
| # | ||
| # Author: Leonardo de Moura (leonardo) | ||
| ############################################ | ||
|
|
||
| import ctypes | ||
|
|
||
| class Z3Exception(Exception): | ||
| def __init__(self, value): | ||
| self.value = value | ||
| def __str__(self): | ||
| return str(self.value) | ||
|
|
||
| class ContextObj(ctypes.c_void_p): | ||
| def __init__(self, context): self._as_parameter_ = context | ||
| def from_param(obj): return obj | ||
|
|
||
| class Config(ctypes.c_void_p): | ||
| def __init__(self, config): self._as_parameter_ = config | ||
| def from_param(obj): return obj | ||
|
|
||
| class Symbol(ctypes.c_void_p): | ||
| def __init__(self, symbol): self._as_parameter_ = symbol | ||
| def from_param(obj): return obj | ||
|
|
||
| class Sort(ctypes.c_void_p): | ||
| def __init__(self, sort): self._as_parameter_ = sort | ||
| def from_param(obj): return obj | ||
|
|
||
| class FuncDecl(ctypes.c_void_p): | ||
| def __init__(self, decl): self._as_parameter_ = decl | ||
| def from_param(obj): return obj | ||
|
|
||
| class Ast(ctypes.c_void_p): | ||
| def __init__(self, ast): self._as_parameter_ = ast | ||
| def from_param(obj): return obj | ||
|
|
||
| class Pattern(ctypes.c_void_p): | ||
| def __init__(self, pattern): self._as_parameter_ = pattern | ||
| def from_param(obj): return obj | ||
|
|
||
| class Model(ctypes.c_void_p): | ||
| def __init__(self, model): self._as_parameter_ = model | ||
| def from_param(obj): return obj | ||
|
|
||
| class Literals(ctypes.c_void_p): | ||
| def __init__(self, literals): self._as_parameter_ = literals | ||
| def from_param(obj): return obj | ||
|
|
||
| class Constructor(ctypes.c_void_p): | ||
| def __init__(self, constructor): self._as_parameter_ = constructor | ||
| def from_param(obj): return obj | ||
|
|
||
| class ConstructorList(ctypes.c_void_p): | ||
| def __init__(self, constructor_list): self._as_parameter_ = constructor_list | ||
| def from_param(obj): return obj | ||
|
|
||
| class GoalObj(ctypes.c_void_p): | ||
| def __init__(self, goal): self._as_parameter_ = goal | ||
| def from_param(obj): return obj | ||
|
|
||
| class TacticObj(ctypes.c_void_p): | ||
| def __init__(self, tactic): self._as_parameter_ = tactic | ||
| def from_param(obj): return obj | ||
|
|
||
| class ProbeObj(ctypes.c_void_p): | ||
| def __init__(self, probe): self._as_parameter_ = probe | ||
| def from_param(obj): return obj | ||
|
|
||
| class ApplyResultObj(ctypes.c_void_p): | ||
| def __init__(self, obj): self._as_parameter_ = obj | ||
| def from_param(obj): return obj | ||
|
|
||
| class StatsObj(ctypes.c_void_p): | ||
| def __init__(self, statistics): self._as_parameter_ = statistics | ||
| def from_param(obj): return obj | ||
|
|
||
| class SolverObj(ctypes.c_void_p): | ||
| def __init__(self, solver): self._as_parameter_ = solver | ||
| def from_param(obj): return obj | ||
|
|
||
| class FixedpointObj(ctypes.c_void_p): | ||
| def __init__(self, fixedpoint): self._as_parameter_ = fixedpoint | ||
| def from_param(obj): return obj | ||
|
|
||
| class OptimizeObj(ctypes.c_void_p): | ||
| def __init__(self, optimize): self._as_parameter_ = optimize | ||
| def from_param(obj): return obj | ||
|
|
||
| class ModelObj(ctypes.c_void_p): | ||
| def __init__(self, model): self._as_parameter_ = model | ||
| def from_param(obj): return obj | ||
|
|
||
| class AstVectorObj(ctypes.c_void_p): | ||
| def __init__(self, vector): self._as_parameter_ = vector | ||
| def from_param(obj): return obj | ||
|
|
||
| class AstMapObj(ctypes.c_void_p): | ||
| def __init__(self, ast_map): self._as_parameter_ = ast_map | ||
| def from_param(obj): return obj | ||
|
|
||
| class Params(ctypes.c_void_p): | ||
| def __init__(self, params): self._as_parameter_ = params | ||
| def from_param(obj): return obj | ||
|
|
||
| class ParamDescrs(ctypes.c_void_p): | ||
| def __init__(self, paramdescrs): self._as_parameter_ = paramdescrs | ||
| def from_param(obj): return obj | ||
|
|
||
| class FuncInterpObj(ctypes.c_void_p): | ||
| def __init__(self, f): self._as_parameter_ = f | ||
| def from_param(obj): return obj | ||
|
|
||
| class FuncEntryObj(ctypes.c_void_p): | ||
| def __init__(self, e): self._as_parameter_ = e | ||
| def from_param(obj): return obj | ||
|
|
||
| class RCFNumObj(ctypes.c_void_p): | ||
| def __init__(self, e): self._as_parameter_ = e | ||
| def from_param(obj): return obj |