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

Variables

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

Function Documentation

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

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

Definition at line 1468 of file z3py.py.

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

1469 def And(*args):
1470  """Create a Z3 and-expression or and-probe.
1471 
1472  >>> p, q, r = Bools('p q r')
1473  >>> And(p, q, r)
1474  And(p, q, r)
1475  >>> P = BoolVector('p', 5)
1476  >>> And(P)
1477  And(p__0, p__1, p__2, p__3, p__4)
1478  """
1479  last_arg = None
1480  if len(args) > 0:
1481  last_arg = args[len(args)-1]
1482  if isinstance(last_arg, Context):
1483  ctx = args[len(args)-1]
1484  args = args[:len(args)-1]
1485  else:
1486  ctx = main_ctx()
1487  args = _get_args(args)
1488  ctx_args = _ctx_from_ast_arg_list(args, ctx)
1489  if __debug__:
1490  _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
1491  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1492  if _has_probe(args):
1493  return _probe_and(args, ctx)
1494  else:
1495  args = _coerce_expr_list(args, ctx)
1496  _args, sz = _to_ast_array(args)
1497  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
def And
Definition: z3py.py:1468
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 main_ctx
Definition: z3py.py:188
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().

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

4468 def args2params(arguments, keywords, ctx=None):
4469  """Convert python arguments into a Z3_params object.
4470  A ':' is added to the keywords, and '_' is replaced with '-'
4471 
4472  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
4473  (params model true relevancy 2 elim_and true)
4474  """
4475  if __debug__:
4476  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
4477  prev = None
4478  r = ParamsRef(ctx)
4479  for a in arguments:
4480  if prev == None:
4481  prev = a
4482  else:
4483  r.set(prev, a)
4484  prev = None
4485  for k in keywords:
4486  v = keywords[k]
4487  r.set(k, v)
4488  return r
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().

3977 def Array(name, dom, rng):
3978  """Return an array constant named `name` with the given domain and range sorts.
3979 
3980  >>> a = Array('a', IntSort(), IntSort())
3981  >>> a.sort()
3982  Array(Int, Int)
3983  >>> a[0]
3984  a[0]
3985  """
3986  s = ArraySort(dom, rng)
3987  ctx = s.ctx
3988  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
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
Definition: z3py.py:3976
def ArraySort
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().

3956 def ArraySort(d, r):
3957  """Return the Z3 array sort with the given domain and range sorts.
3958 
3959  >>> A = ArraySort(IntSort(), BoolSort())
3960  >>> A
3961  Array(Int, Bool)
3962  >>> A.domain()
3963  Int
3964  >>> A.range()
3965  Bool
3966  >>> AA = ArraySort(IntSort(), A)
3967  >>> AA
3968  Array(Int, Array(Int, Bool))
3969  """
3970  if __debug__:
3971  _z3_assert(is_sort(d), "Z3 sort expected")
3972  _z3_assert(is_sort(r), "Z3 sort expected")
3973  _z3_assert(d.ctx == r.ctx, "Context mismatch")
3974  ctx = d.ctx
3975  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
def ArraySort
Definition: z3py.py:3955
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
Definition: z3py.py:532
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.

7369 def binary_interpolant(a,b,p=None,ctx=None):
7370  """Compute an interpolant for a binary conjunction.
7371 
7372  If a & b is unsatisfiable, returns an interpolant for a & b.
7373  This is a formula phi such that
7374 
7375  1) a implies phi
7376  2) b implies not phi
7377  3) All the uninterpreted symbols of phi occur in both a and b.
7378 
7379  If a & b is satisfiable, raises an object of class ModelRef
7380  that represents a model of a &b.
7381 
7382  If parameters p are supplied, these are used in creating the
7383  solver that determines satisfiability.
7384 
7385  x = Int('x')
7386  print binary_interpolant(x<0,x>2)
7387  Not(x >= 0)
7388  """
7389  f = And(Interpolant(a),b)
7390  return tree_interpolant(f,p,ctx)[0]
def And
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().

3466 def BitVec(name, bv, ctx=None):
3467  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3468  If `ctx=None`, then the global context is used.
3469 
3470  >>> x = BitVec('x', 16)
3471  >>> is_bv(x)
3472  True
3473  >>> x.size()
3474  16
3475  >>> x.sort()
3476  BitVec(16)
3477  >>> word = BitVecSort(16)
3478  >>> x2 = BitVec('x', word)
3479  >>> eq(x, x2)
3480  True
3481  """
3482  if isinstance(bv, BitVecSortRef):
3483  ctx = bv.ctx
3484  else:
3485  ctx = _get_ctx(ctx)
3486  bv = BitVecSort(bv, ctx)
3487  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
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().

3489 def BitVecs(names, bv, ctx=None):
3490  """Return a tuple of bit-vector constants of size bv.
3491 
3492  >>> x, y, z = BitVecs('x y z', 16)
3493  >>> x.size()
3494  16
3495  >>> x.sort()
3496  BitVec(16)
3497  >>> Sum(x, y, z)
3498  0 + x + y + z
3499  >>> Product(x, y, z)
3500  1*x*y*z
3501  >>> simplify(Product(x, y, z))
3502  x*y*z
3503  """
3504  ctx = _get_ctx(ctx)
3505  if isinstance(names, str):
3506  names = names.split(" ")
3507  return [BitVec(name, bv, ctx) for name in names]
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().

3436 def BitVecSort(sz, ctx=None):
3437  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3438 
3439  >>> Byte = BitVecSort(8)
3440  >>> Word = BitVecSort(16)
3441  >>> Byte
3442  BitVec(8)
3443  >>> x = Const('x', Byte)
3444  >>> eq(x, BitVec('x', 8))
3445  True
3446  """
3447  ctx = _get_ctx(ctx)
3448  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
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().

3450 def BitVecVal(val, bv, ctx=None):
3451  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3452 
3453  >>> v = BitVecVal(10, 32)
3454  >>> v
3455  10
3456  >>> print("0x%.8x" % v.as_long())
3457  0x0000000a
3458  """
3459  if is_bv_sort(bv):
3460  ctx = bv.ctx
3461  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3462  else:
3463  ctx = _get_ctx(ctx)
3464  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
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
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().

1361 def Bool(name, ctx=None):
1362  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1363 
1364  >>> p = Bool('p')
1365  >>> q = Bool('q')
1366  >>> And(p, q)
1367  And(p, q)
1368  """
1369  ctx = _get_ctx(ctx)
1370  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
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().

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

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

1343 def BoolVal(val, ctx=None):
1344  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1345 
1346  >>> BoolVal(True)
1347  True
1348  >>> is_true(BoolVal(True))
1349  True
1350  >>> is_true(True)
1351  False
1352  >>> is_false(BoolVal(False))
1353  True
1354  """
1355  ctx = _get_ctx(ctx)
1356  if val == False:
1357  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1358  else:
1359  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
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().

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

3418 def BV2Int(a):
3419  """Return the Z3 expression BV2Int(a).
3420 
3421  >>> b = BitVec('b', 3)
3422  >>> BV2Int(b).sort()
3423  Int
3424  >>> x = Int('x')
3425  >>> x > BV2Int(b)
3426  x > BV2Int(b)
3427  >>> solve(x > BV2Int(b), b == 1, x < 3)
3428  [b = 1, x = 2]
3429  """
3430  if __debug__:
3431  _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
3432  ctx = a.ctx
3433  ## investigate problem with bv2int
3434  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
def BV2Int
Definition: z3py.py:3417
def is_bv
Definition: z3py.py:3390
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 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.

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

3509 def Concat(*args):
3510  """Create a Z3 bit-vector concatenation expression.
3511 
3512  >>> v = BitVecVal(1, 4)
3513  >>> Concat(v, v+1, v)
3514  Concat(Concat(1, 1 + 1), 1)
3515  >>> simplify(Concat(v, v+1, v))
3516  289
3517  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3518  121
3519  """
3520  args = _get_args(args)
3521  if __debug__:
3522  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
3523  _z3_assert(len(args) >= 2, "At least two arguments expected.")
3524  ctx = args[0].ctx
3525  r = args[0]
3526  for i in range(len(args) - 1):
3527  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3528  return r
def is_bv
Definition: z3py.py:3390
def Concat
Definition: z3py.py:3508
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 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().

6941 def Cond(p, t1, t2, ctx=None):
6942  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
6943 
6944  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
6945  """
6946  p = _to_probe(p, ctx)
6947  t1 = _to_tactic(t1, ctx)
6948  t2 = _to_tactic(t2, ctx)
6949  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
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().

1135 def Const(name, sort):
1136  """Create a constant of the given sort.
1137 
1138  >>> Const('x', IntSort())
1139  x
1140  """
1141  if __debug__:
1142  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1143  ctx = sort.ctx
1144  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
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
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().

1146 def Consts(names, sort):
1147  """Create a several constants of the given sort.
1148 
1149  `names` is a string containing the names of all constants to be created.
1150  Blank spaces separate the names of different constants.
1151 
1152  >>> x, y, z = Consts('x y z', IntSort())
1153  >>> x + y + z
1154  x + y + z
1155  """
1156  if isinstance(names, str):
1157  names = names.split(" ")
1158  return [Const(name, sort) for name in names]
def Consts
Definition: z3py.py:1145
def Const
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 def CreateDatatypes(*ds):
4211  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4212 
4213  In the following example we define a Tree-List using two mutually recursive datatypes.
4214 
4215  >>> TreeList = Datatype('TreeList')
4216  >>> Tree = Datatype('Tree')
4217  >>> # Tree has two constructors: leaf and node
4218  >>> Tree.declare('leaf', ('val', IntSort()))
4219  >>> # a node contains a list of trees
4220  >>> Tree.declare('node', ('children', TreeList))
4221  >>> TreeList.declare('nil')
4222  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4223  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4224  >>> Tree.val(Tree.leaf(10))
4225  val(leaf(10))
4226  >>> simplify(Tree.val(Tree.leaf(10)))
4227  10
4228  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4229  >>> n1
4230  node(cons(leaf(10), cons(leaf(20), nil)))
4231  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4232  >>> simplify(n2 == n1)
4233  False
4234  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4235  True
4236  """
4237  ds = _get_args(ds)
4238  if __debug__:
4239  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4240  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
4241  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
4242  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
4243  ctx = ds[0].ctx
4244  num = len(ds)
4245  names = (Symbol * num)()
4246  out = (Sort * num)()
4247  clists = (ConstructorList * num)()
4248  to_delete = []
4249  for i in range(num):
4250  d = ds[i]
4251  names[i] = to_symbol(d.name, ctx)
4252  num_cs = len(d.constructors)
4253  cs = (Constructor * num_cs)()
4254  for j in range(num_cs):
4255  c = d.constructors[j]
4256  cname = to_symbol(c[0], ctx)
4257  rname = to_symbol(c[1], ctx)
4258  fs = c[2]
4259  num_fs = len(fs)
4260  fnames = (Symbol * num_fs)()
4261  sorts = (Sort * num_fs)()
4262  refs = (ctypes.c_uint * num_fs)()
4263  for k in range(num_fs):
4264  fname = fs[k][0]
4265  ftype = fs[k][1]
4266  fnames[k] = to_symbol(fname, ctx)
4267  if isinstance(ftype, Datatype):
4268  if __debug__:
4269  _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4270  sorts[k] = None
4271  refs[k] = ds.index(ftype)
4272  else:
4273  if __debug__:
4274  _z3_assert(is_sort(ftype), "Z3 sort expected")
4275  sorts[k] = ftype.ast
4276  refs[k] = 0
4277  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4278  to_delete.append(ScopedConstructor(cs[j], ctx))
4279  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4280  to_delete.append(ScopedConstructorList(clists[i], ctx))
4281  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4282  result = []
4283  ## Create a field for every constructor, recognizer and accessor
4284  for i in range(num):
4285  dref = DatatypeSortRef(out[i], ctx)
4286  num_cs = dref.num_constructors()
4287  for j in range(num_cs):
4288  cref = dref.constructor(j)
4289  cref_name = cref.name()
4290  cref_arity = cref.arity()
4291  if cref.arity() == 0:
4292  cref = cref()
4293  setattr(dref, cref_name, cref)
4294  rref = dref.recognizer(j)
4295  setattr(dref, rref.name(), rref)
4296  for k in range(cref_arity):
4297  aref = dref.accessor(j, k)
4298  setattr(dref, aref.name(), aref)
4299  result.append(dref)
4300  return tuple(result)
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.
def CreateDatatypes
Definition: z3py.py:4209
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 is_sort
Definition: z3py.py:532
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().

564 def DeclareSort(name, ctx=None):
565  """Create a new uninterpred sort named `name`.
566 
567  If `ctx=None`, then the new sort is declared in the global Z3Py context.
568 
569  >>> A = DeclareSort('A')
570  >>> a = Const('a', A)
571  >>> b = Const('b', A)
572  >>> a.sort() == A
573  True
574  >>> b.sort() == A
575  True
576  >>> a == b
577  a == b
578  """
579  ctx = _get_ctx(ctx)
580  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
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 def describe_probes():
6872  """Display a (tabular) description of all available probes in Z3."""
6873  if in_html_mode():
6874  even = True
6875  print('<table border="1" cellpadding="2" cellspacing="0">')
6876  for p in probes():
6877  if even:
6878  print('<tr style="background-color:#CFCFCF">')
6879  even = False
6880  else:
6881  print('<tr>')
6882  even = True
6883  print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
6884  print('</table>')
6885  else:
6886  for p in probes():
6887  print('%s : %s' % (p, probe_description(p)))
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 def describe_tactics():
6684  """Display a (tabular) description of all available tactics in Z3."""
6685  if in_html_mode():
6686  even = True
6687  print('<table border="1" cellpadding="2" cellspacing="0">')
6688  for t in tactics():
6689  if even:
6690  print('<tr style="background-color:#CFCFCF">')
6691  even = False
6692  else:
6693  print('<tr>')
6694  even = True
6695  print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
6696  print('</table>')
6697  else:
6698  for t in tactics():
6699  print('%s : %s' % (t, tactic_description(t)))
def tactic_description
Definition: z3py.py:6674
def describe_tactics
Definition: z3py.py:6682
def tactics
Definition: z3py.py:6664
def z3py.disable_trace (   msg)

Definition at line 61 of file z3py.py.

61 
62 def disable_trace(msg):
63  Z3_disable_trace(msg)
def disable_trace
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.

1104 def Distinct(*args):
1105  """Create a Z3 distinct expression.
1106 
1107  >>> x = Int('x')
1108  >>> y = Int('y')
1109  >>> Distinct(x, y)
1110  x != y
1111  >>> z = Int('z')
1112  >>> Distinct(x, y, z)
1113  Distinct(x, y, z)
1114  >>> simplify(Distinct(x, y, z))
1115  Distinct(x, y, z)
1116  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1117  And(Not(x == y), Not(x == z), Not(y == z))
1118  """
1119  args = _get_args(args)
1120  ctx = _ctx_from_ast_arg_list(args)
1121  if __debug__:
1122  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
1123  args = _coerce_expr_list(args, ctx)
1124  _args, sz = _to_ast_array(args)
1125  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
def Distinct
Definition: z3py.py:1103
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 z3py.enable_trace (   msg)

Definition at line 58 of file z3py.py.

58 
59 def enable_trace(msg):
60  Z3_enable_trace(msg)
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
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().

4399 def EnumSort(name, values, ctx=None):
4400  """Return a new enumeration sort named `name` containing the given values.
4401 
4402  The result is a pair (sort, list of constants).
4403  Example:
4404  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
4405  """
4406  if __debug__:
4407  _z3_assert(isinstance(name, str), "Name must be a string")
4408  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
4409  _z3_assert(len(values) > 0, "At least one value expected")
4410  ctx = _get_ctx(ctx)
4411  num = len(values)
4412  _val_names = (Symbol * num)()
4413  for i in range(num):
4414  _val_names[i] = to_symbol(values[i])
4415  _values = (FuncDecl * num)()
4416  _testers = (FuncDecl * num)()
4417  name = to_symbol(name)
4418  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
4419  V = []
4420  for i in range(num):
4421  V.append(FuncDeclRef(_values[i], ctx))
4422  V = [a() for a in V]
4423  return S, V
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().

373 def eq(a, b):
374  """Return `True` if `a` and `b` are structurally identical AST nodes.
375 
376  >>> x = Int('x')
377  >>> y = Int('y')
378  >>> eq(x, y)
379  False
380  >>> eq(x + 1, x + 1)
381  True
382  >>> eq(x + 1, 1 + x)
383  False
384  >>> eq(simplify(x + 1), simplify(1 + x))
385  True
386  """
387  if __debug__:
388  _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
389  return a.eq(b)
def is_ast
Definition: z3py.py:352
def eq
Definition: z3py.py:372
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().

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

3530 def Extract(high, low, a):
3531  """Create a Z3 bit-vector extraction expression.
3532 
3533  >>> x = BitVec('x', 8)
3534  >>> Extract(6, 2, x)
3535  Extract(6, 2, x)
3536  >>> Extract(6, 2, x).sort()
3537  BitVec(5)
3538  """
3539  if __debug__:
3540  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3541  _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
3542  _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
3543  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
def is_bv
Definition: z3py.py:3390
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 Extract
Definition: z3py.py:3529
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.

6904 def FailIf(p, ctx=None):
6905  """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6906 
6907  In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
6908 
6909  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
6910  >>> x, y = Ints('x y')
6911  >>> g = Goal()
6912  >>> g.add(x > 0)
6913  >>> g.add(y > 0)
6914  >>> t(g)
6915  [[x > 0, y > 0]]
6916  >>> g.add(x == y + 1)
6917  >>> t(g)
6918  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6919  """
6920  p = _to_probe(p, ctx)
6921  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
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().

1790 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1791  """Create a Z3 forall formula.
1792 
1793  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
1794 
1795  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1796 
1797  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1798  >>> x = Int('x')
1799  >>> y = Int('y')
1800  >>> ForAll([x, y], f(x, y) >= x)
1801  ForAll([x, y], f(x, y) >= x)
1802  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
1803  ForAll([x, y], f(x, y) >= x)
1804  >>> ForAll([x, y], f(x, y) >= x, weight=10)
1805  ForAll([x, y], f(x, y) >= x)
1806  """
1807  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
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.

1401 def FreshBool(prefix='b', ctx=None):
1402  """Return a fresh Boolean constant in the given context using the given prefix.
1403 
1404  If `ctx=None`, then the global context is used.
1405 
1406  >>> b1 = FreshBool()
1407  >>> b2 = FreshBool()
1408  >>> eq(b1, b2)
1409  False
1410  """
1411  ctx = _get_ctx(ctx)
1412  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
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.

2753 def FreshInt(prefix='x', ctx=None):
2754  """Return a fresh integer constant in the given context using the given prefix.
2755 
2756  >>> x = FreshInt()
2757  >>> y = FreshInt()
2758  >>> eq(x, y)
2759  False
2760  >>> x.sort()
2761  Int
2762  """
2763  ctx = _get_ctx(ctx)
2764  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
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.

2805 def FreshReal(prefix='b', ctx=None):
2806  """Return a fresh real constant in the given context using the given prefix.
2807 
2808  >>> x = FreshReal()
2809  >>> y = FreshReal()
2810  >>> eq(x, y)
2811  False
2812  >>> x.sort()
2813  Real
2814  """
2815  ctx = _get_ctx(ctx)
2816  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
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().

702 def Function(name, *sig):
703  """Create a new Z3 uninterpreted function with the given sorts.
704 
705  >>> f = Function('f', IntSort(), IntSort())
706  >>> f(f(0))
707  f(f(0))
708  """
709  sig = _get_args(sig)
710  if __debug__:
711  _z3_assert(len(sig) > 0, "At least two arguments expected")
712  arity = len(sig) - 1
713  rng = sig[arity]
714  if __debug__:
715  _z3_assert(is_sort(rng), "Z3 sort expected")
716  dom = (Sort * arity)()
717  for i in range(arity):
718  if __debug__:
719  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
720  dom[i] = sig[i].ast
721  ctx = rng.ctx
722  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
Function Declarations.
Definition: z3py.py:587
def Function
Definition: z3py.py:701
def is_sort
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 def get_as_array_func(n):
5535  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
5536  if __debug__:
5537  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
5538  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
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
Definition: z3py.py:5533
def is_as_array
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 def get_map_func(a):
3940  """Return the function declaration associated with a Z3 map array expression.
3941 
3942  >>> f = Function('f', IntSort(), IntSort())
3943  >>> b = Array('b', IntSort(), IntSort())
3944  >>> a = Map(f, b)
3945  >>> eq(f, get_map_func(a))
3946  True
3947  >>> get_map_func(a)
3948  f
3949  >>> get_map_func(a)(0)
3950  f(0)
3951  """
3952  if __debug__:
3953  _z3_assert(is_map(a), "Z3 array map expression expected.")
3954  return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
Function Declarations.
Definition: z3py.py:587
def is_map
Definition: z3py.py:3923
def get_map_func
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.

248 def get_param(name):
249  """Return the value of a Z3 global (or module) parameter
250 
251  >>> get_param('nlsat.reorder')
252  'true'
253  """
254  ptr = (ctypes.c_char_p * 1)()
255  if Z3_global_param_get(str(name), ptr):
256  r = z3core._to_pystr(ptr[0])
257  return r
258  raise Z3Exception("failed to retrieve value for '%s'" % name)
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
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 def get_var_index(a):
1039  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1040 
1041  >>> x = Int('x')
1042  >>> y = Int('y')
1043  >>> is_var(x)
1044  False
1045  >>> is_const(x)
1046  True
1047  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1048  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1049  >>> q = ForAll([x, y], f(x, y) == x + y)
1050  >>> q.body()
1051  f(Var(1), Var(0)) == Var(1) + Var(0)
1052  >>> b = q.body()
1053  >>> b.arg(0)
1054  f(Var(1), Var(0))
1055  >>> v1 = b.arg(0).arg(0)
1056  >>> v2 = b.arg(0).arg(1)
1057  >>> v1
1058  Var(1)
1059  >>> v2
1060  Var(0)
1061  >>> get_var_index(v1)
1062  1
1063  >>> get_var_index(v2)
1064  0
1065  """
1066  if __debug__:
1067  _z3_assert(is_var(a), "Z3 bound variable expected")
1068  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
def is_var
Definition: z3py.py:1013
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
Definition: z3py.py:1037
def z3py.get_version ( )

Definition at line 72 of file z3py.py.

72 
73 def get_version():
74  major = ctypes.c_uint(0)
75  minor = ctypes.c_uint(0)
76  build = ctypes.c_uint(0)
77  rev = ctypes.c_uint(0)
78  Z3_get_version(major, minor, build, rev)
79  return (major.value, minor.value, build.value, rev.value)
80 
81 # We use _z3_assert instead of the assert command because we want to
# 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.

64 
65 def get_version_string():
66  major = ctypes.c_uint(0)
67  minor = ctypes.c_uint(0)
68  build = ctypes.c_uint(0)
69  rev = ctypes.c_uint(0)
70  Z3_get_version(major, minor, build, rev)
71  return "%s.%s.%s" % (major.value, minor.value, build.value)
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_string
Definition: z3py.py:64
def z3py.help_simplify ( )
Return a string describing all options available for Z3 `simplify` procedure.

Definition at line 6980 of file z3py.py.

6981 def help_simplify():
6982  """Return a string describing all options available for Z3 `simplify` procedure."""
6983  print(Z3_simplify_get_help(main_ctx().ref()))
def main_ctx
Definition: z3py.py:188
Z3_string Z3_API Z3_simplify_get_help(__in Z3_context c)
Return a string describing all available parameters.
def help_simplify
Definition: z3py.py:6980
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.

1082 def If(a, b, c, ctx=None):
1083  """Create a Z3 if-then-else expression.
1084 
1085  >>> x = Int('x')
1086  >>> y = Int('y')
1087  >>> max = If(x > y, x, y)
1088  >>> max
1089  If(x > y, x, y)
1090  >>> simplify(max)
1091  If(x <= y, y, x)
1092  """
1093  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1094  return Cond(a, b, c, ctx)
1095  else:
1096  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1097  s = BoolSort(ctx)
1098  a = s.cast(a)
1099  b, c = _coerce_exprs(b, c, ctx)
1100  if __debug__:
1101  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1102  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
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().

1414 def Implies(a, b, ctx=None):
1415  """Create a Z3 implies expression.
1416 
1417  >>> p, q = Bools('p q')
1418  >>> Implies(p, q)
1419  Implies(p, q)
1420  >>> simplify(Implies(p, q))
1421  Or(Not(p), q)
1422  """
1423  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1424  s = BoolSort(ctx)
1425  a = s.cast(a)
1426  b = s.cast(b)
1427  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
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().

2718 def Int(name, ctx=None):
2719  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
2720 
2721  >>> x = Int('x')
2722  >>> is_int(x)
2723  True
2724  >>> is_int(x + 1)
2725  True
2726  """
2727  ctx = _get_ctx(ctx)
2728  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
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().

7296 def Interpolant(a,ctx=None):
7297  """Create an interpolation operator.
7298 
7299  The argument is an interpolation pattern (see tree_interpolant).
7300 
7301  >>> x = Int('x')
7302  >>> print Interpolant(x>0)
7303  interp(x > 0)
7304  """
7305  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
7306  s = BoolSort(ctx)
7307  a = s.cast(a)
7308  return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
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().

2730 def Ints(names, ctx=None):
2731  """Return a tuple of Integer constants.
2732 
2733  >>> x, y, z = Ints('x y z')
2734  >>> Sum(x, y, z)
2735  x + y + z
2736  """
2737  ctx = _get_ctx(ctx)
2738  if isinstance(names, str):
2739  names = names.split(" ")
2740  return [Int(name, ctx) for name in names]
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().

2615 def IntSort(ctx=None):
2616  """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
2617 
2618  >>> IntSort()
2619  Int
2620  >>> x = Const('x', IntSort())
2621  >>> is_int(x)
2622  True
2623  >>> x.sort() == IntSort()
2624  True
2625  >>> x.sort() == BoolSort()
2626  False
2627  """
2628  ctx = _get_ctx(ctx)
2629  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
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().

2662 def IntVal(val, ctx=None):
2663  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
2664 
2665  >>> IntVal(1)
2666  1
2667  >>> IntVal("100")
2668  100
2669  """
2670  ctx = _get_ctx(ctx)
2671  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
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.

2742 def IntVector(prefix, sz, ctx=None):
2743  """Return a list of integer constants of size `sz`.
2744 
2745  >>> X = IntVector('x', 3)
2746  >>> X
2747  [x__0, x__1, x__2]
2748  >>> Sum(X)
2749  x__0 + x__1 + x__2
2750  """
2751  return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
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.

