Z3Py sources

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

python/z3consts.py

@@ -0,0 +1,240 @@
+# Automatically generated file, generator: mk_z3consts.py
+
+# enum Z3_lbool
+Z3_L_TRUE = 1
+Z3_L_UNDEF = 0
+Z3_L_FALSE = -1
+
+# enum Z3_symbol_kind
+Z3_INT_SYMBOL = 0
+Z3_STRING_SYMBOL = 1
+
+# enum Z3_parameter_kind
+Z3_PARAMETER_FUNC_DECL = 6
+Z3_PARAMETER_DOUBLE = 1
+Z3_PARAMETER_SYMBOL = 3
+Z3_PARAMETER_INT = 0
+Z3_PARAMETER_AST = 5
+Z3_PARAMETER_SORT = 4
+Z3_PARAMETER_RATIONAL = 2
+
+# enum Z3_sort_kind
+Z3_BV_SORT = 4
+Z3_FINITE_DOMAIN_SORT = 8
+Z3_ARRAY_SORT = 5
+Z3_UNKNOWN_SORT = 1000
+Z3_RELATION_SORT = 7
+Z3_REAL_SORT = 3
+Z3_INT_SORT = 2
+Z3_UNINTERPRETED_SORT = 0
+Z3_BOOL_SORT = 1
+Z3_DATATYPE_SORT = 6
+
+# enum Z3_ast_kind
+Z3_VAR_AST = 2
+Z3_SORT_AST = 4
+Z3_QUANTIFIER_AST = 3
+Z3_UNKNOWN_AST = 1000
+Z3_FUNC_DECL_AST = 5
+Z3_NUMERAL_AST = 0
+Z3_APP_AST = 1
+
+# enum Z3_decl_kind
+Z3_OP_LABEL = 1792
+Z3_OP_PR_REWRITE = 1294
+Z3_OP_UNINTERPRETED = 2051
+Z3_OP_SUB = 519
+Z3_OP_ZERO_EXT = 1058
+Z3_OP_ADD = 518
+Z3_OP_IS_INT = 528
+Z3_OP_BREDOR = 1061
+Z3_OP_BNOT = 1051
+Z3_OP_BNOR = 1054
+Z3_OP_PR_CNF_STAR = 1315
+Z3_OP_RA_JOIN = 1539
+Z3_OP_LE = 514
+Z3_OP_SET_UNION = 773
+Z3_OP_PR_UNDEF = 1280
+Z3_OP_BREDAND = 1062
+Z3_OP_LT = 516
+Z3_OP_RA_UNION = 1540
+Z3_OP_BADD = 1028
+Z3_OP_BUREM0 = 1039
+Z3_OP_OEQ = 267
+Z3_OP_PR_MODUS_PONENS = 1284
+Z3_OP_RA_CLONE = 1548
+Z3_OP_REPEAT = 1060
+Z3_OP_RA_NEGATION_FILTER = 1544
+Z3_OP_BSMOD0 = 1040
+Z3_OP_BLSHR = 1065
+Z3_OP_BASHR = 1066
+Z3_OP_PR_UNIT_RESOLUTION = 1304
+Z3_OP_ROTATE_RIGHT = 1068
+Z3_OP_ARRAY_DEFAULT = 772
+Z3_OP_PR_PULL_QUANT = 1296
+Z3_OP_PR_APPLY_DEF = 1310
+Z3_OP_PR_REWRITE_STAR = 1295
+Z3_OP_IDIV = 523
+Z3_OP_PR_GOAL = 1283
+Z3_OP_PR_IFF_TRUE = 1305
+Z3_OP_LABEL_LIT = 1793
+Z3_OP_BOR = 1050
+Z3_OP_PR_SYMMETRY = 1286
+Z3_OP_TRUE = 256
+Z3_OP_SET_COMPLEMENT = 776
+Z3_OP_CONCAT = 1056
+Z3_OP_PR_NOT_OR_ELIM = 1293
+Z3_OP_IFF = 263
+Z3_OP_BSHL = 1064
+Z3_OP_PR_TRANSITIVITY = 1287
+Z3_OP_SGT = 1048
+Z3_OP_RA_WIDEN = 1541
+Z3_OP_PR_DEF_INTRO = 1309
+Z3_OP_NOT = 265
+Z3_OP_PR_QUANT_INTRO = 1290
+Z3_OP_UGT = 1047
+Z3_OP_DT_RECOGNISER = 2049
+Z3_OP_SET_INTERSECT = 774
+Z3_OP_BSREM = 1033
+Z3_OP_RA_STORE = 1536
+Z3_OP_SLT = 1046
+Z3_OP_ROTATE_LEFT = 1067
+Z3_OP_PR_NNF_NEG = 1313
+Z3_OP_PR_REFLEXIVITY = 1285
+Z3_OP_ULEQ = 1041
+Z3_OP_BIT1 = 1025
+Z3_OP_BIT0 = 1026
+Z3_OP_EQ = 258
+Z3_OP_BMUL = 1030
+Z3_OP_ARRAY_MAP = 771
+Z3_OP_STORE = 768
+Z3_OP_PR_HYPOTHESIS = 1302
+Z3_OP_RA_RENAME = 1545
+Z3_OP_AND = 261
+Z3_OP_TO_REAL = 526
+Z3_OP_PR_NNF_POS = 1312
+Z3_OP_PR_AND_ELIM = 1292
+Z3_OP_MOD = 525
+Z3_OP_BUDIV0 = 1037
+Z3_OP_PR_TRUE = 1281
+Z3_OP_BNAND = 1053
+Z3_OP_PR_ELIM_UNUSED_VARS = 1299
+Z3_OP_RA_FILTER = 1543
+Z3_OP_FD_LT = 1549
+Z3_OP_RA_EMPTY = 1537
+Z3_OP_DIV = 522
+Z3_OP_ANUM = 512
+Z3_OP_MUL = 521
+Z3_OP_UGEQ = 1043
+Z3_OP_BSREM0 = 1038
+Z3_OP_PR_TH_LEMMA = 1318
+Z3_OP_BXOR = 1052
+Z3_OP_DISTINCT = 259
+Z3_OP_PR_IFF_FALSE = 1306
+Z3_OP_BV2INT = 1072
+Z3_OP_EXT_ROTATE_LEFT = 1069
+Z3_OP_PR_PULL_QUANT_STAR = 1297
+Z3_OP_BSUB = 1029
+Z3_OP_PR_ASSERTED = 1282
+Z3_OP_BXNOR = 1055
+Z3_OP_EXTRACT = 1059
+Z3_OP_PR_DER = 1300
+Z3_OP_DT_CONSTRUCTOR = 2048
+Z3_OP_GT = 517
+Z3_OP_BUREM = 1034
+Z3_OP_IMPLIES = 266
+Z3_OP_SLEQ = 1042
+Z3_OP_GE = 515
+Z3_OP_BAND = 1049
+Z3_OP_ITE = 260
+Z3_OP_AS_ARRAY = 778
+Z3_OP_RA_SELECT = 1547
+Z3_OP_CONST_ARRAY = 770
+Z3_OP_BSDIV = 1031
+Z3_OP_OR = 262
+Z3_OP_AGNUM = 513
+Z3_OP_PR_PUSH_QUANT = 1298
+Z3_OP_BSMOD = 1035
+Z3_OP_PR_IFF_OEQ = 1311
+Z3_OP_PR_LEMMA = 1303
+Z3_OP_SET_SUBSET = 777
+Z3_OP_SELECT = 769
+Z3_OP_RA_PROJECT = 1542
+Z3_OP_BNEG = 1027
+Z3_OP_UMINUS = 520
+Z3_OP_REM = 524
+Z3_OP_TO_INT = 527
+Z3_OP_PR_QUANT_INST = 1301
+Z3_OP_SGEQ = 1044
+Z3_OP_POWER = 529
+Z3_OP_XOR3 = 1074
+Z3_OP_RA_IS_EMPTY = 1538
+Z3_OP_CARRY = 1073
+Z3_OP_DT_ACCESSOR = 2050
+Z3_OP_PR_TRANSITIVITY_STAR = 1288
+Z3_OP_PR_NNF_STAR = 1314
+Z3_OP_PR_COMMUTATIVITY = 1307
+Z3_OP_ULT = 1045
+Z3_OP_BSDIV0 = 1036
+Z3_OP_SET_DIFFERENCE = 775
+Z3_OP_INT2BV = 1071
+Z3_OP_XOR = 264
+Z3_OP_PR_MODUS_PONENS_OEQ = 1317
+Z3_OP_BNUM = 1024
+Z3_OP_BUDIV = 1032
+Z3_OP_PR_MONOTONICITY = 1289
+Z3_OP_PR_DEF_AXIOM = 1308
+Z3_OP_FALSE = 257
+Z3_OP_EXT_ROTATE_RIGHT = 1070
+Z3_OP_PR_DISTRIBUTIVITY = 1291
+Z3_OP_SIGN_EXT = 1057
+Z3_OP_PR_SKOLEMIZE = 1316
+Z3_OP_BCOMP = 1063
+Z3_OP_RA_COMPLEMENT = 1546
+
+# enum Z3_param_kind
+Z3_PK_BOOL = 1
+Z3_PK_SYMBOL = 3
+Z3_PK_OTHER = 5
+Z3_PK_INVALID = 6
+Z3_PK_UINT = 0
+Z3_PK_STRING = 4
+Z3_PK_DOUBLE = 2
+
+# enum Z3_search_failure
+Z3_QUANTIFIERS = 7
+Z3_UNKNOWN = 1
+Z3_CANCELED = 4
+Z3_MEMOUT_WATERMARK = 3
+Z3_THEORY = 6
+Z3_NO_FAILURE = 0
+Z3_TIMEOUT = 2
+Z3_NUM_CONFLICTS = 5
+
+# enum Z3_ast_print_mode
+Z3_PRINT_SMTLIB2_COMPLIANT = 3
+Z3_PRINT_SMTLIB_COMPLIANT = 2
+Z3_PRINT_SMTLIB_FULL = 0
+Z3_PRINT_LOW_LEVEL = 1
+
+# enum Z3_error_code
+Z3_INVALID_PATTERN = 6
+Z3_MEMOUT_FAIL = 7
+Z3_NO_PARSER = 5
+Z3_OK = 0
+Z3_INVALID_ARG = 3
+Z3_EXCEPTION = 12
+Z3_IOB = 2
+Z3_INTERNAL_FATAL = 9
+Z3_INVALID_USAGE = 10
+Z3_FILE_ACCESS_ERROR = 8
+Z3_SORT_ERROR = 1
+Z3_PARSER_ERROR = 4
+Z3_DEC_REF_ERROR = 11
+
+# enum Z3_goal_prec
+Z3_GOAL_UNDER = 1
+Z3_GOAL_PRECISE = 0
+Z3_GOAL_UNDER_OVER = 3
+Z3_GOAL_OVER = 2
+

python/z3printer.py

@@ -0,0 +1,988 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+# 
+# Z3 Python interface
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+import sys, io, z3
+from z3consts import *
+from z3core import *
+
+##############################
+#
+# Configuration
+#
+##############################
+
+# Z3 operator names to Z3Py
+_z3_op_to_str = {
+    Z3_OP_TRUE : 'True', Z3_OP_FALSE : 'False', Z3_OP_EQ : '==', Z3_OP_DISTINCT : 'Distinct', 
+    Z3_OP_ITE : 'If', Z3_OP_AND : 'And', Z3_OP_OR : 'Or', Z3_OP_IFF : '==', Z3_OP_XOR : 'Xor',
+    Z3_OP_NOT : 'Not', Z3_OP_IMPLIES : 'Implies', Z3_OP_IDIV : '/', Z3_OP_MOD : '%',
+    Z3_OP_TO_REAL : 'ToReal', Z3_OP_TO_INT : 'ToInt', Z3_OP_POWER : '**', Z3_OP_IS_INT : 'IsInt', 
+    Z3_OP_BADD : '+', Z3_OP_BSUB : '-', Z3_OP_BMUL : '*', Z3_OP_BOR : '|', Z3_OP_BAND : '&',
+    Z3_OP_BNOT : '~', Z3_OP_BXOR : '^', Z3_OP_BNEG : '-', Z3_OP_BUDIV : 'UDiv', Z3_OP_BSDIV : '/', Z3_OP_BSMOD : '%',
+    Z3_OP_BSREM : 'SRem', Z3_OP_BUREM : 'URem', Z3_OP_EXT_ROTATE_LEFT : 'RotateLeft', Z3_OP_EXT_ROTATE_RIGHT : 'RotateRight',
+    Z3_OP_SLEQ : '<=', Z3_OP_SLT : '<', Z3_OP_SGEQ : '>=', Z3_OP_SGT : '>',
+    Z3_OP_ULEQ : 'ULE', Z3_OP_ULT : 'ULT', Z3_OP_UGEQ : 'UGE', Z3_OP_UGT : 'UGT',
+    Z3_OP_SIGN_EXT : 'SignExt', Z3_OP_ZERO_EXT : 'ZeroExt', Z3_OP_REPEAT : 'RepeatBitVec', 
+    Z3_OP_BASHR : '>>', Z3_OP_BSHL : '<<', Z3_OP_BLSHR : 'LShR', 
+    Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
+    Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', 
+    Z3_OP_CONST_ARRAY : 'K' 
+    }
+
+# List of infix operators
+_z3_infix = [ 
+    Z3_OP_EQ, Z3_OP_IFF, Z3_OP_ADD, Z3_OP_SUB, Z3_OP_MUL, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_POWER,
+    Z3_OP_LE, Z3_OP_LT, Z3_OP_GE, Z3_OP_GT, Z3_OP_BADD, Z3_OP_BSUB, Z3_OP_BMUL, Z3_OP_BSDIV, Z3_OP_BSMOD, Z3_OP_BOR, Z3_OP_BAND,
+    Z3_OP_BXOR, Z3_OP_BSDIV, Z3_OP_SLEQ, Z3_OP_SLT, Z3_OP_SGEQ, Z3_OP_SGT, Z3_OP_BASHR, Z3_OP_BSHL
+    ]
+
+_z3_unary = [ Z3_OP_UMINUS, Z3_OP_BNOT, Z3_OP_BNEG ]
+
+# Precedence
+_z3_precedence = {
+    Z3_OP_POWER : 0,
+    Z3_OP_UMINUS : 1, Z3_OP_BNEG : 1, Z3_OP_BNOT : 1,
+    Z3_OP_MUL : 2, Z3_OP_DIV : 2, Z3_OP_IDIV : 2, Z3_OP_MOD : 2, Z3_OP_BMUL : 2, Z3_OP_BSDIV : 2, Z3_OP_BSMOD : 2,
+    Z3_OP_ADD : 3, Z3_OP_SUB : 3, Z3_OP_BADD : 3, Z3_OP_BSUB : 3,
+    Z3_OP_BASHR : 4, Z3_OP_BSHL : 4,
+    Z3_OP_BAND : 5,
+    Z3_OP_BXOR : 6,
+    Z3_OP_BOR : 7,
+    Z3_OP_LE : 8, Z3_OP_LT : 8, Z3_OP_GE : 8, Z3_OP_GT : 8, Z3_OP_EQ : 8, Z3_OP_SLEQ : 8, Z3_OP_SLT : 8, Z3_OP_SGEQ : 8, Z3_OP_SGT : 8,
+    Z3_OP_IFF : 8
+    }
+
+def _is_assoc(k):
+    return k == Z3_OP_BOR or k == Z3_OP_BXOR or k == Z3_OP_BAND or k == Z3_OP_ADD or k == Z3_OP_BADD or k == Z3_OP_MUL or k == Z3_OP_BMUL
+
+def _is_left_assoc(k):
+    return _is_assoc(k) or k == Z3_OP_SUB or k == Z3_OP_BSUB
+
+def _is_html_assoc(k):
+    return k == Z3_OP_AND or k == Z3_OP_OR or k == Z3_OP_IFF or _is_assoc(k)
+
+def _is_html_left_assoc(k):
+    return _is_html_assoc(k) or k == Z3_OP_SUB or k == Z3_OP_BSUB
+
+def _is_add(k):
+    return k == Z3_OP_ADD or k == Z3_OP_BADD
+
+def _is_sub(k):
+    return k == Z3_OP_SUB or k == Z3_OP_BSUB
+
+_z3_infix_compact = [ Z3_OP_MUL, Z3_OP_BMUL, Z3_OP_POWER, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_BSDIV, Z3_OP_BSMOD ]
+
+_ellipses = '...'
+
+_html_ellipses = '&hellip;'
+# Overwrite some of the operators for HTML
+_z3_pre_html_op_to_str = { Z3_OP_EQ : '=', Z3_OP_IFF : '=', Z3_OP_NOT : '&not;',
+                           Z3_OP_AND : '&and;', Z3_OP_OR : '&or;', Z3_OP_IMPLIES : '&rArr;',
+                           Z3_OP_LT : '&lt;', Z3_OP_GT : '&gt;', Z3_OP_LE : '&le;', Z3_OP_GE : '&ge;', 
+                           Z3_OP_MUL : '&middot;', 
+                           Z3_OP_SLEQ : '&le;', Z3_OP_SLT : '&lt;', Z3_OP_SGEQ : '&ge;', Z3_OP_SGT : '&gt;',
+                           Z3_OP_ULEQ : '&le;<sub>u</sub>', Z3_OP_ULT : '&lt;<sub>u</sub>', 
+                           Z3_OP_UGEQ : '&ge;<sub>u</sub>', Z3_OP_UGT : '&gt;<sub>u</sub>',
+                           Z3_OP_BMUL : '&middot;',
+                           Z3_OP_BUDIV : '/<sub>u</sub>', Z3_OP_BUREM : '%<sub>u</sub>', 
+                           Z3_OP_BASHR : '&gt;&gt;', Z3_OP_BSHL : '&lt;&lt;',
+                           Z3_OP_BLSHR : '&gt;&gt;<sub>u</sub>'
+                           }
+
+# Extra operators that are infix/unary for HTML
+_z3_html_infix = [ Z3_OP_AND, Z3_OP_OR, Z3_OP_IMPLIES,
+                   Z3_OP_ULEQ, Z3_OP_ULT, Z3_OP_UGEQ, Z3_OP_UGT, Z3_OP_BUDIV, Z3_OP_BUREM, Z3_OP_BLSHR
+                   ]
+
+_z3_html_unary = [ Z3_OP_NOT ]
+
+# Extra Precedence for HTML
+_z3_pre_html_precedence = { Z3_OP_BUDIV : 2, Z3_OP_BUREM : 2,
+                            Z3_OP_BLSHR : 4,
+                            Z3_OP_ULEQ : 8, Z3_OP_ULT : 8, 
+                            Z3_OP_UGEQ : 8, Z3_OP_UGT : 8,
+                            Z3_OP_ULEQ : 8, Z3_OP_ULT : 8, 
+                            Z3_OP_UGEQ : 8, Z3_OP_UGT : 8,
+                            Z3_OP_NOT : 1,
+                            Z3_OP_AND : 10,
+                            Z3_OP_OR  : 11,
+                            Z3_OP_IMPLIES : 12 }
+
+##############################
+#
+# End of Configuration
+#
+##############################
+
+def _support_pp(a):
+    return isinstance(a, z3.Z3PPObject) or isinstance(a, list) or isinstance(a, tuple)
+
+_infix_map = {}
+_unary_map = {}
+_infix_compact_map = {}
+
+for _k in _z3_infix:
+    _infix_map[_k] = True
+for _k in _z3_unary:
+    _unary_map[_k] = True
+for _k in _z3_infix_compact:
+    _infix_compact_map[_k] = True
+
+def _is_infix(k):
+    global _infix_map
+    return _infix_map.get(k, False)
+
+def _is_infix_compact(k):
+    global _infix_compact_map
+    return _infix_compact_map.get(k, False)
+
+def _is_unary(k):
+    global _unary_map
+    return _unary_map.get(k, False)
+
+def _op_name(a):
+    if isinstance(a, z3.FuncDeclRef):
+        f = a
+    else:
+        f = a.decl()
+    k = f.kind()
+    n = _z3_op_to_str.get(k, None)
+    if n == None:
+        return f.name()
+    else:
+        return n
+
+def _get_precedence(k):
+    global _z3_precedence
+    return _z3_precedence.get(k, 100000)
+
+_z3_html_op_to_str = {}
+for _k, _v in _z3_op_to_str.iteritems():
+    _z3_html_op_to_str[_k] = _v
+for _k, _v in _z3_pre_html_op_to_str.iteritems():
+    _z3_html_op_to_str[_k] = _v
+
+_z3_html_precedence = {}
+for _k, _v in _z3_precedence.iteritems():
+    _z3_html_precedence[_k] = _v
+for _k, _v in _z3_pre_html_precedence.iteritems():
+    _z3_html_precedence[_k] = _v
+
+_html_infix_map = {}
+_html_unary_map = {}
+for _k in _z3_infix:
+    _html_infix_map[_k] = True
+for _k in _z3_html_infix:
+    _html_infix_map[_k] = True
+for _k in _z3_unary:
+    _html_unary_map[_k] = True
+for _k in _z3_html_unary:
+    _html_unary_map[_k] = True
+
+def _is_html_infix(k):
+    global _html_infix_map
+    return _html_infix_map.get(k, False)
+
+def _is_html_unary(k):
+    global _html_unary_map
+    return _html_unary_map.get(k, False)
+
+def _html_op_name(a):
+    global _z3_html_op_to_str
+    if isinstance(a, z3.FuncDeclRef):
+        f = a
+    else:
+        f = a.decl()
+    k = f.kind()
+    n = _z3_html_op_to_str.get(k, None)
+    if n == None:
+        sym = Z3_get_decl_name(f.ctx_ref(), f.ast)
+        if Z3_get_symbol_kind(f.ctx_ref(), sym) == Z3_INT_SYMBOL:
+            return "&#950;<sub>%s</sub>" % Z3_get_symbol_int(f.ctx_ref(), sym)
+        else:
+            # Sanitize the string
+            return f.name()
+    else:
+        return n
+
+def _get_html_precedence(k):
+    global _z3_html_predence
+    return _z3_html_precedence.get(k, 100000)
+
+class FormatObject:
+    def is_compose(self):
+        return False
+    def is_choice(self):
+        return False
+    def is_indent(self):
+        return False
+    def is_string(self):
+        return False
+    def is_linebreak(self):
+        return False
+    def is_nil(self):
+        return True
+    def children(self):
+        return []
+    def as_tuple(self):
+        return None
+    def space_upto_nl(self):
+        return (0, False)
+    def flat(self):
+        return self
+
+class NAryFormatObject(FormatObject):
+    def __init__(self, fs):
+        assert all(map(lambda a: isinstance(a, FormatObject), fs))
+        self.children = fs
+    def children(self):
+        return self.children
+
+class ComposeFormatObject(NAryFormatObject):
+    def is_compose(sef):
+        return True
+    def as_tuple(self):
+        return ('compose', map(lambda a: a.as_tuple(), self.children))
+    def space_upto_nl(self):
+        r = 0
+        for child in self.children:
+            s, nl = child.space_upto_nl()
+            r = r + s
+            if nl:
+                return (r, True)
+        return (r, False)
+    def flat(self):
+        return compose(map(lambda a: a.flat(), self.children))
+
+class ChoiceFormatObject(NAryFormatObject):
+    def is_choice(sef):
+        return True
+    def as_tuple(self):
+        return ('choice', map(lambda a: a.as_tuple(), self.children))
+    def space_upto_nl(self):
+        return self.children[0].space_upto_nl()
+    def flat(self):
+        return self.children[0].flat()
+
+class IndentFormatObject(FormatObject):
+    def __init__(self, indent, child):
+        assert isinstance(child, FormatObject)
+        self.indent = indent
+        self.child  = child
+    def children(self):
+        return [self.child]
+    def as_tuple(self):
+        return ('indent', self.indent, self.child.as_tuple())
+    def space_upto_nl(self):
+        return self.child.space_upto_nl()
+    def flat(self):
+        return indent(self.indent, self.child.flat())
+    def is_indent(self):
+        return True
+
+class LineBreakFormatObject(FormatObject):
+    def __init__(self):
+        self.space = ' '
+    def is_linebreak(self):
+        return True
+    def as_tuple(self):
+        return '<line-break>'
+    def space_upto_nl(self):
+        return (0, True)
+    def flat(self):
+        return to_format(self.space)
+
+class StringFormatObject(FormatObject):
+    def __init__(self, string):
+        assert isinstance(string, str)
+        self.string = string
+    def is_string(self):
+        return True
+    def as_tuple(self):
+        return self.string
+    def space_upto_nl(self):
+        return (getattr(self, 'size', len(self.string)), False)
+
+def fits(f, space_left):
+    s, nl = f.space_upto_nl()
+    return s <= space_left
+
+def to_format(arg, size=None):
+    if isinstance(arg, FormatObject):
+        return arg
+    else:
+        r = StringFormatObject(str(arg))
+        if size != None:
+            r.size = size
+        return r
+
+def compose(*args):
+    if len(args) == 1 and (isinstance(args[0], list) or isinstance(args[0], tuple)):
+        args = args[0]
+    return ComposeFormatObject(args)
+
+def indent(i, arg):
+    return IndentFormatObject(i, arg)
+
+def group(arg):
+    return ChoiceFormatObject([arg.flat(), arg])
+
+def line_break():
+    return LineBreakFormatObject()
+
+def _len(a):
+    if isinstance(a, StringFormatObject):
+        return getattr(a, 'size', len(a.string))
+    else:
+        return len(a)
+
+def seq(args, sep=',', space=True):
+    nl = line_break()
+    if not space:
+        nl.space = ''
+    r = []
+    r.append(args[0])
+    num  = len(args)
+    for i in range(num - 1):
+        r.append(to_format(sep))
+        r.append(nl)
+        r.append(args[i+1])
+    return compose(r)
+
+def seq1(header, args, lp='(', rp=')'):
+    return group(compose(to_format(header),
+                         to_format(lp),
+                         indent(len(lp) + _len(header),
+                                seq(args)),
+                         to_format(rp)))
+
+def seq2(header, args, i=4, lp='(', rp=')'):
+    if len(args) == 0:
+        return compose(to_format(header), to_format(lp), to_format(rp))
+    else:
+        return group(compose(indent(len(lp), compose(to_format(lp), to_format(header))),
+                             indent(i, compose(seq(args), to_format(rp)))))
+
+def seq3(args, lp='(', rp=')'):
+    if len(args) == 0:
+        return compose(to_format(lp), to_format(rp))
+    else:
+        return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp))))
+
+class StopPPException:
+    def __str__(self):
+        return 'pp-interrupted'
+
+class PP:
+    def __init__(self):
+        self.max_lines  = 200
+        self.max_width  = 60
+        self.bounded    = False
+        self.max_indent = 40
+        
+    def pp_string(self, f, indent):
+        if not self.bounded or self.pos <= self.max_width:
+            sz = _len(f)
+            if self.bounded and self.pos + sz > self.max_width:
+                self.out.write(_ellipses)
+            else:
+                self.pos = self.pos + sz
+                self.ribbon_pos = self.ribbon_pos + sz
+                self.out.write(unicode(f.string))
+
+    def pp_compose(self, f, indent):
+        for c in f.children:
+            self.pp(c, indent)
+
+    def pp_choice(self, f, indent):
+        space_left = self.max_width - self.pos
+        if space_left > 0 and fits(f.children[0], space_left):
+            self.pp(f.children[0], indent)
+        else:
+            self.pp(f.children[1], indent)
+    
+    def pp_line_break(self, f, indent):
+        self.pos = indent
+        self.ribbon_pos = 0
+        self.line = self.line + 1
+        if self.line < self.max_lines: 
+            self.out.write(unicode('\n'))
+            for i in range(indent):
+                self.out.write(unicode(' '))
+        else:
+            self.out.write(unicode('\n...'))
+            raise StopPPException()
+
+    def pp(self, f, indent):
+        if f.is_string():
+            self.pp_string(f, indent)
+        elif f.is_indent():
+            self.pp(f.child, min(indent + f.indent, self.max_indent))
+        elif f.is_compose():
+            self.pp_compose(f, indent)
+        elif f.is_choice():
+            self.pp_choice(f, indent)
+        elif f.is_linebreak():
+            self.pp_line_break(f, indent)
+        else:
+            return
+
+    def __call__(self, out, f):
+        try:
+            self.pos = 0
+            self.ribbon_pos = 0
+            self.line = 0
+            self.out  = out
+            self.pp(f, 0)
+        except StopPPException:
+            return
+    
+class Formatter:
+    def __init__(self):
+        global _ellipses
+        self.max_depth           = 20
+        self.max_args            = 128
+        self.rational_to_decimal = False
+        self.precision           = 10
+        self.ellipses            = to_format(_ellipses)
+        self.max_visited         = 10000
+    
+    def pp_ellipses(self):
+        return self.ellipses
+
+    def pp_arrow(self):
+        return ' ->'
+
+    def pp_unknown(self):
+        return '<unknown>'
+        
+    def pp_name(self, a):
+        return to_format(_op_name(a))
+
+    def is_infix(self, a):
+        return _is_infix(a)
+    
+    def is_unary(self, a):
+        return _is_unary(a)
+
+    def get_precedence(self, a):
+        return _get_precedence(a)
+
+    def is_infix_compact(self, a):
+        return _is_infix_compact(a)
+
+    def is_infix_unary(self, a):
+        return self.is_infix(a) or self.is_unary(a) 
+
+    def add_paren(self, a):
+        return compose(to_format('('), indent(1, a), to_format(')'))
+    
+    def pp_sort(self, s):
+        if isinstance(s, z3.ArraySortRef):
+            return seq1('Array', (self.pp_sort(s.domain()), self.pp_sort(s.range())))
+        elif isinstance(s, z3.BitVecSortRef):
+            return seq1('BitVec', (to_format(s.size()), ))
+        else:
+            return to_format(s.name())
+
+    def pp_const(self, a):
+        return self.pp_name(a)
+
+    def pp_int(self, a):
+        return to_format(a.as_string())
+        
+    def pp_rational(self, a):
+        if not self.rational_to_decimal:
+            return to_format(a.as_string())
+        else:
+            return to_format(a.as_decimal(self.precision))
+
+    def pp_algebraic(self, a):
+        return to_format(a.as_decimal(self.precision))
+
+    def pp_bv(self, a):
+        return to_format(a.as_string())
+
+    def pp_prefix(self, a, d, xs):
+        r  = []
+        sz = 0
+        for child in a.children(): 
+            r.append(self.pp_expr(child, d+1, xs))
+            sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                break
+        return seq1(self.pp_name(a), r)
+
+    def is_assoc(self, k):
+        return _is_assoc(k)
+
+    def is_left_assoc(self, k):
+        return _is_left_assoc(k)
+
+    def infix_args_core(self, a, d, xs, r):
+        sz = len(r)
+        k  = a.decl().kind()
+        p  = self.get_precedence(k)
+        first = True
+        for child in a.children():
+            child_pp = self.pp_expr(child, d+1, xs)
+            child_k = None
+            if z3.is_app(child):
+                child_k = child.decl().kind()
+            if k == child_k and (self.is_assoc(k) or (first and self.is_left_assoc(k))):
+                self.infix_args_core(child, d, xs, r)
+                sz = len(r)
+                if sz > self.max_args:
+                    return
+            elif self.is_infix_unary(child_k):
+                child_p = self.get_precedence(child_k)
+                if p > child_p or (_is_add(k) and _is_sub(child_k)) or (_is_sub(k) and first and _is_add(child_k)):
+                    r.append(child_pp)
+                else: 
+                    r.append(self.add_paren(child_pp))
+                sz = sz + 1
+            elif z3.is_quantifier(child):
+                r.append(self.add_paren(child_pp))
+            else:
+                r.append(child_pp)
+                sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                return
+            first = False
+
+    def infix_args(self, a, d, xs):
+        r = []
+        self.infix_args_core(a, d, xs, r)
+        return r
+
+    def pp_infix(self, a, d, xs):
+        k  = a.decl().kind()
+        if self.is_infix_compact(k):
+            op = self.pp_name(a)
+            return group(seq(self.infix_args(a, d, xs), op, False))
+        else:
+            op = self.pp_name(a)
+            sz = _len(op)
+            op.string = ' ' + op.string
+            op.size   = sz + 1
+            return group(seq(self.infix_args(a, d, xs), op))
+
+    def pp_unary(self, a, d, xs):
+        k  = a.decl().kind()
+        p  = self.get_precedence(k)
+        child    = a.children()[0]
+        child_k  = None
+        if z3.is_app(child):
+            child_k = child.decl().kind()
+        child_pp = self.pp_expr(child, d+1, xs)        
+        if k != child_k and self.is_infix_unary(child_k):
+            child_p = self.get_precedence(child_k)
+            if p <= child_p:
+                child_pp = self.add_paren(child_pp)
+        if z3.is_quantifier(child):
+            child_pp = self.add_paren(child_pp)
+        name = self.pp_name(a)
+        return compose(to_format(name), indent(_len(name), child_pp))
+
+    def pp_power_arg(self, arg, d, xs):
+        r = self.pp_expr(arg, d+1, xs)
+        k = None
+        if z3.is_app(arg):
+            k = arg.decl().kind()
+        if self.is_infix_unary(k) or (z3.is_rational_value(arg) and arg.denominator_as_long() != 1):
+            return self.add_paren(r)
+        else:
+            return r
+
+    def pp_power(self, a, d, xs):
+        arg1_pp = self.pp_power_arg(a.arg(0), d+1, xs)
+        arg2_pp = self.pp_power_arg(a.arg(1), d+1, xs)
+        return group(seq((arg1_pp, arg2_pp), '**', False))
+
+    def pp_neq(self):
+        return to_format("!=")
+
+    def pp_distinct(self, a, d, xs):
+        if a.num_args() == 2:
+            op = self.pp_neq()
+            sz = _len(op)
+            op.string = ' ' + op.string
+            op.size   = sz + 1
+            return group(seq(self.infix_args(a, d, xs), op))
+        else:
+            return self.pp_prefix(a, d, xs)
+
+    def pp_select(self, a, d, xs):
+        if a.num_args() != 2:
+            return self.pp_prefix(a, d, xs)
+        else:
+            arg1_pp = self.pp_expr(a.arg(0), d+1, xs)
+            arg2_pp = self.pp_expr(a.arg(1), d+1, xs)
+            return compose(arg1_pp, indent(2, compose(to_format('['), arg2_pp, to_format(']'))))
+
+    def pp_unary_param(self, a, d, xs):
+        p   = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+        arg = self.pp_expr(a.arg(0), d+1, xs)
+        return seq1(self.pp_name(a), [ to_format(p), arg ])
+
+    def pp_extract(self, a, d, xs):
+        h   = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+        l   = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1)
+        arg = self.pp_expr(a.arg(0), d+1, xs)
+        return seq1(self.pp_name(a), [ to_format(h), to_format(l), arg ])
+
+    def pp_pattern(self, a, d, xs):
+        if a.num_args() == 1:
+            return self.pp_expr(a.arg(0), d, xs)
+        else:
+            return seq1('MultiPattern', [ self.pp_expr(arg, d+1, xs) for arg in a.children() ])
+
+    def pp_map(self, a, d, xs):
+        r  = []
+        sz = 0
+        f  = z3.get_map_func(a)
+        r.append(to_format(f.name()))
+        for child in a.children(): 
+            r.append(self.pp_expr(child, d+1, xs))
+            sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                break
+        return seq1(self.pp_name(a), r)
+
+    def pp_K(self, a, d, xs):
+        return seq1(self.pp_name(a), [ self.pp_sort(a.domain()), self.pp_expr(a.arg(0), d+1, xs) ])
+
+    def pp_app(self, a, d, xs):
+        if z3.is_int_value(a):
+            return self.pp_int(a)
+        elif z3.is_rational_value(a):
+            return self.pp_rational(a)
+        elif z3.is_algebraic_value(a):
+            return self.pp_algebraic(a)
+        elif z3.is_bv_value(a):
+            return self.pp_bv(a)
+        elif z3.is_const(a):
+            return self.pp_const(a)
+        else:
+            f = a.decl()
+            k = f.kind()
+            if k == Z3_OP_POWER:
+                return self.pp_power(a, d, xs)
+            elif k == Z3_OP_DISTINCT:
+                return self.pp_distinct(a, d, xs)
+            elif k == Z3_OP_SELECT:
+                return self.pp_select(a, d, xs)
+            elif k == Z3_OP_SIGN_EXT or k == Z3_OP_ZERO_EXT or k == Z3_OP_REPEAT:
+                return self.pp_unary_param(a, d, xs)
+            elif k == Z3_OP_EXTRACT:
+                return self.pp_extract(a, d, xs)
+            elif k == Z3_OP_ARRAY_MAP:
+                return self.pp_map(a, d, xs)
+            elif k == Z3_OP_CONST_ARRAY:
+                return self.pp_K(a, d, xs)
+            elif z3.is_pattern(a):
+                return self.pp_pattern(a, d, xs)
+            elif self.is_infix(k):
+                return self.pp_infix(a, d, xs)
+            elif self.is_unary(k):
+                return self.pp_unary(a, d, xs)
+            else:
+                return self.pp_prefix(a, d, xs)
+
+    def pp_var(self, a, d, xs):
+        idx = z3.get_var_index(a)
+        sz  = len(xs)
+        if idx >= sz:
+            return seq1('Var', (to_format(idx),))
+        else:
+            return to_format(xs[sz - idx - 1])
+        
+    def pp_quantifier(self, a, d, xs):
+        ys = [ to_format(a.var_name(i)) for i in range(a.num_vars()) ]
+        new_xs  = xs + ys
+        body_pp = self.pp_expr(a.body(), d+1, new_xs)
+        if len(ys) == 1:
+            ys_pp = ys[0]
+        else:
+            ys_pp   = seq3(ys, '[', ']')
+        if a.is_forall():
+            header = 'ForAll'
+        else:
+            header = 'Exists'
+        return seq1(header, (ys_pp, body_pp))
+
+    def pp_expr(self, a, d, xs):
+        self.visited = self.visited + 1
+        if d > self.max_depth or self.visited > self.max_visited:
+            return self.pp_ellipses()
+        if z3.is_app(a):
+            return self.pp_app(a, d, xs)
+        elif z3.is_quantifier(a):
+            return self.pp_quantifier(a, d, xs)
+        elif z3.is_var(a):
+            return self.pp_var(a, d, xs)
+        else:
+            return to_format(self.pp_unknown())
+
+    def pp_seq_core(self, f, a, d, xs):
+        self.visited = self.visited + 1
+        if d > self.max_depth or self.visited > self.max_visited:
+            return self.pp_ellipses()
+        r = []
+        sz = 0
+        for elem in a:
+            r.append(f(elem, d+1, xs))
+            sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                break
+        return seq3(r, '[', ']')
+        
+    def pp_seq(self, a, d, xs):
+        return self.pp_seq_core(self.pp_expr, a, d, xs)
+
+    def pp_seq_seq(self, a, d, xs):
+        return self.pp_seq_core(self.pp_seq, a, d, xs)
+
+    def pp_model(self, m):
+        r = []
+        sz = 0
+        for d in m:
+            i = m[d]
+            if isinstance(i, z3.FuncInterp):
+                i_pp = self.pp_func_interp(i)
+            else:
+                i_pp = self.pp_expr(i, 0, [])
+            name = self.pp_name(d)
+            r.append(compose(name, to_format(' = '), indent(_len(name) + 3, i_pp)))
+            sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                break
+        return seq3(r, '[', ']')
+
+    def pp_func_entry(self, e):
+        num = e.num_args()
+        if num > 1:
+            args = []
+            for i in range(num):
+                args.append(self.pp_expr(e.arg_value(i), 0, []))
+            args_pp = group(seq3(args))
+        else:
+            args_pp   = self.pp_expr(e.arg_value(0), 0, [])
+        value_pp = self.pp_expr(e.value(), 0, []) 
+        return group(seq((args_pp, value_pp), self.pp_arrow()))
+
+    def pp_func_interp(self, f):
+        r = []
+        sz = 0
+        num = f.num_entries()
+        for i in range(num):
+            r.append(self.pp_func_entry(f.entry(i)))
+            sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                break
+        if sz <= self.max_args:
+            else_pp = self.pp_expr(f.else_value(), 0, [])
+            r.append(group(seq((to_format('else'), else_pp), self.pp_arrow())))
+        return seq3(r, '[', ']')
+
+    def pp_list(self, a):
+        r = []
+        sz = 0
+        for elem in a:
+            if _support_pp(elem):
+                r.append(self.main(elem))
+            else:
+                r.append(to_format(str(elem)))
+            sz = sz + 1
+            if sz > self.max_args:
+                r.append(self.pp_ellipses())
+                break
+        if isinstance(a, tuple):
+            return seq3(r)
+        else:
+            return seq3(r, '[', ']')
+
+    def main(self, a):
+        if z3.is_expr(a):
+            return self.pp_expr(a, 0, [])
+        elif z3.is_sort(a):
+            return self.pp_sort(a)
+        elif z3.is_func_decl(a):
+            return self.pp_name(a)
+        elif isinstance(a, z3.Goal) or isinstance(a, z3.AstVector):
+            return self.pp_seq(a, 0, [])
+        elif isinstance(a, z3.Solver):
+            return self.pp_seq(a.assertions(), 0, [])
+        elif isinstance(a, z3.Fixedpoint):
+            return a.sexpr()
+        elif isinstance(a, z3.ApplyResult):
+            return self.pp_seq_seq(a, 0, [])
+        elif isinstance(a, z3.ModelRef):
+            return self.pp_model(a)
+        elif isinstance(a, z3.FuncInterp):
+            return self.pp_func_interp(a)
+        elif isinstance(a, list) or isinstance(a, tuple):
+            return self.pp_list(a)
+        else:
+            return to_format(self.pp_unknown())
+
+    def __call__(self, a):
+        self.visited = 0
+        return self.main(a)
+
+class HTMLFormatter(Formatter):
+    def __init__(self):
+        Formatter.__init__(self)
+        global _html_ellipses
+        self.ellipses = to_format(_html_ellipses)
+
+    def pp_arrow(self):
+        return to_format(' &rarr;', 1)
+
+    def pp_unknown(self):
+        return '<b>unknown</b>'
+        
+    def pp_name(self, a):
+        r = _html_op_name(a)
+        if r[0] == '&' or r[0] == '/' or r[0] == '%':
+            return to_format(r, 1)
+        else:
+            pos = r.find('__')
+            if pos == -1 or pos == 0:
+                return to_format(r)
+            else:
+                sz = len(r)
+                if pos + 2 == sz:
+                    return to_format(r)
+                else:
+                    return to_format('%s<sub>%s</sub>' % (r[0:pos], r[pos+2:sz]), sz - 2)
+
+    def is_assoc(self, k):
+        return _is_html_assoc(k)
+
+    def is_left_assoc(self, k):
+        return _is_html_left_assoc(k)
+
+    def is_infix(self, a):
+        return _is_html_infix(a)
+    
+    def is_unary(self, a):
+        return _is_html_unary(a)
+
+    def get_precedence(self, a):
+        return _get_html_precedence(a)
+
+    def pp_neq(self):
+        return to_format("&ne;")
+
+    def pp_power(self, a, d, xs):
+        arg1_pp = self.pp_power_arg(a.arg(0), d+1, xs)
+        arg2_pp = self.pp_expr(a.arg(1), d+1, xs)
+        return compose(arg1_pp, to_format('<sup>', 1), arg2_pp, to_format('</sup>', 1)) 
+
+    def pp_var(self, a, d, xs):
+        idx = z3.get_var_index(a)
+        sz  = len(xs)
+        if idx >= sz:
+            # 957 is the greek letter nu
+            return to_format('&#957;<sub>%s</sub>' % idx, 1)
+        else:
+            return to_format(xs[sz - idx - 1])
+
+    def pp_quantifier(self, a, d, xs):
+        ys = [ to_format(a.var_name(i)) for i in range(a.num_vars()) ]
+        new_xs  = xs + ys
+        body_pp = self.pp_expr(a.body(), d+1, new_xs)
+        ys_pp = group(seq(ys))
+        if a.is_forall():
+            header = '&forall;'
+        else:
+            header = '&exist;'
+        return group(compose(to_format(header, 1), 
+                             indent(1, compose(ys_pp, to_format(' :'), line_break(), body_pp))))
+
+
+_PP        = PP()
+_Formatter = Formatter()
+
+def set_pp_option(k, v):
+    if k == 'html_mode':
+        if v:
+            set_html_mode(True)
+        else:
+            set_html_mode(False)
+        return True
+    val = getattr(_PP, k, None)
+    if val != None:
+        z3._z3_assert(type(v) == type(val), "Invalid pretty print option value")
+        setattr(_PP, k, v)
+        return True
+    val = getattr(_Formatter, k, None)
+    if val != None:
+        z3._z3_assert(type(v) == type(val), "Invalid pretty print option value")
+        setattr(_Formatter, k, v)
+        return True
+    return False
+
+def obj_to_string(a):
+    out = io.StringIO()
+    _PP(out, _Formatter(a))
+    return out.getvalue()
+
+_html_out = None
+
+def set_html_mode(flag=True):
+    global _Formatter
+    if flag:
+        _Formatter = HTMLFormatter()
+    else:
+        _Formatter = Formatter()
+
+def in_html_mode():
+    return isinstance(_Formatter, HTMLFormatter)
+
+def pp(a):
+    if _support_pp(a):
+        print obj_to_string(a)
+    else:
+        print a
+
+def print_matrix(m):
+    z3._z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected")
+    if not in_html_mode():
+        print obj_to_string(m)
+    else:
+        print '<table cellpadding="2", cellspacing="0", border="1">'
+        for r in m:
+            z3._z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected")
+            print '<tr>'
+            for c in r:
+                print '<td>%s</td>' % c
+            print '</tr>'
+        print '</table>'
+    
+def insert_line_breaks(s, width):
+    """Break s in lines of size width (approx)"""
+    sz = len(s)
+    if sz <= width:
+        return s
+    new_str = io.StringIO()
+    w = 0
+    for i in range(sz):
+        if w > width and s[i] == ' ':
+            new_str.write(u'<br />')
+            w = 0
+        else:
+            new_str.write(unicode(s[i]))
+        w = w + 1
+    return new_str.getvalue()

python/z3tactics.py

@@ -0,0 +1,356 @@
+# Automatically generated file, generator: mk_z3tactics.py
+import z3core
+import z3
+
+def simplify_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'simplify'), ctx)
+
+def split_clause_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'split-clause'), ctx)
+
+def normalize_bounds_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'normalize-bounds'), ctx)
+
+def elim_uncnstr_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'elim-uncnstr'), ctx)
+
+def elim_and_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'elim-and'), ctx)
+
+def add_bounds_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'add-bounds'), ctx)
+
+def aig_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'aig'), ctx)
+
+def skip_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'skip'), ctx)
+
+def fail_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fail'), ctx)
+
+def smt_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'smt'), ctx)
+
+def bit_blast_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'bit-blast'), ctx)
+
+def bv1_blast_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'bv1-blast'), ctx)
+
+def sat_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'sat'), ctx)
+
+def sat_preprocess_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'sat-preprocess'), ctx)
+
+def ctx_simplify_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'ctx-simplify'), ctx)
+
+def ctx_solver_simplify_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'ctx-solver-simplify'), ctx)
+
+def der_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'der'), ctx)
+
+def unit_subsume_simplify_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'unit-subsume-simplify'), ctx)
+
+def occf_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'occf'), ctx)
+
+def qe_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qe'), ctx)
+
+def qe_sat_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qe-sat'), ctx)
+
+def propagate_values_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'propagate-values'), ctx)
+
+def snf_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'snf'), ctx)
+
+def nnf_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'nnf'), ctx)
+
+def solve_eqs_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'solve-eqs'), ctx)
+
+def max_bv_sharing_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'max-bv-sharing'), ctx)
+
+def elim_term_ite_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'elim-term-ite'), ctx)
+
+def fix_dl_var_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fix-dl-var'), ctx)
+
+def tseitin_cnf_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'tseitin-cnf'), ctx)
+
+def tseitin_cnf_core_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'tseitin-cnf-core'), ctx)
+
+def degree_shift_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'degree-shift'), ctx)
+
+def purify_arith_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'purify-arith'), ctx)
+
+def nlsat_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'nlsat'), ctx)
+
+def factor_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'factor'), ctx)
+
+def fm_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fm'), ctx)
+
+def fail_if_undecided_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fail-if-undecided'), ctx)
+
+def diff_neq_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'diff-neq'), ctx)
+
+def lia2pb_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'lia2pb'), ctx)
+
+def fpa2bv_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fpa2bv'), ctx)
+
+def qffpa_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qffpa'), ctx)
+
+def pb2bv_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'pb2bv'), ctx)
+
+def recover_01_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'recover-01'), ctx)
+
+def symmetry_reduce_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'symmetry-reduce'), ctx)
+
+def distribute_forall_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'distribute-forall'), ctx)
+
+def reduce_args_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'reduce-args'), ctx)
+
+def reduce_bv_size_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'reduce-bv-size'), ctx)
+
+def propagate_ineqs_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'propagate-ineqs'), ctx)
+
+def cofactor_term_ite_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'cofactor-term-ite'), ctx)
+
+def mip_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'mip'), ctx)
+
+def nla2bv_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'nla2bv'), ctx)
+
+def vsubst_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'vsubst'), ctx)
+
+def qfbv_sls_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfbv-sls'), ctx)
+
+def qflia_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qflia'), ctx)
+
+def qflra_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qflra'), ctx)
+
+def qfnia_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfnia'), ctx)
+
+def qfnra_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfnra'), ctx)
+
+def qfbv_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfbv'), ctx)
+
+def subpaving_tactic(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'subpaving'), ctx)
+
+def memory_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'memory'), ctx)
+
+def depth_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'depth'), ctx)
+
+def size_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'size'), ctx)
+
+def num_exprs_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-exprs'), ctx)
+
+def num_consts_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-consts'), ctx)
+
+def num_bool_consts_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-bool-consts'), ctx)
+
+def num_arith_consts_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-arith-consts'), ctx)
+
+def num_bv_consts_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-bv-consts'), ctx)
+
+def produce_proofs_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-proofs'), ctx)
+
+def produce_model_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-model'), ctx)
+
+def produce_unsat_cores_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-unsat-cores'), ctx)
+
+def has_patterns_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'has-patterns'), ctx)
+
+def is_propositional_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-propositional'), ctx)
+
+def is_qfbv_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfbv'), ctx)
+
+def is_qfbv_eq_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfbv-eq'), ctx)
+
+def is_qflia_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qflia'), ctx)
+
+def is_qflra_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qflra'), ctx)
+
+def is_qflira_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qflira'), ctx)
+
+def is_ilp_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-ilp'), ctx)
+
+def is_mip_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-mip'), ctx)
+
+def is_unbounded_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-unbounded'), ctx)
+
+def is_pb_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-pb'), ctx)
+
+def arith_max_deg_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-max-deg'), ctx)
+
+def arith_avg_deg_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-avg-deg'), ctx)
+
+def arith_max_bw_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-max-bw'), ctx)
+
+def arith_avg_bw_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-avg-bw'), ctx)
+
+def is_qfnia_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfnia'), ctx)
+
+def is_qfnra_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfnra'), ctx)
+
+def is_nia_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-nia'), ctx)
+
+def is_nra_probe(ctx=None):
+  ctx = z3._get_ctx(ctx)
+  return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-nra'), ctx)
+

python/z3test.py

@@ -0,0 +1,9 @@
+import z3, doctest
+import sys, re
+
+if re.compile("64 bit").search(sys.version):
+    z3.init("..\\x64\\external_64\\z3.dll")
+else:
+    z3.init("..\\external\\z3.dll")
+    
+doctest.testmod(z3)

python/z3types.py

@@ -0,0 +1,107 @@
+import ctypes, z3core
+
+class Z3Exception(Exception):
+    def __init__(self, value):
+        self.value = value
+    def __str__(self):
+        return repr(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 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