Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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_option
 
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 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_select
 
def is_store
 
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 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
 

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 1392 of file z3py.py.

Referenced by Goal.as_expr(), Bool(), Bools(), and BoolVector().

1393 def And(*args):
1394  """Create a Z3 and-expression or and-probe.
1395 
1396  >>> p, q, r = Bools('p q r')
1397  >>> And(p, q, r)
1398  And(p, q, r)
1399  >>> P = BoolVector('p', 5)
1400  >>> And(P)
1401  And(p__0, p__1, p__2, p__3, p__4)
1402  """
1403  args = _get_args(args)
1404  ctx = _ctx_from_ast_arg_list(args)
1405  if __debug__:
1406  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1407  if _has_probe(args):
1408  return _probe_and(args, ctx)
1409  else:
1410  args = _coerce_expr_list(args, ctx)
1411  _args, sz = _to_ast_array(args)
1412  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 6421 of file z3py.py.

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

6422 def AndThen(*ts, **ks):
6423  """Return a tactic that applies the tactics in `*ts` in sequence.
6424 
6425  >>> x, y = Ints('x y')
6426  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
6427  >>> t(And(x == 0, y > x + 1))
6428  [[Not(y <= 1)]]
6429  >>> t(And(x == 0, y > x + 1)).as_expr()
6430  Not(y <= 1)
6431  """
6432  if __debug__:
6433  _z3_assert(len(ts) >= 2, "At least two arguments expected")
6434  ctx = ks.get('ctx', None)
6435  num = len(ts)
6436  r = ts[0]
6437  for i in range(num - 1):
6438  r = _and_then(r, ts[i+1], ctx)
6439  return r
def z3py.append_log (   s)
Append user-defined string to interaction log. 

Definition at line 78 of file z3py.py.

78 
79 def append_log(s):
80  """Append user-defined string to interaction log. """
81  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 1 :relevancy 2 :elim-and 1)

Definition at line 4383 of file z3py.py.

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

4384 def args2params(arguments, keywords, ctx=None):
4385  """Convert python arguments into a Z3_params object.
4386  A ':' is added to the keywords, and '_' is replaced with '-'
4387 
4388  >>> args2params([':model', True, ':relevancy', 2], {'elim_and' : True})
4389  (params :model 1 :relevancy 2 :elim-and 1)
4390  """
4391  if __debug__:
4392  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
4393  prev = None
4394  r = ParamsRef(ctx)
4395  for a in arguments:
4396  if prev == None:
4397  prev = a
4398  else:
4399  r.set(prev, a)
4400  prev = None
4401  for k, v in keywords.iteritems():
4402  k = ':' + k.replace('_', '-')
4403  r.set(k, v)
4404  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 3894 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().

3895 def Array(name, dom, rng):
3896  """Return an array constant named `name` with the given domain and range sorts.
3897 
3898  >>> a = Array('a', IntSort(), IntSort())
3899  >>> a.sort()
3900  Array(Int, Int)
3901  >>> a[0]
3902  a[0]
3903  """
3904  s = ArraySort(dom, rng)
3905  ctx = s.ctx
3906  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 3873 of file z3py.py.

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

3874 def ArraySort(d, r):
3875  """Return the Z3 array sort with the given domain and range sorts.
3876 
3877  >>> A = ArraySort(IntSort(), BoolSort())
3878  >>> A
3879  Array(Int, Bool)
3880  >>> A.domain()
3881  Int
3882  >>> A.range()
3883  Bool
3884  >>> AA = ArraySort(IntSort(), A)
3885  >>> AA
3886  Array(Int, Array(Int, Bool))
3887  """
3888  if __debug__:
3889  _z3_assert(is_sort(d), "Z3 sort expected")
3890  _z3_assert(is_sort(r), "Z3 sort expected")
3891  _z3_assert(d.ctx == r.ctx, "Context mismatch")
3892  ctx = d.ctx
3893  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
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 3357 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().

3358 def BitVec(name, bv, ctx=None):
3359  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3360  If `ctx=None`, then the global context is used.
3361 
3362  >>> x = BitVec('x', 16)
3363  >>> is_bv(x)
3364  True
3365  >>> x.size()
3366  16
3367  >>> x.sort()
3368  BitVec(16)
3369  >>> word = BitVecSort(16)
3370  >>> x2 = BitVec('x', word)
3371  >>> eq(x, x2)
3372  True
3373  """
3374  if isinstance(bv, BitVecSortRef):
3375  ctx = bv.ctx
3376  else:
3377  ctx = _get_ctx(ctx)
3378  bv = BitVecSort(bv, ctx)
3379  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 3380 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().

3381 def BitVecs(names, bv, ctx=None):
3382  """Return a tuple of bit-vector constants of size bv.
3383 
3384  >>> x, y, z = BitVecs('x y z', 16)
3385  >>> x.size()
3386  16
3387  >>> x.sort()
3388  BitVec(16)
3389  >>> Sum(x, y, z)
3390  0 + x + y + z
3391  >>> Product(x, y, z)
3392  1*x*y*z
3393  >>> simplify(Product(x, y, z))
3394  x*y*z
3395  """
3396  ctx = _get_ctx(ctx)
3397  if isinstance(names, str):
3398  names = names.split(" ")
3399  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 3327 of file z3py.py.

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

3328 def BitVecSort(sz, ctx=None):
3329  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3330 
3331  >>> Byte = BitVecSort(8)
3332  >>> Word = BitVecSort(16)
3333  >>> Byte
3334  BitVec(8)
3335  >>> x = Const('x', Byte)
3336  >>> eq(x, BitVec('x', 8))
3337  True
3338  """
3339  ctx = _get_ctx(ctx)
3340  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 3341 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().

3342 def BitVecVal(val, bv, ctx=None):
3343  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3344 
3345  >>> v = BitVecVal(10, 32)
3346  >>> v
3347  10
3348  >>> print "0x%.8x" % v.as_long()
3349  0x0000000a
3350  """
3351  if is_bv_sort(bv):
3352  ctx = bv.ctx
3353  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3354  else:
3355  ctx = _get_ctx(ctx)
3356  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 1284 of file z3py.py.

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

1285 def Bool(name, ctx=None):
1286  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1287 
1288  >>> p = Bool('p')
1289  >>> q = Bool('q')
1290  >>> And(p, q)
1291  And(p, q)
1292  """
1293  ctx = _get_ctx(ctx)
1294  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 1295 of file z3py.py.

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

1296 def Bools(names, ctx=None):
1297  """Return a tuple of Boolean constants.
1298 
1299  `names` is a single string containing all names separated by blank spaces.
1300  If `ctx=None`, then the global context is used.
1301 
1302  >>> p, q, r = Bools('p q r')
1303  >>> And(p, Or(q, r))
1304  And(p, Or(q, r))
1305  """
1306  ctx = _get_ctx(ctx)
1307  if isinstance(names, str):
1308  names = names.split(" ")
1309  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 1249 of file z3py.py.

Referenced by ArrayRef.__getitem__(), ArraySort(), Bool(), ArraySortRef.domain(), ArrayRef.domain(), If(), IntSort(), is_arith_sort(), Context.MkBoolSort(), ArraySortRef.range(), ArrayRef.range(), and ArrayRef.sort().

1250 def BoolSort(ctx=None):
1251  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1252 
1253  >>> BoolSort()
1254  Bool
1255  >>> p = Const('p', BoolSort())
1256  >>> is_bool(p)
1257  True
1258  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1259  >>> r(0, 1)
1260  r(0, 1)
1261  >>> is_bool(r(0, 1))
1262  True
1263  """
1264  ctx = _get_ctx(ctx)
1265  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 1266 of file z3py.py.

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

1267 def BoolVal(val, ctx=None):
1268  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1269 
1270  >>> BoolVal(True)
1271  True
1272  >>> is_true(BoolVal(True))
1273  True
1274  >>> is_true(True)
1275  False
1276  >>> is_false(BoolVal(False))
1277  True
1278  """
1279  ctx = _get_ctx(ctx)
1280  if val == False:
1281  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1282  else:
1283  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 1310 of file z3py.py.

Referenced by And(), and Or().

1311 def BoolVector(prefix, sz, ctx=None):
1312  """Return a list of Boolean constants of size `sz`.
1313 
1314  The constants are named using the given prefix.
1315  If `ctx=None`, then the global context is used.
1316 
1317  >>> P = BoolVector('p', 3)
1318  >>> P
1319  [p__0, p__1, p__2]
1320  >>> And(P)
1321  And(p__0, p__1, p__2)
1322  """
1323  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 3309 of file z3py.py.

3310 def BV2Int(a):
3311  """Return the Z3 expression BV2Int(a).
3312 
3313  >>> b = BitVec('b', 3)
3314  >>> BV2Int(b).sort()
3315  Int
3316  >>> x = Int('x')
3317  >>> x > BV2Int(b)
3318  x > BV2Int(b)
3319  >>> solve(x > BV2Int(b), b == 1, x < 3)
3320  [b = 1, x = 2]
3321  """
3322  if __debug__:
3323  _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
3324  ctx = a.ctx
3325  ## investigate problem with bv2int
3326  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 2771 of file z3py.py.

2772 def Cbrt(a, ctx=None):
2773  """ Return a Z3 expression which represents the cubic root of a.
2774 
2775  >>> x = Real('x')
2776  >>> Cbrt(x)
2777  x**(1/3)
2778  """
2779  if not is_expr(a):
2780  ctx = _get_ctx(ctx)
2781  a = RealVal(a, ctx)
2782  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 3400 of file z3py.py.

Referenced by BitVecRef.size().

3401 def Concat(*args):
3402  """Create a Z3 bit-vector concatenation expression.
3403 
3404  >>> v = BitVecVal(1, 4)
3405  >>> Concat(v, v+1, v)
3406  Concat(Concat(1, 1 + 1), 1)
3407  >>> simplify(Concat(v, v+1, v))
3408  289
3409  >>> print "%.3x" % simplify(Concat(v, v+1, v)).as_long()
3410  121
3411  """
3412  args = _get_args(args)
3413  if __debug__:
3414  _z3_assert(all(map(is_bv, args)), "All arguments must be Z3 bit-vector expressions.")
3415  _z3_assert(len(args) >= 2, "At least two arguments expected.")
3416  ctx = args[0].ctx
3417  r = args[0]
3418  for i in range(len(args) - 1):
3419  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3420  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 6824 of file z3py.py.

Referenced by If().