2319 def is_add(a):
2320  """Return `True` if `a` is an expression of the form b + c.
2321 
2322  >>> x, y = Ints('x y')
2323  >>> is_add(x + y)
2324  True
2325  >>> is_add(x - y)
2326  False
2327  """
2328  return is_app_of(a, Z3_OP_ADD)
def is_add
Definition: z3py.py:2318
def is_app_of
Definition: z3py.py:1069
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 def is_algebraic_value(a):
2307  """Return `True` if `a` is an algerbraic value of sort Real.
2308 
2309  >>> is_algebraic_value(RealVal("3/5"))
2310  False
2311  >>> n = simplify(Sqrt(2))
2312  >>> n
2313  1.4142135623?
2314  >>> is_algebraic_value(n)
2315  True
2316  """
2317  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
def is_arith
Definition: z3py.py:2199
def is_algebraic_value
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.

1273 def is_and(a):
1274  """Return `True` if `a` is a Z3 and expression.
1275 
1276  >>> p, q = Bools('p q')
1277  >>> is_and(And(p, q))
1278  True
1279  >>> is_and(Or(p, q))
1280  False
1281  """
1282  return is_app_of(a, Z3_OP_AND)
def is_and
Definition: z3py.py:1272
def is_app_of
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().

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

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

2200 def is_arith(a):
2201  """Return `True` if `a` is an arithmetical expression.
2202 
2203  >>> x = Int('x')
2204  >>> is_arith(x)
2205  True
2206  >>> is_arith(x + 1)
2207  True
2208  >>> is_arith(1)
2209  False
2210  >>> is_arith(IntVal(1))
2211  True
2212  >>> y = Real('y')
2213  >>> is_arith(y)
2214  True
2215  >>> is_arith(y + 1)
2216  True
2217  """
2218  return isinstance(a, ArithRef)
def is_arith
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 def is_arith_sort(s):
1904  """Return `True` if s is an arithmetical sort (type).
1905 
1906  >>> is_arith_sort(IntSort())
1907  True
1908  >>> is_arith_sort(RealSort())
1909  True
1910  >>> is_arith_sort(BoolSort())
1911  False
1912  >>> n = Int('x') + 1
1913  >>> is_arith_sort(n.sort())
1914  True
1915  """
1916  return isinstance(s, ArithSortRef)
def is_arith_sort
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.

3887 def is_array(a):
3888  """Return `True` if `a` is a Z3 array expression.
3889 
3890  >>> a = Array('a', IntSort(), IntSort())
3891  >>> is_array(a)
3892  True
3893  >>> is_array(Store(a, 0, 1))
3894  True
3895  >>> is_array(a[0])
3896  False
3897  """
3898  return isinstance(a, ArrayRef)
def is_array
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 def is_as_array(n):
5531  """Return true if n is a Z3 expression of the form (_ as-array f)."""
5532  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
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
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().

353 def is_ast(a):
354  """Return `True` if `a` is an AST node.
355 
356  >>> is_ast(10)
357  False
358  >>> is_ast(IntVal(10))
359  True
360  >>> is_ast(Int('x'))
361  True
362  >>> is_ast(BoolSort())
363  True
364  >>> is_ast(Function('f', IntSort(), IntSort()))
365  True
366  >>> is_ast("x")
367  False
368  >>> is_ast(Solver())
369  False
370  """
371  return isinstance(a, AstRef)
def is_ast
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().

1226 def is_bool(a):
1227  """Return `True` if `a` is a Z3 Boolean expression.
1228 
1229  >>> p = Bool('p')
1230  >>> is_bool(p)
1231  True
1232  >>> q = Bool('q')
1233  >>> is_bool(And(p, q))
1234  True
1235  >>> x = Real('x')
1236  >>> is_bool(x)
1237  False
1238  >>> is_bool(x == 0)
1239  True
1240  """
1241  return isinstance(a, BoolRef)
def is_bool
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().

3391 def is_bv(a):
3392  """Return `True` if `a` is a Z3 bit-vector expression.
3393 
3394  >>> b = BitVec('b', 32)
3395  >>> is_bv(b)
3396  True
3397  >>> is_bv(b + 10)
3398  True
3399  >>> is_bv(Int('x'))
3400  False
3401  """
3402  return isinstance(a, BitVecRef)
def is_bv
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().

2930 def is_bv_sort(s):
2931  """Return True if `s` is a Z3 bit-vector sort.
2932 
2933  >>> is_bv_sort(BitVecSort(32))
2934  True
2935  >>> is_bv_sort(IntSort())
2936  False
2937  """
2938  return isinstance(s, BitVecSortRef)
def is_bv_sort
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 def is_bv_value(a):
3405  """Return `True` if `a` is a Z3 bit-vector numeral value.
3406 
3407  >>> b = BitVec('b', 32)
3408  >>> is_bv_value(b)
3409  False
3410  >>> b = BitVecVal(10, 32)
3411  >>> b
3412  10
3413  >>> is_bv_value(b)
3414  True
3415  """
3416  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
def is_bv
Definition: z3py.py:3390
def is_bv_value
Definition: z3py.py:3403
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().

996 def is_const(a):
997  """Return `True` if `a` is Z3 constant/variable expression.
998 
999  >>> a = Int('a')
1000  >>> is_const(a)
1001  True
1002  >>> is_const(a + 1)
1003  False
1004  >>> is_const(1)
1005  False
1006  >>> is_const(IntVal(1))
1007  True
1008  >>> x = Int('x')
1009  >>> is_const(ForAll(x, x >= 0))
1010  False
1011  """
1012  return is_app(a) and a.num_args() == 0
def is_const
Definition: z3py.py:995
def is_app
Definition: z3py.py:970
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 def is_const_array(a):
3901  """Return `True` if `a` is a Z3 constant array.
3902 
3903  >>> a = K(IntSort(), 10)
3904  >>> is_const_array(a)
3905  True
3906  >>> a = Array('a', IntSort(), IntSort())
3907  >>> is_const_array(a)
3908  False
3909  """
3910  return is_app_of(a, Z3_OP_CONST_ARRAY)
def is_app_of
Definition: z3py.py:1069
def is_const_array
Definition: z3py.py:3899
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 def is_distinct(a):
1316  """Return `True` if `a` is a Z3 distinct expression.
1317 
1318  >>> x, y, z = Ints('x y z')
1319  >>> is_distinct(x == y)
1320  False
1321  >>> is_distinct(Distinct(x, y, z))
1322  True
1323  """
1324  return is_app_of(a, Z3_OP_DISTINCT)
def is_distinct
Definition: z3py.py:1314
def is_app_of
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.

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

1306 def is_eq(a):
1307  """Return `True` if `a` is a Z3 equality expression.
1308 
1309  >>> x, y = Ints('x y')
1310  >>> is_eq(x == y)
1311  True
1312  """
1313  return is_app_of(a, Z3_OP_EQ)
def is_eq
Definition: z3py.py:1305
def is_app_of
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().

951 def is_expr(a):
952  """Return `True` if `a` is a Z3 expression.
953 
954  >>> a = Int('a')
955  >>> is_expr(a)
956  True
957  >>> is_expr(a + 1)
958  True
959  >>> is_expr(IntSort())
960  False
961  >>> is_expr(1)
962  False
963  >>> is_expr(IntVal(1))
964  True
965  >>> x = Int('x')
966  >>> is_expr(ForAll(x, x >= 0))
967  True
968  """
969  return isinstance(a, ExprRef)
def is_expr
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().

1260 def is_false(a):
1261  """Return `True` if `a` is the Z3 false expression.
1262 
1263  >>> p = Bool('p')
1264  >>> is_false(p)
1265  False
1266  >>> is_false(False)
1267  False
1268  >>> is_false(BoolVal(False))
1269  True
1270  """
1271  return is_app_of(a, Z3_OP_FALSE)
def is_false
Definition: z3py.py:1259
def is_app_of
Definition: z3py.py:1069
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 def is_func_decl(a):
691  """Return `True` if `a` is a Z3 function declaration.
692 
693  >>> f = Function('f', IntSort(), IntSort())
694  >>> is_func_decl(f)
695  True
696  >>> x = Real('x')
697  >>> is_func_decl(x)
698  False
699  """
700  return isinstance(a, FuncDeclRef)
def is_func_decl
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.

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

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

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

2220 def is_int(a):
2221  """Return `True` if `a` is an integer expression.
2222 
2223  >>> x = Int('x')
2224  >>> is_int(x + 1)
2225  True
2226  >>> is_int(1)
2227  False
2228  >>> is_int(IntVal(1))
2229  True
2230  >>> y = Real('y')
2231  >>> is_int(y)
2232  False
2233  >>> is_int(y + 1)
2234  False
2235  """
2236  return is_arith(a) and a.is_int()
def is_arith
Definition: z3py.py:2199
def is_int
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 def is_int_value(a):
2263  """Return `True` if `a` is an integer value of sort Int.
2264 
2265  >>> is_int_value(IntVal(1))
2266  True
2267  >>> is_int_value(1)
2268  False
2269  >>> is_int_value(Int('x'))
2270  False
2271  >>> n = Int('x') + 1
2272  >>> n
2273  x + 1
2274  >>> n.arg(1)
2275  1
2276  >>> is_int_value(n.arg(1))
2277  True
2278  >>> is_int_value(RealVal("1/3"))
2279  False
2280  >>> is_int_value(RealVal(1))
2281  False
2282  """
2283  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
def is_int_value
Definition: z3py.py:2261
def is_arith
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.

