Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

class  Context
class  Z3PPObject
 ASTs base class. More...
class  AstRef
class  SortRef
class  FuncDeclRef
 Function Declarations. More...
class  ExprRef
 Expressions. More...
class  BoolSortRef
 Booleans. More...
class  BoolRef
class  PatternRef
 Patterns. More...
class  QuantifierRef
 Quantifiers. More...
class  ArithSortRef
 Arithmetic. More...
class  ArithRef
class  IntNumRef
class  RatNumRef
class  AlgebraicNumRef
class  BitVecSortRef
 Bit-Vectors. More...
class  BitVecRef
class  BitVecNumRef
class  ArraySortRef
 Arrays. More...
class  ArrayRef
class  Datatype
class  ScopedConstructor
class  ScopedConstructorList
class  DatatypeSortRef
class  DatatypeRef
class  ParamsRef
 Parameter Sets. More...
class  ParamDescrsRef
class  Goal
class  AstVector
class  AstMap
class  FuncEntry
class  FuncInterp
class  ModelRef
class  Statistics
 Statistics. More...
class  CheckSatResult
class  Solver
class  Fixedpoint
 Fixedpoint. More...
class  ApplyResult
class  Tactic
class  Probe

Functions

def enable_trace
def disable_trace
def get_version_string
def get_version
def open_log
def append_log
def to_symbol
def main_ctx
def set_param
def reset_params
def set_option
def get_param
def is_ast
def eq
def is_sort
def DeclareSort
def is_func_decl
def Function
def is_expr
def is_app
def is_const
def is_var
def get_var_index
def is_app_of
def If
def Distinct
def Const
def Consts
def Var
def RealVar
def RealVarVector
def is_bool
def is_true
def is_false
def is_and
def is_or
def is_not
def is_eq
def is_distinct
def BoolSort
def BoolVal
def Bool
def Bools
def BoolVector
def FreshBool
def Implies
def Xor
def Not
def And
def Or
def is_pattern
def MultiPattern
def is_quantifier
def ForAll
def Exists
def is_arith_sort
def is_arith
def is_int
def is_real
def is_int_value
def is_rational_value
def is_algebraic_value
def is_add
def is_mul
def is_sub
def is_div
def is_idiv
def is_mod
def is_le
def is_lt
def is_ge
def is_gt
def is_is_int
def is_to_real
def is_to_int
def IntSort
def RealSort
def IntVal
def RealVal
def RatVal
def Q
def Int
def Ints
def IntVector
def FreshInt
def Real
def Reals
def RealVector
def FreshReal
def ToReal
def ToInt
def IsInt
def Sqrt
def Cbrt
def is_bv_sort
def is_bv
def is_bv_value
def BV2Int
def BitVecSort
def BitVecVal
def BitVec
def BitVecs
def Concat
def Extract
def ULE
def ULT
def UGE
def UGT
def UDiv
def URem
def SRem
def LShR
def RotateLeft
def RotateRight
def SignExt
def ZeroExt
def RepeatBitVec
def is_array
def is_const_array
def is_K
def is_map
def get_map_func
def ArraySort
def Array
def Update
def Store
def Select
def Map
def K
def is_select
def is_store
def CreateDatatypes
def EnumSort
def args2params
def is_as_array
def get_as_array_func
def SolverFor
def SimpleSolver
def AndThen
def Then
def OrElse
def ParOr
def ParThen
def ParAndThen
def With
def Repeat
def TryFor
def tactics
def tactic_description
def describe_tactics
def is_probe
def probes
def probe_description
def describe_probes
def FailIf
def When
def Cond
def simplify
 Utils.
def help_simplify
def simplify_param_descrs
def substitute
def substitute_vars
def Sum
def Product
def solve
def solve_using
def prove
def parse_smt2_string
def parse_smt2_file
def Interpolant
def tree_interpolant
def binary_interpolant
def sequence_interpolant

Variables

tuple _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
tuple _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
 _main_ctx = None
tuple sat = CheckSatResult(Z3_L_TRUE)
tuple unsat = CheckSatResult(Z3_L_FALSE)
tuple unknown = CheckSatResult(Z3_L_UNDEF)

Function Documentation

def z3py.And (   args)
Create a Z3 and-expression or and-probe. 

>>> p, q, r = Bools('p q r')
>>> And(p, q, r)
And(p, q, r)
>>> P = BoolVector('p', 5)
>>> And(P)
And(p__0, p__1, p__2, p__3, p__4)

Definition at line 1468 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Goal.as_expr(), Bool(), Bools(), BoolVector(), Fixedpoint.query(), tree_interpolant(), and Fixedpoint.update_rule().

01468 
01469 def And(*args):
01470     """Create a Z3 and-expression or and-probe. 
01471     
01472     >>> p, q, r = Bools('p q r')
01473     >>> And(p, q, r)
01474     And(p, q, r)
01475     >>> P = BoolVector('p', 5)
01476     >>> And(P)
01477     And(p__0, p__1, p__2, p__3, p__4)
01478     """
01479     last_arg = None
01480     if len(args) > 0:
01481         last_arg = args[len(args)-1]
01482     if isinstance(last_arg, Context):
01483         ctx = args[len(args)-1]
01484         args = args[:len(args)-1]
01485     else:
01486         ctx = main_ctx()
01487     args = _get_args(args)
01488     ctx_args  = _ctx_from_ast_arg_list(args, ctx)
01489     if __debug__:
01490         _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
01491         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
01492     if _has_probe(args):
01493         return _probe_and(args, ctx)
01494     else:
01495         args  = _coerce_expr_list(args, ctx)
01496         _args, sz = _to_ast_array(args)
01497         return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)