6825 def Cond(p, t1, t2, ctx=None):
6826  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
6827 
6828  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
6829  """
6830  p = _to_probe(p, ctx)
6831  t1 = _to_tactic(t1, ctx)
6832  t2 = _to_tactic(t2, ctx)
6833  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 1079 of file z3py.py.

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

1080 def Const(name, sort):
1081  """Create a constant of the given sort.
1082 
1083  >>> Const('x', IntSort())
1084  x
1085  """
1086  if __debug__:
1087  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1088  ctx = sort.ctx
1089  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 1090 of file z3py.py.

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

1091 def Consts(names, sort):
1092  """Create a several constants of the given sort.
1093 
1094  `names` is a string containing the names of all constants to be created.
1095  Blank spaces separate the names of different constants.
1096 
1097  >>> x, y, z = Consts('x y z', IntSort())
1098  >>> x + y + z
1099  x + y + z
1100  """
1101  if isinstance(names, str):
1102  names = names.split(" ")
1103  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 4125 of file z3py.py.

Referenced by Datatype.create().

4126 def CreateDatatypes(*ds):
4127  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4128 
4129  In the following example we define a Tree-List using two mutually recursive datatypes.
4130 
4131  >>> TreeList = Datatype('TreeList')
4132  >>> Tree = Datatype('Tree')
4133  >>> # Tree has two constructors: leaf and node
4134  >>> Tree.declare('leaf', ('val', IntSort()))
4135  >>> # a node contains a list of trees
4136  >>> Tree.declare('node', ('children', TreeList))
4137  >>> TreeList.declare('nil')
4138  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4139  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4140  >>> Tree.val(Tree.leaf(10))
4141  val(leaf(10))
4142  >>> simplify(Tree.val(Tree.leaf(10)))
4143  10
4144  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4145  >>> n1
4146  node(cons(leaf(10), cons(leaf(20), nil)))
4147  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4148  >>> simplify(n2 == n1)
4149  False
4150  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4151  True
4152  """
4153  ds = _get_args(ds)
4154  if __debug__:
4155  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4156  _z3_assert(all(map(lambda d: isinstance(d, Datatype), ds)), "Arguments must be Datatypes")
4157  _z3_assert(all(map(lambda d: d.ctx == ds[0].ctx, ds)), "Context mismatch")
4158  _z3_assert(all(map(lambda d: d.constructors != [], ds)), "Non-empty Datatypes expected")
4159  ctx = ds[0].ctx
4160  num = len(ds)
4161  names = (Symbol * num)()
4162  out = (Sort * num)()
4163  clists = (ConstructorList * num)()
4164  to_delete = []
4165  for i in range(num):
4166  d = ds[i]
4167  names[i] = to_symbol(d.name, ctx)
4168  num_cs = len(d.constructors)
4169  cs = (Constructor * num_cs)()
4170  for j in range(num_cs):
4171  c = d.constructors[j]
4172  cname = to_symbol(c[0], ctx)
4173  rname = to_symbol(c[1], ctx)
4174  fs = c[2]
4175  num_fs = len(fs)
4176  fnames = (Symbol * num_fs)()
4177  sorts = (Sort * num_fs)()
4178  refs = (ctypes.c_uint * num_fs)()
4179  for k in range(num_fs):
4180  fname = fs[k][0]
4181  ftype = fs[k][1]
4182  fnames[k] = to_symbol(fname, ctx)
4183  if isinstance(ftype, Datatype):
4184  if __debug__:
4185  _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4186  sorts[k] = None
4187  refs[k] = ds.index(ftype)
4188  else:
4189  if __debug__:
4190  _z3_assert(is_sort(ftype), "Z3 sort expected")
4191  sorts[k] = ftype.ast
4192  refs[k] = 0
4193  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4194  to_delete.append(ScopedConstructor(cs[j], ctx))
4195  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4196  to_delete.append(ScopedConstructorList(clists[i], ctx))
4197  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4198  result = []
4199  ## Create a field for every constructor, recognizer and accessor
4200  for i in range(num):
4201  dref = DatatypeSortRef(out[i], ctx)
4202  num_cs = dref.num_constructors()
4203  for j in range(num_cs):
4204  cref = dref.constructor(j)
4205  cref_name = cref.name()
4206  cref_arity = cref.arity()
4207  if cref.arity() == 0:
4208  cref = cref()
4209  setattr(dref, cref_name, cref)
4210  rref = dref.recognizer(j)
4211  setattr(dref, rref.name(), rref)
4212  for k in range(cref_arity):
4213  aref = dref.accessor(j, k)
4214  setattr(dref, aref.name(), aref)
4215  result.append(dref)
4216  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 529 of file z3py.py.

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

530 def DeclareSort(name, ctx=None):
531  """Create a new uninterpred sort named `name`.
532 
533  If `ctx=None`, then the new sort is declared in the global Z3Py context.
534 
535  >>> A = DeclareSort('A')
536  >>> a = Const('a', A)
537  >>> b = Const('b', A)
538  >>> a.sort() == A
539  True
540  >>> b.sort() == A
541  True
542  >>> a == b
543  a == b
544  """
545  ctx = _get_ctx(ctx)
546  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
def z3py.describe_probes ( )
Display a (tabular) description of all available probes in Z3.

Definition at line 6754 of file z3py.py.

6755 def describe_probes():
6756  """Display a (tabular) description of all available probes in Z3."""
6757  if in_html_mode():
6758  even = True
6759  print '<table border="1" cellpadding="2" cellspacing="0">'
6760  for p in probes():
6761  if even:
6762  print '<tr style="background-color:#CFCFCF">'
6763  even = False
6764  else:
6765  print '<tr>'
6766  even = True
6767  print '<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40))
6768  print '</table>'
6769  else:
6770  for p in probes():
6771  print '%s : %s' % (p, probe_description(p))
def z3py.describe_tactics ( )
Display a (tabular) description of all available tactics in Z3.

Definition at line 6566 of file z3py.py.

6567 def describe_tactics():
6568  """Display a (tabular) description of all available tactics in Z3."""
6569  if in_html_mode():
6570  even = True
6571  print '<table border="1" cellpadding="2" cellspacing="0">'
6572  for t in tactics():
6573  if even:
6574  print '<tr style="background-color:#CFCFCF">'
6575  even = False
6576  else:
6577  print '<tr>'
6578  even = True
6579  print '<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40))
6580  print '</table>'
6581  else:
6582  for t in tactics():
6583  print '%s : %s' % (t, tactic_description(t))
def z3py.disable_trace (   msg)

Definition at line 49 of file z3py.py.

49 
50 def disable_trace(msg):
51  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 1048 of file z3py.py.

1049 def Distinct(*args):
1050  """Create a Z3 distinct expression.
1051 
1052  >>> x = Int('x')
1053  >>> y = Int('y')
1054  >>> Distinct(x, y)
1055  x != y
1056  >>> z = Int('z')
1057  >>> Distinct(x, y, z)
1058  Distinct(x, y, z)
1059  >>> simplify(Distinct(x, y, z))
1060  Distinct(x, y, z)
1061  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1062  And(Not(x == y), Not(x == z), Not(y == z))
1063  """
1064  args = _get_args(args)
1065  ctx = _ctx_from_ast_arg_list(args)
1066  if __debug__:
1067  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
1068  args = _coerce_expr_list(args, ctx)
1069  _args, sz = _to_ast_array(args)
1070  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
def z3py.enable_trace (   msg)

Definition at line 46 of file z3py.py.

46 
47 def enable_trace(msg):
48  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 4314 of file z3py.py.

Referenced by Context.MkEnumSort().

4315 def EnumSort(name, values, ctx=None):
4316  """Return a new enumeration sort named `name` containing the given values.
4317 
4318  The result is a pair (sort, list of constants).
4319  Example:
4320  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
4321  """
4322  if __debug__:
4323  _z3_assert(isinstance(name, str), "Name must be a string")
4324  _z3_assert(all(map(lambda v: isinstance(v, str), values)), "Eumeration sort values must be strings")
4325  _z3_assert(len(values) > 0, "At least one value expected")
4326  ctx = _get_ctx(ctx)
4327  num = len(values)
4328  _val_names = (Symbol * num)()
4329  for i in range(num):
4330  _val_names[i] = to_symbol(values[i])
4331  _values = (FuncDecl * num)()
4332  _testers = (FuncDecl * num)()
4333  name = to_symbol(name)
4334  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
4335  V = []
4336  for i in range(num):
4337  V.append(FuncDeclRef(_values[i], ctx))
4338  V = map(lambda a: a(), V)
4339  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 342 of file z3py.py.

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

343 def eq(a, b):
344  """Return `True` if `a` and `b` are structurally identical AST nodes.
345 
346  >>> x = Int('x')
347  >>> y = Int('y')
348  >>> eq(x, y)
349  False
350  >>> eq(x + 1, x + 1)
351  True
352  >>> eq(x + 1, 1 + x)
353  False
354  >>> eq(simplify(x + 1), simplify(1 + x))
355  True
356  """
357  if __debug__:
358  _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
359  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)
>>> Tactic('nnf')(q)
[[f(x!foo!1, y!foo!0) >= x!foo!1]]
>>> Tactic('nnf')(q).as_expr()
f(x!foo!3, y!foo!2) >= x!foo!3

Definition at line 1708 of file z3py.py.

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

1709 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1710  """Create a Z3 exists formula.
1711 
1712  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
1713 
1714  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1715 
1716  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1717  >>> x = Int('x')
1718  >>> y = Int('y')
1719  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
1720  >>> q
1721  Exists([x, y], f(x, y) >= x)
1722  >>> Tactic('nnf')(q)
1723  [[f(x!foo!1, y!foo!0) >= x!foo!1]]
1724  >>> Tactic('nnf')(q).as_expr()
1725  f(x!foo!3, y!foo!2) >= x!foo!3
1726  """
1727  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 3421 of file z3py.py.

3422 def Extract(high, low, a):
3423  """Create a Z3 bit-vector extraction expression.
3424 
3425  >>> x = BitVec('x', 8)
3426  >>> Extract(6, 2, x)
3427  Extract(6, 2, x)
3428  >>> Extract(6, 2, x).sort()
3429  BitVec(5)
3430  """
3431  if __debug__:
3432  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3433  _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
3434  _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
3435  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 6787 of file z3py.py.

6788 def FailIf(p, ctx=None):
6789  """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6790 
6791  In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
6792 
6793  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
6794  >>> x, y = Ints('x y')
6795  >>> g = Goal()
6796  >>> g.add(x > 0)
6797  >>> g.add(y > 0)
6798  >>> t(g)
6799  [[x > 0, y > 0]]
6800  >>> g.add(x == y + 1)
6801  >>> t(g)
6802  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6803  """
6804  p = _to_probe(p, ctx)
6805  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 1689 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().

1690 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1691  """Create a Z3 forall formula.
1692 
1693  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
1694 
1695  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1696 
1697  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1698  >>> x = Int('x')
1699  >>> y = Int('y')
1700  >>> ForAll([x, y], f(x, y) >= x)
1701  ForAll([x, y], f(x, y) >= x)
1702  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
1703  ForAll([x, y], f(x, y) >= x)
1704  >>> ForAll([x, y], f(x, y) >= x, weight=10)
1705  ForAll([x, y], f(x, y) >= x)
1706  """
1707  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
def z3py.FreshBool (   prefix = 'b',
  ctx = None 
)
Return a fresh Bolean 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 1324 of file z3py.py.

1325 def FreshBool(prefix='b', ctx=None):
1326  """Return a fresh Bolean constant in the given context using the given prefix.
1327 
1328  If `ctx=None`, then the global context is used.
1329 
1330  >>> b1 = FreshBool()
1331  >>> b2 = FreshBool()
1332  >>> eq(b1, b2)
1333  False
1334  """
1335  ctx = _get_ctx(ctx)
1336  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 2644 of file z3py.py.

2645 def FreshInt(prefix='x', ctx=None):
2646  """Return a fresh integer constant in the given context using the given prefix.
2647 
2648  >>> x = FreshInt()
2649  >>> y = FreshInt()
2650  >>> eq(x, y)
2651  False
2652  >>> x.sort()
2653  Int
2654  """
2655  ctx = _get_ctx(ctx)
2656  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 2696 of file z3py.py.

2697 def FreshReal(prefix='b', ctx=None):
2698  """Return a fresh real constant in the given context using the given prefix.
2699 
2700  >>> x = FreshReal()
2701  >>> y = FreshReal()
2702  >>> eq(x, y)
2703  False
2704  >>> x.sort()
2705  Real
2706  """
2707  ctx = _get_ctx(ctx)
2708  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 661 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().

662 def Function(name, *sig):
663  """Create a new Z3 uninterpreted function with the given sorts.
664 
665  >>> f = Function('f', IntSort(), IntSort())
666  >>> f(f(0))
667  f(f(0))
668  """
669  sig = _get_args(sig)
670  if __debug__:
671  _z3_assert(len(sig) > 0, "At least two arguments expected")
672  arity = len(sig) - 1
673  rng = sig[arity]
674  if __debug__:
675  _z3_assert(is_sort(rng), "Z3 sort expected")
676  dom = (Sort * arity)()
677  for i in range(arity):
678  if __debug__:
679  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
680  dom[i] = sig[i].ast
681  ctx = rng.ctx
682  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
def z3py.get_as_array_func (   n)
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).

Definition at line 5442 of file z3py.py.

5443 def get_as_array_func(n):
5444  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
5445  if __debug__:
5446  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
5447  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 3856 of file z3py.py.

3857 def get_map_func(a):
3858  """Return the function declaration associated with a Z3 map array expression.
3859 
3860  >>> f = Function('f', IntSort(), IntSort())
3861  >>> b = Array('b', IntSort(), IntSort())
3862  >>> a = Map(f, b)
3863  >>> eq(f, get_map_func(a))
3864  True
3865  >>> get_map_func(a)
3866  f
3867  >>> get_map_func(a)(0)
3868  f(0)
3869  """
3870  if __debug__:
3871  _z3_assert(is_map(a), "Z3 array map expression expected.")
3872  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_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 982 of file z3py.py.

983 def get_var_index(a):
984  """Return the de-Bruijn index of the Z3 bounded variable `a`.
985 
986  >>> x = Int('x')
987  >>> y = Int('y')
988  >>> is_var(x)
989  False
990  >>> is_const(x)
991  True
992  >>> f = Function('f', IntSort(), IntSort(), IntSort())
993  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
994  >>> q = ForAll([x, y], f(x, y) == x + y)
995  >>> q.body()
996  f(Var(1), Var(0)) == Var(1) + Var(0)
997  >>> b = q.body()
998  >>> b.arg(0)
999  f(Var(1), Var(0))
1000  >>> v1 = b.arg(0).arg(0)
1001  >>> v2 = b.arg(0).arg(1)
1002  >>> v1
1003  Var(1)
1004  >>> v2
1005  Var(0)
1006  >>> get_var_index(v1)
1007  1
1008  >>> get_var_index(v2)
1009  0
1010  """
1011  if __debug__:
1012  _z3_assert(is_var(a), "Z3 bound variable expected")
1013  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
def z3py.get_version ( )

Definition at line 60 of file z3py.py.

60 
61 def get_version():
62  major = ctypes.c_uint(0)
63  minor = ctypes.c_uint(0)
64  build = ctypes.c_uint(0)
65  rev = ctypes.c_uint(0)
66  Z3_get_version(major, minor, build, rev)
67  return (major.value, minor.value, build.value, rev.value)
68 
69 # We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com
def z3py.get_version_string ( )

Definition at line 52 of file z3py.py.

52 
53 def get_version_string():
54  major = ctypes.c_uint(0)
55  minor = ctypes.c_uint(0)
56  build = ctypes.c_uint(0)
57  rev = ctypes.c_uint(0)
58  Z3_get_version(major, minor, build, rev)
59  return "%s.%s.%s" % (major.value, minor.value, build.value)
def z3py.help_simplify ( )
Return a string describing all options available for Z3 `simplify` procedure.

Definition at line 6864 of file z3py.py.

6865 def help_simplify():
6866  """Return a string describing all options available for Z3 `simplify` procedure."""
6867  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 1026 of file z3py.py.

1027 def If(a, b, c, ctx=None):
1028  """Create a Z3 if-then-else expression.
1029 
1030  >>> x = Int('x')
1031  >>> y = Int('y')
1032  >>> max = If(x > y, x, y)
1033  >>> max
1034  If(x > y, x, y)
1035  >>> simplify(max)
1036  If(x <= y, y, x)
1037  """
1038  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1039  return Cond(a, b, c, ctx)
1040  else:
1041  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1042  s = BoolSort(ctx)
1043  a = s.cast(a)
1044  b, c = _coerce_exprs(b, c, ctx)
1045  if __debug__:
1046  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1047  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 1337 of file z3py.py.

Referenced by Store(), Solver.unsat_core(), and Update().

1338 def Implies(a, b, ctx=None):
1339  """Create a Z3 implies expression.
1340 
1341  >>> p, q = Bools('p q')
1342  >>> Implies(p, q)
1343  Implies(p, q)
1344  >>> simplify(Implies(p, q))
1345  Or(Not(p), q)
1346  """
1347  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1348  s = BoolSort(ctx)
1349  a = s.cast(a)
1350  b = s.cast(b)
1351  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 2609 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(), 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(), 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_store(), 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(), Solver.sexpr(), SimpleSolver(), Goal.simplify(), SolverFor(), ArithRef.sort(), Solver.statistics(), Store(), ToReal(), Goal.translate(), AstVector.translate(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

2610 def Int(name, ctx=None):
2611  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
2612 
2613  >>> x = Int('x')
2614  >>> is_int(x)
2615  True
2616  >>> is_int(x + 1)
2617  True
2618  """
2619  ctx = _get_ctx(ctx)
2620  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).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 2621 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().

2622 def Ints(names, ctx=None):
2623  """Return a tuple of Integer constants.
2624 
2625  >>> x, y, z = Ints('x y z')
2626  >>> Sum(x, y, z)
2627  x + y + z
2628  """
2629  ctx = _get_ctx(ctx)
2630  if isinstance(names, str):
2631  names = names.split(" ")
2632  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 2504 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(), 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(), 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.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().

2505 def IntSort(ctx=None):
2506  """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
2507 
2508  >>> IntSort()
2509  Int
2510  >>> x = Const('x', IntSort())
2511  >>> is_int(x)
2512  True
2513  >>> x.sort() == IntSort()
2514  True
2515  >>> x.sort() == BoolSort()
2516  False
2517  """
2518  ctx = _get_ctx(ctx)
2519  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 2553 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().

2554 def IntVal(val, ctx=None):
2555  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
2556 
2557  >>> IntVal(1)
2558  1
2559  >>> IntVal("100")
2560  100
2561  """
2562  ctx = _get_ctx(ctx)
2563  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 2633 of file z3py.py.

2634 def IntVector(prefix, sz, ctx=None):
2635  """Return a list of integer constants of size `sz`.
2636 
2637  >>> X = IntVector('x', 3)
2638  >>> X
2639  [x__0, x__1, x__2]
2640  >>> Sum(X)
2641  x__0 + x__1 + x__2
2642  """
2643  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 2217 of file z3py.py.

2218 def is_add(a):
2219  """Return `True` if `a` is an expression of the form b + c.
2220 
2221  >>> x, y = Ints('x y')
2222  >>> is_add(x + y)
2223  True
2224  >>> is_add(x - y)
2225  False
2226  """
2227  return is_app_of(a, Z3_OP_ADD)
def z3py.is_algebraic_value (   a)
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 2204 of file z3py.py.

2205 def is_algebraic_value(a):
2206  """Return `True` if `a` is an algerbraic value of sort Real.
2207 
2208  >>> is_algebraic_value(RealVal("3/5"))
2209  False
2210  >>> n = simplify(Sqrt(2))
2211  >>> n
2212  1.4142135623?
2213  >>> is_algebraic_value(n)
2214  True
2215  """
2216  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 1196 of file z3py.py.

1197 def is_and(a):
1198  """Return `True` if `a` is a Z3 and expression.
1199 
1200  >>> p, q = Bools('p q')
1201  >>> is_and(And(p, q))
1202  True
1203  >>> is_and(Or(p, q))
1204  False
1205  """
1206  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 915 of file z3py.py.

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

916 def is_app(a):
917  """Return `True` if `a` is a Z3 function application.
918 
919  Note that, constants are function applications with 0 arguments.
920 
921  >>> a = Int('a')
922  >>> is_app(a)
923  True
924  >>> is_app(a + 1)
925  True
926  >>> is_app(IntSort())
927  False
928  >>> is_app(1)
929  False
930  >>> is_app(IntVal(1))
931  True
932  >>> x = Int('x')
933  >>> is_app(ForAll(x, x >= 0))
934  False
935  """
936  if not isinstance(a, ExprRef):
937  return False
938  k = _ast_kind(a.ctx, a)
939  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 1014 of file z3py.py.

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

1015 def is_app_of(a, k):
1016  """Return `True` if `a` is an application of the given kind `k`.
1017 
1018  >>> x = Int('x')
1019  >>> n = x + 1
1020  >>> is_app_of(n, Z3_OP_ADD)
1021  True
1022  >>> is_app_of(n, Z3_OP_MUL)
1023  False
1024  """
1025  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 2098 of file z3py.py.

Referenced by is_algebraic_value().

2099 def is_arith(a):
2100  """Return `True` if `a` is an arithmetical expression.
2101 
2102  >>> x = Int('x')
2103  >>> is_arith(x)
2104  True
2105  >>> is_arith(x + 1)
2106  True
2107  >>> is_arith(1)
2108  False
2109  >>> is_arith(IntVal(1))
2110  True
2111  >>> y = Real('y')
2112  >>> is_arith(y)
2113  True
2114  >>> is_arith(y + 1)
2115  True
2116  """
2117  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 1801 of file z3py.py.

1802 def is_arith_sort(s):
1803  """Return `True` if s is an arithmetical sort (type).
1804 
1805  >>> is_arith_sort(IntSort())
1806  True
1807  >>> is_arith_sort(RealSort())
1808  True
1809  >>> is_arith_sort(BoolSort())
1810  False
1811  >>> n = Int('x') + 1
1812  >>> is_arith_sort(n.sort())
1813  True
1814  """
1815  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 3778 of file z3py.py.

3779 def is_array(a):
3780  """Return `True` if `a` is a Z3 array expression.
3781 
3782  >>> a = Array('a', IntSort(), IntSort())
3783  >>> is_array(a)
3784  True
3785  >>> is_array(Store(a, 0, 1))
3786  True
3787  >>> is_array(a[0])
3788  False
3789  """
3790  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 5438 of file z3py.py.

Referenced by get_as_array_func().

5439 def is_as_array(n):
5440  """Return true if n is a Z3 expression of the form (_ as-array f)."""
5441  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 322 of file z3py.py.

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

323 def is_ast(a):
324  """Return `True` if `a` is an AST node.
325 
326  >>> is_ast(10)
327  False
328  >>> is_ast(IntVal(10))
329  True
330  >>> is_ast(Int('x'))
331  True
332  >>> is_ast(BoolSort())
333  True
334  >>> is_ast(Function('f', IntSort(), IntSort()))
335  True
336  >>> is_ast("x")
337  False
338  >>> is_ast(Solver())
339  False
340  """
341  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 1149 of file z3py.py.

Referenced by BoolSort(), and prove().

1150 def is_bool(a):
1151  """Return `True` if `a` is a Z3 Boolean expression.
1152 
1153  >>> p = Bool('p')
1154  >>> is_bool(p)
1155  True
1156  >>> q = Bool('q')
1157  >>> is_bool(And(p, q))
1158  True
1159  >>> x = Real('x')
1160  >>> is_bool(x)
1161  False
1162  >>> is_bool(x == 0)
1163  True
1164  """
1165  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 3282 of file z3py.py.

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

3283 def is_bv(a):
3284  """Return `True` if `a` is a Z3 bit-vector expression.
3285 
3286  >>> b = BitVec('b', 32)
3287  >>> is_bv(b)
3288  True
3289  >>> is_bv(b + 10)
3290  True
3291  >>> is_bv(Int('x'))
3292  False
3293  """
3294  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 2821 of file z3py.py.

Referenced by BitVecVal().

2822 def is_bv_sort(s):
2823  """Return True if `s` is a Z3 bit-vector sort.
2824 
2825  >>> is_bv_sort(BitVecSort(32))
2826  True
2827  >>> is_bv_sort(IntSort())
2828  False
2829  """
2830  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 3295 of file z3py.py.

3296 def is_bv_value(a):
3297  """Return `True` if `a` is a Z3 bit-vector numeral value.
3298 
3299  >>> b = BitVec('b', 32)
3300  >>> is_bv_value(b)
3301  False
3302  >>> b = BitVecVal(10, 32)
3303  >>> b
3304  10
3305  >>> is_bv_value(b)
3306  True
3307  """
3308  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 940 of file z3py.py.

Referenced by prove().

941 def is_const(a):
942  """Return `True` if `a` is Z3 constant/variable expression.
943 
944  >>> a = Int('a')
945  >>> is_const(a)
946  True
947  >>> is_const(a + 1)
948  False
949  >>> is_const(1)
950  False
951  >>> is_const(IntVal(1))
952  True
953  >>> x = Int('x')
954  >>> is_const(ForAll(x, x >= 0))
955  False
956  """
957  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 3817 of file z3py.py.

3818 def is_const_array(a):
3819  """Return `True` if `a` is a Z3 constant array.
3820 
3821  >>> a = K(IntSort(), 10)
3822  >>> is_const_array(a)
3823  True
3824  >>> a = Array('a', IntSort(), IntSort())
3825  >>> is_const_array(a)
3826  False
3827  """
3828  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 1238 of file z3py.py.

1239 def is_distinct(a):
1240  """Return `True` if `a` is a Z3 distinct expression.
1241 
1242  >>> x, y, z = Ints('x y z')
1243  >>> is_distinct(x == y)
1244  False
1245  >>> is_distinct(Distinct(x, y, z))
1246  True
1247  """
1248  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 2250 of file z3py.py.

2251 def is_div(a):
2252  """Return `True` if `a` is an expression of the form b / c.
2253 
2254  >>> x, y = Reals('x y')
2255  >>> is_div(x / y)
2256  True
2257  >>> is_div(x + y)
2258  False
2259  >>> x, y = Ints('x y')
2260  >>> is_div(x / y)
2261  False
2262  >>> is_idiv(x / y)
2263  True
2264  """
2265  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 1229 of file z3py.py.

1230 def is_eq(a):
1231  """Return `True` if `a` is a Z3 equality expression.
1232 
1233  >>> x, y = Ints('x y')
1234  >>> is_eq(x == y)
1235  True
1236  """
1237  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 895 of file z3py.py.

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

896 def is_expr(a):
897  """Return `True` if `a` is a Z3 expression.
898 
899  >>> a = Int('a')
900  >>> is_expr(a)
901  True
902  >>> is_expr(a + 1)
903  True
904  >>> is_expr(IntSort())
905  False
906  >>> is_expr(1)
907  False
908  >>> is_expr(IntVal(1))
909  True
910  >>> x = Int('x')
911  >>> is_expr(ForAll(x, x >= 0))
912  True
913  """
914  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 1183 of file z3py.py.

Referenced by BoolVal().

1184 def is_false(a):
1185  """Return `True` if `a` is the Z3 false expression.
1186 
1187  >>> p = Bool('p')
1188  >>> is_false(p)
1189  False
1190  >>> is_false(False)
1191  False
1192  >>> is_false(BoolVal(False))
1193  True
1194  """
1195  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 649 of file z3py.py.

Referenced by prove().

650 def is_func_decl(a):
651  """Return `True` if `a` is a Z3 function declaration.
652 
653  >>> f = Function('f', IntSort(), IntSort())
654  >>> is_func_decl(f)
655  True
656  >>> x = Real('x')
657  >>> is_func_decl(x)
658  False
659  """
660  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 2310 of file z3py.py.

2311 def is_ge(a):
2312  """Return `True` if `a` is an expression of the form b >= c.
2313 
2314  >>> x, y = Ints('x y')
2315  >>> is_ge(x >= y)
2316  True
2317  >>> is_ge(x == y)
2318  False
2319  """
2320  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 2321 of file z3py.py.

2322 def is_gt(a):
2323  """Return `True` if `a` is an expression of the form b > c.
2324 
2325  >>> x, y = Ints('x y')
2326  >>> is_gt(x > y)
2327  True
2328  >>> is_gt(x == y)
2329  False
2330  """
2331  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 2266 of file z3py.py.

Referenced by is_div().

2267 def is_idiv(a):
2268  """Return `True` if `a` is an expression of the form b div c.
2269 
2270  >>> x, y = Ints('x y')
2271  >>> is_idiv(x / y)
2272  True
2273  >>> is_idiv(x + y)
2274  False
2275  """
2276  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 2118 of file z3py.py.

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

2119 def is_int(a):
2120  """Return `True` if `a` is an integer expression.
2121 
2122  >>> x = Int('x')
2123  >>> is_int(x + 1)
2124  True
2125  >>> is_int(1)
2126  False
2127  >>> is_int(IntVal(1))
2128  True
2129  >>> y = Real('y')
2130  >>> is_int(y)
2131  False
2132  >>> is_int(y + 1)
2133  False
2134  """
2135  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 2160 of file z3py.py.

2161 def is_int_value(a):
2162  """Return `True` if `a` is an integer value of sort Int.
2163 
2164  >>> is_int_value(IntVal(1))
2165  True
2166  >>> is_int_value(1)
2167  False
2168  >>> is_int_value(Int('x'))
2169  False
2170  >>> n = Int('x') + 1
2171  >>> n
2172  x + 1
2173  >>> n.arg(1)
2174  1
2175  >>> is_int_value(n.arg(1))
2176  True
2177  >>> is_int_value(RealVal("1/3"))
2178  False
2179  >>> is_int_value(RealVal(1))
2180  False
2181  """
2182  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 2332 of file z3py.py.

2333 def is_is_int(a):
2334  """Return `True` if `a` is an expression of the form IsInt(b).
2335 
2336  >>> x = Real('x')
2337  >>> is_is_int(IsInt(x))
2338  True
2339  >>> is_is_int(x)
2340  False
2341  """
2342  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 3829 of file z3py.py.

3830 def is_K(a):
3831  """Return `True` if `a` is a Z3 constant array.
3832 
3833  >>> a = K(IntSort(), 10)
3834  >>> is_K(a)
3835  True
3836  >>> a = Array('a', IntSort(), IntSort())
3837  >>> is_K(a)
3838  False
3839  """
3840  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 2288 of file z3py.py.

2289 def is_le(a):
2290  """Return `True` if `a` is an expression of the form b <= c.
2291 
2292  >>> x, y = Ints('x y')
2293  >>> is_le(x <= y)
2294  True
2295  >>> is_le(x < y)
2296  False
2297  """
2298  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 2299 of file z3py.py.

2300 def is_lt(a):
2301  """Return `True` if `a` is an expression of the form b < c.
2302 
2303  >>> x, y = Ints('x y')
2304  >>> is_lt(x < y)
2305  True
2306  >>> is_lt(x == y)
2307  False
2308  """
2309  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 3841 of file z3py.py.

Referenced by get_map_func().

3842 def is_map(a):
3843  """Return `True` if `a` is a Z3 map array expression.
3844 
3845  >>> f = Function('f', IntSort(), IntSort())
3846  >>> b = Array('b', IntSort(), IntSort())
3847  >>> a = Map(f, b)
3848  >>> a
3849  Map(f, b)
3850  >>> is_map(a)
3851  True
3852  >>> is_map(b)
3853  False
3854  """
3855  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 2277 of file z3py.py.

2278 def is_mod(a):
2279  """Return `True` if `a` is an expression of the form b % c.
2280 
2281  >>> x, y = Ints('x y')
2282  >>> is_mod(x % y)
2283  True
2284  >>> is_mod(x + y)
2285  False
2286  """
2287  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 2228 of file z3py.py.

2229 def is_mul(a):
2230  """Return `True` if `a` is an expression of the form b * c.
2231 
2232  >>> x, y = Ints('x y')
2233  >>> is_mul(x * y)
2234  True
2235  >>> is_mul(x - y)
2236  False
2237  """
2238  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 1218 of file z3py.py.

1219 def is_not(a):
1220  """Return `True` if `a` is a Z3 not expression.
1221 
1222  >>> p = Bool('p')
1223  >>> is_not(p)
1224  False
1225  >>> is_not(Not(p))
1226  True
1227  """
1228  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 1207 of file z3py.py.

1208 def is_or(a):
1209  """Return `True` if `a` is a Z3 or expression.
1210 
1211  >>> p, q = Bools('p q')
1212  >>> is_or(Or(p, q))
1213  True
1214  >>> is_or(And(p, q))
1215  False
1216  """
1217  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 1448 of file z3py.py.

Referenced by MultiPattern().

1449 def is_pattern(a):
1450  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1451 
1452  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1453 
1454  >>> f = Function('f', IntSort(), IntSort())
1455  >>> x = Int('x')
1456  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1457  >>> q
1458  ForAll(x, f(x) == 0)
1459  >>> q.num_patterns()
1460  1
1461  >>> is_pattern(q.pattern(0))
1462  True
1463  >>> q.pattern(0)
1464  f(Var(0))
1465  """
1466  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 6720 of file z3py.py.

Referenced by eq().

6721 def is_probe(p):
6722  """Return `True` if `p` is a Z3 probe.
6723 
6724  >>> is_probe(Int('x'))
6725  False
6726  >>> is_probe(Probe('memory'))
6727  True
6728  """
6729  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 1648 of file z3py.py.

1649 def is_quantifier(a):
1650  """Return `True` if `a` is a Z3 quantifier.
1651 
1652  >>> f = Function('f', IntSort(), IntSort())
1653  >>> x = Int('x')
1654  >>> q = ForAll(x, f(x) == 0)
1655  >>> is_quantifier(q)
1656  True
1657  >>> is_quantifier(f(x))
1658  False
1659  """
1660  return isinstance(a, QuantifierRef)
def z3py.is_rational_value (   a)
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 2183 of file z3py.py.

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

2184 def is_rational_value(a):
2185  """Return `True` if `a` is rational value of sort Real.
2186 
2187  >>> is_rational_value(RealVal(1))
2188  True
2189  >>> is_rational_value(RealVal("3/5"))
2190  True
2191  >>> is_rational_value(IntVal(1))
2192  False
2193  >>> is_rational_value(1)
2194  False
2195  >>> n = Real('x') + 1
2196  >>> n.arg(1)
2197  1
2198  >>> is_rational_value(n.arg(1))
2199  True
2200  >>> is_rational_value(Real('x'))
2201  False
2202  """
2203  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 2136 of file z3py.py.

Referenced by Real(), and RealSort().

2137 def is_real(a):
2138  """Return `True` if `a` is a real expression.
2139 
2140  >>> x = Int('x')
2141  >>> is_real(x + 1)
2142  False
2143  >>> y = Real('y')
2144  >>> is_real(y)
2145  True
2146  >>> is_real(y + 1)
2147  True
2148  >>> is_real(1)
2149  False
2150  >>> is_real(RealVal(1))
2151  True
2152  """
2153  return is_arith(a) and a.is_real()
def is_select (   a)
Return `True` if `a` is a Z3 array select.

>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True
Return `True` if `a` is a Z3 array select application.

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

Definition at line 3791 of file z3py.py.

Referenced by K().

3792 def is_select(a):
3793  """Return `True` if `a` is a Z3 array select.
3794 
3795  >>> a = Array('a', IntSort(), IntSort())
3796  >>> is_select(a)
3797  False
3798  >>> i = Int('i')
3799  >>> is_select(a[i])
3800  True
3801  """
3802  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 498 of file z3py.py.

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

499 def is_sort(s):
500  """Return `True` if `s` is a Z3 sort.
501 
502  >>> is_sort(IntSort())
503  True
504  >>> is_sort(Int('x'))
505  False
506  >>> is_expr(Int('x'))
507  True
508  """
509  return isinstance(s, SortRef)
def is_store (   a)
Return `True` if `a` is a Z3 array store.

>>> a = Array('a', IntSort(), IntSort())
>>> is_store(a)
False
>>> i = Int('i')
>>> is_store(a[i])
False
>>> is_store(Store(a, i, i + 1))
True
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 3803 of file z3py.py.

Referenced by K().

3804 def is_store(a):
3805  """Return `True` if `a` is a Z3 array store.
3806 
3807  >>> a = Array('a', IntSort(), IntSort())
3808  >>> is_store(a)
3809  False
3810  >>> i = Int('i')
3811  >>> is_store(a[i])
3812  False
3813  >>> is_store(Store(a, i, i + 1))
3814  True
3815  """
3816  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 2239 of file z3py.py.

2240 def is_sub(a):
2241  """Return `True` if `a` is an expression of the form b - c.
2242 
2243  >>> x, y = Ints('x y')
2244  >>> is_sub(x - y)
2245  True
2246  >>> is_sub(x + y)
2247  False
2248  """
2249  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 2357 of file z3py.py.

2358 def is_to_int(a):
2359  """Return `True` if `a` is an expression of the form ToInt(b).
2360 
2361  >>> x = Real('x')
2362  >>> n = ToInt(x)
2363  >>> n
2364  ToInt(x)
2365  >>> is_to_int(n)
2366  True
2367  >>> is_to_int(x)
2368  False
2369  """
2370  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 2343 of file z3py.py.

2344 def is_to_real(a):
2345  """Return `True` if `a` is an expression of the form ToReal(b).
2346 
2347  >>> x = Int('x')
2348  >>> n = ToReal(x)
2349  >>> n
2350  ToReal(x)
2351  >>> is_to_real(n)
2352  True
2353  >>> is_to_real(x)
2354  False
2355  """
2356  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 1166 of file z3py.py.

Referenced by BoolVal().

1167 def is_true(a):
1168  """Return `True` if `a` is the Z3 true expression.
1169 
1170  >>> p = Bool('p')
1171  >>> is_true(p)
1172  False
1173  >>> is_true(simplify(p == p))
1174  True
1175  >>> x = Real('x')
1176  >>> is_true(x == 0)
1177  False
1178  >>> # True is a Python Boolean expression
1179  >>> is_true(True)
1180  False
1181  """
1182  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 958 of file z3py.py.

Referenced by get_var_index().

959 def is_var(a):
960  """Return `True` if `a` is variable.
961 
962  Z3 uses de-Bruijn indices for representing bound variables in
963  quantifiers.
964 
965  >>> x = Int('x')
966  >>> is_var(x)
967  False
968  >>> is_const(x)
969  True
970  >>> f = Function('f', IntSort(), IntSort())
971  >>> # Z3 replaces x with bound variables when ForAll is executed.
972  >>> q = ForAll(x, f(x) == x)
973  >>> b = q.body()
974  >>> b
975  f(Var(0)) == Var(0)
976  >>> b.arg(1)
977  Var(0)
978  >>> is_var(b.arg(1))
979  True
980  """
981  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 2743 of file z3py.py.

Referenced by is_is_int().

2744 def IsInt(a):
2745  """ Return the Z3 predicate IsInt(a).
2746 
2747  >>> x = Real('x')
2748  >>> IsInt(x + "1/2")
2749  IsInt(x + 1/2)
2750  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
2751  [x = 1/2]
2752  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
2753  no solution
2754  """
2755  if __debug__:
2756  _z3_assert(a.is_real(), "Z3 real expression expected.")
2757  ctx = a.ctx
2758  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 3980 of file z3py.py.

Referenced by is_const_array(), and is_K().

3981 def K(dom, v):
3982  """Return a Z3 constant array expression.
3983 
3984  >>> a = K(IntSort(), 10)
3985  >>> a
3986  K(Int, 10)
3987  >>> a.sort()
3988  Array(Int, Int)
3989  >>> i = Int('i')
3990  >>> a[i]
3991  K(Int, 10)[i]
3992  >>> simplify(a[i])
3993  10
3994  """
3995  if __debug__:
3996  _z3_assert(is_sort(dom), "Z3 sort expected")
3997  ctx = dom.ctx
3998  if not is_expr(v):
3999  v = _py2expr(v, ctx)
4000  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()
-4L
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2L
>>> 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 3568 of file z3py.py.

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

3569 def LShR(a, b):
3570  """Create the Z3 expression logical right shift.
3571 
3572  Use the operator >> for the arithmetical right shift.
3573 
3574  >>> x, y = BitVecs('x y', 32)
3575  >>> LShR(x, y)
3576  LShR(x, y)
3577  >>> (x >> y).sexpr()
3578  '(bvashr x y)'
3579  >>> LShR(x, y).sexpr()
3580  '(bvlshr x y)'
3581  >>> BitVecVal(4, 3)
3582  4
3583  >>> BitVecVal(4, 3).as_signed_long()
3584  -4L
3585  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3586  -2L
3587  >>> simplify(BitVecVal(4, 3) >> 1)
3588  6
3589  >>> simplify(LShR(BitVecVal(4, 3), 1))
3590  2
3591  >>> simplify(BitVecVal(2, 3) >> 1)
3592  1
3593  >>> simplify(LShR(BitVecVal(2, 3), 1))
3594  1
3595  """
3596  _check_bv_args(a, b)
3597  a, b = _coerce_exprs(a, b)
3598  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 197 of file z3py.py.

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

198 def main_ctx():
199  """Return a reference to the global Z3 context.
200 
201  >>> x = Real('x')
202  >>> x.ctx == main_ctx()
203  True
204  >>> c = Context()
205  >>> c == main_ctx()
206  False
207  >>> x2 = Real('x', c)
208  >>> x2.ctx == c
209  True
210  >>> eq(x, x2)
211  False
212  """
213  global _main_ctx
214  if _main_ctx == None:
215  _main_ctx = Context()
216  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 3958 of file z3py.py.

Referenced by get_map_func(), and is_map().

3959 def Map(f, *args):
3960  """Return a Z3 map array expression.
3961 
3962  >>> f = Function('f', IntSort(), IntSort(), IntSort())
3963  >>> a1 = Array('a1', IntSort(), IntSort())
3964  >>> a2 = Array('a2', IntSort(), IntSort())
3965  >>> b = Map(f, a1, a2)
3966  >>> b
3967  Map(f, a1, a2)
3968  >>> prove(b[0] == f(a1[0], a2[0]))
3969  proved
3970  """
3971  args = _get_args(args)
3972  if __debug__:
3973  _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
3974  _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
3975  _z3_assert(all(map(is_array, args)), "Z3 array expected expected")
3976  _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
3977  _args, sz = _to_ast_array(args)
3978  ctx = f.ctx
3979  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 1467 of file z3py.py.

1468 def MultiPattern(*args):
1469  """Create a Z3 multi-pattern using the given expressions `*args`
1470 
1471  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1472 
1473  >>> f = Function('f', IntSort(), IntSort())
1474  >>> g = Function('g', IntSort(), IntSort())
1475  >>> x = Int('x')
1476  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1477  >>> q
1478  ForAll(x, f(x) != g(x))
1479  >>> q.num_patterns()
1480  1
1481  >>> is_pattern(q.pattern(0))
1482  True
1483  >>> q.pattern(0)
1484  MultiPattern(f(Var(0)), g(Var(0)))
1485  """
1486  if __debug__:
1487  _z3_assert(len(args) > 0, "At least one argument expected")
1488  _z3_assert(all(map(is_expr, args)), "Z3 expressions expected")
1489  ctx = args[0].ctx
1490  args, sz = _to_ast_array(args)
1491  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 1367 of file z3py.py.

Referenced by Implies(), prove(), and Xor().

1368 def Not(a, ctx=None):
1369  """Create a Z3 not expression or probe.
1370 
1371  >>> p = Bool('p')
1372  >>> Not(Not(p))
1373  Not(Not(p))
1374  >>> simplify(Not(Not(p)))
1375  p
1376  """
1377  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1378  if is_probe(a):
1379  # Not is also used to build probes
1380  return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1381  else:
1382  s = BoolSort(ctx)
1383  a = s.cast(a)
1384  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 74 of file z3py.py.

74 
75 def open_log(fname):
76  """Log interaction to a file. This function must be invoked immediately after init(). """
77  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 1413 of file z3py.py.

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

1414 def Or(*args):
1415  """Create a Z3 or-expression or or-probe.
1416 
1417  >>> p, q, r = Bools('p q r')
1418  >>> Or(p, q, r)
1419  Or(p, q, r)
1420  >>> P = BoolVector('p', 5)
1421  >>> Or(P)
1422  Or(p__0, p__1, p__2, p__3, p__4)
1423  """
1424  args = _get_args(args)
1425  ctx = _ctx_from_ast_arg_list(args)
1426  if __debug__:
1427  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1428  if _has_probe(args):
1429  return _probe_or(args, ctx)
1430  else:
1431  args = _coerce_expr_list(args, ctx)
1432  _args, sz = _to_ast_array(args)
1433  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 6452 of file z3py.py.

6453 def OrElse(*ts, **ks):
6454  """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
6455 
6456  >>> x = Int('x')
6457  >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
6458  >>> # Tactic split-clause fails if there is no clause in the given goal.
6459  >>> t(x == 0)
6460  [[x == 0]]
6461  >>> t(Or(x == 0, x == 1))
6462  [[x == 0], [x == 1]]
6463  """
6464  if __debug__:
6465  _z3_assert(len(ts) >= 2, "At least two arguments expected")
6466  ctx = ks.get('ctx', None)
6467  num = len(ts)
6468  r = ts[0]
6469  for i in range(num - 1):
6470  r = _or_else(r, ts[i+1], ctx)
6471  return r
def z3py.ParAndThen (   t1,
  t2,
  ctx = None 
)
Alias for ParThen(t1, t2, ctx).

Definition at line 6504 of file z3py.py.

6505 def ParAndThen(t1, t2, ctx=None):
6506  """Alias for ParThen(t1, t2, ctx)."""
6507  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 6472 of file z3py.py.

6473 def ParOr(*ts, **ks):
6474  """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
6475 
6476  >>> x = Int('x')
6477  >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
6478  >>> t(x + 1 == 2)
6479  [[x == 1]]
6480  """
6481  if __debug__:
6482  _z3_assert(len(ts) >= 2, "At least two arguments expected")
6483  ctx = _get_ctx(ks.get('ctx', None))
6484  ts = map(lambda t: _to_tactic(t, ctx), ts)
6485  sz = len(ts)
6486  _args = (TacticObj * sz)()
6487  for i in range(sz):
6488  _args[i] = ts[i].tactic
6489  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 7167 of file z3py.py.

7168 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
7169  """Parse a file in SMT 2.0 format using the given sorts and decls.
7170 
7171  This function is similar to parse_smt2_string().
7172  """
7173  ctx = _get_ctx(ctx)
7174  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7175  dsz, dnames, ddecls = _dict2darray(decls, ctx)
7176  return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
7177 
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 7147 of file z3py.py.

Referenced by parse_smt2_file().

7148 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
7149  """Parse a string in SMT 2.0 format using the given sorts and decls.
7150 
7151  The arguments sorts and decls are Python dictionaries used to initialize
7152  the symbol table used for the SMT 2.0 parser.
7153 
7154  >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
7155  And(x > 0, x < 10)
7156  >>> x, y = Ints('x y')
7157  >>> f = Function('f', IntSort(), IntSort())
7158  >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
7159  x + f(y) > 0
7160  >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
7161  a > 0
7162  """
7163  ctx = _get_ctx(ctx)
7164  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7165  dsz, dnames, ddecls = _dict2darray(decls, ctx)
7166  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 6490 of file z3py.py.

Referenced by ParAndThen().

6491 def ParThen(t1, t2, ctx=None):
6492  """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
6493 
6494  >>> x, y = Ints('x y')
6495  >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
6496  >>> t(And(Or(x == 1, x == 2), y == x + 1))
6497  [[x == 1, y == 2], [x == 2, y == 3]]
6498  """
6499  t1 = _to_tactic(t1, ctx)
6500  t2 = _to_tactic(t2, ctx)
6501  if __debug__:
6502  _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
6503  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 6746 of file z3py.py.

Referenced by describe_probes().

6747 def probe_description(name, ctx=None):
6748  """Return a short description for the probe named `name`.
6749 
6750  >>> d = probe_description('memory')
6751  """
6752  ctx = _get_ctx(ctx)
6753  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 6736 of file z3py.py.

Referenced by describe_probes().

6737 def probes(ctx=None):
6738  """Return a list of all available probes in Z3.
6739 
6740  >>> l = probes()
6741  >>> l.count('memory') == 1
6742  True
6743  """
6744  ctx = _get_ctx(ctx)
6745  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 6943 of file z3py.py.

Referenced by BitVecs().

6944 def Product(*args):
6945  """Create the product of the Z3 expressions.
6946 
6947  >>> a, b, c = Ints('a b c')
6948  >>> Product(a, b, c)
6949  a*b*c
6950  >>> Product([a, b, c])
6951  a*b*c
6952  >>> A = IntVector('a', 5)
6953  >>> Product(A)
6954  a__0*a__1*a__2*a__3*a__4
6955  """
6956  args = _get_args(args)
6957  if __debug__:
6958  _z3_assert(len(args) > 0, "Non empty list of arguments expected")
6959  ctx = _ctx_from_ast_arg_list(args)
6960  if __debug__:
6961  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
6962  args = _coerce_expr_list(args, ctx)
6963  if is_bv(args[0]):
6964  return reduce(lambda a, b: a * b, args, 1)
6965  else:
6966  _args, sz = _to_ast_array(args)
6967  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 7025 of file z3py.py.

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

7026 def prove(claim, **keywords):
7027  """Try to prove the given claim.
7028 
7029  This is a simple function for creating demonstrations. It tries to prove
7030  `claim` by showing the negation is unsatisfiable.
7031 
7032  >>> p, q = Bools('p q')
7033  >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
7034  proved
7035  """
7036  if __debug__:
7037  _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
7038  s = Solver()
7039  s.set(**keywords)
7040  s.add(Not(claim))
7041  if keywords.get('show', False):
7042  print s
7043  r = s.check()
7044  if r == unsat:
7045  print "proved"
7046  elif r == unknown:
7047  print "failed to prove"
7048  print s.model()
7049  else:
7050  print "counterexample"
7051  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 2597 of file z3py.py.

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

2598 def Q(a, b, ctx=None):
2599  """Return a Z3 rational a/b.
2600 
2601  If `ctx=None`, then the global context is used.
2602 
2603  >>> Q(3,5)
2604  3/5
2605  >>> Q(3,5).sort()
2606  Real
2607  """
2608  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 2582 of file z3py.py.

Referenced by Q().

2583 def RatVal(a, b, ctx=None):
2584  """Return a Z3 rational a/b.
2585 
2586  If `ctx=None`, then the global context is used.
2587 
2588  >>> RatVal(3,5)
2589  3/5
2590  >>> RatVal(3,5).sort()
2591  Real
2592  """
2593  if __debug__:
2594  _z3_assert(isinstance(a, int) or isinstance(a, str) or isinstance(a, long), "First argument cannot be converted into an integer")
2595  _z3_assert(isinstance(b, int) or isinstance(b, str) or isinstance(a, long), "Second argument cannot be converted into an integer")
2596  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 2657 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().

2658 def Real(name, ctx=None):
2659  """Return a real constant named `name`. If `ctx=None`, then the global context is used.
2660 
2661  >>> x = Real('x')
2662  >>> is_real(x)
2663  True
2664  >>> is_real(x + 1)
2665  True
2666  """
2667  ctx = _get_ctx(ctx)
2668  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 2669 of file z3py.py.

Referenced by is_div().

2670 def Reals(names, ctx=None):
2671  """Return a tuple of real constants.
2672 
2673  >>> x, y, z = Reals('x y z')
2674  >>> Sum(x, y, z)
2675  x + y + z
2676  >>> Sum(x, y, z).sort()
2677  Real
2678  """
2679  ctx = _get_ctx(ctx)
2680  if isinstance(names, str):
2681  names = names.split(" ")
2682  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 2520 of file z3py.py.

Referenced by ArithSortRef.cast(), FreshReal(), is_arith_sort(), Context.MkRealSort(), Real(), and QuantifierRef.var_sort().

2521 def RealSort(ctx=None):
2522  """Return the real sort in the given context. If `ctx=None`, then the global context is used.
2523 
2524  >>> RealSort()
2525  Real
2526  >>> x = Const('x', RealSort())
2527  >>> is_real(x)
2528  True
2529  >>> is_int(x)
2530  False
2531  >>> x.sort() == RealSort()
2532  True
2533  """
2534  ctx = _get_ctx(ctx)
2535  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 2564 of file z3py.py.

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

2565 def RealVal(val, ctx=None):
2566  """Return a Z3 real value.
2567 
2568  `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
2569  If `ctx=None`, then the global context is used.
2570 
2571  >>> RealVal(1)
2572  1
2573  >>> RealVal(1).sort()
2574  Real
2575  >>> RealVal("3/5")
2576  3/5
2577  >>> RealVal("1.5")
2578  3/2
2579  """
2580  ctx = _get_ctx(ctx)
2581  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
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 2683 of file z3py.py.

2684 def RealVector(prefix, sz, ctx=None):
2685  """Return a list of real constants of size `sz`.
2686 
2687  >>> X = RealVector('x', 3)
2688  >>> X
2689  [x__0, x__1, x__2]
2690  >>> Sum(X)
2691  x__0 + x__1 + x__2
2692  >>> Sum(X).sort()
2693  Real
2694  """
2695  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 6521 of file z3py.py.

6522 def Repeat(t, max=4294967295, ctx=None):
6523  """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
6524 
6525  >>> x, y = Ints('x y')
6526  >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
6527  >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
6528  >>> r = t(c)
6529  >>> for subgoal in r: print subgoal
6530  [x == 0, y == 0, x > y]
6531  [x == 0, y == 1, x > y]
6532  [x == 1, y == 0, x > y]
6533  [x == 1, y == 1, x > y]
6534  >>> t = Then(t, Tactic('propagate-values'))
6535  >>> t(c)
6536  [[x == 1, y == 0]]
6537  """
6538  t = _to_tactic(t, ctx)
6539  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 3685 of file z3py.py.

3686 def RepeatBitVec(n, a):
3687  """Return an expression representing `n` copies of `a`.
3688 
3689  >>> x = BitVec('x', 8)
3690  >>> n = RepeatBitVec(4, x)
3691  >>> n
3692  RepeatBitVec(4, x)
3693  >>> n.size()
3694  32
3695  >>> v0 = BitVecVal(10, 4)
3696  >>> print "%.x" % v0.as_long()
3697  a
3698  >>> v = simplify(RepeatBitVec(4, v0))
3699  >>> v.size()
3700  16
3701  >>> print "%.x" % v.as_long()
3702  aaaa
3703  """
3704  if __debug__:
3705  _z3_assert(isinstance(n, int), "First argument must be an integer")
3706  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3707  return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
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 3599 of file z3py.py.

3600 def RotateLeft(a, b):
3601  """Return an expression representing `a` rotated to the left `b` times.
3602 
3603  >>> a, b = BitVecs('a b', 16)
3604  >>> RotateLeft(a, b)
3605  RotateLeft(a, b)
3606  >>> simplify(RotateLeft(a, 0))
3607  a
3608  >>> simplify(RotateLeft(a, 16))
3609  a
3610  """
3611  _check_bv_args(a, b)
3612  a, b = _coerce_exprs(a, b)
3613  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 3614 of file z3py.py.

3615 def RotateRight(a, b):
3616  """Return an expression representing `a` rotated to the right `b` times.
3617 
3618  >>> a, b = BitVecs('a b', 16)
3619  >>> RotateRight(a, b)
3620  RotateRight(a, b)
3621  >>> simplify(RotateRight(a, 0))
3622  a
3623  >>> simplify(RotateRight(a, 16))
3624  a
3625  """
3626  _check_bv_args(a, b)
3627  a, b = _coerce_exprs(a, b)
3628  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 3944 of file z3py.py.

3945 def Select(a, i):
3946  """Return a Z3 select array expression.
3947 
3948  >>> a = Array('a', IntSort(), IntSort())
3949  >>> i = Int('i')
3950  >>> Select(a, i)
3951  a[i]
3952  >>> eq(Select(a, i), a[i])
3953  True
3954  """
3955  if __debug__:
3956  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
3957  return a[i]
def z3py.set_option (   args,
  kws 
)
Update parameters of the global context `main_ctx()`, and global configuration options of Z3Py. See `Context.set()`.

>>> set_option(precision=10)

Definition at line 223 of file z3py.py.

224 def set_option(*args, **kws):
225  """Update parameters of the global context `main_ctx()`, and global configuration options of Z3Py. See `Context.set()`.
226 
227  >>> set_option(precision=10)
228  """
229  new_kws = {}
230  for k, v in kws.iteritems():
231  if not set_pp_option(k, v):
232  new_kws[k] = v
233  main_ctx().set(*args, **new_kws)
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 3629 of file z3py.py.

3630 def SignExt(n, a):
3631  """Return a bit-vector expression with `n` extra sign-bits.
3632 
3633  >>> x = BitVec('x', 16)
3634  >>> n = SignExt(8, x)
3635  >>> n.size()
3636  24
3637  >>> n
3638  SignExt(8, x)
3639  >>> n.sort()
3640  BitVec(24)
3641  >>> v0 = BitVecVal(2, 2)
3642  >>> v0
3643  2
3644  >>> v0.size()
3645  2
3646  >>> v = simplify(SignExt(6, v0))
3647  >>> v
3648  254
3649  >>> v.size()
3650  8
3651  >>> print "%.x" % v.as_long()
3652  fe
3653  """
3654  if __debug__:
3655  _z3_assert(isinstance(n, int), "First argument must be an integer")
3656  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3657  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 5957 of file z3py.py.

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

5958 def SimpleSolver(ctx=None):
5959  """Return a simple general purpose solver with limited amount of preprocessing.
5960 
5961  >>> s = SimpleSolver()
5962  >>> x = Int('x')
5963  >>> s.add(x > 0)
5964  >>> s.check()
5965  sat
5966  """
5967  ctx = _get_ctx(ctx)
5968  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 6840 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().

6841 def simplify(a, *arguments, **keywords):
6842  """Simplify the expression `a` using the given options.
6843 
6844  This function has many options. Use `help_simplify` to obtain the complete list.
6845 
6846  >>> x = Int('x')
6847  >>> y = Int('y')
6848  >>> simplify(x + 1 + y + x + 1)
6849  2 + 2*x + y
6850  >>> simplify((x + 1)*(y + 1), som=True)
6851  1 + x + y + x*y
6852  >>> simplify(Distinct(x, y, 1), blast_distinct=True)
6853  And(Not(x == y), Not(x == 1), Not(y == 1))
6854  >>> simplify(And(x == 0, y == 1), elim_and=True)
6855  Not(Or(Not(x == 0), Not(y == 1)))
6856  """
6857  if __debug__:
6858  _z3_assert(is_expr(a), "Z3 expression expected")
6859  if len(arguments) > 0 or len(keywords) > 0:
6860  p = args2params(arguments, keywords, a.ctx)
6861  return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
6862  else:
6863  return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
def z3py.simplify_param_descrs ( )
Return the set of parameter descriptions for Z3 `simplify` procedure.

Definition at line 6868 of file z3py.py.

6869 def simplify_param_descrs():
6870  """Return the set of parameter descriptions for Z3 `simplify` procedure."""
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, b = Ints('a b')
>>> solve(a + b == 3, Or(a == 0, a == 1), a != 0)
[b = 2, a = 1]

Definition at line 6968 of file z3py.py.

Referenced by BV2Int(), and IsInt().

6969 def solve(*args, **keywords):
6970  """Solve the constraints `*args`.
6971 
6972  This is a simple function for creating demonstrations. It creates a solver,
6973  configure it using the options in `keywords`, adds the constraints
6974  in `args`, and invokes check.
6975 
6976  >>> a, b = Ints('a b')
6977  >>> solve(a + b == 3, Or(a == 0, a == 1), a != 0)
6978  [b = 2, a = 1]
6979  """
6980  s = Solver()
6981  s.set(**keywords)
6982  s.add(*args)
6983  if keywords.get('show', False):
6984  print s
6985  r = s.check()
6986  if r == unsat:
6987  print "no solution"
6988  elif r == unknown:
6989  print "failed to solve"
6990  try:
6991  print s.model()
6992  except Z3Exception:
6993  return
6994  else:
6995  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 6996 of file z3py.py.

6997 def solve_using(s, *args, **keywords):
6998  """Solve the constraints `*args` using solver `s`.
6999 
7000  This is a simple function for creating demonstrations. It is similar to `solve`,
7001  but it uses the given solver `s`.
7002  It configures solver `s` using the options in `keywords`, adds the constraints
7003  in `args`, and invokes check.
7004  """
7005  if __debug__:
7006  _z3_assert(isinstance(s, Solver), "Solver object expected")
7007  s.set(**keywords)
7008  s.add(*args)
7009  if keywords.get('show', False):
7010  print "Problem:"
7011  print s
7012  r = s.check()
7013  if r == unsat:
7014  print "no solution"
7015  elif r == unknown:
7016  print "failed to solve"
7017  try:
7018  print s.model()
7019  except Z3Exception:
7020  return
7021  else:
7022  if keywords.get('show', False):
7023  print "Solution:"
7024  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 5937 of file z3py.py.

5938 def SolverFor(logic, ctx=None):
5939  """Create a solver customized for the given logic.
5940 
5941  The parameter `logic` is a string. It should be contains
5942  the name of a SMT-LIB logic.
5943  See http://www.smtlib.org/ for the name of all available logics.
5944 
5945  >>> s = SolverFor("QF_LIA")
5946  >>> x = Int('x')
5947  >>> s.add(x > 0)
5948  >>> s.add(x < 2)
5949  >>> s.check()
5950  sat
5951  >>> s.model()
5952  [x = 1]
5953  """
5954  ctx = _get_ctx(ctx)
5955  logic = to_symbol(logic)
5956  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 2759 of file z3py.py.

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

2760 def Sqrt(a, ctx=None):
2761  """ Return a Z3 expression which represents the square root of a.
2762 
2763  >>> x = Real('x')
2764  >>> Sqrt(x)
2765  x**(1/2)
2766  """
2767  if not is_expr(a):
2768  ctx = _get_ctx(ctx)
2769  a = RealVal(a, ctx)
2770  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 3548 of file z3py.py.

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

3549 def SRem(a, b):
3550  """Create the Z3 expression signed remainder.
3551 
3552  Use the operator % for signed modulus, and URem() for unsigned remainder.
3553 
3554  >>> x = BitVec('x', 32)
3555  >>> y = BitVec('y', 32)
3556  >>> SRem(x, y)
3557  SRem(x, y)
3558  >>> SRem(x, y).sort()
3559  BitVec(32)
3560  >>> (x % y).sexpr()
3561  '(bvsmod x y)'
3562  >>> SRem(x, y).sexpr()
3563  '(bvsrem x y)'
3564  """
3565  _check_bv_args(a, b)
3566  a, b = _coerce_exprs(a, b)
3567  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 3928 of file z3py.py.

Referenced by is_array(), is_store(), and K().

3929 def Store(a, i, v):
3930  """Return a Z3 store array expression.
3931 
3932  >>> a = Array('a', IntSort(), IntSort())
3933  >>> i, v = Ints('i v')
3934  >>> s = Store(a, i, v)
3935  >>> s.sort()
3936  Array(Int, Int)
3937  >>> prove(s[i] == v)
3938  proved
3939  >>> j = Int('j')
3940  >>> prove(Implies(i != j, s[j] == a[j]))
3941  proved
3942  """
3943  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))
2 + y
>>> f = Function('f', IntSort(), IntSort())
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
2

Definition at line 6872 of file z3py.py.

6873 def substitute(t, *m):
6874  """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.
6875 
6876  >>> x = Int('x')
6877  >>> y = Int('y')
6878  >>> substitute(x + 1, (x, y + 1))
6879  2 + y
6880  >>> f = Function('f', IntSort(), IntSort())
6881  >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
6882  2
6883  """
6884  if isinstance(m, tuple):
6885  m1 = _get_args(m)
6886  if isinstance(m1, list):
6887  m = _get_args(m1)
6888  if __debug__:
6889  _z3_assert(is_expr(t), "Z3 expression expected")
6890  _z3_assert(all(map(lambda p: isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()), m)), "Z3 invalid substitution, expression pairs expected.")
6891  num = len(m)
6892  _from = (Ast * num)()
6893  _to = (Ast * num)()
6894  for i in range(num):
6895  _from[i] = m[i][0].as_ast()
6896  _to[i] = m[i][1].as_ast()
6897  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 6898 of file z3py.py.

6899 def substitute_vars(t, *m):
6900  """Substitute the free variables in t with the expression in m.
6901 
6902  >>> v0 = Var(0, IntSort())
6903  >>> v1 = Var(1, IntSort())
6904  >>> x = Int('x')
6905  >>> f = Function('f', IntSort(), IntSort(), IntSort())
6906  >>> # replace v0 with x+1 and v1 with x
6907  >>> substitute_vars(f(v0, v1), x + 1, x)
6908  f(x + 1, x)
6909  """
6910  if __debug__:
6911  _z3_assert(is_expr(t), "Z3 expression expected")
6912  _z3_assert(all(map(is_expr, m)), "Z3 invalid substitution, list of expressions expected.")
6913  num = len(m)
6914  _to = (Ast * num)()
6915  for i in range(num):
6916  _to[i] = m[i].as_ast()
6917  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 6918 of file z3py.py.

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

6919 def Sum(*args):
6920  """Create the sum of the Z3 expressions.
6921 
6922  >>> a, b, c = Ints('a b c')
6923  >>> Sum(a, b, c)
6924  a + b + c
6925  >>> Sum([a, b, c])
6926  a + b + c
6927  >>> A = IntVector('a', 5)
6928  >>> Sum(A)
6929  a__0 + a__1 + a__2 + a__3 + a__4
6930  """
6931  args = _get_args(args)
6932  if __debug__:
6933  _z3_assert(len(args) > 0, "Non empty list of arguments expected")
6934  ctx = _ctx_from_ast_arg_list(args)
6935  if __debug__:
6936  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
6937  args = _coerce_expr_list(args, ctx)
6938  if is_bv(args[0]):
6939  return reduce(lambda a, b: a + b, args, 0)
6940  else:
6941  _args, sz = _to_ast_array(args)
6942  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 6558 of file z3py.py.

Referenced by describe_tactics().

6559 def tactic_description(name, ctx=None):
6560  """Return a short description for the tactic named `name`.
6561 
6562  >>> d = tactic_description('simplify')
6563  """
6564  ctx = _get_ctx(ctx)
6565  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 6548 of file z3py.py.

Referenced by describe_tactics().

6549 def tactics(ctx=None):
6550  """Return a list of all available tactics in Z3.
6551 
6552  >>> l = tactics()
6553  >>> l.count('simplify') == 1
6554  True
6555  """
6556  ctx = _get_ctx(ctx)
6557  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 6440 of file z3py.py.

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

6441 def Then(*ts, **ks):
6442  """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
6443 
6444  >>> x, y = Ints('x y')
6445  >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
6446  >>> t(And(x == 0, y > x + 1))
6447  [[Not(y <= 1)]]
6448  >>> t(And(x == 0, y > x + 1)).as_expr()
6449  Not(y <= 1)
6450  """
6451  return AndThen(*ts, **ks)
def z3py.to_symbol (   s,
  ctx = None 
)
Convert an integer or string into a Z3 symbol.

Definition at line 82 of file z3py.py.

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

82 
83 def to_symbol(s, ctx=None):
84  """Convert an integer or string into a Z3 symbol."""
85  if isinstance(s, int):
86  return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
87  else:
88  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 2726 of file z3py.py.

Referenced by is_to_int().

2727 def ToInt(a):
2728  """ Return the Z3 expression ToInt(a).
2729 
2730  >>> x = Real('x')
2731  >>> x.sort()
2732  Real
2733  >>> n = ToInt(x)
2734  >>> n
2735  ToInt(x)
2736  >>> n.sort()
2737  Int
2738  """
2739  if __debug__:
2740  _z3_assert(a.is_real(), "Z3 real expression expected.")
2741  ctx = a.ctx
2742  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 2709 of file z3py.py.

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

2710 def ToReal(a):
2711  """ Return the Z3 expression ToReal(a).
2712 
2713  >>> x = Int('x')
2714  >>> x.sort()
2715  Int
2716  >>> n = ToReal(x)
2717  >>> n
2718  ToReal(x)
2719  >>> n.sort()
2720  Real
2721  """
2722  if __debug__:
2723  _z3_assert(a.is_int(), "Z3 integer expression expected.")
2724  ctx = a.ctx
2725  return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), 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 6540 of file z3py.py.

6541 def TryFor(t, ms, ctx=None):
6542  """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
6543 
6544  If `t` does not terminate in `ms` milliseconds, then it fails.
6545  """
6546  t = _to_tactic(t, ctx)
6547  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 3508 of file z3py.py.

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

3509 def UDiv(a, b):
3510  """Create the Z3 expression (unsigned) division `self / other`.
3511 
3512  Use the operator / for signed division.
3513 
3514  >>> x = BitVec('x', 32)
3515  >>> y = BitVec('y', 32)
3516  >>> UDiv(x, y)
3517  UDiv(x, y)
3518  >>> UDiv(x, y).sort()
3519  BitVec(32)
3520  >>> (x / y).sexpr()
3521  '(bvsdiv x y)'
3522  >>> UDiv(x, y).sexpr()
3523  '(bvudiv x y)'
3524  """
3525  _check_bv_args(a, b)
3526  a, b = _coerce_exprs(a, b)
3527  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 3474 of file z3py.py.

Referenced by BitVecRef.__ge__().

3475 def UGE(a, b):
3476  """Create the Z3 expression (unsigned) `other >= self`.
3477 
3478  Use the operator >= for signed greater than or equal to.
3479 
3480  >>> x, y = BitVecs('x y', 32)
3481  >>> UGE(x, y)
3482  UGE(x, y)
3483  >>> (x >= y).sexpr()
3484  '(bvsge x y)'
3485  >>> UGE(x, y).sexpr()
3486  '(bvuge x y)'
3487  """
3488  _check_bv_args(a, b)
3489  a, b = _coerce_exprs(a, b)
3490  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 3491 of file z3py.py.

Referenced by BitVecRef.__gt__().

3492 def UGT(a, b):
3493  """Create the Z3 expression (unsigned) `other > self`.
3494 
3495  Use the operator > for signed greater than.
3496 
3497  >>> x, y = BitVecs('x y', 32)
3498  >>> UGT(x, y)
3499  UGT(x, y)
3500  >>> (x > y).sexpr()
3501  '(bvsgt x y)'
3502  >>> UGT(x, y).sexpr()
3503  '(bvugt x y)'
3504  """
3505  _check_bv_args(a, b)
3506  a, b = _coerce_exprs(a, b)
3507  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 3440 of file z3py.py.

Referenced by BitVecRef.__le__().

3441 def ULE(a, b):
3442  """Create the Z3 expression (unsigned) `other <= self`.
3443 
3444  Use the operator <= for signed less than or equal to.
3445 
3446  >>> x, y = BitVecs('x y', 32)
3447  >>> ULE(x, y)
3448  ULE(x, y)
3449  >>> (x <= y).sexpr()
3450  '(bvsle x y)'
3451  >>> ULE(x, y).sexpr()
3452  '(bvule x y)'
3453  """
3454  _check_bv_args(a, b)
3455  a, b = _coerce_exprs(a, b)
3456  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 3457 of file z3py.py.

Referenced by BitVecRef.__lt__().

3458 def ULT(a, b):
3459  """Create the Z3 expression (unsigned) `other < self`.
3460 
3461  Use the operator < for signed less than.
3462 
3463  >>> x, y = BitVecs('x y', 32)
3464  >>> ULT(x, y)
3465  ULT(x, y)
3466  >>> (x < y).sexpr()
3467  '(bvslt x y)'
3468  >>> ULT(x, y).sexpr()
3469  '(bvult x y)'
3470  """
3471  _check_bv_args(a, b)
3472  a, b = _coerce_exprs(a, b)
3473  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 3907 of file z3py.py.

Referenced by Store().

3908 def Update(a, i, v):
3909  """Return a Z3 store array expression.
3910 
3911  >>> a = Array('a', IntSort(), IntSort())
3912  >>> i, v = Ints('i v')
3913  >>> s = Update(a, i, v)
3914  >>> s.sort()
3915  Array(Int, Int)
3916  >>> prove(s[i] == v)
3917  proved
3918  >>> j = Int('j')
3919  >>> prove(Implies(i != j, s[j] == a[j]))
3920  proved
3921  """
3922  if __debug__:
3923  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
3924  i = a.domain().cast(i)
3925  v = a.range().cast(v)
3926  ctx = a.ctx
3927  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 3528 of file z3py.py.

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

3529 def URem(a, b):
3530  """Create the Z3 expression (unsigned) remainder `self % other`.
3531 
3532  Use the operator % for signed modulus, and SRem() for signed remainder.
3533 
3534  >>> x = BitVec('x', 32)
3535  >>> y = BitVec('y', 32)
3536  >>> URem(x, y)
3537  URem(x, y)
3538  >>> URem(x, y).sort()
3539  BitVec(32)
3540  >>> (x % y).sexpr()
3541  '(bvsmod x y)'
3542  >>> URem(x, y).sexpr()
3543  '(bvurem x y)'
3544  """
3545  _check_bv_args(a, b)
3546  a, b = _coerce_exprs(a, b)
3547  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 1104 of file z3py.py.

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

1105 def Var(idx, s):
1106  """Create a Z3 free variable. Free variables are used to create quantified formulas.
1107 
1108  >>> Var(0, IntSort())
1109  Var(0)
1110  >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1111  False
1112  """
1113  if __debug__:
1114  _z3_assert(is_sort(s), "Z3 sort expected")
1115  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 6806 of file z3py.py.

6807 def When(p, t, ctx=None):
6808  """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6809 
6810  >>> t = When(Probe('size') > 2, Tactic('simplify'))
6811  >>> x, y = Ints('x y')
6812  >>> g = Goal()
6813  >>> g.add(x > 0)
6814  >>> g.add(y > 0)
6815  >>> t(g)
6816  [[x > 0, y > 0]]
6817  >>> g.add(x == y + 1)
6818  >>> t(g)
6819  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6820  """
6821  p = _to_probe(p, ctx)
6822  t = _to_tactic(t, ctx)
6823  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 6508 of file z3py.py.

Referenced by Goal.prec().

6509 def With(t, *args, **keys):
6510  """Return a tactic that applies tactic `t` using the given configuration options.
6511 
6512  >>> x, y = Ints('x y')
6513  >>> t = With(Tactic('simplify'), som=True)
6514  >>> t((x + 1)*(y + 2) == 0)
6515  [[2*x + y + x*y == -2]]
6516  """
6517  ctx = keys.get('ctx', None)
6518  t = _to_tactic(t, ctx)
6519  p = args2params(args, keys, t.ctx)
6520  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 1352 of file z3py.py.

1353 def Xor(a, b, ctx=None):
1354  """Create a Z3 Xor expression.
1355 
1356  >>> p, q = Bools('p q')
1357  >>> Xor(p, q)
1358  Xor(p, q)
1359  >>> simplify(Xor(p, q))
1360  Not(p) == q
1361  """
1362  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1363  s = BoolSort(ctx)
1364  a = s.cast(a)
1365  b = s.cast(b)
1366  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 3658 of file z3py.py.

3659 def ZeroExt(n, a):
3660  """Return a bit-vector expression with `n` extra zero-bits.
3661 
3662  >>> x = BitVec('x', 16)
3663  >>> n = ZeroExt(8, x)
3664  >>> n.size()
3665  24
3666  >>> n
3667  ZeroExt(8, x)
3668  >>> n.sort()
3669  BitVec(24)
3670  >>> v0 = BitVecVal(2, 2)
3671  >>> v0
3672  2
3673  >>> v0.size()
3674  2
3675  >>> v = simplify(ZeroExt(6, v0))
3676  >>> v
3677  2
3678  >>> v.size()
3679  8
3680  """
3681  if __debug__:
3682  _z3_assert(isinstance(n, int), "First argument must be an integer")
3683  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3684  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 96 of file z3py.py.

_main_ctx None

Definition at line 196 of file z3py.py.

tuple _Z3Python_error_handler _error_handler_fptr(_Z3python_error_handler_core)

Definition at line 114 of file z3py.py.

tuple sat CheckSatResult(Z3_L_TRUE)

Definition at line 5620 of file z3py.py.

tuple unknown CheckSatResult(Z3_L_UNDEF)

Definition at line 5622 of file z3py.py.

tuple unsat CheckSatResult(Z3_L_FALSE)

Definition at line 5621 of file z3py.py.