2434 def is_is_int(a):
2435  """Return `True` if `a` is an expression of the form IsInt(b).
2436 
2437  >>> x = Real('x')
2438  >>> is_is_int(IsInt(x))
2439  True
2440  >>> is_is_int(x)
2441  False
2442  """
2443  return is_app_of(a, Z3_OP_IS_INT)
def is_is_int
Definition: z3py.py:2433
def is_app_of
Definition: z3py.py:1069
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.

3912 def is_K(a):
3913  """Return `True` if `a` is a Z3 constant array.
3914 
3915  >>> a = K(IntSort(), 10)
3916  >>> is_K(a)
3917  True
3918  >>> a = Array('a', IntSort(), IntSort())
3919  >>> is_K(a)
3920  False
3921  """
3922  return is_app_of(a, Z3_OP_CONST_ARRAY)
def is_app_of
Definition: z3py.py:1069
def is_K
Definition: z3py.py:3911
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.

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

2401 def is_lt(a):
2402  """Return `True` if `a` is an expression of the form b < c.
2403 
2404  >>> x, y = Ints('x y')
2405  >>> is_lt(x < y)
2406  True
2407  >>> is_lt(x == y)
2408  False
2409  """
2410  return is_app_of(a, Z3_OP_LT)
def is_lt
Definition: z3py.py:2400
def is_app_of
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().

3924 def is_map(a):
3925  """Return `True` if `a` is a Z3 map array expression.
3926 
3927  >>> f = Function('f', IntSort(), IntSort())
3928  >>> b = Array('b', IntSort(), IntSort())
3929  >>> a = Map(f, b)
3930  >>> a
3931  Map(f, b)
3932  >>> is_map(a)
3933  True
3934  >>> is_map(b)
3935  False
3936  """
3937  return is_app_of(a, Z3_OP_ARRAY_MAP)
def is_map
Definition: z3py.py:3923
def is_app_of
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.

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

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

1295 def is_not(a):
1296  """Return `True` if `a` is a Z3 not expression.
1297 
1298  >>> p = Bool('p')
1299  >>> is_not(p)
1300  False
1301  >>> is_not(Not(p))
1302  True
1303  """
1304  return is_app_of(a, Z3_OP_NOT)
def is_not
Definition: z3py.py:1294
def is_app_of
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.

1284 def is_or(a):
1285  """Return `True` if `a` is a Z3 or expression.
1286 
1287  >>> p, q = Bools('p q')
1288  >>> is_or(Or(p, q))
1289  True
1290  >>> is_or(And(p, q))
1291  False
1292  """
1293  return is_app_of(a, Z3_OP_OR)
def is_app_of
Definition: z3py.py:1069
def is_or
Definition: z3py.py:1283
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().

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

6837 def is_probe(p):
6838  """Return `True` if `p` is a Z3 probe.
6839 
6840  >>> is_probe(Int('x'))
6841  False
6842  >>> is_probe(Probe('memory'))
6843  True
6844  """
6845  return isinstance(p, Probe)
def is_probe
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 def is_quantifier(a):
1750  """Return `True` if `a` is a Z3 quantifier.
1751 
1752  >>> f = Function('f', IntSort(), IntSort())
1753  >>> x = Int('x')
1754  >>> q = ForAll(x, f(x) == 0)
1755  >>> is_quantifier(q)
1756  True
1757  >>> is_quantifier(f(x))
1758  False
1759  """
1760  return isinstance(a, QuantifierRef)
def is_quantifier
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 def is_rational_value(a):
2286  """Return `True` if `a` is rational value of sort Real.
2287 
2288  >>> is_rational_value(RealVal(1))
2289  True
2290  >>> is_rational_value(RealVal("3/5"))
2291  True
2292  >>> is_rational_value(IntVal(1))
2293  False
2294  >>> is_rational_value(1)
2295  False
2296  >>> n = Real('x') + 1
2297  >>> n.arg(1)
2298  1
2299  >>> is_rational_value(n.arg(1))
2300  True
2301  >>> is_rational_value(Real('x'))
2302  False
2303  """
2304  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
def is_arith
Definition: z3py.py:2199
def is_rational_value
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().

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

4084 def is_select(a):
4085  """Return `True` if `a` is a Z3 array select application.
4086 
4087  >>> a = Array('a', IntSort(), IntSort())
4088  >>> is_select(a)
4089  False
4090  >>> i = Int('i')
4091  >>> is_select(a[i])
4092  True
4093  """
4094  return is_app_of(a, Z3_OP_SELECT)
def is_select
Definition: z3py.py:4083
def is_app_of
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().

533 def is_sort(s):
534  """Return `True` if `s` is a Z3 sort.
535 
536  >>> is_sort(IntSort())
537  True
538  >>> is_sort(Int('x'))
539  False
540  >>> is_expr(Int('x'))
541  True
542  """
543  return isinstance(s, SortRef)
def is_sort
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.

4096 def is_store(a):
4097  """Return `True` if `a` is a Z3 array store application.
4098 
4099  >>> a = Array('a', IntSort(), IntSort())
4100  >>> is_store(a)
4101  False
4102  >>> is_store(Store(a, 0, 1))
4103  True
4104  """
4105  return is_app_of(a, Z3_OP_STORE)
def is_store
Definition: z3py.py:4095
def is_app_of
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.

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

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

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

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

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

2852 def IsInt(a):
2853  """ Return the Z3 predicate IsInt(a).
2854 
2855  >>> x = Real('x')
2856  >>> IsInt(x + "1/2")
2857  IsInt(x + 1/2)
2858  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
2859  [x = 1/2]
2860  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
2861  no solution
2862  """
2863  if __debug__:
2864  _z3_assert(a.is_real(), "Z3 real expression expected.")
2865  ctx = a.ctx
2866  return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
def IsInt
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().

4063 def K(dom, v):
4064  """Return a Z3 constant array expression.
4065 
4066  >>> a = K(IntSort(), 10)
4067  >>> a
4068  K(Int, 10)
4069  >>> a.sort()
4070  Array(Int, Int)
4071  >>> i = Int('i')
4072  >>> a[i]
4073  K(Int, 10)[i]
4074  >>> simplify(a[i])
4075  10
4076  """
4077  if __debug__:
4078  _z3_assert(is_sort(dom), "Z3 sort expected")
4079  ctx = dom.ctx
4080  if not is_expr(v):
4081  v = _py2expr(v, ctx)
4082  return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
def K
Definition: z3py.py:4062
def is_expr
Definition: z3py.py:950
def is_sort
Definition: z3py.py:532
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__().

3677 def LShR(a, b):
3678  """Create the Z3 expression logical right shift.
3679 
3680  Use the operator >> for the arithmetical right shift.
3681 
3682  >>> x, y = BitVecs('x y', 32)
3683  >>> LShR(x, y)
3684  LShR(x, y)
3685  >>> (x >> y).sexpr()
3686  '(bvashr x y)'
3687  >>> LShR(x, y).sexpr()
3688  '(bvlshr x y)'
3689  >>> BitVecVal(4, 3)
3690  4
3691  >>> BitVecVal(4, 3).as_signed_long()
3692  -4
3693  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3694  -2
3695  >>> simplify(BitVecVal(4, 3) >> 1)
3696  6
3697  >>> simplify(LShR(BitVecVal(4, 3), 1))
3698  2
3699  >>> simplify(BitVecVal(2, 3) >> 1)
3700  1
3701  >>> simplify(LShR(BitVecVal(2, 3), 1))
3702  1
3703  """
3704  _check_bv_args(a, b)
3705  a, b = _coerce_exprs(a, b)
3706  return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def LShR
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().

189 def main_ctx():
190  """Return a reference to the global Z3 context.
191 
192  >>> x = Real('x')
193  >>> x.ctx == main_ctx()
194  True
195  >>> c = Context()
196  >>> c == main_ctx()
197  False
198  >>> x2 = Real('x', c)
199  >>> x2.ctx == c
200  True
201  >>> eq(x, x2)
202  False
203  """
204  global _main_ctx
205  if _main_ctx == None:
206  _main_ctx = Context()
207  return _main_ctx
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().

4041 def Map(f, *args):
4042  """Return a Z3 map array expression.
4043 
4044  >>> f = Function('f', IntSort(), IntSort(), IntSort())
4045  >>> a1 = Array('a1', IntSort(), IntSort())
4046  >>> a2 = Array('a2', IntSort(), IntSort())
4047  >>> b = Map(f, a1, a2)
4048  >>> b
4049  Map(f, a1, a2)
4050  >>> prove(b[0] == f(a1[0], a2[0]))
4051  proved
4052  """
4053  args = _get_args(args)
4054  if __debug__:
4055  _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
4056  _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
4057  _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
4058  _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
4059  _args, sz = _to_ast_array(args)
4060  ctx = f.ctx
4061  return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
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
Definition: z3py.py:4040
def is_func_decl
Definition: z3py.py:689
def is_array
Definition: z3py.py:3886
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.

1565 def MultiPattern(*args):
1566  """Create a Z3 multi-pattern using the given expressions `*args`
1567 
1568  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1569 
1570  >>> f = Function('f', IntSort(), IntSort())
1571  >>> g = Function('g', IntSort(), IntSort())
1572  >>> x = Int('x')
1573  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1574  >>> q
1575  ForAll(x, f(x) != g(x))
1576  >>> q.num_patterns()
1577  1
1578  >>> is_pattern(q.pattern(0))
1579  True
1580  >>> q.pattern(0)
1581  MultiPattern(f(Var(0)), g(Var(0)))
1582  """
1583  if __debug__:
1584  _z3_assert(len(args) > 0, "At least one argument expected")
1585  _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
1586  ctx = args[0].ctx
1587  args, sz = _to_ast_array(args)
1588  return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
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 is_expr
Definition: z3py.py:950
def MultiPattern
Definition: z3py.py:1564
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().

1444 def Not(a, ctx=None):
1445  """Create a Z3 not expression or probe.
1446 
1447  >>> p = Bool('p')
1448  >>> Not(Not(p))
1449  Not(Not(p))
1450  >>> simplify(Not(Not(p)))
1451  p
1452  """
1453  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1454  if is_probe(a):
1455  # Not is also used to build probes
1456  return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1457  else:
1458  s = BoolSort(ctx)
1459  a = s.cast(a)
1460  return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
def Not
Definition: z3py.py:1443
def BoolSort
Definition: z3py.py:1325
def is_probe
Definition: z3py.py:6836
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 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 
87 def open_log(fname):
88  """Log interaction to a file. This function must be invoked immediately after init(). """
89  Z3_open_log(fname)
Z3_bool Z3_API Z3_open_log(__in Z3_string filename)
Log interaction to a file.
def open_log
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().

1499 def Or(*args):
1500  """Create a Z3 or-expression or or-probe.
1501 
1502  >>> p, q, r = Bools('p q r')
1503  >>> Or(p, q, r)
1504  Or(p, q, r)
1505  >>> P = BoolVector('p', 5)
1506  >>> Or(P)
1507  Or(p__0, p__1, p__2, p__3, p__4)
1508  """
1509  last_arg = None
1510  if len(args) > 0:
1511  last_arg = args[len(args)-1]
1512  if isinstance(last_arg, Context):
1513  ctx = args[len(args)-1]
1514  args = args[:len(args)-1]
1515  else:
1516  ctx = main_ctx()
1517  args = _get_args(args)
1518  ctx_args = _ctx_from_ast_arg_list(args, ctx)
1519  if __debug__:
1520  _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
1521  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1522  if _has_probe(args):
1523  return _probe_or(args, ctx)
1524  else:
1525  args = _coerce_expr_list(args, ctx)
1526  _args, sz = _to_ast_array(args)
1527  return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
def main_ctx
Definition: z3py.py:188
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 Or
Definition: z3py.py:1498
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.

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

6621 def ParAndThen(t1, t2, ctx=None):
6622  """Alias for ParThen(t1, t2, ctx)."""
6623  return ParThen(t1, t2, ctx)
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.

6589 def ParOr(*ts, **ks):
6590  """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
6591 
6592  >>> x = Int('x')
6593  >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
6594  >>> t(x + 1 == 2)
6595  [[x == 1]]
6596  """
6597  if __debug__:
6598  _z3_assert(len(ts) >= 2, "At least two arguments expected")
6599  ctx = _get_ctx(ks.get('ctx', None))
6600  ts = [ _to_tactic(t, ctx) for t in ts ]
6601  sz = len(ts)
6602  _args = (TacticObj * sz)()
6603  for i in range(sz):
6604  _args[i] = ts[i].tactic
6605  return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
def ParOr
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.

7286 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
7287  """Parse a file in SMT 2.0 format using the given sorts and decls.
7288 
7289  This function is similar to parse_smt2_string().
7290  """
7291  ctx = _get_ctx(ctx)
7292  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7293  dsz, dnames, ddecls = _dict2darray(decls, ctx)
7294  return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
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().

7266 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
7267  """Parse a string in SMT 2.0 format using the given sorts and decls.
7268 
7269  The arguments sorts and decls are Python dictionaries used to initialize
7270  the symbol table used for the SMT 2.0 parser.
7271 
7272  >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
7273  And(x > 0, x < 10)
7274  >>> x, y = Ints('x y')
7275  >>> f = Function('f', IntSort(), IntSort())
7276  >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
7277  x + f(y) > 0
7278  >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
7279  a > 0
7280  """
7281  ctx = _get_ctx(ctx)
7282  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7283  dsz, dnames, ddecls = _dict2darray(decls, ctx)
7284  return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
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().

6607 def ParThen(t1, t2, ctx=None):
6608  """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
6609 
6610  >>> x, y = Ints('x y')
6611  >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
6612  >>> t(And(Or(x == 1, x == 2), y == x + 1))
6613  [[x == 1, y == 2], [x == 2, y == 3]]
6614  """
6615  t1 = _to_tactic(t1, ctx)
6616  t2 = _to_tactic(t2, ctx)
6617  if __debug__:
6618  _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
6619  return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
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().

6863 def probe_description(name, ctx=None):
6864  """Return a short description for the probe named `name`.
6865 
6866  >>> d = probe_description('memory')
6867  """
6868  ctx = _get_ctx(ctx)
6869  return Z3_probe_get_descr(ctx.ref(), name)
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().

6853 def probes(ctx=None):
6854  """Return a list of all available probes in Z3.
6855 
6856  >>> l = probes()
6857  >>> l.count('memory') == 1
6858  True
6859  """
6860  ctx = _get_ctx(ctx)
6861  return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]
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().

7060 def Product(*args):
7061  """Create the product of the Z3 expressions.
7062 
7063  >>> a, b, c = Ints('a b c')
7064  >>> Product(a, b, c)
7065  a*b*c
7066  >>> Product([a, b, c])
7067  a*b*c
7068  >>> A = IntVector('a', 5)
7069  >>> Product(A)
7070  a__0*a__1*a__2*a__3*a__4
7071  """
7072  args = _get_args(args)
7073  if __debug__:
7074  _z3_assert(len(args) > 0, "Non empty list of arguments expected")
7075  ctx = _ctx_from_ast_arg_list(args)
7076  if __debug__:
7077  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
7078  args = _coerce_expr_list(args, ctx)
7079  if is_bv(args[0]):
7080  return _reduce(lambda a, b: a * b, args, 1)
7081  else:
7082  _args, sz = _to_ast_array(args)
7083  return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
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 is_bv
Definition: z3py.py:3390
def Product
Definition: z3py.py:7059
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().

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

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

2691 def RatVal(a, b, ctx=None):
2692  """Return a Z3 rational a/b.
2693 
2694  If `ctx=None`, then the global context is used.
2695 
2696  >>> RatVal(3,5)
2697  3/5
2698  >>> RatVal(3,5).sort()
2699  Real
2700  """
2701  if __debug__:
2702  _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
2703  _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
2704  return simplify(RealVal(a, ctx)/RealVal(b, ctx))
def simplify
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().

2766 def Real(name, ctx=None):
2767  """Return a real constant named `name`. If `ctx=None`, then the global context is used.
2768 
2769  >>> x = Real('x')
2770  >>> is_real(x)
2771  True
2772  >>> is_real(x + 1)
2773  True
2774  """
2775  ctx = _get_ctx(ctx)
2776  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
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().

2778 def Reals(names, ctx=None):
2779  """Return a tuple of real constants.
2780 
2781  >>> x, y, z = Reals('x y z')
2782  >>> Sum(x, y, z)
2783  x + y + z
2784  >>> Sum(x, y, z).sort()
2785  Real
2786  """
2787  ctx = _get_ctx(ctx)
2788  if isinstance(names, str):
2789  names = names.split(" ")
2790  return [Real(name, ctx) for name in names]
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().

2631 def RealSort(ctx=None):
2632  """Return the real sort in the given context. If `ctx=None`, then the global context is used.
2633 
2634  >>> RealSort()
2635  Real
2636  >>> x = Const('x', RealSort())
2637  >>> is_real(x)
2638  True
2639  >>> is_int(x)
2640  False
2641  >>> x.sort() == RealSort()
2642  True
2643  """
2644  ctx = _get_ctx(ctx)
2645  return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
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().

2673 def RealVal(val, ctx=None):
2674  """Return a Z3 real value.
2675 
2676  `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
2677  If `ctx=None`, then the global context is used.
2678 
2679  >>> RealVal(1)
2680  1
2681  >>> RealVal(1).sort()
2682  Real
2683  >>> RealVal("3/5")
2684  3/5
2685  >>> RealVal("1.5")
2686  3/2
2687  """
2688  ctx = _get_ctx(ctx)
2689  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
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().

1172 def RealVar(idx, ctx=None):
1173  """
1174  Create a real free variable. Free variables are used to create quantified formulas.
1175  They are also used to create polynomials.
1176 
1177  >>> RealVar(0)
1178  Var(0)
1179  """
1180  return Var(idx, RealSort(ctx))
def RealSort
Definition: z3py.py:2630
def RealVar
Definition: z3py.py:1171
def Var
Definition: z3py.py:1159
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.

1182 def RealVarVector(n, ctx=None):
1183  """
1184  Create a list of Real free variables.
1185  The variables have ids: 0, 1, ..., n-1
1186 
1187  >>> x0, x1, x2, x3 = RealVarVector(4)
1188  >>> x2
1189  Var(2)
1190  """
1191  return [ RealVar(i, ctx) for i in range(n) ]
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.

2792 def RealVector(prefix, sz, ctx=None):
2793  """Return a list of real constants of size `sz`.
2794 
2795  >>> X = RealVector('x', 3)
2796  >>> X
2797  [x__0, x__1, x__2]
2798  >>> Sum(X)
2799  x__0 + x__1 + x__2
2800  >>> Sum(X).sort()
2801  Real
2802  """
2803  return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]
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.

6638 def Repeat(t, max=4294967295, ctx=None):
6639  """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
6640 
6641  >>> x, y = Ints('x y')
6642  >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
6643  >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
6644  >>> r = t(c)
6645  >>> for subgoal in r: print(subgoal)
6646  [x == 0, y == 0, x > y]
6647  [x == 0, y == 1, x > y]
6648  [x == 1, y == 0, x > y]
6649  [x == 1, y == 1, x > y]
6650  >>> t = Then(t, Tactic('propagate-values'))
6651  >>> t(c)
6652  [[x == 1, y == 0]]
6653  """
6654  t = _to_tactic(t, ctx)
6655  return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)
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.

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

Definition at line 237 of file z3py.py.

238 def reset_params():
239  """Reset all global (or module) parameters.
240  """
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.

3708 def RotateLeft(a, b):
3709  """Return an expression representing `a` rotated to the left `b` times.
3710 
3711  >>> a, b = BitVecs('a b', 16)
3712  >>> RotateLeft(a, b)
3713  RotateLeft(a, b)
3714  >>> simplify(RotateLeft(a, 0))
3715  a
3716  >>> simplify(RotateLeft(a, 16))
3717  a
3718  """
3719  _check_bv_args(a, b)
3720  a, b = _coerce_exprs(a, b)
3721  return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def RotateLeft
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.

3723 def RotateRight(a, b):
3724  """Return an expression representing `a` rotated to the right `b` times.
3725 
3726  >>> a, b = BitVecs('a b', 16)
3727  >>> RotateRight(a, b)
3728  RotateRight(a, b)
3729  >>> simplify(RotateRight(a, 0))
3730  a
3731  >>> simplify(RotateRight(a, 16))
3732  a
3733  """
3734  _check_bv_args(a, b)
3735  a, b = _coerce_exprs(a, b)
3736  return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
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
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.

4027 def Select(a, i):
4028  """Return a Z3 select array expression.
4029 
4030  >>> a = Array('a', IntSort(), IntSort())
4031  >>> i = Int('i')
4032  >>> Select(a, i)
4033  a[i]
4034  >>> eq(Select(a, i), a[i])
4035  True
4036  """
4037  if __debug__:
4038  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
4039  return a[i]
def Select
Definition: z3py.py:4026
def is_array
Definition: z3py.py:3886
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.

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

243 def set_option(*args, **kws):
244  """Alias for 'set_param' for backward compatibility.
245  """
246  return set_param(*args, **kws)
def set_option
Definition: z3py.py:242
def set_param
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().

215 def set_param(*args, **kws):
216  """Set Z3 global (or module) parameters.
217 
218  >>> set_param(precision=10)
219  """
220  if __debug__:
221  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
222  new_kws = {}
223  for k in kws:
224  v = kws[k]
225  if not set_pp_option(k, v):
226  new_kws[k] = v
227  for key in new_kws:
228  value = new_kws[key]
229  Z3_global_param_set(str(key).upper(), _to_param_value(value))
230  prev = None
231  for a in args:
232  if prev == None:
233  prev = a
234  else:
235  Z3_global_param_set(str(prev), _to_param_value(a))
236  prev = None
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 set_param
Definition: z3py.py:214
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.

3738 def SignExt(n, a):
3739  """Return a bit-vector expression with `n` extra sign-bits.
3740 
3741  >>> x = BitVec('x', 16)
3742  >>> n = SignExt(8, x)
3743  >>> n.size()
3744  24
3745  >>> n
3746  SignExt(8, x)
3747  >>> n.sort()
3748  BitVec(24)
3749  >>> v0 = BitVecVal(2, 2)
3750  >>> v0
3751  2
3752  >>> v0.size()
3753  2
3754  >>> v = simplify(SignExt(6, v0))
3755  >>> v
3756  254
3757  >>> v.size()
3758  8
3759  >>> print("%.x" % v.as_long())
3760  fe
3761  """
3762  if __debug__:
3763  _z3_assert(isinstance(n, int), "First argument must be an integer")
3764  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3765  return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
def SignExt
Definition: z3py.py:3737
def is_bv
Definition: z3py.py:3390
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 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().

6074 def SimpleSolver(ctx=None):
6075  """Return a simple general purpose solver with limited amount of preprocessing.
6076 
6077  >>> s = SimpleSolver()
6078  >>> x = Int('x')
6079  >>> s.add(x > 0)
6080  >>> s.check()
6081  sat
6082  """
6083  ctx = _get_ctx(ctx)
6084  return Solver(Z3_mk_simple_solver(ctx.ref()), ctx)
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().

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

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

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

6054 def SolverFor(logic, ctx=None):
6055  """Create a solver customized for the given logic.
6056 
6057  The parameter `logic` is a string. It should be contains
6058  the name of a SMT-LIB logic.
6059  See http://www.smtlib.org/ for the name of all available logics.
6060 
6061  >>> s = SolverFor("QF_LIA")
6062  >>> x = Int('x')
6063  >>> s.add(x > 0)
6064  >>> s.add(x < 2)
6065  >>> s.check()
6066  sat
6067  >>> s.model()
6068  [x = 1]
6069  """
6070  ctx = _get_ctx(ctx)
6071  logic = to_symbol(logic)
6072  return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx)
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().

2868 def Sqrt(a, ctx=None):
2869  """ Return a Z3 expression which represents the square root of a.
2870 
2871  >>> x = Real('x')
2872  >>> Sqrt(x)
2873  x**(1/2)
2874  """
2875  if not is_expr(a):
2876  ctx = _get_ctx(ctx)
2877  a = RealVal(a, ctx)
2878  return a ** "1/2"
def is_expr
Definition: z3py.py:950
def RealVal
Definition: z3py.py:2672
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().

3657 def SRem(a, b):
3658  """Create the Z3 expression signed remainder.
3659 
3660  Use the operator % for signed modulus, and URem() for unsigned remainder.
3661 
3662  >>> x = BitVec('x', 32)
3663  >>> y = BitVec('y', 32)
3664  >>> SRem(x, y)
3665  SRem(x, y)
3666  >>> SRem(x, y).sort()
3667  BitVec(32)
3668  >>> (x % y).sexpr()
3669  '(bvsmod x y)'
3670  >>> SRem(x, y).sexpr()
3671  '(bvsrem x y)'
3672  """
3673  _check_bv_args(a, b)
3674  a, b = _coerce_exprs(a, b)
3675  return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
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
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().

4011 def Store(a, i, v):
4012  """Return a Z3 store array expression.
4013 
4014  >>> a = Array('a', IntSort(), IntSort())
4015  >>> i, v = Ints('i v')
4016  >>> s = Store(a, i, v)
4017  >>> s.sort()
4018  Array(Int, Int)
4019  >>> prove(s[i] == v)
4020  proved
4021  >>> j = Int('j')
4022  >>> prove(Implies(i != j, s[j] == a[j]))
4023  proved
4024  """
4025  return Update(a, i, v)
def Update
Definition: z3py.py:3989
def Store
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.

6989 def substitute(t, *m):
6990  """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.
6991 
6992  >>> x = Int('x')
6993  >>> y = Int('y')
6994  >>> substitute(x + 1, (x, y + 1))
6995  y + 1 + 1
6996  >>> f = Function('f', IntSort(), IntSort())
6997  >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
6998  1 + 1
6999  """
7000  if isinstance(m, tuple):
7001  m1 = _get_args(m)
7002  if isinstance(m1, list):
7003  m = m1
7004  if __debug__:
7005  _z3_assert(is_expr(t), "Z3 expression expected")
7006  _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.")
7007  num = len(m)
7008  _from = (Ast * num)()
7009  _to = (Ast * num)()
7010  for i in range(num):
7011  _from[i] = m[i][0].as_ast()
7012  _to[i] = m[i][1].as_ast()
7013  return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
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 is_expr
Definition: z3py.py:950
def substitute
Definition: z3py.py:6988
def eq
Definition: z3py.py:372
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.

7015 def substitute_vars(t, *m):
7016  """Substitute the free variables in t with the expression in m.
7017 
7018  >>> v0 = Var(0, IntSort())
7019  >>> v1 = Var(1, IntSort())
7020  >>> x = Int('x')
7021  >>> f = Function('f', IntSort(), IntSort(), IntSort())
7022  >>> # replace v0 with x+1 and v1 with x
7023  >>> substitute_vars(f(v0, v1), x + 1, x)
7024  f(x + 1, x)
7025  """
7026  if __debug__:
7027  _z3_assert(is_expr(t), "Z3 expression expected")
7028  _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
7029  num = len(m)
7030  _to = (Ast * num)()
7031  for i in range(num):
7032  _to[i] = m[i].as_ast()
7033  return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
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 is_expr
Definition: z3py.py:950
def substitute_vars
Definition: z3py.py:7014
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().

7035 def Sum(*args):
7036  """Create the sum of the Z3 expressions.
7037 
7038  >>> a, b, c = Ints('a b c')
7039  >>> Sum(a, b, c)
7040  a + b + c
7041  >>> Sum([a, b, c])
7042  a + b + c
7043  >>> A = IntVector('a', 5)
7044  >>> Sum(A)
7045  a__0 + a__1 + a__2 + a__3 + a__4
7046  """
7047  args = _get_args(args)
7048  if __debug__:
7049  _z3_assert(len(args) > 0, "Non empty list of arguments expected")
7050  ctx = _ctx_from_ast_arg_list(args)
7051  if __debug__:
7052  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
7053  args = _coerce_expr_list(args, ctx)
7054  if is_bv(args[0]):
7055  return _reduce(lambda a, b: a + b, args, 0)
7056  else:
7057  _args, sz = _to_ast_array(args)
7058  return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)
def is_bv
Definition: z3py.py:3390
def Sum
Definition: z3py.py:7034
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().

6675 def tactic_description(name, ctx=None):
6676  """Return a short description for the tactic named `name`.
6677 
6678  >>> d = tactic_description('simplify')
6679  """
6680  ctx = _get_ctx(ctx)
6681  return Z3_tactic_get_descr(ctx.ref(), name)
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().

6665 def tactics(ctx=None):
6666  """Return a list of all available tactics in Z3.
6667 
6668  >>> l = tactics()
6669  >>> l.count('simplify') == 1
6670  True
6671  """
6672  ctx = _get_ctx(ctx)
6673  return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]
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().

6557 def Then(*ts, **ks):
6558  """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
6559 
6560  >>> x, y = Ints('x y')
6561  >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
6562  >>> t(And(x == 0, y > x + 1))
6563  [[Not(y <= 1)]]
6564  >>> t(And(x == 0, y > x + 1)).as_expr()
6565  Not(y <= 1)
6566  """
6567  return AndThen(*ts, **ks)
def AndThen
Definition: z3py.py:6537
def Then
Definition: z3py.py:6556
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 
95 def to_symbol(s, ctx=None):
96  """Convert an integer or string into a Z3 symbol."""
97  if isinstance(s, int):
98  return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
99  else:
100  return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
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().

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

2818 def ToReal(a):
2819  """ Return the Z3 expression ToReal(a).
2820 
2821  >>> x = Int('x')
2822  >>> x.sort()
2823  Int
2824  >>> n = ToReal(x)
2825  >>> n
2826  ToReal(x)
2827  >>> n.sort()
2828  Real
2829  """
2830  if __debug__:
2831  _z3_assert(a.is_int(), "Z3 integer expression expected.")
2832  ctx = a.ctx
2833  return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
def ToReal
Definition: z3py.py:2817
Z3_ast Z3_API Z3_mk_int2real(__in Z3_context c, __in Z3_ast t1)
Coerce an integer to a real.
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().

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

6657 def TryFor(t, ms, ctx=None):
6658  """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
6659 
6660  If `t` does not terminate in `ms` milliseconds, then it fails.
6661  """
6662  t = _to_tactic(t, ctx)
6663  return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)
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__().

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

3583 def UGE(a, b):
3584  """Create the Z3 expression (unsigned) `other >= self`.
3585 
3586  Use the operator >= for signed greater than or equal to.
3587 
3588  >>> x, y = BitVecs('x y', 32)
3589  >>> UGE(x, y)
3590  UGE(x, y)
3591  >>> (x >= y).sexpr()
3592  '(bvsge x y)'
3593  >>> UGE(x, y).sexpr()
3594  '(bvuge x y)'
3595  """
3596  _check_bv_args(a, b)
3597  a, b = _coerce_exprs(a, b)
3598  return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def UGE
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__().

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

3549 def ULE(a, b):
3550  """Create the Z3 expression (unsigned) `other <= self`.
3551 
3552  Use the operator <= for signed less than or equal to.
3553 
3554  >>> x, y = BitVecs('x y', 32)
3555  >>> ULE(x, y)
3556  ULE(x, y)
3557  >>> (x <= y).sexpr()
3558  '(bvsle x y)'
3559  >>> ULE(x, y).sexpr()
3560  '(bvule x y)'
3561  """
3562  _check_bv_args(a, b)
3563  a, b = _coerce_exprs(a, b)
3564  return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
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
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__().

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

3990 def Update(a, i, v):
3991  """Return a Z3 store array expression.
3992 
3993  >>> a = Array('a', IntSort(), IntSort())
3994  >>> i, v = Ints('i v')
3995  >>> s = Update(a, i, v)
3996  >>> s.sort()
3997  Array(Int, Int)
3998  >>> prove(s[i] == v)
3999  proved
4000  >>> j = Int('j')
4001  >>> prove(Implies(i != j, s[j] == a[j]))
4002  proved
4003  """
4004  if __debug__:
4005  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
4006  i = a.domain().cast(i)
4007  v = a.range().cast(v)
4008  ctx = a.ctx
4009  return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
def Update
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 is_array
Definition: z3py.py:3886
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().

3637 def URem(a, b):
3638  """Create the Z3 expression (unsigned) remainder `self % other`.
3639 
3640  Use the operator % for signed modulus, and SRem() for signed remainder.
3641 
3642  >>> x = BitVec('x', 32)
3643  >>> y = BitVec('y', 32)
3644  >>> URem(x, y)
3645  URem(x, y)
3646  >>> URem(x, y).sort()
3647  BitVec(32)
3648  >>> (x % y).sexpr()
3649  '(bvsmod x y)'
3650  >>> URem(x, y).sexpr()
3651  '(bvurem x y)'
3652  """
3653  _check_bv_args(a, b)
3654  a, b = _coerce_exprs(a, b)
3655  return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
Z3_ast Z3_API Z3_mk_bvurem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned remainder.
def URem
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().

1160 def Var(idx, s):
1161  """Create a Z3 free variable. Free variables are used to create quantified formulas.
1162 
1163  >>> Var(0, IntSort())
1164  Var(0)
1165  >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1166  False
1167  """
1168  if __debug__:
1169  _z3_assert(is_sort(s), "Z3 sort expected")
1170  return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
Z3_ast Z3_API Z3_mk_bound(__in Z3_context c, __in unsigned index, __in Z3_sort ty)
Create a bound variable.
def Var
Definition: z3py.py:1159
def is_sort
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.

6923 def When(p, t, ctx=None):
6924  """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6925 
6926  >>> t = When(Probe('size') > 2, Tactic('simplify'))
6927  >>> x, y = Ints('x y')
6928  >>> g = Goal()
6929  >>> g.add(x > 0)
6930  >>> g.add(y > 0)
6931  >>> t(g)
6932  [[x > 0, y > 0]]
6933  >>> g.add(x == y + 1)
6934  >>> t(g)
6935  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6936  """
6937  p = _to_probe(p, ctx)
6938  t = _to_tactic(t, ctx)
6939  return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
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().

6625 def With(t, *args, **keys):
6626  """Return a tactic that applies tactic `t` using the given configuration options.
6627 
6628  >>> x, y = Ints('x y')
6629  >>> t = With(Tactic('simplify'), som=True)
6630  >>> t((x + 1)*(y + 2) == 0)
6631  [[2*x + y + x*y == -2]]
6632  """
6633  ctx = keys.get('ctx', None)
6634  t = _to_tactic(t, ctx)
6635  p = args2params(args, keys, t.ctx)
6636  return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
def With
Definition: z3py.py:6624
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 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.

1429 def Xor(a, b, ctx=None):
1430  """Create a Z3 Xor expression.
1431 
1432  >>> p, q = Bools('p q')
1433  >>> Xor(p, q)
1434  Xor(p, q)
1435  >>> simplify(Xor(p, q))
1436  Not(p) == q
1437  """
1438  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1439  s = BoolSort(ctx)
1440  a = s.cast(a)
1441  b = s.cast(b)
1442  return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
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.

3767 def ZeroExt(n, a):
3768  """Return a bit-vector expression with `n` extra zero-bits.
3769 
3770  >>> x = BitVec('x', 16)
3771  >>> n = ZeroExt(8, x)
3772  >>> n.size()
3773  24
3774  >>> n
3775  ZeroExt(8, x)
3776  >>> n.sort()
3777  BitVec(24)
3778  >>> v0 = BitVecVal(2, 2)
3779  >>> v0
3780  2
3781  >>> v0.size()
3782  2
3783  >>> v = simplify(ZeroExt(6, v0))
3784  >>> v
3785  2
3786  >>> v.size()
3787  8
3788  """
3789  if __debug__:
3790  _z3_assert(isinstance(n, int), "First argument must be an integer")
3791  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3792  return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
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
Definition: z3py.py:3766
def is_bv
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.