def z3py.AndThen (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` in sequence.

>>> x, y = Ints('x y')
>>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
>>> t(And(x == 0, y > x + 1))
[[Not(y <= 1)]]
>>> t(And(x == 0, y > x + 1)).as_expr()
Not(y <= 1)

Definition at line 6537 of file z3py.py.

Referenced by Context.Then(), and Then().

06537 
06538 def AndThen(*ts, **ks):
06539     """Return a tactic that applies the tactics in `*ts` in sequence.
06540     
06541     >>> x, y = Ints('x y')
06542     >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
06543     >>> t(And(x == 0, y > x + 1))
06544     [[Not(y <= 1)]]
06545     >>> t(And(x == 0, y > x + 1)).as_expr()
06546     Not(y <= 1)
06547     """
06548     if __debug__:
06549         _z3_assert(len(ts) >= 2, "At least two arguments expected")
06550     ctx = ks.get('ctx', None)
06551     num = len(ts)
06552     r = ts[0]
06553     for i in range(num - 1):
06554         r = _and_then(r, ts[i+1], ctx)
06555     return r

def z3py.append_log (   s)
Append user-defined string to interaction log. 

Definition at line 90 of file z3py.py.

00090 
00091 def append_log(s):
00092     """Append user-defined string to interaction log. """
00093     Z3_append_log(s)

def z3py.args2params (   arguments,
  keywords,
  ctx = None 
)
Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'

>>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
(params model true relevancy 2 elim_and true)

Definition at line 4467 of file z3py.py.

Referenced by Tactic.apply(), Fixedpoint.set(), simplify(), and With().

04467 
04468 def args2params(arguments, keywords, ctx=None):
04469     """Convert python arguments into a Z3_params object.
04470     A ':' is added to the keywords, and '_' is replaced with '-'
04471 
04472     >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
04473     (params model true relevancy 2 elim_and true)
04474     """
04475     if __debug__:
04476         _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
04477     prev = None
04478     r    = ParamsRef(ctx)
04479     for a in arguments:
04480         if prev == None:
04481             prev = a
04482         else:
04483             r.set(prev, a)
04484             prev = None
04485     for k in keywords:
04486         v = keywords[k]
04487         r.set(k, v)
04488     return r

def z3py.Array (   name,
  dom,
  rng 
)
Return an array constant named `name` with the given domain and range sorts.

>>> a = Array('a', IntSort(), IntSort())
>>> a.sort()
Array(Int, Int)
>>> a[0]
a[0]

Definition at line 3976 of file z3py.py.

Referenced by ArrayRef.__getitem__(), ArraySort(), ArrayRef.domain(), get_map_func(), is_array(), is_const_array(), is_K(), is_map(), is_select(), is_store(), K(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), Store(), and Update().

03976 
03977 def Array(name, dom, rng):
03978     """Return an array constant named `name` with the given domain and range sorts.
03979 
03980     >>> a = Array('a', IntSort(), IntSort())
03981     >>> a.sort()
03982     Array(Int, Int)
03983     >>> a[0]
03984     a[0]
03985     """
03986     s = ArraySort(dom, rng)
03987     ctx = s.ctx
03988     return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)

def z3py.ArraySort (   d,
  r 
)
Return the Z3 array sort with the given domain and range sorts.

>>> A = ArraySort(IntSort(), BoolSort())
>>> A
Array(Int, Bool)
>>> A.domain()
Int
>>> A.range()
Bool
>>> AA = ArraySort(IntSort(), A)
>>> AA
Array(Int, Array(Int, Bool))

Definition at line 3955 of file z3py.py.

Referenced by Array(), Sort.create(), ArraySortRef.domain(), Context.mkArraySort(), Context.MkArraySort(), and ArraySortRef.range().

03955 
03956 def ArraySort(d, r):
03957     """Return the Z3 array sort with the given domain and range sorts.
03958     
03959     >>> A = ArraySort(IntSort(), BoolSort())
03960     >>> A
03961     Array(Int, Bool)
03962     >>> A.domain()
03963     Int
03964     >>> A.range()
03965     Bool
03966     >>> AA = ArraySort(IntSort(), A)
03967     >>> AA
03968     Array(Int, Array(Int, Bool))
03969     """
03970     if __debug__:
03971         _z3_assert(is_sort(d), "Z3 sort expected")
03972         _z3_assert(is_sort(r), "Z3 sort expected")
03973         _z3_assert(d.ctx == r.ctx, "Context mismatch")
03974     ctx = d.ctx
03975     return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)

def z3py.binary_interpolant (   a,
  b,
  p = None,
  ctx = None 
)
Compute an interpolant for a binary conjunction.

If a & b is unsatisfiable, returns an interpolant for a & b.
This is a formula phi such that

1) a implies phi
2) b implies not phi
3) All the uninterpreted symbols of phi occur in both a and b.

If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a &b.

If parameters p are supplied, these are used in creating the
solver that determines satisfiability.

x = Int('x')
print binary_interpolant(x<0,x>2)
Not(x >= 0)

Definition at line 7368 of file z3py.py.

07368 
07369 def binary_interpolant(a,b,p=None,ctx=None):
07370     """Compute an interpolant for a binary conjunction.
07371 
07372     If a & b is unsatisfiable, returns an interpolant for a & b.
07373     This is a formula phi such that
07374 
07375     1) a implies phi
07376     2) b implies not phi
07377     3) All the uninterpreted symbols of phi occur in both a and b.
07378 
07379     If a & b is satisfiable, raises an object of class ModelRef
07380     that represents a model of a &b.
07381 
07382     If parameters p are supplied, these are used in creating the
07383     solver that determines satisfiability.
07384 
07385     x = Int('x')
07386     print binary_interpolant(x<0,x>2)
07387     Not(x >= 0)
07388     """
07389     f = And(Interpolant(a),b)
07390     return tree_interpolant(f,p,ctx)[0]

def z3py.BitVec (   name,
  bv,
  ctx = None 
)
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
If `ctx=None`, then the global context is used.

>>> x  = BitVec('x', 16)
>>> is_bv(x)
True
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> word = BitVecSort(16)
>>> x2 = BitVec('x', word)
>>> eq(x, x2)
True

Definition at line 3465 of file z3py.py.

Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__invert__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__neg__(), BitVecRef.__or__(), BitVecRef.__pos__(), BitVecRef.__radd__(), BitVecRef.__rand__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), BitVecRef.__rrshift__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BitVecs(), BitVecSort(), BV2Int(), Extract(), is_bv(), is_bv_value(), RepeatBitVec(), SignExt(), BitVecRef.size(), BitVecRef.sort(), SRem(), UDiv(), URem(), and ZeroExt().

03465 
03466 def BitVec(name, bv, ctx=None):
03467     """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
03468     If `ctx=None`, then the global context is used.
03469 
03470     >>> x  = BitVec('x', 16)
03471     >>> is_bv(x)
03472     True
03473     >>> x.size()
03474     16
03475     >>> x.sort()
03476     BitVec(16)
03477     >>> word = BitVecSort(16)
03478     >>> x2 = BitVec('x', word)
03479     >>> eq(x, x2)
03480     True
03481     """
03482     if isinstance(bv, BitVecSortRef):
03483         ctx = bv.ctx
03484     else:
03485         ctx = _get_ctx(ctx)
03486         bv = BitVecSort(bv, ctx)
03487     return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)

def z3py.BitVecs (   names,
  bv,
  ctx = None 
)
Return a tuple of bit-vector constants of size bv. 

>>> x, y, z = BitVecs('x y z', 16)
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> Sum(x, y, z)
0 + x + y + z
>>> Product(x, y, z)
1*x*y*z
>>> simplify(Product(x, y, z))
x*y*z

Definition at line 3488 of file z3py.py.

Referenced by BitVecRef.__ge__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__rshift__(), LShR(), RotateLeft(), RotateRight(), UGE(), UGT(), ULE(), and ULT().

03488 
03489 def BitVecs(names, bv, ctx=None):
03490     """Return a tuple of bit-vector constants of size bv. 
03491     
03492     >>> x, y, z = BitVecs('x y z', 16)
03493     >>> x.size()
03494     16
03495     >>> x.sort()
03496     BitVec(16)
03497     >>> Sum(x, y, z)
03498     0 + x + y + z
03499     >>> Product(x, y, z)
03500     1*x*y*z
03501     >>> simplify(Product(x, y, z))
03502     x*y*z
03503     """
03504     ctx = _get_ctx(ctx)
03505     if isinstance(names, str):
03506         names = names.split(" ")
03507     return [BitVec(name, bv, ctx) for name in names]

def z3py.BitVecSort (   sz,
  ctx = None 
)
Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.

>>> Byte = BitVecSort(8)
>>> Word = BitVecSort(16)
>>> Byte
BitVec(8)
>>> x = Const('x', Byte)
>>> eq(x, BitVec('x', 8))
True

Definition at line 3435 of file z3py.py.

Referenced by BitVec(), BitVecSortRef.cast(), Sort.create(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), and BitVecRef.sort().

03435 
03436 def BitVecSort(sz, ctx=None):
03437     """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
03438 
03439     >>> Byte = BitVecSort(8)
03440     >>> Word = BitVecSort(16)
03441     >>> Byte
03442     BitVec(8)
03443     >>> x = Const('x', Byte)
03444     >>> eq(x, BitVec('x', 8))
03445     True
03446     """
03447     ctx = _get_ctx(ctx)
03448     return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)

def z3py.BitVecVal (   val,
  bv,
  ctx = None 
)
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.

>>> v = BitVecVal(10, 32)
>>> v
10
>>> print("0x%.8x" % v.as_long())
0x0000000a

Definition at line 3449 of file z3py.py.

Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), Concat(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().

03449 
03450 def BitVecVal(val, bv, ctx=None):
03451     """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
03452     
03453     >>> v = BitVecVal(10, 32)
03454     >>> v
03455     10
03456     >>> print("0x%.8x" % v.as_long())
03457     0x0000000a
03458     """
03459     if is_bv_sort(bv):
03460         ctx = bv.ctx
03461         return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
03462     else:
03463         ctx = _get_ctx(ctx)
03464         return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)

def z3py.Bool (   name,
  ctx = None 
)
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.

>>> p = Bool('p')
>>> q = Bool('q')
>>> And(p, q)
And(p, q)

Definition at line 1360 of file z3py.py.

Referenced by Solver.assert_and_track(), and Not().

01360 
01361 def Bool(name, ctx=None):
01362     """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
01363     
01364     >>> p = Bool('p')
01365     >>> q = Bool('q')
01366     >>> And(p, q)
01367     And(p, q)
01368     """
01369     ctx = _get_ctx(ctx)
01370     return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)

def z3py.Bools (   names,
  ctx = None 
)
Return a tuple of Boolean constants. 

`names` is a single string containing all names separated by blank spaces. 
If `ctx=None`, then the global context is used.

>>> p, q, r = Bools('p q r')
>>> And(p, Or(q, r))
And(p, Or(q, r))

Definition at line 1371 of file z3py.py.

Referenced by And(), Implies(), Or(), Solver.unsat_core(), and Xor().

01371 
01372 def Bools(names, ctx=None):
01373     """Return a tuple of Boolean constants. 
01374     
01375     `names` is a single string containing all names separated by blank spaces. 
01376     If `ctx=None`, then the global context is used.
01377 
01378     >>> p, q, r = Bools('p q r')
01379     >>> And(p, Or(q, r))
01380     And(p, Or(q, r))
01381     """
01382     ctx = _get_ctx(ctx)
01383     if isinstance(names, str):
01384         names = names.split(" ")
01385     return [Bool(name, ctx) for name in names]

def z3py.BoolSort (   ctx = None)
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.

>>> BoolSort()
Bool
>>> p = Const('p', BoolSort())
>>> is_bool(p)
True
>>> r = Function('r', IntSort(), IntSort(), BoolSort())
>>> r(0, 1)
r(0, 1)
>>> is_bool(r(0, 1))
True

Definition at line 1325 of file z3py.py.

Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Bool(), Sort.create(), ArraySortRef.domain(), ArrayRef.domain(), Context.getBoolSort(), If(), IntSort(), is_arith_sort(), Context.MkBoolConst(), Context.mkBoolSort(), Context.MkBoolSort(), ArraySortRef.range(), ArrayRef.range(), and ArrayRef.sort().

01325 
01326 def BoolSort(ctx=None):
01327     """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
01328     
01329     >>> BoolSort()
01330     Bool
01331     >>> p = Const('p', BoolSort())
01332     >>> is_bool(p)
01333     True
01334     >>> r = Function('r', IntSort(), IntSort(), BoolSort())
01335     >>> r(0, 1)
01336     r(0, 1)
01337     >>> is_bool(r(0, 1))
01338     True
01339     """
01340     ctx = _get_ctx(ctx)
01341     return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)

def z3py.BoolVal (   val,
  ctx = None 
)
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.

>>> BoolVal(True)
True
>>> is_true(BoolVal(True))
True
>>> is_true(True)
False
>>> is_false(BoolVal(False))
True

Definition at line 1342 of file z3py.py.

Referenced by ApplyResult.as_expr(), BoolSortRef.cast(), and Solver.to_smt2().

01342 
01343 def BoolVal(val, ctx=None):
01344     """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
01345     
01346     >>> BoolVal(True)
01347     True
01348     >>> is_true(BoolVal(True))
01349     True
01350     >>> is_true(True)
01351     False
01352     >>> is_false(BoolVal(False))
01353     True
01354     """
01355     ctx = _get_ctx(ctx)
01356     if val == False:
01357         return BoolRef(Z3_mk_false(ctx.ref()), ctx)
01358     else:
01359         return BoolRef(Z3_mk_true(ctx.ref()), ctx)

def z3py.BoolVector (   prefix,
  sz,
  ctx = None 
)
Return a list of Boolean constants of size `sz`.

The constants are named using the given prefix.
If `ctx=None`, then the global context is used.

>>> P = BoolVector('p', 3)
>>> P
[p__0, p__1, p__2]
>>> And(P)
And(p__0, p__1, p__2)

Definition at line 1386 of file z3py.py.

Referenced by And(), and Or().

01386 
01387 def BoolVector(prefix, sz, ctx=None):
01388     """Return a list of Boolean constants of size `sz`.
01389 
01390     The constants are named using the given prefix.
01391     If `ctx=None`, then the global context is used.
01392     
01393     >>> P = BoolVector('p', 3)
01394     >>> P
01395     [p__0, p__1, p__2]
01396     >>> And(P)
01397     And(p__0, p__1, p__2)
01398     """
01399     return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]

def z3py.BV2Int (   a)
Return the Z3 expression BV2Int(a). 

>>> b = BitVec('b', 3)
>>> BV2Int(b).sort()
Int
>>> x = Int('x')
>>> x > BV2Int(b)
x > BV2Int(b)
>>> solve(x > BV2Int(b), b == 1, x < 3)
[b = 1, x = 2]

Definition at line 3417 of file z3py.py.

03417 
03418 def BV2Int(a):
03419     """Return the Z3 expression BV2Int(a). 
03420     
03421     >>> b = BitVec('b', 3)
03422     >>> BV2Int(b).sort()
03423     Int
03424     >>> x = Int('x')
03425     >>> x > BV2Int(b)
03426     x > BV2Int(b)
03427     >>> solve(x > BV2Int(b), b == 1, x < 3)
03428     [b = 1, x = 2]
03429     """
03430     if __debug__:
03431         _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
03432     ctx = a.ctx
03433     ## investigate problem with bv2int
03434     return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)

def z3py.Cbrt (   a,
  ctx = None 
)
Return a Z3 expression which represents the cubic root of a. 

>>> x = Real('x')
>>> Cbrt(x)
x**(1/3)

Definition at line 2879 of file z3py.py.

02879 
02880 def Cbrt(a, ctx=None):
02881     """ Return a Z3 expression which represents the cubic root of a. 
02882     
02883     >>> x = Real('x')
02884     >>> Cbrt(x)
02885     x**(1/3)
02886     """
02887     if not is_expr(a):
02888         ctx = _get_ctx(ctx)
02889         a = RealVal(a, ctx)
02890     return a ** "1/3"

def z3py.Concat (   args)
Create a Z3 bit-vector concatenation expression. 

>>> v = BitVecVal(1, 4)
>>> Concat(v, v+1, v)
Concat(Concat(1, 1 + 1), 1)
>>> simplify(Concat(v, v+1, v))
289
>>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
121

Definition at line 3508 of file z3py.py.

Referenced by BitVecRef.size().

03508 
03509 def Concat(*args):
03510     """Create a Z3 bit-vector concatenation expression. 
03511     
03512     >>> v = BitVecVal(1, 4)
03513     >>> Concat(v, v+1, v)
03514     Concat(Concat(1, 1 + 1), 1)
03515     >>> simplify(Concat(v, v+1, v))
03516     289
03517     >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
03518     121
03519     """
03520     args = _get_args(args)
03521     if __debug__:
03522         _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
03523         _z3_assert(len(args) >= 2, "At least two arguments expected.")
03524     ctx = args[0].ctx
03525     r   = args[0]
03526     for i in range(len(args) - 1):
03527         r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
03528     return r

def z3py.Cond (   p,
  t1,
  t2,
  ctx = None 
)
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.

>>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))

Definition at line 6940 of file z3py.py.

Referenced by If().

06940 
06941 def Cond(p, t1, t2, ctx=None):
06942     """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
06943     
06944     >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
06945     """
06946     p = _to_probe(p, ctx)
06947     t1 = _to_tactic(t1, ctx)
06948     t2 = _to_tactic(t2, ctx)
06949     return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)

def z3py.Const (   name,
  sort 
)
Create a constant of the given sort.

>>> Const('x', IntSort())
x

Definition at line 1134 of file z3py.py.

Referenced by BitVecSort(), Consts(), IntSort(), RealSort(), and DatatypeSortRef.recognizer().

01134 
01135 def Const(name, sort):
01136     """Create a constant of the given sort.
01137 
01138     >>> Const('x', IntSort())
01139     x
01140     """
01141     if __debug__:
01142         _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
01143     ctx = sort.ctx
01144     return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)

def z3py.Consts (   names,
  sort 
)
Create a several constants of the given sort. 

`names` is a string containing the names of all constants to be created. 
Blank spaces separate the names of different constants.

>>> x, y, z = Consts('x y z', IntSort())
>>> x + y + z
x + y + z

Definition at line 1145 of file z3py.py.

Referenced by ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().

01145 
01146 def Consts(names, sort):
01147     """Create a several constants of the given sort. 
01148     
01149     `names` is a string containing the names of all constants to be created. 
01150     Blank spaces separate the names of different constants.
01151     
01152     >>> x, y, z = Consts('x y z', IntSort())
01153     >>> x + y + z
01154     x + y + z
01155     """
01156     if isinstance(names, str):
01157         names = names.split(" ")
01158     return [Const(name, sort) for name in names]

def z3py.CreateDatatypes (   ds)
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.

In the following example we define a Tree-List using two mutually recursive datatypes.

>>> TreeList = Datatype('TreeList')
>>> Tree     = Datatype('Tree')
>>> # Tree has two constructors: leaf and node
>>> Tree.declare('leaf', ('val', IntSort()))
>>> # a node contains a list of trees
>>> Tree.declare('node', ('children', TreeList))
>>> TreeList.declare('nil')
>>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
>>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
>>> Tree.val(Tree.leaf(10))
val(leaf(10))
>>> simplify(Tree.val(Tree.leaf(10)))
10
>>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
>>> n1
node(cons(leaf(10), cons(leaf(20), nil)))
>>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
>>> simplify(n2 == n1)
False
>>> simplify(TreeList.car(Tree.children(n2)) == n1)
True

Definition at line 4209 of file z3py.py.

Referenced by Datatype.create().

04209 
04210 def CreateDatatypes(*ds):
04211     """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
04212     
04213     In the following example we define a Tree-List using two mutually recursive datatypes.
04214 
04215     >>> TreeList = Datatype('TreeList')
04216     >>> Tree     = Datatype('Tree')
04217     >>> # Tree has two constructors: leaf and node
04218     >>> Tree.declare('leaf', ('val', IntSort()))
04219     >>> # a node contains a list of trees
04220     >>> Tree.declare('node', ('children', TreeList))
04221     >>> TreeList.declare('nil')
04222     >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
04223     >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
04224     >>> Tree.val(Tree.leaf(10))
04225     val(leaf(10))
04226     >>> simplify(Tree.val(Tree.leaf(10)))
04227     10
04228     >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
04229     >>> n1
04230     node(cons(leaf(10), cons(leaf(20), nil)))
04231     >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
04232     >>> simplify(n2 == n1)
04233     False
04234     >>> simplify(TreeList.car(Tree.children(n2)) == n1)
04235     True
04236     """
04237     ds = _get_args(ds)
04238     if __debug__:
04239         _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
04240         _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
04241         _z3_assert(all([d.ctx == ds[0].ctx for d in  ds]), "Context mismatch")
04242         _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
04243     ctx = ds[0].ctx
04244     num    = len(ds)
04245     names  = (Symbol * num)()
04246     out    = (Sort * num)()
04247     clists = (ConstructorList * num)()
04248     to_delete = []
04249     for i in range(num):
04250         d        = ds[i]
04251         names[i] = to_symbol(d.name, ctx)
04252         num_cs   = len(d.constructors)
04253         cs       = (Constructor * num_cs)()
04254         for j in range(num_cs):
04255             c      = d.constructors[j]
04256             cname  = to_symbol(c[0], ctx)
04257             rname  = to_symbol(c[1], ctx)
04258             fs     = c[2]
04259             num_fs = len(fs)
04260             fnames = (Symbol * num_fs)()
04261             sorts  = (Sort   * num_fs)()
04262             refs   = (ctypes.c_uint * num_fs)()
04263             for k in range(num_fs):
04264                 fname = fs[k][0]
04265                 ftype = fs[k][1]
04266                 fnames[k] = to_symbol(fname, ctx)
04267                 if isinstance(ftype, Datatype):
04268                     if __debug__:
04269                         _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
04270                     sorts[k] = None
04271                     refs[k]  = ds.index(ftype)
04272                 else:
04273                     if __debug__:
04274                         _z3_assert(is_sort(ftype), "Z3 sort expected")
04275                     sorts[k] = ftype.ast
04276                     refs[k]  = 0
04277             cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
04278             to_delete.append(ScopedConstructor(cs[j], ctx))
04279         clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
04280         to_delete.append(ScopedConstructorList(clists[i], ctx))
04281     Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
04282     result = []
04283     ## Create a field for every constructor, recognizer and accessor
04284     for i in range(num):
04285         dref = DatatypeSortRef(out[i], ctx)
04286         num_cs = dref.num_constructors()
04287         for j in range(num_cs):
04288             cref       = dref.constructor(j)
04289             cref_name  = cref.name()
04290             cref_arity = cref.arity()
04291             if cref.arity() == 0:
04292                 cref = cref()
04293             setattr(dref, cref_name, cref)
04294             rref  = dref.recognizer(j)
04295             setattr(dref, rref.name(), rref)
04296             for k in range(cref_arity):
04297                 aref = dref.accessor(j, k)
04298                 setattr(dref, aref.name(), aref)
04299         result.append(dref)
04300     return tuple(result)

def z3py.DeclareSort (   name,
  ctx = None 
)
Create a new uninterpred sort named `name`.

If `ctx=None`, then the new sort is declared in the global Z3Py context.

>>> A = DeclareSort('A')
>>> a = Const('a', A)
>>> b = Const('b', A)
>>> a.sort() == A
True
>>> b.sort() == A
True
>>> a == b
a == b

Definition at line 563 of file z3py.py.

Referenced by ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().

00563 
00564 def DeclareSort(name, ctx=None):
00565     """Create a new uninterpred sort named `name`.
00566 
00567     If `ctx=None`, then the new sort is declared in the global Z3Py context.
00568 
00569     >>> A = DeclareSort('A')
00570     >>> a = Const('a', A)
00571     >>> b = Const('b', A)
00572     >>> a.sort() == A
00573     True
00574     >>> b.sort() == A
00575     True
00576     >>> a == b
00577     a == b
00578     """
00579     ctx = _get_ctx(ctx)
00580     return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)

Display a (tabular) description of all available probes in Z3.

Definition at line 6870 of file z3py.py.

06870 
06871 def describe_probes():
06872     """Display a (tabular) description of all available probes in Z3."""
06873     if in_html_mode():
06874         even = True
06875         print('<table border="1" cellpadding="2" cellspacing="0">')
06876         for p in probes():
06877             if even:
06878                 print('<tr style="background-color:#CFCFCF">')
06879                 even = False
06880             else:
06881                 print('<tr>')
06882                 even = True
06883             print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
06884         print('</table>')
06885     else:
06886         for p in probes():
06887             print('%s : %s' % (p, probe_description(p)))

Display a (tabular) description of all available tactics in Z3.

Definition at line 6682 of file z3py.py.

06682 
06683 def describe_tactics():
06684     """Display a (tabular) description of all available tactics in Z3."""
06685     if in_html_mode():
06686         even = True
06687         print('<table border="1" cellpadding="2" cellspacing="0">')
06688         for t in tactics():
06689             if even:
06690                 print('<tr style="background-color:#CFCFCF">')
06691                 even = False
06692             else:
06693                 print('<tr>')
06694                 even = True
06695             print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
06696         print('</table>')
06697     else:
06698         for t in tactics():
06699             print('%s : %s' % (t, tactic_description(t)))

def z3py.disable_trace (   msg)

Definition at line 61 of file z3py.py.

00061 
00062 def disable_trace(msg):
00063     Z3_disable_trace(msg)

def z3py.Distinct (   args)
Create a Z3 distinct expression. 

>>> x = Int('x')
>>> y = Int('y')
>>> Distinct(x, y)
x != y
>>> z = Int('z')
>>> Distinct(x, y, z)
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z))
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z), blast_distinct=True)
And(Not(x == y), Not(x == z), Not(y == z))

Definition at line 1103 of file z3py.py.

01103 
01104 def Distinct(*args):
01105     """Create a Z3 distinct expression. 
01106     
01107     >>> x = Int('x')
01108     >>> y = Int('y')
01109     >>> Distinct(x, y)
01110     x != y
01111     >>> z = Int('z')
01112     >>> Distinct(x, y, z)
01113     Distinct(x, y, z)
01114     >>> simplify(Distinct(x, y, z))
01115     Distinct(x, y, z)
01116     >>> simplify(Distinct(x, y, z), blast_distinct=True)
01117     And(Not(x == y), Not(x == z), Not(y == z))
01118     """
01119     args  = _get_args(args)
01120     ctx   = _ctx_from_ast_arg_list(args)
01121     if __debug__:
01122         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
01123     args  = _coerce_expr_list(args, ctx)
01124     _args, sz = _to_ast_array(args)
01125     return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)

def z3py.enable_trace (   msg)

Definition at line 58 of file z3py.py.

00058 
00059 def enable_trace(msg):
00060     Z3_enable_trace(msg)

def z3py.EnumSort (   name,
  values,
  ctx = None 
)
Return a new enumeration sort named `name` containing the given values.

The result is a pair (sort, list of constants).
Example:
    >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])

Definition at line 4398 of file z3py.py.

Referenced by Context.mkEnumSort(), and Context.MkEnumSort().

04398 
04399 def EnumSort(name, values, ctx=None):
04400     """Return a new enumeration sort named `name` containing the given values.
04401 
04402     The result is a pair (sort, list of constants).
04403     Example:
04404         >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
04405     """
04406     if __debug__:
04407         _z3_assert(isinstance(name, str), "Name must be a string")
04408         _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
04409         _z3_assert(len(values) > 0, "At least one value expected")
04410     ctx = _get_ctx(ctx)
04411     num = len(values)
04412     _val_names   = (Symbol * num)()
04413     for i in range(num):
04414         _val_names[i] = to_symbol(values[i])
04415     _values  = (FuncDecl * num)()
04416     _testers = (FuncDecl * num)() 
04417     name = to_symbol(name)
04418     S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
04419     V = []
04420     for i in range(num):
04421         V.append(FuncDeclRef(_values[i], ctx))
04422     V = [a() for a in V]
04423     return S, V

def z3py.eq (   a,
  b 
)
Return `True` if `a` and `b` are structurally identical AST nodes.

>>> x = Int('x')
>>> y = Int('y')
>>> eq(x, y)
False
>>> eq(x + 1, x + 1)
True
>>> eq(x + 1, 1 + x)
False
>>> eq(simplify(x + 1), simplify(1 + x))
True

Definition at line 372 of file z3py.py.

Referenced by BitVec(), BitVecSort(), FreshBool(), FreshInt(), FreshReal(), get_map_func(), Select(), and substitute().

00372 
00373 def eq(a, b):
00374     """Return `True` if `a` and `b` are structurally identical AST nodes.
00375     
00376     >>> x = Int('x')
00377     >>> y = Int('y')
00378     >>> eq(x, y)
00379     False
00380     >>> eq(x + 1, x + 1)
00381     True
00382     >>> eq(x + 1, 1 + x)
00383     False
00384     >>> eq(simplify(x + 1), simplify(1 + x))
00385     True
00386     """
00387     if __debug__:
00388         _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
00389     return a.eq(b)

def z3py.Exists (   vs,
  body,
  weight = 1,
  qid = "",
  skid = "",
  patterns = [],
  no_patterns = [] 
)
Create a Z3 exists formula.

The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = Exists([x, y], f(x, y) >= x, skid="foo")
>>> q
Exists([x, y], f(x, y) >= x)
>>> is_quantifier(q)
True
>>> r = Tactic('nnf')(q).as_expr()
>>> is_quantifier(r)
False

Definition at line 1808 of file z3py.py.

Referenced by Fixedpoint.abstract(), and QuantifierRef.is_forall().

01808 
01809 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01810     """Create a Z3 exists formula.
01811     
01812     The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
01813 
01814     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01815 
01816     >>> f = Function('f', IntSort(), IntSort(), IntSort())
01817     >>> x = Int('x')
01818     >>> y = Int('y')
01819     >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
01820     >>> q
01821     Exists([x, y], f(x, y) >= x)
01822     >>> is_quantifier(q)
01823     True
01824     >>> r = Tactic('nnf')(q).as_expr()
01825     >>> is_quantifier(r)
01826     False
01827     """
01828     return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)

def z3py.Extract (   high,
  low,
  a 
)
Create a Z3 bit-vector extraction expression.

>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)

Definition at line 3529 of file z3py.py.

03529 
03530 def Extract(high, low, a):
03531     """Create a Z3 bit-vector extraction expression.
03532 
03533     >>> x = BitVec('x', 8)
03534     >>> Extract(6, 2, x)
03535     Extract(6, 2, x)
03536     >>> Extract(6, 2, x).sort()
03537     BitVec(5)
03538     """
03539     if __debug__:
03540         _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
03541         _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
03542         _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
03543     return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)

def z3py.FailIf (   p,
  ctx = None 
)
Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.

In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.

>>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(y > 0)
>>> t(g)
[[x > 0, y > 0]]
>>> g.add(x == y + 1)
>>> t(g)
[[Not(x <= 0), Not(y <= 0), x == 1 + y]]

Definition at line 6903 of file z3py.py.

06903 
06904 def FailIf(p, ctx=None):
06905     """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
06906 
06907     In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
06908 
06909     >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
06910     >>> x, y = Ints('x y')
06911     >>> g = Goal()
06912     >>> g.add(x > 0)
06913     >>> g.add(y > 0)
06914     >>> t(g)
06915     [[x > 0, y > 0]]
06916     >>> g.add(x == y + 1)
06917     >>> t(g)
06918     [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
06919     """
06920     p = _to_probe(p, ctx)
06921     return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)

def z3py.ForAll (   vs,
  body,
  weight = 1,
  qid = "",
  skid = "",
  patterns = [],
  no_patterns = [] 
)
Create a Z3 forall formula.

The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> ForAll([x, y], f(x, y) >= x)
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, weight=10)
ForAll([x, y], f(x, y) >= x)

Definition at line 1789 of file z3py.py.

Referenced by Fixedpoint.abstract(), QuantifierRef.body(), QuantifierRef.children(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

01789 
01790 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01791     """Create a Z3 forall formula.
01792     
01793     The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
01794 
01795     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01796 
01797     >>> f = Function('f', IntSort(), IntSort(), IntSort())
01798     >>> x = Int('x')
01799     >>> y = Int('y')
01800     >>> ForAll([x, y], f(x, y) >= x)
01801     ForAll([x, y], f(x, y) >= x)
01802     >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
01803     ForAll([x, y], f(x, y) >= x)
01804     >>> ForAll([x, y], f(x, y) >= x, weight=10)
01805     ForAll([x, y], f(x, y) >= x)
01806     """
01807     return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)

def z3py.FreshBool (   prefix = 'b',
  ctx = None 
)
Return a fresh Boolean constant in the given context using the given prefix.

If `ctx=None`, then the global context is used.    

>>> b1 = FreshBool()
>>> b2 = FreshBool()
>>> eq(b1, b2)
False

Definition at line 1400 of file z3py.py.

01400 
01401 def FreshBool(prefix='b', ctx=None):
01402     """Return a fresh Boolean constant in the given context using the given prefix.
01403     
01404     If `ctx=None`, then the global context is used.    
01405 
01406     >>> b1 = FreshBool()
01407     >>> b2 = FreshBool()
01408     >>> eq(b1, b2)
01409     False
01410     """
01411     ctx = _get_ctx(ctx)
01412     return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)

def z3py.FreshInt (   prefix = 'x',
  ctx = None 
)
Return a fresh integer constant in the given context using the given prefix.

>>> x = FreshInt()
>>> y = FreshInt()
>>> eq(x, y)
False
>>> x.sort()
Int

Definition at line 2752 of file z3py.py.

02752 
02753 def FreshInt(prefix='x', ctx=None):
02754     """Return a fresh integer constant in the given context using the given prefix.
02755 
02756     >>> x = FreshInt()
02757     >>> y = FreshInt()
02758     >>> eq(x, y)
02759     False
02760     >>> x.sort()
02761     Int
02762     """
02763     ctx = _get_ctx(ctx)
02764     return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)

def z3py.FreshReal (   prefix = 'b',
  ctx = None 
)
Return a fresh real constant in the given context using the given prefix.

>>> x = FreshReal()
>>> y = FreshReal()
>>> eq(x, y)
False
>>> x.sort()
Real

Definition at line 2804 of file z3py.py.

02804 
02805 def FreshReal(prefix='b', ctx=None):
02806     """Return a fresh real constant in the given context using the given prefix.
02807 
02808     >>> x = FreshReal()
02809     >>> y = FreshReal()
02810     >>> eq(x, y)
02811     False
02812     >>> x.sort()
02813     Real
02814     """
02815     ctx = _get_ctx(ctx)
02816     return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)

def z3py.Function (   name,
  sig 
)
Create a new Z3 uninterpreted function with the given sorts. 

>>> f = Function('f', IntSort(), IntSort())
>>> f(f(0))
f(f(0))

Definition at line 701 of file z3py.py.

Referenced by ModelRef.__getitem__(), ModelRef.__len__(), FuncEntry.arg_value(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), QuantifierRef.children(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), ModelRef.get_interp(), get_map_func(), QuantifierRef.is_forall(), is_map(), is_pattern(), is_quantifier(), Map(), MultiPattern(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

00701 
00702 def Function(name, *sig):
00703     """Create a new Z3 uninterpreted function with the given sorts. 
00704     
00705     >>> f = Function('f', IntSort(), IntSort())
00706     >>> f(f(0))
00707     f(f(0))
00708     """
00709     sig = _get_args(sig)
00710     if __debug__:
00711         _z3_assert(len(sig) > 0, "At least two arguments expected")
00712     arity = len(sig) - 1
00713     rng   = sig[arity]
00714     if __debug__:
00715         _z3_assert(is_sort(rng), "Z3 sort expected")
00716     dom   = (Sort * arity)()
00717     for i in range(arity):
00718         if __debug__:
00719             _z3_assert(is_sort(sig[i]), "Z3 sort expected")
00720         dom[i] = sig[i].ast
00721     ctx = rng.ctx
00722     return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)

Return the function declaration f associated with a Z3 expression of the form (_ as-array f).

Definition at line 5533 of file z3py.py.

05533 
05534 def get_as_array_func(n):
05535     """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
05536     if __debug__:
05537         _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
05538     return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)

def z3py.get_map_func (   a)
Return the function declaration associated with a Z3 map array expression.

>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a  = Map(f, b)
>>> eq(f, get_map_func(a))
True
>>> get_map_func(a)
f
>>> get_map_func(a)(0)
f(0)

Definition at line 3938 of file z3py.py.

03938 
03939 def get_map_func(a):
03940     """Return the function declaration associated with a Z3 map array expression.
03941 
03942     >>> f = Function('f', IntSort(), IntSort())
03943     >>> b = Array('b', IntSort(), IntSort())
03944     >>> a  = Map(f, b)
03945     >>> eq(f, get_map_func(a))
03946     True
03947     >>> get_map_func(a)
03948     f
03949     >>> get_map_func(a)(0)
03950     f(0)
03951     """
03952     if __debug__:
03953         _z3_assert(is_map(a), "Z3 array map expression expected.")
03954     return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)

def z3py.get_param (   name)
Return the value of a Z3 global (or module) parameter

>>> get_param('nlsat.reorder')
'true'

Definition at line 247 of file z3py.py.

00247 
00248 def get_param(name):
00249     """Return the value of a Z3 global (or module) parameter
00250 
00251     >>> get_param('nlsat.reorder')
00252     'true'
00253     """
00254     ptr = (ctypes.c_char_p * 1)()
00255     if Z3_global_param_get(str(name), ptr):
00256         r = z3core._to_pystr(ptr[0])
00257         return r
00258     raise Z3Exception("failed to retrieve value for '%s'" % name)

def z3py.get_var_index (   a)
Return the de-Bruijn index of the Z3 bounded variable `a`.

>>> x = Int('x')
>>> y = Int('y')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> # Z3 replaces x and y with bound variables when ForAll is executed.
>>> q = ForAll([x, y], f(x, y) == x + y)
>>> q.body()
f(Var(1), Var(0)) == Var(1) + Var(0)
>>> b = q.body()
>>> b.arg(0)
f(Var(1), Var(0))
>>> v1 = b.arg(0).arg(0)
>>> v2 = b.arg(0).arg(1)
>>> v1
Var(1)
>>> v2
Var(0)
>>> get_var_index(v1)
1
>>> get_var_index(v2)
0

Definition at line 1037 of file z3py.py.

01037 
01038 def get_var_index(a):
01039     """Return the de-Bruijn index of the Z3 bounded variable `a`.
01040     
01041     >>> x = Int('x')
01042     >>> y = Int('y')
01043     >>> is_var(x)
01044     False
01045     >>> is_const(x)
01046     True
01047     >>> f = Function('f', IntSort(), IntSort(), IntSort())
01048     >>> # Z3 replaces x and y with bound variables when ForAll is executed.
01049     >>> q = ForAll([x, y], f(x, y) == x + y)
01050     >>> q.body()
01051     f(Var(1), Var(0)) == Var(1) + Var(0)
01052     >>> b = q.body()
01053     >>> b.arg(0)
01054     f(Var(1), Var(0))
01055     >>> v1 = b.arg(0).arg(0)
01056     >>> v2 = b.arg(0).arg(1)
01057     >>> v1
01058     Var(1)
01059     >>> v2
01060     Var(0)
01061     >>> get_var_index(v1)
01062     1
01063     >>> get_var_index(v2)
01064     0
01065     """
01066     if __debug__:
01067         _z3_assert(is_var(a), "Z3 bound variable expected")
01068     return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))

Definition at line 72 of file z3py.py.

00072 
00073 def get_version():
00074   major = ctypes.c_uint(0)
00075   minor = ctypes.c_uint(0)
00076   build = ctypes.c_uint(0)
00077   rev = ctypes.c_uint(0)
00078   Z3_get_version(major, minor, build, rev)
00079   return (major.value, minor.value, build.value, rev.value)
00080 
00081 # We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com

Definition at line 64 of file z3py.py.

00064 
00065 def get_version_string():
00066   major = ctypes.c_uint(0)
00067   minor = ctypes.c_uint(0)
00068   build = ctypes.c_uint(0)
00069   rev = ctypes.c_uint(0)
00070   Z3_get_version(major, minor, build, rev)
00071   return "%s.%s.%s" % (major.value, minor.value, build.value)

Return a string describing all options available for Z3 `simplify` procedure.

Definition at line 6980 of file z3py.py.

06980 
06981 def help_simplify():
06982     """Return a string describing all options available for Z3 `simplify` procedure."""
06983     print(Z3_simplify_get_help(main_ctx().ref()))

def z3py.If (   a,
  b,
  c,
  ctx = None 
)
Create a Z3 if-then-else expression. 

>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
>>> max
If(x > y, x, y)
>>> simplify(max)
If(x <= y, y, x)

Definition at line 1081 of file z3py.py.

01081 
01082 def If(a, b, c, ctx=None):
01083     """Create a Z3 if-then-else expression. 
01084     
01085     >>> x = Int('x')
01086     >>> y = Int('y')
01087     >>> max = If(x > y, x, y)
01088     >>> max
01089     If(x > y, x, y)
01090     >>> simplify(max)
01091     If(x <= y, y, x)
01092     """
01093     if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
01094         return Cond(a, b, c, ctx)
01095     else:
01096         ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
01097         s = BoolSort(ctx)
01098         a = s.cast(a)
01099         b, c = _coerce_exprs(b, c, ctx)
01100         if __debug__:
01101             _z3_assert(a.ctx == b.ctx, "Context mismatch")
01102         return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)

def z3py.Implies (   a,
  b,
  ctx = None 
)
Create a Z3 implies expression. 

>>> p, q = Bools('p q')
>>> Implies(p, q)
Implies(p, q)
>>> simplify(Implies(p, q))
Or(Not(p), q)

Definition at line 1413 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Store(), Solver.unsat_core(), Update(), and Fixedpoint.update_rule().

01413 
01414 def Implies(a, b, ctx=None):
01415     """Create a Z3 implies expression. 
01416     
01417     >>> p, q = Bools('p q')
01418     >>> Implies(p, q)
01419     Implies(p, q)
01420     >>> simplify(Implies(p, q))
01421     Or(Not(p), q)
01422     """
01423     ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
01424     s = BoolSort(ctx)
01425     a = s.cast(a)
01426     b = s.cast(b)
01427     return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.Int (   name,
  ctx = None 
)
Return an integer constant named `name`. If `ctx=None`, then the global context is used.

>>> x = Int('x')
>>> is_int(x)
True
>>> is_int(x + 1)
True

Definition at line 2717 of file z3py.py.

Referenced by ArithRef.__add__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ArithRef.__mod__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), binary_interpolant(), QuantifierRef.body(), BV2Int(), Solver.check(), QuantifierRef.children(), ModelRef.decls(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), Goal.insert(), Solver.insert(), Interpolant(), is_arith(), is_arith_sort(), is_bv(), QuantifierRef.is_forall(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_int_value(), is_pattern(), is_quantifier(), ArithSortRef.is_real(), is_real(), is_select(), is_to_real(), K(), AstMap.keys(), Statistics.keys(), Solver.model(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), Solver.pop(), AstVector.push(), Solver.push(), Solver.reason_unknown(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), sequence_interpolant(), Solver.sexpr(), Goal.simplify(), ArithRef.sort(), Solver.statistics(), Store(), ToReal(), Goal.translate(), AstVector.translate(), tree_interpolant(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

02717 
02718 def Int(name, ctx=None):
02719     """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
02720 
02721     >>> x = Int('x')
02722     >>> is_int(x)
02723     True
02724     >>> is_int(x + 1)
02725     True
02726     """
02727     ctx = _get_ctx(ctx)
02728     return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)

def z3py.Interpolant (   a,
  ctx = None 
)
Create an interpolation operator.

The argument is an interpolation pattern (see tree_interpolant). 

>>> x = Int('x')
>>> print Interpolant(x>0)
interp(x > 0)

Definition at line 7295 of file z3py.py.

Referenced by binary_interpolant(), and tree_interpolant().

07295 
07296 def Interpolant(a,ctx=None):
07297     """Create an interpolation operator.
07298     
07299     The argument is an interpolation pattern (see tree_interpolant). 
07300 
07301     >>> x = Int('x')
07302     >>> print Interpolant(x>0)
07303     interp(x > 0)
07304     """
07305     ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
07306     s = BoolSort(ctx)
07307     a = s.cast(a)
07308     return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)

def z3py.Ints (   names,
  ctx = None 
)
Return a tuple of Integer constants. 

>>> x, y, z = Ints('x y z')
>>> Sum(x, y, z)
x + y + z

Definition at line 2729 of file z3py.py.

Referenced by ArithRef.__ge__(), Goal.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ArithRef.__lt__(), Goal.depth(), Goal.get(), Goal.inconsistent(), is_add(), is_div(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Goal.prec(), Goal.size(), Store(), Solver.unsat_core(), and Update().

02729 
02730 def Ints(names, ctx=None):
02731     """Return a tuple of Integer constants. 
02732     
02733     >>> x, y, z = Ints('x y z')
02734     >>> Sum(x, y, z)
02735     x + y + z
02736     """
02737     ctx = _get_ctx(ctx)
02738     if isinstance(names, str):
02739         names = names.split(" ")
02740     return [Int(name, ctx) for name in names]

def z3py.IntSort (   ctx = None)
Return the interger sort in the given context. If `ctx=None`, then the global context is used.

>>> IntSort()
Int
>>> x = Const('x', IntSort())
>>> is_int(x)
True
>>> x.sort() == IntSort()
True
>>> x.sort() == BoolSort()
False

Definition at line 2614 of file z3py.py.

Referenced by ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), DatatypeSortRef.accessor(), FuncEntry.arg_value(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), ArithSortRef.cast(), QuantifierRef.children(), DatatypeSortRef.constructor(), Sort.create(), Datatype.create(), CreateDatatypes(), Datatype.declare(), ModelRef.decls(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), FreshInt(), ModelRef.get_interp(), get_map_func(), Context.getIntSort(), Int(), is_arith_sort(), is_array(), is_bv_sort(), is_const_array(), QuantifierRef.is_forall(), is_K(), is_map(), is_pattern(), is_quantifier(), is_select(), is_store(), K(), Map(), Context.MkInt(), Context.MkIntConst(), Context.mkIntSort(), Context.MkIntSort(), MultiPattern(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), ArraySortRef.range(), ArrayRef.range(), DatatypeSortRef.recognizer(), Select(), ArrayRef.sort(), Store(), Update(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

02614 
02615 def IntSort(ctx=None):
02616     """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
02617     
02618     >>> IntSort()
02619     Int
02620     >>> x = Const('x', IntSort())
02621     >>> is_int(x)
02622     True
02623     >>> x.sort() == IntSort()
02624     True
02625     >>> x.sort() == BoolSort()
02626     False
02627     """
02628     ctx = _get_ctx(ctx)
02629     return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)

def z3py.IntVal (   val,
  ctx = None 
)
Return a Z3 integer value. If `ctx=None`, then the global context is used.

>>> IntVal(1)
1
>>> IntVal("100")
100

Definition at line 2661 of file z3py.py.

Referenced by AstMap.__len__(), ArithRef.__mod__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), IntNumRef.as_long(), IntNumRef.as_string(), is_arith(), is_int(), is_int_value(), is_rational_value(), AstMap.keys(), and AstMap.reset().

02661 
02662 def IntVal(val, ctx=None):
02663     """Return a Z3 integer value. If `ctx=None`, then the global context is used.
02664     
02665     >>> IntVal(1)
02666     1
02667     >>> IntVal("100")
02668     100
02669     """
02670     ctx = _get_ctx(ctx)
02671     return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)

def z3py.IntVector (   prefix,
  sz,
  ctx = None 
)
Return a list of integer constants of size `sz`.

>>> X = IntVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2

Definition at line 2741 of file z3py.py.

02741 
02742 def IntVector(prefix, sz, ctx=None):
02743     """Return a list of integer constants of size `sz`.
02744     
02745     >>> X = IntVector('x', 3)
02746     >>> X
02747     [x__0, x__1, x__2]
02748     >>> Sum(X)
02749     x__0 + x__1 + x__2
02750     """
02751     return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]

def z3py.is_add (   a)
Return `True` if `a` is an expression of the form b + c.

>>> x, y = Ints('x y')
>>> is_add(x + y)
True
>>> is_add(x - y)
False

Definition at line 2318 of file z3py.py.

02318 
02319 def is_add(a):
02320     """Return `True` if `a` is an expression of the form b + c.
02321     
02322     >>> x, y = Ints('x y')
02323     >>> is_add(x + y)
02324     True
02325     >>> is_add(x - y)
02326     False
02327     """
02328     return is_app_of(a, Z3_OP_ADD)

Return `True` if `a` is an algerbraic value of sort Real.

>>> is_algebraic_value(RealVal("3/5"))
False
>>> n = simplify(Sqrt(2))
>>> n
1.4142135623?
>>> is_algebraic_value(n)
True

Definition at line 2305 of file z3py.py.

02305 
02306 def is_algebraic_value(a):
02307     """Return `True` if `a` is an algerbraic value of sort Real.
02308     
02309     >>> is_algebraic_value(RealVal("3/5"))
02310     False
02311     >>> n = simplify(Sqrt(2))
02312     >>> n
02313     1.4142135623?
02314     >>> is_algebraic_value(n)
02315     True
02316     """
02317     return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())

def z3py.is_and (   a)
Return `True` if `a` is a Z3 and expression.

>>> p, q = Bools('p q')
>>> is_and(And(p, q))
True
>>> is_and(Or(p, q))
False

Definition at line 1272 of file z3py.py.

01272 
01273 def is_and(a):
01274     """Return `True` if `a` is a Z3 and expression.
01275     
01276     >>> p, q = Bools('p q')
01277     >>> is_and(And(p, q))
01278     True
01279     >>> is_and(Or(p, q))
01280     False
01281     """
01282     return is_app_of(a, Z3_OP_AND)

def z3py.is_app (   a)
Return `True` if `a` is a Z3 function application. 

Note that, constants are function applications with 0 arguments. 

>>> a = Int('a')
>>> is_app(a)
True
>>> is_app(a + 1)
True
>>> is_app(IntSort())
False
>>> is_app(1)
False
>>> is_app(IntVal(1))
True
>>> x = Int('x')
>>> is_app(ForAll(x, x >= 0))
False

Definition at line 970 of file z3py.py.

Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), and ExprRef.num_args().

00970 
00971 def is_app(a):
00972     """Return `True` if `a` is a Z3 function application. 
00973     
00974     Note that, constants are function applications with 0 arguments. 
00975 
00976     >>> a = Int('a')
00977     >>> is_app(a)
00978     True
00979     >>> is_app(a + 1)
00980     True
00981     >>> is_app(IntSort())
00982     False
00983     >>> is_app(1)
00984     False
00985     >>> is_app(IntVal(1))
00986     True
00987     >>> x = Int('x')
00988     >>> is_app(ForAll(x, x >= 0))
00989     False
00990     """
00991     if not isinstance(a, ExprRef):
00992         return False
00993     k = _ast_kind(a.ctx, a)
00994     return k == Z3_NUMERAL_AST or k == Z3_APP_AST

def z3py.is_app_of (   a,
  k 
)
Return `True` if `a` is an application of the given kind `k`. 

>>> x = Int('x')
>>> n = x + 1
>>> is_app_of(n, Z3_OP_ADD)
True
>>> is_app_of(n, Z3_OP_MUL)
False

Definition at line 1069 of file z3py.py.

Referenced by is_add(), is_and(), is_distinct(), is_eq(), is_false(), is_not(), is_or(), and is_true().

01069 
01070 def is_app_of(a, k):
01071     """Return `True` if `a` is an application of the given kind `k`. 
01072     
01073     >>> x = Int('x')
01074     >>> n = x + 1
01075     >>> is_app_of(n, Z3_OP_ADD)
01076     True
01077     >>> is_app_of(n, Z3_OP_MUL)
01078     False
01079     """
01080     return is_app(a) and a.decl().kind() == k

def z3py.is_arith (   a)
Return `True` if `a` is an arithmetical expression.

>>> x = Int('x')
>>> is_arith(x)
True
>>> is_arith(x + 1)
True
>>> is_arith(1)
False
>>> is_arith(IntVal(1))
True
>>> y = Real('y')
>>> is_arith(y)
True
>>> is_arith(y + 1)
True

Definition at line 2199 of file z3py.py.

Referenced by is_algebraic_value().

02199 
02200 def is_arith(a):
02201     """Return `True` if `a` is an arithmetical expression.
02202     
02203     >>> x = Int('x')
02204     >>> is_arith(x)
02205     True
02206     >>> is_arith(x + 1)
02207     True
02208     >>> is_arith(1)
02209     False
02210     >>> is_arith(IntVal(1))
02211     True
02212     >>> y = Real('y')
02213     >>> is_arith(y)
02214     True
02215     >>> is_arith(y + 1)
02216     True
02217     """
02218     return isinstance(a, ArithRef)

def z3py.is_arith_sort (   s)
Return `True` if s is an arithmetical sort (type).

>>> is_arith_sort(IntSort())
True
>>> is_arith_sort(RealSort())
True
>>> is_arith_sort(BoolSort())
False
>>> n = Int('x') + 1
>>> is_arith_sort(n.sort())
True

Definition at line 1902 of file z3py.py.

01902 
01903 def is_arith_sort(s):
01904     """Return `True` if s is an arithmetical sort (type).
01905     
01906     >>> is_arith_sort(IntSort())
01907     True
01908     >>> is_arith_sort(RealSort())
01909     True
01910     >>> is_arith_sort(BoolSort())
01911     False
01912     >>> n = Int('x') + 1
01913     >>> is_arith_sort(n.sort())
01914     True
01915     """
01916     return isinstance(s, ArithSortRef)
    
def z3py.is_array (   a)
Return `True` if `a` is a Z3 array expression.

>>> a = Array('a', IntSort(), IntSort())
>>> is_array(a)
True
>>> is_array(Store(a, 0, 1))
True
>>> is_array(a[0])
False

Definition at line 3886 of file z3py.py.

03886 
03887 def is_array(a):
03888     """Return `True` if `a` is a Z3 array expression.
03889     
03890     >>> a = Array('a', IntSort(), IntSort())
03891     >>> is_array(a)
03892     True
03893     >>> is_array(Store(a, 0, 1))
03894     True
03895     >>> is_array(a[0])
03896     False
03897     """
03898     return isinstance(a, ArrayRef)

def z3py.is_as_array (   n)
Return true if n is a Z3 expression of the form (_ as-array f).

Definition at line 5529 of file z3py.py.

Referenced by get_as_array_func().

05529 
05530 def is_as_array(n):
05531     """Return true if n is a Z3 expression of the form (_ as-array f)."""
05532     return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())

def z3py.is_ast (   a)
Return `True` if `a` is an AST node.

>>> is_ast(10)
False
>>> is_ast(IntVal(10))
True
>>> is_ast(Int('x'))
True
>>> is_ast(BoolSort())
True
>>> is_ast(Function('f', IntSort(), IntSort()))
True
>>> is_ast("x")
False
>>> is_ast(Solver())
False

Definition at line 352 of file z3py.py.

Referenced by AstRef.eq(), and eq().

00352 
00353 def is_ast(a):
00354     """Return `True` if `a` is an AST node.
00355     
00356     >>> is_ast(10)
00357     False
00358     >>> is_ast(IntVal(10))
00359     True
00360     >>> is_ast(Int('x'))
00361     True
00362     >>> is_ast(BoolSort())
00363     True
00364     >>> is_ast(Function('f', IntSort(), IntSort()))
00365     True
00366     >>> is_ast("x")
00367     False
00368     >>> is_ast(Solver())
00369     False
00370     """
00371     return isinstance(a, AstRef)

def z3py.is_bool (   a)
Return `True` if `a` is a Z3 Boolean expression.

>>> p = Bool('p')
>>> is_bool(p)
True
>>> q = Bool('q')
>>> is_bool(And(p, q))
True
>>> x = Real('x')
>>> is_bool(x)
False
>>> is_bool(x == 0)
True

Definition at line 1225 of file z3py.py.

Referenced by BoolSort(), and prove().

01225 
01226 def is_bool(a):
01227     """Return `True` if `a` is a Z3 Boolean expression.
01228 
01229     >>> p = Bool('p')
01230     >>> is_bool(p)
01231     True
01232     >>> q = Bool('q')
01233     >>> is_bool(And(p, q))
01234     True
01235     >>> x = Real('x')
01236     >>> is_bool(x)
01237     False
01238     >>> is_bool(x == 0)
01239     True
01240     """
01241     return isinstance(a, BoolRef)

def z3py.is_bv (   a)
Return `True` if `a` is a Z3 bit-vector expression.

>>> b = BitVec('b', 32)
>>> is_bv(b)
True
>>> is_bv(b + 10)
True
>>> is_bv(Int('x'))
False

Definition at line 3390 of file z3py.py.

Referenced by BitVec(), BV2Int(), Concat(), Extract(), Product(), and Sum().

03390 
03391 def is_bv(a):
03392     """Return `True` if `a` is a Z3 bit-vector expression.
03393     
03394     >>> b = BitVec('b', 32)
03395     >>> is_bv(b)
03396     True
03397     >>> is_bv(b + 10)
03398     True
03399     >>> is_bv(Int('x'))
03400     False
03401     """
03402     return isinstance(a, BitVecRef)

def z3py.is_bv_sort (   s)
Return True if `s` is a Z3 bit-vector sort.

>>> is_bv_sort(BitVecSort(32))
True
>>> is_bv_sort(IntSort())
False

Definition at line 2929 of file z3py.py.

Referenced by BitVecVal().

02929 
02930 def is_bv_sort(s):
02931     """Return True if `s` is a Z3 bit-vector sort.
02932 
02933     >>> is_bv_sort(BitVecSort(32))
02934     True
02935     >>> is_bv_sort(IntSort())
02936     False
02937     """
02938     return isinstance(s, BitVecSortRef)

def z3py.is_bv_value (   a)
Return `True` if `a` is a Z3 bit-vector numeral value.

>>> b = BitVec('b', 32)
>>> is_bv_value(b)
False
>>> b = BitVecVal(10, 32)
>>> b
10
>>> is_bv_value(b)
True

Definition at line 3403 of file z3py.py.

03403 
03404 def is_bv_value(a):
03405     """Return `True` if `a` is a Z3 bit-vector numeral value.
03406 
03407     >>> b = BitVec('b', 32)
03408     >>> is_bv_value(b)
03409     False
03410     >>> b = BitVecVal(10, 32)
03411     >>> b
03412     10
03413     >>> is_bv_value(b)
03414     True
03415     """
03416     return is_bv(a) and _is_numeral(a.ctx, a.as_ast())

def z3py.is_const (   a)
Return `True` if `a` is Z3 constant/variable expression. 

>>> a = Int('a')
>>> is_const(a)
True
>>> is_const(a + 1)
False
>>> is_const(1)
False
>>> is_const(IntVal(1))
True
>>> x = Int('x')
>>> is_const(ForAll(x, x >= 0))
False

Definition at line 995 of file z3py.py.

Referenced by prove().

00995 
00996 def is_const(a):
00997     """Return `True` if `a` is Z3 constant/variable expression. 
00998     
00999     >>> a = Int('a')
01000     >>> is_const(a)
01001     True
01002     >>> is_const(a + 1)
01003     False
01004     >>> is_const(1)
01005     False
01006     >>> is_const(IntVal(1))
01007     True
01008     >>> x = Int('x')
01009     >>> is_const(ForAll(x, x >= 0))
01010     False
01011     """
01012     return is_app(a) and a.num_args() == 0

def z3py.is_const_array (   a)
Return `True` if `a` is a Z3 constant array.

>>> a = K(IntSort(), 10)
>>> is_const_array(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_const_array(a)
False

Definition at line 3899 of file z3py.py.

03899 
03900 def is_const_array(a):
03901     """Return `True` if `a` is a Z3 constant array.
03902 
03903     >>> a = K(IntSort(), 10)
03904     >>> is_const_array(a)
03905     True
03906     >>> a = Array('a', IntSort(), IntSort())
03907     >>> is_const_array(a)
03908     False
03909     """
03910     return is_app_of(a, Z3_OP_CONST_ARRAY)

def z3py.is_distinct (   a)
Return `True` if `a` is a Z3 distinct expression.

>>> x, y, z = Ints('x y z')
>>> is_distinct(x == y)
False
>>> is_distinct(Distinct(x, y, z))
True

Definition at line 1314 of file z3py.py.

01314 
01315 def is_distinct(a):
01316     """Return `True` if `a` is a Z3 distinct expression.
01317     
01318     >>> x, y, z = Ints('x y z')
01319     >>> is_distinct(x == y)
01320     False
01321     >>> is_distinct(Distinct(x, y, z))
01322     True
01323     """
01324     return is_app_of(a, Z3_OP_DISTINCT)

def z3py.is_div (   a)
Return `True` if `a` is an expression of the form b / c.

>>> x, y = Reals('x y')
>>> is_div(x / y)
True
>>> is_div(x + y)
False
>>> x, y = Ints('x y')
>>> is_div(x / y)
False
>>> is_idiv(x / y)
True

Definition at line 2351 of file z3py.py.

02351 
02352 def is_div(a):
02353     """Return `True` if `a` is an expression of the form b / c.
02354     
02355     >>> x, y = Reals('x y')
02356     >>> is_div(x / y)
02357     True
02358     >>> is_div(x + y)
02359     False
02360     >>> x, y = Ints('x y')
02361     >>> is_div(x / y)
02362     False
02363     >>> is_idiv(x / y)
02364     True
02365     """
02366     return is_app_of(a, Z3_OP_DIV)

def z3py.is_eq (   a)
Return `True` if `a` is a Z3 equality expression.

>>> x, y = Ints('x y')
>>> is_eq(x == y)
True

Definition at line 1305 of file z3py.py.

01305 
01306 def is_eq(a):
01307     """Return `True` if `a` is a Z3 equality expression.
01308     
01309     >>> x, y = Ints('x y')
01310     >>> is_eq(x == y)
01311     True
01312     """
01313     return is_app_of(a, Z3_OP_EQ)

def z3py.is_expr (   a)
Return `True` if `a` is a Z3 expression.

>>> a = Int('a')
>>> is_expr(a)
True
>>> is_expr(a + 1)
True
>>> is_expr(IntSort())
False
>>> is_expr(1)
False
>>> is_expr(IntVal(1))
True
>>> x = Int('x')
>>> is_expr(ForAll(x, x >= 0))
True

Definition at line 950 of file z3py.py.

Referenced by SortRef.cast(), BoolSortRef.cast(), Cbrt(), ExprRef.children(), is_var(), simplify(), substitute(), and substitute_vars().

00950 
00951 def is_expr(a):
00952     """Return `True` if `a` is a Z3 expression.
00953     
00954     >>> a = Int('a')
00955     >>> is_expr(a)
00956     True
00957     >>> is_expr(a + 1)
00958     True
00959     >>> is_expr(IntSort())
00960     False
00961     >>> is_expr(1)
00962     False
00963     >>> is_expr(IntVal(1))
00964     True
00965     >>> x = Int('x')
00966     >>> is_expr(ForAll(x, x >= 0))
00967     True
00968     """
00969     return isinstance(a, ExprRef)

def z3py.is_false (   a)
Return `True` if `a` is the Z3 false expression.

>>> p = Bool('p')
>>> is_false(p)
False
>>> is_false(False)
False
>>> is_false(BoolVal(False))
True

Definition at line 1259 of file z3py.py.

Referenced by BoolVal().

01259 
01260 def is_false(a):
01261     """Return `True` if `a` is the Z3 false expression.
01262 
01263     >>> p = Bool('p')
01264     >>> is_false(p)
01265     False
01266     >>> is_false(False)
01267     False
01268     >>> is_false(BoolVal(False))
01269     True
01270     """
01271     return is_app_of(a, Z3_OP_FALSE)

def z3py.is_func_decl (   a)
Return `True` if `a` is a Z3 function declaration.

>>> f = Function('f', IntSort(), IntSort())
>>> is_func_decl(f)
True
>>> x = Real('x')
>>> is_func_decl(x)
False

Definition at line 689 of file z3py.py.

Referenced by prove().

00689 
00690 def is_func_decl(a):
00691     """Return `True` if `a` is a Z3 function declaration.
00692     
00693     >>> f = Function('f', IntSort(), IntSort())
00694     >>> is_func_decl(f)
00695     True
00696     >>> x = Real('x')
00697     >>> is_func_decl(x)
00698     False
00699     """
00700     return isinstance(a, FuncDeclRef)

def z3py.is_ge (   a)
Return `True` if `a` is an expression of the form b >= c.

>>> x, y = Ints('x y')
>>> is_ge(x >= y)
True
>>> is_ge(x == y)
False

Definition at line 2411 of file z3py.py.

02411 
02412 def is_ge(a):
02413     """Return `True` if `a` is an expression of the form b >= c.
02414     
02415     >>> x, y = Ints('x y')
02416     >>> is_ge(x >= y)
02417     True
02418     >>> is_ge(x == y)
02419     False
02420     """
02421     return is_app_of(a, Z3_OP_GE)

def z3py.is_gt (   a)
Return `True` if `a` is an expression of the form b > c.

>>> x, y = Ints('x y')
>>> is_gt(x > y)
True
>>> is_gt(x == y)
False

Definition at line 2422 of file z3py.py.

02422 
02423 def is_gt(a):
02424     """Return `True` if `a` is an expression of the form b > c.
02425     
02426     >>> x, y = Ints('x y')
02427     >>> is_gt(x > y)
02428     True
02429     >>> is_gt(x == y)
02430     False
02431     """
02432     return is_app_of(a, Z3_OP_GT)

def z3py.is_idiv (   a)
Return `True` if `a` is an expression of the form b div c.

>>> x, y = Ints('x y')
>>> is_idiv(x / y)
True
>>> is_idiv(x + y)
False

Definition at line 2367 of file z3py.py.

Referenced by is_div().

02367 
02368 def is_idiv(a):
02369     """Return `True` if `a` is an expression of the form b div c.
02370     
02371     >>> x, y = Ints('x y')
02372     >>> is_idiv(x / y)
02373     True
02374     >>> is_idiv(x + y)
02375     False
02376     """
02377     return is_app_of(a, Z3_OP_IDIV)

def z3py.is_int (   a)
Return `True` if `a` is an integer expression.

>>> x = Int('x')
>>> is_int(x + 1)
True
>>> is_int(1)
False
>>> is_int(IntVal(1))
True
>>> y = Real('y')
>>> is_int(y)
False
>>> is_int(y + 1)
False

Definition at line 2219 of file z3py.py.

Referenced by Int(), IntSort(), and RealSort().

02219 
02220 def is_int(a):
02221     """Return `True` if `a` is an integer expression.
02222     
02223     >>> x = Int('x')
02224     >>> is_int(x + 1)
02225     True
02226     >>> is_int(1)
02227     False
02228     >>> is_int(IntVal(1))
02229     True
02230     >>> y = Real('y')
02231     >>> is_int(y)
02232     False
02233     >>> is_int(y + 1)
02234     False
02235     """
02236     return is_arith(a) and a.is_int()

def z3py.is_int_value (   a)
Return `True` if `a` is an integer value of sort Int.

>>> is_int_value(IntVal(1))
True
>>> is_int_value(1)
False
>>> is_int_value(Int('x'))
False
>>> n = Int('x') + 1
>>> n
x + 1
>>> n.arg(1)
1
>>> is_int_value(n.arg(1))
True
>>> is_int_value(RealVal("1/3"))
False
>>> is_int_value(RealVal(1))
False

Definition at line 2261 of file z3py.py.

02261 
02262 def is_int_value(a):
02263     """Return `True` if `a` is an integer value of sort Int.
02264     
02265     >>> is_int_value(IntVal(1))
02266     True
02267     >>> is_int_value(1)
02268     False
02269     >>> is_int_value(Int('x'))
02270     False
02271     >>> n = Int('x') + 1
02272     >>> n
02273     x + 1
02274     >>> n.arg(1)
02275     1
02276     >>> is_int_value(n.arg(1))
02277     True
02278     >>> is_int_value(RealVal("1/3"))
02279     False
02280     >>> is_int_value(RealVal(1))
02281     False
02282     """
02283     return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())

def z3py.is_is_int (   a)
Return `True` if `a` is an expression of the form IsInt(b).

>>> x = Real('x')
>>> is_is_int(IsInt(x))
True
>>> is_is_int(x)
False

Definition at line 2433 of file z3py.py.

02433 
02434 def is_is_int(a):
02435     """Return `True` if `a` is an expression of the form IsInt(b).
02436     
02437     >>> x = Real('x')
02438     >>> is_is_int(IsInt(x))
02439     True
02440     >>> is_is_int(x)
02441     False
02442     """
02443     return is_app_of(a, Z3_OP_IS_INT)

def z3py.is_K (   a)
Return `True` if `a` is a Z3 constant array.

>>> a = K(IntSort(), 10)
>>> is_K(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_K(a)
False

Definition at line 3911 of file z3py.py.

03911 
03912 def is_K(a):
03913     """Return `True` if `a` is a Z3 constant array.
03914 
03915     >>> a = K(IntSort(), 10)
03916     >>> is_K(a)
03917     True
03918     >>> a = Array('a', IntSort(), IntSort())
03919     >>> is_K(a)
03920     False
03921     """
03922     return is_app_of(a, Z3_OP_CONST_ARRAY)

def z3py.is_le (   a)
Return `True` if `a` is an expression of the form b <= c.

>>> x, y = Ints('x y')
>>> is_le(x <= y)
True
>>> is_le(x < y)
False

Definition at line 2389 of file z3py.py.

02389 
02390 def is_le(a):
02391     """Return `True` if `a` is an expression of the form b <= c.
02392     
02393     >>> x, y = Ints('x y')
02394     >>> is_le(x <= y)
02395     True
02396     >>> is_le(x < y)
02397     False
02398     """
02399     return is_app_of(a, Z3_OP_LE)

def z3py.is_lt (   a)
Return `True` if `a` is an expression of the form b < c.

>>> x, y = Ints('x y')
>>> is_lt(x < y)
True
>>> is_lt(x == y)
False

Definition at line 2400 of file z3py.py.

02400 
02401 def is_lt(a):
02402     """Return `True` if `a` is an expression of the form b < c.
02403     
02404     >>> x, y = Ints('x y')
02405     >>> is_lt(x < y)
02406     True
02407     >>> is_lt(x == y)
02408     False
02409     """
02410     return is_app_of(a, Z3_OP_LT)

def z3py.is_map (   a)
Return `True` if `a` is a Z3 map array expression. 

>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a  = Map(f, b)
>>> a
Map(f, b)
>>> is_map(a)
True
>>> is_map(b)
False

Definition at line 3923 of file z3py.py.

Referenced by get_map_func().

03923 
03924 def is_map(a):
03925     """Return `True` if `a` is a Z3 map array expression. 
03926 
03927     >>> f = Function('f', IntSort(), IntSort())
03928     >>> b = Array('b', IntSort(), IntSort())
03929     >>> a  = Map(f, b)
03930     >>> a
03931     Map(f, b)
03932     >>> is_map(a)
03933     True
03934     >>> is_map(b)
03935     False
03936     """
03937     return is_app_of(a, Z3_OP_ARRAY_MAP)

def z3py.is_mod (   a)
Return `True` if `a` is an expression of the form b % c.

>>> x, y = Ints('x y')
>>> is_mod(x % y)
True
>>> is_mod(x + y)
False

Definition at line 2378 of file z3py.py.

02378 
02379 def is_mod(a):
02380     """Return `True` if `a` is an expression of the form b % c.
02381 
02382     >>> x, y = Ints('x y')
02383     >>> is_mod(x % y)
02384     True
02385     >>> is_mod(x + y)
02386     False
02387     """
02388     return is_app_of(a, Z3_OP_MOD)

def z3py.is_mul (   a)
Return `True` if `a` is an expression of the form b * c.

>>> x, y = Ints('x y')
>>> is_mul(x * y)
True
>>> is_mul(x - y)
False

Definition at line 2329 of file z3py.py.

02329 
02330 def is_mul(a):
02331     """Return `True` if `a` is an expression of the form b * c.
02332     
02333     >>> x, y = Ints('x y')
02334     >>> is_mul(x * y)
02335     True
02336     >>> is_mul(x - y)
02337     False
02338     """
02339     return is_app_of(a, Z3_OP_MUL)

def z3py.is_not (   a)
Return `True` if `a` is a Z3 not expression.

>>> p = Bool('p')
>>> is_not(p)
False
>>> is_not(Not(p))
True

Definition at line 1294 of file z3py.py.

01294 
01295 def is_not(a):
01296     """Return `True` if `a` is a Z3 not expression.
01297     
01298     >>> p = Bool('p')
01299     >>> is_not(p)
01300     False
01301     >>> is_not(Not(p))
01302     True
01303     """
01304     return is_app_of(a, Z3_OP_NOT)

def z3py.is_or (   a)
Return `True` if `a` is a Z3 or expression.

>>> p, q = Bools('p q')
>>> is_or(Or(p, q))
True
>>> is_or(And(p, q))
False

Definition at line 1283 of file z3py.py.

01283 
01284 def is_or(a):
01285     """Return `True` if `a` is a Z3 or expression.
01286 
01287     >>> p, q = Bools('p q')
01288     >>> is_or(Or(p, q))
01289     True
01290     >>> is_or(And(p, q))
01291     False
01292     """
01293     return is_app_of(a, Z3_OP_OR)

def z3py.is_pattern (   a)
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
>>> q
ForAll(x, f(x) == 0)
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
f(Var(0))

Definition at line 1545 of file z3py.py.

Referenced by MultiPattern().

01545 
01546 def is_pattern(a):
01547     """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
01548 
01549     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01550     
01551     >>> f = Function('f', IntSort(), IntSort())
01552     >>> x = Int('x')
01553     >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
01554     >>> q
01555     ForAll(x, f(x) == 0)
01556     >>> q.num_patterns()
01557     1
01558     >>> is_pattern(q.pattern(0))
01559     True
01560     >>> q.pattern(0)
01561     f(Var(0))
01562     """
01563     return isinstance(a, PatternRef)

def z3py.is_probe (   p)
Return `True` if `p` is a Z3 probe.

>>> is_probe(Int('x'))
False
>>> is_probe(Probe('memory'))
True

Definition at line 6836 of file z3py.py.

Referenced by eq().

06836 
06837 def is_probe(p):
06838     """Return `True` if `p` is a Z3 probe.
06839     
06840     >>> is_probe(Int('x'))
06841     False
06842     >>> is_probe(Probe('memory'))
06843     True
06844     """
06845     return isinstance(p, Probe)

def z3py.is_quantifier (   a)
Return `True` if `a` is a Z3 quantifier.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> is_quantifier(q)
True
>>> is_quantifier(f(x))
False

Definition at line 1748 of file z3py.py.

Referenced by Exists().

01748 
01749 def is_quantifier(a):
01750     """Return `True` if `a` is a Z3 quantifier.
01751     
01752     >>> f = Function('f', IntSort(), IntSort())
01753     >>> x = Int('x')
01754     >>> q = ForAll(x, f(x) == 0)
01755     >>> is_quantifier(q)
01756     True
01757     >>> is_quantifier(f(x))
01758     False
01759     """
01760     return isinstance(a, QuantifierRef)

Return `True` if `a` is rational value of sort Real.

>>> is_rational_value(RealVal(1))
True
>>> is_rational_value(RealVal("3/5"))
True
>>> is_rational_value(IntVal(1))
False
>>> is_rational_value(1)
False
>>> n = Real('x') + 1
>>> n.arg(1)
1
>>> is_rational_value(n.arg(1))
True
>>> is_rational_value(Real('x'))
False

Definition at line 2284 of file z3py.py.

Referenced by RatNumRef.denominator(), and RatNumRef.numerator().

02284 
02285 def is_rational_value(a):
02286     """Return `True` if `a` is rational value of sort Real.
02287     
02288     >>> is_rational_value(RealVal(1))
02289     True
02290     >>> is_rational_value(RealVal("3/5"))
02291     True
02292     >>> is_rational_value(IntVal(1))
02293     False
02294     >>> is_rational_value(1)
02295     False
02296     >>> n = Real('x') + 1
02297     >>> n.arg(1)
02298     1
02299     >>> is_rational_value(n.arg(1))
02300     True
02301     >>> is_rational_value(Real('x'))
02302     False
02303     """
02304     return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())

def z3py.is_real (   a)
Return `True` if `a` is a real expression.

>>> x = Int('x')
>>> is_real(x + 1)
False
>>> y = Real('y')
>>> is_real(y)
True
>>> is_real(y + 1)
True
>>> is_real(1)
False
>>> is_real(RealVal(1))
True

Definition at line 2237 of file z3py.py.

Referenced by Real(), and RealSort().

02237 
02238 def is_real(a):
02239     """Return `True` if `a` is a real expression.
02240     
02241     >>> x = Int('x')
02242     >>> is_real(x + 1)
02243     False
02244     >>> y = Real('y')
02245     >>> is_real(y)
02246     True
02247     >>> is_real(y + 1)
02248     True
02249     >>> is_real(1)
02250     False
02251     >>> is_real(RealVal(1))
02252     True
02253     """
02254     return is_arith(a) and a.is_real()

def z3py.is_select (   a)
Return `True` if `a` is a Z3 array select application.

>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True

Definition at line 4083 of file z3py.py.

04083 
04084 def is_select(a):
04085     """Return `True` if `a` is a Z3 array select application.
04086     
04087     >>> a = Array('a', IntSort(), IntSort())
04088     >>> is_select(a)
04089     False
04090     >>> i = Int('i')
04091     >>> is_select(a[i])
04092     True
04093     """
04094     return is_app_of(a, Z3_OP_SELECT)

def z3py.is_sort (   s)
Return `True` if `s` is a Z3 sort.

>>> is_sort(IntSort())
True
>>> is_sort(Int('x'))
False
>>> is_expr(Int('x'))
True

Definition at line 532 of file z3py.py.

Referenced by ArraySort(), CreateDatatypes(), Function(), prove(), and Var().

00532 
00533 def is_sort(s):
00534     """Return `True` if `s` is a Z3 sort.
00535     
00536     >>> is_sort(IntSort())
00537     True
00538     >>> is_sort(Int('x'))
00539     False
00540     >>> is_expr(Int('x'))
00541     True
00542     """
00543     return isinstance(s, SortRef)

def z3py.is_store (   a)
Return `True` if `a` is a Z3 array store application.

>>> a = Array('a', IntSort(), IntSort())
>>> is_store(a)
False
>>> is_store(Store(a, 0, 1))
True

Definition at line 4095 of file z3py.py.

04095 
04096 def is_store(a):
04097     """Return `True` if `a` is a Z3 array store application.
04098     
04099     >>> a = Array('a', IntSort(), IntSort())
04100     >>> is_store(a)
04101     False
04102     >>> is_store(Store(a, 0, 1))
04103     True
04104     """
04105     return is_app_of(a, Z3_OP_STORE)

def z3py.is_sub (   a)
Return `True` if `a` is an expression of the form b - c.

>>> x, y = Ints('x y')
>>> is_sub(x - y)
True
>>> is_sub(x + y)
False

Definition at line 2340 of file z3py.py.

02340 
02341 def is_sub(a):
02342     """Return `True` if `a` is an expression of the form b - c.
02343     
02344     >>> x, y = Ints('x y')
02345     >>> is_sub(x - y)
02346     True
02347     >>> is_sub(x + y)
02348     False
02349     """
02350     return is_app_of(a, Z3_OP_SUB)

def z3py.is_to_int (   a)
Return `True` if `a` is an expression of the form ToInt(b).

>>> x = Real('x')
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> is_to_int(n)
True
>>> is_to_int(x)
False

Definition at line 2458 of file z3py.py.

02458 
02459 def is_to_int(a):
02460     """Return `True` if `a` is an expression of the form ToInt(b).
02461     
02462     >>> x = Real('x')
02463     >>> n = ToInt(x)
02464     >>> n
02465     ToInt(x)
02466     >>> is_to_int(n)
02467     True
02468     >>> is_to_int(x)
02469     False
02470     """
02471     return is_app_of(a, Z3_OP_TO_INT)

def z3py.is_to_real (   a)
Return `True` if `a` is an expression of the form ToReal(b).

>>> x = Int('x')
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> is_to_real(n)
True
>>> is_to_real(x)
False

Definition at line 2444 of file z3py.py.

02444 
02445 def is_to_real(a):
02446     """Return `True` if `a` is an expression of the form ToReal(b).
02447     
02448     >>> x = Int('x')
02449     >>> n = ToReal(x)
02450     >>> n
02451     ToReal(x)
02452     >>> is_to_real(n)
02453     True
02454     >>> is_to_real(x)
02455     False
02456     """
02457     return is_app_of(a, Z3_OP_TO_REAL)

def z3py.is_true (   a)
Return `True` if `a` is the Z3 true expression.

>>> p = Bool('p')
>>> is_true(p)
False
>>> is_true(simplify(p == p))
True
>>> x = Real('x')
>>> is_true(x == 0)
False
>>> # True is a Python Boolean expression
>>> is_true(True)
False

Definition at line 1242 of file z3py.py.

Referenced by BoolVal().

01242 
01243 def is_true(a):
01244     """Return `True` if `a` is the Z3 true expression.
01245     
01246     >>> p = Bool('p')
01247     >>> is_true(p)
01248     False
01249     >>> is_true(simplify(p == p))
01250     True
01251     >>> x = Real('x')
01252     >>> is_true(x == 0)
01253     False
01254     >>> # True is a Python Boolean expression
01255     >>> is_true(True)
01256     False
01257     """
01258     return is_app_of(a, Z3_OP_TRUE)

def z3py.is_var (   a)
Return `True` if `a` is variable. 

Z3 uses de-Bruijn indices for representing bound variables in
quantifiers.

>>> x = Int('x')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort())
>>> # Z3 replaces x with bound variables when ForAll is executed.
>>> q = ForAll(x, f(x) == x)
>>> b = q.body()
>>> b
f(Var(0)) == Var(0)
>>> b.arg(1)
Var(0)
>>> is_var(b.arg(1))
True

Definition at line 1013 of file z3py.py.

Referenced by get_var_index().

01013 
01014 def is_var(a):
01015     """Return `True` if `a` is variable. 
01016     
01017     Z3 uses de-Bruijn indices for representing bound variables in
01018     quantifiers.
01019 
01020     >>> x = Int('x')
01021     >>> is_var(x)
01022     False
01023     >>> is_const(x)
01024     True
01025     >>> f = Function('f', IntSort(), IntSort())
01026     >>> # Z3 replaces x with bound variables when ForAll is executed.
01027     >>> q = ForAll(x, f(x) == x)
01028     >>> b = q.body()
01029     >>> b
01030     f(Var(0)) == Var(0)
01031     >>> b.arg(1)
01032     Var(0)
01033     >>> is_var(b.arg(1))
01034     True
01035     """
01036     return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST

def z3py.IsInt (   a)
Return the Z3 predicate IsInt(a). 

>>> x = Real('x')
>>> IsInt(x + "1/2")
IsInt(x + 1/2)
>>> solve(IsInt(x + "1/2"), x > 0, x < 1)
[x = 1/2]
>>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
no solution

Definition at line 2851 of file z3py.py.

Referenced by is_is_int().

02851 
02852 def IsInt(a):
02853     """ Return the Z3 predicate IsInt(a). 
02854     
02855     >>> x = Real('x')
02856     >>> IsInt(x + "1/2")
02857     IsInt(x + 1/2)
02858     >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
02859     [x = 1/2]
02860     >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
02861     no solution
02862     """
02863     if __debug__:
02864         _z3_assert(a.is_real(), "Z3 real expression expected.")
02865     ctx = a.ctx
02866     return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
    
def z3py.K (   dom,
  v 
)
Return a Z3 constant array expression. 

>>> a = K(IntSort(), 10)
>>> a
K(Int, 10)
>>> a.sort()
Array(Int, Int)
>>> i = Int('i')
>>> a[i]
K(Int, 10)[i]
>>> simplify(a[i])
10

Definition at line 4062 of file z3py.py.

Referenced by is_const_array(), and is_K().

04062 
04063 def K(dom, v):
04064     """Return a Z3 constant array expression. 
04065     
04066     >>> a = K(IntSort(), 10)
04067     >>> a
04068     K(Int, 10)
04069     >>> a.sort()
04070     Array(Int, Int)
04071     >>> i = Int('i')
04072     >>> a[i]
04073     K(Int, 10)[i]
04074     >>> simplify(a[i])
04075     10
04076     """
04077     if __debug__:
04078         _z3_assert(is_sort(dom), "Z3 sort expected")
04079     ctx = dom.ctx
04080     if not is_expr(v):
04081         v = _py2expr(v, ctx)
04082     return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)

def z3py.LShR (   a,
  b 
)
Create the Z3 expression logical right shift.

Use the operator >> for the arithmetical right shift.

>>> x, y = BitVecs('x y', 32)
>>> LShR(x, y)
LShR(x, y)
>>> (x >> y).sexpr()
'(bvashr x y)'
>>> LShR(x, y).sexpr()
'(bvlshr x y)'
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> simplify(BitVecVal(4, 3) >> 1)
6
>>> simplify(LShR(BitVecVal(4, 3), 1))
2
>>> simplify(BitVecVal(2, 3) >> 1)
1
>>> simplify(LShR(BitVecVal(2, 3), 1))
1

Definition at line 3676 of file z3py.py.

Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), and BitVecRef.__rshift__().

03676 
03677 def LShR(a, b):
03678     """Create the Z3 expression logical right shift.
03679 
03680     Use the operator >> for the arithmetical right shift.
03681 
03682     >>> x, y = BitVecs('x y', 32)
03683     >>> LShR(x, y)
03684     LShR(x, y)
03685     >>> (x >> y).sexpr()
03686     '(bvashr x y)'
03687     >>> LShR(x, y).sexpr()
03688     '(bvlshr x y)'
03689     >>> BitVecVal(4, 3)
03690     4
03691     >>> BitVecVal(4, 3).as_signed_long()
03692     -4
03693     >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
03694     -2
03695     >>> simplify(BitVecVal(4, 3) >> 1)
03696     6
03697     >>> simplify(LShR(BitVecVal(4, 3), 1))
03698     2
03699     >>> simplify(BitVecVal(2, 3) >> 1)
03700     1
03701     >>> simplify(LShR(BitVecVal(2, 3), 1))
03702     1
03703     """
03704     _check_bv_args(a, b)
03705     a, b = _coerce_exprs(a, b)
03706     return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.main_ctx ( )
Return a reference to the global Z3 context. 

>>> x = Real('x')
>>> x.ctx == main_ctx()
True
>>> c = Context()
>>> c == main_ctx()
False
>>> x2 = Real('x', c)
>>> x2.ctx == c
True
>>> eq(x, x2)
False

Definition at line 188 of file z3py.py.

Referenced by And(), help_simplify(), simplify_param_descrs(), and Goal.translate().

00188 
00189 def main_ctx():
00190     """Return a reference to the global Z3 context. 
00191     
00192     >>> x = Real('x')
00193     >>> x.ctx == main_ctx()
00194     True
00195     >>> c = Context()
00196     >>> c == main_ctx()
00197     False
00198     >>> x2 = Real('x', c)
00199     >>> x2.ctx == c
00200     True
00201     >>> eq(x, x2)
00202     False
00203     """
00204     global _main_ctx
00205     if _main_ctx == None:
00206         _main_ctx = Context()
00207     return _main_ctx    

def z3py.Map (   f,
  args 
)
Return a Z3 map array expression. 

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> a1 = Array('a1', IntSort(), IntSort())
>>> a2 = Array('a2', IntSort(), IntSort())
>>> b  = Map(f, a1, a2)
>>> b
Map(f, a1, a2)
>>> prove(b[0] == f(a1[0], a2[0]))
proved

Definition at line 4040 of file z3py.py.

Referenced by Context.Context(), get_map_func(), InterpolationContext.InterpolationContext(), and is_map().

04040 
04041 def Map(f, *args):
04042     """Return a Z3 map array expression. 
04043 
04044     >>> f = Function('f', IntSort(), IntSort(), IntSort())
04045     >>> a1 = Array('a1', IntSort(), IntSort())
04046     >>> a2 = Array('a2', IntSort(), IntSort())
04047     >>> b  = Map(f, a1, a2)
04048     >>> b
04049     Map(f, a1, a2)
04050     >>> prove(b[0] == f(a1[0], a2[0]))
04051     proved
04052     """
04053     args = _get_args(args)
04054     if __debug__:
04055         _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
04056         _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
04057         _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
04058         _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
04059     _args, sz = _to_ast_array(args)
04060     ctx = f.ctx
04061     return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)

def z3py.MultiPattern (   args)
Create a Z3 multi-pattern using the given expressions `*args`

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
>>> q
ForAll(x, f(x) != g(x))
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
MultiPattern(f(Var(0)), g(Var(0)))

Definition at line 1564 of file z3py.py.

01564 
01565 def MultiPattern(*args):
01566     """Create a Z3 multi-pattern using the given expressions `*args`
01567 
01568     See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01569     
01570     >>> f = Function('f', IntSort(), IntSort())
01571     >>> g = Function('g', IntSort(), IntSort())
01572     >>> x = Int('x')
01573     >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
01574     >>> q
01575     ForAll(x, f(x) != g(x))
01576     >>> q.num_patterns()
01577     1
01578     >>> is_pattern(q.pattern(0))
01579     True
01580     >>> q.pattern(0)
01581     MultiPattern(f(Var(0)), g(Var(0)))
01582     """
01583     if __debug__:
01584         _z3_assert(len(args) > 0, "At least one argument expected")
01585         _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
01586     ctx = args[0].ctx
01587     args, sz = _to_ast_array(args)
01588     return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)

def z3py.Not (   a,
  ctx = None 
)
Create a Z3 not expression or probe. 

>>> p = Bool('p')
>>> Not(Not(p))
Not(Not(p))
>>> simplify(Not(Not(p)))
p

Definition at line 1443 of file z3py.py.

Referenced by binary_interpolant(), Implies(), prove(), sequence_interpolant(), tree_interpolant(), and Xor().

01443 
01444 def Not(a, ctx=None):
01445     """Create a Z3 not expression or probe. 
01446     
01447     >>> p = Bool('p')
01448     >>> Not(Not(p))
01449     Not(Not(p))
01450     >>> simplify(Not(Not(p)))
01451     p
01452     """
01453     ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
01454     if is_probe(a):
01455         # Not is also used to build probes
01456         return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
01457     else:
01458         s = BoolSort(ctx)
01459         a = s.cast(a)
01460         return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)

def z3py.open_log (   fname)
Log interaction to a file. This function must be invoked immediately after init(). 

Definition at line 86 of file z3py.py.

00086 
00087 def open_log(fname):
00088     """Log interaction to a file. This function must be invoked immediately after init(). """
00089     Z3_open_log(fname)

def z3py.Or (   args)
Create a Z3 or-expression or or-probe. 

>>> p, q, r = Bools('p q r')
>>> Or(p, q, r)
Or(p, q, r)
>>> P = BoolVector('p', 5)
>>> Or(P)
Or(p__0, p__1, p__2, p__3, p__4)

Definition at line 1498 of file z3py.py.

Referenced by ApplyResult.as_expr(), Bools(), and Implies().

01498 
01499 def Or(*args):
01500     """Create a Z3 or-expression or or-probe. 
01501     
01502     >>> p, q, r = Bools('p q r')
01503     >>> Or(p, q, r)
01504     Or(p, q, r)
01505     >>> P = BoolVector('p', 5)
01506     >>> Or(P)
01507     Or(p__0, p__1, p__2, p__3, p__4)
01508     """
01509     last_arg = None
01510     if len(args) > 0:
01511         last_arg = args[len(args)-1]
01512     if isinstance(last_arg, Context):
01513         ctx = args[len(args)-1]
01514         args = args[:len(args)-1]
01515     else:
01516         ctx = main_ctx()
01517     args = _get_args(args)
01518     ctx_args  = _ctx_from_ast_arg_list(args, ctx)
01519     if __debug__:
01520         _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
01521         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
01522     if _has_probe(args):
01523         return _probe_or(args, ctx)
01524     else:
01525         args  = _coerce_expr_list(args, ctx)
01526         _args, sz = _to_ast_array(args)
01527         return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)

def z3py.OrElse (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).

>>> x = Int('x')
>>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
>>> # Tactic split-clause fails if there is no clause in the given goal.
>>> t(x == 0)
[[x == 0]]
>>> t(Or(x == 0, x == 1))
[[x == 0], [x == 1]]

Definition at line 6568 of file z3py.py.

06568 
06569 def OrElse(*ts, **ks):
06570     """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
06571 
06572     >>> x = Int('x')
06573     >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
06574     >>> # Tactic split-clause fails if there is no clause in the given goal.
06575     >>> t(x == 0)
06576     [[x == 0]]
06577     >>> t(Or(x == 0, x == 1))
06578     [[x == 0], [x == 1]]
06579     """
06580     if __debug__:
06581         _z3_assert(len(ts) >= 2, "At least two arguments expected")
06582     ctx = ks.get('ctx', None)
06583     num = len(ts)
06584     r = ts[0]
06585     for i in range(num - 1):
06586         r = _or_else(r, ts[i+1], ctx)
06587     return r

def z3py.ParAndThen (   t1,
  t2,
  ctx = None 
)
Alias for ParThen(t1, t2, ctx).

Definition at line 6620 of file z3py.py.

06620 
06621 def ParAndThen(t1, t2, ctx=None):
06622     """Alias for ParThen(t1, t2, ctx)."""
06623     return ParThen(t1, t2, ctx)

def z3py.ParOr (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).

>>> x = Int('x')
>>> t = ParOr(Tactic('simplify'), Tactic('fail'))
>>> t(x + 1 == 2)
[[x == 1]]

Definition at line 6588 of file z3py.py.

06588 
06589 def ParOr(*ts, **ks):
06590     """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
06591 
06592     >>> x = Int('x')
06593     >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
06594     >>> t(x + 1 == 2)
06595     [[x == 1]]
06596     """
06597     if __debug__:
06598         _z3_assert(len(ts) >= 2, "At least two arguments expected")
06599     ctx = _get_ctx(ks.get('ctx', None))
06600     ts  = [ _to_tactic(t, ctx) for t in ts ]
06601     sz  = len(ts)
06602     _args = (TacticObj * sz)()
06603     for i in range(sz):
06604         _args[i] = ts[i].tactic
06605     return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)

def z3py.parse_smt2_file (   f,
  sorts = {},
  decls = {},
  ctx = None 
)
Parse a file in SMT 2.0 format using the given sorts and decls.

This function is similar to parse_smt2_string().

Definition at line 7285 of file z3py.py.

07285 
07286 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
07287     """Parse a file in SMT 2.0 format using the given sorts and decls.
07288     
07289     This function is similar to parse_smt2_string().
07290     """
07291     ctx = _get_ctx(ctx)
07292     ssz, snames, ssorts = _dict2sarray(sorts, ctx)
07293     dsz, dnames, ddecls = _dict2darray(decls, ctx)
07294     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
   
def z3py.parse_smt2_string (   s,
  sorts = {},
  decls = {},
  ctx = None 
)
Parse a string in SMT 2.0 format using the given sorts and decls.

The arguments sorts and decls are Python dictionaries used to initialize
the symbol table used for the SMT 2.0 parser.

>>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
And(x > 0, x < 10)
>>> x, y = Ints('x y')
>>> f = Function('f', IntSort(), IntSort())
>>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
x + f(y) > 0
>>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
a > 0

Definition at line 7265 of file z3py.py.

Referenced by parse_smt2_file().

07265 
07266 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
07267     """Parse a string in SMT 2.0 format using the given sorts and decls.
07268     
07269     The arguments sorts and decls are Python dictionaries used to initialize
07270     the symbol table used for the SMT 2.0 parser.
07271 
07272     >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
07273     And(x > 0, x < 10)
07274     >>> x, y = Ints('x y')
07275     >>> f = Function('f', IntSort(), IntSort())
07276     >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
07277     x + f(y) > 0
07278     >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
07279     a > 0
07280     """
07281     ctx = _get_ctx(ctx)
07282     ssz, snames, ssorts = _dict2sarray(sorts, ctx)
07283     dsz, dnames, ddecls = _dict2darray(decls, ctx)
07284     return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)

def z3py.ParThen (   t1,
  t2,
  ctx = None 
)
Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.

>>> x, y = Ints('x y')
>>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
>>> t(And(Or(x == 1, x == 2), y == x + 1))
[[x == 1, y == 2], [x == 2, y == 3]]

Definition at line 6606 of file z3py.py.

Referenced by ParAndThen().

06606 
06607 def ParThen(t1, t2, ctx=None):
06608     """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
06609     
06610     >>> x, y = Ints('x y')
06611     >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
06612     >>> t(And(Or(x == 1, x == 2), y == x + 1))
06613     [[x == 1, y == 2], [x == 2, y == 3]]
06614     """
06615     t1 = _to_tactic(t1, ctx)
06616     t2 = _to_tactic(t2, ctx)
06617     if __debug__:
06618         _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
06619     return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)

def z3py.probe_description (   name,
  ctx = None 
)
Return a short description for the probe named `name`.

>>> d = probe_description('memory')

Definition at line 6862 of file z3py.py.

Referenced by describe_probes().

06862 
06863 def probe_description(name, ctx=None):
06864     """Return a short description for the probe named `name`.
06865     
06866     >>> d = probe_description('memory')
06867     """
06868     ctx = _get_ctx(ctx)
06869     return Z3_probe_get_descr(ctx.ref(), name)

def z3py.probes (   ctx = None)
Return a list of all available probes in Z3.

>>> l = probes()
>>> l.count('memory') == 1
True

Definition at line 6852 of file z3py.py.

Referenced by describe_probes().

06852 
06853 def probes(ctx=None):
06854     """Return a list of all available probes in Z3.
06855     
06856     >>> l = probes()
06857     >>> l.count('memory') == 1
06858     True
06859     """
06860     ctx = _get_ctx(ctx)
06861     return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]

def z3py.Product (   args)
Create the product of the Z3 expressions. 

>>> a, b, c = Ints('a b c')
>>> Product(a, b, c)
a*b*c
>>> Product([a, b, c])
a*b*c
>>> A = IntVector('a', 5)
>>> Product(A)
a__0*a__1*a__2*a__3*a__4

Definition at line 7059 of file z3py.py.

Referenced by BitVecs().

07059 
07060 def Product(*args):
07061     """Create the product of the Z3 expressions. 
07062     
07063     >>> a, b, c = Ints('a b c')
07064     >>> Product(a, b, c)
07065     a*b*c
07066     >>> Product([a, b, c])
07067     a*b*c
07068     >>> A = IntVector('a', 5)
07069     >>> Product(A)
07070     a__0*a__1*a__2*a__3*a__4
07071     """
07072     args  = _get_args(args)
07073     if __debug__:
07074         _z3_assert(len(args) > 0, "Non empty list of arguments expected")
07075     ctx   = _ctx_from_ast_arg_list(args)
07076     if __debug__:
07077         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
07078     args  = _coerce_expr_list(args, ctx)
07079     if is_bv(args[0]):
07080         return _reduce(lambda a, b: a * b, args, 1)
07081     else:
07082         _args, sz = _to_ast_array(args)
07083         return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)

def z3py.prove (   claim,
  keywords 
)
Try to prove the given claim.

This is a simple function for creating demonstrations.  It tries to prove
`claim` by showing the negation is unsatisfiable.

>>> p, q = Bools('p q')
>>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
proved

Definition at line 7141 of file z3py.py.

Referenced by Map(), Store(), and Update().

07141 
07142 def prove(claim, **keywords):
07143     """Try to prove the given claim.
07144 
07145     This is a simple function for creating demonstrations.  It tries to prove
07146     `claim` by showing the negation is unsatisfiable.
07147 
07148     >>> p, q = Bools('p q')
07149     >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
07150     proved
07151     """
07152     if __debug__:
07153         _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
07154     s = Solver()
07155     s.set(**keywords)
07156     s.add(Not(claim))
07157     if keywords.get('show', False):
07158         print(s)
07159     r = s.check()
07160     if r == unsat:
07161         print("proved")
07162     elif r == unknown:
07163         print("failed to prove")
07164         print(s.model())
07165     else:
07166         print("counterexample")
07167         print(s.model())

def z3py.Q (   a,
  b,
  ctx = None 
)
Return a Z3 rational a/b.

If `ctx=None`, then the global context is used.

>>> Q(3,5)
3/5
>>> Q(3,5).sort()
Real

Definition at line 2705 of file z3py.py.

Referenced by RatNumRef.as_string(), RatNumRef.denominator(), and RatNumRef.numerator().

02705 
02706 def Q(a, b, ctx=None):
02707     """Return a Z3 rational a/b.
02708     
02709     If `ctx=None`, then the global context is used.
02710 
02711     >>> Q(3,5)
02712     3/5
02713     >>> Q(3,5).sort()
02714     Real
02715     """
02716     return simplify(RatVal(a, b))

def z3py.RatVal (   a,
  b,
  ctx = None 
)
Return a Z3 rational a/b.

If `ctx=None`, then the global context is used.

>>> RatVal(3,5)
3/5
>>> RatVal(3,5).sort()
Real

Definition at line 2690 of file z3py.py.

Referenced by Q().

02690 
02691 def RatVal(a, b, ctx=None):
02692     """Return a Z3 rational a/b.
02693 
02694     If `ctx=None`, then the global context is used.
02695     
02696     >>> RatVal(3,5)
02697     3/5
02698     >>> RatVal(3,5).sort()
02699     Real
02700     """
02701     if __debug__:
02702         _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
02703         _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
02704     return simplify(RealVal(a, ctx)/RealVal(b, ctx))

def z3py.Real (   name,
  ctx = None 
)
Return a real constant named `name`. If `ctx=None`, then the global context is used.

>>> x = Real('x')
>>> is_real(x)
True
>>> is_real(x + 1)
True

Definition at line 2765 of file z3py.py.

Referenced by ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_is_int(), is_rational_value(), ArithSortRef.is_real(), ArithRef.is_real(), is_real(), is_to_int(), IsInt(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().

02765 
02766 def Real(name, ctx=None):
02767     """Return a real constant named `name`. If `ctx=None`, then the global context is used.
02768 
02769     >>> x = Real('x')
02770     >>> is_real(x)
02771     True
02772     >>> is_real(x + 1)
02773     True
02774     """
02775     ctx = _get_ctx(ctx)
02776     return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)

def z3py.Reals (   names,
  ctx = None 
)
Return a tuple of real constants. 

>>> x, y, z = Reals('x y z')
>>> Sum(x, y, z)
x + y + z
>>> Sum(x, y, z).sort()
Real

Definition at line 2777 of file z3py.py.

Referenced by is_div().

02777 
02778 def Reals(names, ctx=None):
02779     """Return a tuple of real constants. 
02780     
02781     >>> x, y, z = Reals('x y z')
02782     >>> Sum(x, y, z)
02783     x + y + z
02784     >>> Sum(x, y, z).sort()
02785     Real
02786     """
02787     ctx = _get_ctx(ctx)
02788     if isinstance(names, str):
02789         names = names.split(" ")
02790     return [Real(name, ctx) for name in names]

def z3py.RealSort (   ctx = None)
Return the real sort in the given context. If `ctx=None`, then the global context is used.

>>> RealSort()
Real
>>> x = Const('x', RealSort())
>>> is_real(x)
True
>>> is_int(x)
False
>>> x.sort() == RealSort()
True

Definition at line 2630 of file z3py.py.

Referenced by ArithSortRef.cast(), Sort.create(), FreshReal(), Context.getRealSort(), is_arith_sort(), Context.MkReal(), Context.MkRealConst(), Context.mkRealSort(), Context.MkRealSort(), Real(), RealVar(), and QuantifierRef.var_sort().

02630 
02631 def RealSort(ctx=None):
02632     """Return the real sort in the given context. If `ctx=None`, then the global context is used.
02633     
02634     >>> RealSort()
02635     Real
02636     >>> x = Const('x', RealSort())
02637     >>> is_real(x)
02638     True
02639     >>> is_int(x)
02640     False
02641     >>> x.sort() == RealSort()
02642     True
02643     """
02644     ctx = _get_ctx(ctx)
02645     return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)

def z3py.RealVal (   val,
  ctx = None 
)
Return a Z3 real value. 

`val` may be a Python int, long, float or string representing a number in decimal or rational notation.
If `ctx=None`, then the global context is used.

>>> RealVal(1)
1
>>> RealVal(1).sort()
Real
>>> RealVal("3/5")
3/5
>>> RealVal("1.5")
3/2

Definition at line 2672 of file z3py.py.

Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), RatNumRef.numerator_as_long(), and RatVal().

02672 
02673 def RealVal(val, ctx=None):
02674     """Return a Z3 real value. 
02675     
02676     `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
02677     If `ctx=None`, then the global context is used.
02678     
02679     >>> RealVal(1)
02680     1
02681     >>> RealVal(1).sort()
02682     Real
02683     >>> RealVal("3/5")
02684     3/5
02685     >>> RealVal("1.5")
02686     3/2
02687     """
02688     ctx = _get_ctx(ctx)
02689     return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)

def z3py.RealVar (   idx,
  ctx = None 
)
Create a real free variable. Free variables are used to create quantified formulas.
They are also used to create polynomials.

>>> RealVar(0)
Var(0)

Definition at line 1171 of file z3py.py.

Referenced by RealVarVector().

01171 
01172 def RealVar(idx, ctx=None):
01173     """
01174     Create a real free variable. Free variables are used to create quantified formulas.
01175     They are also used to create polynomials.
01176     
01177     >>> RealVar(0)
01178     Var(0)
01179     """
01180     return Var(idx, RealSort(ctx))

def z3py.RealVarVector (   n,
  ctx = None 
)
Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1

>>> x0, x1, x2, x3 = RealVarVector(4)
>>> x2
Var(2)

Definition at line 1181 of file z3py.py.

01181 
01182 def RealVarVector(n, ctx=None):
01183     """
01184     Create a list of Real free variables.
01185     The variables have ids: 0, 1, ..., n-1
01186     
01187     >>> x0, x1, x2, x3 = RealVarVector(4)
01188     >>> x2
01189     Var(2)
01190     """
01191     return [ RealVar(i, ctx) for i in range(n) ]

def z3py.RealVector (   prefix,
  sz,
  ctx = None 
)
Return a list of real constants of size `sz`.

>>> X = RealVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
>>> Sum(X).sort()
Real

Definition at line 2791 of file z3py.py.

02791 
02792 def RealVector(prefix, sz, ctx=None):
02793     """Return a list of real constants of size `sz`.
02794     
02795     >>> X = RealVector('x', 3)
02796     >>> X
02797     [x__0, x__1, x__2]
02798     >>> Sum(X)
02799     x__0 + x__1 + x__2
02800     >>> Sum(X).sort()
02801     Real
02802     """
02803     return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]

def z3py.Repeat (   t,
  max = 4294967295,
  ctx = None 
)
Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.

>>> x, y = Ints('x y')
>>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
>>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
>>> r = t(c)
>>> for subgoal in r: print(subgoal)
[x == 0, y == 0, x > y]
[x == 0, y == 1, x > y]
[x == 1, y == 0, x > y]
[x == 1, y == 1, x > y]
>>> t = Then(t, Tactic('propagate-values'))
>>> t(c)
[[x == 1, y == 0]]

Definition at line 6637 of file z3py.py.

06637 
06638 def Repeat(t, max=4294967295, ctx=None):
06639     """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
06640 
06641     >>> x, y = Ints('x y')
06642     >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
06643     >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
06644     >>> r = t(c)
06645     >>> for subgoal in r: print(subgoal)
06646     [x == 0, y == 0, x > y]
06647     [x == 0, y == 1, x > y]
06648     [x == 1, y == 0, x > y]
06649     [x == 1, y == 1, x > y]
06650     >>> t = Then(t, Tactic('propagate-values'))
06651     >>> t(c)
06652     [[x == 1, y == 0]]
06653     """
06654     t = _to_tactic(t, ctx)
06655     return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)

def z3py.RepeatBitVec (   n,
  a 
)
Return an expression representing `n` copies of `a`.

>>> x = BitVec('x', 8)
>>> n = RepeatBitVec(4, x)
>>> n
RepeatBitVec(4, x)
>>> n.size()
32
>>> v0 = BitVecVal(10, 4)
>>> print("%.x" % v0.as_long())
a
>>> v = simplify(RepeatBitVec(4, v0))
>>> v.size()
16
>>> print("%.x" % v.as_long())
aaaa

Definition at line 3793 of file z3py.py.

03793 
03794 def RepeatBitVec(n, a):
03795     """Return an expression representing `n` copies of `a`.
03796 
03797     >>> x = BitVec('x', 8)
03798     >>> n = RepeatBitVec(4, x)
03799     >>> n
03800     RepeatBitVec(4, x)
03801     >>> n.size()
03802     32
03803     >>> v0 = BitVecVal(10, 4)
03804     >>> print("%.x" % v0.as_long())
03805     a
03806     >>> v = simplify(RepeatBitVec(4, v0))
03807     >>> v.size()
03808     16
03809     >>> print("%.x" % v.as_long())
03810     aaaa
03811     """
03812     if __debug__:
03813         _z3_assert(isinstance(n, int), "First argument must be an integer")
03814         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03815     return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)

Reset all global (or module) parameters.

Definition at line 237 of file z3py.py.

00237 
00238 def reset_params():
00239     """Reset all global (or module) parameters.
00240     """
00241     Z3_global_param_reset_all()

def z3py.RotateLeft (   a,
  b 
)
Return an expression representing `a` rotated to the left `b` times.

>>> a, b = BitVecs('a b', 16)
>>> RotateLeft(a, b)
RotateLeft(a, b)
>>> simplify(RotateLeft(a, 0))
a
>>> simplify(RotateLeft(a, 16))
a

Definition at line 3707 of file z3py.py.

03707 
03708 def RotateLeft(a, b):
03709     """Return an expression representing `a` rotated to the left `b` times.
03710 
03711     >>> a, b = BitVecs('a b', 16)
03712     >>> RotateLeft(a, b)
03713     RotateLeft(a, b)
03714     >>> simplify(RotateLeft(a, 0))
03715     a
03716     >>> simplify(RotateLeft(a, 16))
03717     a
03718     """
03719     _check_bv_args(a, b)
03720     a, b = _coerce_exprs(a, b)
03721     return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.RotateRight (   a,
  b 
)
Return an expression representing `a` rotated to the right `b` times.

>>> a, b = BitVecs('a b', 16)
>>> RotateRight(a, b)
RotateRight(a, b)
>>> simplify(RotateRight(a, 0))
a
>>> simplify(RotateRight(a, 16))
a

Definition at line 3722 of file z3py.py.

03722 
03723 def RotateRight(a, b):
03724     """Return an expression representing `a` rotated to the right `b` times.
03725 
03726     >>> a, b = BitVecs('a b', 16)
03727     >>> RotateRight(a, b)
03728     RotateRight(a, b)
03729     >>> simplify(RotateRight(a, 0))
03730     a
03731     >>> simplify(RotateRight(a, 16))
03732     a
03733     """
03734     _check_bv_args(a, b)
03735     a, b = _coerce_exprs(a, b)
03736     return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.Select (   a,
  i 
)
Return a Z3 select array expression.

>>> a = Array('a', IntSort(), IntSort())
>>> i = Int('i')
>>> Select(a, i)
a[i]
>>> eq(Select(a, i), a[i])
True

Definition at line 4026 of file z3py.py.

04026 
04027 def Select(a, i):
04028     """Return a Z3 select array expression.
04029 
04030     >>> a = Array('a', IntSort(), IntSort())
04031     >>> i = Int('i')
04032     >>> Select(a, i)
04033     a[i]
04034     >>> eq(Select(a, i), a[i])
04035     True
04036     """
04037     if __debug__:
04038         _z3_assert(is_array(a), "First argument must be a Z3 array expression")
04039     return a[i]

def z3py.sequence_interpolant (   v,
  p = None,
  ctx = None 
)
Compute interpolant for a sequence of formulas.

If len(v) == N, and if the conjunction of the formulas in v is
unsatisfiable, the interpolant is a sequence of formulas w
such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:

1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
and v[i+1]..v[n]

Requires len(v) >= 1. 

If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a & b.

If parameters p are supplied, these are used in creating the
solver that determines satisfiability.

>>> x = Int('x')
>>> y = Int('y')
>>> print sequence_interpolant([x < 0, y == x , y > 2])
[Not(x >= 0), Not(y >= 0)]

Definition at line 7391 of file z3py.py.

07391 
07392 def sequence_interpolant(v,p=None,ctx=None):
07393     """Compute interpolant for a sequence of formulas.
07394 
07395     If len(v) == N, and if the conjunction of the formulas in v is
07396     unsatisfiable, the interpolant is a sequence of formulas w
07397     such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
07398 
07399     1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
07400     2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
07401     and v[i+1]..v[n]
07402     
07403     Requires len(v) >= 1. 
07404 
07405     If a & b is satisfiable, raises an object of class ModelRef
07406     that represents a model of a & b.
07407 
07408     If parameters p are supplied, these are used in creating the
07409     solver that determines satisfiability.
07410 
07411     >>> x = Int('x')
07412     >>> y = Int('y')
07413     >>> print sequence_interpolant([x < 0, y == x , y > 2])
07414     [Not(x >= 0), Not(y >= 0)]
07415     """
07416     f = v[0]
07417     for i in range(1,len(v)):
07418         f = And(Interpolant(f),v[i])
07419     return tree_interpolant(f,p,ctx)
07420 
def z3py.set_option (   args,
  kws 
)
Alias for 'set_param' for backward compatibility.

Definition at line 242 of file z3py.py.

00242 
00243 def set_option(*args, **kws):
00244     """Alias for 'set_param' for backward compatibility.
00245     """
00246     return set_param(*args, **kws)

def z3py.set_param (   args,
  kws 
)
Set Z3 global (or module) parameters.

>>> set_param(precision=10)

Definition at line 214 of file z3py.py.

Referenced by set_option().

00214 
00215 def set_param(*args, **kws):
00216     """Set Z3 global (or module) parameters.
00217 
00218     >>> set_param(precision=10)
00219     """
00220     if __debug__:
00221         _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
00222     new_kws = {}
00223     for k in kws:
00224         v = kws[k]
00225         if not set_pp_option(k, v):
00226             new_kws[k] = v
00227     for key in new_kws:
00228         value = new_kws[key]
00229         Z3_global_param_set(str(key).upper(), _to_param_value(value))
00230     prev = None
00231     for a in args:
00232         if prev == None:
00233             prev = a
00234         else:
00235             Z3_global_param_set(str(prev), _to_param_value(a))
00236             prev = None

def z3py.SignExt (   n,
  a 
)
Return a bit-vector expression with `n` extra sign-bits.

>>> x = BitVec('x', 16)
>>> n = SignExt(8, x)
>>> n.size()
24
>>> n
SignExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(SignExt(6, v0))
>>> v
254
>>> v.size()
8
>>> print("%.x" % v.as_long())
fe

Definition at line 3737 of file z3py.py.

03737 
03738 def SignExt(n, a):
03739     """Return a bit-vector expression with `n` extra sign-bits.
03740 
03741     >>> x = BitVec('x', 16)
03742     >>> n = SignExt(8, x)
03743     >>> n.size()
03744     24
03745     >>> n
03746     SignExt(8, x)
03747     >>> n.sort()
03748     BitVec(24)
03749     >>> v0 = BitVecVal(2, 2)
03750     >>> v0
03751     2
03752     >>> v0.size()
03753     2
03754     >>> v  = simplify(SignExt(6, v0))
03755     >>> v
03756     254
03757     >>> v.size()
03758     8
03759     >>> print("%.x" % v.as_long())
03760     fe
03761     """
03762     if __debug__:
03763         _z3_assert(isinstance(n, int), "First argument must be an integer")
03764         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03765     return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)

def z3py.SimpleSolver (   ctx = None)
Return a simple general purpose solver with limited amount of preprocessing.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat

Definition at line 6073 of file z3py.py.

Referenced by Solver.reason_unknown(), and Solver.statistics().

06073 
06074 def SimpleSolver(ctx=None):
06075     """Return a simple general purpose solver with limited amount of preprocessing.
06076     
06077     >>> s = SimpleSolver()
06078     >>> x = Int('x')
06079     >>> s.add(x > 0)
06080     >>> s.check()
06081     sat
06082     """
06083     ctx = _get_ctx(ctx)
06084     return Solver(Z3_mk_simple_solver(ctx.ref()), ctx)

def z3py.simplify (   a,
  arguments,
  keywords 
)

Utils.

Simplify the expression `a` using the given options.

This function has many options. Use `help_simplify` to obtain the complete list.

>>> x = Int('x')
>>> y = Int('y')
>>> simplify(x + 1 + y + x + 1)
2 + 2*x + y
>>> simplify((x + 1)*(y + 1), som=True)
1 + x + y + x*y
>>> simplify(Distinct(x, y, 1), blast_distinct=True)
And(Not(x == y), Not(x == 1), Not(y == 1))
>>> simplify(And(x == 0, y == 1), elim_and=True)
Not(Or(Not(x == 0), Not(y == 1)))

Definition at line 6956 of file z3py.py.

Referenced by BitVecRef.__invert__(), BitVecRef.__lshift__(), ArithRef.__mod__(), ArithRef.__neg__(), BitVecRef.__neg__(), ArithRef.__pow__(), ArithRef.__rpow__(), BitVecRef.__rshift__(), AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), BitVecs(), Concat(), CreateDatatypes(), Implies(), is_algebraic_value(), K(), LShR(), Not(), Q(), RatVal(), DatatypeSortRef.recognizer(), RepeatBitVec(), RotateLeft(), RotateRight(), SignExt(), Xor(), and ZeroExt().

06956 
06957 def simplify(a, *arguments, **keywords):
06958     """Simplify the expression `a` using the given options.
06959 
06960     This function has many options. Use `help_simplify` to obtain the complete list.
06961     
06962     >>> x = Int('x')
06963     >>> y = Int('y')
06964     >>> simplify(x + 1 + y + x + 1)
06965     2 + 2*x + y
06966     >>> simplify((x + 1)*(y + 1), som=True)
06967     1 + x + y + x*y
06968     >>> simplify(Distinct(x, y, 1), blast_distinct=True)
06969     And(Not(x == y), Not(x == 1), Not(y == 1))
06970     >>> simplify(And(x == 0, y == 1), elim_and=True)
06971     Not(Or(Not(x == 0), Not(y == 1)))
06972     """
06973     if __debug__:
06974         _z3_assert(is_expr(a), "Z3 expression expected")
06975     if len(arguments) > 0 or len(keywords) > 0:
06976         p = args2params(arguments, keywords, a.ctx)
06977         return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
06978     else:
06979         return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)

Return the set of parameter descriptions for Z3 `simplify` procedure.

Definition at line 6984 of file z3py.py.

06984 
06985 def simplify_param_descrs():
06986     """Return the set of parameter descriptions for Z3 `simplify` procedure."""
06987     return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())

def z3py.solve (   args,
  keywords 
)
Solve the constraints `*args`.

This is a simple function for creating demonstrations. It creates a solver,
configure it using the options in `keywords`, adds the constraints
in `args`, and invokes check.

>>> a = Int('a')
>>> solve(a > 0, a < 2)
[a = 1]

Definition at line 7084 of file z3py.py.

Referenced by BV2Int(), and IsInt().

07084 
07085 def solve(*args, **keywords):
07086     """Solve the constraints `*args`.
07087     
07088     This is a simple function for creating demonstrations. It creates a solver,
07089     configure it using the options in `keywords`, adds the constraints
07090     in `args`, and invokes check.
07091     
07092     >>> a = Int('a')
07093     >>> solve(a > 0, a < 2)
07094     [a = 1]
07095     """
07096     s = Solver()
07097     s.set(**keywords)
07098     s.add(*args)
07099     if keywords.get('show', False):
07100         print(s)
07101     r = s.check()
07102     if r == unsat:
07103         print("no solution")
07104     elif r == unknown:
07105         print("failed to solve")
07106         try:
07107             print(s.model())
07108         except Z3Exception:
07109             return
07110     else:
07111         print(s.model())

def z3py.solve_using (   s,
  args,
  keywords 
)
Solve the constraints `*args` using solver `s`.

This is a simple function for creating demonstrations. It is similar to `solve`,
but it uses the given solver `s`.
It configures solver `s` using the options in `keywords`, adds the constraints
in `args`, and invokes check.

Definition at line 7112 of file z3py.py.

07112 
07113 def solve_using(s, *args, **keywords):
07114     """Solve the constraints `*args` using solver `s`.
07115     
07116     This is a simple function for creating demonstrations. It is similar to `solve`,
07117     but it uses the given solver `s`.
07118     It configures solver `s` using the options in `keywords`, adds the constraints
07119     in `args`, and invokes check.
07120     """
07121     if __debug__:
07122         _z3_assert(isinstance(s, Solver), "Solver object expected")
07123     s.set(**keywords)
07124     s.add(*args)
07125     if keywords.get('show', False):
07126         print("Problem:")
07127         print(s)
07128     r = s.check()
07129     if r == unsat:
07130         print("no solution")
07131     elif r == unknown:
07132         print("failed to solve")
07133         try:
07134             print(s.model())
07135         except Z3Exception:
07136             return
07137     else:
07138         if keywords.get('show', False):
07139             print("Solution:")
07140         print(s.model())

def z3py.SolverFor (   logic,
  ctx = None 
)
Create a solver customized for the given logic. 

The parameter `logic` is a string. It should be contains
the name of a SMT-LIB logic.
See http://www.smtlib.org/ for the name of all available logics.

>>> s = SolverFor("QF_LIA")
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> s.check()
sat
>>> s.model()
[x = 1]

Definition at line 6053 of file z3py.py.

06053 
06054 def SolverFor(logic, ctx=None):
06055     """Create a solver customized for the given logic. 
06056 
06057     The parameter `logic` is a string. It should be contains
06058     the name of a SMT-LIB logic.
06059     See http://www.smtlib.org/ for the name of all available logics.
06060 
06061     >>> s = SolverFor("QF_LIA")
06062     >>> x = Int('x')
06063     >>> s.add(x > 0)
06064     >>> s.add(x < 2)
06065     >>> s.check()
06066     sat
06067     >>> s.model()
06068     [x = 1]
06069     """
06070     ctx = _get_ctx(ctx)
06071     logic = to_symbol(logic)
06072     return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx)

def z3py.Sqrt (   a,
  ctx = None 
)
Return a Z3 expression which represents the square root of a. 

>>> x = Real('x')
>>> Sqrt(x)
x**(1/2)

Definition at line 2867 of file z3py.py.

Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), and is_algebraic_value().

02867 
02868 def Sqrt(a, ctx=None):
02869     """ Return a Z3 expression which represents the square root of a. 
02870     
02871     >>> x = Real('x')
02872     >>> Sqrt(x)
02873     x**(1/2)
02874     """
02875     if not is_expr(a):
02876         ctx = _get_ctx(ctx)
02877         a = RealVal(a, ctx)
02878     return a ** "1/2"

def z3py.SRem (   a,
  b 
)
Create the Z3 expression signed remainder.

Use the operator % for signed modulus, and URem() for unsigned remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SRem(x, y)
SRem(x, y)
>>> SRem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'

Definition at line 3656 of file z3py.py.

Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and URem().

03656 
03657 def SRem(a, b):
03658     """Create the Z3 expression signed remainder.
03659     
03660     Use the operator % for signed modulus, and URem() for unsigned remainder.
03661     
03662     >>> x = BitVec('x', 32)
03663     >>> y = BitVec('y', 32)
03664     >>> SRem(x, y)
03665     SRem(x, y)
03666     >>> SRem(x, y).sort()
03667     BitVec(32)
03668     >>> (x % y).sexpr()
03669     '(bvsmod x y)'
03670     >>> SRem(x, y).sexpr()
03671     '(bvsrem x y)'
03672     """
03673     _check_bv_args(a, b)
03674     a, b = _coerce_exprs(a, b)
03675     return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.Store (   a,
  i,
  v 
)
Return a Z3 store array expression.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Store(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

Definition at line 4010 of file z3py.py.

Referenced by is_array(), and is_store().

04010 
04011 def Store(a, i, v):
04012     """Return a Z3 store array expression.
04013 
04014     >>> a    = Array('a', IntSort(), IntSort())
04015     >>> i, v = Ints('i v')
04016     >>> s    = Store(a, i, v)
04017     >>> s.sort()
04018     Array(Int, Int)
04019     >>> prove(s[i] == v)
04020     proved
04021     >>> j    = Int('j')
04022     >>> prove(Implies(i != j, s[j] == a[j]))
04023     proved
04024     """
04025     return Update(a, i, v)

def z3py.substitute (   t,
  m 
)
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.

>>> x = Int('x')
>>> y = Int('y')
>>> substitute(x + 1, (x, y + 1))
y + 1 + 1
>>> f = Function('f', IntSort(), IntSort())
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
1 + 1

Definition at line 6988 of file z3py.py.

06988 
06989 def substitute(t, *m):
06990     """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.
06991     
06992     >>> x = Int('x')
06993     >>> y = Int('y')
06994     >>> substitute(x + 1, (x, y + 1))
06995     y + 1 + 1
06996     >>> f = Function('f', IntSort(), IntSort())
06997     >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
06998     1 + 1
06999     """
07000     if isinstance(m, tuple):
07001         m1 = _get_args(m)
07002         if isinstance(m1, list):
07003             m = m1
07004     if __debug__:
07005         _z3_assert(is_expr(t), "Z3 expression expected")
07006         _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.")
07007     num = len(m)
07008     _from = (Ast * num)()
07009     _to   = (Ast * num)()
07010     for i in range(num):
07011         _from[i] = m[i][0].as_ast()
07012         _to[i]   = m[i][1].as_ast()
07013     return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)

def z3py.substitute_vars (   t,
  m 
)
Substitute the free variables in t with the expression in m.

>>> v0 = Var(0, IntSort())
>>> v1 = Var(1, IntSort())
>>> x  = Int('x')
>>> f  = Function('f', IntSort(), IntSort(), IntSort())
>>> # replace v0 with x+1 and v1 with x
>>> substitute_vars(f(v0, v1), x + 1, x)
f(x + 1, x)

Definition at line 7014 of file z3py.py.

07014 
07015 def substitute_vars(t, *m):
07016     """Substitute the free variables in t with the expression in m.
07017     
07018     >>> v0 = Var(0, IntSort())
07019     >>> v1 = Var(1, IntSort())
07020     >>> x  = Int('x')
07021     >>> f  = Function('f', IntSort(), IntSort(), IntSort())
07022     >>> # replace v0 with x+1 and v1 with x
07023     >>> substitute_vars(f(v0, v1), x + 1, x)
07024     f(x + 1, x)
07025     """
07026     if __debug__:
07027         _z3_assert(is_expr(t), "Z3 expression expected")
07028         _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
07029     num = len(m)
07030     _to   = (Ast * num)()
07031     for i in range(num):
07032         _to[i] = m[i].as_ast()
07033     return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)

def z3py.Sum (   args)
Create the sum of the Z3 expressions. 

>>> a, b, c = Ints('a b c')
>>> Sum(a, b, c)
a + b + c
>>> Sum([a, b, c])
a + b + c
>>> A = IntVector('a', 5)
>>> Sum(A)
a__0 + a__1 + a__2 + a__3 + a__4

Definition at line 7034 of file z3py.py.

Referenced by BitVecs(), Ints(), IntVector(), Reals(), and RealVector().

07034 
07035 def Sum(*args):
07036     """Create the sum of the Z3 expressions. 
07037     
07038     >>> a, b, c = Ints('a b c')
07039     >>> Sum(a, b, c)
07040     a + b + c
07041     >>> Sum([a, b, c])
07042     a + b + c
07043     >>> A = IntVector('a', 5)
07044     >>> Sum(A)
07045     a__0 + a__1 + a__2 + a__3 + a__4
07046     """
07047     args  = _get_args(args)
07048     if __debug__:
07049         _z3_assert(len(args) > 0, "Non empty list of arguments expected")
07050     ctx   = _ctx_from_ast_arg_list(args)
07051     if __debug__:
07052         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
07053     args  = _coerce_expr_list(args, ctx)
07054     if is_bv(args[0]):
07055         return _reduce(lambda a, b: a + b, args, 0)
07056     else:
07057         _args, sz = _to_ast_array(args)
07058         return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)

def z3py.tactic_description (   name,
  ctx = None 
)
Return a short description for the tactic named `name`.

>>> d = tactic_description('simplify')

Definition at line 6674 of file z3py.py.

Referenced by describe_tactics().

06674 
06675 def tactic_description(name, ctx=None):
06676     """Return a short description for the tactic named `name`.
06677 
06678     >>> d = tactic_description('simplify')
06679     """
06680     ctx = _get_ctx(ctx)
06681     return Z3_tactic_get_descr(ctx.ref(), name)

def z3py.tactics (   ctx = None)
Return a list of all available tactics in Z3.

>>> l = tactics()
>>> l.count('simplify') == 1
True

Definition at line 6664 of file z3py.py.

Referenced by describe_tactics().

06664 
06665 def tactics(ctx=None):
06666     """Return a list of all available tactics in Z3.
06667     
06668     >>> l = tactics()
06669     >>> l.count('simplify') == 1
06670     True
06671     """
06672     ctx = _get_ctx(ctx)
06673     return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]

def z3py.Then (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).

>>> x, y = Ints('x y')
>>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
>>> t(And(x == 0, y > x + 1))
[[Not(y <= 1)]]
>>> t(And(x == 0, y > x + 1)).as_expr()
Not(y <= 1)

Definition at line 6556 of file z3py.py.

Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), Goal.depth(), Statistics.get_key_value(), and Statistics.keys().

06556 
06557 def Then(*ts, **ks):
06558     """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
06559     
06560     >>> x, y = Ints('x y')
06561     >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
06562     >>> t(And(x == 0, y > x + 1))
06563     [[Not(y <= 1)]]
06564     >>> t(And(x == 0, y > x + 1)).as_expr()
06565     Not(y <= 1)
06566     """
06567     return AndThen(*ts, **ks)
    
def z3py.to_symbol (   s,
  ctx = None 
)
Convert an integer or string into a Z3 symbol.

Definition at line 94 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DeclareSort(), EnumSort(), Function(), Int(), prove(), Real(), Fixedpoint.set_predicate_representation(), SolverFor(), and Fixedpoint.update_rule().

00094 
00095 def to_symbol(s, ctx=None):
00096     """Convert an integer or string into a Z3 symbol."""
00097     if isinstance(s, int):
00098         return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
00099     else:
00100         return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)

def z3py.ToInt (   a)
Return the Z3 expression ToInt(a). 

>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int

Definition at line 2834 of file z3py.py.

Referenced by is_to_int().

02834 
02835 def ToInt(a):
02836     """ Return the Z3 expression ToInt(a). 
02837     
02838     >>> x = Real('x')
02839     >>> x.sort()
02840     Real
02841     >>> n = ToInt(x)
02842     >>> n
02843     ToInt(x)
02844     >>> n.sort()
02845     Int
02846     """
02847     if __debug__:
02848         _z3_assert(a.is_real(), "Z3 real expression expected.")
02849     ctx = a.ctx
02850     return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)

def z3py.ToReal (   a)
Return the Z3 expression ToReal(a). 

>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real

Definition at line 2817 of file z3py.py.

Referenced by ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), and is_to_real().

02817 
02818 def ToReal(a):
02819     """ Return the Z3 expression ToReal(a). 
02820     
02821     >>> x = Int('x')
02822     >>> x.sort()
02823     Int
02824     >>> n = ToReal(x)
02825     >>> n
02826     ToReal(x)
02827     >>> n.sort()
02828     Real
02829     """
02830     if __debug__:
02831         _z3_assert(a.is_int(), "Z3 integer expression expected.")
02832     ctx = a.ctx
02833     return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)

def z3py.tree_interpolant (   pat,
  p = None,
  ctx = None 
)
Compute interpolant for a tree of formulas.

The input is an interpolation pattern over a set of formulas C.
The pattern pat is a formula combining the formulas in C using
logical conjunction and the "interp" operator (see Interp). This
interp operator is logically the identity operator. It marks the
sub-formulas of the pattern for which interpolants should be
computed. The interpolant is a map sigma from marked subformulas
to formulas, such that, for each marked subformula phi of pat
(where phi sigma is phi with sigma(psi) substituted for each
subformula psi of phi such that psi in dom(sigma)):

  1) phi sigma implies sigma(phi), and

  2) sigma(phi) is in the common uninterpreted vocabulary between
  the formulas of C occurring in phi and those not occurring in
  phi

  and moreover pat sigma implies false. In the simplest case
  an interpolant for the pattern "(and (interp A) B)" maps A
  to an interpolant for A /\ B. 

  The return value is a vector of formulas representing sigma. This
  vector contains sigma(phi) for each marked subformula of pat, in
  pre-order traversal. This means that subformulas of phi occur before phi
  in the vector. Also, subformulas that occur multiply in pat will
  occur multiply in the result vector.

If pat is satisfiable, raises an object of class ModelRef
that represents a model of pat.

If parameters p are supplied, these are used in creating the
solver that determines satisfiability.

>>> x = Int('x')
>>> y = Int('y')
>>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
[Not(x >= 0), Not(y <= 2)]

>>> g = And(Interpolant(x<0),x<2)
>>> try:
...     print tree_interpolant(g).sexpr()
... except ModelRef as m:
...     print m.sexpr()
(define-fun x () Int
  (- 1))

Definition at line 7309 of file z3py.py.

Referenced by binary_interpolant(), and sequence_interpolant().

07309 
07310 def tree_interpolant(pat,p=None,ctx=None):
07311     """Compute interpolant for a tree of formulas.
07312 
07313     The input is an interpolation pattern over a set of formulas C.
07314     The pattern pat is a formula combining the formulas in C using
07315     logical conjunction and the "interp" operator (see Interp). This
07316     interp operator is logically the identity operator. It marks the
07317     sub-formulas of the pattern for which interpolants should be
07318     computed. The interpolant is a map sigma from marked subformulas
07319     to formulas, such that, for each marked subformula phi of pat
07320     (where phi sigma is phi with sigma(psi) substituted for each
07321     subformula psi of phi such that psi in dom(sigma)):
07322 
07323       1) phi sigma implies sigma(phi), and
07324 
07325       2) sigma(phi) is in the common uninterpreted vocabulary between
07326       the formulas of C occurring in phi and those not occurring in
07327       phi
07328 
07329       and moreover pat sigma implies false. In the simplest case
07330       an interpolant for the pattern "(and (interp A) B)" maps A
07331       to an interpolant for A /\ B. 
07332 
07333       The return value is a vector of formulas representing sigma. This
07334       vector contains sigma(phi) for each marked subformula of pat, in
07335       pre-order traversal. This means that subformulas of phi occur before phi
07336       in the vector. Also, subformulas that occur multiply in pat will
07337       occur multiply in the result vector.
07338 
07339     If pat is satisfiable, raises an object of class ModelRef
07340     that represents a model of pat.
07341 
07342     If parameters p are supplied, these are used in creating the
07343     solver that determines satisfiability.
07344 
07345     >>> x = Int('x')
07346     >>> y = Int('y')
07347     >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
07348     [Not(x >= 0), Not(y <= 2)]
07349 
07350     >>> g = And(Interpolant(x<0),x<2)
07351     >>> try:
07352     ...     print tree_interpolant(g).sexpr()
07353     ... except ModelRef as m:
07354     ...     print m.sexpr()
07355     (define-fun x () Int
07356       (- 1))
07357     """
07358     f = pat
07359     ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
07360     ptr = (AstVectorObj * 1)()
07361     mptr = (Model * 1)()
07362     if p == None:
07363         p = ParamsRef(ctx)
07364     res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
07365     if res == Z3_L_FALSE:
07366         return AstVector(ptr[0],ctx)
07367     raise ModelRef(mptr[0], ctx)

def z3py.TryFor (   t,
  ms,
  ctx = None 
)
Return a tactic that applies `t` to a given goal for `ms` milliseconds.

If `t` does not terminate in `ms` milliseconds, then it fails.

Definition at line 6656 of file z3py.py.

06656 
06657 def TryFor(t, ms, ctx=None):
06658     """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
06659     
06660     If `t` does not terminate in `ms` milliseconds, then it fails.
06661     """
06662     t = _to_tactic(t, ctx)
06663     return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)

def z3py.UDiv (   a,
  b 
)
Create the Z3 expression (unsigned) division `self / other`.

Use the operator / for signed division.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> UDiv(x, y)
UDiv(x, y)
>>> UDiv(x, y).sort()
BitVec(32)
>>> (x / y).sexpr()
'(bvsdiv x y)'
>>> UDiv(x, y).sexpr()
'(bvudiv x y)'

Definition at line 3616 of file z3py.py.

Referenced by BitVecRef.__div__(), and BitVecRef.__rdiv__().

03616 
03617 def UDiv(a, b):
03618     """Create the Z3 expression (unsigned) division `self / other`.
03619     
03620     Use the operator / for signed division.
03621     
03622     >>> x = BitVec('x', 32)
03623     >>> y = BitVec('y', 32)
03624     >>> UDiv(x, y)
03625     UDiv(x, y)
03626     >>> UDiv(x, y).sort()
03627     BitVec(32)
03628     >>> (x / y).sexpr()
03629     '(bvsdiv x y)'
03630     >>> UDiv(x, y).sexpr()
03631     '(bvudiv x y)'
03632     """
03633     _check_bv_args(a, b)
03634     a, b = _coerce_exprs(a, b)
03635     return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.UGE (   a,
  b 
)
Create the Z3 expression (unsigned) `other >= self`.

Use the operator >= for signed greater than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> UGE(x, y)
UGE(x, y)
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'

Definition at line 3582 of file z3py.py.

Referenced by BitVecRef.__ge__().

03582 
03583 def UGE(a, b):
03584     """Create the Z3 expression (unsigned) `other >= self`.
03585     
03586     Use the operator >= for signed greater than or equal to.
03587     
03588     >>> x, y = BitVecs('x y', 32)
03589     >>> UGE(x, y)
03590     UGE(x, y)
03591     >>> (x >= y).sexpr()
03592     '(bvsge x y)'
03593     >>> UGE(x, y).sexpr()
03594     '(bvuge x y)'
03595     """
03596     _check_bv_args(a, b)
03597     a, b = _coerce_exprs(a, b)
03598     return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.UGT (   a,
  b 
)
Create the Z3 expression (unsigned) `other > self`.

Use the operator > for signed greater than.

>>> x, y = BitVecs('x y', 32)
>>> UGT(x, y)
UGT(x, y)
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'

Definition at line 3599 of file z3py.py.

Referenced by BitVecRef.__gt__().

03599 
03600 def UGT(a, b):
03601     """Create the Z3 expression (unsigned) `other > self`.
03602     
03603     Use the operator > for signed greater than.
03604     
03605     >>> x, y = BitVecs('x y', 32)
03606     >>> UGT(x, y)
03607     UGT(x, y)
03608     >>> (x > y).sexpr()
03609     '(bvsgt x y)'
03610     >>> UGT(x, y).sexpr()
03611     '(bvugt x y)'
03612     """
03613     _check_bv_args(a, b)
03614     a, b = _coerce_exprs(a, b)
03615     return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.ULE (   a,
  b 
)
Create the Z3 expression (unsigned) `other <= self`.

Use the operator <= for signed less than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> ULE(x, y)
ULE(x, y)
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'

Definition at line 3548 of file z3py.py.

Referenced by BitVecRef.__le__().

03548 
03549 def ULE(a, b):
03550     """Create the Z3 expression (unsigned) `other <= self`.
03551     
03552     Use the operator <= for signed less than or equal to.
03553     
03554     >>> x, y = BitVecs('x y', 32)
03555     >>> ULE(x, y)
03556     ULE(x, y)
03557     >>> (x <= y).sexpr()
03558     '(bvsle x y)'
03559     >>> ULE(x, y).sexpr()
03560     '(bvule x y)'
03561     """
03562     _check_bv_args(a, b)
03563     a, b = _coerce_exprs(a, b)
03564     return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.ULT (   a,
  b 
)
Create the Z3 expression (unsigned) `other < self`.

Use the operator < for signed less than.

>>> x, y = BitVecs('x y', 32)
>>> ULT(x, y)
ULT(x, y)
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'

Definition at line 3565 of file z3py.py.

Referenced by BitVecRef.__lt__().

03565 
03566 def ULT(a, b):
03567     """Create the Z3 expression (unsigned) `other < self`.
03568     
03569     Use the operator < for signed less than.
03570     
03571     >>> x, y = BitVecs('x y', 32)
03572     >>> ULT(x, y)
03573     ULT(x, y)
03574     >>> (x < y).sexpr()
03575     '(bvslt x y)'
03576     >>> ULT(x, y).sexpr()
03577     '(bvult x y)'
03578     """
03579     _check_bv_args(a, b)
03580     a, b = _coerce_exprs(a, b)
03581     return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.Update (   a,
  i,
  v 
)
Return a Z3 store array expression.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Update(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

Definition at line 3989 of file z3py.py.

Referenced by Store().

03989 
03990 def Update(a, i, v):
03991     """Return a Z3 store array expression.
03992 
03993     >>> a    = Array('a', IntSort(), IntSort())
03994     >>> i, v = Ints('i v')
03995     >>> s    = Update(a, i, v)
03996     >>> s.sort()
03997     Array(Int, Int)
03998     >>> prove(s[i] == v)
03999     proved
04000     >>> j    = Int('j')
04001     >>> prove(Implies(i != j, s[j] == a[j]))
04002     proved
04003     """
04004     if __debug__:
04005         _z3_assert(is_array(a), "First argument must be a Z3 array expression")
04006     i = a.domain().cast(i)
04007     v = a.range().cast(v)
04008     ctx = a.ctx
04009     return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)

def z3py.URem (   a,
  b 
)
Create the Z3 expression (unsigned) remainder `self % other`.

Use the operator % for signed modulus, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> URem(x, y)
URem(x, y)
>>> URem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'

Definition at line 3636 of file z3py.py.

Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and SRem().

03636 
03637 def URem(a, b):
03638     """Create the Z3 expression (unsigned) remainder `self % other`.
03639     
03640     Use the operator % for signed modulus, and SRem() for signed remainder.
03641     
03642     >>> x = BitVec('x', 32)
03643     >>> y = BitVec('y', 32)
03644     >>> URem(x, y)
03645     URem(x, y)
03646     >>> URem(x, y).sort()
03647     BitVec(32)
03648     >>> (x % y).sexpr()
03649     '(bvsmod x y)'
03650     >>> URem(x, y).sexpr()
03651     '(bvurem x y)'
03652     """
03653     _check_bv_args(a, b)
03654     a, b = _coerce_exprs(a, b)
03655     return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.Var (   idx,
  s 
)
Create a Z3 free variable. Free variables are used to create quantified formulas.

>>> Var(0, IntSort())
Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort()))
False

Definition at line 1159 of file z3py.py.

Referenced by QuantifierRef.body(), QuantifierRef.children(), is_pattern(), MultiPattern(), QuantifierRef.pattern(), and RealVar().

01159 
01160 def Var(idx, s):
01161     """Create a Z3 free variable. Free variables are used to create quantified formulas.
01162     
01163     >>> Var(0, IntSort())
01164     Var(0)
01165     >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
01166     False
01167     """
01168     if __debug__:
01169         _z3_assert(is_sort(s), "Z3 sort expected")
01170     return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)

def z3py.When (   p,
  t,
  ctx = None 
)
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.

>>> t = When(Probe('size') > 2, Tactic('simplify'))
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(y > 0)
>>> t(g)
[[x > 0, y > 0]]
>>> g.add(x == y + 1)
>>> t(g)
[[Not(x <= 0), Not(y <= 0), x == 1 + y]]

Definition at line 6922 of file z3py.py.

06922 
06923 def When(p, t, ctx=None):
06924     """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
06925     
06926     >>> t = When(Probe('size') > 2, Tactic('simplify'))
06927     >>> x, y = Ints('x y')
06928     >>> g = Goal()
06929     >>> g.add(x > 0)
06930     >>> g.add(y > 0)
06931     >>> t(g)
06932     [[x > 0, y > 0]]
06933     >>> g.add(x == y + 1)
06934     >>> t(g)
06935     [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
06936     """
06937     p = _to_probe(p, ctx)
06938     t = _to_tactic(t, ctx)
06939     return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)

def z3py.With (   t,
  args,
  keys 
)
Return a tactic that applies tactic `t` using the given configuration options.

>>> x, y = Ints('x y')
>>> t = With(Tactic('simplify'), som=True)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]

Definition at line 6624 of file z3py.py.

Referenced by Goal.prec().

06624 
06625 def With(t, *args, **keys):
06626     """Return a tactic that applies tactic `t` using the given configuration options.
06627     
06628     >>> x, y = Ints('x y')
06629     >>> t = With(Tactic('simplify'), som=True)
06630     >>> t((x + 1)*(y + 2) == 0)
06631     [[2*x + y + x*y == -2]]
06632     """
06633     ctx = keys.get('ctx', None)
06634     t = _to_tactic(t, ctx)
06635     p = args2params(args, keys, t.ctx)
06636     return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)

def z3py.Xor (   a,
  b,
  ctx = None 
)
Create a Z3 Xor expression.

>>> p, q = Bools('p q')
>>> Xor(p, q)
Xor(p, q)
>>> simplify(Xor(p, q))
Not(p) == q

Definition at line 1428 of file z3py.py.

01428 
01429 def Xor(a, b, ctx=None):
01430     """Create a Z3 Xor expression.
01431 
01432     >>> p, q = Bools('p q')
01433     >>> Xor(p, q)
01434     Xor(p, q)
01435     >>> simplify(Xor(p, q))
01436     Not(p) == q
01437     """
01438     ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
01439     s = BoolSort(ctx)
01440     a = s.cast(a)
01441     b = s.cast(b)
01442     return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.ZeroExt (   n,
  a 
)
Return a bit-vector expression with `n` extra zero-bits.

>>> x = BitVec('x', 16)
>>> n = ZeroExt(8, x)
>>> n.size()
24
>>> n
ZeroExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(ZeroExt(6, v0))
>>> v
2
>>> v.size()
8

Definition at line 3766 of file z3py.py.

03766 
03767 def ZeroExt(n, a):
03768     """Return a bit-vector expression with `n` extra zero-bits.
03769 
03770     >>> x = BitVec('x', 16)
03771     >>> n = ZeroExt(8, x)
03772     >>> n.size()
03773     24
03774     >>> n
03775     ZeroExt(8, x)
03776     >>> n.sort()
03777     BitVec(24)
03778     >>> v0 = BitVecVal(2, 2)
03779     >>> v0
03780     2
03781     >>> v0.size()
03782     2
03783     >>> v  = simplify(ZeroExt(6, v0))
03784     >>> v
03785     2
03786     >>> v.size()
03787     8
03788     """
03789     if __debug__:
03790         _z3_assert(isinstance(n, int), "First argument must be an integer")
03791         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03792     return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)


Variable Documentation

tuple _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)

Definition at line 108 of file z3py.py.

_main_ctx = None

Definition at line 187 of file z3py.py.

tuple _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)

Definition at line 126 of file z3py.py.

Definition at line 5711 of file z3py.py.

Definition at line 5713 of file z3py.py.

Definition at line 5712 of file z3py.py.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines