Z3
doc/tmp/z3py.py
Go to the documentation of this file.
00001 ############################################
00002 # Copyright (c) 2012 Microsoft Corporation
00003 # 
00004 # Z3 Python interface
00005 #
00006 # Author: Leonardo de Moura (leonardo)
00007 ############################################
00008 
00009 """Z3 is a high performance theorem prover developed at Microsoft Research. Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems.
00010 
00011 Several online tutorials for Z3Py are available at:
00012 http://rise4fun.com/Z3Py/tutorial/guide
00013 
00014 Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable.
00015 
00016 Small example:
00017 
00018 >>> x = Int('x')
00019 >>> y = Int('y')
00020 >>> s = Solver()
00021 >>> s.add(x > 0)
00022 >>> s.add(x < 2)
00023 >>> s.add(y == x + 1)
00024 >>> s.check()
00025 sat
00026 >>> m = s.model()
00027 >>> m[x]
00028 1
00029 >>> m[y]
00030 2
00031 
00032 Z3 exceptions:
00033 
00034 >>> try:
00035 ...   x = Int('x')
00036 ...   y = Bool('y')
00037 ...   # the expression x + y is type incorrect
00038 ...   n = x + y
00039 ... except Z3Exception as ex:
00040 ...   print("failed: %s" % ex)
00041 failed: sort mismatch
00042 """
00043 from z3core import *
00044 from z3types import *
00045 from z3consts import *
00046 from z3printer import *
00047 from fractions import Fraction
00048 import sys
00049 import io
00050 
00051 if sys.version < '3':
00052     def _is_int(v):
00053         return isinstance(v, int) or isinstance(v, long)
00054 else:
00055     def _is_int(v):
00056         return isinstance(v, int)
00057 
00058 def enable_trace(msg):
00059     Z3_enable_trace(msg)
00060 
00061 def disable_trace(msg):
00062     Z3_disable_trace(msg)
00063 
00064 def get_version_string():
00065   major = ctypes.c_uint(0)
00066   minor = ctypes.c_uint(0)
00067   build = ctypes.c_uint(0)
00068   rev = ctypes.c_uint(0)
00069   Z3_get_version(major, minor, build, rev)
00070   return "%s.%s.%s" % (major.value, minor.value, build.value)
00071 
00072 def get_version():
00073   major = ctypes.c_uint(0)
00074   minor = ctypes.c_uint(0)
00075   build = ctypes.c_uint(0)
00076   rev = ctypes.c_uint(0)
00077   Z3_get_version(major, minor, build, rev)
00078   return (major.value, minor.value, build.value, rev.value)
00079 
00080 # We use _z3_assert instead of the assert command because we want to
00081 # produce nice error messages in Z3Py at rise4fun.com
00082 def _z3_assert(cond, msg):
00083     if not cond:
00084         raise Z3Exception(msg)
00085 
00086 def open_log(fname):
00087     """Log interaction to a file. This function must be invoked immediately after init(). """
00088     Z3_open_log(fname)
00089 
00090 def append_log(s):
00091     """Append user-defined string to interaction log. """
00092     Z3_append_log(s)
00093 
00094 def to_symbol(s, ctx=None):
00095     """Convert an integer or string into a Z3 symbol."""
00096     if isinstance(s, int):
00097         return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
00098     else:
00099         return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
00100 
00101 def _symbol2py(ctx, s):
00102     """Convert a Z3 symbol back into a Python object. """
00103     if Z3_get_symbol_kind(ctx.ref(), s) == Z3_INT_SYMBOL:
00104         return "k!%s" % Z3_get_symbol_int(ctx.ref(), s)
00105     else:
00106         return Z3_get_symbol_string(ctx.ref(), s)
00107 
00108 _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
00109 
00110 # Hack for having nary functions that can receive one argument that is the
00111 # list of arguments.
00112 def _get_args(args):
00113     try:
00114         if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
00115             return args[0]
00116         else:
00117             return args
00118     except:  # len is not necessarily defined when args is not a sequence (use reflection?)
00119         return args
00120 
00121 def _Z3python_error_handler_core(c, e):
00122     # Do nothing error handler, just avoid exit(0)
00123     # The wrappers in z3core.py will raise a Z3Exception if an error is detected
00124     return
00125     
00126 _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
00127 
00128 def _to_param_value(val):
00129     if isinstance(val, bool):
00130         if val == True:
00131             return "true"
00132         else:
00133             return "false"
00134     else:
00135         return str(val)
00136 
00137 class Context:
00138     """A Context manages all other Z3 objects, global configuration options, etc.
00139     
00140     Z3Py uses a default global context. For most applications this is sufficient.
00141     An application may use multiple Z3 contexts. Objects created in one context
00142     cannot be used in another one. However, several objects may be "translated" from
00143     one context to another. It is not safe to access Z3 objects from multiple threads.
00144     The only exception is the method `interrupt()` that can be used to interrupt() a long 
00145     computation.
00146     The initialization method receives global configuration options for the new context.
00147     """
00148     def __init__(self, *args, **kws):
00149         if __debug__:
00150             _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
00151         conf = Z3_mk_config()
00152         for key in kws:
00153             value = kws[key]
00154             Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
00155         prev = None
00156         for a in args:
00157             if prev == None:
00158                 prev = a
00159             else:
00160                 Z3_set_param_value(conf, str(prev), _to_param_value(a))
00161                 prev = None
00162         self.lib = lib()
00163         self.ctx = Z3_mk_context_rc(conf)
00164         Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
00165         lib().Z3_set_error_handler.restype  = None
00166         lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
00167         lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler)
00168         Z3_del_config(conf)
00169 
00170     def __del__(self):
00171         self.lib.Z3_del_context(self.ctx)
00172 
00173     def ref(self):
00174         """Return a reference to the actual C pointer to the Z3 context."""
00175         return self.ctx
00176 
00177     def interrupt(self):
00178         """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.  
00179 
00180         This method can be invoked from a thread different from the one executing the
00181         interruptable procedure.
00182         """
00183         Z3_interrupt(self.ref())
00184         
00185 
00186 # Global Z3 context
00187 _main_ctx = None
00188 def main_ctx():
00189     """Return a reference to the global Z3 context. 
00190     
00191     >>> x = Real('x')
00192     >>> x.ctx == main_ctx()
00193     True
00194     >>> c = Context()
00195     >>> c == main_ctx()
00196     False
00197     >>> x2 = Real('x', c)
00198     >>> x2.ctx == c
00199     True
00200     >>> eq(x, x2)
00201     False
00202     """
00203     global _main_ctx
00204     if _main_ctx == None:
00205         _main_ctx = Context()
00206     return _main_ctx    
00207 
00208 def _get_ctx(ctx):
00209     if ctx == None:
00210         return main_ctx()
00211     else:
00212         return ctx
00213 
00214 def set_param(*args, **kws):
00215     """Set Z3 global (or module) parameters.
00216 
00217     >>> set_param(precision=10)
00218     """
00219     if __debug__:
00220         _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
00221     new_kws = {}
00222     for k in kws:
00223         v = kws[k]
00224         if not set_pp_option(k, v):
00225             new_kws[k] = v
00226     for key in new_kws:
00227         value = new_kws[key]
00228         Z3_global_param_set(str(key).upper(), _to_param_value(value))
00229     prev = None
00230     for a in args:
00231         if prev == None:
00232             prev = a
00233         else:
00234             Z3_global_param_set(str(prev), _to_param_value(a))
00235             prev = None
00236 
00237 def reset_params():
00238     """Reset all global (or module) parameters.
00239     """
00240     Z3_global_param_reset_all()
00241 
00242 def set_option(*args, **kws):
00243     """Alias for 'set_param' for backward compatibility.
00244     """
00245     return set_param(*args, **kws)
00246 
00247 def get_param(name):
00248     """Return the value of a Z3 global (or module) parameter
00249 
00250     >>> get_param('nlsat.reorder')
00251     'true'
00252     """
00253     ptr = (ctypes.c_char_p * 1)()
00254     if Z3_global_param_get(str(name), ptr):
00255         r = z3core._to_pystr(ptr[0])
00256         return r
00257     raise Z3Exception("failed to retrieve value for '%s'" % name)
00258 
00259 #########################################
00260 #
00261 # ASTs base class
00262 #
00263 #########################################
00264 
00265 # Mark objects that use pretty printer
00266 class Z3PPObject:
00267     """Superclass for all Z3 objects that have support for pretty printing."""
00268     def use_pp(self):
00269         return True
00270 
00271 class AstRef(Z3PPObject):
00272     """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
00273     def __init__(self, ast, ctx=None):
00274         self.ast  = ast
00275         self.ctx  = _get_ctx(ctx)
00276         Z3_inc_ref(self.ctx.ref(), self.as_ast())
00277 
00278     def __del__(self):
00279         Z3_dec_ref(self.ctx.ref(), self.as_ast())
00280 
00281     def __str__(self):
00282         return obj_to_string(self)
00283 
00284     def __repr__(self):
00285         return obj_to_string(self)
00286 
00287     def sexpr(self):
00288         """Return an string representing the AST node in s-expression notation.
00289         
00290         >>> x = Int('x')
00291         >>> ((x + 1)*x).sexpr()
00292         '(* (+ x 1) x)'
00293         """
00294         return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
00295 
00296     def as_ast(self):
00297         """Return a pointer to the corresponding C Z3_ast object."""
00298         return self.ast
00299 
00300     def get_id(self):
00301         """Return unique identifier for object. It can be used for hash-tables and maps."""
00302         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00303 
00304 
00305     def ctx_ref(self):
00306         """Return a reference to the C context where this AST node is stored."""
00307         return self.ctx.ref()
00308         
00309     def eq(self, other):
00310         """Return `True` if `self` and `other` are structurally identical.
00311         
00312         >>> x = Int('x')
00313         >>> n1 = x + 1
00314         >>> n2 = 1 + x
00315         >>> n1.eq(n2)
00316         False
00317         >>> n1 = simplify(n1)
00318         >>> n2 = simplify(n2)
00319         >>> n1.eq(n2)
00320         True
00321         """
00322         if __debug__:
00323             _z3_assert(is_ast(other), "Z3 AST expected")
00324         return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
00325     
00326     def translate(self, target):
00327         """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 
00328         
00329         >>> c1 = Context()
00330         >>> c2 = Context()
00331         >>> x  = Int('x', c1)
00332         >>> y  = Int('y', c2)
00333         >>> # Nodes in different contexts can't be mixed.
00334         >>> # However, we can translate nodes from one context to another.
00335         >>> x.translate(c2) + y
00336         x + y
00337         """
00338         if __debug__:
00339             _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
00340         return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
00341 
00342     def hash(self):
00343         """Return a hashcode for the `self`.
00344         
00345         >>> n1 = simplify(Int('x') + 1)
00346         >>> n2 = simplify(2 + Int('x') - 1)
00347         >>> n1.hash() == n2.hash()
00348         True
00349         """
00350         return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
00351 
00352 def is_ast(a):
00353     """Return `True` if `a` is an AST node.
00354     
00355     >>> is_ast(10)
00356     False
00357     >>> is_ast(IntVal(10))
00358     True
00359     >>> is_ast(Int('x'))
00360     True
00361     >>> is_ast(BoolSort())
00362     True
00363     >>> is_ast(Function('f', IntSort(), IntSort()))
00364     True
00365     >>> is_ast("x")
00366     False
00367     >>> is_ast(Solver())
00368     False
00369     """
00370     return isinstance(a, AstRef)
00371 
00372 def eq(a, b):
00373     """Return `True` if `a` and `b` are structurally identical AST nodes.
00374     
00375     >>> x = Int('x')
00376     >>> y = Int('y')
00377     >>> eq(x, y)
00378     False
00379     >>> eq(x + 1, x + 1)
00380     True
00381     >>> eq(x + 1, 1 + x)
00382     False
00383     >>> eq(simplify(x + 1), simplify(1 + x))
00384     True
00385     """
00386     if __debug__:
00387         _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
00388     return a.eq(b)
00389 
00390 def _ast_kind(ctx, a):
00391     if is_ast(a):
00392         a = a.as_ast()
00393     return Z3_get_ast_kind(ctx.ref(), a)
00394 
00395 def _ctx_from_ast_arg_list(args, default_ctx=None):
00396     ctx = None
00397     for a in args:
00398         if is_ast(a) or is_probe(a):
00399             if ctx == None:
00400                 ctx = a.ctx
00401             else:
00402                 if __debug__:
00403                     _z3_assert(ctx == a.ctx, "Context mismatch")
00404     if ctx == None:
00405         ctx = default_ctx
00406     return ctx
00407 
00408 def _ctx_from_ast_args(*args):
00409     return _ctx_from_ast_arg_list(args)
00410 
00411 def _to_func_decl_array(args):
00412     sz = len(args)
00413     _args = (FuncDecl * sz)()
00414     for i in range(sz):
00415         _args[i] = args[i].as_func_decl()
00416     return _args, sz
00417 
00418 def _to_ast_array(args):
00419     sz = len(args)
00420     _args = (Ast * sz)()
00421     for i in range(sz):
00422         _args[i] = args[i].as_ast()
00423     return _args, sz
00424 
00425 def _to_ref_array(ref, args):
00426     sz = len(args)
00427     _args = (ref * sz)()
00428     for i in range(sz):
00429         _args[i] = args[i].as_ast()
00430     return _args, sz
00431 
00432 def _to_ast_ref(a, ctx):
00433     k = _ast_kind(ctx, a)
00434     if k == Z3_SORT_AST:
00435         return _to_sort_ref(a, ctx)
00436     elif k == Z3_FUNC_DECL_AST:
00437         return _to_func_decl_ref(a, ctx)
00438     else:
00439         return _to_expr_ref(a, ctx)
00440 
00441 #########################################
00442 #
00443 # Sorts
00444 #
00445 #########################################
00446 
00447 def _sort_kind(ctx, s):
00448     return Z3_get_sort_kind(ctx.ref(), s)
00449 
00450 class SortRef(AstRef):
00451     """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
00452     def as_ast(self):
00453         return Z3_sort_to_ast(self.ctx_ref(), self.ast)
00454 
00455     def get_id(self):
00456         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00457 
00458 
00459     def kind(self):
00460         """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
00461         
00462         >>> b = BoolSort()
00463         >>> b.kind() == Z3_BOOL_SORT
00464         True
00465         >>> b.kind() == Z3_INT_SORT
00466         False
00467         >>> A = ArraySort(IntSort(), IntSort())
00468         >>> A.kind() == Z3_ARRAY_SORT
00469         True
00470         >>> A.kind() == Z3_INT_SORT
00471         False
00472         """
00473         return _sort_kind(self.ctx, self.ast)
00474 
00475     def subsort(self, other):
00476         """Return `True` if `self` is a subsort of `other`. 
00477         
00478         >>> IntSort().subsort(RealSort())
00479         True
00480         """
00481         return False
00482 
00483     def cast(self, val):
00484         """Try to cast `val` as an element of sort `self`. 
00485 
00486         This method is used in Z3Py to convert Python objects such as integers,
00487         floats, longs and strings into Z3 expressions.
00488 
00489         >>> x = Int('x')
00490         >>> RealSort().cast(x)
00491         ToReal(x)
00492         """ 
00493         if __debug__:
00494             _z3_assert(is_expr(val), "Z3 expression expected")
00495             _z3_assert(self.eq(val.sort()), "Sort mismatch")
00496         return val
00497 
00498     def name(self):
00499         """Return the name (string) of sort `self`.
00500         
00501         >>> BoolSort().name()
00502         'Bool'
00503         >>> ArraySort(IntSort(), IntSort()).name()
00504         'Array'
00505         """
00506         return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
00507 
00508     def __eq__(self, other):
00509         """Return `True` if `self` and `other` are the same Z3 sort.
00510         
00511         >>> p = Bool('p')
00512         >>> p.sort() == BoolSort()
00513         True
00514         >>> p.sort() == IntSort()
00515         False
00516         """
00517         if other == None:
00518             return False
00519         return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
00520 
00521     def __ne__(self, other):
00522         """Return `True` if `self` and `other` are not the same Z3 sort.
00523         
00524         >>> p = Bool('p')
00525         >>> p.sort() != BoolSort()
00526         False
00527         >>> p.sort() != IntSort()
00528         True
00529         """
00530         return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
00531 
00532 def is_sort(s):
00533     """Return `True` if `s` is a Z3 sort.
00534     
00535     >>> is_sort(IntSort())
00536     True
00537     >>> is_sort(Int('x'))
00538     False
00539     >>> is_expr(Int('x'))
00540     True
00541     """
00542     return isinstance(s, SortRef)
00543 
00544 def _to_sort_ref(s, ctx):
00545     if __debug__:
00546         _z3_assert(isinstance(s, Sort), "Z3 Sort expected")
00547     k = _sort_kind(ctx, s)
00548     if k == Z3_BOOL_SORT:
00549         return BoolSortRef(s, ctx)
00550     elif k == Z3_INT_SORT or k == Z3_REAL_SORT:
00551         return ArithSortRef(s, ctx)
00552     elif k == Z3_BV_SORT:
00553         return BitVecSortRef(s, ctx)
00554     elif k == Z3_ARRAY_SORT:
00555         return ArraySortRef(s, ctx)
00556     elif k == Z3_DATATYPE_SORT:
00557         return DatatypeSortRef(s, ctx)
00558     return SortRef(s, ctx)
00559 
00560 def _sort(ctx, a):
00561     return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
00562 
00563 def DeclareSort(name, ctx=None):
00564     """Create a new uninterpred sort named `name`.
00565 
00566     If `ctx=None`, then the new sort is declared in the global Z3Py context.
00567 
00568     >>> A = DeclareSort('A')
00569     >>> a = Const('a', A)
00570     >>> b = Const('b', A)
00571     >>> a.sort() == A
00572     True
00573     >>> b.sort() == A
00574     True
00575     >>> a == b
00576     a == b
00577     """
00578     ctx = _get_ctx(ctx)
00579     return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
00580 
00581 #########################################
00582 #
00583 # Function Declarations
00584 #
00585 #########################################
00586 
00587 class FuncDeclRef(AstRef):
00588     """Function declaration. Every constant and function have an associated declaration.
00589     
00590     The declaration assigns a name, a sort (i.e., type), and for function
00591     the sort (i.e., type) of each of its arguments. Note that, in Z3, 
00592     a constant is a function with 0 arguments.
00593     """
00594     def as_ast(self):
00595         return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
00596 
00597     def get_id(self):
00598         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00599 
00600     def as_func_decl(self):
00601         return self.ast
00602 
00603     def name(self):
00604         """Return the name of the function declaration `self`.
00605         
00606         >>> f = Function('f', IntSort(), IntSort())
00607         >>> f.name()
00608         'f'
00609         >>> isinstance(f.name(), str)
00610         True
00611         """
00612         return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
00613 
00614     def arity(self):
00615         """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
00616         
00617         >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00618         >>> f.arity()
00619         2
00620         """
00621         return int(Z3_get_arity(self.ctx_ref(), self.ast))
00622 
00623     def domain(self, i):
00624         """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
00625         
00626         >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00627         >>> f.domain(0)
00628         Int
00629         >>> f.domain(1)
00630         Real
00631         """
00632         if __debug__:
00633             _z3_assert(i < self.arity(), "Index out of bounds")
00634         return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
00635 
00636     def range(self):
00637         """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
00638         
00639         >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00640         >>> f.range()
00641         Bool
00642         """
00643         return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)
00644 
00645     def kind(self):
00646         """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
00647         
00648         >>> x = Int('x')
00649         >>> d = (x + 1).decl()
00650         >>> d.kind() == Z3_OP_ADD
00651         True
00652         >>> d.kind() == Z3_OP_MUL
00653         False
00654         """
00655         return Z3_get_decl_kind(self.ctx_ref(), self.ast)
00656 
00657     def __call__(self, *args):
00658         """Create a Z3 application expression using the function `self`, and the given arguments. 
00659 
00660         The arguments must be Z3 expressions. This method assumes that
00661         the sorts of the elements in `args` match the sorts of the
00662         domain. Limited coersion is supported.  For example, if
00663         args[0] is a Python integer, and the function expects a Z3
00664         integer, then the argument is automatically converted into a
00665         Z3 integer.
00666 
00667         >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00668         >>> x = Int('x')
00669         >>> y = Real('y')
00670         >>> f(x, y)
00671         f(x, y)
00672         >>> f(x, x)
00673         f(x, ToReal(x))
00674         """
00675         args = _get_args(args)
00676         num = len(args)
00677         if __debug__:
00678             _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self)
00679         _args = (Ast * num)()
00680         saved = []
00681         for i in range(num):
00682             # self.domain(i).cast(args[i]) may create a new Z3 expression,
00683             # then we must save in 'saved' to prevent it from being garbage collected.
00684             tmp      = self.domain(i).cast(args[i])
00685             saved.append(tmp)
00686             _args[i] = tmp.as_ast()
00687         return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
00688 
00689 def is_func_decl(a):
00690     """Return `True` if `a` is a Z3 function declaration.
00691     
00692     >>> f = Function('f', IntSort(), IntSort())
00693     >>> is_func_decl(f)
00694     True
00695     >>> x = Real('x')
00696     >>> is_func_decl(x)
00697     False
00698     """
00699     return isinstance(a, FuncDeclRef)
00700 
00701 def Function(name, *sig):
00702     """Create a new Z3 uninterpreted function with the given sorts. 
00703     
00704     >>> f = Function('f', IntSort(), IntSort())
00705     >>> f(f(0))
00706     f(f(0))
00707     """
00708     sig = _get_args(sig)
00709     if __debug__:
00710         _z3_assert(len(sig) > 0, "At least two arguments expected")
00711     arity = len(sig) - 1
00712     rng   = sig[arity]
00713     if __debug__:
00714         _z3_assert(is_sort(rng), "Z3 sort expected")
00715     dom   = (Sort * arity)()
00716     for i in range(arity):
00717         if __debug__:
00718             _z3_assert(is_sort(sig[i]), "Z3 sort expected")
00719         dom[i] = sig[i].ast
00720     ctx = rng.ctx
00721     return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
00722 
00723 def _to_func_decl_ref(a, ctx):
00724     return FuncDeclRef(a, ctx)
00725 
00726 #########################################
00727 #
00728 # Expressions
00729 #
00730 #########################################
00731 
00732 class ExprRef(AstRef):
00733     """Constraints, formulas and terms are expressions in Z3.
00734 
00735     Expressions are ASTs. Every expression has a sort.
00736     There are three main kinds of expressions: 
00737     function applications, quantifiers and bounded variables.
00738     A constant is a function application with 0 arguments.
00739     For quantifier free problems, all expressions are 
00740     function applications.
00741     """
00742     def as_ast(self):
00743         return self.ast
00744 
00745     def get_id(self):
00746         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00747 
00748     def sort(self):
00749         """Return the sort of expression `self`.
00750         
00751         >>> x = Int('x')
00752         >>> (x + 1).sort()
00753         Int
00754         >>> y = Real('y')
00755         >>> (x + y).sort()
00756         Real
00757         """
00758         return _sort(self.ctx, self.as_ast())
00759 
00760     def sort_kind(self):
00761         """Shorthand for `self.sort().kind()`.
00762         
00763         >>> a = Array('a', IntSort(), IntSort())
00764         >>> a.sort_kind() == Z3_ARRAY_SORT
00765         True
00766         >>> a.sort_kind() == Z3_INT_SORT
00767         False
00768         """
00769         return self.sort().kind()
00770 
00771     def __eq__(self, other):
00772         """Return a Z3 expression that represents the constraint `self == other`.
00773 
00774         If `other` is `None`, then this method simply returns `False`. 
00775 
00776         >>> a = Int('a')
00777         >>> b = Int('b')
00778         >>> a == b
00779         a == b
00780         >>> a == None
00781         False
00782         """
00783         if other == None:
00784             return False
00785         a, b = _coerce_exprs(self, other)
00786         return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
00787 
00788     def __ne__(self, other):
00789         """Return a Z3 expression that represents the constraint `self != other`.
00790         
00791         If `other` is `None`, then this method simply returns `True`. 
00792 
00793         >>> a = Int('a')
00794         >>> b = Int('b')
00795         >>> a != b
00796         a != b
00797         >>> a != None
00798         True
00799         """
00800         if other == None:
00801             return True
00802         a, b = _coerce_exprs(self, other)
00803         _args, sz = _to_ast_array((a, b))
00804         return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
00805 
00806     def decl(self):
00807         """Return the Z3 function declaration associated with a Z3 application.
00808         
00809         >>> f = Function('f', IntSort(), IntSort())
00810         >>> a = Int('a')
00811         >>> t = f(a)
00812         >>> eq(t.decl(), f)
00813         True
00814         >>> (a + 1).decl()
00815         +
00816         """
00817         if __debug__:
00818             _z3_assert(is_app(self), "Z3 application expected")
00819         return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
00820     
00821     def num_args(self):
00822         """Return the number of arguments of a Z3 application.
00823 
00824         >>> a = Int('a')
00825         >>> b = Int('b')
00826         >>> (a + b).num_args()
00827         2
00828         >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00829         >>> t = f(a, b, 0)
00830         >>> t.num_args()
00831         3
00832         """
00833         if __debug__:
00834             _z3_assert(is_app(self), "Z3 application expected")
00835         return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
00836 
00837     def arg(self, idx):
00838         """Return argument `idx` of the application `self`. 
00839 
00840         This method assumes that `self` is a function application with at least `idx+1` arguments.
00841 
00842         >>> a = Int('a')
00843         >>> b = Int('b')
00844         >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00845         >>> t = f(a, b, 0)
00846         >>> t.arg(0)
00847         a
00848         >>> t.arg(1)
00849         b
00850         >>> t.arg(2)
00851         0
00852         """
00853         if __debug__:
00854             _z3_assert(is_app(self), "Z3 application expected")
00855             _z3_assert(idx < self.num_args(), "Invalid argument index")
00856         return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
00857 
00858     def children(self):
00859         """Return a list containing the children of the given expression
00860 
00861         >>> a = Int('a')
00862         >>> b = Int('b')
00863         >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00864         >>> t = f(a, b, 0)
00865         >>> t.children()
00866         [a, b, 0]
00867         """
00868         if is_app(self):
00869             return [self.arg(i) for i in range(self.num_args())]
00870         else:
00871             return []
00872 
00873 def _to_expr_ref(a, ctx):
00874     if isinstance(a, Pattern):
00875         return PatternRef(a, ctx)
00876     ctx_ref = ctx.ref()
00877     k = Z3_get_ast_kind(ctx_ref, a) 
00878     if k == Z3_QUANTIFIER_AST:
00879         return QuantifierRef(a, ctx)
00880     sk = Z3_get_sort_kind(ctx_ref, Z3_get_sort(ctx_ref, a))
00881     if sk == Z3_BOOL_SORT:
00882         return BoolRef(a, ctx)
00883     if sk == Z3_INT_SORT:
00884         if k == Z3_NUMERAL_AST:
00885             return IntNumRef(a, ctx)
00886         return ArithRef(a, ctx)
00887     if sk == Z3_REAL_SORT:
00888         if k == Z3_NUMERAL_AST:
00889             return RatNumRef(a, ctx)
00890         if _is_algebraic(ctx, a):
00891             return AlgebraicNumRef(a, ctx)
00892         return ArithRef(a, ctx)
00893     if sk == Z3_BV_SORT:
00894         if k == Z3_NUMERAL_AST:
00895             return BitVecNumRef(a, ctx)
00896         else:
00897             return BitVecRef(a, ctx)
00898     if sk == Z3_ARRAY_SORT:
00899         return ArrayRef(a, ctx)
00900     if sk == Z3_DATATYPE_SORT:
00901         return DatatypeRef(a, ctx)
00902     return ExprRef(a, ctx)
00903 
00904 def _coerce_expr_merge(s, a):
00905     if is_expr(a):
00906         s1 = a.sort()
00907         if s == None:
00908             return s1
00909         if s1.eq(s):
00910             return s
00911         elif s.subsort(s1):
00912             return s1
00913         elif s1.subsort(s):
00914             return s
00915         else:
00916             if __debug__:
00917                 _z3_assert(s1.ctx == s.ctx, "context mismatch")
00918                 _z3_assert(False, "sort mismatch")
00919     else:
00920         return s
00921 
00922 def _coerce_exprs(a, b, ctx=None):
00923     if not is_expr(a) and not is_expr(b):
00924         a = _py2expr(a, ctx)
00925         b = _py2expr(b, ctx)
00926     s = None
00927     s = _coerce_expr_merge(s, a)
00928     s = _coerce_expr_merge(s, b)
00929     a = s.cast(a)
00930     b = s.cast(b)
00931     return (a, b)
00932     
00933 def _reduce(f, l, a):
00934     r = a
00935     for e in l:
00936         r = f(r, e)
00937     return r
00938 
00939 def _coerce_expr_list(alist, ctx=None):
00940     has_expr = False
00941     for a in alist:
00942         if is_expr(a):
00943             has_expr = True
00944             break
00945     if not has_expr:
00946         alist = [ _py2expr(a, ctx) for a in alist ]
00947     s = _reduce(_coerce_expr_merge, alist, None)
00948     return [ s.cast(a) for a in alist ]
00949 
00950 def is_expr(a):
00951     """Return `True` if `a` is a Z3 expression.
00952     
00953     >>> a = Int('a')
00954     >>> is_expr(a)
00955     True
00956     >>> is_expr(a + 1)
00957     True
00958     >>> is_expr(IntSort())
00959     False
00960     >>> is_expr(1)
00961     False
00962     >>> is_expr(IntVal(1))
00963     True
00964     >>> x = Int('x')
00965     >>> is_expr(ForAll(x, x >= 0))
00966     True
00967     """
00968     return isinstance(a, ExprRef)
00969 
00970 def is_app(a):
00971     """Return `True` if `a` is a Z3 function application. 
00972     
00973     Note that, constants are function applications with 0 arguments. 
00974 
00975     >>> a = Int('a')
00976     >>> is_app(a)
00977     True
00978     >>> is_app(a + 1)
00979     True
00980     >>> is_app(IntSort())
00981     False
00982     >>> is_app(1)
00983     False
00984     >>> is_app(IntVal(1))
00985     True
00986     >>> x = Int('x')
00987     >>> is_app(ForAll(x, x >= 0))
00988     False
00989     """
00990     if not isinstance(a, ExprRef):
00991         return False
00992     k = _ast_kind(a.ctx, a)
00993     return k == Z3_NUMERAL_AST or k == Z3_APP_AST
00994 
00995 def is_const(a):
00996     """Return `True` if `a` is Z3 constant/variable expression. 
00997     
00998     >>> a = Int('a')
00999     >>> is_const(a)
01000     True
01001     >>> is_const(a + 1)
01002     False
01003     >>> is_const(1)
01004     False
01005     >>> is_const(IntVal(1))
01006     True
01007     >>> x = Int('x')
01008     >>> is_const(ForAll(x, x >= 0))
01009     False
01010     """
01011     return is_app(a) and a.num_args() == 0
01012 
01013 def is_var(a):
01014     """Return `True` if `a` is variable. 
01015     
01016     Z3 uses de-Bruijn indices for representing bound variables in
01017     quantifiers.
01018 
01019     >>> x = Int('x')
01020     >>> is_var(x)
01021     False
01022     >>> is_const(x)
01023     True
01024     >>> f = Function('f', IntSort(), IntSort())
01025     >>> # Z3 replaces x with bound variables when ForAll is executed.
01026     >>> q = ForAll(x, f(x) == x)
01027     >>> b = q.body()
01028     >>> b
01029     f(Var(0)) == Var(0)
01030     >>> b.arg(1)
01031     Var(0)
01032     >>> is_var(b.arg(1))
01033     True
01034     """
01035     return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
01036 
01037 def get_var_index(a):
01038     """Return the de-Bruijn index of the Z3 bounded variable `a`.
01039     
01040     >>> x = Int('x')
01041     >>> y = Int('y')
01042     >>> is_var(x)
01043     False
01044     >>> is_const(x)
01045     True
01046     >>> f = Function('f', IntSort(), IntSort(), IntSort())
01047     >>> # Z3 replaces x and y with bound variables when ForAll is executed.
01048     >>> q = ForAll([x, y], f(x, y) == x + y)
01049     >>> q.body()
01050     f(Var(1), Var(0)) == Var(1) + Var(0)
01051     >>> b = q.body()
01052     >>> b.arg(0)
01053     f(Var(1), Var(0))
01054     >>> v1 = b.arg(0).arg(0)
01055     >>> v2 = b.arg(0).arg(1)
01056     >>> v1
01057     Var(1)
01058     >>> v2
01059     Var(0)
01060     >>> get_var_index(v1)
01061     1
01062     >>> get_var_index(v2)
01063     0
01064     """
01065     if __debug__:
01066         _z3_assert(is_var(a), "Z3 bound variable expected")
01067     return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
01068 
01069 def is_app_of(a, k):
01070     """Return `True` if `a` is an application of the given kind `k`. 
01071     
01072     >>> x = Int('x')
01073     >>> n = x + 1
01074     >>> is_app_of(n, Z3_OP_ADD)
01075     True
01076     >>> is_app_of(n, Z3_OP_MUL)
01077     False
01078     """
01079     return is_app(a) and a.decl().kind() == k
01080 
01081 def If(a, b, c, ctx=None):
01082     """Create a Z3 if-then-else expression. 
01083     
01084     >>> x = Int('x')
01085     >>> y = Int('y')
01086     >>> max = If(x > y, x, y)
01087     >>> max
01088     If(x > y, x, y)
01089     >>> simplify(max)
01090     If(x <= y, y, x)
01091     """
01092     if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
01093         return Cond(a, b, c, ctx)
01094     else:
01095         ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
01096         s = BoolSort(ctx)
01097         a = s.cast(a)
01098         b, c = _coerce_exprs(b, c, ctx)
01099         if __debug__:
01100             _z3_assert(a.ctx == b.ctx, "Context mismatch")
01101         return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
01102 
01103 def Distinct(*args):
01104     """Create a Z3 distinct expression. 
01105     
01106     >>> x = Int('x')
01107     >>> y = Int('y')
01108     >>> Distinct(x, y)
01109     x != y
01110     >>> z = Int('z')
01111     >>> Distinct(x, y, z)
01112     Distinct(x, y, z)
01113     >>> simplify(Distinct(x, y, z))
01114     Distinct(x, y, z)
01115     >>> simplify(Distinct(x, y, z), blast_distinct=True)
01116     And(Not(x == y), Not(x == z), Not(y == z))
01117     """
01118     args  = _get_args(args)
01119     ctx   = _ctx_from_ast_arg_list(args)
01120     if __debug__:
01121         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
01122     args  = _coerce_expr_list(args, ctx)
01123     _args, sz = _to_ast_array(args)
01124     return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
01125 
01126 def _mk_bin(f, a, b):
01127     args = (Ast * 2)()
01128     if __debug__:
01129         _z3_assert(a.ctx == b.ctx, "Context mismatch")
01130     args[0] = a.as_ast()
01131     args[1] = b.as_ast()
01132     return f(a.ctx.ref(), 2, args)
01133 
01134 def Const(name, sort):
01135     """Create a constant of the given sort.
01136 
01137     >>> Const('x', IntSort())
01138     x
01139     """
01140     if __debug__:
01141         _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
01142     ctx = sort.ctx
01143     return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
01144 
01145 def Consts(names, sort):
01146     """Create a several constants of the given sort. 
01147     
01148     `names` is a string containing the names of all constants to be created. 
01149     Blank spaces separate the names of different constants.
01150     
01151     >>> x, y, z = Consts('x y z', IntSort())
01152     >>> x + y + z
01153     x + y + z
01154     """
01155     if isinstance(names, str):
01156         names = names.split(" ")
01157     return [Const(name, sort) for name in names]
01158 
01159 def Var(idx, s):
01160     """Create a Z3 free variable. Free variables are used to create quantified formulas.
01161     
01162     >>> Var(0, IntSort())
01163     Var(0)
01164     >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
01165     False
01166     """
01167     if __debug__:
01168         _z3_assert(is_sort(s), "Z3 sort expected")
01169     return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
01170 
01171 def RealVar(idx, ctx=None):
01172     """
01173     Create a real free variable. Free variables are used to create quantified formulas.
01174     They are also used to create polynomials.
01175     
01176     >>> RealVar(0)
01177     Var(0)
01178     """
01179     return Var(idx, RealSort(ctx))
01180 
01181 def RealVarVector(n, ctx=None):
01182     """
01183     Create a list of Real free variables.
01184     The variables have ids: 0, 1, ..., n-1
01185     
01186     >>> x0, x1, x2, x3 = RealVarVector(4)
01187     >>> x2
01188     Var(2)
01189     """
01190     return [ RealVar(i, ctx) for i in range(n) ]
01191 
01192 #########################################
01193 #
01194 # Booleans
01195 #
01196 #########################################
01197 
01198 class BoolSortRef(SortRef):
01199     """Boolean sort."""
01200     def cast(self, val):
01201         """Try to cast `val` as a Boolean.
01202         
01203         >>> x = BoolSort().cast(True)
01204         >>> x
01205         True
01206         >>> is_expr(x)
01207         True
01208         >>> is_expr(True)
01209         False
01210         >>> x.sort()
01211         Bool
01212         """
01213         if isinstance(val, bool):
01214             return BoolVal(val, self.ctx)
01215         if __debug__:
01216             _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected")
01217             _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
01218         return val
01219 
01220 class BoolRef(ExprRef):
01221     """All Boolean expressions are instances of this class."""
01222     def sort(self):
01223         return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
01224 
01225 def is_bool(a):
01226     """Return `True` if `a` is a Z3 Boolean expression.
01227 
01228     >>> p = Bool('p')
01229     >>> is_bool(p)
01230     True
01231     >>> q = Bool('q')
01232     >>> is_bool(And(p, q))
01233     True
01234     >>> x = Real('x')
01235     >>> is_bool(x)
01236     False
01237     >>> is_bool(x == 0)
01238     True
01239     """
01240     return isinstance(a, BoolRef)
01241 
01242 def is_true(a):
01243     """Return `True` if `a` is the Z3 true expression.
01244     
01245     >>> p = Bool('p')
01246     >>> is_true(p)
01247     False
01248     >>> is_true(simplify(p == p))
01249     True
01250     >>> x = Real('x')
01251     >>> is_true(x == 0)
01252     False
01253     >>> # True is a Python Boolean expression
01254     >>> is_true(True)
01255     False
01256     """
01257     return is_app_of(a, Z3_OP_TRUE)
01258 
01259 def is_false(a):
01260     """Return `True` if `a` is the Z3 false expression.
01261 
01262     >>> p = Bool('p')
01263     >>> is_false(p)
01264     False
01265     >>> is_false(False)
01266     False
01267     >>> is_false(BoolVal(False))
01268     True
01269     """
01270     return is_app_of(a, Z3_OP_FALSE)
01271 
01272 def is_and(a):
01273     """Return `True` if `a` is a Z3 and expression.
01274     
01275     >>> p, q = Bools('p q')
01276     >>> is_and(And(p, q))
01277     True
01278     >>> is_and(Or(p, q))
01279     False
01280     """
01281     return is_app_of(a, Z3_OP_AND)
01282 
01283 def is_or(a):
01284     """Return `True` if `a` is a Z3 or expression.
01285 
01286     >>> p, q = Bools('p q')
01287     >>> is_or(Or(p, q))
01288     True
01289     >>> is_or(And(p, q))
01290     False
01291     """
01292     return is_app_of(a, Z3_OP_OR)
01293 
01294 def is_not(a):
01295     """Return `True` if `a` is a Z3 not expression.
01296     
01297     >>> p = Bool('p')
01298     >>> is_not(p)
01299     False
01300     >>> is_not(Not(p))
01301     True
01302     """
01303     return is_app_of(a, Z3_OP_NOT)
01304 
01305 def is_eq(a):
01306     """Return `True` if `a` is a Z3 equality expression.
01307     
01308     >>> x, y = Ints('x y')
01309     >>> is_eq(x == y)
01310     True
01311     """
01312     return is_app_of(a, Z3_OP_EQ)
01313 
01314 def is_distinct(a):
01315     """Return `True` if `a` is a Z3 distinct expression.
01316     
01317     >>> x, y, z = Ints('x y z')
01318     >>> is_distinct(x == y)
01319     False
01320     >>> is_distinct(Distinct(x, y, z))
01321     True
01322     """
01323     return is_app_of(a, Z3_OP_DISTINCT)
01324 
01325 def BoolSort(ctx=None):
01326     """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
01327     
01328     >>> BoolSort()
01329     Bool
01330     >>> p = Const('p', BoolSort())
01331     >>> is_bool(p)
01332     True
01333     >>> r = Function('r', IntSort(), IntSort(), BoolSort())
01334     >>> r(0, 1)
01335     r(0, 1)
01336     >>> is_bool(r(0, 1))
01337     True
01338     """
01339     ctx = _get_ctx(ctx)
01340     return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
01341 
01342 def BoolVal(val, ctx=None):
01343     """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
01344     
01345     >>> BoolVal(True)
01346     True
01347     >>> is_true(BoolVal(True))
01348     True
01349     >>> is_true(True)
01350     False
01351     >>> is_false(BoolVal(False))
01352     True
01353     """
01354     ctx = _get_ctx(ctx)
01355     if val == False:
01356         return BoolRef(Z3_mk_false(ctx.ref()), ctx)
01357     else:
01358         return BoolRef(Z3_mk_true(ctx.ref()), ctx)
01359 
01360 def Bool(name, ctx=None):
01361     """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
01362     
01363     >>> p = Bool('p')
01364     >>> q = Bool('q')
01365     >>> And(p, q)
01366     And(p, q)
01367     """
01368     ctx = _get_ctx(ctx)
01369     return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
01370 
01371 def Bools(names, ctx=None):
01372     """Return a tuple of Boolean constants. 
01373     
01374     `names` is a single string containing all names separated by blank spaces. 
01375     If `ctx=None`, then the global context is used.
01376 
01377     >>> p, q, r = Bools('p q r')
01378     >>> And(p, Or(q, r))
01379     And(p, Or(q, r))
01380     """
01381     ctx = _get_ctx(ctx)
01382     if isinstance(names, str):
01383         names = names.split(" ")
01384     return [Bool(name, ctx) for name in names]
01385 
01386 def BoolVector(prefix, sz, ctx=None):
01387     """Return a list of Boolean constants of size `sz`.
01388 
01389     The constants are named using the given prefix.
01390     If `ctx=None`, then the global context is used.
01391     
01392     >>> P = BoolVector('p', 3)
01393     >>> P
01394     [p__0, p__1, p__2]
01395     >>> And(P)
01396     And(p__0, p__1, p__2)
01397     """
01398     return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
01399 
01400 def FreshBool(prefix='b', ctx=None):
01401     """Return a fresh Boolean constant in the given context using the given prefix.
01402     
01403     If `ctx=None`, then the global context is used.    
01404 
01405     >>> b1 = FreshBool()
01406     >>> b2 = FreshBool()
01407     >>> eq(b1, b2)
01408     False
01409     """
01410     ctx = _get_ctx(ctx)
01411     return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
01412 
01413 def Implies(a, b, ctx=None):
01414     """Create a Z3 implies expression. 
01415     
01416     >>> p, q = Bools('p q')
01417     >>> Implies(p, q)
01418     Implies(p, q)
01419     >>> simplify(Implies(p, q))
01420     Or(Not(p), q)
01421     """
01422     ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
01423     s = BoolSort(ctx)
01424     a = s.cast(a)
01425     b = s.cast(b)
01426     return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
01427 
01428 def Xor(a, b, ctx=None):
01429     """Create a Z3 Xor expression.
01430 
01431     >>> p, q = Bools('p q')
01432     >>> Xor(p, q)
01433     Xor(p, q)
01434     >>> simplify(Xor(p, q))
01435     Not(p) == q
01436     """
01437     ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
01438     s = BoolSort(ctx)
01439     a = s.cast(a)
01440     b = s.cast(b)
01441     return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
01442 
01443 def Not(a, ctx=None):
01444     """Create a Z3 not expression or probe. 
01445     
01446     >>> p = Bool('p')
01447     >>> Not(Not(p))
01448     Not(Not(p))
01449     >>> simplify(Not(Not(p)))
01450     p
01451     """
01452     ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
01453     if is_probe(a):
01454         # Not is also used to build probes
01455         return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
01456     else:
01457         s = BoolSort(ctx)
01458         a = s.cast(a)
01459         return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
01460 
01461 def _has_probe(args):
01462     """Return `True` if one of the elements of the given collection is a Z3 probe."""
01463     for arg in args:
01464         if is_probe(arg):
01465             return True
01466     return False
01467 
01468 def And(*args):
01469     """Create a Z3 and-expression or and-probe. 
01470     
01471     >>> p, q, r = Bools('p q r')
01472     >>> And(p, q, r)
01473     And(p, q, r)
01474     >>> P = BoolVector('p', 5)
01475     >>> And(P)
01476     And(p__0, p__1, p__2, p__3, p__4)
01477     """
01478     last_arg = None
01479     if len(args) > 0:
01480         last_arg = args[len(args)-1]
01481     if isinstance(last_arg, Context):
01482         ctx = args[len(args)-1]
01483         args = args[:len(args)-1]
01484     else:
01485         ctx = main_ctx()
01486     args = _get_args(args)
01487     ctx_args  = _ctx_from_ast_arg_list(args, ctx)
01488     if __debug__:
01489         _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
01490         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
01491     if _has_probe(args):
01492         return _probe_and(args, ctx)
01493     else:
01494         args  = _coerce_expr_list(args, ctx)
01495         _args, sz = _to_ast_array(args)
01496         return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
01497 
01498 def Or(*args):
01499     """Create a Z3 or-expression or or-probe. 
01500     
01501     >>> p, q, r = Bools('p q r')
01502     >>> Or(p, q, r)
01503     Or(p, q, r)
01504     >>> P = BoolVector('p', 5)
01505     >>> Or(P)
01506     Or(p__0, p__1, p__2, p__3, p__4)
01507     """
01508     last_arg = None
01509     if len(args) > 0:
01510         last_arg = args[len(args)-1]
01511     if isinstance(last_arg, Context):
01512         ctx = args[len(args)-1]
01513         args = args[:len(args)-1]
01514     else:
01515         ctx = main_ctx()
01516     args = _get_args(args)
01517     ctx_args  = _ctx_from_ast_arg_list(args, ctx)
01518     if __debug__:
01519         _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
01520         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
01521     if _has_probe(args):
01522         return _probe_or(args, ctx)
01523     else:
01524         args  = _coerce_expr_list(args, ctx)
01525         _args, sz = _to_ast_array(args)
01526         return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
01527 
01528 #########################################
01529 #
01530 # Patterns
01531 #
01532 #########################################
01533 
01534 class PatternRef(ExprRef):
01535     """Patterns are hints for quantifier instantiation. 
01536     
01537     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01538     """
01539     def as_ast(self):
01540         return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
01541 
01542     def get_id(self):
01543         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
01544 
01545 def is_pattern(a):
01546     """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
01547 
01548     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01549     
01550     >>> f = Function('f', IntSort(), IntSort())
01551     >>> x = Int('x')
01552     >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
01553     >>> q
01554     ForAll(x, f(x) == 0)
01555     >>> q.num_patterns()
01556     1
01557     >>> is_pattern(q.pattern(0))
01558     True
01559     >>> q.pattern(0)
01560     f(Var(0))
01561     """
01562     return isinstance(a, PatternRef)
01563 
01564 def MultiPattern(*args):
01565     """Create a Z3 multi-pattern using the given expressions `*args`
01566 
01567     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01568     
01569     >>> f = Function('f', IntSort(), IntSort())
01570     >>> g = Function('g', IntSort(), IntSort())
01571     >>> x = Int('x')
01572     >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
01573     >>> q
01574     ForAll(x, f(x) != g(x))
01575     >>> q.num_patterns()
01576     1
01577     >>> is_pattern(q.pattern(0))
01578     True
01579     >>> q.pattern(0)
01580     MultiPattern(f(Var(0)), g(Var(0)))
01581     """
01582     if __debug__:
01583         _z3_assert(len(args) > 0, "At least one argument expected")
01584         _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
01585     ctx = args[0].ctx
01586     args, sz = _to_ast_array(args)
01587     return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
01588 
01589 def _to_pattern(arg):
01590     if is_pattern(arg):
01591         return arg
01592     else:
01593         return MultiPattern(arg)
01594 
01595 #########################################
01596 #
01597 # Quantifiers
01598 #
01599 #########################################
01600 
01601 class QuantifierRef(BoolRef):
01602     """Universally and Existentially quantified formulas."""
01603 
01604     def as_ast(self):
01605         return self.ast
01606 
01607     def get_id(self):
01608         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
01609 
01610     def sort(self):
01611         """Return the Boolean sort."""
01612         return BoolSort(self.ctx)
01613 
01614     def is_forall(self):
01615         """Return `True` if `self` is a universal quantifier.
01616         
01617         >>> f = Function('f', IntSort(), IntSort())
01618         >>> x = Int('x')
01619         >>> q = ForAll(x, f(x) == 0)
01620         >>> q.is_forall()
01621         True
01622         >>> q = Exists(x, f(x) != 0)
01623         >>> q.is_forall()
01624         False
01625         """
01626         return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
01627 
01628     def weight(self):
01629         """Return the weight annotation of `self`.
01630 
01631         >>> f = Function('f', IntSort(), IntSort())
01632         >>> x = Int('x')
01633         >>> q = ForAll(x, f(x) == 0)
01634         >>> q.weight()
01635         1
01636         >>> q = ForAll(x, f(x) == 0, weight=10)
01637         >>> q.weight()
01638         10
01639         """
01640         return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
01641 
01642     def num_patterns(self):
01643         """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
01644 
01645         >>> f = Function('f', IntSort(), IntSort())
01646         >>> g = Function('g', IntSort(), IntSort())
01647         >>> x = Int('x')
01648         >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01649         >>> q.num_patterns()
01650         2
01651         """
01652         return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
01653 
01654     def pattern(self, idx):
01655         """Return a pattern (i.e., quantifier instantiation hints) in `self`.
01656 
01657         >>> f = Function('f', IntSort(), IntSort())
01658         >>> g = Function('g', IntSort(), IntSort())
01659         >>> x = Int('x')
01660         >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01661         >>> q.num_patterns()
01662         2
01663         >>> q.pattern(0)
01664         f(Var(0))
01665         >>> q.pattern(1)
01666         g(Var(0))
01667         """
01668         if __debug__:
01669             _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
01670         return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
01671 
01672     def num_no_patterns(self):
01673         """Return the number of no-patterns."""
01674         return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
01675 
01676     def no_pattern(self, idx):
01677         """Return a no-pattern."""
01678         if __debug__:
01679             _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
01680         return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
01681 
01682     def body(self):
01683         """Return the expression being quantified.
01684 
01685         >>> f = Function('f', IntSort(), IntSort())
01686         >>> x = Int('x')
01687         >>> q = ForAll(x, f(x) == 0)
01688         >>> q.body()
01689         f(Var(0)) == 0
01690         """
01691         return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
01692     
01693     def num_vars(self):
01694         """Return the number of variables bounded by this quantifier. 
01695         
01696         >>> f = Function('f', IntSort(), IntSort(), IntSort())
01697         >>> x = Int('x')
01698         >>> y = Int('y')
01699         >>> q = ForAll([x, y], f(x, y) >= x)
01700         >>> q.num_vars() 
01701         2
01702         """
01703         return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
01704 
01705     def var_name(self, idx):
01706         """Return a string representing a name used when displaying the quantifier. 
01707         
01708         >>> f = Function('f', IntSort(), IntSort(), IntSort())
01709         >>> x = Int('x')
01710         >>> y = Int('y')
01711         >>> q = ForAll([x, y], f(x, y) >= x)
01712         >>> q.var_name(0)
01713         'x'
01714         >>> q.var_name(1)
01715         'y'
01716         """
01717         if __debug__:
01718             _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01719         return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
01720 
01721     def var_sort(self, idx):
01722         """Return the sort of a bound variable.
01723 
01724         >>> f = Function('f', IntSort(), RealSort(), IntSort())
01725         >>> x = Int('x')
01726         >>> y = Real('y')
01727         >>> q = ForAll([x, y], f(x, y) >= x)
01728         >>> q.var_sort(0)
01729         Int
01730         >>> q.var_sort(1)
01731         Real
01732         """
01733         if __debug__:
01734             _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01735         return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
01736 
01737     def children(self):
01738         """Return a list containing a single element self.body()
01739 
01740         >>> f = Function('f', IntSort(), IntSort())
01741         >>> x = Int('x')
01742         >>> q = ForAll(x, f(x) == 0)
01743         >>> q.children()
01744         [f(Var(0)) == 0]
01745         """
01746         return [ self.body() ]
01747 
01748 def is_quantifier(a):
01749     """Return `True` if `a` is a Z3 quantifier.
01750     
01751     >>> f = Function('f', IntSort(), IntSort())
01752     >>> x = Int('x')
01753     >>> q = ForAll(x, f(x) == 0)
01754     >>> is_quantifier(q)
01755     True
01756     >>> is_quantifier(f(x))
01757     False
01758     """
01759     return isinstance(a, QuantifierRef)
01760 
01761 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01762     if __debug__:
01763         _z3_assert(is_bool(body), "Z3 expression expected")
01764         _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)")
01765         _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
01766         _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
01767     ctx = body.ctx
01768     if is_app(vs):
01769         vs = [vs]
01770     num_vars = len(vs)
01771     _vs = (Ast * num_vars)()
01772     for i in range(num_vars):
01773         ## TODO: Check if is constant
01774         _vs[i] = vs[i].as_ast()
01775     patterns = [ _to_pattern(p) for p in patterns ]
01776     num_pats = len(patterns)
01777     _pats = (Pattern * num_pats)()
01778     for i in range(num_pats):
01779         _pats[i] = patterns[i].ast
01780     _no_pats, num_no_pats = _to_ast_array(no_patterns)
01781     qid  = to_symbol(qid, ctx)
01782     skid = to_symbol(skid, ctx)
01783     return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid, 
01784                                                    num_vars, _vs, 
01785                                                    num_pats, _pats, 
01786                                                    num_no_pats, _no_pats, 
01787                                                    body.as_ast()), ctx)
01788 
01789 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01790     """Create a Z3 forall formula.
01791     
01792     The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
01793 
01794     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01795 
01796     >>> f = Function('f', IntSort(), IntSort(), IntSort())
01797     >>> x = Int('x')
01798     >>> y = Int('y')
01799     >>> ForAll([x, y], f(x, y) >= x)
01800     ForAll([x, y], f(x, y) >= x)
01801     >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
01802     ForAll([x, y], f(x, y) >= x)
01803     >>> ForAll([x, y], f(x, y) >= x, weight=10)
01804     ForAll([x, y], f(x, y) >= x)
01805     """
01806     return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
01807 
01808 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01809     """Create a Z3 exists formula.
01810     
01811     The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
01812 
01813     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01814 
01815     >>> f = Function('f', IntSort(), IntSort(), IntSort())
01816     >>> x = Int('x')
01817     >>> y = Int('y')
01818     >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
01819     >>> q
01820     Exists([x, y], f(x, y) >= x)
01821     >>> is_quantifier(q)
01822     True
01823     >>> r = Tactic('nnf')(q).as_expr()
01824     >>> is_quantifier(r)
01825     False
01826     """
01827     return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
01828 
01829 #########################################
01830 #
01831 # Arithmetic
01832 #
01833 #########################################
01834 
01835 class ArithSortRef(SortRef):
01836     """Real and Integer sorts."""
01837 
01838     def is_real(self):
01839         """Return `True` if `self` is of the sort Real.
01840         
01841         >>> x = Real('x')
01842         >>> x.is_real()
01843         True
01844         >>> (x + 1).is_real()
01845         True
01846         >>> x = Int('x')
01847         >>> x.is_real()
01848         False
01849         """
01850         return self.kind() == Z3_REAL_SORT
01851 
01852     def is_int(self):
01853         """Return `True` if `self` is of the sort Integer.
01854         
01855         >>> x = Int('x')
01856         >>> x.is_int()
01857         True
01858         >>> (x + 1).is_int()
01859         True
01860         >>> x = Real('x')
01861         >>> x.is_int()
01862         False
01863         """
01864         return self.kind() == Z3_INT_SORT
01865 
01866     def subsort(self, other):
01867         """Return `True` if `self` is a subsort of `other`."""
01868         return self.is_int() and is_arith_sort(other) and other.is_real()
01869 
01870     def cast(self, val):
01871         """Try to cast `val` as an Integer or Real.
01872         
01873         >>> IntSort().cast(10)
01874         10
01875         >>> is_int(IntSort().cast(10))
01876         True
01877         >>> is_int(10)
01878         False
01879         >>> RealSort().cast(10)
01880         10
01881         >>> is_real(RealSort().cast(10))
01882         True
01883         """
01884         if is_expr(val):
01885             if __debug__:
01886                 _z3_assert(self.ctx == val.ctx, "Context mismatch")
01887             val_s = val.sort()
01888             if self.eq(val_s):
01889                 return val
01890             if val_s.is_int() and self.is_real():
01891                 return ToReal(val)
01892             if __debug__:
01893                 _z3_assert(False, "Z3 Integer/Real expression expected" )
01894         else:
01895             if self.is_int():
01896                 return IntVal(val, self.ctx)
01897             if self.is_real():
01898                 return RealVal(val, self.ctx)
01899             if __debug__:
01900                 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
01901 
01902 def is_arith_sort(s):
01903     """Return `True` if s is an arithmetical sort (type).
01904     
01905     >>> is_arith_sort(IntSort())
01906     True
01907     >>> is_arith_sort(RealSort())
01908     True
01909     >>> is_arith_sort(BoolSort())
01910     False
01911     >>> n = Int('x') + 1
01912     >>> is_arith_sort(n.sort())
01913     True
01914     """
01915     return isinstance(s, ArithSortRef)
01916     
01917 class ArithRef(ExprRef):
01918     """Integer and Real expressions."""
01919 
01920     def sort(self):
01921         """Return the sort (type) of the arithmetical expression `self`.
01922         
01923         >>> Int('x').sort()
01924         Int
01925         >>> (Real('x') + 1).sort()
01926         Real
01927         """
01928         return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
01929 
01930     def is_int(self):
01931         """Return `True` if `self` is an integer expression.
01932         
01933         >>> x = Int('x')
01934         >>> x.is_int()
01935         True
01936         >>> (x + 1).is_int()
01937         True
01938         >>> y = Real('y')
01939         >>> (x + y).is_int()
01940         False
01941         """
01942         return self.sort().is_int()
01943 
01944     def is_real(self):
01945         """Return `True` if `self` is an real expression.
01946         
01947         >>> x = Real('x')
01948         >>> x.is_real()
01949         True
01950         >>> (x + 1).is_real()
01951         True
01952         """
01953         return self.sort().is_real()
01954 
01955     def __add__(self, other):
01956         """Create the Z3 expression `self + other`.
01957         
01958         >>> x = Int('x')
01959         >>> y = Int('y')
01960         >>> x + y
01961         x + y
01962         >>> (x + y).sort()
01963         Int
01964         """
01965         a, b = _coerce_exprs(self, other)
01966         return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
01967 
01968     def __radd__(self, other):
01969         """Create the Z3 expression `other + self`.
01970         
01971         >>> x = Int('x')
01972         >>> 10 + x
01973         10 + x
01974         """
01975         a, b = _coerce_exprs(self, other)
01976         return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
01977 
01978     def __mul__(self, other):
01979         """Create the Z3 expression `self * other`.
01980         
01981         >>> x = Real('x')
01982         >>> y = Real('y')
01983         >>> x * y
01984         x*y
01985         >>> (x * y).sort()
01986         Real
01987         """
01988         a, b = _coerce_exprs(self, other)
01989         return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
01990 
01991     def __rmul__(self, other):
01992         """Create the Z3 expression `other * self`.
01993         
01994         >>> x = Real('x')
01995         >>> 10 * x
01996         10*x
01997         """
01998         a, b = _coerce_exprs(self, other)
01999         return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
02000 
02001     def __sub__(self, other):
02002         """Create the Z3 expression `self - other`.
02003 
02004         >>> x = Int('x')
02005         >>> y = Int('y')
02006         >>> x - y
02007         x - y
02008         >>> (x - y).sort()
02009         Int
02010         """
02011         a, b = _coerce_exprs(self, other)
02012         return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
02013 
02014     def __rsub__(self, other):
02015         """Create the Z3 expression `other - self`.
02016         
02017         >>> x = Int('x')
02018         >>> 10 - x
02019         10 - x
02020         """
02021         a, b = _coerce_exprs(self, other)
02022         return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
02023 
02024     def __pow__(self, other):
02025         """Create the Z3 expression `self**other` (** is the power operator).
02026         
02027         >>> x = Real('x')
02028         >>> x**3
02029         x**3
02030         >>> (x**3).sort()
02031         Real
02032         >>> simplify(IntVal(2)**8)
02033         256
02034         """
02035         a, b = _coerce_exprs(self, other)
02036         return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02037 
02038     def __rpow__(self, other):
02039         """Create the Z3 expression `other**self` (** is the power operator).
02040         
02041         >>> x = Real('x')
02042         >>> 2**x
02043         2**x
02044         >>> (2**x).sort()
02045         Real
02046         >>> simplify(2**IntVal(8))
02047         256
02048         """
02049         a, b = _coerce_exprs(self, other)
02050         return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02051 
02052     def __div__(self, other):
02053         """Create the Z3 expression `other/self`.
02054         
02055         >>> x = Int('x')
02056         >>> y = Int('y')
02057         >>> x/y
02058         x/y
02059         >>> (x/y).sort()
02060         Int
02061         >>> (x/y).sexpr()
02062         '(div x y)'
02063         >>> x = Real('x')
02064         >>> y = Real('y')
02065         >>> x/y
02066         x/y
02067         >>> (x/y).sort()
02068         Real
02069         >>> (x/y).sexpr()
02070         '(/ x y)'
02071         """
02072         a, b = _coerce_exprs(self, other)
02073         return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02074 
02075     def __truediv__(self, other):
02076         """Create the Z3 expression `other/self`."""
02077         return self.__div__(other)
02078 
02079     def __rdiv__(self, other):
02080         """Create the Z3 expression `other/self`.
02081         
02082         >>> x = Int('x')
02083         >>> 10/x
02084         10/x
02085         >>> (10/x).sexpr()
02086         '(div 10 x)'
02087         >>> x = Real('x')
02088         >>> 10/x
02089         10/x
02090         >>> (10/x).sexpr()
02091         '(/ 10.0 x)'
02092         """
02093         a, b = _coerce_exprs(self, other)
02094         return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02095 
02096     def __rtruediv__(self, other):
02097         """Create the Z3 expression `other/self`."""
02098         return self.__rdiv__(other)
02099 
02100     def __mod__(self, other):
02101         """Create the Z3 expression `other%self`.
02102         
02103         >>> x = Int('x')
02104         >>> y = Int('y')
02105         >>> x % y
02106         x%y
02107         >>> simplify(IntVal(10) % IntVal(3))
02108         1
02109         """
02110         a, b = _coerce_exprs(self, other)
02111         if __debug__:
02112             _z3_assert(a.is_int(), "Z3 integer expression expected")
02113         return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02114 
02115     def __rmod__(self, other):
02116         """Create the Z3 expression `other%self`.
02117         
02118         >>> x = Int('x')
02119         >>> 10 % x
02120         10%x
02121         """
02122         a, b = _coerce_exprs(self, other)
02123         if __debug__:
02124             _z3_assert(a.is_int(), "Z3 integer expression expected")
02125         return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02126 
02127     def __neg__(self):
02128         """Return an expression representing `-self`.
02129 
02130         >>> x = Int('x')
02131         >>> -x
02132         -x
02133         >>> simplify(-(-x))
02134         x
02135         """
02136         return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
02137     
02138     def __pos__(self):
02139         """Return `self`.
02140         
02141         >>> x = Int('x')
02142         >>> +x
02143         x
02144         """
02145         return self
02146 
02147     def __le__(self, other):
02148         """Create the Z3 expression `other <= self`.
02149         
02150         >>> x, y = Ints('x y')
02151         >>> x <= y
02152         x <= y
02153         >>> y = Real('y')
02154         >>> x <= y
02155         ToReal(x) <= y
02156         """
02157         a, b = _coerce_exprs(self, other)
02158         return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02159 
02160     def __lt__(self, other):
02161         """Create the Z3 expression `other < self`.
02162         
02163         >>> x, y = Ints('x y')
02164         >>> x < y
02165         x < y
02166         >>> y = Real('y')
02167         >>> x < y
02168         ToReal(x) < y
02169         """
02170         a, b = _coerce_exprs(self, other)
02171         return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02172 
02173     def __gt__(self, other):
02174         """Create the Z3 expression `other > self`.
02175         
02176         >>> x, y = Ints('x y')
02177         >>> x > y
02178         x > y
02179         >>> y = Real('y')
02180         >>> x > y
02181         ToReal(x) > y
02182         """
02183         a, b = _coerce_exprs(self, other)
02184         return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02185         
02186     def __ge__(self, other):
02187         """Create the Z3 expression `other >= self`.
02188         
02189         >>> x, y = Ints('x y')
02190         >>> x >= y
02191         x >= y
02192         >>> y = Real('y')
02193         >>> x >= y
02194         ToReal(x) >= y
02195         """
02196         a, b = _coerce_exprs(self, other)
02197         return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02198 
02199 def is_arith(a):
02200     """Return `True` if `a` is an arithmetical expression.
02201     
02202     >>> x = Int('x')
02203     >>> is_arith(x)
02204     True
02205     >>> is_arith(x + 1)
02206     True
02207     >>> is_arith(1)
02208     False
02209     >>> is_arith(IntVal(1))
02210     True
02211     >>> y = Real('y')
02212     >>> is_arith(y)
02213     True
02214     >>> is_arith(y + 1)
02215     True
02216     """
02217     return isinstance(a, ArithRef)
02218 
02219 def is_int(a):
02220     """Return `True` if `a` is an integer expression.
02221     
02222     >>> x = Int('x')
02223     >>> is_int(x + 1)
02224     True
02225     >>> is_int(1)
02226     False
02227     >>> is_int(IntVal(1))
02228     True
02229     >>> y = Real('y')
02230     >>> is_int(y)
02231     False
02232     >>> is_int(y + 1)
02233     False
02234     """
02235     return is_arith(a) and a.is_int()
02236 
02237 def is_real(a):
02238     """Return `True` if `a` is a real expression.
02239     
02240     >>> x = Int('x')
02241     >>> is_real(x + 1)
02242     False
02243     >>> y = Real('y')
02244     >>> is_real(y)
02245     True
02246     >>> is_real(y + 1)
02247     True
02248     >>> is_real(1)
02249     False
02250     >>> is_real(RealVal(1))
02251     True
02252     """
02253     return is_arith(a) and a.is_real()
02254 
02255 def _is_numeral(ctx, a):
02256     return Z3_is_numeral_ast(ctx.ref(), a)
02257 
02258 def _is_algebraic(ctx, a):
02259     return Z3_is_algebraic_number(ctx.ref(), a)
02260 
02261 def is_int_value(a):
02262     """Return `True` if `a` is an integer value of sort Int.
02263     
02264     >>> is_int_value(IntVal(1))
02265     True
02266     >>> is_int_value(1)
02267     False
02268     >>> is_int_value(Int('x'))
02269     False
02270     >>> n = Int('x') + 1
02271     >>> n
02272     x + 1
02273     >>> n.arg(1)
02274     1
02275     >>> is_int_value(n.arg(1))
02276     True
02277     >>> is_int_value(RealVal("1/3"))
02278     False
02279     >>> is_int_value(RealVal(1))
02280     False
02281     """
02282     return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
02283 
02284 def is_rational_value(a):
02285     """Return `True` if `a` is rational value of sort Real.
02286     
02287     >>> is_rational_value(RealVal(1))
02288     True
02289     >>> is_rational_value(RealVal("3/5"))
02290     True
02291     >>> is_rational_value(IntVal(1))
02292     False
02293     >>> is_rational_value(1)
02294     False
02295     >>> n = Real('x') + 1
02296     >>> n.arg(1)
02297     1
02298     >>> is_rational_value(n.arg(1))
02299     True
02300     >>> is_rational_value(Real('x'))
02301     False
02302     """
02303     return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
02304 
02305 def is_algebraic_value(a):
02306     """Return `True` if `a` is an algerbraic value of sort Real.
02307     
02308     >>> is_algebraic_value(RealVal("3/5"))
02309     False
02310     >>> n = simplify(Sqrt(2))
02311     >>> n
02312     1.4142135623?
02313     >>> is_algebraic_value(n)
02314     True
02315     """
02316     return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
02317 
02318 def is_add(a):
02319     """Return `True` if `a` is an expression of the form b + c.
02320     
02321     >>> x, y = Ints('x y')
02322     >>> is_add(x + y)
02323     True
02324     >>> is_add(x - y)
02325     False
02326     """
02327     return is_app_of(a, Z3_OP_ADD)
02328 
02329 def is_mul(a):
02330     """Return `True` if `a` is an expression of the form b * c.
02331     
02332     >>> x, y = Ints('x y')
02333     >>> is_mul(x * y)
02334     True
02335     >>> is_mul(x - y)
02336     False
02337     """
02338     return is_app_of(a, Z3_OP_MUL)
02339 
02340 def is_sub(a):
02341     """Return `True` if `a` is an expression of the form b - c.
02342     
02343     >>> x, y = Ints('x y')
02344     >>> is_sub(x - y)
02345     True
02346     >>> is_sub(x + y)
02347     False
02348     """
02349     return is_app_of(a, Z3_OP_SUB)
02350 
02351 def is_div(a):
02352     """Return `True` if `a` is an expression of the form b / c.
02353     
02354     >>> x, y = Reals('x y')
02355     >>> is_div(x / y)
02356     True
02357     >>> is_div(x + y)
02358     False
02359     >>> x, y = Ints('x y')
02360     >>> is_div(x / y)
02361     False
02362     >>> is_idiv(x / y)
02363     True
02364     """
02365     return is_app_of(a, Z3_OP_DIV)
02366 
02367 def is_idiv(a):
02368     """Return `True` if `a` is an expression of the form b div c.
02369     
02370     >>> x, y = Ints('x y')
02371     >>> is_idiv(x / y)
02372     True
02373     >>> is_idiv(x + y)
02374     False
02375     """
02376     return is_app_of(a, Z3_OP_IDIV)
02377 
02378 def is_mod(a):
02379     """Return `True` if `a` is an expression of the form b % c.
02380 
02381     >>> x, y = Ints('x y')
02382     >>> is_mod(x % y)
02383     True
02384     >>> is_mod(x + y)
02385     False
02386     """
02387     return is_app_of(a, Z3_OP_MOD)
02388 
02389 def is_le(a):
02390     """Return `True` if `a` is an expression of the form b <= c.
02391     
02392     >>> x, y = Ints('x y')
02393     >>> is_le(x <= y)
02394     True
02395     >>> is_le(x < y)
02396     False
02397     """
02398     return is_app_of(a, Z3_OP_LE)
02399 
02400 def is_lt(a):
02401     """Return `True` if `a` is an expression of the form b < c.
02402     
02403     >>> x, y = Ints('x y')
02404     >>> is_lt(x < y)
02405     True
02406     >>> is_lt(x == y)
02407     False
02408     """
02409     return is_app_of(a, Z3_OP_LT)
02410 
02411 def is_ge(a):
02412     """Return `True` if `a` is an expression of the form b >= c.
02413     
02414     >>> x, y = Ints('x y')
02415     >>> is_ge(x >= y)
02416     True
02417     >>> is_ge(x == y)
02418     False
02419     """
02420     return is_app_of(a, Z3_OP_GE)
02421 
02422 def is_gt(a):
02423     """Return `True` if `a` is an expression of the form b > c.
02424     
02425     >>> x, y = Ints('x y')
02426     >>> is_gt(x > y)
02427     True
02428     >>> is_gt(x == y)
02429     False
02430     """
02431     return is_app_of(a, Z3_OP_GT)
02432 
02433 def is_is_int(a):
02434     """Return `True` if `a` is an expression of the form IsInt(b).
02435     
02436     >>> x = Real('x')
02437     >>> is_is_int(IsInt(x))
02438     True
02439     >>> is_is_int(x)
02440     False
02441     """
02442     return is_app_of(a, Z3_OP_IS_INT)
02443 
02444 def is_to_real(a):
02445     """Return `True` if `a` is an expression of the form ToReal(b).
02446     
02447     >>> x = Int('x')
02448     >>> n = ToReal(x)
02449     >>> n
02450     ToReal(x)
02451     >>> is_to_real(n)
02452     True
02453     >>> is_to_real(x)
02454     False
02455     """
02456     return is_app_of(a, Z3_OP_TO_REAL)
02457 
02458 def is_to_int(a):
02459     """Return `True` if `a` is an expression of the form ToInt(b).
02460     
02461     >>> x = Real('x')
02462     >>> n = ToInt(x)
02463     >>> n
02464     ToInt(x)
02465     >>> is_to_int(n)
02466     True
02467     >>> is_to_int(x)
02468     False
02469     """
02470     return is_app_of(a, Z3_OP_TO_INT)
02471 
02472 class IntNumRef(ArithRef):
02473     """Integer values."""
02474 
02475     def as_long(self):
02476         """Return a Z3 integer numeral as a Python long (bignum) numeral. 
02477         
02478         >>> v = IntVal(1)
02479         >>> v + 1
02480         1 + 1
02481         >>> v.as_long() + 1
02482         2
02483         """
02484         if __debug__:
02485             _z3_assert(self.is_int(), "Integer value expected")
02486         return int(self.as_string())
02487 
02488     def as_string(self):
02489         """Return a Z3 integer numeral as a Python string.
02490         >>> v = IntVal(100)
02491         >>> v.as_string()
02492         '100'
02493         """
02494         return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
02495 
02496 class RatNumRef(ArithRef):
02497     """Rational values."""
02498 
02499     def numerator(self):
02500         """ Return the numerator of a Z3 rational numeral. 
02501 
02502         >>> is_rational_value(RealVal("3/5"))
02503         True
02504         >>> n = RealVal("3/5")
02505         >>> n.numerator()
02506         3
02507         >>> is_rational_value(Q(3,5))
02508         True
02509         >>> Q(3,5).numerator()
02510         3
02511         """
02512         return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
02513 
02514     def denominator(self):
02515         """ Return the denominator of a Z3 rational numeral. 
02516         
02517         >>> is_rational_value(Q(3,5))
02518         True
02519         >>> n = Q(3,5)
02520         >>> n.denominator()
02521         5
02522         """
02523         return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
02524 
02525     def numerator_as_long(self):
02526         """ Return the numerator as a Python long.
02527         
02528         >>> v = RealVal(10000000000)
02529         >>> v
02530         10000000000
02531         >>> v + 1
02532         10000000000 + 1
02533         >>> v.numerator_as_long() + 1 == 10000000001
02534         True
02535         """
02536         return self.numerator().as_long()
02537         
02538     def denominator_as_long(self):
02539         """ Return the denominator as a Python long.
02540 
02541         >>> v = RealVal("1/3")
02542         >>> v
02543         1/3
02544         >>> v.denominator_as_long()
02545         3
02546         """
02547         return self.denominator().as_long()
02548 
02549     def as_decimal(self, prec):
02550         """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
02551         
02552         >>> v = RealVal("1/5")
02553         >>> v.as_decimal(3)
02554         '0.2'
02555         >>> v = RealVal("1/3")
02556         >>> v.as_decimal(3)
02557         '0.333?'
02558         """
02559         return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
02560 
02561     def as_string(self):
02562         """Return a Z3 rational numeral as a Python string.
02563 
02564         >>> v = Q(3,6)
02565         >>> v.as_string()
02566         '1/2'
02567         """
02568         return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
02569 
02570     def as_fraction(self):
02571         """Return a Z3 rational as a Python Fraction object.
02572         
02573         >>> v = RealVal("1/5")
02574         >>> v.as_fraction()
02575         Fraction(1, 5)
02576         """
02577         return Fraction(self.numerator_as_long(), self.denominator_as_long())
02578 
02579 class AlgebraicNumRef(ArithRef):
02580     """Algebraic irrational values."""
02581 
02582     def approx(self, precision=10):
02583         """Return a Z3 rational number that approximates the algebraic number `self`. 
02584         The result `r` is such that |r - self| <= 1/10^precision 
02585         
02586         >>> x = simplify(Sqrt(2))
02587         >>> x.approx(20)
02588         6838717160008073720548335/4835703278458516698824704
02589         >>> x.approx(5)
02590         2965821/2097152
02591         """
02592         return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
02593     def as_decimal(self, prec):
02594         """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places
02595 
02596         >>> x = simplify(Sqrt(2))
02597         >>> x.as_decimal(10)
02598         '1.4142135623?'
02599         >>> x.as_decimal(20)
02600         '1.41421356237309504880?'
02601         """
02602         return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
02603 
02604 def _py2expr(a, ctx=None):
02605     if isinstance(a, bool):
02606         return BoolVal(a, ctx)
02607     if _is_int(a):
02608         return IntVal(a, ctx)
02609     if isinstance(a, float):
02610         return RealVal(a, ctx)
02611     if __debug__:
02612         _z3_assert(False, "Python bool, int, long or float expected")
02613 
02614 def IntSort(ctx=None):
02615     """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
02616     
02617     >>> IntSort()
02618     Int
02619     >>> x = Const('x', IntSort())
02620     >>> is_int(x)
02621     True
02622     >>> x.sort() == IntSort()
02623     True
02624     >>> x.sort() == BoolSort()
02625     False
02626     """
02627     ctx = _get_ctx(ctx)
02628     return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
02629 
02630 def RealSort(ctx=None):
02631     """Return the real sort in the given context. If `ctx=None`, then the global context is used.
02632     
02633     >>> RealSort()
02634     Real
02635     >>> x = Const('x', RealSort())
02636     >>> is_real(x)
02637     True
02638     >>> is_int(x)
02639     False
02640     >>> x.sort() == RealSort()
02641     True
02642     """
02643     ctx = _get_ctx(ctx)
02644     return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
02645 
02646 def _to_int_str(val):
02647     if isinstance(val, float):
02648         return str(int(val))
02649     elif isinstance(val, bool):
02650         if val:
02651             return "1"
02652         else:
02653             return "0"
02654     elif _is_int(val):
02655         return str(val)
02656     elif isinstance(val, str):
02657         return val
02658     if __debug__:
02659         _z3_assert(False, "Python value cannot be used as a Z3 integer")
02660 
02661 def IntVal(val, ctx=None):
02662     """Return a Z3 integer value. If `ctx=None`, then the global context is used.
02663     
02664     >>> IntVal(1)
02665     1
02666     >>> IntVal("100")
02667     100
02668     """
02669     ctx = _get_ctx(ctx)
02670     return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
02671 
02672 def RealVal(val, ctx=None):
02673     """Return a Z3 real value. 
02674     
02675     `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
02676     If `ctx=None`, then the global context is used.
02677     
02678     >>> RealVal(1)
02679     1
02680     >>> RealVal(1).sort()
02681     Real
02682     >>> RealVal("3/5")
02683     3/5
02684     >>> RealVal("1.5")
02685     3/2
02686     """
02687     ctx = _get_ctx(ctx)
02688     return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
02689 
02690 def RatVal(a, b, ctx=None):
02691     """Return a Z3 rational a/b.
02692 
02693     If `ctx=None`, then the global context is used.
02694     
02695     >>> RatVal(3,5)
02696     3/5
02697     >>> RatVal(3,5).sort()
02698     Real
02699     """
02700     if __debug__:
02701         _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
02702         _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
02703     return simplify(RealVal(a, ctx)/RealVal(b, ctx))
02704 
02705 def Q(a, b, ctx=None):
02706     """Return a Z3 rational a/b.
02707     
02708     If `ctx=None`, then the global context is used.
02709 
02710     >>> Q(3,5)
02711     3/5
02712     >>> Q(3,5).sort()
02713     Real
02714     """
02715     return simplify(RatVal(a, b))
02716 
02717 def Int(name, ctx=None):
02718     """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
02719 
02720     >>> x = Int('x')
02721     >>> is_int(x)
02722     True
02723     >>> is_int(x + 1)
02724     True
02725     """
02726     ctx = _get_ctx(ctx)
02727     return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
02728 
02729 def Ints(names, ctx=None):
02730     """Return a tuple of Integer constants. 
02731     
02732     >>> x, y, z = Ints('x y z')
02733     >>> Sum(x, y, z)
02734     x + y + z
02735     """
02736     ctx = _get_ctx(ctx)
02737     if isinstance(names, str):
02738         names = names.split(" ")
02739     return [Int(name, ctx) for name in names]
02740 
02741 def IntVector(prefix, sz, ctx=None):
02742     """Return a list of integer constants of size `sz`.
02743     
02744     >>> X = IntVector('x', 3)
02745     >>> X
02746     [x__0, x__1, x__2]
02747     >>> Sum(X)
02748     x__0 + x__1 + x__2
02749     """
02750     return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
02751 
02752 def FreshInt(prefix='x', ctx=None):
02753     """Return a fresh integer constant in the given context using the given prefix.
02754 
02755     >>> x = FreshInt()
02756     >>> y = FreshInt()
02757     >>> eq(x, y)
02758     False
02759     >>> x.sort()
02760     Int
02761     """
02762     ctx = _get_ctx(ctx)
02763     return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
02764 
02765 def Real(name, ctx=None):
02766     """Return a real constant named `name`. If `ctx=None`, then the global context is used.
02767 
02768     >>> x = Real('x')
02769     >>> is_real(x)
02770     True
02771     >>> is_real(x + 1)
02772     True
02773     """
02774     ctx = _get_ctx(ctx)
02775     return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
02776 
02777 def Reals(names, ctx=None):
02778     """Return a tuple of real constants. 
02779     
02780     >>> x, y, z = Reals('x y z')
02781     >>> Sum(x, y, z)
02782     x + y + z
02783     >>> Sum(x, y, z).sort()
02784     Real
02785     """
02786     ctx = _get_ctx(ctx)
02787     if isinstance(names, str):
02788         names = names.split(" ")
02789     return [Real(name, ctx) for name in names]
02790 
02791 def RealVector(prefix, sz, ctx=None):
02792     """Return a list of real constants of size `sz`.
02793     
02794     >>> X = RealVector('x', 3)
02795     >>> X
02796     [x__0, x__1, x__2]
02797     >>> Sum(X)
02798     x__0 + x__1 + x__2
02799     >>> Sum(X).sort()
02800     Real
02801     """
02802     return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]
02803 
02804 def FreshReal(prefix='b', ctx=None):
02805     """Return a fresh real constant in the given context using the given prefix.
02806 
02807     >>> x = FreshReal()
02808     >>> y = FreshReal()
02809     >>> eq(x, y)
02810     False
02811     >>> x.sort()
02812     Real
02813     """
02814     ctx = _get_ctx(ctx)
02815     return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
02816 
02817 def ToReal(a):
02818     """ Return the Z3 expression ToReal(a). 
02819     
02820     >>> x = Int('x')
02821     >>> x.sort()
02822     Int
02823     >>> n = ToReal(x)
02824     >>> n
02825     ToReal(x)
02826     >>> n.sort()
02827     Real
02828     """
02829     if __debug__:
02830         _z3_assert(a.is_int(), "Z3 integer expression expected.")
02831     ctx = a.ctx
02832     return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
02833 
02834 def ToInt(a):
02835     """ Return the Z3 expression ToInt(a). 
02836     
02837     >>> x = Real('x')
02838     >>> x.sort()
02839     Real
02840     >>> n = ToInt(x)
02841     >>> n
02842     ToInt(x)
02843     >>> n.sort()
02844     Int
02845     """
02846     if __debug__:
02847         _z3_assert(a.is_real(), "Z3 real expression expected.")
02848     ctx = a.ctx
02849     return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
02850 
02851 def IsInt(a):
02852     """ Return the Z3 predicate IsInt(a). 
02853     
02854     >>> x = Real('x')
02855     >>> IsInt(x + "1/2")
02856     IsInt(x + 1/2)
02857     >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
02858     [x = 1/2]
02859     >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
02860     no solution
02861     """
02862     if __debug__:
02863         _z3_assert(a.is_real(), "Z3 real expression expected.")
02864     ctx = a.ctx
02865     return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
02866     
02867 def Sqrt(a, ctx=None):
02868     """ Return a Z3 expression which represents the square root of a. 
02869     
02870     >>> x = Real('x')
02871     >>> Sqrt(x)
02872     x**(1/2)
02873     """
02874     if not is_expr(a):
02875         ctx = _get_ctx(ctx)
02876         a = RealVal(a, ctx)
02877     return a ** "1/2"
02878 
02879 def Cbrt(a, ctx=None):
02880     """ Return a Z3 expression which represents the cubic root of a. 
02881     
02882     >>> x = Real('x')
02883     >>> Cbrt(x)
02884     x**(1/3)
02885     """
02886     if not is_expr(a):
02887         ctx = _get_ctx(ctx)
02888         a = RealVal(a, ctx)
02889     return a ** "1/3"
02890 
02891 #########################################
02892 #
02893 # Bit-Vectors
02894 #
02895 #########################################
02896 
02897 class BitVecSortRef(SortRef):
02898     """Bit-vector sort."""
02899 
02900     def size(self):
02901         """Return the size (number of bits) of the bit-vector sort `self`.
02902         
02903         >>> b = BitVecSort(32)
02904         >>> b.size()
02905         32
02906         """
02907         return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast))
02908 
02909     def subsort(self, other):
02910         return is_bv_sort(other) and self.size() < other.size()
02911 
02912     def cast(self, val):
02913         """Try to cast `val` as a Bit-Vector.
02914 
02915         >>> b = BitVecSort(32)
02916         >>> b.cast(10)
02917         10
02918         >>> b.cast(10).sexpr()
02919         '#x0000000a'
02920         """
02921         if is_expr(val):
02922             if __debug__:
02923                 _z3_assert(self.ctx == val.ctx, "Context mismatch")
02924             # Idea: use sign_extend if sort of val is a bitvector of smaller size
02925             return val
02926         else:
02927             return BitVecVal(val, self)
02928 
02929 def is_bv_sort(s):
02930     """Return True if `s` is a Z3 bit-vector sort.
02931 
02932     >>> is_bv_sort(BitVecSort(32))
02933     True
02934     >>> is_bv_sort(IntSort())
02935     False
02936     """
02937     return isinstance(s, BitVecSortRef)
02938 
02939 class BitVecRef(ExprRef):
02940     """Bit-vector expressions."""
02941 
02942     def sort(self):
02943         """Return the sort of the bit-vector expression `self`.
02944 
02945         >>> x = BitVec('x', 32)
02946         >>> x.sort()
02947         BitVec(32)
02948         >>> x.sort() == BitVecSort(32)
02949         True
02950         """
02951         return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
02952 
02953     def size(self):
02954         """Return the number of bits of the bit-vector expression `self`.
02955         
02956         >>> x = BitVec('x', 32)
02957         >>> (x + 1).size()
02958         32
02959         >>> Concat(x, x).size()
02960         64
02961         """
02962         return self.sort().size()
02963     
02964     def __add__(self, other):
02965         """Create the Z3 expression `self + other`.
02966         
02967         >>> x = BitVec('x', 32)
02968         >>> y = BitVec('y', 32)
02969         >>> x + y
02970         x + y
02971         >>> (x + y).sort()
02972         BitVec(32)
02973         """
02974         a, b = _coerce_exprs(self, other)
02975         return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02976 
02977     def __radd__(self, other):
02978         """Create the Z3 expression `other + self`.
02979         
02980         >>> x = BitVec('x', 32)
02981         >>> 10 + x
02982         10 + x
02983         """
02984         a, b = _coerce_exprs(self, other)
02985         return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02986 
02987     def __mul__(self, other):
02988         """Create the Z3 expression `self * other`.
02989         
02990         >>> x = BitVec('x', 32)
02991         >>> y = BitVec('y', 32)
02992         >>> x * y
02993         x*y
02994         >>> (x * y).sort()
02995         BitVec(32)
02996         """
02997         a, b = _coerce_exprs(self, other)
02998         return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02999 
03000     def __rmul__(self, other):
03001         """Create the Z3 expression `other * self`.
03002         
03003         >>> x = BitVec('x', 32)
03004         >>> 10 * x
03005         10*x
03006         """
03007         a, b = _coerce_exprs(self, other)
03008         return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03009 
03010     def __sub__(self, other):
03011         """Create the Z3 expression `self - other`.
03012         
03013         >>> x = BitVec('x', 32)
03014         >>> y = BitVec('y', 32)
03015         >>> x - y
03016         x - y
03017         >>> (x - y).sort()
03018         BitVec(32)
03019         """
03020         a, b = _coerce_exprs(self, other)
03021         return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03022 
03023     def __rsub__(self, other):
03024         """Create the Z3 expression `other - self`.
03025         
03026         >>> x = BitVec('x', 32)
03027         >>> 10 - x
03028         10 - x
03029         """
03030         a, b = _coerce_exprs(self, other)
03031         return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03032 
03033     def __or__(self, other):
03034         """Create the Z3 expression bitwise-or `self | other`.
03035         
03036         >>> x = BitVec('x', 32)
03037         >>> y = BitVec('y', 32)
03038         >>> x | y
03039         x | y
03040         >>> (x | y).sort()
03041         BitVec(32)
03042         """
03043         a, b = _coerce_exprs(self, other)
03044         return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03045 
03046     def __ror__(self, other):
03047         """Create the Z3 expression bitwise-or `other | self`.
03048         
03049         >>> x = BitVec('x', 32)
03050         >>> 10 | x
03051         10 | x
03052         """
03053         a, b = _coerce_exprs(self, other)
03054         return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03055 
03056     def __and__(self, other):
03057         """Create the Z3 expression bitwise-and `self & other`.
03058         
03059         >>> x = BitVec('x', 32)
03060         >>> y = BitVec('y', 32)
03061         >>> x & y
03062         x & y
03063         >>> (x & y).sort()
03064         BitVec(32)
03065         """
03066         a, b = _coerce_exprs(self, other)
03067         return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03068 
03069     def __rand__(self, other):
03070         """Create the Z3 expression bitwise-or `other & self`.
03071         
03072         >>> x = BitVec('x', 32)
03073         >>> 10 & x
03074         10 & x
03075         """
03076         a, b = _coerce_exprs(self, other)
03077         return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03078 
03079     def __xor__(self, other):
03080         """Create the Z3 expression bitwise-xor `self ^ other`.
03081         
03082         >>> x = BitVec('x', 32)
03083         >>> y = BitVec('y', 32)
03084         >>> x ^ y
03085         x ^ y
03086         >>> (x ^ y).sort()
03087         BitVec(32)
03088         """
03089         a, b = _coerce_exprs(self, other)
03090         return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03091 
03092     def __rxor__(self, other):
03093         """Create the Z3 expression bitwise-xor `other ^ self`.
03094         
03095         >>> x = BitVec('x', 32)
03096         >>> 10 ^ x
03097         10 ^ x
03098         """
03099         a, b = _coerce_exprs(self, other)
03100         return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03101 
03102     def __pos__(self):
03103         """Return `self`.
03104 
03105         >>> x = BitVec('x', 32)
03106         >>> +x
03107         x
03108         """
03109         return self
03110 
03111     def __neg__(self):
03112         """Return an expression representing `-self`.
03113 
03114         >>> x = BitVec('x', 32)
03115         >>> -x
03116         -x
03117         >>> simplify(-(-x))
03118         x
03119         """
03120         return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
03121 
03122     def __invert__(self):
03123         """Create the Z3 expression bitwise-not `~self`.
03124 
03125         >>> x = BitVec('x', 32)
03126         >>> ~x
03127         ~x
03128         >>> simplify(~(~x))
03129         x
03130         """
03131         return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
03132 
03133     def __div__(self, other):
03134         """Create the Z3 expression (signed) division `self / other`.
03135 
03136         Use the function UDiv() for unsigned division.
03137 
03138         >>> x = BitVec('x', 32)
03139         >>> y = BitVec('y', 32)
03140         >>> x / y
03141         x/y
03142         >>> (x / y).sort()
03143         BitVec(32)
03144         >>> (x / y).sexpr()
03145         '(bvsdiv x y)'
03146         >>> UDiv(x, y).sexpr()
03147         '(bvudiv x y)'
03148         """
03149         a, b = _coerce_exprs(self, other)
03150         return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03151 
03152     def __truediv__(self, other):
03153         """Create the Z3 expression (signed) division `self / other`."""
03154         return self.__div__(other)
03155 
03156     def __rdiv__(self, other):
03157         """Create the Z3 expression (signed) division `other / self`.
03158 
03159         Use the function UDiv() for unsigned division.
03160 
03161         >>> x = BitVec('x', 32)
03162         >>> 10 / x
03163         10/x
03164         >>> (10 / x).sexpr()
03165         '(bvsdiv #x0000000a x)'
03166         >>> UDiv(10, x).sexpr()
03167         '(bvudiv #x0000000a x)'
03168         """
03169         a, b = _coerce_exprs(self, other)
03170         return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03171 
03172     def __rtruediv__(self, other):
03173         """Create the Z3 expression (signed) division `other / self`."""
03174         return self.__rdiv__(other)
03175 
03176     def __mod__(self, other):
03177         """Create the Z3 expression (signed) mod `self % other`.
03178 
03179         Use the function URem() for unsigned remainder, and SRem() for signed remainder.
03180 
03181         >>> x = BitVec('x', 32)
03182         >>> y = BitVec('y', 32)
03183         >>> x % y
03184         x%y
03185         >>> (x % y).sort()
03186         BitVec(32)
03187         >>> (x % y).sexpr()
03188         '(bvsmod x y)'
03189         >>> URem(x, y).sexpr()
03190         '(bvurem x y)'
03191         >>> SRem(x, y).sexpr()
03192         '(bvsrem x y)'
03193         """
03194         a, b = _coerce_exprs(self, other)
03195         return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03196 
03197     def __rmod__(self, other):
03198         """Create the Z3 expression (signed) mod `other % self`.
03199 
03200         Use the function URem() for unsigned remainder, and SRem() for signed remainder.
03201 
03202         >>> x = BitVec('x', 32)
03203         >>> 10 % x
03204         10%x
03205         >>> (10 % x).sexpr()
03206         '(bvsmod #x0000000a x)'
03207         >>> URem(10, x).sexpr()
03208         '(bvurem #x0000000a x)'
03209         >>> SRem(10, x).sexpr()
03210         '(bvsrem #x0000000a x)'
03211         """
03212         a, b = _coerce_exprs(self, other)
03213         return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03214 
03215     def __le__(self, other):
03216         """Create the Z3 expression (signed) `other <= self`.
03217         
03218         Use the function ULE() for unsigned less than or equal to.
03219 
03220         >>> x, y = BitVecs('x y', 32)
03221         >>> x <= y
03222         x <= y
03223         >>> (x <= y).sexpr()
03224         '(bvsle x y)'
03225         >>> ULE(x, y).sexpr()
03226         '(bvule x y)'
03227         """
03228         a, b = _coerce_exprs(self, other)
03229         return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03230 
03231     def __lt__(self, other):
03232         """Create the Z3 expression (signed) `other < self`.
03233         
03234         Use the function ULT() for unsigned less than.
03235 
03236         >>> x, y = BitVecs('x y', 32)
03237         >>> x < y
03238         x < y
03239         >>> (x < y).sexpr()
03240         '(bvslt x y)'
03241         >>> ULT(x, y).sexpr()
03242         '(bvult x y)'
03243         """
03244         a, b = _coerce_exprs(self, other)
03245         return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03246 
03247     def __gt__(self, other):
03248         """Create the Z3 expression (signed) `other > self`.
03249         
03250         Use the function UGT() for unsigned greater than.
03251 
03252         >>> x, y = BitVecs('x y', 32)
03253         >>> x > y
03254         x > y
03255         >>> (x > y).sexpr()
03256         '(bvsgt x y)'
03257         >>> UGT(x, y).sexpr()
03258         '(bvugt x y)'
03259         """
03260         a, b = _coerce_exprs(self, other)
03261         return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03262         
03263     def __ge__(self, other):
03264         """Create the Z3 expression (signed) `other >= self`.
03265         
03266         Use the function UGE() for unsigned greater than or equal to.
03267 
03268         >>> x, y = BitVecs('x y', 32)
03269         >>> x >= y
03270         x >= y
03271         >>> (x >= y).sexpr()
03272         '(bvsge x y)'
03273         >>> UGE(x, y).sexpr()
03274         '(bvuge x y)'
03275         """
03276         a, b = _coerce_exprs(self, other)
03277         return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03278 
03279     def __rshift__(self, other):
03280         """Create the Z3 expression (arithmetical) right shift `self >> other`
03281 
03282         Use the function LShR() for the right logical shift
03283 
03284         >>> x, y = BitVecs('x y', 32)
03285         >>> x >> y
03286         x >> y
03287         >>> (x >> y).sexpr()
03288         '(bvashr x y)'
03289         >>> LShR(x, y).sexpr()
03290         '(bvlshr x y)'
03291         >>> BitVecVal(4, 3)
03292         4
03293         >>> BitVecVal(4, 3).as_signed_long()
03294         -4
03295         >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
03296         -2
03297         >>> simplify(BitVecVal(4, 3) >> 1)
03298         6
03299         >>> simplify(LShR(BitVecVal(4, 3), 1))
03300         2
03301         >>> simplify(BitVecVal(2, 3) >> 1)
03302         1
03303         >>> simplify(LShR(BitVecVal(2, 3), 1))
03304         1
03305         """
03306         a, b = _coerce_exprs(self, other)
03307         return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03308 
03309     def __lshift__(self, other):
03310         """Create the Z3 expression left shift `self << other`
03311 
03312         >>> x, y = BitVecs('x y', 32)
03313         >>> x << y
03314         x << y
03315         >>> (x << y).sexpr()
03316         '(bvshl x y)'
03317         >>> simplify(BitVecVal(2, 3) << 1)
03318         4
03319         """
03320         a, b = _coerce_exprs(self, other)
03321         return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03322 
03323     def __rrshift__(self, other):
03324         """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
03325 
03326         Use the function LShR() for the right logical shift
03327 
03328         >>> x = BitVec('x', 32)
03329         >>> 10 >> x
03330         10 >> x
03331         >>> (10 >> x).sexpr()
03332         '(bvashr #x0000000a x)'
03333         """
03334         a, b = _coerce_exprs(self, other)
03335         return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03336 
03337     def __rlshift__(self, other):
03338         """Create the Z3 expression left shift `other << self`.
03339 
03340         Use the function LShR() for the right logical shift
03341 
03342         >>> x = BitVec('x', 32)
03343         >>> 10 << x
03344         10 << x
03345         >>> (10 << x).sexpr()
03346         '(bvshl #x0000000a x)'
03347         """
03348         a, b = _coerce_exprs(self, other)
03349         return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03350 
03351 class BitVecNumRef(BitVecRef):
03352     """Bit-vector values."""
03353 
03354     def as_long(self):
03355         """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. 
03356         
03357         >>> v = BitVecVal(0xbadc0de, 32)
03358         >>> v
03359         195936478
03360         >>> print("0x%.8x" % v.as_long())
03361         0x0badc0de
03362         """
03363         return int(self.as_string())
03364 
03365     def as_signed_long(self):
03366         """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.
03367         
03368         >>> BitVecVal(4, 3).as_signed_long()
03369         -4
03370         >>> BitVecVal(7, 3).as_signed_long()
03371         -1
03372         >>> BitVecVal(3, 3).as_signed_long()
03373         3
03374         >>> BitVecVal(2**32 - 1, 32).as_signed_long()
03375         -1
03376         >>> BitVecVal(2**64 - 1, 64).as_signed_long()
03377         -1
03378         """
03379         sz = self.size()
03380         val = self.as_long()
03381         if val >= 2**(sz - 1):
03382             val = val - 2**sz
03383         if val < -2**(sz - 1):
03384             val = val + 2**sz
03385         return int(val)
03386 
03387     def as_string(self):
03388         return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
03389 
03390 def is_bv(a):
03391     """Return `True` if `a` is a Z3 bit-vector expression.
03392     
03393     >>> b = BitVec('b', 32)
03394     >>> is_bv(b)
03395     True
03396     >>> is_bv(b + 10)
03397     True
03398     >>> is_bv(Int('x'))
03399     False
03400     """
03401     return isinstance(a, BitVecRef)
03402 
03403 def is_bv_value(a):
03404     """Return `True` if `a` is a Z3 bit-vector numeral value.
03405 
03406     >>> b = BitVec('b', 32)
03407     >>> is_bv_value(b)
03408     False
03409     >>> b = BitVecVal(10, 32)
03410     >>> b
03411     10
03412     >>> is_bv_value(b)
03413     True
03414     """
03415     return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
03416 
03417 def BV2Int(a):
03418     """Return the Z3 expression BV2Int(a). 
03419     
03420     >>> b = BitVec('b', 3)
03421     >>> BV2Int(b).sort()
03422     Int
03423     >>> x = Int('x')
03424     >>> x > BV2Int(b)
03425     x > BV2Int(b)
03426     >>> solve(x > BV2Int(b), b == 1, x < 3)
03427     [b = 1, x = 2]
03428     """
03429     if __debug__:
03430         _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
03431     ctx = a.ctx
03432     ## investigate problem with bv2int
03433     return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
03434 
03435 def BitVecSort(sz, ctx=None):
03436     """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
03437 
03438     >>> Byte = BitVecSort(8)
03439     >>> Word = BitVecSort(16)
03440     >>> Byte
03441     BitVec(8)
03442     >>> x = Const('x', Byte)
03443     >>> eq(x, BitVec('x', 8))
03444     True
03445     """
03446     ctx = _get_ctx(ctx)
03447     return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
03448 
03449 def BitVecVal(val, bv, ctx=None):
03450     """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
03451     
03452     >>> v = BitVecVal(10, 32)
03453     >>> v
03454     10
03455     >>> print("0x%.8x" % v.as_long())
03456     0x0000000a
03457     """
03458     if is_bv_sort(bv):
03459         ctx = bv.ctx
03460         return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
03461     else:
03462         ctx = _get_ctx(ctx)
03463         return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
03464 
03465 def BitVec(name, bv, ctx=None):
03466     """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
03467     If `ctx=None`, then the global context is used.
03468 
03469     >>> x  = BitVec('x', 16)
03470     >>> is_bv(x)
03471     True
03472     >>> x.size()
03473     16
03474     >>> x.sort()
03475     BitVec(16)
03476     >>> word = BitVecSort(16)
03477     >>> x2 = BitVec('x', word)
03478     >>> eq(x, x2)
03479     True
03480     """
03481     if isinstance(bv, BitVecSortRef):
03482         ctx = bv.ctx
03483     else:
03484         ctx = _get_ctx(ctx)
03485         bv = BitVecSort(bv, ctx)
03486     return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
03487 
03488 def BitVecs(names, bv, ctx=None):
03489     """Return a tuple of bit-vector constants of size bv. 
03490     
03491     >>> x, y, z = BitVecs('x y z', 16)
03492     >>> x.size()
03493     16
03494     >>> x.sort()
03495     BitVec(16)
03496     >>> Sum(x, y, z)
03497     0 + x + y + z
03498     >>> Product(x, y, z)
03499     1*x*y*z
03500     >>> simplify(Product(x, y, z))
03501     x*y*z
03502     """
03503     ctx = _get_ctx(ctx)
03504     if isinstance(names, str):
03505         names = names.split(" ")
03506     return [BitVec(name, bv, ctx) for name in names]
03507 
03508 def Concat(*args):
03509     """Create a Z3 bit-vector concatenation expression. 
03510     
03511     >>> v = BitVecVal(1, 4)
03512     >>> Concat(v, v+1, v)
03513     Concat(Concat(1, 1 + 1), 1)
03514     >>> simplify(Concat(v, v+1, v))
03515     289
03516     >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
03517     121
03518     """
03519     args = _get_args(args)
03520     if __debug__:
03521         _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
03522         _z3_assert(len(args) >= 2, "At least two arguments expected.")
03523     ctx = args[0].ctx
03524     r   = args[0]
03525     for i in range(len(args) - 1):
03526         r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
03527     return r
03528 
03529 def Extract(high, low, a):
03530     """Create a Z3 bit-vector extraction expression.
03531 
03532     >>> x = BitVec('x', 8)
03533     >>> Extract(6, 2, x)
03534     Extract(6, 2, x)
03535     >>> Extract(6, 2, x).sort()
03536     BitVec(5)
03537     """
03538     if __debug__:
03539         _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
03540         _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
03541         _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
03542     return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
03543 
03544 def _check_bv_args(a, b):
03545     if __debug__:
03546         _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression")
03547 
03548 def ULE(a, b):
03549     """Create the Z3 expression (unsigned) `other <= self`.
03550     
03551     Use the operator <= for signed less than or equal to.
03552     
03553     >>> x, y = BitVecs('x y', 32)
03554     >>> ULE(x, y)
03555     ULE(x, y)
03556     >>> (x <= y).sexpr()
03557     '(bvsle x y)'
03558     >>> ULE(x, y).sexpr()
03559     '(bvule x y)'
03560     """
03561     _check_bv_args(a, b)
03562     a, b = _coerce_exprs(a, b)
03563     return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03564 
03565 def ULT(a, b):
03566     """Create the Z3 expression (unsigned) `other < self`.
03567     
03568     Use the operator < for signed less than.
03569     
03570     >>> x, y = BitVecs('x y', 32)
03571     >>> ULT(x, y)
03572     ULT(x, y)
03573     >>> (x < y).sexpr()
03574     '(bvslt x y)'
03575     >>> ULT(x, y).sexpr()
03576     '(bvult x y)'
03577     """
03578     _check_bv_args(a, b)
03579     a, b = _coerce_exprs(a, b)
03580     return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03581 
03582 def UGE(a, b):
03583     """Create the Z3 expression (unsigned) `other >= self`.
03584     
03585     Use the operator >= for signed greater than or equal to.
03586     
03587     >>> x, y = BitVecs('x y', 32)
03588     >>> UGE(x, y)
03589     UGE(x, y)
03590     >>> (x >= y).sexpr()
03591     '(bvsge x y)'
03592     >>> UGE(x, y).sexpr()
03593     '(bvuge x y)'
03594     """
03595     _check_bv_args(a, b)
03596     a, b = _coerce_exprs(a, b)
03597     return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03598 
03599 def UGT(a, b):
03600     """Create the Z3 expression (unsigned) `other > self`.
03601     
03602     Use the operator > for signed greater than.
03603     
03604     >>> x, y = BitVecs('x y', 32)
03605     >>> UGT(x, y)
03606     UGT(x, y)
03607     >>> (x > y).sexpr()
03608     '(bvsgt x y)'
03609     >>> UGT(x, y).sexpr()
03610     '(bvugt x y)'
03611     """
03612     _check_bv_args(a, b)
03613     a, b = _coerce_exprs(a, b)
03614     return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03615 
03616 def UDiv(a, b):
03617     """Create the Z3 expression (unsigned) division `self / other`.
03618     
03619     Use the operator / for signed division.
03620     
03621     >>> x = BitVec('x', 32)
03622     >>> y = BitVec('y', 32)
03623     >>> UDiv(x, y)
03624     UDiv(x, y)
03625     >>> UDiv(x, y).sort()
03626     BitVec(32)
03627     >>> (x / y).sexpr()
03628     '(bvsdiv x y)'
03629     >>> UDiv(x, y).sexpr()
03630     '(bvudiv x y)'
03631     """
03632     _check_bv_args(a, b)
03633     a, b = _coerce_exprs(a, b)
03634     return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03635 
03636 def URem(a, b):
03637     """Create the Z3 expression (unsigned) remainder `self % other`.
03638     
03639     Use the operator % for signed modulus, and SRem() for signed remainder.
03640     
03641     >>> x = BitVec('x', 32)
03642     >>> y = BitVec('y', 32)
03643     >>> URem(x, y)
03644     URem(x, y)
03645     >>> URem(x, y).sort()
03646     BitVec(32)
03647     >>> (x % y).sexpr()
03648     '(bvsmod x y)'
03649     >>> URem(x, y).sexpr()
03650     '(bvurem x y)'
03651     """
03652     _check_bv_args(a, b)
03653     a, b = _coerce_exprs(a, b)
03654     return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03655 
03656 def SRem(a, b):
03657     """Create the Z3 expression signed remainder.
03658     
03659     Use the operator % for signed modulus, and URem() for unsigned remainder.
03660     
03661     >>> x = BitVec('x', 32)
03662     >>> y = BitVec('y', 32)
03663     >>> SRem(x, y)
03664     SRem(x, y)
03665     >>> SRem(x, y).sort()
03666     BitVec(32)
03667     >>> (x % y).sexpr()
03668     '(bvsmod x y)'
03669     >>> SRem(x, y).sexpr()
03670     '(bvsrem x y)'
03671     """
03672     _check_bv_args(a, b)
03673     a, b = _coerce_exprs(a, b)
03674     return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03675 
03676 def LShR(a, b):
03677     """Create the Z3 expression logical right shift.
03678 
03679     Use the operator >> for the arithmetical right shift.
03680 
03681     >>> x, y = BitVecs('x y', 32)
03682     >>> LShR(x, y)
03683     LShR(x, y)
03684     >>> (x >> y).sexpr()
03685     '(bvashr x y)'
03686     >>> LShR(x, y).sexpr()
03687     '(bvlshr x y)'
03688     >>> BitVecVal(4, 3)
03689     4
03690     >>> BitVecVal(4, 3).as_signed_long()
03691     -4
03692     >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
03693     -2
03694     >>> simplify(BitVecVal(4, 3) >> 1)
03695     6
03696     >>> simplify(LShR(BitVecVal(4, 3), 1))
03697     2
03698     >>> simplify(BitVecVal(2, 3) >> 1)
03699     1
03700     >>> simplify(LShR(BitVecVal(2, 3), 1))
03701     1
03702     """
03703     _check_bv_args(a, b)
03704     a, b = _coerce_exprs(a, b)
03705     return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03706 
03707 def RotateLeft(a, b):
03708     """Return an expression representing `a` rotated to the left `b` times.
03709 
03710     >>> a, b = BitVecs('a b', 16)
03711     >>> RotateLeft(a, b)
03712     RotateLeft(a, b)
03713     >>> simplify(RotateLeft(a, 0))
03714     a
03715     >>> simplify(RotateLeft(a, 16))
03716     a
03717     """
03718     _check_bv_args(a, b)
03719     a, b = _coerce_exprs(a, b)
03720     return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03721 
03722 def RotateRight(a, b):
03723     """Return an expression representing `a` rotated to the right `b` times.
03724 
03725     >>> a, b = BitVecs('a b', 16)
03726     >>> RotateRight(a, b)
03727     RotateRight(a, b)
03728     >>> simplify(RotateRight(a, 0))
03729     a
03730     >>> simplify(RotateRight(a, 16))
03731     a
03732     """
03733     _check_bv_args(a, b)
03734     a, b = _coerce_exprs(a, b)
03735     return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03736 
03737 def SignExt(n, a):
03738     """Return a bit-vector expression with `n` extra sign-bits.
03739 
03740     >>> x = BitVec('x', 16)
03741     >>> n = SignExt(8, x)
03742     >>> n.size()
03743     24
03744     >>> n
03745     SignExt(8, x)
03746     >>> n.sort()
03747     BitVec(24)
03748     >>> v0 = BitVecVal(2, 2)
03749     >>> v0
03750     2
03751     >>> v0.size()
03752     2
03753     >>> v  = simplify(SignExt(6, v0))
03754     >>> v
03755     254
03756     >>> v.size()
03757     8
03758     >>> print("%.x" % v.as_long())
03759     fe
03760     """
03761     if __debug__:
03762         _z3_assert(isinstance(n, int), "First argument must be an integer")
03763         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03764     return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
03765 
03766 def ZeroExt(n, a):
03767     """Return a bit-vector expression with `n` extra zero-bits.
03768 
03769     >>> x = BitVec('x', 16)
03770     >>> n = ZeroExt(8, x)
03771     >>> n.size()
03772     24
03773     >>> n
03774     ZeroExt(8, x)
03775     >>> n.sort()
03776     BitVec(24)
03777     >>> v0 = BitVecVal(2, 2)
03778     >>> v0
03779     2
03780     >>> v0.size()
03781     2
03782     >>> v  = simplify(ZeroExt(6, v0))
03783     >>> v
03784     2
03785     >>> v.size()
03786     8
03787     """
03788     if __debug__:
03789         _z3_assert(isinstance(n, int), "First argument must be an integer")
03790         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03791     return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
03792 
03793 def RepeatBitVec(n, a):
03794     """Return an expression representing `n` copies of `a`.
03795 
03796     >>> x = BitVec('x', 8)
03797     >>> n = RepeatBitVec(4, x)
03798     >>> n
03799     RepeatBitVec(4, x)
03800     >>> n.size()
03801     32
03802     >>> v0 = BitVecVal(10, 4)
03803     >>> print("%.x" % v0.as_long())
03804     a
03805     >>> v = simplify(RepeatBitVec(4, v0))
03806     >>> v.size()
03807     16
03808     >>> print("%.x" % v.as_long())
03809     aaaa
03810     """
03811     if __debug__:
03812         _z3_assert(isinstance(n, int), "First argument must be an integer")
03813         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03814     return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
03815 
03816 #########################################
03817 #
03818 # Arrays
03819 #
03820 #########################################
03821 
03822 class ArraySortRef(SortRef):
03823     """Array sorts."""
03824 
03825     def domain(self):
03826         """Return the domain of the array sort `self`.
03827         
03828         >>> A = ArraySort(IntSort(), BoolSort())
03829         >>> A.domain()
03830         Int
03831         """
03832         return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx)
03833     
03834     def range(self):
03835         """Return the range of the array sort `self`.
03836         
03837         >>> A = ArraySort(IntSort(), BoolSort())
03838         >>> A.range()
03839         Bool
03840         """
03841         return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
03842 
03843 class ArrayRef(ExprRef):
03844     """Array expressions. """
03845 
03846     def sort(self):
03847         """Return the array sort of the array expression `self`.
03848 
03849         >>> a = Array('a', IntSort(), BoolSort())
03850         >>> a.sort()
03851         Array(Int, Bool)
03852         """
03853         return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
03854     
03855     def domain(self):
03856         """Shorthand for `self.sort().domain()`.
03857 
03858         >>> a = Array('a', IntSort(), BoolSort())
03859         >>> a.domain()
03860         Int
03861         """
03862         return self.sort().domain()
03863         
03864     def range(self):
03865         """Shorthand for `self.sort().range()`.
03866 
03867         >>> a = Array('a', IntSort(), BoolSort())
03868         >>> a.range()
03869         Bool
03870         """
03871         return self.sort().range()
03872 
03873     def __getitem__(self, arg):
03874         """Return the Z3 expression `self[arg]`.
03875 
03876         >>> a = Array('a', IntSort(), BoolSort())
03877         >>> i = Int('i')
03878         >>> a[i]
03879         a[i]
03880         >>> a[i].sexpr()
03881         '(select a i)'
03882         """
03883         arg = self.domain().cast(arg)
03884         return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
03885 
03886 def is_array(a):
03887     """Return `True` if `a` is a Z3 array expression.
03888     
03889     >>> a = Array('a', IntSort(), IntSort())
03890     >>> is_array(a)
03891     True
03892     >>> is_array(Store(a, 0, 1))
03893     True
03894     >>> is_array(a[0])
03895     False
03896     """
03897     return isinstance(a, ArrayRef)
03898 
03899 def is_const_array(a):
03900     """Return `True` if `a` is a Z3 constant array.
03901 
03902     >>> a = K(IntSort(), 10)
03903     >>> is_const_array(a)
03904     True
03905     >>> a = Array('a', IntSort(), IntSort())
03906     >>> is_const_array(a)
03907     False
03908     """
03909     return is_app_of(a, Z3_OP_CONST_ARRAY)
03910 
03911 def is_K(a):
03912     """Return `True` if `a` is a Z3 constant array.
03913 
03914     >>> a = K(IntSort(), 10)
03915     >>> is_K(a)
03916     True
03917     >>> a = Array('a', IntSort(), IntSort())
03918     >>> is_K(a)
03919     False
03920     """
03921     return is_app_of(a, Z3_OP_CONST_ARRAY)
03922 
03923 def is_map(a):
03924     """Return `True` if `a` is a Z3 map array expression. 
03925 
03926     >>> f = Function('f', IntSort(), IntSort())
03927     >>> b = Array('b', IntSort(), IntSort())
03928     >>> a  = Map(f, b)
03929     >>> a
03930     Map(f, b)
03931     >>> is_map(a)
03932     True
03933     >>> is_map(b)
03934     False
03935     """
03936     return is_app_of(a, Z3_OP_ARRAY_MAP)
03937 
03938 def get_map_func(a):
03939     """Return the function declaration associated with a Z3 map array expression.
03940 
03941     >>> f = Function('f', IntSort(), IntSort())
03942     >>> b = Array('b', IntSort(), IntSort())
03943     >>> a  = Map(f, b)
03944     >>> eq(f, get_map_func(a))
03945     True
03946     >>> get_map_func(a)
03947     f
03948     >>> get_map_func(a)(0)
03949     f(0)
03950     """
03951     if __debug__:
03952         _z3_assert(is_map(a), "Z3 array map expression expected.")
03953     return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
03954 
03955 def ArraySort(d, r):
03956     """Return the Z3 array sort with the given domain and range sorts.
03957     
03958     >>> A = ArraySort(IntSort(), BoolSort())
03959     >>> A
03960     Array(Int, Bool)
03961     >>> A.domain()
03962     Int
03963     >>> A.range()
03964     Bool
03965     >>> AA = ArraySort(IntSort(), A)
03966     >>> AA
03967     Array(Int, Array(Int, Bool))
03968     """
03969     if __debug__:
03970         _z3_assert(is_sort(d), "Z3 sort expected")
03971         _z3_assert(is_sort(r), "Z3 sort expected")
03972         _z3_assert(d.ctx == r.ctx, "Context mismatch")
03973     ctx = d.ctx
03974     return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
03975 
03976 def Array(name, dom, rng):
03977     """Return an array constant named `name` with the given domain and range sorts.
03978 
03979     >>> a = Array('a', IntSort(), IntSort())
03980     >>> a.sort()
03981     Array(Int, Int)
03982     >>> a[0]
03983     a[0]
03984     """
03985     s = ArraySort(dom, rng)
03986     ctx = s.ctx
03987     return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
03988 
03989 def Update(a, i, v):
03990     """Return a Z3 store array expression.
03991 
03992     >>> a    = Array('a', IntSort(), IntSort())
03993     >>> i, v = Ints('i v')
03994     >>> s    = Update(a, i, v)
03995     >>> s.sort()
03996     Array(Int, Int)
03997     >>> prove(s[i] == v)
03998     proved
03999     >>> j    = Int('j')
04000     >>> prove(Implies(i != j, s[j] == a[j]))
04001     proved
04002     """
04003     if __debug__:
04004         _z3_assert(is_array(a), "First argument must be a Z3 array expression")
04005     i = a.domain().cast(i)
04006     v = a.range().cast(v)
04007     ctx = a.ctx
04008     return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
04009 
04010 def Store(a, i, v):
04011     """Return a Z3 store array expression.
04012 
04013     >>> a    = Array('a', IntSort(), IntSort())
04014     >>> i, v = Ints('i v')
04015     >>> s    = Store(a, i, v)
04016     >>> s.sort()
04017     Array(Int, Int)
04018     >>> prove(s[i] == v)
04019     proved
04020     >>> j    = Int('j')
04021     >>> prove(Implies(i != j, s[j] == a[j]))
04022     proved
04023     """
04024     return Update(a, i, v)
04025 
04026 def Select(a, i):
04027     """Return a Z3 select array expression.
04028 
04029     >>> a = Array('a', IntSort(), IntSort())
04030     >>> i = Int('i')
04031     >>> Select(a, i)
04032     a[i]
04033     >>> eq(Select(a, i), a[i])
04034     True
04035     """
04036     if __debug__:
04037         _z3_assert(is_array(a), "First argument must be a Z3 array expression")
04038     return a[i]
04039 
04040 def Map(f, *args):
04041     """Return a Z3 map array expression. 
04042 
04043     >>> f = Function('f', IntSort(), IntSort(), IntSort())
04044     >>> a1 = Array('a1', IntSort(), IntSort())
04045     >>> a2 = Array('a2', IntSort(), IntSort())
04046     >>> b  = Map(f, a1, a2)
04047     >>> b
04048     Map(f, a1, a2)
04049     >>> prove(b[0] == f(a1[0], a2[0]))
04050     proved
04051     """
04052     args = _get_args(args)
04053     if __debug__:
04054         _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
04055         _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
04056         _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
04057         _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
04058     _args, sz = _to_ast_array(args)
04059     ctx = f.ctx
04060     return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
04061 
04062 def K(dom, v):
04063     """Return a Z3 constant array expression. 
04064     
04065     >>> a = K(IntSort(), 10)
04066     >>> a
04067     K(Int, 10)
04068     >>> a.sort()
04069     Array(Int, Int)
04070     >>> i = Int('i')
04071     >>> a[i]
04072     K(Int, 10)[i]
04073     >>> simplify(a[i])
04074     10
04075     """
04076     if __debug__:
04077         _z3_assert(is_sort(dom), "Z3 sort expected")
04078     ctx = dom.ctx
04079     if not is_expr(v):
04080         v = _py2expr(v, ctx)
04081     return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
04082 
04083 def is_select(a):
04084     """Return `True` if `a` is a Z3 array select application.
04085     
04086     >>> a = Array('a', IntSort(), IntSort())
04087     >>> is_select(a)
04088     False
04089     >>> i = Int('i')
04090     >>> is_select(a[i])
04091     True
04092     """
04093     return is_app_of(a, Z3_OP_SELECT)
04094 
04095 def is_store(a):
04096     """Return `True` if `a` is a Z3 array store application.
04097     
04098     >>> a = Array('a', IntSort(), IntSort())
04099     >>> is_store(a)
04100     False
04101     >>> is_store(Store(a, 0, 1))
04102     True
04103     """
04104     return is_app_of(a, Z3_OP_STORE)
04105 
04106 #########################################
04107 #
04108 # Datatypes
04109 #
04110 #########################################
04111 
04112 def _valid_accessor(acc):
04113     """Return `True` if acc is pair of the form (String, Datatype or Sort). """
04114     return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
04115 
04116 class Datatype:
04117     """Helper class for declaring Z3 datatypes. 
04118 
04119     >>> List = Datatype('List')
04120     >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04121     >>> List.declare('nil')
04122     >>> List = List.create()
04123     >>> # List is now a Z3 declaration
04124     >>> List.nil
04125     nil
04126     >>> List.cons(10, List.nil)
04127     cons(10, nil)
04128     >>> List.cons(10, List.nil).sort()
04129     List
04130     >>> cons = List.cons
04131     >>> nil  = List.nil
04132     >>> car  = List.car
04133     >>> cdr  = List.cdr
04134     >>> n = cons(1, cons(0, nil))
04135     >>> n
04136     cons(1, cons(0, nil))
04137     >>> simplify(cdr(n))
04138     cons(0, nil)
04139     >>> simplify(car(n))
04140     1
04141     """
04142     def __init__(self, name, ctx=None):
04143         self.ctx          = _get_ctx(ctx)
04144         self.name         = name
04145         self.constructors = []
04146 
04147     def declare_core(self, name, rec_name, *args):
04148         if __debug__:
04149             _z3_assert(isinstance(name, str), "String expected")
04150             _z3_assert(isinstance(rec_name, str), "String expected")
04151             _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)")
04152         self.constructors.append((name, rec_name, args))
04153 
04154     def declare(self, name, *args):
04155         """Declare constructor named `name` with the given accessors `args`. 
04156         Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared. 
04157 
04158         In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))` 
04159         declares the constructor named `cons` that builds a new List using an integer and a List. 
04160         It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell, 
04161         and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create 
04162         the actual datatype in Z3.
04163         
04164         >>> List = Datatype('List')
04165         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04166         >>> List.declare('nil')
04167         >>> List = List.create()
04168         """
04169         if __debug__:
04170             _z3_assert(isinstance(name, str), "String expected")
04171             _z3_assert(name != "", "Constructor name cannot be empty")
04172         return self.declare_core(name, "is_" + name, *args)
04173 
04174     def __repr__(self):
04175         return "Datatype(%s, %s)" % (self.name, self.constructors)
04176 
04177     def create(self):
04178         """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
04179         
04180         The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
04181 
04182         >>> List = Datatype('List')
04183         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04184         >>> List.declare('nil')
04185         >>> List = List.create()
04186         >>> List.nil
04187         nil
04188         >>> List.cons(10, List.nil)
04189         cons(10, nil)
04190         """
04191         return CreateDatatypes([self])[0]
04192 
04193 class ScopedConstructor:
04194     """Auxiliary object used to create Z3 datatypes."""
04195     def __init__(self, c, ctx):
04196         self.c   = c
04197         self.ctx = ctx
04198     def __del__(self):
04199         Z3_del_constructor(self.ctx.ref(), self.c)
04200 
04201 class ScopedConstructorList:
04202     """Auxiliary object used to create Z3 datatypes."""
04203     def __init__(self, c, ctx):
04204         self.c   = c
04205         self.ctx = ctx
04206     def __del__(self):
04207         Z3_del_constructor_list(self.ctx.ref(), self.c)
04208 
04209 def CreateDatatypes(*ds):
04210     """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
04211     
04212     In the following example we define a Tree-List using two mutually recursive datatypes.
04213 
04214     >>> TreeList = Datatype('TreeList')
04215     >>> Tree     = Datatype('Tree')
04216     >>> # Tree has two constructors: leaf and node
04217     >>> Tree.declare('leaf', ('val', IntSort()))
04218     >>> # a node contains a list of trees
04219     >>> Tree.declare('node', ('children', TreeList))
04220     >>> TreeList.declare('nil')
04221     >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
04222     >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
04223     >>> Tree.val(Tree.leaf(10))
04224     val(leaf(10))
04225     >>> simplify(Tree.val(Tree.leaf(10)))
04226     10
04227     >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
04228     >>> n1
04229     node(cons(leaf(10), cons(leaf(20), nil)))
04230     >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
04231     >>> simplify(n2 == n1)
04232     False
04233     >>> simplify(TreeList.car(Tree.children(n2)) == n1)
04234     True
04235     """
04236     ds = _get_args(ds)
04237     if __debug__:
04238         _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
04239         _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
04240         _z3_assert(all([d.ctx == ds[0].ctx for d in  ds]), "Context mismatch")
04241         _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
04242     ctx = ds[0].ctx
04243     num    = len(ds)
04244     names  = (Symbol * num)()
04245     out    = (Sort * num)()
04246     clists = (ConstructorList * num)()
04247     to_delete = []
04248     for i in range(num):
04249         d        = ds[i]
04250         names[i] = to_symbol(d.name, ctx)
04251         num_cs   = len(d.constructors)
04252         cs       = (Constructor * num_cs)()
04253         for j in range(num_cs):
04254             c      = d.constructors[j]
04255             cname  = to_symbol(c[0], ctx)
04256             rname  = to_symbol(c[1], ctx)
04257             fs     = c[2]
04258             num_fs = len(fs)
04259             fnames = (Symbol * num_fs)()
04260             sorts  = (Sort   * num_fs)()
04261             refs   = (ctypes.c_uint * num_fs)()
04262             for k in range(num_fs):
04263                 fname = fs[k][0]
04264                 ftype = fs[k][1]
04265                 fnames[k] = to_symbol(fname, ctx)
04266                 if isinstance(ftype, Datatype):
04267                     if __debug__:
04268                         _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
04269                     sorts[k] = None
04270                     refs[k]  = ds.index(ftype)
04271                 else:
04272                     if __debug__:
04273                         _z3_assert(is_sort(ftype), "Z3 sort expected")
04274                     sorts[k] = ftype.ast
04275                     refs[k]  = 0
04276             cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
04277             to_delete.append(ScopedConstructor(cs[j], ctx))
04278         clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
04279         to_delete.append(ScopedConstructorList(clists[i], ctx))
04280     Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
04281     result = []
04282     ## Create a field for every constructor, recognizer and accessor
04283     for i in range(num):
04284         dref = DatatypeSortRef(out[i], ctx)
04285         num_cs = dref.num_constructors()
04286         for j in range(num_cs):
04287             cref       = dref.constructor(j)
04288             cref_name  = cref.name()
04289             cref_arity = cref.arity()
04290             if cref.arity() == 0:
04291                 cref = cref()
04292             setattr(dref, cref_name, cref)
04293             rref  = dref.recognizer(j)
04294             setattr(dref, rref.name(), rref)
04295             for k in range(cref_arity):
04296                 aref = dref.accessor(j, k)
04297                 setattr(dref, aref.name(), aref)
04298         result.append(dref)
04299     return tuple(result)
04300 
04301 class DatatypeSortRef(SortRef):
04302     """Datatype sorts."""
04303     def num_constructors(self):
04304         """Return the number of constructors in the given Z3 datatype. 
04305         
04306         >>> List = Datatype('List')
04307         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04308         >>> List.declare('nil')
04309         >>> List = List.create()
04310         >>> # List is now a Z3 declaration
04311         >>> List.num_constructors()
04312         2
04313         """
04314         return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
04315 
04316     def constructor(self, idx):
04317         """Return a constructor of the datatype `self`.
04318 
04319         >>> List = Datatype('List')
04320         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04321         >>> List.declare('nil')
04322         >>> List = List.create()
04323         >>> # List is now a Z3 declaration
04324         >>> List.num_constructors()
04325         2
04326         >>> List.constructor(0)
04327         cons
04328         >>> List.constructor(1)
04329         nil
04330         """
04331         if __debug__:
04332             _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
04333         return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
04334     
04335     def recognizer(self, idx):
04336         """In Z3, each constructor has an associated recognizer predicate. 
04337 
04338         If the constructor is named `name`, then the recognizer `is_name`.
04339         
04340         >>> List = Datatype('List')
04341         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04342         >>> List.declare('nil')
04343         >>> List = List.create()
04344         >>> # List is now a Z3 declaration
04345         >>> List.num_constructors()
04346         2
04347         >>> List.recognizer(0)
04348         is_cons
04349         >>> List.recognizer(1)
04350         is_nil
04351         >>> simplify(List.is_nil(List.cons(10, List.nil)))
04352         False
04353         >>> simplify(List.is_cons(List.cons(10, List.nil)))
04354         True
04355         >>> l = Const('l', List)
04356         >>> simplify(List.is_cons(l))
04357         is_cons(l)
04358         """
04359         if __debug__:
04360             _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
04361         return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
04362 
04363     def accessor(self, i, j):
04364         """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
04365         
04366         >>> List = Datatype('List')
04367         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04368         >>> List.declare('nil')
04369         >>> List = List.create()
04370         >>> List.num_constructors()
04371         2
04372         >>> List.constructor(0)
04373         cons
04374         >>> num_accs = List.constructor(0).arity()
04375         >>> num_accs
04376         2
04377         >>> List.accessor(0, 0)
04378         car
04379         >>> List.accessor(0, 1)
04380         cdr
04381         >>> List.constructor(1)
04382         nil
04383         >>> num_accs = List.constructor(1).arity()
04384         >>> num_accs
04385         0
04386         """
04387         if __debug__:
04388             _z3_assert(i < self.num_constructors(), "Invalid constructor index")
04389             _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
04390         return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
04391 
04392 class DatatypeRef(ExprRef):
04393     """Datatype expressions."""
04394     def sort(self):
04395         """Return the datatype sort of the datatype expression `self`."""
04396         return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
04397 
04398 def EnumSort(name, values, ctx=None):
04399     """Return a new enumeration sort named `name` containing the given values.
04400 
04401     The result is a pair (sort, list of constants).
04402     Example:
04403         >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
04404     """
04405     if __debug__:
04406         _z3_assert(isinstance(name, str), "Name must be a string")
04407         _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
04408         _z3_assert(len(values) > 0, "At least one value expected")
04409     ctx = _get_ctx(ctx)
04410     num = len(values)
04411     _val_names   = (Symbol * num)()
04412     for i in range(num):
04413         _val_names[i] = to_symbol(values[i])
04414     _values  = (FuncDecl * num)()
04415     _testers = (FuncDecl * num)() 
04416     name = to_symbol(name)
04417     S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
04418     V = []
04419     for i in range(num):
04420         V.append(FuncDeclRef(_values[i], ctx))
04421     V = [a() for a in V]
04422     return S, V
04423 
04424 #########################################
04425 #
04426 # Parameter Sets
04427 #
04428 #########################################
04429 
04430 class ParamsRef:
04431     """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
04432     
04433     Consider using the function `args2params` to create instances of this object.
04434     """
04435     def __init__(self, ctx=None):
04436         self.ctx    = _get_ctx(ctx)
04437         self.params = Z3_mk_params(self.ctx.ref())
04438         Z3_params_inc_ref(self.ctx.ref(), self.params)
04439 
04440     def __del__(self):
04441         Z3_params_dec_ref(self.ctx.ref(), self.params)
04442 
04443     def set(self, name, val):
04444         """Set parameter name with value val."""
04445         if __debug__:
04446             _z3_assert(isinstance(name, str), "parameter name must be a string")
04447         name_sym = to_symbol(name, self.ctx)
04448         if isinstance(val, bool):
04449             Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
04450         elif isinstance(val, int):
04451             Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
04452         elif isinstance(val, float):
04453             Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
04454         elif isinstance(val, str):
04455             Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx))
04456         else:
04457             if __debug__:
04458                 _z3_assert(False, "invalid parameter value")
04459 
04460     def __repr__(self):
04461         return Z3_params_to_string(self.ctx.ref(), self.params)
04462 
04463     def validate(self, ds):
04464         _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
04465         Z3_params_validate(self.ctx.ref(), self.params, ds.descr)
04466 
04467 def args2params(arguments, keywords, ctx=None):
04468     """Convert python arguments into a Z3_params object.
04469     A ':' is added to the keywords, and '_' is replaced with '-'
04470 
04471     >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
04472     (params model true relevancy 2 elim_and true)
04473     """
04474     if __debug__:
04475         _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
04476     prev = None
04477     r    = ParamsRef(ctx)
04478     for a in arguments:
04479         if prev == None:
04480             prev = a
04481         else:
04482             r.set(prev, a)
04483             prev = None
04484     for k in keywords:
04485         v = keywords[k]
04486         r.set(k, v)
04487     return r
04488 
04489 class ParamDescrsRef:
04490     """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
04491     """
04492     def __init__(self, descr, ctx=None):
04493         _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
04494         self.ctx    = _get_ctx(ctx)
04495         self.descr  = descr
04496         Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
04497 
04498     def __del__(self):
04499         Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
04500 
04501     def size(self):
04502         """Return the size of in the parameter description `self`.
04503         """
04504         return int(Z3_param_descrs_size(self.ctx.ref(), self.descr))
04505 
04506     def __len__(self):
04507         """Return the size of in the parameter description `self`.
04508         """
04509         return self.size()
04510 
04511     def get_name(self, i):
04512         """Return the i-th parameter name in the parameter description `self`.
04513         """
04514         return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i))
04515     
04516     def get_kind(self, n):
04517         """Return the kind of the parameter named `n`.
04518         """
04519         return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
04520     
04521     def __getitem__(self, arg):
04522         if _is_int(arg):
04523             return self.get_name(arg)
04524         else:
04525             return self.get_kind(arg)
04526 
04527     def __repr__(self):
04528         return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
04529 
04530 #########################################
04531 #
04532 # Goals
04533 #
04534 #########################################
04535 
04536 class Goal(Z3PPObject):
04537     """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
04538     
04539     Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
04540     A goal has a solution if one of its subgoals has a solution.
04541     A goal is unsatisfiable if all subgoals are unsatisfiable.
04542     """
04543 
04544     def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
04545         if __debug__:
04546             _z3_assert(goal == None or ctx != None, "If goal is different from None, then ctx must be also different from None")
04547         self.ctx    = _get_ctx(ctx)
04548         self.goal   = goal
04549         if self.goal == None:
04550             self.goal   = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
04551         Z3_goal_inc_ref(self.ctx.ref(), self.goal)
04552 
04553     def __del__(self):
04554         if self.goal != None:
04555             Z3_goal_dec_ref(self.ctx.ref(), self.goal)
04556 
04557     def depth(self):
04558         """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
04559 
04560         >>> x, y = Ints('x y')
04561         >>> g = Goal()
04562         >>> g.add(x == 0, y >= x + 1)
04563         >>> g.depth()
04564         0
04565         >>> r = Then('simplify', 'solve-eqs')(g)
04566         >>> # r has 1 subgoal
04567         >>> len(r)
04568         1
04569         >>> r[0].depth()
04570         2
04571         """
04572         return int(Z3_goal_depth(self.ctx.ref(), self.goal))
04573 
04574     def inconsistent(self):
04575         """Return `True` if `self` contains the `False` constraints.
04576         
04577         >>> x, y = Ints('x y')
04578         >>> g = Goal()
04579         >>> g.inconsistent()
04580         False
04581         >>> g.add(x == 0, x == 1)
04582         >>> g 
04583         [x == 0, x == 1]
04584         >>> g.inconsistent()
04585         False
04586         >>> g2 = Tactic('propagate-values')(g)[0]
04587         >>> g2.inconsistent()
04588         True
04589         """
04590         return Z3_goal_inconsistent(self.ctx.ref(), self.goal)
04591 
04592     def prec(self):
04593         """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
04594         
04595         >>> g = Goal()
04596         >>> g.prec() == Z3_GOAL_PRECISE
04597         True
04598         >>> x, y = Ints('x y')
04599         >>> g.add(x == y + 1)
04600         >>> g.prec() == Z3_GOAL_PRECISE
04601         True
04602         >>> t  = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
04603         >>> g2 = t(g)[0]
04604         >>> g2
04605         [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
04606         >>> g2.prec() == Z3_GOAL_PRECISE
04607         False
04608         >>> g2.prec() == Z3_GOAL_UNDER
04609         True
04610         """
04611         return Z3_goal_precision(self.ctx.ref(), self.goal)
04612 
04613     def precision(self):
04614         """Alias for `prec()`.
04615 
04616         >>> g = Goal()
04617         >>> g.precision() == Z3_GOAL_PRECISE
04618         True
04619         """
04620         return self.prec()
04621 
04622     def size(self):
04623         """Return the number of constraints in the goal `self`.
04624         
04625         >>> g = Goal()
04626         >>> g.size()
04627         0
04628         >>> x, y = Ints('x y')
04629         >>> g.add(x == 0, y > x)
04630         >>> g.size()
04631         2
04632         """
04633         return int(Z3_goal_size(self.ctx.ref(), self.goal))
04634 
04635     def __len__(self):
04636         """Return the number of constraints in the goal `self`.
04637 
04638         >>> g = Goal()
04639         >>> len(g)
04640         0
04641         >>> x, y = Ints('x y')
04642         >>> g.add(x == 0, y > x)
04643         >>> len(g)
04644         2
04645         """
04646         return self.size()
04647 
04648     def get(self, i):
04649         """Return a constraint in the goal `self`.
04650         
04651         >>> g = Goal()
04652         >>> x, y = Ints('x y')
04653         >>> g.add(x == 0, y > x)
04654         >>> g.get(0)
04655         x == 0
04656         >>> g.get(1)
04657         y > x
04658         """
04659         return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx)
04660 
04661     def __getitem__(self, arg):
04662         """Return a constraint in the goal `self`.
04663         
04664         >>> g = Goal()
04665         >>> x, y = Ints('x y')
04666         >>> g.add(x == 0, y > x)
04667         >>> g[0]
04668         x == 0
04669         >>> g[1]
04670         y > x
04671         """
04672         if arg >= len(self):
04673             raise IndexError
04674         return self.get(arg)
04675 
04676     def assert_exprs(self, *args):
04677         """Assert constraints into the goal.
04678         
04679         >>> x = Int('x')
04680         >>> g = Goal()
04681         >>> g.assert_exprs(x > 0, x < 2)
04682         >>> g
04683         [x > 0, x < 2]
04684         """
04685         args = _get_args(args)
04686         s    = BoolSort(self.ctx)
04687         for arg in args:
04688             arg = s.cast(arg)
04689             Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast())
04690 
04691     def append(self, *args):
04692         """Add constraints.
04693         
04694         >>> x = Int('x')
04695         >>> g = Goal()
04696         >>> g.append(x > 0, x < 2)
04697         >>> g
04698         [x > 0, x < 2]
04699         """
04700         self.assert_exprs(*args)
04701         
04702     def insert(self, *args):
04703         """Add constraints.
04704         
04705         >>> x = Int('x')
04706         >>> g = Goal()
04707         >>> g.insert(x > 0, x < 2)
04708         >>> g
04709         [x > 0, x < 2]
04710         """
04711         self.assert_exprs(*args)
04712 
04713     def add(self, *args):
04714         """Add constraints.
04715         
04716         >>> x = Int('x')
04717         >>> g = Goal()
04718         >>> g.add(x > 0, x < 2)
04719         >>> g
04720         [x > 0, x < 2]
04721         """
04722         self.assert_exprs(*args)
04723 
04724     def __repr__(self):
04725         return obj_to_string(self)
04726 
04727     def sexpr(self):
04728         """Return a textual representation of the s-expression representing the goal."""
04729         return Z3_goal_to_string(self.ctx.ref(), self.goal)
04730 
04731     def translate(self, target):
04732         """Copy goal `self` to context `target`.
04733         
04734         >>> x = Int('x')
04735         >>> g = Goal()
04736         >>> g.add(x > 10)
04737         >>> g
04738         [x > 10]
04739         >>> c2 = Context()
04740         >>> g2 = g.translate(c2)
04741         >>> g2
04742         [x > 10]
04743         >>> g.ctx == main_ctx()
04744         True
04745         >>> g2.ctx == c2
04746         True
04747         >>> g2.ctx == main_ctx()
04748         False
04749         """
04750         if __debug__:
04751             _z3_assert(isinstance(target, Context), "target must be a context")
04752         return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)
04753 
04754     def simplify(self, *arguments, **keywords):
04755         """Return a new simplified goal.
04756         
04757         This method is essentially invoking the simplify tactic.
04758         
04759         >>> g = Goal()
04760         >>> x = Int('x')
04761         >>> g.add(x + 1 >= 2)
04762         >>> g
04763         [x + 1 >= 2]
04764         >>> g2 = g.simplify()
04765         >>> g2
04766         [x >= 1]
04767         >>> # g was not modified
04768         >>> g
04769         [x + 1 >= 2]
04770         """
04771         t = Tactic('simplify')
04772         return t.apply(self, *arguments, **keywords)[0]
04773 
04774     def as_expr(self):
04775         """Return goal `self` as a single Z3 expression.
04776         
04777         >>> x = Int('x')
04778         >>> g = Goal()
04779         >>> g.as_expr()
04780         True
04781         >>> g.add(x > 1)
04782         >>> g.as_expr()
04783         x > 1
04784         >>> g.add(x < 10)
04785         >>> g.as_expr()
04786         And(x > 1, x < 10)
04787         """
04788         sz = len(self)
04789         if sz == 0:
04790             return BoolVal(True, self.ctx)
04791         elif sz == 1:
04792             return self.get(0)
04793         else:
04794             return And([ self.get(i) for i in range(len(self)) ])
04795 
04796 #########################################
04797 #
04798 # AST Vector
04799 #
04800 #########################################
04801 class AstVector(Z3PPObject):
04802     """A collection (vector) of ASTs."""
04803 
04804     def __init__(self, v=None, ctx=None):
04805         self.vector = None
04806         if v == None:
04807             self.ctx = _get_ctx(ctx)
04808             self.vector = Z3_mk_ast_vector(self.ctx.ref())
04809         else:
04810             self.vector = v
04811             assert ctx != None
04812             self.ctx    = ctx
04813         Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
04814 
04815     def __del__(self):
04816         if self.vector != None:
04817             Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
04818         
04819     def __len__(self):
04820         """Return the size of the vector `self`.
04821 
04822         >>> A = AstVector()
04823         >>> len(A)
04824         0
04825         >>> A.push(Int('x'))
04826         >>> A.push(Int('x'))
04827         >>> len(A)
04828         2
04829         """
04830         return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
04831 
04832     def __getitem__(self, i):
04833         """Return the AST at position `i`.
04834 
04835         >>> A = AstVector()
04836         >>> A.push(Int('x') + 1)
04837         >>> A.push(Int('y'))
04838         >>> A[0]
04839         x + 1
04840         >>> A[1]
04841         y
04842         """
04843         if i >= self.__len__():
04844             raise IndexError
04845         return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
04846 
04847     def __setitem__(self, i, v):
04848         """Update AST at position `i`.
04849         
04850         >>> A = AstVector()
04851         >>> A.push(Int('x') + 1)
04852         >>> A.push(Int('y'))
04853         >>> A[0]
04854         x + 1
04855         >>> A[0] = Int('x')
04856         >>> A[0]
04857         x
04858         """
04859         if i >= self.__len__():
04860             raise IndexError
04861         Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
04862         
04863     def push(self, v):
04864         """Add `v` in the end of the vector.
04865 
04866         >>> A = AstVector()
04867         >>> len(A)
04868         0
04869         >>> A.push(Int('x'))
04870         >>> len(A)
04871         1
04872         """
04873         Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
04874 
04875     def resize(self, sz):
04876         """Resize the vector to `sz` elements.
04877 
04878         >>> A = AstVector()
04879         >>> A.resize(10)
04880         >>> len(A)
04881         10
04882         >>> for i in range(10): A[i] = Int('x')
04883         >>> A[5]
04884         x
04885         """
04886         Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
04887 
04888     def __contains__(self, item):
04889         """Return `True` if the vector contains `item`.
04890 
04891         >>> x = Int('x')
04892         >>> A = AstVector()
04893         >>> x in A
04894         False
04895         >>> A.push(x)
04896         >>> x in A
04897         True
04898         >>> (x+1) in A
04899         False
04900         >>> A.push(x+1)
04901         >>> (x+1) in A
04902         True
04903         >>> A
04904         [x, x + 1]
04905         """
04906         for elem in self:
04907             if elem.eq(item):
04908                 return True
04909         return False
04910         
04911     def translate(self, other_ctx):
04912         """Copy vector `self` to context `other_ctx`.
04913 
04914         >>> x = Int('x')
04915         >>> A = AstVector()
04916         >>> A.push(x)
04917         >>> c2 = Context()
04918         >>> B = A.translate(c2)
04919         >>> B
04920         [x]
04921         """
04922         return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
04923 
04924     def __repr__(self):
04925         return obj_to_string(self)
04926 
04927     def sexpr(self):
04928         """Return a textual representation of the s-expression representing the vector."""
04929         return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
04930 
04931 #########################################
04932 #
04933 # AST Map
04934 #
04935 #########################################
04936 class AstMap:
04937     """A mapping from ASTs to ASTs."""
04938 
04939     def __init__(self, m=None, ctx=None):
04940         self.map = None
04941         if m == None:
04942             self.ctx = _get_ctx(ctx)
04943             self.map = Z3_mk_ast_map(self.ctx.ref())
04944         else:
04945             self.map = m
04946             assert ctx != None
04947             self.ctx    = ctx
04948         Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
04949 
04950     def __del__(self):
04951         if self.map != None:
04952             Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
04953 
04954     def __len__(self):
04955         """Return the size of the map. 
04956 
04957         >>> M = AstMap()
04958         >>> len(M)
04959         0
04960         >>> x = Int('x')
04961         >>> M[x] = IntVal(1)
04962         >>> len(M)
04963         1
04964         """
04965         return int(Z3_ast_map_size(self.ctx.ref(), self.map))
04966 
04967     def __contains__(self, key):
04968         """Return `True` if the map contains key `key`.
04969 
04970         >>> M = AstMap()
04971         >>> x = Int('x')
04972         >>> M[x] = x + 1
04973         >>> x in M
04974         True
04975         >>> x+1 in M
04976         False
04977         """
04978         return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
04979         
04980     def __getitem__(self, key):
04981         """Retrieve the value associated with key `key`.
04982 
04983         >>> M = AstMap()
04984         >>> x = Int('x')
04985         >>> M[x] = x + 1
04986         >>> M[x]
04987         x + 1
04988         """
04989         return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
04990 
04991     def __setitem__(self, k, v):
04992         """Add/Update key `k` with value `v`.
04993 
04994         >>> M = AstMap()
04995         >>> x = Int('x')
04996         >>> M[x] = x + 1
04997         >>> len(M)
04998         1
04999         >>> M[x]
05000         x + 1
05001         >>> M[x] = IntVal(1)
05002         >>> M[x]
05003         1
05004         """
05005         Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
05006 
05007     def __repr__(self):
05008         return Z3_ast_map_to_string(self.ctx.ref(), self.map)
05009 
05010     def erase(self, k):
05011         """Remove the entry associated with key `k`.
05012 
05013         >>> M = AstMap()
05014         >>> x = Int('x')
05015         >>> M[x] = x + 1
05016         >>> len(M)
05017         1
05018         >>> M.erase(x)
05019         >>> len(M)
05020         0
05021         """
05022         Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
05023 
05024     def reset(self):
05025         """Remove all entries from the map.
05026 
05027         >>> M = AstMap()
05028         >>> x = Int('x')
05029         >>> M[x]   = x + 1
05030         >>> M[x+x] = IntVal(1)
05031         >>> len(M)
05032         2
05033         >>> M.reset()
05034         >>> len(M)
05035         0
05036         """
05037         Z3_ast_map_reset(self.ctx.ref(), self.map)
05038 
05039     def keys(self):
05040         """Return an AstVector containing all keys in the map.
05041 
05042         >>> M = AstMap()
05043         >>> x = Int('x')
05044         >>> M[x]   = x + 1
05045         >>> M[x+x] = IntVal(1)
05046         >>> M.keys()
05047         [x, x + x]
05048         """
05049         return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
05050 
05051 #########################################
05052 #
05053 # Model
05054 #
05055 #########################################
05056 
05057 class FuncEntry:
05058     """Store the value of the interpretation of a function in a particular point."""
05059 
05060     def __init__(self, entry, ctx):
05061         self.entry = entry
05062         self.ctx   = ctx
05063         Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
05064 
05065     def __del__(self):
05066         Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
05067 
05068     def num_args(self):
05069         """Return the number of arguments in the given entry.
05070         
05071         >>> f = Function('f', IntSort(), IntSort(), IntSort())
05072         >>> s = Solver()
05073         >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05074         >>> s.check()
05075         sat
05076         >>> m = s.model()
05077         >>> f_i = m[f]
05078         >>> f_i.num_entries()
05079         3
05080         >>> e = f_i.entry(0)
05081         >>> e.num_args()
05082         2
05083         """
05084         return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
05085 
05086     def arg_value(self, idx):
05087         """Return the value of argument `idx`.
05088         
05089         >>> f = Function('f', IntSort(), IntSort(), IntSort())
05090         >>> s = Solver()
05091         >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05092         >>> s.check()
05093         sat
05094         >>> m = s.model()
05095         >>> f_i = m[f]
05096         >>> f_i.num_entries()
05097         3
05098         >>> e = f_i.entry(0)
05099         >>> e
05100         [0, 1, 10]
05101         >>> e.num_args()
05102         2
05103         >>> e.arg_value(0)
05104         0
05105         >>> e.arg_value(1)
05106         1
05107         >>> try:
05108         ...   e.arg_value(2)
05109         ... except IndexError:
05110         ...   print("index error")
05111         index error
05112         """
05113         if idx >= self.num_args():
05114             raise IndexError
05115         return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
05116 
05117     def value(self):
05118         """Return the value of the function at point `self`.
05119         
05120         >>> f = Function('f', IntSort(), IntSort(), IntSort())
05121         >>> s = Solver()
05122         >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05123         >>> s.check()
05124         sat
05125         >>> m = s.model()
05126         >>> f_i = m[f]
05127         >>> f_i.num_entries()
05128         3
05129         >>> e = f_i.entry(0)
05130         >>> e
05131         [0, 1, 10]
05132         >>> e.num_args()
05133         2
05134         >>> e.value()
05135         10
05136         """
05137         return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
05138     
05139     def as_list(self):
05140         """Return entry `self` as a Python list.
05141         >>> f = Function('f', IntSort(), IntSort(), IntSort())
05142         >>> s = Solver()
05143         >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05144         >>> s.check()
05145         sat
05146         >>> m = s.model()
05147         >>> f_i = m[f]
05148         >>> f_i.num_entries()
05149         3
05150         >>> e = f_i.entry(0)
05151         >>> e.as_list()
05152         [0, 1, 10]
05153         """
05154         args = [ self.arg_value(i) for i in range(self.num_args())]
05155         args.append(self.value())
05156         return args
05157 
05158     def __repr__(self):
05159         return repr(self.as_list())
05160     
05161 class FuncInterp(Z3PPObject):
05162     """Stores the interpretation of a function in a Z3 model."""
05163 
05164     def __init__(self, f, ctx):
05165         self.f   = f
05166         self.ctx = ctx
05167         if self.f != None:
05168             Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
05169 
05170     def __del__(self):
05171         if self.f != None:
05172             Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
05173 
05174     def else_value(self):
05175         """
05176         Return the `else` value for a function interpretation.
05177         Return None if Z3 did not specify the `else` value for
05178         this object.
05179 
05180         >>> f = Function('f', IntSort(), IntSort())
05181         >>> s = Solver()
05182         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05183         >>> s.check()
05184         sat
05185         >>> m = s.model()
05186         >>> m[f]
05187         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05188         >>> m[f].else_value()
05189         1
05190         """
05191         r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
05192         if r:
05193             return _to_expr_ref(r, self.ctx)
05194         else:
05195             return None
05196 
05197     def num_entries(self):
05198         """Return the number of entries/points in the function interpretation `self`.
05199 
05200         >>> f = Function('f', IntSort(), IntSort())
05201         >>> s = Solver()
05202         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05203         >>> s.check()
05204         sat
05205         >>> m = s.model()
05206         >>> m[f]
05207         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05208         >>> m[f].num_entries()
05209         3
05210         """
05211         return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
05212 
05213     def arity(self):
05214         """Return the number of arguments for each entry in the function interpretation `self`.
05215 
05216         >>> f = Function('f', IntSort(), IntSort())
05217         >>> s = Solver()
05218         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05219         >>> s.check()
05220         sat
05221         >>> m = s.model()
05222         >>> m[f].arity()
05223         1
05224         """
05225         return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
05226     
05227     def entry(self, idx):
05228         """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
05229 
05230         >>> f = Function('f', IntSort(), IntSort())
05231         >>> s = Solver()
05232         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05233         >>> s.check()
05234         sat
05235         >>> m = s.model()
05236         >>> m[f]
05237         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05238         >>> m[f].num_entries()
05239         3
05240         >>> m[f].entry(0)
05241         [0, 1]
05242         >>> m[f].entry(1)
05243         [1, 1]
05244         >>> m[f].entry(2)
05245         [2, 0]
05246         """
05247         if idx >= self.num_entries():
05248             raise IndexError
05249         return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
05250     
05251     def as_list(self):
05252         """Return the function interpretation as a Python list.
05253         >>> f = Function('f', IntSort(), IntSort())
05254         >>> s = Solver()
05255         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05256         >>> s.check()
05257         sat
05258         >>> m = s.model()
05259         >>> m[f]
05260         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05261         >>> m[f].as_list()
05262         [[0, 1], [1, 1], [2, 0], 1]
05263         """
05264         r = [ self.entry(i).as_list() for i in range(self.num_entries())]
05265         r.append(self.else_value())
05266         return r
05267 
05268     def __repr__(self):
05269         return obj_to_string(self)
05270 
05271 class ModelRef(Z3PPObject):
05272     """Model/Solution of a satisfiability problem (aka system of constraints)."""
05273 
05274     def __init__(self, m, ctx):
05275         assert ctx != None
05276         self.model = m
05277         self.ctx   = ctx
05278         Z3_model_inc_ref(self.ctx.ref(), self.model)
05279 
05280     def __del__(self):
05281         Z3_model_dec_ref(self.ctx.ref(), self.model)
05282 
05283     def __repr__(self):
05284         return obj_to_string(self)
05285 
05286     def sexpr(self):
05287         """Return a textual representation of the s-expression representing the model."""
05288         return Z3_model_to_string(self.ctx.ref(), self.model)
05289 
05290     def eval(self, t, model_completion=False):
05291         """Evaluate the expression `t` in the model `self`. If `model_completion` is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model `self`.
05292 
05293         >>> x = Int('x')
05294         >>> s = Solver()
05295         >>> s.add(x > 0, x < 2)
05296         >>> s.check()
05297         sat
05298         >>> m = s.model()
05299         >>> m.eval(x + 1)
05300         2
05301         >>> m.eval(x == 1)
05302         True
05303         >>> y = Int('y')
05304         >>> m.eval(y + x)
05305         1 + y
05306         >>> m.eval(y)
05307         y
05308         >>> m.eval(y, model_completion=True)
05309         0
05310         >>> # Now, m contains an interpretation for y
05311         >>> m.eval(y + x)
05312         1
05313         """
05314         r = (Ast * 1)()
05315         if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
05316             return _to_expr_ref(r[0], self.ctx)
05317         raise Z3Exception("failed to evaluate expression in the model")
05318 
05319     def evaluate(self, t, model_completion=False):
05320         """Alias for `eval`.
05321         
05322         >>> x = Int('x')
05323         >>> s = Solver()
05324         >>> s.add(x > 0, x < 2)
05325         >>> s.check()
05326         sat
05327         >>> m = s.model()
05328         >>> m.evaluate(x + 1)
05329         2
05330         >>> m.evaluate(x == 1)
05331         True
05332         >>> y = Int('y')
05333         >>> m.evaluate(y + x)
05334         1 + y
05335         >>> m.evaluate(y)
05336         y
05337         >>> m.evaluate(y, model_completion=True)
05338         0
05339         >>> # Now, m contains an interpretation for y
05340         >>> m.evaluate(y + x)
05341         1
05342         """
05343         return self.eval(t, model_completion)
05344 
05345     def __len__(self):
05346         """Return the number of constant and function declarations in the model `self`.
05347 
05348         >>> f = Function('f', IntSort(), IntSort())
05349         >>> x = Int('x')
05350         >>> s = Solver()
05351         >>> s.add(x > 0, f(x) != x)
05352         >>> s.check()
05353         sat
05354         >>> m = s.model()
05355         >>> len(m)
05356         2
05357         """
05358         return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
05359 
05360     def get_interp(self, decl):
05361         """Return the interpretation for a given declaration or constant.
05362 
05363         >>> f = Function('f', IntSort(), IntSort())
05364         >>> x = Int('x')
05365         >>> s = Solver()
05366         >>> s.add(x > 0, x < 2, f(x) == 0)
05367         >>> s.check()
05368         sat
05369         >>> m = s.model()
05370         >>> m[x]
05371         1
05372         >>> m[f]
05373         [1 -> 0, else -> 0]
05374         """
05375         if __debug__:
05376             _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected")
05377         if is_const(decl):
05378             decl = decl.decl()
05379         try:
05380             if decl.arity() == 0:
05381                 r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
05382                 if is_as_array(r):
05383                     return self.get_interp(get_as_array_func(r))
05384                 else:
05385                     return r
05386             else:
05387                 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
05388         except Z3Exception:
05389             return None
05390 
05391     def num_sorts(self):
05392         """Return the number of unintepreted sorts that contain an interpretation in the model `self`.
05393         
05394         >>> A = DeclareSort('A')
05395         >>> a, b = Consts('a b', A)
05396         >>> s = Solver()
05397         >>> s.add(a != b)
05398         >>> s.check()
05399         sat
05400         >>> m = s.model()
05401         >>> m.num_sorts()
05402         1
05403         """
05404         return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
05405 
05406     def get_sort(self, idx):
05407         """Return the unintepreted sort at position `idx` < self.num_sorts().
05408         
05409         >>> A = DeclareSort('A')
05410         >>> B = DeclareSort('B')
05411         >>> a1, a2 = Consts('a1 a2', A)
05412         >>> b1, b2 = Consts('b1 b2', B)
05413         >>> s = Solver()
05414         >>> s.add(a1 != a2, b1 != b2)
05415         >>> s.check()
05416         sat
05417         >>> m = s.model()
05418         >>> m.num_sorts()
05419         2
05420         >>> m.get_sort(0)
05421         A
05422         >>> m.get_sort(1)
05423         B
05424         """
05425         if idx >= self.num_sorts():
05426             raise IndexError
05427         return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
05428     
05429     def sorts(self):
05430         """Return all uninterpreted sorts that have an interpretation in the model `self`.
05431 
05432         >>> A = DeclareSort('A')
05433         >>> B = DeclareSort('B')
05434         >>> a1, a2 = Consts('a1 a2', A)
05435         >>> b1, b2 = Consts('b1 b2', B)
05436         >>> s = Solver()
05437         >>> s.add(a1 != a2, b1 != b2)
05438         >>> s.check()
05439         sat
05440         >>> m = s.model()
05441         >>> m.sorts()
05442         [A, B]
05443         """
05444         return [ self.get_sort(i) for i in range(self.num_sorts()) ]
05445 
05446     def get_universe(self, s):
05447         """Return the intepretation for the uninterpreted sort `s` in the model `self`.
05448 
05449         >>> A = DeclareSort('A')
05450         >>> a, b = Consts('a b', A)
05451         >>> s = Solver()
05452         >>> s.add(a != b)
05453         >>> s.check()
05454         sat
05455         >>> m = s.model()
05456         >>> m.get_universe(A)
05457         [A!val!0, A!val!1]
05458         """
05459         if __debug__:
05460             _z3_assert(isinstance(s, SortRef), "Z3 sort expected")
05461         try:
05462             return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx)
05463         except Z3Exception:
05464             return None
05465 
05466     def __getitem__(self, idx):
05467         """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned.
05468         
05469         The elements can be retrieved using position or the actual declaration.
05470 
05471         >>> f = Function('f', IntSort(), IntSort())
05472         >>> x = Int('x')
05473         >>> s = Solver()
05474         >>> s.add(x > 0, x < 2, f(x) == 0)
05475         >>> s.check()
05476         sat
05477         >>> m = s.model()
05478         >>> len(m)
05479         2
05480         >>> m[0]
05481         x
05482         >>> m[1]
05483         f
05484         >>> m[x]
05485         1
05486         >>> m[f]
05487         [1 -> 0, else -> 0]
05488         >>> for d in m: print("%s -> %s" % (d, m[d]))
05489         x -> 1
05490         f -> [1 -> 0, else -> 0]
05491         """
05492         if isinstance(idx, int):
05493             if idx >= len(self):
05494                 raise IndexError
05495             num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
05496             if (idx < num_consts):
05497                 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx)
05498             else:
05499                 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx)
05500         if isinstance(idx, FuncDeclRef):
05501             return self.get_interp(idx)
05502         if is_const(idx):
05503             return self.get_interp(idx.decl())
05504         if isinstance(idx, SortRef):
05505             return self.get_universe(idx)
05506         if __debug__:
05507             _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
05508         return None
05509 
05510     def decls(self):
05511         """Return a list with all symbols that have an interpreation in the model `self`.
05512         >>> f = Function('f', IntSort(), IntSort())
05513         >>> x = Int('x')
05514         >>> s = Solver()
05515         >>> s.add(x > 0, x < 2, f(x) == 0)
05516         >>> s.check()
05517         sat
05518         >>> m = s.model()
05519         >>> m.decls()
05520         [x, f]
05521         """
05522         r = []
05523         for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
05524             r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
05525         for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
05526             r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
05527         return r
05528 
05529 def is_as_array(n):
05530     """Return true if n is a Z3 expression of the form (_ as-array f)."""
05531     return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
05532 
05533 def get_as_array_func(n):
05534     """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
05535     if __debug__:
05536         _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
05537     return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
05538 
05539 #########################################
05540 #
05541 # Statistics
05542 #
05543 #########################################
05544 class Statistics:
05545     """Statistics for `Solver.check()`."""
05546 
05547     def __init__(self, stats, ctx):
05548         self.stats = stats
05549         self.ctx   = ctx
05550         Z3_stats_inc_ref(self.ctx.ref(), self.stats)
05551 
05552     def __del__(self):
05553         Z3_stats_dec_ref(self.ctx.ref(), self.stats)
05554 
05555     def __repr__(self):
05556         if in_html_mode():
05557             out = io.StringIO()
05558             even = True
05559             out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
05560             for k, v in self:
05561                 if even:
05562                     out.write(u('<tr style="background-color:#CFCFCF">'))
05563                     even = False
05564                 else:
05565                     out.write(u('<tr>'))
05566                     even = True
05567                 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
05568             out.write(u('</table>'))
05569             return out.getvalue()
05570         else:
05571             return Z3_stats_to_string(self.ctx.ref(), self.stats)
05572 
05573     def __len__(self):
05574         """Return the number of statistical counters. 
05575 
05576         >>> x = Int('x') 
05577         >>> s = Then('simplify', 'nlsat').solver()
05578         >>> s.add(x > 0)
05579         >>> s.check()
05580         sat
05581         >>> st = s.statistics()
05582         >>> len(st)
05583         2
05584         """
05585         return int(Z3_stats_size(self.ctx.ref(), self.stats))
05586 
05587     def __getitem__(self, idx):
05588         """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
05589 
05590         >>> x = Int('x') 
05591         >>> s = Then('simplify', 'nlsat').solver()
05592         >>> s.add(x > 0)
05593         >>> s.check()
05594         sat
05595         >>> st = s.statistics()
05596         >>> len(st)
05597         2
05598         >>> st[0]
05599         ('nlsat propagations', 2)
05600         >>> st[1]
05601         ('nlsat stages', 2)
05602         """
05603         if idx >= len(self):
05604             raise IndexError
05605         if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
05606             val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
05607         else:
05608             val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
05609         return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
05610     
05611     def keys(self):
05612         """Return the list of statistical counters.
05613         
05614         >>> x = Int('x') 
05615         >>> s = Then('simplify', 'nlsat').solver()
05616         >>> s.add(x > 0)
05617         >>> s.check()
05618         sat
05619         >>> st = s.statistics()
05620         >>> st.keys()
05621         ['nlsat propagations', 'nlsat stages']
05622         """
05623         return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
05624 
05625     def get_key_value(self, key):
05626         """Return the value of a particular statistical counter.
05627 
05628         >>> x = Int('x') 
05629         >>> s = Then('simplify', 'nlsat').solver()
05630         >>> s.add(x > 0)
05631         >>> s.check()
05632         sat
05633         >>> st = s.statistics()
05634         >>> st.get_key_value('nlsat propagations')
05635         2
05636         """
05637         for idx in range(len(self)):
05638             if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
05639                 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
05640                     return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
05641                 else:
05642                     return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
05643         raise Z3Exception("unknown key")
05644                
05645     def __getattr__(self, name):
05646         """Access the value of statistical using attributes.
05647         
05648         Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
05649         we should use '_' (e.g., 'nlsat_propagations').
05650 
05651         >>> x = Int('x') 
05652         >>> s = Then('simplify', 'nlsat').solver()
05653         >>> s.add(x > 0)
05654         >>> s.check()
05655         sat
05656         >>> st = s.statistics() 
05657         >>> st.keys()
05658         ['nlsat propagations', 'nlsat stages']
05659         >>> st.nlsat_propagations
05660         2
05661         >>> st.nlsat_stages
05662         2
05663         """
05664         key = name.replace('_', ' ')
05665         try:
05666             return self.get_key_value(key)
05667         except Z3Exception:
05668             raise AttributeError
05669             
05670 #########################################
05671 #
05672 # Solver
05673 #
05674 #########################################
05675 class CheckSatResult:
05676     """Represents the result of a satisfiability check: sat, unsat, unknown.
05677     
05678     >>> s = Solver()
05679     >>> s.check()
05680     sat
05681     >>> r = s.check()
05682     >>> isinstance(r, CheckSatResult)
05683     True
05684     """
05685 
05686     def __init__(self, r):
05687         self.r = r
05688 
05689     def __eq__(self, other):
05690         return isinstance(other, CheckSatResult) and self.r == other.r
05691 
05692     def __ne__(self, other):
05693         return not self.__eq__(other)
05694 
05695     def __repr__(self):
05696         if in_html_mode():
05697             if self.r == Z3_L_TRUE:
05698                 return "<b>sat</b>"
05699             elif self.r == Z3_L_FALSE:
05700                 return "<b>unsat</b>"
05701             else:
05702                 return "<b>unknown</b>"
05703         else:
05704             if self.r == Z3_L_TRUE:
05705                 return "sat"
05706             elif self.r == Z3_L_FALSE:
05707                 return "unsat"
05708             else:
05709                 return "unknown"
05710 
05711 sat     = CheckSatResult(Z3_L_TRUE)
05712 unsat   = CheckSatResult(Z3_L_FALSE)
05713 unknown = CheckSatResult(Z3_L_UNDEF) 
05714 
05715 class Solver(Z3PPObject):
05716     """Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc."""
05717 
05718     def __init__(self, solver=None, ctx=None):
05719         assert solver == None or ctx != None
05720         self.ctx    = _get_ctx(ctx)
05721         self.solver = None
05722         if solver == None:
05723             self.solver = Z3_mk_solver(self.ctx.ref())
05724         else:
05725             self.solver = solver
05726         Z3_solver_inc_ref(self.ctx.ref(), self.solver)
05727 
05728     def __del__(self):
05729         if self.solver != None:
05730             Z3_solver_dec_ref(self.ctx.ref(), self.solver)
05731 
05732     def set(self, *args, **keys):
05733         """Set a configuration option. The method `help()` return a string containing all available options.
05734         
05735         >>> s = Solver()
05736         >>> # The option MBQI can be set using three different approaches.
05737         >>> s.set(mbqi=True)
05738         >>> s.set('MBQI', True)
05739         >>> s.set(':mbqi', True)
05740         """
05741         p = args2params(args, keys, self.ctx)
05742         Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
05743 
05744     def push(self):
05745         """Create a backtracking point.
05746 
05747         >>> x = Int('x')
05748         >>> s = Solver()
05749         >>> s.add(x > 0)
05750         >>> s
05751         [x > 0]
05752         >>> s.push()
05753         >>> s.add(x < 1)
05754         >>> s
05755         [x > 0, x < 1]
05756         >>> s.check()
05757         unsat
05758         >>> s.pop()
05759         >>> s.check()
05760         sat
05761         >>> s
05762         [x > 0]
05763         """
05764         Z3_solver_push(self.ctx.ref(), self.solver)
05765 
05766     def pop(self, num=1):
05767         """Backtrack \c num backtracking points.
05768         
05769         >>> x = Int('x')
05770         >>> s = Solver()
05771         >>> s.add(x > 0)
05772         >>> s
05773         [x > 0]
05774         >>> s.push()
05775         >>> s.add(x < 1)
05776         >>> s
05777         [x > 0, x < 1]
05778         >>> s.check()
05779         unsat
05780         >>> s.pop()
05781         >>> s.check()
05782         sat
05783         >>> s
05784         [x > 0]
05785         """
05786         Z3_solver_pop(self.ctx.ref(), self.solver, num)
05787 
05788     def reset(self):
05789         """Remove all asserted constraints and backtracking points created using `push()`.
05790         
05791         >>> x = Int('x')
05792         >>> s = Solver()
05793         >>> s.add(x > 0)
05794         >>> s
05795         [x > 0]
05796         >>> s.reset()
05797         >>> s
05798         []
05799         """
05800         Z3_solver_reset(self.ctx.ref(), self.solver)
05801     
05802     def assert_exprs(self, *args):
05803         """Assert constraints into the solver.
05804         
05805         >>> x = Int('x')
05806         >>> s = Solver()
05807         >>> s.assert_exprs(x > 0, x < 2)
05808         >>> s
05809         [x > 0, x < 2]
05810         """
05811         args = _get_args(args)
05812         s    = BoolSort(self.ctx)
05813         for arg in args:
05814             if isinstance(arg, Goal) or isinstance(arg, AstVector):
05815                 for f in arg:
05816                     Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
05817             else:
05818                 arg = s.cast(arg)
05819                 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
05820 
05821     def add(self, *args):
05822         """Assert constraints into the solver.
05823         
05824         >>> x = Int('x')
05825         >>> s = Solver()
05826         >>> s.add(x > 0, x < 2)
05827         >>> s
05828         [x > 0, x < 2]
05829         """
05830         self.assert_exprs(*args)
05831 
05832     def append(self, *args):
05833         """Assert constraints into the solver.
05834         
05835         >>> x = Int('x')
05836         >>> s = Solver()
05837         >>> s.append(x > 0, x < 2)
05838         >>> s
05839         [x > 0, x < 2]
05840         """
05841         self.assert_exprs(*args)
05842 
05843     def insert(self, *args):
05844         """Assert constraints into the solver.
05845         
05846         >>> x = Int('x')
05847         >>> s = Solver()
05848         >>> s.insert(x > 0, x < 2)
05849         >>> s
05850         [x > 0, x < 2]
05851         """
05852         self.assert_exprs(*args)
05853 
05854     def assert_and_track(self, a, p):
05855         """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
05856         
05857         If `p` is a string, it will be automatically converted into a Boolean constant.
05858         
05859         >>> x = Int('x')
05860         >>> p3 = Bool('p3')
05861         >>> s = Solver()
05862         >>> s.set(unsat_core=True)
05863         >>> s.assert_and_track(x > 0,  'p1')
05864         >>> s.assert_and_track(x != 1, 'p2')
05865         >>> s.assert_and_track(x < 0,  p3)
05866         >>> print(s.check())
05867         unsat
05868         >>> c = s.unsat_core()
05869         >>> len(c)
05870         2
05871         >>> Bool('p1') in c
05872         True
05873         >>> Bool('p2') in c
05874         False
05875         >>> p3 in c
05876         True
05877         """
05878         if isinstance(p, str):
05879             p = Bool(p, self.ctx)
05880         _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
05881         _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
05882         Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
05883 
05884     def check(self, *assumptions):
05885         """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
05886         
05887         >>> x = Int('x')
05888         >>> s = Solver()
05889         >>> s.check()
05890         sat
05891         >>> s.add(x > 0, x < 2)
05892         >>> s.check()
05893         sat
05894         >>> s.model()
05895         [x = 1]
05896         >>> s.add(x < 1)
05897         >>> s.check()
05898         unsat
05899         >>> s.reset()
05900         >>> s.add(2**x == 4)
05901         >>> s.check()
05902         unknown
05903         """
05904         assumptions = _get_args(assumptions)
05905         num = len(assumptions)
05906         _assumptions = (Ast * num)()
05907         for i in range(num):
05908             _assumptions[i] = assumptions[i].as_ast()
05909         r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
05910         return CheckSatResult(r)
05911 
05912     def model(self):
05913         """Return a model for the last `check()`. 
05914         
05915         This function raises an exception if 
05916         a model is not available (e.g., last `check()` returned unsat).
05917 
05918         >>> s = Solver()
05919         >>> a = Int('a')
05920         >>> s.add(a + 2 == 0)
05921         >>> s.check()
05922         sat
05923         >>> s.model()
05924         [a = -2]
05925         """
05926         try:
05927             return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
05928         except Z3Exception:
05929             raise Z3Exception("model is not available")
05930 
05931     def unsat_core(self):
05932         """Return a subset (as an AST vector) of the assumptions provided to the last check().
05933         
05934         These are the assumptions Z3 used in the unsatisfiability proof.
05935         Assumptions are available in Z3. They are used to extract unsatisfiable cores. 
05936         They may be also used to "retract" assumptions. Note that, assumptions are not really 
05937         "soft constraints", but they can be used to implement them. 
05938 
05939         >>> p1, p2, p3 = Bools('p1 p2 p3')
05940         >>> x, y       = Ints('x y')
05941         >>> s          = Solver()
05942         >>> s.add(Implies(p1, x > 0))
05943         >>> s.add(Implies(p2, y > x))
05944         >>> s.add(Implies(p2, y < 1))
05945         >>> s.add(Implies(p3, y > -3))
05946         >>> s.check(p1, p2, p3)
05947         unsat
05948         >>> core = s.unsat_core()
05949         >>> len(core)
05950         2
05951         >>> p1 in core
05952         True
05953         >>> p2 in core
05954         True
05955         >>> p3 in core
05956         False
05957         >>> # "Retracting" p2
05958         >>> s.check(p1, p3)
05959         sat
05960         """
05961         return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
05962 
05963     def proof(self):
05964         """Return a proof for the last `check()`. Proof construction must be enabled."""
05965         return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
05966 
05967     def assertions(self):
05968         """Return an AST vector containing all added constraints.
05969         
05970         >>> s = Solver()
05971         >>> s.assertions()
05972         []
05973         >>> a = Int('a')
05974         >>> s.add(a > 0)
05975         >>> s.add(a < 10)
05976         >>> s.assertions()
05977         [a > 0, a < 10]
05978         """
05979         return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
05980 
05981     def statistics(self):
05982         """Return statistics for the last `check()`.
05983         
05984         >>> s = SimpleSolver()
05985         >>> x = Int('x')
05986         >>> s.add(x > 0)
05987         >>> s.check()
05988         sat
05989         >>> st = s.statistics()
05990         >>> st.get_key_value('final checks')
05991         1
05992         >>> len(st) > 0
05993         True
05994         >>> st[0] != 0
05995         True
05996         """
05997         return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
05998 
05999     def reason_unknown(self):
06000         """Return a string describing why the last `check()` returned `unknown`.
06001         
06002         >>> x = Int('x')
06003         >>> s = SimpleSolver()
06004         >>> s.add(2**x == 4)
06005         >>> s.check()
06006         unknown
06007         >>> s.reason_unknown()
06008         '(incomplete (theory arithmetic))'
06009         """
06010         return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
06011     
06012     def help(self):
06013         """Display a string describing all available options."""
06014         print(Z3_solver_get_help(self.ctx.ref(), self.solver))
06015 
06016     def param_descrs(self):
06017         """Return the parameter description set."""
06018         return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
06019 
06020     def __repr__(self):
06021         """Return a formatted string with all added constraints."""
06022         return obj_to_string(self)
06023 
06024     def sexpr(self):
06025         """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
06026         
06027         >>> x = Int('x')
06028         >>> s = Solver()
06029         >>> s.add(x > 0)
06030         >>> s.add(x < 2)
06031         >>> r = s.sexpr()
06032         """
06033         return Z3_solver_to_string(self.ctx.ref(), self.solver)
06034 
06035     def to_smt2(self):
06036         """return SMTLIB2 formatted benchmark for solver's assertions"""
06037         es = self.assertions()
06038         sz = len(es)
06039         sz1 = sz
06040         if sz1 > 0:
06041             sz1 -= 1
06042         v = (Ast * sz1)()
06043         for i in range(sz1):
06044             v[i] = es[i].as_ast()
06045         if sz > 0:
06046             e = es[sz1].as_ast()
06047         else:
06048             e = BoolVal(True, self.ctx).as_ast()
06049         return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
06050 
06051 
06052 
06053 def SolverFor(logic, ctx=None):
06054     """Create a solver customized for the given logic. 
06055 
06056     The parameter `logic` is a string. It should be contains
06057     the name of a SMT-LIB logic.
06058     See http://www.smtlib.org/ for the name of all available logics.
06059 
06060     >>> s = SolverFor("QF_LIA")
06061     >>> x = Int('x')
06062     >>> s.add(x > 0)
06063     >>> s.add(x < 2)
06064     >>> s.check()
06065     sat
06066     >>> s.model()
06067     [x = 1]
06068     """
06069     ctx = _get_ctx(ctx)
06070     logic = to_symbol(logic)
06071     return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx)
06072 
06073 def SimpleSolver(ctx=None):
06074     """Return a simple general purpose solver with limited amount of preprocessing.
06075     
06076     >>> s = SimpleSolver()
06077     >>> x = Int('x')
06078     >>> s.add(x > 0)
06079     >>> s.check()
06080     sat
06081     """
06082     ctx = _get_ctx(ctx)
06083     return Solver(Z3_mk_simple_solver(ctx.ref()), ctx)
06084 
06085 #########################################
06086 #
06087 # Fixedpoint
06088 #
06089 #########################################
06090 
06091 class Fixedpoint(Z3PPObject):
06092     """Fixedpoint API provides methods for solving with recursive predicates"""
06093     
06094     def __init__(self, fixedpoint=None, ctx=None):
06095         assert fixedpoint == None or ctx != None
06096         self.ctx    = _get_ctx(ctx)
06097         self.fixedpoint = None
06098         if fixedpoint == None:
06099             self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
06100         else:
06101             self.fixedpoint = fixedpoint
06102         Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
06103         self.vars = []
06104 
06105     def __del__(self):
06106         if self.fixedpoint != None:
06107             Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
06108 
06109     def set(self, *args, **keys):
06110         """Set a configuration option. The method `help()` return a string containing all available options.        
06111         """
06112         p = args2params(args, keys, self.ctx)
06113         Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
06114 
06115     def help(self):
06116         """Display a string describing all available options."""
06117         print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
06118             
06119     def param_descrs(self):
06120         """Return the parameter description set."""
06121         return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
06122     
06123     def assert_exprs(self, *args):
06124         """Assert constraints as background axioms for the fixedpoint solver."""
06125         args = _get_args(args)
06126         s    = BoolSort(self.ctx)
06127         for arg in args:
06128             if isinstance(arg, Goal) or isinstance(arg, AstVector):
06129                 for f in arg:
06130                     f = self.abstract(f)
06131                     Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
06132             else:
06133                 arg = s.cast(arg)
06134                 arg = self.abstract(arg)
06135                 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
06136 
06137     def add(self, *args):
06138         """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
06139         self.assert_exprs(*args)
06140 
06141     def append(self, *args):
06142         """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
06143         self.assert_exprs(*args)
06144 
06145     def insert(self, *args):
06146         """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
06147         self.assert_exprs(*args)
06148 
06149     def add_rule(self, head, body = None, name = None):
06150         """Assert rules defining recursive predicates to the fixedpoint solver.
06151         >>> a = Bool('a')
06152         >>> b = Bool('b')
06153         >>> s = Fixedpoint()
06154         >>> s.register_relation(a.decl())
06155         >>> s.register_relation(b.decl())
06156         >>> s.fact(a)
06157         >>> s.rule(b, a)
06158         >>> s.query(b)
06159         sat
06160         """
06161         if name == None:
06162             name = ""
06163         name = to_symbol(name, self.ctx)
06164         if body == None:
06165             head = self.abstract(head)
06166             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)            
06167         else:
06168             body = _get_args(body)
06169             f    = self.abstract(Implies(And(body),head))
06170             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
06171         
06172     def rule(self, head, body = None, name = None):
06173         """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
06174         self.add_rule(head, body, name)
06175         
06176     def fact(self, head, name = None):
06177         """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
06178         self.add_rule(head, None, name)
06179 
06180     def query(self, *query):
06181         """Query the fixedpoint engine whether formula is derivable.
06182            You can also pass an tuple or list of recursive predicates.
06183         """
06184         query = _get_args(query)
06185         sz = len(query)
06186         if sz >= 1 and isinstance(query[0], FuncDecl):            
06187             _decls = (FuncDecl * sz)()
06188             i = 0
06189             for q in query:
06190                 _decls[i] = q.ast
06191                 i = i + 1
06192             r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
06193         else:
06194             if sz == 1:
06195                 query = query[0]
06196             else:
06197                 query = And(query)
06198             query = self.abstract(query, False)
06199             r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
06200         return CheckSatResult(r)
06201 
06202     def push(self):
06203         """create a backtracking point for added rules, facts and assertions"""
06204         Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
06205 
06206     def pop(self):
06207         """restore to previously created backtracking point"""
06208         Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
06209 
06210     def update_rule(self, head, body, name):
06211         """update rule"""
06212         if name == None:
06213             name = ""
06214         name = to_symbol(name, self.ctx)
06215         body = _get_args(body)
06216         f    = self.abstract(Implies(And(body),head))
06217         Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
06218 
06219     def get_answer(self):       
06220         """Retrieve answer from last query call."""
06221         r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
06222         return _to_expr_ref(r, self.ctx)
06223 
06224     def get_num_levels(self, predicate):
06225         """Retrieve number of levels used for predicate in PDR engine"""
06226         return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
06227 
06228     def get_cover_delta(self, level, predicate):
06229         """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
06230         r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
06231         return _to_expr_ref(r, self.ctx)
06232     
06233     def add_cover(self, level, predicate, property):
06234         """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
06235         Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
06236 
06237     def register_relation(self, *relations):
06238         """Register relation as recursive"""
06239         relations = _get_args(relations)
06240         for f in relations:
06241             Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
06242 
06243     def set_predicate_representation(self, f, *representations):
06244         """Control how relation is represented"""
06245         representations = _get_args(representations)
06246         representations = [to_symbol(s) for s in representations]
06247         sz = len(representations)
06248         args = (Symbol * sz)()
06249         for i in range(sz):
06250             args[i] = representations[i]
06251         Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
06252 
06253     def parse_string(self, s):
06254         """Parse rules and queries from a string"""
06255         return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
06256         
06257     def parse_file(self, f):
06258         """Parse rules and queries from a file"""
06259         return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
06260 
06261     def get_rules(self):
06262         """retrieve rules that have been added to fixedpoint context"""
06263         return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
06264 
06265     def get_assertions(self):
06266         """retrieve assertions that have been added to fixedpoint context"""
06267         return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
06268 
06269     def __repr__(self):
06270         """Return a formatted string with all added rules and constraints."""
06271         return self.sexpr()
06272 
06273     def sexpr(self):
06274         """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.        
06275         """
06276         return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
06277 
06278     def to_string(self, queries):
06279         """Return a formatted string (in Lisp-like format) with all added constraints.
06280            We say the string is in s-expression format.
06281            Include also queries.
06282         """
06283         args, len = _to_ast_array(queries)
06284         return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
06285     
06286     def statistics(self):
06287         """Return statistics for the last `query()`.
06288         """
06289         return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
06290 
06291     def reason_unknown(self):
06292         """Return a string describing why the last `query()` returned `unknown`.
06293         """
06294         return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
06295 
06296     def declare_var(self, *vars):
06297         """Add variable or several variables.
06298         The added variable or variables will be bound in the rules
06299         and queries
06300         """
06301         vars = _get_args(vars)
06302         for v in vars:
06303             self.vars += [v]
06304         
06305     def abstract(self, fml, is_forall=True):
06306         if self.vars == []:
06307             return fml
06308         if is_forall:
06309             return ForAll(self.vars, fml)
06310         else:
06311             return Exists(self.vars, fml)
06312 
06313 #########################################
06314 #
06315 # ApplyResult
06316 #
06317 #########################################
06318 class ApplyResult(Z3PPObject):
06319     """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters."""
06320     
06321     def __init__(self, result, ctx):
06322         self.result = result
06323         self.ctx    = ctx
06324         Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
06325 
06326     def __del__(self):
06327         Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
06328 
06329     def __len__(self):
06330         """Return the number of subgoals in `self`.
06331         
06332         >>> a, b = Ints('a b')
06333         >>> g = Goal()
06334         >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
06335         >>> t = Tactic('split-clause')
06336         >>> r = t(g)
06337         >>> len(r)
06338         2
06339         >>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
06340         >>> len(t(g))
06341         4
06342         >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
06343         >>> len(t(g))
06344         1
06345         """
06346         return int(Z3_apply_result_get_num_subgoals(self.ctx.ref(), self.result))
06347 
06348     def __getitem__(self, idx):
06349         """Return one of the subgoals stored in ApplyResult object `self`.
06350 
06351         >>> a, b = Ints('a b')
06352         >>> g = Goal()
06353         >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
06354         >>> t = Tactic('split-clause')
06355         >>> r = t(g)
06356         >>> r[0]        
06357         [a == 0, Or(b == 0, b == 1), a > b]
06358         >>> r[1]
06359         [a == 1, Or(b == 0, b == 1), a > b]
06360         """
06361         if idx >= len(self):
06362             raise IndexError
06363         return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx)
06364 
06365     def __repr__(self):
06366         return obj_to_string(self)
06367 
06368     def sexpr(self):
06369         """Return a textual representation of the s-expression representing the set of subgoals in `self`."""
06370         return Z3_apply_result_to_string(self.ctx.ref(), self.result)
06371 
06372     def convert_model(self, model, idx=0):
06373         """Convert a model for a subgoal into a model for the original goal.
06374 
06375         >>> a, b = Ints('a b')
06376         >>> g = Goal()
06377         >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
06378         >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
06379         >>> r = t(g)
06380         >>> r[0]        
06381         [Or(b == 0, b == 1), Not(0 <= b)]
06382         >>> r[1]
06383         [Or(b == 0, b == 1), Not(1 <= b)]
06384         >>> # Remark: the subgoal r[0] is unsatisfiable
06385         >>> # Creating a solver for solving the second subgoal
06386         >>> s = Solver()
06387         >>> s.add(r[1])
06388         >>> s.check()
06389         sat
06390         >>> s.model()
06391         [b = 0]
06392         >>> # Model s.model() does not assign a value to `a`
06393         >>> # It is a model for subgoal `r[1]`, but not for goal `g`
06394         >>> # The method convert_model creates a model for `g` from a model for `r[1]`.
06395         >>> r.convert_model(s.model(), 1)
06396         [b = 0, a = 1]
06397         """
06398         if __debug__:
06399             _z3_assert(idx < len(self), "index out of bounds")
06400             _z3_assert(isinstance(model, ModelRef), "Z3 Model expected")
06401         return ModelRef(Z3_apply_result_convert_model(self.ctx.ref(), self.result, idx, model.model), self.ctx)
06402 
06403     def as_expr(self):
06404         """Return a Z3 expression consisting of all subgoals.
06405         
06406         >>> x = Int('x')
06407         >>> g = Goal()
06408         >>> g.add(x > 1)
06409         >>> g.add(Or(x == 2, x == 3))
06410         >>> r = Tactic('simplify')(g)
06411         >>> r
06412         [[Not(x <= 1), Or(x == 2, x == 3)]]
06413         >>> r.as_expr()
06414         And(Not(x <= 1), Or(x == 2, x == 3))
06415         >>> r = Tactic('split-clause')(g)
06416         >>> r
06417         [[x > 1, x == 2], [x > 1, x == 3]]
06418         >>> r.as_expr()
06419         Or(And(x > 1, x == 2), And(x > 1, x == 3))
06420         """
06421         sz = len(self)
06422         if sz == 0:
06423             return BoolVal(False, self.ctx)
06424         elif sz == 1:
06425             return self[0].as_expr()
06426         else:
06427             return Or([ self[i].as_expr() for i in range(len(self)) ])
06428         
06429 #########################################
06430 #
06431 # Tactics
06432 #
06433 #########################################
06434 class Tactic:
06435     """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver().
06436 
06437     Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
06438     """
06439     def __init__(self, tactic, ctx=None):
06440         self.ctx    = _get_ctx(ctx)
06441         self.tactic = None
06442         if isinstance(tactic, TacticObj):
06443             self.tactic = tactic
06444         else:
06445             if __debug__:
06446                 _z3_assert(isinstance(tactic, str), "tactic name expected")
06447             try:
06448                 self.tactic = Z3_mk_tactic(self.ctx.ref(), str(tactic))
06449             except Z3Exception:
06450                 raise Z3Exception("unknown tactic '%s'" % tactic)
06451         Z3_tactic_inc_ref(self.ctx.ref(), self.tactic)
06452 
06453     def __del__(self):
06454         if self.tactic != None:
06455             Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
06456 
06457     def solver(self):
06458         """Create a solver using the tactic `self`.
06459 
06460         The solver supports the methods `push()` and `pop()`, but it
06461         will always solve each `check()` from scratch.
06462         
06463         >>> t = Then('simplify', 'nlsat')
06464         >>> s = t.solver()
06465         >>> x = Real('x')
06466         >>> s.add(x**2 == 2, x > 0)
06467         >>> s.check()
06468         sat
06469         >>> s.model()
06470         [x = 1.4142135623?]
06471         """
06472         return Solver(Z3_mk_solver_from_tactic(self.ctx.ref(), self.tactic), self.ctx)
06473 
06474     def apply(self, goal, *arguments, **keywords):
06475         """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
06476         
06477         >>> x, y = Ints('x y')
06478         >>> t = Tactic('solve-eqs')
06479         >>> t.apply(And(x == 0, y >= x + 1))
06480         [[y >= 1]]
06481         """
06482         if __debug__:
06483             _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected")
06484         goal = _to_goal(goal)
06485         if len(arguments) > 0 or len(keywords) > 0:
06486             p = args2params(arguments, keywords, self.ctx)
06487             return ApplyResult(Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
06488         else:
06489             return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
06490 
06491     def __call__(self, goal, *arguments, **keywords):
06492         """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
06493         
06494         >>> x, y = Ints('x y')
06495         >>> t = Tactic('solve-eqs')
06496         >>> t(And(x == 0, y >= x + 1))
06497         [[y >= 1]]
06498         """
06499         return self.apply(goal, *arguments, **keywords)
06500 
06501     def help(self):
06502         """Display a string containing a description of the available options for the `self` tactic."""
06503         print(Z3_tactic_get_help(self.ctx.ref(), self.tactic))
06504 
06505     def param_descrs(self):
06506         """Return the parameter description set."""
06507         return ParamDescrsRef(Z3_tactic_get_param_descrs(self.ctx.ref(), self.tactic), self.ctx)
06508 
06509 def _to_goal(a):
06510     if isinstance(a, BoolRef):
06511         goal = Goal(ctx = a.ctx)
06512         goal.add(a)
06513         return goal
06514     else:
06515         return a
06516 
06517 def _to_tactic(t, ctx=None):
06518     if isinstance(t, Tactic):
06519         return t
06520     else:
06521         return Tactic(t, ctx)
06522 
06523 def _and_then(t1, t2, ctx=None):
06524     t1 = _to_tactic(t1, ctx)
06525     t2 = _to_tactic(t2, ctx)
06526     if __debug__:
06527         _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
06528     return Tactic(Z3_tactic_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
06529 
06530 def _or_else(t1, t2, ctx=None):
06531     t1 = _to_tactic(t1, ctx)
06532     t2 = _to_tactic(t2, ctx)
06533     if __debug__:
06534         _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
06535     return Tactic(Z3_tactic_or_else(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
06536 
06537 def AndThen(*ts, **ks):
06538     """Return a tactic that applies the tactics in `*ts` in sequence.
06539     
06540     >>> x, y = Ints('x y')
06541     >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
06542     >>> t(And(x == 0, y > x + 1))
06543     [[Not(y <= 1)]]
06544     >>> t(And(x == 0, y > x + 1)).as_expr()
06545     Not(y <= 1)
06546     """
06547     if __debug__:
06548         _z3_assert(len(ts) >= 2, "At least two arguments expected")
06549     ctx = ks.get('ctx', None)
06550     num = len(ts)
06551     r = ts[0]
06552     for i in range(num - 1):
06553         r = _and_then(r, ts[i+1], ctx)
06554     return r
06555 
06556 def Then(*ts, **ks):
06557     """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
06558     
06559     >>> x, y = Ints('x y')
06560     >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
06561     >>> t(And(x == 0, y > x + 1))
06562     [[Not(y <= 1)]]
06563     >>> t(And(x == 0, y > x + 1)).as_expr()
06564     Not(y <= 1)
06565     """
06566     return AndThen(*ts, **ks)
06567     
06568 def OrElse(*ts, **ks):
06569     """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
06570 
06571     >>> x = Int('x')
06572     >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
06573     >>> # Tactic split-clause fails if there is no clause in the given goal.
06574     >>> t(x == 0)
06575     [[x == 0]]
06576     >>> t(Or(x == 0, x == 1))
06577     [[x == 0], [x == 1]]
06578     """
06579     if __debug__:
06580         _z3_assert(len(ts) >= 2, "At least two arguments expected")
06581     ctx = ks.get('ctx', None)
06582     num = len(ts)
06583     r = ts[0]
06584     for i in range(num - 1):
06585         r = _or_else(r, ts[i+1], ctx)
06586     return r
06587 
06588 def ParOr(*ts, **ks):
06589     """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
06590 
06591     >>> x = Int('x')
06592     >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
06593     >>> t(x + 1 == 2)
06594     [[x == 1]]
06595     """
06596     if __debug__:
06597         _z3_assert(len(ts) >= 2, "At least two arguments expected")
06598     ctx = _get_ctx(ks.get('ctx', None))
06599     ts  = [ _to_tactic(t, ctx) for t in ts ]
06600     sz  = len(ts)
06601     _args = (TacticObj * sz)()
06602     for i in range(sz):
06603         _args[i] = ts[i].tactic
06604     return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
06605 
06606 def ParThen(t1, t2, ctx=None):
06607     """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
06608     
06609     >>> x, y = Ints('x y')
06610     >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
06611     >>> t(And(Or(x == 1, x == 2), y == x + 1))
06612     [[x == 1, y == 2], [x == 2, y == 3]]
06613     """
06614     t1 = _to_tactic(t1, ctx)
06615     t2 = _to_tactic(t2, ctx)
06616     if __debug__:
06617         _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
06618     return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
06619 
06620 def ParAndThen(t1, t2, ctx=None):
06621     """Alias for ParThen(t1, t2, ctx)."""
06622     return ParThen(t1, t2, ctx)
06623 
06624 def With(t, *args, **keys):
06625     """Return a tactic that applies tactic `t` using the given configuration options.
06626     
06627     >>> x, y = Ints('x y')
06628     >>> t = With(Tactic('simplify'), som=True)
06629     >>> t((x + 1)*(y + 2) == 0)
06630     [[2*x + y + x*y == -2]]
06631     """
06632     ctx = keys.get('ctx', None)
06633     t = _to_tactic(t, ctx)
06634     p = args2params(args, keys, t.ctx)
06635     return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
06636 
06637 def Repeat(t, max=4294967295, ctx=None):
06638     """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
06639 
06640     >>> x, y = Ints('x y')
06641     >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
06642     >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
06643     >>> r = t(c)
06644     >>> for subgoal in r: print(subgoal)
06645     [x == 0, y == 0, x > y]
06646     [x == 0, y == 1, x > y]
06647     [x == 1, y == 0, x > y]
06648     [x == 1, y == 1, x > y]
06649     >>> t = Then(t, Tactic('propagate-values'))
06650     >>> t(c)
06651     [[x == 1, y == 0]]
06652     """
06653     t = _to_tactic(t, ctx)
06654     return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)
06655 
06656 def TryFor(t, ms, ctx=None):
06657     """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
06658     
06659     If `t` does not terminate in `ms` milliseconds, then it fails.
06660     """
06661     t = _to_tactic(t, ctx)
06662     return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)
06663 
06664 def tactics(ctx=None):
06665     """Return a list of all available tactics in Z3.
06666     
06667     >>> l = tactics()
06668     >>> l.count('simplify') == 1
06669     True
06670     """
06671     ctx = _get_ctx(ctx)
06672     return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]
06673 
06674 def tactic_description(name, ctx=None):
06675     """Return a short description for the tactic named `name`.
06676 
06677     >>> d = tactic_description('simplify')
06678     """
06679     ctx = _get_ctx(ctx)
06680     return Z3_tactic_get_descr(ctx.ref(), name)
06681 
06682 def describe_tactics():
06683     """Display a (tabular) description of all available tactics in Z3."""
06684     if in_html_mode():
06685         even = True
06686         print('<table border="1" cellpadding="2" cellspacing="0">')
06687         for t in tactics():
06688             if even:
06689                 print('<tr style="background-color:#CFCFCF">')
06690                 even = False
06691             else:
06692                 print('<tr>')
06693                 even = True
06694             print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
06695         print('</table>')
06696     else:
06697         for t in tactics():
06698             print('%s : %s' % (t, tactic_description(t)))
06699 
06700 class Probe:
06701     """Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used."""
06702     def __init__(self, probe, ctx=None):
06703         self.ctx    = _get_ctx(ctx)
06704         self.probe  = None
06705         if isinstance(probe, ProbeObj):
06706             self.probe = probe
06707         elif isinstance(probe, float):
06708             self.probe = Z3_probe_const(self.ctx.ref(), probe)
06709         elif _is_int(probe):
06710             self.probe = Z3_probe_const(self.ctx.ref(), float(probe))
06711         elif isinstance(probe, bool):
06712             if probe:
06713                 self.probe = Z3_probe_const(self.ctx.ref(), 1.0)
06714             else:
06715                 self.probe = Z3_probe_const(self.ctx.ref(), 0.0)
06716         else:
06717             if __debug__:
06718                 _z3_assert(isinstance(probe, str), "probe name expected")
06719             try:
06720                 self.probe = Z3_mk_probe(self.ctx.ref(), probe)
06721             except Z3Exception:
06722                 raise Z3Exception("unknown probe '%s'" % probe)
06723         Z3_probe_inc_ref(self.ctx.ref(), self.probe)
06724 
06725     def __del__(self):
06726         if self.probe != None:
06727             Z3_probe_dec_ref(self.ctx.ref(), self.probe)
06728 
06729     def __lt__(self, other):
06730         """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`.
06731 
06732         >>> p = Probe('size') < 10
06733         >>> x = Int('x')
06734         >>> g = Goal()
06735         >>> g.add(x > 0)
06736         >>> g.add(x < 10)
06737         >>> p(g)
06738         1.0
06739         """
06740         return Probe(Z3_probe_lt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06741 
06742     def __gt__(self, other):
06743         """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`.
06744 
06745         >>> p = Probe('size') > 10
06746         >>> x = Int('x')
06747         >>> g = Goal()
06748         >>> g.add(x > 0)
06749         >>> g.add(x < 10)
06750         >>> p(g)
06751         0.0
06752         """
06753         return Probe(Z3_probe_gt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06754 
06755     def __le__(self, other):
06756         """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`.
06757 
06758         >>> p = Probe('size') <= 2
06759         >>> x = Int('x')
06760         >>> g = Goal()
06761         >>> g.add(x > 0)
06762         >>> g.add(x < 10)
06763         >>> p(g)
06764         1.0
06765         """
06766         return Probe(Z3_probe_le(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06767 
06768     def __ge__(self, other):
06769         """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`.
06770 
06771         >>> p = Probe('size') >= 2
06772         >>> x = Int('x')
06773         >>> g = Goal()
06774         >>> g.add(x > 0)
06775         >>> g.add(x < 10)
06776         >>> p(g)
06777         1.0
06778         """
06779         return Probe(Z3_probe_ge(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06780 
06781     def __eq__(self, other):
06782         """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`.
06783 
06784         >>> p = Probe('size') == 2
06785         >>> x = Int('x')
06786         >>> g = Goal()
06787         >>> g.add(x > 0)
06788         >>> g.add(x < 10)
06789         >>> p(g)
06790         1.0
06791         """
06792         return Probe(Z3_probe_eq(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06793 
06794     def __ne__(self, other):
06795         """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`.
06796 
06797         >>> p = Probe('size') != 2
06798         >>> x = Int('x')
06799         >>> g = Goal()
06800         >>> g.add(x > 0)
06801         >>> g.add(x < 10)
06802         >>> p(g)
06803         0.0
06804         """
06805         p = self.__eq__(other)
06806         return Probe(Z3_probe_not(self.ctx.ref(), p.probe), self.ctx)
06807 
06808     def __call__(self, goal):
06809         """Evaluate the probe `self` in the given goal.
06810         
06811         >>> p = Probe('size')
06812         >>> x = Int('x')
06813         >>> g = Goal()
06814         >>> g.add(x > 0)
06815         >>> g.add(x < 10)
06816         >>> p(g)
06817         2.0
06818         >>> g.add(x < 20)
06819         >>> p(g)
06820         3.0
06821         >>> p = Probe('num-consts')
06822         >>> p(g)
06823         1.0
06824         >>> p = Probe('is-propositional')
06825         >>> p(g)
06826         0.0
06827         >>> p = Probe('is-qflia')
06828         >>> p(g)
06829         1.0
06830         """
06831         if __debug__:
06832             _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expression expected") 
06833         goal = _to_goal(goal)
06834         return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal)
06835 
06836 def is_probe(p):
06837     """Return `True` if `p` is a Z3 probe.
06838     
06839     >>> is_probe(Int('x'))
06840     False
06841     >>> is_probe(Probe('memory'))
06842     True
06843     """
06844     return isinstance(p, Probe)
06845 
06846 def _to_probe(p, ctx=None):
06847     if is_probe(p):
06848         return p
06849     else:
06850         return Probe(p, ctx)
06851 
06852 def probes(ctx=None):
06853     """Return a list of all available probes in Z3.
06854     
06855     >>> l = probes()
06856     >>> l.count('memory') == 1
06857     True
06858     """
06859     ctx = _get_ctx(ctx)
06860     return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]
06861 
06862 def probe_description(name, ctx=None):
06863     """Return a short description for the probe named `name`.
06864     
06865     >>> d = probe_description('memory')
06866     """
06867     ctx = _get_ctx(ctx)
06868     return Z3_probe_get_descr(ctx.ref(), name)
06869 
06870 def describe_probes():
06871     """Display a (tabular) description of all available probes in Z3."""
06872     if in_html_mode():
06873         even = True
06874         print('<table border="1" cellpadding="2" cellspacing="0">')
06875         for p in probes():
06876             if even:
06877                 print('<tr style="background-color:#CFCFCF">')
06878                 even = False
06879             else:
06880                 print('<tr>')
06881                 even = True
06882             print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
06883         print('</table>')
06884     else:
06885         for p in probes():
06886             print('%s : %s' % (p, probe_description(p)))
06887 
06888 def _probe_nary(f, args, ctx):
06889     if __debug__:
06890         _z3_assert(len(args) > 0, "At least one argument expected")
06891     num = len(args)
06892     r = _to_probe(args[0], ctx)
06893     for i in range(num - 1):
06894         r = Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
06895     return r
06896 
06897 def _probe_and(args, ctx):
06898     return _probe_nary(Z3_probe_and, args, ctx)
06899 
06900 def _probe_or(args, ctx):
06901     return _probe_nary(Z3_probe_or, args, ctx)
06902 
06903 def FailIf(p, ctx=None):
06904     """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
06905 
06906     In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
06907 
06908     >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
06909     >>> x, y = Ints('x y')
06910     >>> g = Goal()
06911     >>> g.add(x > 0)
06912     >>> g.add(y > 0)
06913     >>> t(g)
06914     [[x > 0, y > 0]]
06915     >>> g.add(x == y + 1)
06916     >>> t(g)
06917     [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
06918     """
06919     p = _to_probe(p, ctx)
06920     return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
06921 
06922 def When(p, t, ctx=None):
06923     """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
06924     
06925     >>> t = When(Probe('size') > 2, Tactic('simplify'))
06926     >>> x, y = Ints('x y')
06927     >>> g = Goal()
06928     >>> g.add(x > 0)
06929     >>> g.add(y > 0)
06930     >>> t(g)
06931     [[x > 0, y > 0]]
06932     >>> g.add(x == y + 1)
06933     >>> t(g)
06934     [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
06935     """
06936     p = _to_probe(p, ctx)
06937     t = _to_tactic(t, ctx)
06938     return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
06939 
06940 def Cond(p, t1, t2, ctx=None):
06941     """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
06942     
06943     >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
06944     """
06945     p = _to_probe(p, ctx)
06946     t1 = _to_tactic(t1, ctx)
06947     t2 = _to_tactic(t2, ctx)
06948     return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
06949 
06950 #########################################
06951 #
06952 # Utils
06953 #
06954 #########################################
06955 
06956 def simplify(a, *arguments, **keywords):
06957     """Simplify the expression `a` using the given options.
06958 
06959     This function has many options. Use `help_simplify` to obtain the complete list.
06960     
06961     >>> x = Int('x')
06962     >>> y = Int('y')
06963     >>> simplify(x + 1 + y + x + 1)
06964     2 + 2*x + y
06965     >>> simplify((x + 1)*(y + 1), som=True)
06966     1 + x + y + x*y
06967     >>> simplify(Distinct(x, y, 1), blast_distinct=True)
06968     And(Not(x == y), Not(x == 1), Not(y == 1))
06969     >>> simplify(And(x == 0, y == 1), elim_and=True)
06970     Not(Or(Not(x == 0), Not(y == 1)))
06971     """
06972     if __debug__:
06973         _z3_assert(is_expr(a), "Z3 expression expected")
06974     if len(arguments) > 0 or len(keywords) > 0:
06975         p = args2params(arguments, keywords, a.ctx)
06976         return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
06977     else:
06978         return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
06979 
06980 def help_simplify():
06981     """Return a string describing all options available for Z3 `simplify` procedure."""
06982     print(Z3_simplify_get_help(main_ctx().ref()))
06983 
06984 def simplify_param_descrs():
06985     """Return the set of parameter descriptions for Z3 `simplify` procedure."""
06986     return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())
06987 
06988 def substitute(t, *m):
06989     """Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to.
06990     
06991     >>> x = Int('x')
06992     >>> y = Int('y')
06993     >>> substitute(x + 1, (x, y + 1))
06994     y + 1 + 1
06995     >>> f = Function('f', IntSort(), IntSort())
06996     >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
06997     1 + 1
06998     """
06999     if isinstance(m, tuple):
07000         m1 = _get_args(m)
07001         if isinstance(m1, list):
07002             m = m1
07003     if __debug__:
07004         _z3_assert(is_expr(t), "Z3 expression expected")
07005         _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
07006     num = len(m)
07007     _from = (Ast * num)()
07008     _to   = (Ast * num)()
07009     for i in range(num):
07010         _from[i] = m[i][0].as_ast()
07011         _to[i]   = m[i][1].as_ast()
07012     return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
07013 
07014 def substitute_vars(t, *m):
07015     """Substitute the free variables in t with the expression in m.
07016     
07017     >>> v0 = Var(0, IntSort())
07018     >>> v1 = Var(1, IntSort())
07019     >>> x  = Int('x')
07020     >>> f  = Function('f', IntSort(), IntSort(), IntSort())
07021     >>> # replace v0 with x+1 and v1 with x
07022     >>> substitute_vars(f(v0, v1), x + 1, x)
07023     f(x + 1, x)
07024     """
07025     if __debug__:
07026         _z3_assert(is_expr(t), "Z3 expression expected")
07027         _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
07028     num = len(m)
07029     _to   = (Ast * num)()
07030     for i in range(num):
07031         _to[i] = m[i].as_ast()
07032     return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
07033 
07034 def Sum(*args):
07035     """Create the sum of the Z3 expressions. 
07036     
07037     >>> a, b, c = Ints('a b c')
07038     >>> Sum(a, b, c)
07039     a + b + c
07040     >>> Sum([a, b, c])
07041     a + b + c
07042     >>> A = IntVector('a', 5)
07043     >>> Sum(A)
07044     a__0 + a__1 + a__2 + a__3 + a__4
07045     """
07046     args  = _get_args(args)
07047     if __debug__:
07048         _z3_assert(len(args) > 0, "Non empty list of arguments expected")
07049     ctx   = _ctx_from_ast_arg_list(args)
07050     if __debug__:
07051         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
07052     args  = _coerce_expr_list(args, ctx)
07053     if is_bv(args[0]):
07054         return _reduce(lambda a, b: a + b, args, 0)
07055     else:
07056         _args, sz = _to_ast_array(args)
07057         return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)
07058 
07059 def Product(*args):
07060     """Create the product of the Z3 expressions. 
07061     
07062     >>> a, b, c = Ints('a b c')
07063     >>> Product(a, b, c)
07064     a*b*c
07065     >>> Product([a, b, c])
07066     a*b*c
07067     >>> A = IntVector('a', 5)
07068     >>> Product(A)
07069     a__0*a__1*a__2*a__3*a__4
07070     """
07071     args  = _get_args(args)
07072     if __debug__:
07073         _z3_assert(len(args) > 0, "Non empty list of arguments expected")
07074     ctx   = _ctx_from_ast_arg_list(args)
07075     if __debug__:
07076         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
07077     args  = _coerce_expr_list(args, ctx)
07078     if is_bv(args[0]):
07079         return _reduce(lambda a, b: a * b, args, 1)
07080     else:
07081         _args, sz = _to_ast_array(args)
07082         return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
07083 
07084 def solve(*args, **keywords):
07085     """Solve the constraints `*args`.
07086     
07087     This is a simple function for creating demonstrations. It creates a solver,
07088     configure it using the options in `keywords`, adds the constraints
07089     in `args`, and invokes check.
07090     
07091     >>> a = Int('a')
07092     >>> solve(a > 0, a < 2)
07093     [a = 1]
07094     """
07095     s = Solver()
07096     s.set(**keywords)
07097     s.add(*args)
07098     if keywords.get('show', False):
07099         print(s)
07100     r = s.check()
07101     if r == unsat:
07102         print("no solution")
07103     elif r == unknown:
07104         print("failed to solve")
07105         try:
07106             print(s.model())
07107         except Z3Exception:
07108             return
07109     else:
07110         print(s.model())
07111 
07112 def solve_using(s, *args, **keywords):
07113     """Solve the constraints `*args` using solver `s`.
07114     
07115     This is a simple function for creating demonstrations. It is similar to `solve`,
07116     but it uses the given solver `s`.
07117     It configures solver `s` using the options in `keywords`, adds the constraints
07118     in `args`, and invokes check.
07119     """
07120     if __debug__:
07121         _z3_assert(isinstance(s, Solver), "Solver object expected")
07122     s.set(**keywords)
07123     s.add(*args)
07124     if keywords.get('show', False):
07125         print("Problem:")
07126         print(s)
07127     r = s.check()
07128     if r == unsat:
07129         print("no solution")
07130     elif r == unknown:
07131         print("failed to solve")
07132         try:
07133             print(s.model())
07134         except Z3Exception:
07135             return
07136     else:
07137         if keywords.get('show', False):
07138             print("Solution:")
07139         print(s.model())
07140 
07141 def prove(claim, **keywords):
07142     """Try to prove the given claim.
07143 
07144     This is a simple function for creating demonstrations.  It tries to prove
07145     `claim` by showing the negation is unsatisfiable.
07146 
07147     >>> p, q = Bools('p q')
07148     >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
07149     proved
07150     """
07151     if __debug__:
07152         _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
07153     s = Solver()
07154     s.set(**keywords)
07155     s.add(Not(claim))
07156     if keywords.get('show', False):
07157         print(s)
07158     r = s.check()
07159     if r == unsat:
07160         print("proved")
07161     elif r == unknown:
07162         print("failed to prove")
07163         print(s.model())
07164     else:
07165         print("counterexample")
07166         print(s.model())
07167 
07168 def _solve_html(*args, **keywords):
07169     """Version of funcion `solve` used in RiSE4Fun."""
07170     s = Solver()
07171     s.set(**keywords)
07172     s.add(*args)
07173     if keywords.get('show', False):
07174         print("<b>Problem:</b>")
07175         print(s)
07176     r = s.check()
07177     if r == unsat:
07178         print("<b>no solution</b>")
07179     elif r == unknown:
07180         print("<b>failed to solve</b>")
07181         try:
07182             print(s.model())
07183         except Z3Exception:
07184             return
07185     else:
07186         if keywords.get('show', False):
07187             print("<b>Solution:</b>")
07188         print(s.model())
07189 
07190 def _solve_using_html(s, *args, **keywords):
07191     """Version of funcion `solve_using` used in RiSE4Fun."""
07192     if __debug__:
07193         _z3_assert(isinstance(s, Solver), "Solver object expected")
07194     s.set(**keywords)
07195     s.add(*args)
07196     if keywords.get('show', False):
07197         print("<b>Problem:</b>")
07198         print(s)
07199     r = s.check()
07200     if r == unsat:
07201         print("<b>no solution</b>")
07202     elif r == unknown:
07203         print("<b>failed to solve</b>")
07204         try:
07205             print(s.model())
07206         except Z3Exception:
07207             return
07208     else:
07209         if keywords.get('show', False):
07210             print("<b>Solution:</b>")
07211         print(s.model())
07212 
07213 def _prove_html(claim, **keywords):
07214     """Version of funcion `prove` used in RiSE4Fun."""
07215     if __debug__:
07216         _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
07217     s = Solver()
07218     s.set(**keywords)
07219     s.add(Not(claim))
07220     if keywords.get('show', False):
07221         print(s)
07222     r = s.check()
07223     if r == unsat:
07224         print("<b>proved</b>")
07225     elif r == unknown:
07226         print("<b>failed to prove</b>")
07227         print(s.model())
07228     else:
07229         print("<b>counterexample</b>")
07230         print(s.model())
07231 
07232 def _dict2sarray(sorts, ctx):
07233     sz = len(sorts)
07234     _names = (Symbol * sz)()
07235     _sorts = (Sort * sz) ()
07236     i = 0
07237     for k in sorts:
07238         v = sorts[k]
07239         if __debug__:
07240             _z3_assert(isinstance(k, str), "String expected")
07241             _z3_assert(is_sort(v), "Z3 sort expected")
07242         _names[i] = to_symbol(k, ctx)
07243         _sorts[i] = v.ast
07244         i = i + 1
07245     return sz, _names, _sorts
07246 
07247 def _dict2darray(decls, ctx):
07248     sz = len(decls)
07249     _names = (Symbol * sz)()
07250     _decls = (FuncDecl * sz) ()
07251     i = 0
07252     for k in decls:
07253         v = decls[k]
07254         if __debug__:
07255             _z3_assert(isinstance(k, str), "String expected")
07256             _z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected")
07257         _names[i] = to_symbol(k, ctx)
07258         if is_const(v):
07259             _decls[i] = v.decl().ast
07260         else:
07261             _decls[i] = v.ast
07262         i = i + 1
07263     return sz, _names, _decls
07264 
07265 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
07266     """Parse a string in SMT 2.0 format using the given sorts and decls.
07267     
07268     The arguments sorts and decls are Python dictionaries used to initialize
07269     the symbol table used for the SMT 2.0 parser.
07270 
07271     >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
07272     And(x > 0, x < 10)
07273     >>> x, y = Ints('x y')
07274     >>> f = Function('f', IntSort(), IntSort())
07275     >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
07276     x + f(y) > 0
07277     >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
07278     a > 0
07279     """
07280     ctx = _get_ctx(ctx)
07281     ssz, snames, ssorts = _dict2sarray(sorts, ctx)
07282     dsz, dnames, ddecls = _dict2darray(decls, ctx)
07283     return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
07284 
07285 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
07286     """Parse a file in SMT 2.0 format using the given sorts and decls.
07287     
07288     This function is similar to parse_smt2_string().
07289     """
07290     ctx = _get_ctx(ctx)
07291     ssz, snames, ssorts = _dict2sarray(sorts, ctx)
07292     dsz, dnames, ddecls = _dict2darray(decls, ctx)
07293     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
07294    
07295 def Interpolant(a,ctx=None):
07296     """Create an interpolation operator.
07297     
07298     The argument is an interpolation pattern (see tree_interpolant). 
07299 
07300     >>> x = Int('x')
07301     >>> print Interpolant(x>0)
07302     interp(x > 0)
07303     """
07304     ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
07305     s = BoolSort(ctx)
07306     a = s.cast(a)
07307     return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
07308 
07309 def tree_interpolant(pat,p=None,ctx=None):
07310     """Compute interpolant for a tree of formulas.
07311 
07312     The input is an interpolation pattern over a set of formulas C.
07313     The pattern pat is a formula combining the formulas in C using
07314     logical conjunction and the "interp" operator (see Interp). This
07315     interp operator is logically the identity operator. It marks the
07316     sub-formulas of the pattern for which interpolants should be
07317     computed. The interpolant is a map sigma from marked subformulas
07318     to formulas, such that, for each marked subformula phi of pat
07319     (where phi sigma is phi with sigma(psi) substituted for each
07320     subformula psi of phi such that psi in dom(sigma)):
07321 
07322       1) phi sigma implies sigma(phi), and
07323 
07324       2) sigma(phi) is in the common uninterpreted vocabulary between
07325       the formulas of C occurring in phi and those not occurring in
07326       phi
07327 
07328       and moreover pat sigma implies false. In the simplest case
07329       an interpolant for the pattern "(and (interp A) B)" maps A
07330       to an interpolant for A /\ B. 
07331 
07332       The return value is a vector of formulas representing sigma. This
07333       vector contains sigma(phi) for each marked subformula of pat, in
07334       pre-order traversal. This means that subformulas of phi occur before phi
07335       in the vector. Also, subformulas that occur multiply in pat will
07336       occur multiply in the result vector.
07337 
07338     If pat is satisfiable, raises an object of class ModelRef
07339     that represents a model of pat.
07340 
07341     If parameters p are supplied, these are used in creating the
07342     solver that determines satisfiability.
07343 
07344     >>> x = Int('x')
07345     >>> y = Int('y')
07346     >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
07347     [Not(x >= 0), Not(y <= 2)]
07348 
07349     >>> g = And(Interpolant(x<0),x<2)
07350     >>> try:
07351     ...     print tree_interpolant(g).sexpr()
07352     ... except ModelRef as m:
07353     ...     print m.sexpr()
07354     (define-fun x () Int
07355       (- 1))
07356     """
07357     f = pat
07358     ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
07359     ptr = (AstVectorObj * 1)()
07360     mptr = (Model * 1)()
07361     if p == None:
07362         p = ParamsRef(ctx)
07363     res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
07364     if res == Z3_L_FALSE:
07365         return AstVector(ptr[0],ctx)
07366     raise ModelRef(mptr[0], ctx)
07367 
07368 def binary_interpolant(a,b,p=None,ctx=None):
07369     """Compute an interpolant for a binary conjunction.
07370 
07371     If a & b is unsatisfiable, returns an interpolant for a & b.
07372     This is a formula phi such that
07373 
07374     1) a implies phi
07375     2) b implies not phi
07376     3) All the uninterpreted symbols of phi occur in both a and b.
07377 
07378     If a & b is satisfiable, raises an object of class ModelRef
07379     that represents a model of a &b.
07380 
07381     If parameters p are supplied, these are used in creating the
07382     solver that determines satisfiability.
07383 
07384     x = Int('x')
07385     print binary_interpolant(x<0,x>2)
07386     Not(x >= 0)
07387     """
07388     f = And(Interpolant(a),b)
07389     return tree_interpolant(f,p,ctx)[0]
07390 
07391 def sequence_interpolant(v,p=None,ctx=None):
07392     """Compute interpolant for a sequence of formulas.
07393 
07394     If len(v) == N, and if the conjunction of the formulas in v is
07395     unsatisfiable, the interpolant is a sequence of formulas w
07396     such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
07397 
07398     1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
07399     2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
07400     and v[i+1]..v[n]
07401     
07402     Requires len(v) >= 1. 
07403 
07404     If a & b is satisfiable, raises an object of class ModelRef
07405     that represents a model of a & b.
07406 
07407     If parameters p are supplied, these are used in creating the
07408     solver that determines satisfiability.
07409 
07410     >>> x = Int('x')
07411     >>> y = Int('y')
07412     >>> print sequence_interpolant([x < 0, y == x , y > 2])
07413     [Not(x >= 0), Not(y >= 0)]
07414     """
07415     f = v[0]
07416     for i in range(1,len(v)):
07417         f = And(Interpolant(f),v[i])
07418     return tree_interpolant(f,p,ctx)
07419 
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines