Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

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

Functions

def enable_trace (msg)
 
def disable_trace (msg)
 
def get_version_string ()
 
def get_version ()
 
def open_log (fname)
 
def append_log (s)
 
def to_symbol
 
def main_ctx ()
 
def set_param (args, kws)
 
def reset_params ()
 
def set_option (args, kws)
 
def get_param (name)
 
def is_ast (a)
 
def eq (a, b)
 
def is_sort (s)
 
def DeclareSort
 
def is_func_decl (a)
 
def Function (name, sig)
 
def is_expr (a)
 
def is_app (a)
 
def is_const (a)
 
def is_var (a)
 
def get_var_index (a)
 
def is_app_of (a, k)
 
def If
 
def Distinct (args)
 
def Const (name, sort)
 
def Consts (names, sort)
 
def Var (idx, s)
 
def RealVar
 
def RealVarVector
 
def is_bool (a)
 
def is_true (a)
 
def is_false (a)
 
def is_and (a)
 
def is_or (a)
 
def is_not (a)
 
def is_eq (a)
 
def is_distinct (a)
 
def BoolSort
 
def BoolVal
 
def Bool
 
def Bools
 
def BoolVector
 
def FreshBool
 
def Implies
 
def Xor
 
def Not
 
def And (args)
 
def Or (args)
 
def is_pattern (a)
 
def MultiPattern (args)
 
def is_quantifier (a)
 
def ForAll
 
def Exists
 
def is_arith_sort (s)
 
def is_arith (a)
 
def is_int (a)
 
def is_real (a)
 
def is_int_value (a)
 
def is_rational_value (a)
 
def is_algebraic_value (a)
 
def is_add (a)
 
def is_mul (a)
 
def is_sub (a)
 
def is_div (a)
 
def is_idiv (a)
 
def is_mod (a)
 
def is_le (a)
 
def is_lt (a)
 
def is_ge (a)
 
def is_gt (a)
 
def is_is_int (a)
 
def is_to_real (a)
 
def is_to_int (a)
 
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 (a)
 
def ToInt (a)
 
def IsInt (a)
 
def Sqrt
 
def Cbrt
 
def is_bv_sort (s)
 
def is_bv (a)
 
def is_bv_value (a)
 
def BV2Int (a)
 
def BitVecSort
 
def BitVecVal
 
def BitVec
 
def BitVecs
 
def Concat (args)
 
def Extract (high, low, a)
 
def ULE (a, b)
 
def ULT (a, b)
 
def UGE (a, b)
 
def UGT (a, b)
 
def UDiv (a, b)
 
def URem (a, b)
 
def SRem (a, b)
 
def LShR (a, b)
 
def RotateLeft (a, b)
 
def RotateRight (a, b)
 
def SignExt (n, a)
 
def ZeroExt (n, a)
 
def RepeatBitVec (n, a)
 
def is_array (a)
 
def is_const_array (a)
 
def is_K (a)
 
def is_map (a)
 
def get_map_func (a)
 
def ArraySort (d, r)
 
def Array (name, dom, rng)
 
def Update (a, i, v)
 
def Store (a, i, v)
 
def Select (a, i)
 
def Map (f, args)
 
def K (dom, v)
 
def is_select (a)
 
def is_store (a)
 
def CreateDatatypes (ds)
 
def EnumSort
 
def args2params
 
def is_as_array (n)
 
def get_as_array_func (n)
 
def SolverFor
 
def SimpleSolver
 
def AndThen (ts, ks)
 
def Then (ts, ks)
 
def OrElse (ts, ks)
 
def ParOr (ts, ks)
 
def ParThen
 
def ParAndThen
 
def With (t, args, keys)
 
def Repeat
 
def TryFor
 
def tactics
 
def tactic_description
 
def describe_tactics ()
 
def is_probe (p)
 
def probes
 
def probe_description
 
def describe_probes ()
 
def FailIf
 
def When
 
def Cond
 
def simplify (a, arguments, keywords)
 Utils. More...
 
def help_simplify ()
 
def simplify_param_descrs ()
 
def substitute (t, m)
 
def substitute_vars (t, m)
 
def Sum (args)
 
def Product (args)
 
def solve (args, keywords)
 
def solve_using (s, args, keywords)
 
def prove (claim, keywords)
 
def parse_smt2_string
 
def parse_smt2_file
 
def Interpolant
 
def tree_interpolant
 
def binary_interpolant
 
def sequence_interpolant
 

Variables

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

Function Documentation

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

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

Definition at line 1468 of file z3py.py.

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

1468 def And(*args):
1469  """Create a Z3 and-expression or and-probe.
1470 
1471  >>> p, q, r = Bools('p q r')
1472  >>> And(p, q, r)
1473  And(p, q, r)
1474  >>> P = BoolVector('p', 5)
1475  >>> And(P)
1476  And(p__0, p__1, p__2, p__3, p__4)
1477  """
1478  last_arg = None
1479  if len(args) > 0:
1480  last_arg = args[len(args)-1]
1481  if isinstance(last_arg, Context):
1482  ctx = args[len(args)-1]
1483  args = args[:len(args)-1]
1484  else:
1485  ctx = main_ctx()
1486  args = _get_args(args)
1487  ctx_args = _ctx_from_ast_arg_list(args, ctx)
1488  if __debug__:
1489  _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
1490  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1491  if _has_probe(args):
1492  return _probe_and(args, ctx)
1493  else:
1494  args = _coerce_expr_list(args, ctx)
1495  _args, sz = _to_ast_array(args)
1496  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1497 
def And(args)
Definition: z3py.py:1468
def main_ctx()
Definition: z3py.py:188
Z3_ast Z3_API Z3_mk_and(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].The array args must have num_arg...
def z3py.AndThen (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` in sequence.

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

Definition at line 6537 of file z3py.py.

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

6537 def AndThen(*ts, **ks):
6538  """Return a tactic that applies the tactics in `*ts` in sequence.
6539 
6540  >>> x, y = Ints('x y')
6541  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
6542  >>> t(And(x == 0, y > x + 1))
6543  [[Not(y <= 1)]]
6544  >>> t(And(x == 0, y > x + 1)).as_expr()
6545  Not(y <= 1)
6546  """
6547  if __debug__:
6548  _z3_assert(len(ts) >= 2, "At least two arguments expected")
6549  ctx = ks.get('ctx', None)
6550  num = len(ts)
6551  r = ts[0]
6552  for i in range(num - 1):
6553  r = _and_then(r, ts[i+1], ctx)
6554  return r
6555 
def AndThen(ts, ks)
Definition: z3py.py:6537
def z3py.append_log (   s)
Append user-defined string to interaction log. 

Definition at line 90 of file z3py.py.

90 def append_log(s):
91  """Append user-defined string to interaction log. """
92  Z3_append_log(s)
93 
void Z3_API Z3_append_log(__in Z3_string string)
Append user-defined string to interaction log.
def append_log(s)
Definition: z3py.py:90
def z3py.args2params (   arguments,
  keywords,
  ctx = None 
)
Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'

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

Definition at line 4467 of file z3py.py.

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

4467 def args2params(arguments, keywords, ctx=None):
4468  """Convert python arguments into a Z3_params object.
4469  A ':' is added to the keywords, and '_' is replaced with '-'
4470 
4471  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
4472  (params model true relevancy 2 elim_and true)
4473  """
4474  if __debug__:
4475  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
4476  prev = None
4477  r = ParamsRef(ctx)
4478  for a in arguments:
4479  if prev == None:
4480  prev = a
4481  else:
4482  r.set(prev, a)
4483  prev = None
4484  for k in keywords:
4485  v = keywords[k]
4486  r.set(k, v)
4487  return r
4488 
def args2params
Definition: z3py.py:4467
Parameter Sets.
Definition: z3py.py:4430
def z3py.Array (   name,
  dom,
  rng 
)
Return an array constant named `name` with the given domain and range sorts.

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

Definition at line 3976 of file z3py.py.

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

3976 def Array(name, dom, rng):
3977  """Return an array constant named `name` with the given domain and range sorts.
3978 
3979  >>> a = Array('a', IntSort(), IntSort())
3980  >>> a.sort()
3981  Array(Int, Int)
3982  >>> a[0]
3983  a[0]
3984  """
3985  s = ArraySort(dom, rng)
3986  ctx = s.ctx
3987  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
3988 
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
def Array(name, dom, rng)
Definition: z3py.py:3976
def ArraySort(d, r)
Definition: z3py.py:3955
def to_symbol
Definition: z3py.py:94
def z3py.ArraySort (   d,
  r 
)
Return the Z3 array sort with the given domain and range sorts.

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

Definition at line 3955 of file z3py.py.

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

3955 def ArraySort(d, r):
3956  """Return the Z3 array sort with the given domain and range sorts.
3957 
3958  >>> A = ArraySort(IntSort(), BoolSort())
3959  >>> A
3960  Array(Int, Bool)
3961  >>> A.domain()
3962  Int
3963  >>> A.range()
3964  Bool
3965  >>> AA = ArraySort(IntSort(), A)
3966  >>> AA
3967  Array(Int, Array(Int, Bool))
3968  """
3969  if __debug__:
3970  _z3_assert(is_sort(d), "Z3 sort expected")
3971  _z3_assert(is_sort(r), "Z3 sort expected")
3972  _z3_assert(d.ctx == r.ctx, "Context mismatch")
3973  ctx = d.ctx
3974  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
3975 
Z3_sort Z3_API Z3_mk_array_sort(__in Z3_context c, __in Z3_sort domain, __in Z3_sort range)
Create an array type.
Arrays.
Definition: z3py.py:3822
def is_sort(s)
Definition: z3py.py:532
def ArraySort(d, r)
Definition: z3py.py:3955
def z3py.binary_interpolant (   a,
  b,
  p = None,
  ctx = None 
)
Compute an interpolant for a binary conjunction.

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

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

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

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

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

Definition at line 7368 of file z3py.py.

7368 def binary_interpolant(a,b,p=None,ctx=None):
7369  """Compute an interpolant for a binary conjunction.
7370 
7371  If a & b is unsatisfiable, returns an interpolant for a & b.
7372  This is a formula phi such that
7373 
7374  1) a implies phi
7375  2) b implies not phi
7376  3) All the uninterpreted symbols of phi occur in both a and b.
7377 
7378  If a & b is satisfiable, raises an object of class ModelRef
7379  that represents a model of a &b.
7380 
7381  If parameters p are supplied, these are used in creating the
7382  solver that determines satisfiability.
7383 
7384  x = Int('x')
7385  print binary_interpolant(x<0,x>2)
7386  Not(x >= 0)
7387  """
7388  f = And(Interpolant(a),b)
7389  return tree_interpolant(f,p,ctx)[0]
7390 
def And(args)
Definition: z3py.py:1468
def Interpolant
Definition: z3py.py:7295
def tree_interpolant
Definition: z3py.py:7309
def binary_interpolant
Definition: z3py.py:7368
def z3py.BitVec (   name,
  bv,
  ctx = None 
)
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
If `ctx=None`, then the global context is used.

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

Definition at line 3465 of file z3py.py.

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

3465 def BitVec(name, bv, ctx=None):
3466  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3467  If `ctx=None`, then the global context is used.
3468 
3469  >>> x = BitVec('x', 16)
3470  >>> is_bv(x)
3471  True
3472  >>> x.size()
3473  16
3474  >>> x.sort()
3475  BitVec(16)
3476  >>> word = BitVecSort(16)
3477  >>> x2 = BitVec('x', word)
3478  >>> eq(x, x2)
3479  True
3480  """
3481  if isinstance(bv, BitVecSortRef):
3482  ctx = bv.ctx
3483  else:
3484  ctx = _get_ctx(ctx)
3485  bv = BitVecSort(bv, ctx)
3486  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
3487 
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
def BitVecSort
Definition: z3py.py:3435
def BitVec
Definition: z3py.py:3465
def to_symbol
Definition: z3py.py:94
def z3py.BitVecs (   names,
  bv,
  ctx = None 
)
Return a tuple of bit-vector constants of size bv. 

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

Definition at line 3488 of file z3py.py.

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

3488 def BitVecs(names, bv, ctx=None):
3489  """Return a tuple of bit-vector constants of size bv.
3490 
3491  >>> x, y, z = BitVecs('x y z', 16)
3492  >>> x.size()
3493  16
3494  >>> x.sort()
3495  BitVec(16)
3496  >>> Sum(x, y, z)
3497  0 + x + y + z
3498  >>> Product(x, y, z)
3499  1*x*y*z
3500  >>> simplify(Product(x, y, z))
3501  x*y*z
3502  """
3503  ctx = _get_ctx(ctx)
3504  if isinstance(names, str):
3505  names = names.split(" ")
3506  return [BitVec(name, bv, ctx) for name in names]
3507 
def BitVec
Definition: z3py.py:3465
def BitVecs
Definition: z3py.py:3488
def z3py.BitVecSort (   sz,
  ctx = None 
)
Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.

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

Definition at line 3435 of file z3py.py.

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

3435 def BitVecSort(sz, ctx=None):
3436  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3437 
3438  >>> Byte = BitVecSort(8)
3439  >>> Word = BitVecSort(16)
3440  >>> Byte
3441  BitVec(8)
3442  >>> x = Const('x', Byte)
3443  >>> eq(x, BitVec('x', 8))
3444  True
3445  """
3446  ctx = _get_ctx(ctx)
3447  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
3448 
Z3_sort Z3_API Z3_mk_bv_sort(__in Z3_context c, __in unsigned sz)
Create a bit-vector type of the given size.
def BitVecSort
Definition: z3py.py:3435
Bit-Vectors.
Definition: z3py.py:2897
def z3py.BitVecVal (   val,
  bv,
  ctx = None 
)
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.

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

Definition at line 3449 of file z3py.py.

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

3449 def BitVecVal(val, bv, ctx=None):
3450  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3451 
3452  >>> v = BitVecVal(10, 32)
3453  >>> v
3454  10
3455  >>> print("0x%.8x" % v.as_long())
3456  0x0000000a
3457  """
3458  if is_bv_sort(bv):
3459  ctx = bv.ctx
3460  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3461  else:
3462  ctx = _get_ctx(ctx)
3463  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3464 
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
def BitVecSort
Definition: z3py.py:3435
def BitVecVal
Definition: z3py.py:3449
def is_bv_sort(s)
Definition: z3py.py:2929
def z3py.Bool (   name,
  ctx = None 
)
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.

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

Definition at line 1360 of file z3py.py.

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

1360 def Bool(name, ctx=None):
1361  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1362 
1363  >>> p = Bool('p')
1364  >>> q = Bool('q')
1365  >>> And(p, q)
1366  And(p, q)
1367  """
1368  ctx = _get_ctx(ctx)
1369  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1370 
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
def BoolSort
Definition: z3py.py:1325
def Bool
Definition: z3py.py:1360
def to_symbol
Definition: z3py.py:94
def z3py.Bools (   names,
  ctx = None 
)
Return a tuple of Boolean constants. 

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

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

Definition at line 1371 of file z3py.py.

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

1371 def Bools(names, ctx=None):
1372  """Return a tuple of Boolean constants.
1373 
1374  `names` is a single string containing all names separated by blank spaces.
1375  If `ctx=None`, then the global context is used.
1376 
1377  >>> p, q, r = Bools('p q r')
1378  >>> And(p, Or(q, r))
1379  And(p, Or(q, r))
1380  """
1381  ctx = _get_ctx(ctx)
1382  if isinstance(names, str):
1383  names = names.split(" ")
1384  return [Bool(name, ctx) for name in names]
1385 
def Bools
Definition: z3py.py:1371
def Bool
Definition: z3py.py:1360
def z3py.BoolSort (   ctx = None)
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.

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

Definition at line 1325 of file z3py.py.

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

1325 def BoolSort(ctx=None):
1326  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1327 
1328  >>> BoolSort()
1329  Bool
1330  >>> p = Const('p', BoolSort())
1331  >>> is_bool(p)
1332  True
1333  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1334  >>> r(0, 1)
1335  r(0, 1)
1336  >>> is_bool(r(0, 1))
1337  True
1338  """
1339  ctx = _get_ctx(ctx)
1340  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1341 
def BoolSort
Definition: z3py.py:1325
def is_bool(a)
Definition: z3py.py:1225
def z3py.BoolVal (   val,
  ctx = None 
)
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.

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

Definition at line 1342 of file z3py.py.

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

1342 def BoolVal(val, ctx=None):
1343  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1344 
1345  >>> BoolVal(True)
1346  True
1347  >>> is_true(BoolVal(True))
1348  True
1349  >>> is_true(True)
1350  False
1351  >>> is_false(BoolVal(False))
1352  True
1353  """
1354  ctx = _get_ctx(ctx)
1355  if val == False:
1356  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1357  else:
1358  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1359 
def BoolVal
Definition: z3py.py:1342
Z3_ast Z3_API Z3_mk_true(__in Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_false(__in Z3_context c)
Create an AST node representing false.
def z3py.BoolVector (   prefix,
  sz,
  ctx = None 
)
Return a list of Boolean constants of size `sz`.

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

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

Definition at line 1386 of file z3py.py.

Referenced by And(), and Or().

1386 def BoolVector(prefix, sz, ctx=None):
1387  """Return a list of Boolean constants of size `sz`.
1388 
1389  The constants are named using the given prefix.
1390  If `ctx=None`, then the global context is used.
1391 
1392  >>> P = BoolVector('p', 3)
1393  >>> P
1394  [p__0, p__1, p__2]
1395  >>> And(P)
1396  And(p__0, p__1, p__2)
1397  """
1398  return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
1399 
def Bool
Definition: z3py.py:1360
def BoolVector
Definition: z3py.py:1386
def z3py.BV2Int (   a)
Return the Z3 expression BV2Int(a). 

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

Definition at line 3417 of file z3py.py.

3417 def BV2Int(a):
3418  """Return the Z3 expression BV2Int(a).
3419 
3420  >>> b = BitVec('b', 3)
3421  >>> BV2Int(b).sort()
3422  Int
3423  >>> x = Int('x')
3424  >>> x > BV2Int(b)
3425  x > BV2Int(b)
3426  >>> solve(x > BV2Int(b), b == 1, x < 3)
3427  [b = 1, x = 2]
3428  """
3429  if __debug__:
3430  _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
3431  ctx = a.ctx
3432  ## investigate problem with bv2int
3433  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
3434 
Z3_ast Z3_API Z3_mk_bv2int(__in Z3_context c, __in Z3_ast t1, Z3_bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
def BV2Int(a)
Definition: z3py.py:3417
def is_bv(a)
Definition: z3py.py:3390
def z3py.Cbrt (   a,
  ctx = None 
)
Return a Z3 expression which represents the cubic root of a. 

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

Definition at line 2879 of file z3py.py.

2879 def Cbrt(a, ctx=None):
2880  """ Return a Z3 expression which represents the cubic root of a.
2881 
2882  >>> x = Real('x')
2883  >>> Cbrt(x)
2884  x**(1/3)
2885  """
2886  if not is_expr(a):
2887  ctx = _get_ctx(ctx)
2888  a = RealVal(a, ctx)
2889  return a ** "1/3"
2890 
def Cbrt
Definition: z3py.py:2879
def RealVal
Definition: z3py.py:2672
def is_expr(a)
Definition: z3py.py:950
def z3py.Concat (   args)
Create a Z3 bit-vector concatenation expression. 

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

Definition at line 3508 of file z3py.py.

Referenced by BitVecRef.size().

3508 def Concat(*args):
3509  """Create a Z3 bit-vector concatenation expression.
3510 
3511  >>> v = BitVecVal(1, 4)
3512  >>> Concat(v, v+1, v)
3513  Concat(Concat(1, 1 + 1), 1)
3514  >>> simplify(Concat(v, v+1, v))
3515  289
3516  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3517  121
3518  """
3519  args = _get_args(args)
3520  if __debug__:
3521  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
3522  _z3_assert(len(args) >= 2, "At least two arguments expected.")
3523  ctx = args[0].ctx
3524  r = args[0]
3525  for i in range(len(args) - 1):
3526  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3527  return r
3528 
Z3_ast Z3_API Z3_mk_concat(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Concatenate the given bit-vectors.
def is_bv(a)
Definition: z3py.py:3390
def Concat(args)
Definition: z3py.py:3508
def z3py.Cond (   p,
  t1,
  t2,
  ctx = None 
)
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.

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

Definition at line 6940 of file z3py.py.

Referenced by If().

6940 def Cond(p, t1, t2, ctx=None):
6941  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
6942 
6943  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
6944  """
6945  p = _to_probe(p, ctx)
6946  t1 = _to_tactic(t1, ctx)
6947  t2 = _to_tactic(t2, ctx)
6948  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
6949 
Z3_tactic Z3_API Z3_tactic_cond(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
def Cond
Definition: z3py.py:6940
def z3py.Const (   name,
  sort 
)
Create a constant of the given sort.

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

Definition at line 1134 of file z3py.py.

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

1134 def Const(name, sort):
1135  """Create a constant of the given sort.
1136 
1137  >>> Const('x', IntSort())
1138  x
1139  """
1140  if __debug__:
1141  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1142  ctx = sort.ctx
1143  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1144 
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
def Const(name, sort)
Definition: z3py.py:1134
def to_symbol
Definition: z3py.py:94
def z3py.Consts (   names,
  sort 
)
Create a several constants of the given sort. 

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

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

Definition at line 1145 of file z3py.py.

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

1145 def Consts(names, sort):
1146  """Create a several constants of the given sort.
1147 
1148  `names` is a string containing the names of all constants to be created.
1149  Blank spaces separate the names of different constants.
1150 
1151  >>> x, y, z = Consts('x y z', IntSort())
1152  >>> x + y + z
1153  x + y + z
1154  """
1155  if isinstance(names, str):
1156  names = names.split(" ")
1157  return [Const(name, sort) for name in names]
1158 
def Consts(names, sort)
Definition: z3py.py:1145
def Const(name, sort)
Definition: z3py.py:1134
def z3py.CreateDatatypes (   ds)
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.

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

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

Definition at line 4209 of file z3py.py.

Referenced by Datatype.create().

4210  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4211 
4212  In the following example we define a Tree-List using two mutually recursive datatypes.
4213 
4214  >>> TreeList = Datatype('TreeList')
4215  >>> Tree = Datatype('Tree')
4216  >>> # Tree has two constructors: leaf and node
4217  >>> Tree.declare('leaf', ('val', IntSort()))
4218  >>> # a node contains a list of trees
4219  >>> Tree.declare('node', ('children', TreeList))
4220  >>> TreeList.declare('nil')
4221  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4222  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4223  >>> Tree.val(Tree.leaf(10))
4224  val(leaf(10))
4225  >>> simplify(Tree.val(Tree.leaf(10)))
4226  10
4227  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4228  >>> n1
4229  node(cons(leaf(10), cons(leaf(20), nil)))
4230  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4231  >>> simplify(n2 == n1)
4232  False
4233  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4234  True
4235  """
4236  ds = _get_args(ds)
4237  if __debug__:
4238  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4239  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
4240  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
4241  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
4242  ctx = ds[0].ctx
4243  num = len(ds)
4244  names = (Symbol * num)()
4245  out = (Sort * num)()
4246  clists = (ConstructorList * num)()
4247  to_delete = []
4248  for i in range(num):
4249  d = ds[i]
4250  names[i] = to_symbol(d.name, ctx)
4251  num_cs = len(d.constructors)
4252  cs = (Constructor * num_cs)()
4253  for j in range(num_cs):
4254  c = d.constructors[j]
4255  cname = to_symbol(c[0], ctx)
4256  rname = to_symbol(c[1], ctx)
4257  fs = c[2]
4258  num_fs = len(fs)
4259  fnames = (Symbol * num_fs)()
4260  sorts = (Sort * num_fs)()
4261  refs = (ctypes.c_uint * num_fs)()
4262  for k in range(num_fs):
4263  fname = fs[k][0]
4264  ftype = fs[k][1]
4265  fnames[k] = to_symbol(fname, ctx)
4266  if isinstance(ftype, Datatype):
4267  if __debug__:
4268  _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4269  sorts[k] = None
4270  refs[k] = ds.index(ftype)
4271  else:
4272  if __debug__:
4273  _z3_assert(is_sort(ftype), "Z3 sort expected")
4274  sorts[k] = ftype.ast
4275  refs[k] = 0
4276  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4277  to_delete.append(ScopedConstructor(cs[j], ctx))
4278  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4279  to_delete.append(ScopedConstructorList(clists[i], ctx))
4280  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4281  result = []
4282  ## Create a field for every constructor, recognizer and accessor
4283  for i in range(num):
4284  dref = DatatypeSortRef(out[i], ctx)
4285  num_cs = dref.num_constructors()
4286  for j in range(num_cs):
4287  cref = dref.constructor(j)
4288  cref_name = cref.name()
4289  cref_arity = cref.arity()
4290  if cref.arity() == 0:
4291  cref = cref()
4292  setattr(dref, cref_name, cref)
4293  rref = dref.recognizer(j)
4294  setattr(dref, rref.name(), rref)
4295  for k in range(cref_arity):
4296  aref = dref.accessor(j, k)
4297  setattr(dref, aref.name(), aref)
4298  result.append(dref)
4299  return tuple(result)
4300 
def CreateDatatypes(ds)
Definition: z3py.py:4209
def is_sort(s)
Definition: z3py.py:532
BEGIN_MLAPI_EXCLUDE Z3_constructor Z3_API Z3_mk_constructor(__in Z3_context c, __in Z3_symbol name, __in Z3_symbol recognizer, __in unsigned num_fields, __in_ecount(num_fields) Z3_symbol const field_names[], __in_ecount(num_fields) Z3_sort_opt const sorts[], __in_ecount(num_fields) unsigned sort_refs[])
Create a constructor.
void Z3_API Z3_mk_datatypes(__in Z3_context c, __in unsigned num_sorts, __in_ecount(num_sorts) Z3_symbol const sort_names[], __out_ecount(num_sorts) Z3_sort sorts[], __inout_ecount(num_sorts) Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
def to_symbol
Definition: z3py.py:94
Z3_constructor_list Z3_API Z3_mk_constructor_list(__in Z3_context c, __in unsigned num_constructors, __in_ecount(num_constructors) Z3_constructor const constructors[])
Create list of constructors.
def z3py.DeclareSort (   name,
  ctx = None 
)
Create a new uninterpred sort named `name`.

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

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

Definition at line 563 of file z3py.py.

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

563 def DeclareSort(name, ctx=None):
564  """Create a new uninterpred sort named `name`.
565 
566  If `ctx=None`, then the new sort is declared in the global Z3Py context.
567 
568  >>> A = DeclareSort('A')
569  >>> a = Const('a', A)
570  >>> b = Const('b', A)
571  >>> a.sort() == A
572  True
573  >>> b.sort() == A
574  True
575  >>> a == b
576  a == b
577  """
578  ctx = _get_ctx(ctx)
579  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
580 
Z3_sort Z3_API Z3_mk_uninterpreted_sort(__in Z3_context c, __in Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
def DeclareSort
Definition: z3py.py:563
def to_symbol
Definition: z3py.py:94
def z3py.describe_probes ( )
Display a (tabular) description of all available probes in Z3.

Definition at line 6870 of file z3py.py.

6871  """Display a (tabular) description of all available probes in Z3."""
6872  if in_html_mode():
6873  even = True
6874  print('<table border="1" cellpadding="2" cellspacing="0">')
6875  for p in probes():
6876  if even:
6877  print('<tr style="background-color:#CFCFCF">')
6878  even = False
6879  else:
6880  print('<tr>')
6881  even = True
6882  print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
6883  print('</table>')
6884  else:
6885  for p in probes():
6886  print('%s : %s' % (p, probe_description(p)))
6887 
def probe_description
Definition: z3py.py:6862
def probes
Definition: z3py.py:6852
def describe_probes()
Definition: z3py.py:6870
def z3py.describe_tactics ( )
Display a (tabular) description of all available tactics in Z3.

Definition at line 6682 of file z3py.py.

6683  """Display a (tabular) description of all available tactics in Z3."""
6684  if in_html_mode():
6685  even = True
6686  print('<table border="1" cellpadding="2" cellspacing="0">')
6687  for t in tactics():
6688  if even:
6689  print('<tr style="background-color:#CFCFCF">')
6690  even = False
6691  else:
6692  print('<tr>')
6693  even = True
6694  print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
6695  print('</table>')
6696  else:
6697  for t in tactics():
6698  print('%s : %s' % (t, tactic_description(t)))
6699 
def describe_tactics()
Definition: z3py.py:6682
def tactic_description
Definition: z3py.py:6674
def tactics
Definition: z3py.py:6664
def z3py.disable_trace (   msg)

Definition at line 61 of file z3py.py.

61 def disable_trace(msg):
62  Z3_disable_trace(msg)
63 
def disable_trace(msg)
Definition: z3py.py:61
void Z3_API Z3_disable_trace(__in Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def z3py.Distinct (   args)
Create a Z3 distinct expression. 

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

Definition at line 1103 of file z3py.py.

1103 def Distinct(*args):
1104  """Create a Z3 distinct expression.
1105 
1106  >>> x = Int('x')
1107  >>> y = Int('y')
1108  >>> Distinct(x, y)
1109  x != y
1110  >>> z = Int('z')
1111  >>> Distinct(x, y, z)
1112  Distinct(x, y, z)
1113  >>> simplify(Distinct(x, y, z))
1114  Distinct(x, y, z)
1115  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1116  And(Not(x == y), Not(x == z), Not(y == z))
1117  """
1118  args = _get_args(args)
1119  ctx = _ctx_from_ast_arg_list(args)
1120  if __debug__:
1121  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
1122  args = _coerce_expr_list(args, ctx)
1123  _args, sz = _to_ast_array(args)
1124  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1125 
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
def Distinct(args)
Definition: z3py.py:1103
def z3py.enable_trace (   msg)

Definition at line 58 of file z3py.py.

58 def enable_trace(msg):
59  Z3_enable_trace(msg)
60 
void Z3_API Z3_enable_trace(__in Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def enable_trace(msg)
Definition: z3py.py:58
def z3py.EnumSort (   name,
  values,
  ctx = None 
)
Return a new enumeration sort named `name` containing the given values.

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

Definition at line 4398 of file z3py.py.

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

4398 def EnumSort(name, values, ctx=None):
4399  """Return a new enumeration sort named `name` containing the given values.
4400 
4401  The result is a pair (sort, list of constants).
4402  Example:
4403  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
4404  """
4405  if __debug__:
4406  _z3_assert(isinstance(name, str), "Name must be a string")
4407  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
4408  _z3_assert(len(values) > 0, "At least one value expected")
4409  ctx = _get_ctx(ctx)
4410  num = len(values)
4411  _val_names = (Symbol * num)()
4412  for i in range(num):
4413  _val_names[i] = to_symbol(values[i])
4414  _values = (FuncDecl * num)()
4415  _testers = (FuncDecl * num)()
4416  name = to_symbol(name)
4417  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
4418  V = []
4419  for i in range(num):
4420  V.append(FuncDeclRef(_values[i], ctx))
4421  V = [a() for a in V]
4422  return S, V
4423 
Function Declarations.
Definition: z3py.py:587
Z3_sort Z3_API Z3_mk_enumeration_sort(__in Z3_context c, __in Z3_symbol name, __in unsigned n, __in_ecount(n) Z3_symbol const enum_names[], __out_ecount(n) Z3_func_decl enum_consts[], __out_ecount(n) Z3_func_decl enum_testers[])
Create a enumeration sort.
def EnumSort
Definition: z3py.py:4398
def to_symbol
Definition: z3py.py:94
def z3py.eq (   a,
  b 
)
Return `True` if `a` and `b` are structurally identical AST nodes.

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

Definition at line 372 of file z3py.py.

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

372 def eq(a, b):
373  """Return `True` if `a` and `b` are structurally identical AST nodes.
374 
375  >>> x = Int('x')
376  >>> y = Int('y')
377  >>> eq(x, y)
378  False
379  >>> eq(x + 1, x + 1)
380  True
381  >>> eq(x + 1, 1 + x)
382  False
383  >>> eq(simplify(x + 1), simplify(1 + x))
384  True
385  """
386  if __debug__:
387  _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
388  return a.eq(b)
389 
def eq(a, b)
Definition: z3py.py:372
def is_ast(a)
Definition: z3py.py:352
def z3py.Exists (   vs,
  body,
  weight = 1,
  qid = "",
  skid = "",
  patterns = [],
  no_patterns = [] 
)
Create a Z3 exists formula.

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

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

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

Definition at line 1808 of file z3py.py.

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

1808 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1809  """Create a Z3 exists formula.
1810 
1811  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
1812 
1813  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1814 
1815  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1816  >>> x = Int('x')
1817  >>> y = Int('y')
1818  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
1819  >>> q
1820  Exists([x, y], f(x, y) >= x)
1821  >>> is_quantifier(q)
1822  True
1823  >>> r = Tactic('nnf')(q).as_expr()
1824  >>> is_quantifier(r)
1825  False
1826  """
1827  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
1828 
def Exists
Definition: z3py.py:1808
def z3py.Extract (   high,
  low,
  a 
)
Create a Z3 bit-vector extraction expression.

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

Definition at line 3529 of file z3py.py.

3529 def Extract(high, low, a):
3530  """Create a Z3 bit-vector extraction expression.
3531 
3532  >>> x = BitVec('x', 8)
3533  >>> Extract(6, 2, x)
3534  Extract(6, 2, x)
3535  >>> Extract(6, 2, x).sort()
3536  BitVec(5)
3537  """
3538  if __debug__:
3539  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3540  _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
3541  _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
3542  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
3543 
def Extract(high, low, a)
Definition: z3py.py:3529
Z3_ast Z3_API Z3_mk_extract(__in Z3_context c, __in unsigned high, __in unsigned low, __in Z3_ast t1)
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n...
def is_bv(a)
Definition: z3py.py:3390
def z3py.FailIf (   p,
  ctx = None 
)
Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.

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

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

Definition at line 6903 of file z3py.py.

6903 def FailIf(p, ctx=None):
6904  """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6905 
6906  In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
6907 
6908  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
6909  >>> x, y = Ints('x y')
6910  >>> g = Goal()
6911  >>> g.add(x > 0)
6912  >>> g.add(y > 0)
6913  >>> t(g)
6914  [[x > 0, y > 0]]
6915  >>> g.add(x == y + 1)
6916  >>> t(g)
6917  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6918  """
6919  p = _to_probe(p, ctx)
6920  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
6921 
Z3_tactic Z3_API Z3_tactic_fail_if(__in Z3_context c, __in Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
def FailIf
Definition: z3py.py:6903
def z3py.ForAll (   vs,
  body,
  weight = 1,
  qid = "",
  skid = "",
  patterns = [],
  no_patterns = [] 
)
Create a Z3 forall formula.

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

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

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

Definition at line 1789 of file z3py.py.

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

1789 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1790  """Create a Z3 forall formula.
1791 
1792  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
1793 
1794  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1795 
1796  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1797  >>> x = Int('x')
1798  >>> y = Int('y')
1799  >>> ForAll([x, y], f(x, y) >= x)
1800  ForAll([x, y], f(x, y) >= x)
1801  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
1802  ForAll([x, y], f(x, y) >= x)
1803  >>> ForAll([x, y], f(x, y) >= x, weight=10)
1804  ForAll([x, y], f(x, y) >= x)
1805  """
1806  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
1807 
def ForAll
Definition: z3py.py:1789
def z3py.FreshBool (   prefix = 'b',
  ctx = None 
)
Return a fresh Boolean constant in the given context using the given prefix.

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

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

Definition at line 1400 of file z3py.py.

1400 def FreshBool(prefix='b', ctx=None):
1401  """Return a fresh Boolean constant in the given context using the given prefix.
1402 
1403  If `ctx=None`, then the global context is used.
1404 
1405  >>> b1 = FreshBool()
1406  >>> b2 = FreshBool()
1407  >>> eq(b1, b2)
1408  False
1409  """
1410  ctx = _get_ctx(ctx)
1411  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1412 
def BoolSort
Definition: z3py.py:1325
Z3_ast Z3_API Z3_mk_fresh_const(__in Z3_context c, __in Z3_string prefix, __in Z3_sort ty)
Declare and create a fresh constant.
def FreshBool
Definition: z3py.py:1400
def z3py.FreshInt (   prefix = 'x',
  ctx = None 
)
Return a fresh integer constant in the given context using the given prefix.

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

Definition at line 2752 of file z3py.py.

2752 def FreshInt(prefix='x', ctx=None):
2753  """Return a fresh integer constant in the given context using the given prefix.
2754 
2755  >>> x = FreshInt()
2756  >>> y = FreshInt()
2757  >>> eq(x, y)
2758  False
2759  >>> x.sort()
2760  Int
2761  """
2762  ctx = _get_ctx(ctx)
2763  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
2764 
def IntSort
Definition: z3py.py:2614
Z3_ast Z3_API Z3_mk_fresh_const(__in Z3_context c, __in Z3_string prefix, __in Z3_sort ty)
Declare and create a fresh constant.
def FreshInt
Definition: z3py.py:2752
def z3py.FreshReal (   prefix = 'b',
  ctx = None 
)
Return a fresh real constant in the given context using the given prefix.

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

Definition at line 2804 of file z3py.py.

2804 def FreshReal(prefix='b', ctx=None):
2805  """Return a fresh real constant in the given context using the given prefix.
2806 
2807  >>> x = FreshReal()
2808  >>> y = FreshReal()
2809  >>> eq(x, y)
2810  False
2811  >>> x.sort()
2812  Real
2813  """
2814  ctx = _get_ctx(ctx)
2815  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
2816 
def RealSort
Definition: z3py.py:2630
Z3_ast Z3_API Z3_mk_fresh_const(__in Z3_context c, __in Z3_string prefix, __in Z3_sort ty)
Declare and create a fresh constant.
def FreshReal
Definition: z3py.py:2804
def z3py.Function (   name,
  sig 
)
Create a new Z3 uninterpreted function with the given sorts. 

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

Definition at line 701 of file z3py.py.

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

701 def Function(name, *sig):
702  """Create a new Z3 uninterpreted function with the given sorts.
703 
704  >>> f = Function('f', IntSort(), IntSort())
705  >>> f(f(0))
706  f(f(0))
707  """
708  sig = _get_args(sig)
709  if __debug__:
710  _z3_assert(len(sig) > 0, "At least two arguments expected")
711  arity = len(sig) - 1
712  rng = sig[arity]
713  if __debug__:
714  _z3_assert(is_sort(rng), "Z3 sort expected")
715  dom = (Sort * arity)()
716  for i in range(arity):
717  if __debug__:
718  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
719  dom[i] = sig[i].ast
720  ctx = rng.ctx
721  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
722 
Function Declarations.
Definition: z3py.py:587
def Function(name, sig)
Definition: z3py.py:701
def is_sort(s)
Definition: z3py.py:532
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
def to_symbol
Definition: z3py.py:94
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 5533 of file z3py.py.

5534  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
5535  if __debug__:
5536  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
5537  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
5538 
Function Declarations.
Definition: z3py.py:587
Z3_func_decl Z3_API Z3_get_as_array_func_decl(__in Z3_context c, __in Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
def get_as_array_func(n)
Definition: z3py.py:5533
def is_as_array(n)
Definition: z3py.py:5529
def z3py.get_map_func (   a)
Return the function declaration associated with a Z3 map array expression.

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

Definition at line 3938 of file z3py.py.

3939  """Return the function declaration associated with a Z3 map array expression.
3940 
3941  >>> f = Function('f', IntSort(), IntSort())
3942  >>> b = Array('b', IntSort(), IntSort())
3943  >>> a = Map(f, b)
3944  >>> eq(f, get_map_func(a))
3945  True
3946  >>> get_map_func(a)
3947  f
3948  >>> get_map_func(a)(0)
3949  f(0)
3950  """
3951  if __debug__:
3952  _z3_assert(is_map(a), "Z3 array map expression expected.")
3953  return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
3954 
Function Declarations.
Definition: z3py.py:587
def is_map(a)
Definition: z3py.py:3923
def get_map_func(a)
Definition: z3py.py:3938
Z3_ast Z3_API Z3_get_decl_ast_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the expresson value associated with an expression parameter.
Z3_func_decl Z3_API Z3_to_func_decl(__in Z3_context c, __in Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
def z3py.get_param (   name)
Return the value of a Z3 global (or module) parameter

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

Definition at line 247 of file z3py.py.

247 def get_param(name):
248  """Return the value of a Z3 global (or module) parameter
249 
250  >>> get_param('nlsat.reorder')
251  'true'
252  """
253  ptr = (ctypes.c_char_p * 1)()
254  if Z3_global_param_get(str(name), ptr):
255  r = z3core._to_pystr(ptr[0])
256  return r
257  raise Z3Exception("failed to retrieve value for '%s'" % name)
258 
Z3_bool Z3_API Z3_global_param_get(__in Z3_string param_id, __out Z3_string_ptr param_value)
Get a global (or module) parameter.
def get_param(name)
Definition: z3py.py:247
def z3py.get_var_index (   a)
Return the de-Bruijn index of the Z3 bounded variable `a`.

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

Definition at line 1037 of file z3py.py.

1038  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1039 
1040  >>> x = Int('x')
1041  >>> y = Int('y')
1042  >>> is_var(x)
1043  False
1044  >>> is_const(x)
1045  True
1046  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1047  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1048  >>> q = ForAll([x, y], f(x, y) == x + y)
1049  >>> q.body()
1050  f(Var(1), Var(0)) == Var(1) + Var(0)
1051  >>> b = q.body()
1052  >>> b.arg(0)
1053  f(Var(1), Var(0))
1054  >>> v1 = b.arg(0).arg(0)
1055  >>> v2 = b.arg(0).arg(1)
1056  >>> v1
1057  Var(1)
1058  >>> v2
1059  Var(0)
1060  >>> get_var_index(v1)
1061  1
1062  >>> get_var_index(v2)
1063  0
1064  """
1065  if __debug__:
1066  _z3_assert(is_var(a), "Z3 bound variable expected")
1067  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1068 
unsigned Z3_API Z3_get_index_value(__in Z3_context c, __in Z3_ast a)
Return index of de-Brujin bound variable.
def get_var_index(a)
Definition: z3py.py:1037
def is_var(a)
Definition: z3py.py:1013
def z3py.get_version ( )

Definition at line 72 of file z3py.py.

73  major = ctypes.c_uint(0)
74  minor = ctypes.c_uint(0)
75  build = ctypes.c_uint(0)
76  rev = ctypes.c_uint(0)
77  Z3_get_version(major, minor, build, rev)
78  return (major.value, minor.value, build.value, rev.value)
79 
80 # We use _z3_assert instead of the assert command because we want to
81 # produce nice error messages in Z3Py at rise4fun.com
void Z3_API Z3_get_version(__out unsigned *major, __out unsigned *minor, __out unsigned *build_number, __out unsigned *revision_number)
Return Z3 version number information.
def get_version()
Definition: z3py.py:72
def z3py.get_version_string ( )

Definition at line 64 of file z3py.py.

65  major = ctypes.c_uint(0)
66  minor = ctypes.c_uint(0)
67  build = ctypes.c_uint(0)
68  rev = ctypes.c_uint(0)
69  Z3_get_version(major, minor, build, rev)
70  return "%s.%s.%s" % (major.value, minor.value, build.value)
71 
def get_version_string()
Definition: z3py.py:64
void Z3_API Z3_get_version(__out unsigned *major, __out unsigned *minor, __out unsigned *build_number, __out unsigned *revision_number)
Return Z3 version number information.
def z3py.help_simplify ( )
Return a string describing all options available for Z3 `simplify` procedure.

Definition at line 6980 of file z3py.py.

6981  """Return a string describing all options available for Z3 `simplify` procedure."""
6982  print(Z3_simplify_get_help(main_ctx().ref()))
6983 
def main_ctx()
Definition: z3py.py:188
def help_simplify()
Definition: z3py.py:6980
Z3_string Z3_API Z3_simplify_get_help(__in Z3_context c)
Return a string describing all available parameters.
def z3py.If (   a,
  b,
  c,
  ctx = None 
)
Create a Z3 if-then-else expression. 

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

Definition at line 1081 of file z3py.py.

1081 def If(a, b, c, ctx=None):
1082  """Create a Z3 if-then-else expression.
1083 
1084  >>> x = Int('x')
1085  >>> y = Int('y')
1086  >>> max = If(x > y, x, y)
1087  >>> max
1088  If(x > y, x, y)
1089  >>> simplify(max)
1090  If(x <= y, y, x)
1091  """
1092  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1093  return Cond(a, b, c, ctx)
1094  else:
1095  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1096  s = BoolSort(ctx)
1097  a = s.cast(a)
1098  b, c = _coerce_exprs(b, c, ctx)
1099  if __debug__:
1100  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1101  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1102 
def BoolSort
Definition: z3py.py:1325
def If
Definition: z3py.py:1081
Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
def Cond
Definition: z3py.py:6940
def z3py.Implies (   a,
  b,
  ctx = None 
)
Create a Z3 implies expression. 

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

Definition at line 1413 of file z3py.py.

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

1413 def Implies(a, b, ctx=None):
1414  """Create a Z3 implies expression.
1415 
1416  >>> p, q = Bools('p q')
1417  >>> Implies(p, q)
1418  Implies(p, q)
1419  >>> simplify(Implies(p, q))
1420  Or(Not(p), q)
1421  """
1422  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1423  s = BoolSort(ctx)
1424  a = s.cast(a)
1425  b = s.cast(b)
1426  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1427 
def BoolSort
Definition: z3py.py:1325
def Implies
Definition: z3py.py:1413
Z3_ast Z3_API Z3_mk_implies(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 implies t2.
def z3py.Int (   name,
  ctx = None 
)
Return an integer constant named `name`. If `ctx=None`, then the global context is used.

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

Definition at line 2717 of file z3py.py.

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

2717 def Int(name, ctx=None):
2718  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
2719 
2720  >>> x = Int('x')
2721  >>> is_int(x)
2722  True
2723  >>> is_int(x + 1)
2724  True
2725  """
2726  ctx = _get_ctx(ctx)
2727  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
2728 
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
def IntSort
Definition: z3py.py:2614
def Int
Definition: z3py.py:2717
def to_symbol
Definition: z3py.py:94
def z3py.Interpolant (   a,
  ctx = None 
)
Create an interpolation operator.

The argument is an interpolation pattern (see tree_interpolant). 

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

Definition at line 7295 of file z3py.py.

Referenced by binary_interpolant(), and tree_interpolant().

7295 def Interpolant(a,ctx=None):
7296  """Create an interpolation operator.
7297 
7298  The argument is an interpolation pattern (see tree_interpolant).
7299 
7300  >>> x = Int('x')
7301  >>> print Interpolant(x>0)
7302  interp(x > 0)
7303  """
7304  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
7305  s = BoolSort(ctx)
7306  a = s.cast(a)
7307  return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
7308 
def BoolSort
Definition: z3py.py:1325
def Interpolant
Definition: z3py.py:7295
Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a)
Create an AST node marking a formula position for interpolation.
def z3py.Ints (   names,
  ctx = None 
)
Return a tuple of Integer constants. 

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

Definition at line 2729 of file z3py.py.

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

2729 def Ints(names, ctx=None):
2730  """Return a tuple of Integer constants.
2731 
2732  >>> x, y, z = Ints('x y z')
2733  >>> Sum(x, y, z)
2734  x + y + z
2735  """
2736  ctx = _get_ctx(ctx)
2737  if isinstance(names, str):
2738  names = names.split(" ")
2739  return [Int(name, ctx) for name in names]
2740 
def Ints
Definition: z3py.py:2729
def Int
Definition: z3py.py:2717
def z3py.IntSort (   ctx = None)
Return the interger sort in the given context. If `ctx=None`, then the global context is used.

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

Definition at line 2614 of file z3py.py.

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

2614 def IntSort(ctx=None):
2615  """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
2616 
2617  >>> IntSort()
2618  Int
2619  >>> x = Const('x', IntSort())
2620  >>> is_int(x)
2621  True
2622  >>> x.sort() == IntSort()
2623  True
2624  >>> x.sort() == BoolSort()
2625  False
2626  """
2627  ctx = _get_ctx(ctx)
2628  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
2629 
def IntSort
Definition: z3py.py:2614
Arithmetic.
Definition: z3py.py:1835
Z3_sort Z3_API Z3_mk_int_sort(__in Z3_context c)
Create the integer type.
def z3py.IntVal (   val,
  ctx = None 
)
Return a Z3 integer value. If `ctx=None`, then the global context is used.

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

Definition at line 2661 of file z3py.py.

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

2661 def IntVal(val, ctx=None):
2662  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
2663 
2664  >>> IntVal(1)
2665  1
2666  >>> IntVal("100")
2667  100
2668  """
2669  ctx = _get_ctx(ctx)
2670  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
2671 
def IntSort
Definition: z3py.py:2614
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
def IntVal
Definition: z3py.py:2661
def z3py.IntVector (   prefix,
  sz,
  ctx = None 
)
Return a list of integer constants of size `sz`.

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

Definition at line 2741 of file z3py.py.

2741 def IntVector(prefix, sz, ctx=None):
2742  """Return a list of integer constants of size `sz`.
2743 
2744  >>> X = IntVector('x', 3)
2745  >>> X
2746  [x__0, x__1, x__2]
2747  >>> Sum(X)
2748  x__0 + x__1 + x__2
2749  """
2750  return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
2751 
def Int
Definition: z3py.py:2717
def IntVector
Definition: z3py.py:2741
def z3py.is_add (   a)
Return `True` if `a` is an expression of the form b + c.

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

Definition at line 2318 of file z3py.py.

2318 def is_add(a):
2319  """Return `True` if `a` is an expression of the form b + c.
2320 
2321  >>> x, y = Ints('x y')
2322  >>> is_add(x + y)
2323  True
2324  >>> is_add(x - y)
2325  False
2326  """
2327  return is_app_of(a, Z3_OP_ADD)
2328 
def is_app_of(a, k)
Definition: z3py.py:1069
def is_add(a)
Definition: z3py.py:2318
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 2305 of file z3py.py.

2306  """Return `True` if `a` is an algerbraic value of sort Real.
2307 
2308  >>> is_algebraic_value(RealVal("3/5"))
2309  False
2310  >>> n = simplify(Sqrt(2))
2311  >>> n
2312  1.4142135623?
2313  >>> is_algebraic_value(n)
2314  True
2315  """
2316  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2317 
def is_arith(a)
Definition: z3py.py:2199
def is_algebraic_value(a)
Definition: z3py.py:2305
def z3py.is_and (   a)
Return `True` if `a` is a Z3 and expression.

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

Definition at line 1272 of file z3py.py.

1272 def is_and(a):
1273  """Return `True` if `a` is a Z3 and expression.
1274 
1275  >>> p, q = Bools('p q')
1276  >>> is_and(And(p, q))
1277  True
1278  >>> is_and(Or(p, q))
1279  False
1280  """
1281  return is_app_of(a, Z3_OP_AND)
1282 
def is_and(a)
Definition: z3py.py:1272
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_app (   a)
Return `True` if `a` is a Z3 function application. 

Note that, constants are function applications with 0 arguments. 

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

Definition at line 970 of file z3py.py.

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

970 def is_app(a):
971  """Return `True` if `a` is a Z3 function application.
972 
973  Note that, constants are function applications with 0 arguments.
974 
975  >>> a = Int('a')
976  >>> is_app(a)
977  True
978  >>> is_app(a + 1)
979  True
980  >>> is_app(IntSort())
981  False
982  >>> is_app(1)
983  False
984  >>> is_app(IntVal(1))
985  True
986  >>> x = Int('x')
987  >>> is_app(ForAll(x, x >= 0))
988  False
989  """
990  if not isinstance(a, ExprRef):
991  return False
992  k = _ast_kind(a.ctx, a)
993  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
994 
def is_app(a)
Definition: z3py.py:970
def z3py.is_app_of (   a,
  k 
)
Return `True` if `a` is an application of the given kind `k`. 

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

Definition at line 1069 of file z3py.py.

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

1069 def is_app_of(a, k):
1070  """Return `True` if `a` is an application of the given kind `k`.
1071 
1072  >>> x = Int('x')
1073  >>> n = x + 1
1074  >>> is_app_of(n, Z3_OP_ADD)
1075  True
1076  >>> is_app_of(n, Z3_OP_MUL)
1077  False
1078  """
1079  return is_app(a) and a.decl().kind() == k
1080 
def is_app(a)
Definition: z3py.py:970
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_arith (   a)
Return `True` if `a` is an arithmetical expression.

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

Definition at line 2199 of file z3py.py.

Referenced by is_algebraic_value().

2199 def is_arith(a):
2200  """Return `True` if `a` is an arithmetical expression.
2201 
2202  >>> x = Int('x')
2203  >>> is_arith(x)
2204  True
2205  >>> is_arith(x + 1)
2206  True
2207  >>> is_arith(1)
2208  False
2209  >>> is_arith(IntVal(1))
2210  True
2211  >>> y = Real('y')
2212  >>> is_arith(y)
2213  True
2214  >>> is_arith(y + 1)
2215  True
2216  """
2217  return isinstance(a, ArithRef)
2218 
def is_arith(a)
Definition: z3py.py:2199
def z3py.is_arith_sort (   s)
Return `True` if s is an arithmetical sort (type).

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

Definition at line 1902 of file z3py.py.

1903  """Return `True` if s is an arithmetical sort (type).
1904 
1905  >>> is_arith_sort(IntSort())
1906  True
1907  >>> is_arith_sort(RealSort())
1908  True
1909  >>> is_arith_sort(BoolSort())
1910  False
1911  >>> n = Int('x') + 1
1912  >>> is_arith_sort(n.sort())
1913  True
1914  """
1915  return isinstance(s, ArithSortRef)
1916 
def is_arith_sort(s)
Definition: z3py.py:1902
def z3py.is_array (   a)
Return `True` if `a` is a Z3 array expression.

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

Definition at line 3886 of file z3py.py.

3886 def is_array(a):
3887  """Return `True` if `a` is a Z3 array expression.
3888 
3889  >>> a = Array('a', IntSort(), IntSort())
3890  >>> is_array(a)
3891  True
3892  >>> is_array(Store(a, 0, 1))
3893  True
3894  >>> is_array(a[0])
3895  False
3896  """
3897  return isinstance(a, ArrayRef)
3898 
def is_array(a)
Definition: z3py.py:3886
def z3py.is_as_array (   n)
Return true if n is a Z3 expression of the form (_ as-array f).

Definition at line 5529 of file z3py.py.

Referenced by get_as_array_func().

5530  """Return true if n is a Z3 expression of the form (_ as-array f)."""
5531  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
5532 
Z3_bool Z3_API Z3_is_as_array(__in Z3_context c, __in Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3...
def is_as_array(n)
Definition: z3py.py:5529
def z3py.is_ast (   a)
Return `True` if `a` is an AST node.

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

Definition at line 352 of file z3py.py.

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

352 def is_ast(a):
353  """Return `True` if `a` is an AST node.
354 
355  >>> is_ast(10)
356  False
357  >>> is_ast(IntVal(10))
358  True
359  >>> is_ast(Int('x'))
360  True
361  >>> is_ast(BoolSort())
362  True
363  >>> is_ast(Function('f', IntSort(), IntSort()))
364  True
365  >>> is_ast("x")
366  False
367  >>> is_ast(Solver())
368  False
369  """
370  return isinstance(a, AstRef)
371 
def is_ast(a)
Definition: z3py.py:352
def z3py.is_bool (   a)
Return `True` if `a` is a Z3 Boolean expression.

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

Definition at line 1225 of file z3py.py.

Referenced by BoolSort(), and prove().

1225 def is_bool(a):
1226  """Return `True` if `a` is a Z3 Boolean expression.
1227 
1228  >>> p = Bool('p')
1229  >>> is_bool(p)
1230  True
1231  >>> q = Bool('q')
1232  >>> is_bool(And(p, q))
1233  True
1234  >>> x = Real('x')
1235  >>> is_bool(x)
1236  False
1237  >>> is_bool(x == 0)
1238  True
1239  """
1240  return isinstance(a, BoolRef)
1241 
def is_bool(a)
Definition: z3py.py:1225
def z3py.is_bv (   a)
Return `True` if `a` is a Z3 bit-vector expression.

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

Definition at line 3390 of file z3py.py.

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

3390 def is_bv(a):
3391  """Return `True` if `a` is a Z3 bit-vector expression.
3392 
3393  >>> b = BitVec('b', 32)
3394  >>> is_bv(b)
3395  True
3396  >>> is_bv(b + 10)
3397  True
3398  >>> is_bv(Int('x'))
3399  False
3400  """
3401  return isinstance(a, BitVecRef)
3402 
def is_bv(a)
Definition: z3py.py:3390
def z3py.is_bv_sort (   s)
Return True if `s` is a Z3 bit-vector sort.

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

Definition at line 2929 of file z3py.py.

Referenced by BitVecVal().

2929 def is_bv_sort(s):
2930  """Return True if `s` is a Z3 bit-vector sort.
2931 
2932  >>> is_bv_sort(BitVecSort(32))
2933  True
2934  >>> is_bv_sort(IntSort())
2935  False
2936  """
2937  return isinstance(s, BitVecSortRef)
2938 
def is_bv_sort(s)
Definition: z3py.py:2929
def z3py.is_bv_value (   a)
Return `True` if `a` is a Z3 bit-vector numeral value.

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

Definition at line 3403 of file z3py.py.

3404  """Return `True` if `a` is a Z3 bit-vector numeral value.
3405 
3406  >>> b = BitVec('b', 32)
3407  >>> is_bv_value(b)
3408  False
3409  >>> b = BitVecVal(10, 32)
3410  >>> b
3411  10
3412  >>> is_bv_value(b)
3413  True
3414  """
3415  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3416 
def is_bv_value(a)
Definition: z3py.py:3403
def is_bv(a)
Definition: z3py.py:3390
def z3py.is_const (   a)
Return `True` if `a` is Z3 constant/variable expression. 

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

Definition at line 995 of file z3py.py.

Referenced by prove().

995 def is_const(a):
996  """Return `True` if `a` is Z3 constant/variable expression.
997 
998  >>> a = Int('a')
999  >>> is_const(a)
1000  True
1001  >>> is_const(a + 1)
1002  False
1003  >>> is_const(1)
1004  False
1005  >>> is_const(IntVal(1))
1006  True
1007  >>> x = Int('x')
1008  >>> is_const(ForAll(x, x >= 0))
1009  False
1010  """
1011  return is_app(a) and a.num_args() == 0
1012 
def is_app(a)
Definition: z3py.py:970
def is_const(a)
Definition: z3py.py:995
def z3py.is_const_array (   a)
Return `True` if `a` is a Z3 constant array.

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

Definition at line 3899 of file z3py.py.

3900  """Return `True` if `a` is a Z3 constant array.
3901 
3902  >>> a = K(IntSort(), 10)
3903  >>> is_const_array(a)
3904  True
3905  >>> a = Array('a', IntSort(), IntSort())
3906  >>> is_const_array(a)
3907  False
3908  """
3909  return is_app_of(a, Z3_OP_CONST_ARRAY)
3910 
def is_const_array(a)
Definition: z3py.py:3899
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_distinct (   a)
Return `True` if `a` is a Z3 distinct expression.

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

Definition at line 1314 of file z3py.py.

1315  """Return `True` if `a` is a Z3 distinct expression.
1316 
1317  >>> x, y, z = Ints('x y z')
1318  >>> is_distinct(x == y)
1319  False
1320  >>> is_distinct(Distinct(x, y, z))
1321  True
1322  """
1323  return is_app_of(a, Z3_OP_DISTINCT)
1324 
def is_distinct(a)
Definition: z3py.py:1314
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_div (   a)
Return `True` if `a` is an expression of the form b / c.

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

Definition at line 2351 of file z3py.py.

2351 def is_div(a):
2352  """Return `True` if `a` is an expression of the form b / c.
2353 
2354  >>> x, y = Reals('x y')
2355  >>> is_div(x / y)
2356  True
2357  >>> is_div(x + y)
2358  False
2359  >>> x, y = Ints('x y')
2360  >>> is_div(x / y)
2361  False
2362  >>> is_idiv(x / y)
2363  True
2364  """
2365  return is_app_of(a, Z3_OP_DIV)
2366 
def is_div(a)
Definition: z3py.py:2351
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_eq (   a)
Return `True` if `a` is a Z3 equality expression.

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

Definition at line 1305 of file z3py.py.

1305 def is_eq(a):
1306  """Return `True` if `a` is a Z3 equality expression.
1307 
1308  >>> x, y = Ints('x y')
1309  >>> is_eq(x == y)
1310  True
1311  """
1312  return is_app_of(a, Z3_OP_EQ)
1313 
def is_eq(a)
Definition: z3py.py:1305
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_expr (   a)
Return `True` if `a` is a Z3 expression.

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

Definition at line 950 of file z3py.py.

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

950 def is_expr(a):
951  """Return `True` if `a` is a Z3 expression.
952 
953  >>> a = Int('a')
954  >>> is_expr(a)
955  True
956  >>> is_expr(a + 1)
957  True
958  >>> is_expr(IntSort())
959  False
960  >>> is_expr(1)
961  False
962  >>> is_expr(IntVal(1))
963  True
964  >>> x = Int('x')
965  >>> is_expr(ForAll(x, x >= 0))
966  True
967  """
968  return isinstance(a, ExprRef)
969 
def is_expr(a)
Definition: z3py.py:950
def z3py.is_false (   a)
Return `True` if `a` is the Z3 false expression.

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

Definition at line 1259 of file z3py.py.

Referenced by BoolVal().

1259 def is_false(a):
1260  """Return `True` if `a` is the Z3 false expression.
1261 
1262  >>> p = Bool('p')
1263  >>> is_false(p)
1264  False
1265  >>> is_false(False)
1266  False
1267  >>> is_false(BoolVal(False))
1268  True
1269  """
1270  return is_app_of(a, Z3_OP_FALSE)
1271 
def is_app_of(a, k)
Definition: z3py.py:1069
def is_false(a)
Definition: z3py.py:1259
def z3py.is_func_decl (   a)
Return `True` if `a` is a Z3 function declaration.

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

Definition at line 689 of file z3py.py.

Referenced by prove().

690  """Return `True` if `a` is a Z3 function declaration.
691 
692  >>> f = Function('f', IntSort(), IntSort())
693  >>> is_func_decl(f)
694  True
695  >>> x = Real('x')
696  >>> is_func_decl(x)
697  False
698  """
699  return isinstance(a, FuncDeclRef)
700 
def is_func_decl(a)
Definition: z3py.py:689
def z3py.is_ge (   a)
Return `True` if `a` is an expression of the form b >= c.

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

Definition at line 2411 of file z3py.py.

2411 def is_ge(a):
2412  """Return `True` if `a` is an expression of the form b >= c.
2413 
2414  >>> x, y = Ints('x y')
2415  >>> is_ge(x >= y)
2416  True
2417  >>> is_ge(x == y)
2418  False
2419  """
2420  return is_app_of(a, Z3_OP_GE)
2421 
def is_ge(a)
Definition: z3py.py:2411
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_gt (   a)
Return `True` if `a` is an expression of the form b > c.

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

Definition at line 2422 of file z3py.py.

2422 def is_gt(a):
2423  """Return `True` if `a` is an expression of the form b > c.
2424 
2425  >>> x, y = Ints('x y')
2426  >>> is_gt(x > y)
2427  True
2428  >>> is_gt(x == y)
2429  False
2430  """
2431  return is_app_of(a, Z3_OP_GT)
2432 
def is_gt(a)
Definition: z3py.py:2422
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_idiv (   a)
Return `True` if `a` is an expression of the form b div c.

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

Definition at line 2367 of file z3py.py.

Referenced by is_div().

2367 def is_idiv(a):
2368  """Return `True` if `a` is an expression of the form b div c.
2369 
2370  >>> x, y = Ints('x y')
2371  >>> is_idiv(x / y)
2372  True
2373  >>> is_idiv(x + y)
2374  False
2375  """
2376  return is_app_of(a, Z3_OP_IDIV)
2377 
def is_idiv(a)
Definition: z3py.py:2367
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_int (   a)
Return `True` if `a` is an integer expression.

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

Definition at line 2219 of file z3py.py.

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

2219 def is_int(a):
2220  """Return `True` if `a` is an integer expression.
2221 
2222  >>> x = Int('x')
2223  >>> is_int(x + 1)
2224  True
2225  >>> is_int(1)
2226  False
2227  >>> is_int(IntVal(1))
2228  True
2229  >>> y = Real('y')
2230  >>> is_int(y)
2231  False
2232  >>> is_int(y + 1)
2233  False
2234  """
2235  return is_arith(a) and a.is_int()
2236 
def is_arith(a)
Definition: z3py.py:2199
def is_int(a)
Definition: z3py.py:2219
def z3py.is_int_value (   a)
Return `True` if `a` is an integer value of sort Int.

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

Definition at line 2261 of file z3py.py.

2262  """Return `True` if `a` is an integer value of sort Int.
2263 
2264  >>> is_int_value(IntVal(1))
2265  True
2266  >>> is_int_value(1)
2267  False
2268  >>> is_int_value(Int('x'))
2269  False
2270  >>> n = Int('x') + 1
2271  >>> n
2272  x + 1
2273  >>> n.arg(1)
2274  1
2275  >>> is_int_value(n.arg(1))
2276  True
2277  >>> is_int_value(RealVal("1/3"))
2278  False
2279  >>> is_int_value(RealVal(1))
2280  False
2281  """
2282  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2283 
def is_int_value(a)
Definition: z3py.py:2261
def is_arith(a)
Definition: z3py.py:2199
def z3py.is_is_int (   a)
Return `True` if `a` is an expression of the form IsInt(b).

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

Definition at line 2433 of file z3py.py.

2433 def is_is_int(a):
2434  """Return `True` if `a` is an expression of the form IsInt(b).
2435 
2436  >>> x = Real('x')
2437  >>> is_is_int(IsInt(x))
2438  True
2439  >>> is_is_int(x)
2440  False
2441  """
2442  return is_app_of(a, Z3_OP_IS_INT)
2443 
def is_app_of(a, k)
Definition: z3py.py:1069
def is_is_int(a)
Definition: z3py.py:2433
def z3py.is_K (   a)
Return `True` if `a` is a Z3 constant array.

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

Definition at line 3911 of file z3py.py.

3911 def is_K(a):
3912  """Return `True` if `a` is a Z3 constant array.
3913 
3914  >>> a = K(IntSort(), 10)
3915  >>> is_K(a)
3916  True
3917  >>> a = Array('a', IntSort(), IntSort())
3918  >>> is_K(a)
3919  False
3920  """
3921  return is_app_of(a, Z3_OP_CONST_ARRAY)
3922 
def is_K(a)
Definition: z3py.py:3911
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_le (   a)
Return `True` if `a` is an expression of the form b <= c.

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

Definition at line 2389 of file z3py.py.

2389 def is_le(a):
2390  """Return `True` if `a` is an expression of the form b <= c.
2391 
2392  >>> x, y = Ints('x y')
2393  >>> is_le(x <= y)
2394  True
2395  >>> is_le(x < y)
2396  False
2397  """
2398  return is_app_of(a, Z3_OP_LE)
2399 
def is_le(a)
Definition: z3py.py:2389
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_lt (   a)
Return `True` if `a` is an expression of the form b < c.

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

Definition at line 2400 of file z3py.py.

2400 def is_lt(a):
2401  """Return `True` if `a` is an expression of the form b < c.
2402 
2403  >>> x, y = Ints('x y')
2404  >>> is_lt(x < y)
2405  True
2406  >>> is_lt(x == y)
2407  False
2408  """
2409  return is_app_of(a, Z3_OP_LT)
2410 
def is_lt(a)
Definition: z3py.py:2400
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_map (   a)
Return `True` if `a` is a Z3 map array expression. 

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

Definition at line 3923 of file z3py.py.

Referenced by get_map_func().

3923 def is_map(a):
3924  """Return `True` if `a` is a Z3 map array expression.
3925 
3926  >>> f = Function('f', IntSort(), IntSort())
3927  >>> b = Array('b', IntSort(), IntSort())
3928  >>> a = Map(f, b)
3929  >>> a
3930  Map(f, b)
3931  >>> is_map(a)
3932  True
3933  >>> is_map(b)
3934  False
3935  """
3936  return is_app_of(a, Z3_OP_ARRAY_MAP)
3937 
def is_map(a)
Definition: z3py.py:3923
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_mod (   a)
Return `True` if `a` is an expression of the form b % c.

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

Definition at line 2378 of file z3py.py.

2378 def is_mod(a):
2379  """Return `True` if `a` is an expression of the form b % c.
2380 
2381  >>> x, y = Ints('x y')
2382  >>> is_mod(x % y)
2383  True
2384  >>> is_mod(x + y)
2385  False
2386  """
2387  return is_app_of(a, Z3_OP_MOD)
2388 
def is_mod(a)
Definition: z3py.py:2378
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_mul (   a)
Return `True` if `a` is an expression of the form b * c.

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

Definition at line 2329 of file z3py.py.

2329 def is_mul(a):
2330  """Return `True` if `a` is an expression of the form b * c.
2331 
2332  >>> x, y = Ints('x y')
2333  >>> is_mul(x * y)
2334  True
2335  >>> is_mul(x - y)
2336  False
2337  """
2338  return is_app_of(a, Z3_OP_MUL)
2339 
def is_app_of(a, k)
Definition: z3py.py:1069
def is_mul(a)
Definition: z3py.py:2329
def z3py.is_not (   a)
Return `True` if `a` is a Z3 not expression.

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

Definition at line 1294 of file z3py.py.

1294 def is_not(a):
1295  """Return `True` if `a` is a Z3 not expression.
1296 
1297  >>> p = Bool('p')
1298  >>> is_not(p)
1299  False
1300  >>> is_not(Not(p))
1301  True
1302  """
1303  return is_app_of(a, Z3_OP_NOT)
1304 
def is_not(a)
Definition: z3py.py:1294
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_or (   a)
Return `True` if `a` is a Z3 or expression.

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

Definition at line 1283 of file z3py.py.

1283 def is_or(a):
1284  """Return `True` if `a` is a Z3 or expression.
1285 
1286  >>> p, q = Bools('p q')
1287  >>> is_or(Or(p, q))
1288  True
1289  >>> is_or(And(p, q))
1290  False
1291  """
1292  return is_app_of(a, Z3_OP_OR)
1293 
def is_or(a)
Definition: z3py.py:1283
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_pattern (   a)
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.

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

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

Definition at line 1545 of file z3py.py.

Referenced by MultiPattern().

1545 def is_pattern(a):
1546  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1547 
1548  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1549 
1550  >>> f = Function('f', IntSort(), IntSort())
1551  >>> x = Int('x')
1552  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1553  >>> q
1554  ForAll(x, f(x) == 0)
1555  >>> q.num_patterns()
1556  1
1557  >>> is_pattern(q.pattern(0))
1558  True
1559  >>> q.pattern(0)
1560  f(Var(0))
1561  """
1562  return isinstance(a, PatternRef)
1563 
def is_pattern(a)
Definition: z3py.py:1545
def z3py.is_probe (   p)
Return `True` if `p` is a Z3 probe.

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

Definition at line 6836 of file z3py.py.

Referenced by eq().

6836 def is_probe(p):
6837  """Return `True` if `p` is a Z3 probe.
6838 
6839  >>> is_probe(Int('x'))
6840  False
6841  >>> is_probe(Probe('memory'))
6842  True
6843  """
6844  return isinstance(p, Probe)
6845 
def is_probe(p)
Definition: z3py.py:6836
def z3py.is_quantifier (   a)
Return `True` if `a` is a Z3 quantifier.

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

Definition at line 1748 of file z3py.py.

Referenced by Exists().

1749  """Return `True` if `a` is a Z3 quantifier.
1750 
1751  >>> f = Function('f', IntSort(), IntSort())
1752  >>> x = Int('x')
1753  >>> q = ForAll(x, f(x) == 0)
1754  >>> is_quantifier(q)
1755  True
1756  >>> is_quantifier(f(x))
1757  False
1758  """
1759  return isinstance(a, QuantifierRef)
1760 
def is_quantifier(a)
Definition: z3py.py:1748
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 2284 of file z3py.py.

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

2285  """Return `True` if `a` is rational value of sort Real.
2286 
2287  >>> is_rational_value(RealVal(1))
2288  True
2289  >>> is_rational_value(RealVal("3/5"))
2290  True
2291  >>> is_rational_value(IntVal(1))
2292  False
2293  >>> is_rational_value(1)
2294  False
2295  >>> n = Real('x') + 1
2296  >>> n.arg(1)
2297  1
2298  >>> is_rational_value(n.arg(1))
2299  True
2300  >>> is_rational_value(Real('x'))
2301  False
2302  """
2303  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2304 
def is_arith(a)
Definition: z3py.py:2199
def is_rational_value(a)
Definition: z3py.py:2284
def z3py.is_real (   a)
Return `True` if `a` is a real expression.

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

Definition at line 2237 of file z3py.py.

Referenced by Real(), and RealSort().

2237 def is_real(a):
2238  """Return `True` if `a` is a real expression.
2239 
2240  >>> x = Int('x')
2241  >>> is_real(x + 1)
2242  False
2243  >>> y = Real('y')
2244  >>> is_real(y)
2245  True
2246  >>> is_real(y + 1)
2247  True
2248  >>> is_real(1)
2249  False
2250  >>> is_real(RealVal(1))
2251  True
2252  """
2253  return is_arith(a) and a.is_real()
2254 
def is_real(a)
Definition: z3py.py:2237
def is_arith(a)
Definition: z3py.py:2199
def z3py.is_select (   a)
Return `True` if `a` is a Z3 array select application.

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

Definition at line 4083 of file z3py.py.

4083 def is_select(a):
4084  """Return `True` if `a` is a Z3 array select application.
4085 
4086  >>> a = Array('a', IntSort(), IntSort())
4087  >>> is_select(a)
4088  False
4089  >>> i = Int('i')
4090  >>> is_select(a[i])
4091  True
4092  """
4093  return is_app_of(a, Z3_OP_SELECT)
4094 
def is_select(a)
Definition: z3py.py:4083
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_sort (   s)
Return `True` if `s` is a Z3 sort.

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

Definition at line 532 of file z3py.py.

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

532 def is_sort(s):
533  """Return `True` if `s` is a Z3 sort.
534 
535  >>> is_sort(IntSort())
536  True
537  >>> is_sort(Int('x'))
538  False
539  >>> is_expr(Int('x'))
540  True
541  """
542  return isinstance(s, SortRef)
543 
def is_sort(s)
Definition: z3py.py:532
def z3py.is_store (   a)
Return `True` if `a` is a Z3 array store application.

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

Definition at line 4095 of file z3py.py.

4095 def is_store(a):
4096  """Return `True` if `a` is a Z3 array store application.
4097 
4098  >>> a = Array('a', IntSort(), IntSort())
4099  >>> is_store(a)
4100  False
4101  >>> is_store(Store(a, 0, 1))
4102  True
4103  """
4104  return is_app_of(a, Z3_OP_STORE)
4105 
def is_store(a)
Definition: z3py.py:4095
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_sub (   a)
Return `True` if `a` is an expression of the form b - c.

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

Definition at line 2340 of file z3py.py.

2340 def is_sub(a):
2341  """Return `True` if `a` is an expression of the form b - c.
2342 
2343  >>> x, y = Ints('x y')
2344  >>> is_sub(x - y)
2345  True
2346  >>> is_sub(x + y)
2347  False
2348  """
2349  return is_app_of(a, Z3_OP_SUB)
2350 
def is_app_of(a, k)
Definition: z3py.py:1069
def is_sub(a)
Definition: z3py.py:2340
def z3py.is_to_int (   a)
Return `True` if `a` is an expression of the form ToInt(b).

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

Definition at line 2458 of file z3py.py.

2458 def is_to_int(a):
2459  """Return `True` if `a` is an expression of the form ToInt(b).
2460 
2461  >>> x = Real('x')
2462  >>> n = ToInt(x)
2463  >>> n
2464  ToInt(x)
2465  >>> is_to_int(n)
2466  True
2467  >>> is_to_int(x)
2468  False
2469  """
2470  return is_app_of(a, Z3_OP_TO_INT)
2471 
def is_app_of(a, k)
Definition: z3py.py:1069
def is_to_int(a)
Definition: z3py.py:2458
def z3py.is_to_real (   a)
Return `True` if `a` is an expression of the form ToReal(b).

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

Definition at line 2444 of file z3py.py.

2444 def is_to_real(a):
2445  """Return `True` if `a` is an expression of the form ToReal(b).
2446 
2447  >>> x = Int('x')
2448  >>> n = ToReal(x)
2449  >>> n
2450  ToReal(x)
2451  >>> is_to_real(n)
2452  True
2453  >>> is_to_real(x)
2454  False
2455  """
2456  return is_app_of(a, Z3_OP_TO_REAL)
2457 
def is_to_real(a)
Definition: z3py.py:2444
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_true (   a)
Return `True` if `a` is the Z3 true expression.

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

Definition at line 1242 of file z3py.py.

Referenced by BoolVal().

1242 def is_true(a):
1243  """Return `True` if `a` is the Z3 true expression.
1244 
1245  >>> p = Bool('p')
1246  >>> is_true(p)
1247  False
1248  >>> is_true(simplify(p == p))
1249  True
1250  >>> x = Real('x')
1251  >>> is_true(x == 0)
1252  False
1253  >>> # True is a Python Boolean expression
1254  >>> is_true(True)
1255  False
1256  """
1257  return is_app_of(a, Z3_OP_TRUE)
1258 
def is_true(a)
Definition: z3py.py:1242
def is_app_of(a, k)
Definition: z3py.py:1069
def z3py.is_var (   a)
Return `True` if `a` is variable. 

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

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

Definition at line 1013 of file z3py.py.

Referenced by get_var_index().

1013 def is_var(a):
1014  """Return `True` if `a` is variable.
1015 
1016  Z3 uses de-Bruijn indices for representing bound variables in
1017  quantifiers.
1018 
1019  >>> x = Int('x')
1020  >>> is_var(x)
1021  False
1022  >>> is_const(x)
1023  True
1024  >>> f = Function('f', IntSort(), IntSort())
1025  >>> # Z3 replaces x with bound variables when ForAll is executed.
1026  >>> q = ForAll(x, f(x) == x)
1027  >>> b = q.body()
1028  >>> b
1029  f(Var(0)) == Var(0)
1030  >>> b.arg(1)
1031  Var(0)
1032  >>> is_var(b.arg(1))
1033  True
1034  """
1035  return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
1036 
def is_expr(a)
Definition: z3py.py:950
def is_var(a)
Definition: z3py.py:1013
def z3py.IsInt (   a)
Return the Z3 predicate IsInt(a). 

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

Definition at line 2851 of file z3py.py.

Referenced by is_is_int().

2851 def IsInt(a):
2852  """ Return the Z3 predicate IsInt(a).
2853 
2854  >>> x = Real('x')
2855  >>> IsInt(x + "1/2")
2856  IsInt(x + 1/2)
2857  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
2858  [x = 1/2]
2859  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
2860  no solution
2861  """
2862  if __debug__:
2863  _z3_assert(a.is_real(), "Z3 real expression expected.")
2864  ctx = a.ctx
2865  return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
2866 
def IsInt(a)
Definition: z3py.py:2851
Z3_ast Z3_API Z3_mk_is_int(__in Z3_context c, __in Z3_ast t1)
Check if a real number is an integer.
def z3py.K (   dom,
  v 
)
Return a Z3 constant array expression. 

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

Definition at line 4062 of file z3py.py.

Referenced by is_const_array(), and is_K().

4062 def K(dom, v):
4063  """Return a Z3 constant array expression.
4064 
4065  >>> a = K(IntSort(), 10)
4066  >>> a
4067  K(Int, 10)
4068  >>> a.sort()
4069  Array(Int, Int)
4070  >>> i = Int('i')
4071  >>> a[i]
4072  K(Int, 10)[i]
4073  >>> simplify(a[i])
4074  10
4075  """
4076  if __debug__:
4077  _z3_assert(is_sort(dom), "Z3 sort expected")
4078  ctx = dom.ctx
4079  if not is_expr(v):
4080  v = _py2expr(v, ctx)
4081  return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
4082 
def is_sort(s)
Definition: z3py.py:532
def K(dom, v)
Definition: z3py.py:4062
def is_expr(a)
Definition: z3py.py:950
Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v)
Create the constant array.
def z3py.LShR (   a,
  b 
)
Create the Z3 expression logical right shift.

Use the operator >> for the arithmetical right shift.

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

Definition at line 3676 of file z3py.py.

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

3676 def LShR(a, b):
3677  """Create the Z3 expression logical right shift.
3678 
3679  Use the operator >> for the arithmetical right shift.
3680 
3681  >>> x, y = BitVecs('x y', 32)
3682  >>> LShR(x, y)
3683  LShR(x, y)
3684  >>> (x >> y).sexpr()
3685  '(bvashr x y)'
3686  >>> LShR(x, y).sexpr()
3687  '(bvlshr x y)'
3688  >>> BitVecVal(4, 3)
3689  4
3690  >>> BitVecVal(4, 3).as_signed_long()
3691  -4
3692  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3693  -2
3694  >>> simplify(BitVecVal(4, 3) >> 1)
3695  6
3696  >>> simplify(LShR(BitVecVal(4, 3), 1))
3697  2
3698  >>> simplify(BitVecVal(2, 3) >> 1)
3699  1
3700  >>> simplify(LShR(BitVecVal(2, 3), 1))
3701  1
3702  """
3703  _check_bv_args(a, b)
3704  a, b = _coerce_exprs(a, b)
3705  return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3706 
def LShR(a, b)
Definition: z3py.py:3676
Z3_ast Z3_API Z3_mk_bvlshr(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Logical shift right.
def z3py.main_ctx ( )
Return a reference to the global Z3 context. 

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

Definition at line 188 of file z3py.py.

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

188 def main_ctx():
189  """Return a reference to the global Z3 context.
190 
191  >>> x = Real('x')
192  >>> x.ctx == main_ctx()
193  True
194  >>> c = Context()
195  >>> c == main_ctx()
196  False
197  >>> x2 = Real('x', c)
198  >>> x2.ctx == c
199  True
200  >>> eq(x, x2)
201  False
202  """
203  global _main_ctx
204  if _main_ctx == None:
205  _main_ctx = Context()
206  return _main_ctx
207 
def main_ctx()
Definition: z3py.py:188
def z3py.Map (   f,
  args 
)
Return a Z3 map array expression. 

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

Definition at line 4040 of file z3py.py.

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

4040 def Map(f, *args):
4041  """Return a Z3 map array expression.
4042 
4043  >>> f = Function('f', IntSort(), IntSort(), IntSort())
4044  >>> a1 = Array('a1', IntSort(), IntSort())
4045  >>> a2 = Array('a2', IntSort(), IntSort())
4046  >>> b = Map(f, a1, a2)
4047  >>> b
4048  Map(f, a1, a2)
4049  >>> prove(b[0] == f(a1[0], a2[0]))
4050  proved
4051  """
4052  args = _get_args(args)
4053  if __debug__:
4054  _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
4055  _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
4056  _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
4057  _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
4058  _args, sz = _to_ast_array(args)
4059  ctx = f.ctx
4060  return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
4061 
def is_array(a)
Definition: z3py.py:3886
Z3_ast Z3_API Z3_mk_map(__in Z3_context c, __in Z3_func_decl f, unsigned n, __in Z3_ast const *args)
map f on the the argument arrays.
def Map(f, args)
Definition: z3py.py:4040
def is_func_decl(a)
Definition: z3py.py:689
def z3py.MultiPattern (   args)
Create a Z3 multi-pattern using the given expressions `*args`

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

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

Definition at line 1564 of file z3py.py.

1564 def MultiPattern(*args):
1565  """Create a Z3 multi-pattern using the given expressions `*args`
1566 
1567  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1568 
1569  >>> f = Function('f', IntSort(), IntSort())
1570  >>> g = Function('g', IntSort(), IntSort())
1571  >>> x = Int('x')
1572  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1573  >>> q
1574  ForAll(x, f(x) != g(x))
1575  >>> q.num_patterns()
1576  1
1577  >>> is_pattern(q.pattern(0))
1578  True
1579  >>> q.pattern(0)
1580  MultiPattern(f(Var(0)), g(Var(0)))
1581  """
1582  if __debug__:
1583  _z3_assert(len(args) > 0, "At least one argument expected")
1584  _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
1585  ctx = args[0].ctx
1586  args, sz = _to_ast_array(args)
1587  return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
1588 
Z3_pattern Z3_API Z3_mk_pattern(__in Z3_context c, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_ast const terms[])
Create a pattern for quantifier instantiation.
Patterns.
Definition: z3py.py:1534
def MultiPattern(args)
Definition: z3py.py:1564
def is_expr(a)
Definition: z3py.py:950
def z3py.Not (   a,
  ctx = None 
)
Create a Z3 not expression or probe. 

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

Definition at line 1443 of file z3py.py.

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

1443 def Not(a, ctx=None):
1444  """Create a Z3 not expression or probe.
1445 
1446  >>> p = Bool('p')
1447  >>> Not(Not(p))
1448  Not(Not(p))
1449  >>> simplify(Not(Not(p)))
1450  p
1451  """
1452  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1453  if is_probe(a):
1454  # Not is also used to build probes
1455  return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1456  else:
1457  s = BoolSort(ctx)
1458  a = s.cast(a)
1459  return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
1460 
def Not
Definition: z3py.py:1443
def BoolSort
Definition: z3py.py:1325
Z3_probe Z3_API Z3_probe_not(__in Z3_context x, __in Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a)
Create an AST node representing not(a).
def is_probe(p)
Definition: z3py.py:6836
def z3py.open_log (   fname)
Log interaction to a file. This function must be invoked immediately after init(). 

Definition at line 86 of file z3py.py.

86 def open_log(fname):
87  """Log interaction to a file. This function must be invoked immediately after init(). """
88  Z3_open_log(fname)
89 
Z3_bool Z3_API Z3_open_log(__in Z3_string filename)
Log interaction to a file.
def open_log(fname)
Definition: z3py.py:86
def z3py.Or (   args)
Create a Z3 or-expression or or-probe. 

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

Definition at line 1498 of file z3py.py.

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

1498 def Or(*args):
1499  """Create a Z3 or-expression or or-probe.
1500 
1501  >>> p, q, r = Bools('p q r')
1502  >>> Or(p, q, r)
1503  Or(p, q, r)
1504  >>> P = BoolVector('p', 5)
1505  >>> Or(P)
1506  Or(p__0, p__1, p__2, p__3, p__4)
1507  """
1508  last_arg = None
1509  if len(args) > 0:
1510  last_arg = args[len(args)-1]
1511  if isinstance(last_arg, Context):
1512  ctx = args[len(args)-1]
1513  args = args[:len(args)-1]
1514  else:
1515  ctx = main_ctx()
1516  args = _get_args(args)
1517  ctx_args = _ctx_from_ast_arg_list(args, ctx)
1518  if __debug__:
1519  _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
1520  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1521  if _has_probe(args):
1522  return _probe_or(args, ctx)
1523  else:
1524  args = _coerce_expr_list(args, ctx)
1525  _args, sz = _to_ast_array(args)
1526  return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
1527 
def main_ctx()
Definition: z3py.py:188
def Or(args)
Definition: z3py.py:1498
Z3_ast Z3_API Z3_mk_or(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].The array args must have num_args ...
def z3py.OrElse (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).

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

Definition at line 6568 of file z3py.py.

6568 def OrElse(*ts, **ks):
6569  """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
6570 
6571  >>> x = Int('x')
6572  >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
6573  >>> # Tactic split-clause fails if there is no clause in the given goal.
6574  >>> t(x == 0)
6575  [[x == 0]]
6576  >>> t(Or(x == 0, x == 1))
6577  [[x == 0], [x == 1]]
6578  """
6579  if __debug__:
6580  _z3_assert(len(ts) >= 2, "At least two arguments expected")
6581  ctx = ks.get('ctx', None)
6582  num = len(ts)
6583  r = ts[0]
6584  for i in range(num - 1):
6585  r = _or_else(r, ts[i+1], ctx)
6586  return r
6587 
def OrElse(ts, ks)
Definition: z3py.py:6568
def z3py.ParAndThen (   t1,
  t2,
  ctx = None 
)
Alias for ParThen(t1, t2, ctx).

Definition at line 6620 of file z3py.py.

6620 def ParAndThen(t1, t2, ctx=None):
6621  """Alias for ParThen(t1, t2, ctx)."""
6622  return ParThen(t1, t2, ctx)
6623 
def ParThen
Definition: z3py.py:6606
def ParAndThen
Definition: z3py.py:6620
def z3py.ParOr (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).

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

Definition at line 6588 of file z3py.py.

6588 def ParOr(*ts, **ks):
6589  """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
6590 
6591  >>> x = Int('x')
6592  >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
6593  >>> t(x + 1 == 2)
6594  [[x == 1]]
6595  """
6596  if __debug__:
6597  _z3_assert(len(ts) >= 2, "At least two arguments expected")
6598  ctx = _get_ctx(ks.get('ctx', None))
6599  ts = [ _to_tactic(t, ctx) for t in ts ]
6600  sz = len(ts)
6601  _args = (TacticObj * sz)()
6602  for i in range(sz):
6603  _args[i] = ts[i].tactic
6604  return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
6605 
def ParOr(ts, ks)
Definition: z3py.py:6588
Z3_tactic Z3_API Z3_tactic_par_or(__in Z3_context c, __in unsigned num, __in_ecount(num) Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
def z3py.parse_smt2_file (   f,
  sorts = {},
  decls = {},
  ctx = None 
)
Parse a file in SMT 2.0 format using the given sorts and decls.

This function is similar to parse_smt2_string().

Definition at line 7285 of file z3py.py.

7285 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
7286  """Parse a file in SMT 2.0 format using the given sorts and decls.
7287 
7288  This function is similar to parse_smt2_string().
7289  """
7290  ctx = _get_ctx(ctx)
7291  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7292  dsz, dnames, ddecls = _dict2darray(decls, ctx)
7293  return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
7294 
Z3_ast Z3_API Z3_parse_smtlib2_file(__in Z3_context c, __in Z3_string file_name, __in unsigned num_sorts, __in_ecount(num_sorts) Z3_symbol const sort_names[], __in_ecount(num_sorts) Z3_sort const sorts[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol const decl_names[], __in_ecount(num_decls) Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
def parse_smt2_file
Definition: z3py.py:7285
def z3py.parse_smt2_string (   s,
  sorts = {},
  decls = {},
  ctx = None 
)
Parse a string in SMT 2.0 format using the given sorts and decls.

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

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

Definition at line 7265 of file z3py.py.

Referenced by parse_smt2_file().

7265 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
7266  """Parse a string in SMT 2.0 format using the given sorts and decls.
7267 
7268  The arguments sorts and decls are Python dictionaries used to initialize
7269  the symbol table used for the SMT 2.0 parser.
7270 
7271  >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
7272  And(x > 0, x < 10)
7273  >>> x, y = Ints('x y')
7274  >>> f = Function('f', IntSort(), IntSort())
7275  >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
7276  x + f(y) > 0
7277  >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
7278  a > 0
7279  """
7280  ctx = _get_ctx(ctx)
7281  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7282  dsz, dnames, ddecls = _dict2darray(decls, ctx)
7283  return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
7284 
def parse_smt2_string
Definition: z3py.py:7265
def z3py.ParThen (   t1,
  t2,
  ctx = None 
)
Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.

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

Definition at line 6606 of file z3py.py.

Referenced by ParAndThen().

6606 def ParThen(t1, t2, ctx=None):
6607  """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
6608 
6609  >>> x, y = Ints('x y')
6610  >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
6611  >>> t(And(Or(x == 1, x == 2), y == x + 1))
6612  [[x == 1, y == 2], [x == 2, y == 3]]
6613  """
6614  t1 = _to_tactic(t1, ctx)
6615  t2 = _to_tactic(t2, ctx)
6616  if __debug__:
6617  _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
6618  return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
6619 
Z3_tactic Z3_API Z3_tactic_par_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
def ParThen
Definition: z3py.py:6606
def z3py.probe_description (   name,
  ctx = None 
)
Return a short description for the probe named `name`.

>>> d = probe_description('memory')

Definition at line 6862 of file z3py.py.

Referenced by describe_probes().

6862 def probe_description(name, ctx=None):
6863  """Return a short description for the probe named `name`.
6864 
6865  >>> d = probe_description('memory')
6866  """
6867  ctx = _get_ctx(ctx)
6868  return Z3_probe_get_descr(ctx.ref(), name)
6869 
Z3_string Z3_API Z3_probe_get_descr(__in Z3_context c, __in Z3_string name)
Return a string containing a description of the probe with the given name.
def probe_description
Definition: z3py.py:6862
def z3py.probes (   ctx = None)
Return a list of all available probes in Z3.

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

Definition at line 6852 of file z3py.py.

Referenced by describe_probes().

6852 def probes(ctx=None):
6853  """Return a list of all available probes in Z3.
6854 
6855  >>> l = probes()
6856  >>> l.count('memory') == 1
6857  True
6858  """
6859  ctx = _get_ctx(ctx)
6860  return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]
6861 
Z3_string Z3_API Z3_get_probe_name(__in Z3_context c, unsigned i)
Return the name of the i probe.
def probes
Definition: z3py.py:6852
unsigned Z3_API Z3_get_num_probes(__in Z3_context c)
Return the number of builtin probes available in Z3.
def z3py.Product (   args)
Create the product of the Z3 expressions. 

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

Definition at line 7059 of file z3py.py.

Referenced by BitVecs().

7059 def Product(*args):
7060  """Create the product of the Z3 expressions.
7061 
7062  >>> a, b, c = Ints('a b c')
7063  >>> Product(a, b, c)
7064  a*b*c
7065  >>> Product([a, b, c])
7066  a*b*c
7067  >>> A = IntVector('a', 5)
7068  >>> Product(A)
7069  a__0*a__1*a__2*a__3*a__4
7070  """
7071  args = _get_args(args)
7072  if __debug__:
7073  _z3_assert(len(args) > 0, "Non empty list of arguments expected")
7074  ctx = _ctx_from_ast_arg_list(args)
7075  if __debug__:
7076  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
7077  args = _coerce_expr_list(args, ctx)
7078  if is_bv(args[0]):
7079  return _reduce(lambda a, b: a * b, args, 1)
7080  else:
7081  _args, sz = _to_ast_array(args)
7082  return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
7083 
Z3_ast Z3_API Z3_mk_mul(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].The array args must have num_args el...
def Product(args)
Definition: z3py.py:7059
def is_bv(a)
Definition: z3py.py:3390
def z3py.prove (   claim,
  keywords 
)
Try to prove the given claim.

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

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

Definition at line 7141 of file z3py.py.

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

7141 def prove(claim, **keywords):
7142  """Try to prove the given claim.
7143 
7144  This is a simple function for creating demonstrations. It tries to prove
7145  `claim` by showing the negation is unsatisfiable.
7146 
7147  >>> p, q = Bools('p q')
7148  >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
7149  proved
7150  """
7151  if __debug__:
7152  _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
7153  s = Solver()
7154  s.set(**keywords)
7155  s.add(Not(claim))
7156  if keywords.get('show', False):
7157  print(s)
7158  r = s.check()
7159  if r == unsat:
7160  print("proved")
7161  elif r == unknown:
7162  print("failed to prove")
7163  print(s.model())
7164  else:
7165  print("counterexample")
7166  print(s.model())
7167 
def Not
Definition: z3py.py:1443
def prove(claim, keywords)
Definition: z3py.py:7141
def is_bool(a)
Definition: z3py.py:1225
def z3py.Q (   a,
  b,
  ctx = None 
)
Return a Z3 rational a/b.

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

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

Definition at line 2705 of file z3py.py.

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

2705 def Q(a, b, ctx=None):
2706  """Return a Z3 rational a/b.
2707 
2708  If `ctx=None`, then the global context is used.
2709 
2710  >>> Q(3,5)
2711  3/5
2712  >>> Q(3,5).sort()
2713  Real
2714  """
2715  return simplify(RatVal(a, b))
2716 
def simplify(a, arguments, keywords)
Utils.
Definition: z3py.py:6956
def Q
Definition: z3py.py:2705
def RatVal
Definition: z3py.py:2690
def z3py.RatVal (   a,
  b,
  ctx = None 
)
Return a Z3 rational a/b.

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

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

Definition at line 2690 of file z3py.py.

Referenced by Q().

2690 def RatVal(a, b, ctx=None):
2691  """Return a Z3 rational a/b.
2692 
2693  If `ctx=None`, then the global context is used.
2694 
2695  >>> RatVal(3,5)
2696  3/5
2697  >>> RatVal(3,5).sort()
2698  Real
2699  """
2700  if __debug__:
2701  _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
2702  _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
2703  return simplify(RealVal(a, ctx)/RealVal(b, ctx))
2704 
def simplify(a, arguments, keywords)
Utils.
Definition: z3py.py:6956
def RealVal
Definition: z3py.py:2672
def RatVal
Definition: z3py.py:2690
def z3py.Real (   name,
  ctx = None 
)
Return a real constant named `name`. If `ctx=None`, then the global context is used.

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

Definition at line 2765 of file z3py.py.

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

2765 def Real(name, ctx=None):
2766  """Return a real constant named `name`. If `ctx=None`, then the global context is used.
2767 
2768  >>> x = Real('x')
2769  >>> is_real(x)
2770  True
2771  >>> is_real(x + 1)
2772  True
2773  """
2774  ctx = _get_ctx(ctx)
2775  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
2776 
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
def RealSort
Definition: z3py.py:2630
def Real
Definition: z3py.py:2765
def to_symbol
Definition: z3py.py:94
def z3py.Reals (   names,
  ctx = None 
)
Return a tuple of real constants. 

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

Definition at line 2777 of file z3py.py.

Referenced by is_div().

2777 def Reals(names, ctx=None):
2778  """Return a tuple of real constants.
2779 
2780  >>> x, y, z = Reals('x y z')
2781  >>> Sum(x, y, z)
2782  x + y + z
2783  >>> Sum(x, y, z).sort()
2784  Real
2785  """
2786  ctx = _get_ctx(ctx)
2787  if isinstance(names, str):
2788  names = names.split(" ")
2789  return [Real(name, ctx) for name in names]
2790 
def Real
Definition: z3py.py:2765
def Reals
Definition: z3py.py:2777
def z3py.RealSort (   ctx = None)
Return the real sort in the given context. If `ctx=None`, then the global context is used.

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

Definition at line 2630 of file z3py.py.

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

2630 def RealSort(ctx=None):
2631  """Return the real sort in the given context. If `ctx=None`, then the global context is used.
2632 
2633  >>> RealSort()
2634  Real
2635  >>> x = Const('x', RealSort())
2636  >>> is_real(x)
2637  True
2638  >>> is_int(x)
2639  False
2640  >>> x.sort() == RealSort()
2641  True
2642  """
2643  ctx = _get_ctx(ctx)
2644  return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
2645 
def RealSort
Definition: z3py.py:2630
Z3_sort Z3_API Z3_mk_real_sort(__in Z3_context c)
Create the real type.
Arithmetic.
Definition: z3py.py:1835
def z3py.RealVal (   val,
  ctx = None 
)
Return a Z3 real value. 

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

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

Definition at line 2672 of file z3py.py.

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

2672 def RealVal(val, ctx=None):
2673  """Return a Z3 real value.
2674 
2675  `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
2676  If `ctx=None`, then the global context is used.
2677 
2678  >>> RealVal(1)
2679  1
2680  >>> RealVal(1).sort()
2681  Real
2682  >>> RealVal("3/5")
2683  3/5
2684  >>> RealVal("1.5")
2685  3/2
2686  """
2687  ctx = _get_ctx(ctx)
2688  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
2689 
def RealSort
Definition: z3py.py:2630
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
def RealVal
Definition: z3py.py:2672
def z3py.RealVar (   idx,
  ctx = None 
)
Create a real free variable. Free variables are used to create quantified formulas.
They are also used to create polynomials.

>>> RealVar(0)
Var(0)

Definition at line 1171 of file z3py.py.

Referenced by RealVarVector().

1171 def RealVar(idx, ctx=None):
1172  """
1173  Create a real free variable. Free variables are used to create quantified formulas.
1174  They are also used to create polynomials.
1175 
1176  >>> RealVar(0)
1177  Var(0)
1178  """
1179  return Var(idx, RealSort(ctx))
1180 
def RealSort
Definition: z3py.py:2630
def Var(idx, s)
Definition: z3py.py:1159
def RealVar
Definition: z3py.py:1171
def z3py.RealVarVector (   n,
  ctx = None 
)
Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1

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

Definition at line 1181 of file z3py.py.

1181 def RealVarVector(n, ctx=None):
1182  """
1183  Create a list of Real free variables.
1184  The variables have ids: 0, 1, ..., n-1
1185 
1186  >>> x0, x1, x2, x3 = RealVarVector(4)
1187  >>> x2
1188  Var(2)
1189  """
1190  return [ RealVar(i, ctx) for i in range(n) ]
1191 
def RealVarVector
Definition: z3py.py:1181
def RealVar
Definition: z3py.py:1171
def z3py.RealVector (   prefix,
  sz,
  ctx = None 
)
Return a list of real constants of size `sz`.

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

Definition at line 2791 of file z3py.py.

2791 def RealVector(prefix, sz, ctx=None):
2792  """Return a list of real constants of size `sz`.
2793 
2794  >>> X = RealVector('x', 3)
2795  >>> X
2796  [x__0, x__1, x__2]
2797  >>> Sum(X)
2798  x__0 + x__1 + x__2
2799  >>> Sum(X).sort()
2800  Real
2801  """
2802  return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]
2803 
def Real
Definition: z3py.py:2765
def RealVector
Definition: z3py.py:2791
def z3py.Repeat (   t,
  max = 4294967295,
  ctx = None 
)
Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.

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

Definition at line 6637 of file z3py.py.

6637 def Repeat(t, max=4294967295, ctx=None):
6638  """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
6639 
6640  >>> x, y = Ints('x y')
6641  >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
6642  >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
6643  >>> r = t(c)
6644  >>> for subgoal in r: print(subgoal)
6645  [x == 0, y == 0, x > y]
6646  [x == 0, y == 1, x > y]
6647  [x == 1, y == 0, x > y]
6648  [x == 1, y == 1, x > y]
6649  >>> t = Then(t, Tactic('propagate-values'))
6650  >>> t(c)
6651  [[x == 1, y == 0]]
6652  """
6653  t = _to_tactic(t, ctx)
6654  return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)
6655 
Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
def Repeat
Definition: z3py.py:6637
def z3py.RepeatBitVec (   n,
  a 
)
Return an expression representing `n` copies of `a`.

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

Definition at line 3793 of file z3py.py.

3793 def RepeatBitVec(n, a):
3794  """Return an expression representing `n` copies of `a`.
3795 
3796  >>> x = BitVec('x', 8)
3797  >>> n = RepeatBitVec(4, x)
3798  >>> n
3799  RepeatBitVec(4, x)
3800  >>> n.size()
3801  32
3802  >>> v0 = BitVecVal(10, 4)
3803  >>> print("%.x" % v0.as_long())
3804  a
3805  >>> v = simplify(RepeatBitVec(4, v0))
3806  >>> v.size()
3807  16
3808  >>> print("%.x" % v.as_long())
3809  aaaa
3810  """
3811  if __debug__:
3812  _z3_assert(isinstance(n, int), "First argument must be an integer")
3813  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3814  return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
3815 
Z3_ast Z3_API Z3_mk_repeat(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Repeat the given bit-vector up length i.
def is_bv(a)
Definition: z3py.py:3390
def RepeatBitVec(n, a)
Definition: z3py.py:3793
def z3py.reset_params ( )
Reset all global (or module) parameters.

Definition at line 237 of file z3py.py.

238  """Reset all global (or module) parameters.
239  """
241 
def reset_params()
Definition: z3py.py:237
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
def z3py.RotateLeft (   a,
  b 
)
Return an expression representing `a` rotated to the left `b` times.

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

Definition at line 3707 of file z3py.py.

3707 def RotateLeft(a, b):
3708  """Return an expression representing `a` rotated to the left `b` times.
3709 
3710  >>> a, b = BitVecs('a b', 16)
3711  >>> RotateLeft(a, b)
3712  RotateLeft(a, b)
3713  >>> simplify(RotateLeft(a, 0))
3714  a
3715  >>> simplify(RotateLeft(a, 16))
3716  a
3717  """
3718  _check_bv_args(a, b)
3719  a, b = _coerce_exprs(a, b)
3720  return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3721 
def RotateLeft(a, b)
Definition: z3py.py:3707
Z3_ast Z3_API Z3_mk_ext_rotate_left(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Rotate bits of t1 to the left t2 times.
def z3py.RotateRight (   a,
  b 
)
Return an expression representing `a` rotated to the right `b` times.

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

Definition at line 3722 of file z3py.py.

3722 def RotateRight(a, b):
3723  """Return an expression representing `a` rotated to the right `b` times.
3724 
3725  >>> a, b = BitVecs('a b', 16)
3726  >>> RotateRight(a, b)
3727  RotateRight(a, b)
3728  >>> simplify(RotateRight(a, 0))
3729  a
3730  >>> simplify(RotateRight(a, 16))
3731  a
3732  """
3733  _check_bv_args(a, b)
3734  a, b = _coerce_exprs(a, b)
3735  return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3736 
Z3_ast Z3_API Z3_mk_ext_rotate_right(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Rotate bits of t1 to the right t2 times.
def RotateRight(a, b)
Definition: z3py.py:3722
def z3py.Select (   a,
  i 
)
Return a Z3 select array expression.

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

Definition at line 4026 of file z3py.py.

4026 def Select(a, i):
4027  """Return a Z3 select array expression.
4028 
4029  >>> a = Array('a', IntSort(), IntSort())
4030  >>> i = Int('i')
4031  >>> Select(a, i)
4032  a[i]
4033  >>> eq(Select(a, i), a[i])
4034  True
4035  """
4036  if __debug__:
4037  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
4038  return a[i]
4039 
def is_array(a)
Definition: z3py.py:3886
def Select(a, i)
Definition: z3py.py:4026
def z3py.sequence_interpolant (   v,
  p = None,
  ctx = None 
)
Compute interpolant for a sequence of formulas.

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

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

Requires len(v) >= 1. 

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

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

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

Definition at line 7391 of file z3py.py.

7391 def sequence_interpolant(v,p=None,ctx=None):
7392  """Compute interpolant for a sequence of formulas.
7393 
7394  If len(v) == N, and if the conjunction of the formulas in v is
7395  unsatisfiable, the interpolant is a sequence of formulas w
7396  such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
7397 
7398  1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
7399  2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
7400  and v[i+1]..v[n]
7401 
7402  Requires len(v) >= 1.
7403 
7404  If a & b is satisfiable, raises an object of class ModelRef
7405  that represents a model of a & b.
7406 
7407  If parameters p are supplied, these are used in creating the
7408  solver that determines satisfiability.
7409 
7410  >>> x = Int('x')
7411  >>> y = Int('y')
7412  >>> print sequence_interpolant([x < 0, y == x , y > 2])
7413  [Not(x >= 0), Not(y >= 0)]
7414  """
7415  f = v[0]
7416  for i in range(1,len(v)):
7417  f = And(Interpolant(f),v[i])
7418  return tree_interpolant(f,p,ctx)
7419 
7420 
def And(args)
Definition: z3py.py:1468
def sequence_interpolant
Definition: z3py.py:7391
def Interpolant
Definition: z3py.py:7295
def tree_interpolant
Definition: z3py.py:7309
def z3py.set_option (   args,
  kws 
)
Alias for 'set_param' for backward compatibility.

Definition at line 242 of file z3py.py.

242 def set_option(*args, **kws):
243  """Alias for 'set_param' for backward compatibility.
244  """
245  return set_param(*args, **kws)
246 
def set_option(args, kws)
Definition: z3py.py:242
def set_param(args, kws)
Definition: z3py.py:214
def z3py.set_param (   args,
  kws 
)
Set Z3 global (or module) parameters.

>>> set_param(precision=10)

Definition at line 214 of file z3py.py.

Referenced by set_option().

214 def set_param(*args, **kws):
215  """Set Z3 global (or module) parameters.
216 
217  >>> set_param(precision=10)
218  """
219  if __debug__:
220  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
221  new_kws = {}
222  for k in kws:
223  v = kws[k]
224  if not set_pp_option(k, v):
225  new_kws[k] = v
226  for key in new_kws:
227  value = new_kws[key]
228  Z3_global_param_set(str(key).upper(), _to_param_value(value))
229  prev = None
230  for a in args:
231  if prev == None:
232  prev = a
233  else:
234  Z3_global_param_set(str(prev), _to_param_value(a))
235  prev = None
236 
def set_param(args, kws)
Definition: z3py.py:214
void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
def z3py.SignExt (   n,
  a 
)
Return a bit-vector expression with `n` extra sign-bits.

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

Definition at line 3737 of file z3py.py.

3737 def SignExt(n, a):
3738  """Return a bit-vector expression with `n` extra sign-bits.
3739 
3740  >>> x = BitVec('x', 16)
3741  >>> n = SignExt(8, x)
3742  >>> n.size()
3743  24
3744  >>> n
3745  SignExt(8, x)
3746  >>> n.sort()
3747  BitVec(24)
3748  >>> v0 = BitVecVal(2, 2)
3749  >>> v0
3750  2
3751  >>> v0.size()
3752  2
3753  >>> v = simplify(SignExt(6, v0))
3754  >>> v
3755  254
3756  >>> v.size()
3757  8
3758  >>> print("%.x" % v.as_long())
3759  fe
3760  """
3761  if __debug__:
3762  _z3_assert(isinstance(n, int), "First argument must be an integer")
3763  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3764  return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
3765 
def SignExt(n, a)
Definition: z3py.py:3737
Z3_ast Z3_API Z3_mk_sign_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
def is_bv(a)
Definition: z3py.py:3390
def z3py.SimpleSolver (   ctx = None)
Return a simple general purpose solver with limited amount of preprocessing.

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

Definition at line 6073 of file z3py.py.

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

6073 def SimpleSolver(ctx=None):
6074  """Return a simple general purpose solver with limited amount of preprocessing.
6075 
6076  >>> s = SimpleSolver()
6077  >>> x = Int('x')
6078  >>> s.add(x > 0)
6079  >>> s.check()
6080  sat
6081  """
6082  ctx = _get_ctx(ctx)
6083  return Solver(Z3_mk_simple_solver(ctx.ref()), ctx)
6084 
Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c)
Create a new (incremental) solver.
def SimpleSolver
Definition: z3py.py:6073
def z3py.simplify (   a,
  arguments,
  keywords 
)

Utils.

Simplify the expression `a` using the given options.

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

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

Definition at line 6956 of file z3py.py.

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

6956 def simplify(a, *arguments, **keywords):
6957  """Simplify the expression `a` using the given options.
6958 
6959  This function has many options. Use `help_simplify` to obtain the complete list.
6960 
6961  >>> x = Int('x')
6962  >>> y = Int('y')
6963  >>> simplify(x + 1 + y + x + 1)
6964  2 + 2*x + y
6965  >>> simplify((x + 1)*(y + 1), som=True)
6966  1 + x + y + x*y
6967  >>> simplify(Distinct(x, y, 1), blast_distinct=True)
6968  And(Not(x == y), Not(x == 1), Not(y == 1))
6969  >>> simplify(And(x == 0, y == 1), elim_and=True)
6970  Not(Or(Not(x == 0), Not(y == 1)))
6971  """
6972  if __debug__:
6973  _z3_assert(is_expr(a), "Z3 expression expected")
6974  if len(arguments) > 0 or len(keywords) > 0:
6975  p = args2params(arguments, keywords, a.ctx)
6976  return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
6977  else:
6978  return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
6979 
def simplify(a, arguments, keywords)
Utils.
Definition: z3py.py:6956
def args2params
Definition: z3py.py:4467
Z3_ast Z3_API Z3_simplify(__in Z3_context c, __in Z3_ast a)
Interface to simplifier.
def is_expr(a)
Definition: z3py.py:950
Z3_ast Z3_API Z3_simplify_ex(__in Z3_context c, __in Z3_ast a, __in Z3_params p)
Interface to simplifier.
def z3py.simplify_param_descrs ( )
Return the set of parameter descriptions for Z3 `simplify` procedure.

Definition at line 6984 of file z3py.py.

6985  """Return the set of parameter descriptions for Z3 `simplify` procedure."""
6987 
def main_ctx()
Definition: z3py.py:188
def simplify_param_descrs()
Definition: z3py.py:6984
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(__in Z3_context c)
Return the parameter description set for the 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 = Int('a')
>>> solve(a > 0, a < 2)
[a = 1]

Definition at line 7084 of file z3py.py.

Referenced by BV2Int(), and IsInt().

7084 def solve(*args, **keywords):
7085  """Solve the constraints `*args`.
7086 
7087  This is a simple function for creating demonstrations. It creates a solver,
7088  configure it using the options in `keywords`, adds the constraints
7089  in `args`, and invokes check.
7090 
7091  >>> a = Int('a')
7092  >>> solve(a > 0, a < 2)
7093  [a = 1]
7094  """
7095  s = Solver()
7096  s.set(**keywords)
7097  s.add(*args)
7098  if keywords.get('show', False):
7099  print(s)
7100  r = s.check()
7101  if r == unsat:
7102  print("no solution")
7103  elif r == unknown:
7104  print("failed to solve")
7105  try:
7106  print(s.model())
7107  except Z3Exception:
7108  return
7109  else:
7110  print(s.model())
7111 
def solve(args, keywords)
Definition: z3py.py:7084
def z3py.solve_using (   s,
  args,
  keywords 
)
Solve the constraints `*args` using solver `s`.

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

Definition at line 7112 of file z3py.py.

7112 def solve_using(s, *args, **keywords):
7113  """Solve the constraints `*args` using solver `s`.
7114 
7115  This is a simple function for creating demonstrations. It is similar to `solve`,
7116  but it uses the given solver `s`.
7117  It configures solver `s` using the options in `keywords`, adds the constraints
7118  in `args`, and invokes check.
7119  """
7120  if __debug__:
7121  _z3_assert(isinstance(s, Solver), "Solver object expected")
7122  s.set(**keywords)
7123  s.add(*args)
7124  if keywords.get('show', False):
7125  print("Problem:")
7126  print(s)
7127  r = s.check()
7128  if r == unsat:
7129  print("no solution")
7130  elif r == unknown:
7131  print("failed to solve")
7132  try:
7133  print(s.model())
7134  except Z3Exception:
7135  return
7136  else:
7137  if keywords.get('show', False):
7138  print("Solution:")
7139  print(s.model())
7140 
def solve_using(s, args, keywords)
Definition: z3py.py:7112
def z3py.SolverFor (   logic,
  ctx = None 
)
Create a solver customized for the given logic. 

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

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

Definition at line 6053 of file z3py.py.

6053 def SolverFor(logic, ctx=None):
6054  """Create a solver customized for the given logic.
6055 
6056  The parameter `logic` is a string. It should be contains
6057  the name of a SMT-LIB logic.
6058  See http://www.smtlib.org/ for the name of all available logics.
6059 
6060  >>> s = SolverFor("QF_LIA")
6061  >>> x = Int('x')
6062  >>> s.add(x > 0)
6063  >>> s.add(x < 2)
6064  >>> s.check()
6065  sat
6066  >>> s.model()
6067  [x = 1]
6068  """
6069  ctx = _get_ctx(ctx)
6070  logic = to_symbol(logic)
6071  return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx)
6072 
def SolverFor
Definition: z3py.py:6053
Z3_solver Z3_API Z3_mk_solver_for_logic(__in Z3_context c, __in Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
def to_symbol
Definition: z3py.py:94
def z3py.Sqrt (   a,
  ctx = None 
)
Return a Z3 expression which represents the square root of a. 

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

Definition at line 2867 of file z3py.py.

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

2867 def Sqrt(a, ctx=None):
2868  """ Return a Z3 expression which represents the square root of a.
2869 
2870  >>> x = Real('x')
2871  >>> Sqrt(x)
2872  x**(1/2)
2873  """
2874  if not is_expr(a):
2875  ctx = _get_ctx(ctx)
2876  a = RealVal(a, ctx)
2877  return a ** "1/2"
2878 
def RealVal
Definition: z3py.py:2672
def is_expr(a)
Definition: z3py.py:950
def Sqrt
Definition: z3py.py:2867
def z3py.SRem (   a,
  b 
)
Create the Z3 expression signed remainder.

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

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

Definition at line 3656 of file z3py.py.

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

3656 def SRem(a, b):
3657  """Create the Z3 expression signed remainder.
3658 
3659  Use the operator % for signed modulus, and URem() for unsigned remainder.
3660 
3661  >>> x = BitVec('x', 32)
3662  >>> y = BitVec('y', 32)
3663  >>> SRem(x, y)
3664  SRem(x, y)
3665  >>> SRem(x, y).sort()
3666  BitVec(32)
3667  >>> (x % y).sexpr()
3668  '(bvsmod x y)'
3669  >>> SRem(x, y).sexpr()
3670  '(bvsrem x y)'
3671  """
3672  _check_bv_args(a, b)
3673  a, b = _coerce_exprs(a, b)
3674  return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3675 
Z3_ast Z3_API Z3_mk_bvsrem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
def SRem(a, b)
Definition: z3py.py:3656
def z3py.Store (   a,
  i,
  v 
)
Return a Z3 store array expression.

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

Definition at line 4010 of file z3py.py.

Referenced by is_array(), and is_store().

4010 def Store(a, i, v):
4011  """Return a Z3 store array expression.
4012 
4013  >>> a = Array('a', IntSort(), IntSort())
4014  >>> i, v = Ints('i v')
4015  >>> s = Store(a, i, v)
4016  >>> s.sort()
4017  Array(Int, Int)
4018  >>> prove(s[i] == v)
4019  proved
4020  >>> j = Int('j')
4021  >>> prove(Implies(i != j, s[j] == a[j]))
4022  proved
4023  """
4024  return Update(a, i, v)
4025 
def Update(a, i, v)
Definition: z3py.py:3989
def Store(a, i, v)
Definition: z3py.py:4010
def z3py.substitute (   t,
  m 
)
Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to.

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

Definition at line 6988 of file z3py.py.

6988 def substitute(t, *m):
6989  """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.
6990 
6991  >>> x = Int('x')
6992  >>> y = Int('y')
6993  >>> substitute(x + 1, (x, y + 1))
6994  y + 1 + 1
6995  >>> f = Function('f', IntSort(), IntSort())
6996  >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
6997  1 + 1
6998  """
6999  if isinstance(m, tuple):
7000  m1 = _get_args(m)
7001  if isinstance(m1, list):
7002  m = m1
7003  if __debug__:
7004  _z3_assert(is_expr(t), "Z3 expression expected")
7005  _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
7006  num = len(m)
7007  _from = (Ast * num)()
7008  _to = (Ast * num)()
7009  for i in range(num):
7010  _from[i] = m[i][0].as_ast()
7011  _to[i] = m[i][1].as_ast()
7012  return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
7013 
Z3_ast Z3_API Z3_substitute(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const from[], __in_ecount(num_exprs) Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
def substitute(t, m)
Definition: z3py.py:6988
def eq(a, b)
Definition: z3py.py:372
def is_expr(a)
Definition: z3py.py:950
def z3py.substitute_vars (   t,
  m 
)
Substitute the free variables in t with the expression in m.

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

Definition at line 7014 of file z3py.py.

7014 def substitute_vars(t, *m):
7015  """Substitute the free variables in t with the expression in m.
7016 
7017  >>> v0 = Var(0, IntSort())
7018  >>> v1 = Var(1, IntSort())
7019  >>> x = Int('x')
7020  >>> f = Function('f', IntSort(), IntSort(), IntSort())
7021  >>> # replace v0 with x+1 and v1 with x
7022  >>> substitute_vars(f(v0, v1), x + 1, x)
7023  f(x + 1, x)
7024  """
7025  if __debug__:
7026  _z3_assert(is_expr(t), "Z3 expression expected")
7027  _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
7028  num = len(m)
7029  _to = (Ast * num)()
7030  for i in range(num):
7031  _to[i] = m[i].as_ast()
7032  return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
7033 
Z3_ast Z3_API Z3_substitute_vars(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
def substitute_vars(t, m)
Definition: z3py.py:7014
def is_expr(a)
Definition: z3py.py:950
def z3py.Sum (   args)
Create the sum of the Z3 expressions. 

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

Definition at line 7034 of file z3py.py.

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

7034 def Sum(*args):
7035  """Create the sum of the Z3 expressions.
7036 
7037  >>> a, b, c = Ints('a b c')
7038  >>> Sum(a, b, c)
7039  a + b + c
7040  >>> Sum([a, b, c])
7041  a + b + c
7042  >>> A = IntVector('a', 5)
7043  >>> Sum(A)
7044  a__0 + a__1 + a__2 + a__3 + a__4
7045  """
7046  args = _get_args(args)
7047  if __debug__:
7048  _z3_assert(len(args) > 0, "Non empty list of arguments expected")
7049  ctx = _ctx_from_ast_arg_list(args)
7050  if __debug__:
7051  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
7052  args = _coerce_expr_list(args, ctx)
7053  if is_bv(args[0]):
7054  return _reduce(lambda a, b: a + b, args, 0)
7055  else:
7056  _args, sz = _to_ast_array(args)
7057  return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)
7058 
def Sum(args)
Definition: z3py.py:7034
def is_bv(a)
Definition: z3py.py:3390
Z3_ast Z3_API Z3_mk_add(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].The array args must have num_args el...
def z3py.tactic_description (   name,
  ctx = None 
)
Return a short description for the tactic named `name`.

>>> d = tactic_description('simplify')

Definition at line 6674 of file z3py.py.

Referenced by describe_tactics().

6674 def tactic_description(name, ctx=None):
6675  """Return a short description for the tactic named `name`.
6676 
6677  >>> d = tactic_description('simplify')
6678  """
6679  ctx = _get_ctx(ctx)
6680  return Z3_tactic_get_descr(ctx.ref(), name)
6681 
Z3_string Z3_API Z3_tactic_get_descr(__in Z3_context c, __in Z3_string name)
Return a string containing a description of the tactic with the given name.
def tactic_description
Definition: z3py.py:6674
def z3py.tactics (   ctx = None)
Return a list of all available tactics in Z3.

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

Definition at line 6664 of file z3py.py.

Referenced by describe_tactics().

6664 def tactics(ctx=None):
6665  """Return a list of all available tactics in Z3.
6666 
6667  >>> l = tactics()
6668  >>> l.count('simplify') == 1
6669  True
6670  """
6671  ctx = _get_ctx(ctx)
6672  return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]
6673 
Z3_string Z3_API Z3_get_tactic_name(__in Z3_context c, unsigned i)
Return the name of the idx tactic.
unsigned Z3_API Z3_get_num_tactics(__in Z3_context c)
Return the number of builtin tactics available in Z3.
def tactics
Definition: z3py.py:6664
def z3py.Then (   ts,
  ks 
)
Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).

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

Definition at line 6556 of file z3py.py.

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

6556 def Then(*ts, **ks):
6557  """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
6558 
6559  >>> x, y = Ints('x y')
6560  >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
6561  >>> t(And(x == 0, y > x + 1))
6562  [[Not(y <= 1)]]
6563  >>> t(And(x == 0, y > x + 1)).as_expr()
6564  Not(y <= 1)
6565  """
6566  return AndThen(*ts, **ks)
6567 
def Then(ts, ks)
Definition: z3py.py:6556
def AndThen(ts, ks)
Definition: z3py.py:6537
def z3py.to_symbol (   s,
  ctx = None 
)
Convert an integer or string into a Z3 symbol.

Definition at line 94 of file z3py.py.

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

94 def to_symbol(s, ctx=None):
95  """Convert an integer or string into a Z3 symbol."""
96  if isinstance(s, int):
97  return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
98  else:
99  return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
100 
Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in Z3_string s)
Create a Z3 symbol using a C string.
def to_symbol
Definition: z3py.py:94
Z3_symbol Z3_API Z3_mk_int_symbol(__in Z3_context c, __in int i)
Create a Z3 symbol using an integer.
def z3py.ToInt (   a)
Return the Z3 expression ToInt(a). 

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

Definition at line 2834 of file z3py.py.

Referenced by is_to_int().

2834 def ToInt(a):
2835  """ Return the Z3 expression ToInt(a).
2836 
2837  >>> x = Real('x')
2838  >>> x.sort()
2839  Real
2840  >>> n = ToInt(x)
2841  >>> n
2842  ToInt(x)
2843  >>> n.sort()
2844  Int
2845  """
2846  if __debug__:
2847  _z3_assert(a.is_real(), "Z3 real expression expected.")
2848  ctx = a.ctx
2849  return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
2850 
Z3_ast Z3_API Z3_mk_real2int(__in Z3_context c, __in Z3_ast t1)
Coerce a real to an integer.
def ToInt(a)
Definition: z3py.py:2834
def z3py.ToReal (   a)
Return the Z3 expression ToReal(a). 

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

Definition at line 2817 of file z3py.py.

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

2817 def ToReal(a):
2818  """ Return the Z3 expression ToReal(a).
2819 
2820  >>> x = Int('x')
2821  >>> x.sort()
2822  Int
2823  >>> n = ToReal(x)
2824  >>> n
2825  ToReal(x)
2826  >>> n.sort()
2827  Real
2828  """
2829  if __debug__:
2830  _z3_assert(a.is_int(), "Z3 integer expression expected.")
2831  ctx = a.ctx
2832  return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
2833 
Z3_ast Z3_API Z3_mk_int2real(__in Z3_context c, __in Z3_ast t1)
Coerce an integer to a real.
def ToReal(a)
Definition: z3py.py:2817
def z3py.tree_interpolant (   pat,
  p = None,
  ctx = None 
)
Compute interpolant for a tree of formulas.

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

  1) phi sigma implies sigma(phi), and

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

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

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

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

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

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

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

Definition at line 7309 of file z3py.py.

Referenced by binary_interpolant(), and sequence_interpolant().

7309 def tree_interpolant(pat,p=None,ctx=None):
7310  """Compute interpolant for a tree of formulas.
7311 
7312  The input is an interpolation pattern over a set of formulas C.
7313  The pattern pat is a formula combining the formulas in C using
7314  logical conjunction and the "interp" operator (see Interp). This
7315  interp operator is logically the identity operator. It marks the
7316  sub-formulas of the pattern for which interpolants should be
7317  computed. The interpolant is a map sigma from marked subformulas
7318  to formulas, such that, for each marked subformula phi of pat
7319  (where phi sigma is phi with sigma(psi) substituted for each
7320  subformula psi of phi such that psi in dom(sigma)):
7321 
7322  1) phi sigma implies sigma(phi), and
7323 
7324  2) sigma(phi) is in the common uninterpreted vocabulary between
7325  the formulas of C occurring in phi and those not occurring in
7326  phi
7327 
7328  and moreover pat sigma implies false. In the simplest case
7329  an interpolant for the pattern "(and (interp A) B)" maps A
7330  to an interpolant for A /\ B.
7331 
7332  The return value is a vector of formulas representing sigma. This
7333  vector contains sigma(phi) for each marked subformula of pat, in
7334  pre-order traversal. This means that subformulas of phi occur before phi
7335  in the vector. Also, subformulas that occur multiply in pat will
7336  occur multiply in the result vector.
7337 
7338  If pat is satisfiable, raises an object of class ModelRef
7339  that represents a model of pat.
7340 
7341  If parameters p are supplied, these are used in creating the
7342  solver that determines satisfiability.
7343 
7344  >>> x = Int('x')
7345  >>> y = Int('y')
7346  >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
7347  [Not(x >= 0), Not(y <= 2)]
7348 
7349  >>> g = And(Interpolant(x<0),x<2)
7350  >>> try:
7351  ... print tree_interpolant(g).sexpr()
7352  ... except ModelRef as m:
7353  ... print m.sexpr()
7354  (define-fun x () Int
7355  (- 1))
7356  """
7357  f = pat
7358  ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
7359  ptr = (AstVectorObj * 1)()
7360  mptr = (Model * 1)()
7361  if p == None:
7362  p = ParamsRef(ctx)
7363  res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
7364  if res == Z3_L_FALSE:
7365  return AstVector(ptr[0],ctx)
7366  raise ModelRef(mptr[0], ctx)
7367 
Parameter Sets.
Definition: z3py.py:4430
def tree_interpolant
Definition: z3py.py:7309
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model)
def z3py.TryFor (   t,
  ms,
  ctx = None 
)
Return a tactic that applies `t` to a given goal for `ms` milliseconds.

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

Definition at line 6656 of file z3py.py.

6656 def TryFor(t, ms, ctx=None):
6657  """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
6658 
6659  If `t` does not terminate in `ms` milliseconds, then it fails.
6660  """
6661  t = _to_tactic(t, ctx)
6662  return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)
6663 
Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
def TryFor
Definition: z3py.py:6656
def z3py.UDiv (   a,
  b 
)
Create the Z3 expression (unsigned) division `self / other`.

Use the operator / for signed division.

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

Definition at line 3616 of file z3py.py.

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

3616 def UDiv(a, b):
3617  """Create the Z3 expression (unsigned) division `self / other`.
3618 
3619  Use the operator / for signed division.
3620 
3621  >>> x = BitVec('x', 32)
3622  >>> y = BitVec('y', 32)
3623  >>> UDiv(x, y)
3624  UDiv(x, y)
3625  >>> UDiv(x, y).sort()
3626  BitVec(32)
3627  >>> (x / y).sexpr()
3628  '(bvsdiv x y)'
3629  >>> UDiv(x, y).sexpr()
3630  '(bvudiv x y)'
3631  """
3632  _check_bv_args(a, b)
3633  a, b = _coerce_exprs(a, b)
3634  return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3635 
Z3_ast Z3_API Z3_mk_bvudiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned division.
def UDiv(a, b)
Definition: z3py.py:3616
def z3py.UGE (   a,
  b 
)
Create the Z3 expression (unsigned) `other >= self`.

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

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

Definition at line 3582 of file z3py.py.

Referenced by BitVecRef.__ge__().

3582 def UGE(a, b):
3583  """Create the Z3 expression (unsigned) `other >= self`.
3584 
3585  Use the operator >= for signed greater than or equal to.
3586 
3587  >>> x, y = BitVecs('x y', 32)
3588  >>> UGE(x, y)
3589  UGE(x, y)
3590  >>> (x >= y).sexpr()
3591  '(bvsge x y)'
3592  >>> UGE(x, y).sexpr()
3593  '(bvuge x y)'
3594  """
3595  _check_bv_args(a, b)
3596  a, b = _coerce_exprs(a, b)
3597  return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3598 
def UGE(a, b)
Definition: z3py.py:3582
Z3_ast Z3_API Z3_mk_bvuge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than or equal to.
def z3py.UGT (   a,
  b 
)
Create the Z3 expression (unsigned) `other > self`.

Use the operator > for signed greater than.

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

Definition at line 3599 of file z3py.py.

Referenced by BitVecRef.__gt__().

3599 def UGT(a, b):
3600  """Create the Z3 expression (unsigned) `other > self`.
3601 
3602  Use the operator > for signed greater than.
3603 
3604  >>> x, y = BitVecs('x y', 32)
3605  >>> UGT(x, y)
3606  UGT(x, y)
3607  >>> (x > y).sexpr()
3608  '(bvsgt x y)'
3609  >>> UGT(x, y).sexpr()
3610  '(bvugt x y)'
3611  """
3612  _check_bv_args(a, b)
3613  a, b = _coerce_exprs(a, b)
3614  return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3615 
Z3_ast Z3_API Z3_mk_bvugt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than.
def UGT(a, b)
Definition: z3py.py:3599
def z3py.ULE (   a,
  b 
)
Create the Z3 expression (unsigned) `other <= self`.

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

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

Definition at line 3548 of file z3py.py.

Referenced by BitVecRef.__le__().

3548 def ULE(a, b):
3549  """Create the Z3 expression (unsigned) `other <= self`.
3550 
3551  Use the operator <= for signed less than or equal to.
3552 
3553  >>> x, y = BitVecs('x y', 32)
3554  >>> ULE(x, y)
3555  ULE(x, y)
3556  >>> (x <= y).sexpr()
3557  '(bvsle x y)'
3558  >>> ULE(x, y).sexpr()
3559  '(bvule x y)'
3560  """
3561  _check_bv_args(a, b)
3562  a, b = _coerce_exprs(a, b)
3563  return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3564 
Z3_ast Z3_API Z3_mk_bvule(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than or equal to.
def ULE(a, b)
Definition: z3py.py:3548
def z3py.ULT (   a,
  b 
)
Create the Z3 expression (unsigned) `other < self`.

Use the operator < for signed less than.

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

Definition at line 3565 of file z3py.py.

Referenced by BitVecRef.__lt__().

3565 def ULT(a, b):
3566  """Create the Z3 expression (unsigned) `other < self`.
3567 
3568  Use the operator < for signed less than.
3569 
3570  >>> x, y = BitVecs('x y', 32)
3571  >>> ULT(x, y)
3572  ULT(x, y)
3573  >>> (x < y).sexpr()
3574  '(bvslt x y)'
3575  >>> ULT(x, y).sexpr()
3576  '(bvult x y)'
3577  """
3578  _check_bv_args(a, b)
3579  a, b = _coerce_exprs(a, b)
3580  return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3581 
def ULT(a, b)
Definition: z3py.py:3565
Z3_ast Z3_API Z3_mk_bvult(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than.
def z3py.Update (   a,
  i,
  v 
)
Return a Z3 store array expression.

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

Definition at line 3989 of file z3py.py.

Referenced by Store().

3989 def Update(a, i, v):
3990  """Return a Z3 store array expression.
3991 
3992  >>> a = Array('a', IntSort(), IntSort())
3993  >>> i, v = Ints('i v')
3994  >>> s = Update(a, i, v)
3995  >>> s.sort()
3996  Array(Int, Int)
3997  >>> prove(s[i] == v)
3998  proved
3999  >>> j = Int('j')
4000  >>> prove(Implies(i != j, s[j] == a[j]))
4001  proved
4002  """
4003  if __debug__:
4004  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
4005  i = a.domain().cast(i)
4006  v = a.range().cast(v)
4007  ctx = a.ctx
4008  return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
4009 
def is_array(a)
Definition: z3py.py:3886
def Update(a, i, v)
Definition: z3py.py:3989
Z3_ast Z3_API Z3_mk_store(__in Z3_context c, __in Z3_ast a, __in Z3_ast i, __in Z3_ast v)
Array update.
def z3py.URem (   a,
  b 
)
Create the Z3 expression (unsigned) remainder `self % other`.

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

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

Definition at line 3636 of file z3py.py.

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

3636 def URem(a, b):
3637  """Create the Z3 expression (unsigned) remainder `self % other`.
3638 
3639  Use the operator % for signed modulus, and SRem() for signed remainder.
3640 
3641  >>> x = BitVec('x', 32)
3642  >>> y = BitVec('y', 32)
3643  >>> URem(x, y)
3644  URem(x, y)
3645  >>> URem(x, y).sort()
3646  BitVec(32)
3647  >>> (x % y).sexpr()
3648  '(bvsmod x y)'
3649  >>> URem(x, y).sexpr()
3650  '(bvurem x y)'
3651  """
3652  _check_bv_args(a, b)
3653  a, b = _coerce_exprs(a, b)
3654  return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3655 
Z3_ast Z3_API Z3_mk_bvurem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned remainder.
def URem(a, b)
Definition: z3py.py:3636
def z3py.Var (   idx,
  s 
)
Create a Z3 free variable. Free variables are used to create quantified formulas.

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

Definition at line 1159 of file z3py.py.

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

1159 def Var(idx, s):
1160  """Create a Z3 free variable. Free variables are used to create quantified formulas.
1161 
1162  >>> Var(0, IntSort())
1163  Var(0)
1164  >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1165  False
1166  """
1167  if __debug__:
1168  _z3_assert(is_sort(s), "Z3 sort expected")
1169  return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1170 
Z3_ast Z3_API Z3_mk_bound(__in Z3_context c, __in unsigned index, __in Z3_sort ty)
Create a bound variable.
def Var(idx, s)
Definition: z3py.py:1159
def is_sort(s)
Definition: z3py.py:532
def z3py.When (   p,
  t,
  ctx = None 
)
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.

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

Definition at line 6922 of file z3py.py.

6922 def When(p, t, ctx=None):
6923  """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6924 
6925  >>> t = When(Probe('size') > 2, Tactic('simplify'))
6926  >>> x, y = Ints('x y')
6927  >>> g = Goal()
6928  >>> g.add(x > 0)
6929  >>> g.add(y > 0)
6930  >>> t(g)
6931  [[x > 0, y > 0]]
6932  >>> g.add(x == y + 1)
6933  >>> t(g)
6934  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6935  """
6936  p = _to_probe(p, ctx)
6937  t = _to_tactic(t, ctx)
6938  return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
6939 
def When
Definition: z3py.py:6922
Z3_tactic Z3_API Z3_tactic_when(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
def z3py.With (   t,
  args,
  keys 
)
Return a tactic that applies tactic `t` using the given configuration options.

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

Definition at line 6624 of file z3py.py.

Referenced by Goal.prec().

6624 def With(t, *args, **keys):
6625  """Return a tactic that applies tactic `t` using the given configuration options.
6626 
6627  >>> x, y = Ints('x y')
6628  >>> t = With(Tactic('simplify'), som=True)
6629  >>> t((x + 1)*(y + 2) == 0)
6630  [[2*x + y + x*y == -2]]
6631  """
6632  ctx = keys.get('ctx', None)
6633  t = _to_tactic(t, ctx)
6634  p = args2params(args, keys, t.ctx)
6635  return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
6636 
def args2params
Definition: z3py.py:4467
Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p)
Return a tactic that applies t using the given set of parameters.
def With(t, args, keys)
Definition: z3py.py:6624
def z3py.Xor (   a,
  b,
  ctx = None 
)
Create a Z3 Xor expression.

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

Definition at line 1428 of file z3py.py.

1428 def Xor(a, b, ctx=None):
1429  """Create a Z3 Xor expression.
1430 
1431  >>> p, q = Bools('p q')
1432  >>> Xor(p, q)
1433  Xor(p, q)
1434  >>> simplify(Xor(p, q))
1435  Not(p) == q
1436  """
1437  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1438  s = BoolSort(ctx)
1439  a = s.cast(a)
1440  b = s.cast(b)
1441  return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1442 
def BoolSort
Definition: z3py.py:1325
def Xor
Definition: z3py.py:1428
Z3_ast Z3_API Z3_mk_xor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 xor t2.
def z3py.ZeroExt (   n,
  a 
)
Return a bit-vector expression with `n` extra zero-bits.

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

Definition at line 3766 of file z3py.py.

3766 def ZeroExt(n, a):
3767  """Return a bit-vector expression with `n` extra zero-bits.
3768 
3769  >>> x = BitVec('x', 16)
3770  >>> n = ZeroExt(8, x)
3771  >>> n.size()
3772  24
3773  >>> n
3774  ZeroExt(8, x)
3775  >>> n.sort()
3776  BitVec(24)
3777  >>> v0 = BitVecVal(2, 2)
3778  >>> v0
3779  2
3780  >>> v0.size()
3781  2
3782  >>> v = simplify(ZeroExt(6, v0))
3783  >>> v
3784  2
3785  >>> v.size()
3786  8
3787  """
3788  if __debug__:
3789  _z3_assert(isinstance(n, int), "First argument must be an integer")
3790  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3791  return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
3792 
Z3_ast Z3_API Z3_mk_zero_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i...
def ZeroExt(n, a)
Definition: z3py.py:3766
def is_bv(a)
Definition: z3py.py:3390

Variable Documentation

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

Definition at line 108 of file z3py.py.

_main_ctx = None

Definition at line 187 of file z3py.py.

tuple _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)

Definition at line 126 of file z3py.py.

tuple sat = CheckSatResult(Z3_L_TRUE)

Definition at line 5711 of file z3py.py.

tuple unknown = CheckSatResult(Z3_L_UNDEF)

Definition at line 5713 of file z3py.py.

tuple unsat = CheckSatResult(Z3_L_FALSE)

Definition at line 5712 of file z3py.py.