Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

class  AlgebraicNumRef
 
class  ApplyResult
 
class  ArithRef
 
class  ArithSortRef
 Arithmetic. More...
 
class  ArrayRef
 
class  ArraySortRef
 Arrays. More...
 
class  AstMap
 
class  AstRef
 
class  AstVector
 
class  BitVecNumRef
 
class  BitVecRef
 
class  BitVecSortRef
 Bit-Vectors. More...
 
class  BoolRef
 
class  BoolSortRef
 Booleans. More...
 
class  CheckSatResult
 
class  Context
 
class  Datatype
 
class  DatatypeRef
 
class  DatatypeSortRef
 
class  ExprRef
 Expressions. More...
 
class  FiniteDomainNumRef
 
class  FiniteDomainRef
 
class  FiniteDomainSortRef
 
class  Fixedpoint
 Fixedpoint. More...
 
class  FPNumRef
 FP Numerals. More...
 
class  FPRef
 FP Expressions. More...
 
class  FPRMRef
 
class  FPRMSortRef
 
class  FPSortRef
 FP Sorts. More...
 
class  FuncDeclRef
 Function Declarations. More...
 
class  FuncEntry
 
class  FuncInterp
 
class  Goal
 
class  IntNumRef
 
class  ModelRef
 
class  Optimize
 
class  OptimizeObjective
 Optimize. More...
 
class  ParamDescrsRef
 
class  ParamsRef
 Parameter Sets. More...
 
class  PatternRef
 Patterns. More...
 
class  Probe
 
class  QuantifierRef
 Quantifiers. More...
 
class  RatNumRef
 
class  ReRef
 
class  ReSortRef
 Regular expressions. More...
 
class  ScopedConstructor
 
class  ScopedConstructorList
 
class  SeqRef
 
class  SeqSortRef
 Strings, Sequences and Regular expressions. More...
 
class  Solver
 
class  SortRef
 
class  Statistics
 Statistics. More...
 
class  Tactic
 
class  Z3PPObject
 ASTs base class. More...
 

Functions

def z3_debug ()
 
def enable_trace (msg)
 
def disable_trace (msg)
 
def get_version_string ()
 
def get_version ()
 
def get_full_version ()
 
def open_log (fname)
 
def append_log (s)
 
def to_symbol (s, ctx=None)
 
def z3_error_handler (c, e)
 
def main_ctx ()
 
def get_ctx (ctx)
 
def set_param (args, kws)
 
def reset_params ()
 
def set_option (args, kws)
 
def get_param (name)
 
def is_ast (a)
 
def eq (a, b)
 
def is_sort (s)
 
def DeclareSort (name, ctx=None)
 
def is_func_decl (a)
 
def Function (name, sig)
 
def RecFunction (name, sig)
 
def RecAddDefinition (f, args, body)
 
def is_expr (a)
 
def is_app (a)
 
def is_const (a)
 
def is_var (a)
 
def get_var_index (a)
 
def is_app_of (a, k)
 
def If (a, b, c, ctx=None)
 
def Distinct (args)
 
def Const (name, sort)
 
def Consts (names, sort)
 
def FreshConst (sort, prefix='c')
 
def Var (idx, s)
 
def RealVar (idx, ctx=None)
 
def RealVarVector (n, ctx=None)
 
def is_bool (a)
 
def is_true (a)
 
def is_false (a)
 
def is_and (a)
 
def is_or (a)
 
def is_implies (a)
 
def is_not (a)
 
def is_eq (a)
 
def is_distinct (a)
 
def BoolSort (ctx=None)
 
def BoolVal (val, ctx=None)
 
def Bool (name, ctx=None)
 
def Bools (names, ctx=None)
 
def BoolVector (prefix, sz, ctx=None)
 
def FreshBool (prefix='b', ctx=None)
 
def Implies (a, b, ctx=None)
 
def Xor (a, b, ctx=None)
 
def Not (a, ctx=None)
 
def mk_not (a)
 
def And (args)
 
def Or (args)
 
def is_pattern (a)
 
def MultiPattern (args)
 
def is_quantifier (a)
 
def ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Lambda (vs, body)
 
def is_arith_sort (s)
 
def is_arith (a)
 
def is_int (a)
 
def is_real (a)
 
def is_int_value (a)
 
def is_rational_value (a)
 
def is_algebraic_value (a)
 
def is_add (a)
 
def is_mul (a)
 
def is_sub (a)
 
def is_div (a)
 
def is_idiv (a)
 
def is_mod (a)
 
def is_le (a)
 
def is_lt (a)
 
def is_ge (a)
 
def is_gt (a)
 
def is_is_int (a)
 
def is_to_real (a)
 
def is_to_int (a)
 
def IntSort (ctx=None)
 
def RealSort (ctx=None)
 
def IntVal (val, ctx=None)
 
def RealVal (val, ctx=None)
 
def RatVal (a, b, ctx=None)
 
def Q (a, b, ctx=None)
 
def Int (name, ctx=None)
 
def Ints (names, ctx=None)
 
def IntVector (prefix, sz, ctx=None)
 
def FreshInt (prefix='x', ctx=None)
 
def Real (name, ctx=None)
 
def Reals (names, ctx=None)
 
def RealVector (prefix, sz, ctx=None)
 
def FreshReal (prefix='b', ctx=None)
 
def ToReal (a)
 
def ToInt (a)
 
def IsInt (a)
 
def Sqrt (a, ctx=None)
 
def Cbrt (a, ctx=None)
 
def is_bv_sort (s)
 
def is_bv (a)
 
def is_bv_value (a)
 
def BV2Int (a, is_signed=False)
 
def Int2BV (a, num_bits)
 
def BitVecSort (sz, ctx=None)
 
def BitVecVal (val, bv, ctx=None)
 
def BitVec (name, bv, ctx=None)
 
def BitVecs (names, bv, ctx=None)
 
def Concat (args)
 
def Extract (high, low, a)
 
def ULE (a, b)
 
def ULT (a, b)
 
def UGE (a, b)
 
def UGT (a, b)
 
def UDiv (a, b)
 
def URem (a, b)
 
def SRem (a, b)
 
def LShR (a, b)
 
def RotateLeft (a, b)
 
def RotateRight (a, b)
 
def SignExt (n, a)
 
def ZeroExt (n, a)
 
def RepeatBitVec (n, a)
 
def BVRedAnd (a)
 
def BVRedOr (a)
 
def BVAddNoOverflow (a, b, signed)
 
def BVAddNoUnderflow (a, b)
 
def BVSubNoOverflow (a, b)
 
def BVSubNoUnderflow (a, b, signed)
 
def BVSDivNoOverflow (a, b)
 
def BVSNegNoOverflow (a)
 
def BVMulNoOverflow (a, b, signed)
 
def BVMulNoUnderflow (a, b)
 
def is_array_sort (a)
 
def is_array (a)
 
def is_const_array (a)
 
def is_K (a)
 
def is_map (a)
 
def is_default (a)
 
def get_map_func (a)
 
def ArraySort (sig)
 
def Array (name, dom, rng)
 
def Update (a, i, v)
 
def Default (a)
 
def Store (a, i, v)
 
def Select (a, i)
 
def Map (f, args)
 
def K (dom, v)
 
def Ext (a, b)
 
def SetHasSize (a, k)
 
def is_select (a)
 
def is_store (a)
 
def SetSort (s)
 Sets. More...
 
def EmptySet (s)
 
def FullSet (s)
 
def SetUnion (args)
 
def SetIntersect (args)
 
def SetAdd (s, e)
 
def SetDel (s, e)
 
def SetComplement (s)
 
def SetDifference (a, b)
 
def IsMember (e, s)
 
def IsSubset (a, b)
 
def CreateDatatypes (ds)
 
def TupleSort (name, sorts, ctx=None)
 
def DisjointSum (name, sorts, ctx=None)
 
def EnumSort (name, values, ctx=None)
 
def args2params (arguments, keywords, ctx=None)
 
def Model (ctx=None)
 
def is_as_array (n)
 
def get_as_array_func (n)
 
def SolverFor (logic, ctx=None)
 
def SimpleSolver (ctx=None)
 
def FiniteDomainSort (name, sz, ctx=None)
 
def is_finite_domain_sort (s)
 
def is_finite_domain (a)
 
def FiniteDomainVal (val, sort, ctx=None)
 
def is_finite_domain_value (a)
 
def AndThen (ts, ks)
 
def Then (ts, ks)
 
def OrElse (ts, ks)
 
def ParOr (ts, ks)
 
def ParThen (t1, t2, ctx=None)
 
def ParAndThen (t1, t2, ctx=None)
 
def With (t, args, keys)
 
def WithParams (t, p)
 
def Repeat (t, max=4294967295, ctx=None)
 
def TryFor (t, ms, ctx=None)
 
def tactics (ctx=None)
 
def tactic_description (name, ctx=None)
 
def describe_tactics ()
 
def is_probe (p)
 
def probes (ctx=None)
 
def probe_description (name, ctx=None)
 
def describe_probes ()
 
def FailIf (p, ctx=None)
 
def When (p, t, ctx=None)
 
def Cond (p, t1, t2, ctx=None)
 
def simplify (a, arguments, keywords)
 Utils. More...
 
def help_simplify ()
 
def simplify_param_descrs ()
 
def substitute (t, m)
 
def substitute_vars (t, m)
 
def Sum (args)
 
def Product (args)
 
def AtMost (args)
 
def AtLeast (args)
 
def PbLe (args, k)
 
def PbGe (args, k)
 
def PbEq (args, k, ctx=None)
 
def solve (args, keywords)
 
def solve_using (s, args, keywords)
 
def prove (claim, keywords)
 
def parse_smt2_string (s, sorts={}, decls={}, ctx=None)
 
def parse_smt2_file (f, sorts={}, decls={}, ctx=None)
 
def get_default_rounding_mode (ctx=None)
 
def set_default_rounding_mode (rm, ctx=None)
 
def get_default_fp_sort (ctx=None)
 
def set_default_fp_sort (ebits, sbits, ctx=None)
 
def Float16 (ctx=None)
 
def FloatHalf (ctx=None)
 
def Float32 (ctx=None)
 
def FloatSingle (ctx=None)
 
def Float64 (ctx=None)
 
def FloatDouble (ctx=None)
 
def Float128 (ctx=None)
 
def FloatQuadruple (ctx=None)
 
def is_fp_sort (s)
 
def is_fprm_sort (s)
 
def RoundNearestTiesToEven (ctx=None)
 
def RNE (ctx=None)
 
def RoundNearestTiesToAway (ctx=None)
 
def RNA (ctx=None)
 
def RoundTowardPositive (ctx=None)
 
def RTP (ctx=None)
 
def RoundTowardNegative (ctx=None)
 
def RTN (ctx=None)
 
def RoundTowardZero (ctx=None)
 
def RTZ (ctx=None)
 
def is_fprm (a)
 
def is_fprm_value (a)
 
def is_fp (a)
 
def is_fp_value (a)
 
def FPSort (ebits, sbits, ctx=None)
 
def fpNaN (s)
 
def fpPlusInfinity (s)
 
def fpMinusInfinity (s)
 
def fpInfinity (s, negative)
 
def fpPlusZero (s)
 
def fpMinusZero (s)
 
def fpZero (s, negative)
 
def FPVal (sig, exp=None, fps=None, ctx=None)
 
def FP (name, fpsort, ctx=None)
 
def FPs (names, fpsort, ctx=None)
 
def fpAbs (a, ctx=None)
 
def fpNeg (a, ctx=None)
 
def fpAdd (rm, a, b, ctx=None)
 
def fpSub (rm, a, b, ctx=None)
 
def fpMul (rm, a, b, ctx=None)
 
def fpDiv (rm, a, b, ctx=None)
 
def fpRem (a, b, ctx=None)
 
def fpMin (a, b, ctx=None)
 
def fpMax (a, b, ctx=None)
 
def fpFMA (rm, a, b, c, ctx=None)
 
def fpSqrt (rm, a, ctx=None)
 
def fpRoundToIntegral (rm, a, ctx=None)
 
def fpIsNaN (a, ctx=None)
 
def fpIsInf (a, ctx=None)
 
def fpIsZero (a, ctx=None)
 
def fpIsNormal (a, ctx=None)
 
def fpIsSubnormal (a, ctx=None)
 
def fpIsNegative (a, ctx=None)
 
def fpIsPositive (a, ctx=None)
 
def fpLT (a, b, ctx=None)
 
def fpLEQ (a, b, ctx=None)
 
def fpGT (a, b, ctx=None)
 
def fpGEQ (a, b, ctx=None)
 
def fpEQ (a, b, ctx=None)
 
def fpNEQ (a, b, ctx=None)
 
def fpFP (sgn, exp, sig, ctx=None)
 
def fpToFP (a1, a2=None, a3=None, ctx=None)
 
def fpBVToFP (v, sort, ctx=None)
 
def fpFPToFP (rm, v, sort, ctx=None)
 
def fpRealToFP (rm, v, sort, ctx=None)
 
def fpSignedToFP (rm, v, sort, ctx=None)
 
def fpUnsignedToFP (rm, v, sort, ctx=None)
 
def fpToFPUnsigned (rm, x, s, ctx=None)
 
def fpToSBV (rm, x, s, ctx=None)
 
def fpToUBV (rm, x, s, ctx=None)
 
def fpToReal (x, ctx=None)
 
def fpToIEEEBV (x, ctx=None)
 
def StringSort (ctx=None)
 
def SeqSort (s)
 
def is_seq (a)
 
def is_string (a)
 
def is_string_value (a)
 
def StringVal (s, ctx=None)
 
def String (name, ctx=None)
 
def Strings (names, ctx=None)
 
def SubString (s, offset, length)
 
def SubSeq (s, offset, length)
 
def Empty (s)
 
def Full (s)
 
def Unit (a)
 
def PrefixOf (a, b)
 
def SuffixOf (a, b)
 
def Contains (a, b)
 
def Replace (s, src, dst)
 
def IndexOf (s, substr)
 
def IndexOf (s, substr, offset)
 
def LastIndexOf (s, substr)
 
def Length (s)
 
def StrToInt (s)
 
def IntToStr (s)
 
def Re (s, ctx=None)
 
def ReSort (s)
 
def is_re (s)
 
def InRe (s, re)
 
def Union (args)
 
def Intersect (args)
 
def Plus (re)
 
def Option (re)
 
def Complement (re)
 
def Star (re)
 
def Loop (re, lo, hi=0)
 
def Range (lo, hi, ctx=None)
 
def PartialOrder (a, index)
 
def LinearOrder (a, index)
 
def TreeOrder (a, index)
 
def PiecewiseLinearOrder (a, index)
 
def TransitiveClosure (f)
 

Variables

 Z3_DEBUG = __debug__
 
 sat = CheckSatResult(Z3_L_TRUE)
 
 unsat = CheckSatResult(Z3_L_FALSE)
 
 unknown = CheckSatResult(Z3_L_UNDEF)
 

Function Documentation

◆ And()

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

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

1680 def And(*args):
1681  """Create a Z3 and-expression or and-probe.
1682 
1683  >>> p, q, r = Bools('p q r')
1684  >>> And(p, q, r)
1685  And(p, q, r)
1686  >>> P = BoolVector('p', 5)
1687  >>> And(P)
1688  And(p__0, p__1, p__2, p__3, p__4)
1689  """
1690  last_arg = None
1691  if len(args) > 0:
1692  last_arg = args[len(args)-1]
1693  if isinstance(last_arg, Context):
1694  ctx = args[len(args)-1]
1695  args = args[:len(args)-1]
1696  elif len(args) == 1 and isinstance(args[0], AstVector):
1697  ctx = args[0].ctx
1698  args = [a for a in args[0]]
1699  else:
1700  ctx = main_ctx()
1701  args = _get_args(args)
1702  ctx_args = _ctx_from_ast_arg_list(args, ctx)
1703  if z3_debug():
1704  _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch")
1705  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1706  if _has_probe(args):
1707  return _probe_and(args, ctx)
1708  else:
1709  args = _coerce_expr_list(args, ctx)
1710  _args, sz = _to_ast_array(args)
1711  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1712 
def And(args)
Definition: z3py.py:1680
def main_ctx()
Definition: z3py.py:211
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
def z3_debug()
Definition: z3py.py:56

◆ AndThen()

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

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

7745 def AndThen(*ts, **ks):
7746  """Return a tactic that applies the tactics in `*ts` in sequence.
7747 
7748  >>> x, y = Ints('x y')
7749  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
7750  >>> t(And(x == 0, y > x + 1))
7751  [[Not(y <= 1)]]
7752  >>> t(And(x == 0, y > x + 1)).as_expr()
7753  Not(y <= 1)
7754  """
7755  if z3_debug():
7756  _z3_assert(len(ts) >= 2, "At least two arguments expected")
7757  ctx = ks.get('ctx', None)
7758  num = len(ts)
7759  r = ts[0]
7760  for i in range(num - 1):
7761  r = _and_then(r, ts[i+1], ctx)
7762  return r
7763 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def AndThen(ts, ks)
Definition: z3py.py:7745
def z3_debug()
Definition: z3py.py:56

◆ append_log()

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

Definition at line 105 of file z3py.py.

105 def append_log(s):
106  """Append user-defined string to interaction log. """
107  Z3_append_log(s)
108 
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
def append_log(s)
Definition: z3py.py:105

◆ args2params()

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

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

5070 def args2params(arguments, keywords, ctx=None):
5071  """Convert python arguments into a Z3_params object.
5072  A ':' is added to the keywords, and '_' is replaced with '-'
5073 
5074  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5075  (params model true relevancy 2 elim_and true)
5076  """
5077  if z3_debug():
5078  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5079  prev = None
5080  r = ParamsRef(ctx)
5081  for a in arguments:
5082  if prev is None:
5083  prev = a
5084  else:
5085  r.set(prev, a)
5086  prev = None
5087  for k in keywords:
5088  v = keywords[k]
5089  r.set(k, v)
5090  return r
5091 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5070
def z3_debug()
Definition: z3py.py:56

◆ Array()

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 4403 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(), Lambda(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), Store(), and Update().

4403 def Array(name, dom, rng):
4404  """Return an array constant named `name` with the given domain and range sorts.
4405 
4406  >>> a = Array('a', IntSort(), IntSort())
4407  >>> a.sort()
4408  Array(Int, Int)
4409  >>> a[0]
4410  a[0]
4411  """
4412  s = ArraySort(dom, rng)
4413  ctx = s.ctx
4414  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4415 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def ArraySort(sig)
Definition: z3py.py:4371
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def Array(name, dom, rng)
Definition: z3py.py:4403

◆ ArraySort()

def z3py.ArraySort (   sig)
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 4371 of file z3py.py.

Referenced by ArraySortRef.domain(), Context.mkArraySort(), Context.MkArraySort(), ArraySortRef.range(), Sort.translate(), and Sort.Translate().

4371 def ArraySort(*sig):
4372  """Return the Z3 array sort with the given domain and range sorts.
4373 
4374  >>> A = ArraySort(IntSort(), BoolSort())
4375  >>> A
4376  Array(Int, Bool)
4377  >>> A.domain()
4378  Int
4379  >>> A.range()
4380  Bool
4381  >>> AA = ArraySort(IntSort(), A)
4382  >>> AA
4383  Array(Int, Array(Int, Bool))
4384  """
4385  sig = _get_args(sig)
4386  if z3_debug():
4387  _z3_assert(len(sig) > 1, "At least two arguments expected")
4388  arity = len(sig) - 1
4389  r = sig[arity]
4390  d = sig[0]
4391  if z3_debug():
4392  for s in sig:
4393  _z3_assert(is_sort(s), "Z3 sort expected")
4394  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4395  ctx = d.ctx
4396  if len(sig) == 2:
4397  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4398  dom = (Sort * arity)()
4399  for i in range(arity):
4400  dom[i] = sig[i].ast
4401  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4402 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def ArraySort(sig)
Definition: z3py.py:4371
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
def is_sort(s)
Definition: z3py.py:596
def z3_debug()
Definition: z3py.py:56

◆ AtLeast()

def z3py.AtLeast (   args)
Create an at-most Pseudo-Boolean k constraint.

>>> a, b, c = Bools('a b c')
>>> f = AtLeast(a, b, c, 2)

Definition at line 8326 of file z3py.py.

8326 def AtLeast(*args):
8327  """Create an at-most Pseudo-Boolean k constraint.
8328 
8329  >>> a, b, c = Bools('a b c')
8330  >>> f = AtLeast(a, b, c, 2)
8331  """
8332  args = _get_args(args)
8333  if z3_debug():
8334  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8335  ctx = _ctx_from_ast_arg_list(args)
8336  if z3_debug():
8337  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8338  args1 = _coerce_expr_list(args[:-1], ctx)
8339  k = args[-1]
8340  _args, sz = _to_ast_array(args1)
8341  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8342 
def AtLeast(args)
Definition: z3py.py:8326
def z3_debug()
Definition: z3py.py:56
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ AtMost()

def z3py.AtMost (   args)
Create an at-most Pseudo-Boolean k constraint.

>>> a, b, c = Bools('a b c')
>>> f = AtMost(a, b, c, 2)

Definition at line 8309 of file z3py.py.

8309 def AtMost(*args):
8310  """Create an at-most Pseudo-Boolean k constraint.
8311 
8312  >>> a, b, c = Bools('a b c')
8313  >>> f = AtMost(a, b, c, 2)
8314  """
8315  args = _get_args(args)
8316  if z3_debug():
8317  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8318  ctx = _ctx_from_ast_arg_list(args)
8319  if z3_debug():
8320  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8321  args1 = _coerce_expr_list(args[:-1], ctx)
8322  k = args[-1]
8323  _args, sz = _to_ast_array(args1)
8324  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8325 
def AtMost(args)
Definition: z3py.py:8309
def z3_debug()
Definition: z3py.py:56
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ BitVec()

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 3770 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().

3770 def BitVec(name, bv, ctx=None):
3771  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3772  If `ctx=None`, then the global context is used.
3773 
3774  >>> x = BitVec('x', 16)
3775  >>> is_bv(x)
3776  True
3777  >>> x.size()
3778  16
3779  >>> x.sort()
3780  BitVec(16)
3781  >>> word = BitVecSort(16)
3782  >>> x2 = BitVec('x', word)
3783  >>> eq(x, x2)
3784  True
3785  """
3786  if isinstance(bv, BitVecSortRef):
3787  ctx = bv.ctx
3788  else:
3789  ctx = _get_ctx(ctx)
3790  bv = BitVecSort(bv, ctx)
3791  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
3792 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def BitVec(name, bv, ctx=None)
Definition: z3py.py:3770
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740

◆ BitVecs()

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 3793 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().

3793 def BitVecs(names, bv, ctx=None):
3794  """Return a tuple of bit-vector constants of size bv.
3795 
3796  >>> x, y, z = BitVecs('x y z', 16)
3797  >>> x.size()
3798  16
3799  >>> x.sort()
3800  BitVec(16)
3801  >>> Sum(x, y, z)
3802  0 + x + y + z
3803  >>> Product(x, y, z)
3804  1*x*y*z
3805  >>> simplify(Product(x, y, z))
3806  x*y*z
3807  """
3808  ctx = _get_ctx(ctx)
3809  if isinstance(names, str):
3810  names = names.split(" ")
3811  return [BitVec(name, bv, ctx) for name in names]
3812 
def BitVec(name, bv, ctx=None)
Definition: z3py.py:3770
def BitVecs(names, bv, ctx=None)
Definition: z3py.py:3793

◆ BitVecSort()

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

Referenced by BitVec(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), BitVecRef.sort(), Sort.translate(), and Sort.Translate().

3740 def BitVecSort(sz, ctx=None):
3741  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3742 
3743  >>> Byte = BitVecSort(8)
3744  >>> Word = BitVecSort(16)
3745  >>> Byte
3746  BitVec(8)
3747  >>> x = Const('x', Byte)
3748  >>> eq(x, BitVec('x', 8))
3749  True
3750  """
3751  ctx = _get_ctx(ctx)
3752  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
3753 
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740

◆ BitVecVal()

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

Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), Concat(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().

3754 def BitVecVal(val, bv, ctx=None):
3755  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3756 
3757  >>> v = BitVecVal(10, 32)
3758  >>> v
3759  10
3760  >>> print("0x%.8x" % v.as_long())
3761  0x0000000a
3762  """
3763  if is_bv_sort(bv):
3764  ctx = bv.ctx
3765  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3766  else:
3767  ctx = _get_ctx(ctx)
3768  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3769 
def BitVecVal(val, bv, ctx=None)
Definition: z3py.py:3754
def is_bv_sort(s)
Definition: z3py.py:3222
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ Bool()

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

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

1568 def Bool(name, ctx=None):
1569  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1570 
1571  >>> p = Bool('p')
1572  >>> q = Bool('q')
1573  >>> And(p, q)
1574  And(p, q)
1575  """
1576  ctx = _get_ctx(ctx)
1577  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1578 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def Bool(name, ctx=None)
Definition: z3py.py:1568
def BoolSort(ctx=None)
Definition: z3py.py:1533

◆ Bools()

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

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

1579 def Bools(names, ctx=None):
1580  """Return a tuple of Boolean constants.
1581 
1582  `names` is a single string containing all names separated by blank spaces.
1583  If `ctx=None`, then the global context is used.
1584 
1585  >>> p, q, r = Bools('p q r')
1586  >>> And(p, Or(q, r))
1587  And(p, Or(q, r))
1588  """
1589  ctx = _get_ctx(ctx)
1590  if isinstance(names, str):
1591  names = names.split(" ")
1592  return [Bool(name, ctx) for name in names]
1593 
def Bools(names, ctx=None)
Definition: z3py.py:1579
def Bool(name, ctx=None)
Definition: z3py.py:1568

◆ BoolSort()

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

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

1533 def BoolSort(ctx=None):
1534  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1535 
1536  >>> BoolSort()
1537  Bool
1538  >>> p = Const('p', BoolSort())
1539  >>> is_bool(p)
1540  True
1541  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1542  >>> r(0, 1)
1543  r(0, 1)
1544  >>> is_bool(r(0, 1))
1545  True
1546  """
1547  ctx = _get_ctx(ctx)
1548  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1549 
def is_bool(a)
Definition: z3py.py:1422
def BoolSort(ctx=None)
Definition: z3py.py:1533

◆ BoolVal()

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

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

1550 def BoolVal(val, ctx=None):
1551  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1552 
1553  >>> BoolVal(True)
1554  True
1555  >>> is_true(BoolVal(True))
1556  True
1557  >>> is_true(True)
1558  False
1559  >>> is_false(BoolVal(False))
1560  True
1561  """
1562  ctx = _get_ctx(ctx)
1563  if val == False:
1564  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1565  else:
1566  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1567 
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
def BoolVal(val, ctx=None)
Definition: z3py.py:1550

◆ BoolVector()

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

Referenced by And(), and Or().

1594 def BoolVector(prefix, sz, ctx=None):
1595  """Return a list of Boolean constants of size `sz`.
1596 
1597  The constants are named using the given prefix.
1598  If `ctx=None`, then the global context is used.
1599 
1600  >>> P = BoolVector('p', 3)
1601  >>> P
1602  [p__0, p__1, p__2]
1603  >>> And(P)
1604  And(p__0, p__1, p__2)
1605  """
1606  return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
1607 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def BoolVector(prefix, sz, ctx=None)
Definition: z3py.py:1594
def Bool(name, ctx=None)
Definition: z3py.py:1568

◆ BV2Int()

def z3py.BV2Int (   a,
  is_signed = False 
)
Return the Z3 expression BV2Int(a).

>>> b = BitVec('b', 3)
>>> BV2Int(b).sort()
Int
>>> x = Int('x')
>>> x > BV2Int(b)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=False)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=True)
x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
>>> solve(x > BV2Int(b), b == 1, x < 3)
[x = 2, b = 1]

Definition at line 3710 of file z3py.py.

3710 def BV2Int(a, is_signed=False):
3711  """Return the Z3 expression BV2Int(a).
3712 
3713  >>> b = BitVec('b', 3)
3714  >>> BV2Int(b).sort()
3715  Int
3716  >>> x = Int('x')
3717  >>> x > BV2Int(b)
3718  x > BV2Int(b)
3719  >>> x > BV2Int(b, is_signed=False)
3720  x > BV2Int(b)
3721  >>> x > BV2Int(b, is_signed=True)
3722  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3723  >>> solve(x > BV2Int(b), b == 1, x < 3)
3724  [x = 2, b = 1]
3725  """
3726  if z3_debug():
3727  _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
3728  ctx = a.ctx
3729 
3730  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3731 
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, 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 z3_debug()
Definition: z3py.py:56
def BV2Int(a, is_signed=False)
Definition: z3py.py:3710
def is_bv(a)
Definition: z3py.py:3683

◆ BVAddNoOverflow()

def z3py.BVAddNoOverflow (   a,
  b,
  signed 
)
A predicate the determines that bit-vector addition does not overflow

Definition at line 4165 of file z3py.py.

4165 def BVAddNoOverflow(a, b, signed):
4166  """A predicate the determines that bit-vector addition does not overflow"""
4167  _check_bv_args(a, b)
4168  a, b = _coerce_exprs(a, b)
4169  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4170 
def BVAddNoOverflow(a, b, signed)
Definition: z3py.py:4165
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

◆ BVAddNoUnderflow()

def z3py.BVAddNoUnderflow (   a,
  b 
)
A predicate the determines that signed bit-vector addition does not underflow

Definition at line 4171 of file z3py.py.

4171 def BVAddNoUnderflow(a, b):
4172  """A predicate the determines that signed bit-vector addition does not underflow"""
4173  _check_bv_args(a, b)
4174  a, b = _coerce_exprs(a, b)
4175  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4176 
def BVAddNoUnderflow(a, b)
Definition: z3py.py:4171
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow...

◆ BVMulNoOverflow()

def z3py.BVMulNoOverflow (   a,
  b,
  signed 
)
A predicate the determines that bit-vector multiplication does not overflow

Definition at line 4202 of file z3py.py.

4202 def BVMulNoOverflow(a, b, signed):
4203  """A predicate the determines that bit-vector multiplication does not overflow"""
4204  _check_bv_args(a, b)
4205  a, b = _coerce_exprs(a, b)
4206  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4207 
4208 
def BVMulNoOverflow(a, b, signed)
Definition: z3py.py:4202
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow...

◆ BVMulNoUnderflow()

def z3py.BVMulNoUnderflow (   a,
  b 
)
A predicate the determines that bit-vector signed multiplication does not underflow

Definition at line 4209 of file z3py.py.

4209 def BVMulNoUnderflow(a, b):
4210  """A predicate the determines that bit-vector signed multiplication does not underflow"""
4211  _check_bv_args(a, b)
4212  a, b = _coerce_exprs(a, b)
4213  return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4214 
4215 
4216 
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
def BVMulNoUnderflow(a, b)
Definition: z3py.py:4209

◆ BVRedAnd()

def z3py.BVRedAnd (   a)
Return the reduction-and expression of `a`.

Definition at line 4153 of file z3py.py.

4153 def BVRedAnd(a):
4154  """Return the reduction-and expression of `a`."""
4155  if z3_debug():
4156  _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
4157  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4158 
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
def BVRedAnd(a)
Definition: z3py.py:4153
def z3_debug()
Definition: z3py.py:56
def is_bv(a)
Definition: z3py.py:3683

◆ BVRedOr()

def z3py.BVRedOr (   a)
Return the reduction-or expression of `a`.

Definition at line 4159 of file z3py.py.

4159 def BVRedOr(a):
4160  """Return the reduction-or expression of `a`."""
4161  if z3_debug():
4162  _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
4163  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4164 
def BVRedOr(a)
Definition: z3py.py:4159
def z3_debug()
Definition: z3py.py:56
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
def is_bv(a)
Definition: z3py.py:3683

◆ BVSDivNoOverflow()

def z3py.BVSDivNoOverflow (   a,
  b 
)
A predicate the determines that bit-vector signed division does not overflow

Definition at line 4190 of file z3py.py.

4190 def BVSDivNoOverflow(a, b):
4191  """A predicate the determines that bit-vector signed division does not overflow"""
4192  _check_bv_args(a, b)
4193  a, b = _coerce_exprs(a, b)
4194  return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4195 
def BVSDivNoOverflow(a, b)
Definition: z3py.py:4190
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow...

◆ BVSNegNoOverflow()

def z3py.BVSNegNoOverflow (   a)
A predicate the determines that bit-vector unary negation does not overflow

Definition at line 4196 of file z3py.py.

4196 def BVSNegNoOverflow(a):
4197  """A predicate the determines that bit-vector unary negation does not overflow"""
4198  if z3_debug():
4199  _z3_assert(is_bv(a), "Argument should be a bit-vector")
4200  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4201 
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector...
def z3_debug()
Definition: z3py.py:56
def BVSNegNoOverflow(a)
Definition: z3py.py:4196
def is_bv(a)
Definition: z3py.py:3683

◆ BVSubNoOverflow()

def z3py.BVSubNoOverflow (   a,
  b 
)
A predicate the determines that bit-vector subtraction does not overflow

Definition at line 4177 of file z3py.py.

4177 def BVSubNoOverflow(a, b):
4178  """A predicate the determines that bit-vector subtraction does not overflow"""
4179  _check_bv_args(a, b)
4180  a, b = _coerce_exprs(a, b)
4181  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4182 
4183 
def BVSubNoOverflow(a, b)
Definition: z3py.py:4177
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow...

◆ BVSubNoUnderflow()

def z3py.BVSubNoUnderflow (   a,
  b,
  signed 
)
A predicate the determines that bit-vector subtraction does not underflow

Definition at line 4184 of file z3py.py.

4184 def BVSubNoUnderflow(a, b, signed):
4185  """A predicate the determines that bit-vector subtraction does not underflow"""
4186  _check_bv_args(a, b)
4187  a, b = _coerce_exprs(a, b)
4188  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4189 
def BVSubNoUnderflow(a, b, signed)
Definition: z3py.py:4184
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow...

◆ Cbrt()

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

3172 def Cbrt(a, ctx=None):
3173  """ Return a Z3 expression which represents the cubic root of a.
3174 
3175  >>> x = Real('x')
3176  >>> Cbrt(x)
3177  x**(1/3)
3178  """
3179  if not is_expr(a):
3180  ctx = _get_ctx(ctx)
3181  a = RealVal(a, ctx)
3182  return a ** "1/3"
3183 
def Cbrt(a, ctx=None)
Definition: z3py.py:3172
def RealVal(val, ctx=None)
Definition: z3py.py:2965
def is_expr(a)
Definition: z3py.py:1115

◆ Complement()

def z3py.Complement (   re)
Create the complement regular expression.

Definition at line 10384 of file z3py.py.

10384 def Complement(re):
10385  """Create the complement regular expression."""
10386  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
10387 
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
def Complement(re)
Definition: z3py.py:10384

◆ Concat()

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

Referenced by Contains(), and BitVecRef.size().

3813 def Concat(*args):
3814  """Create a Z3 bit-vector concatenation expression.
3815 
3816  >>> v = BitVecVal(1, 4)
3817  >>> Concat(v, v+1, v)
3818  Concat(Concat(1, 1 + 1), 1)
3819  >>> simplify(Concat(v, v+1, v))
3820  289
3821  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3822  121
3823  """
3824  args = _get_args(args)
3825  sz = len(args)
3826  if z3_debug():
3827  _z3_assert(sz >= 2, "At least two arguments expected.")
3828 
3829  ctx = None
3830  for a in args:
3831  if is_expr(a):
3832  ctx = a.ctx
3833  break
3834  if is_seq(args[0]) or isinstance(args[0], str):
3835  args = [_coerce_seq(s, ctx) for s in args]
3836  if z3_debug():
3837  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
3838  v = (Ast * sz)()
3839  for i in range(sz):
3840  v[i] = args[i].as_ast()
3841  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
3842 
3843  if is_re(args[0]):
3844  if z3_debug():
3845  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
3846  v = (Ast * sz)()
3847  for i in range(sz):
3848  v[i] = args[i].as_ast()
3849  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
3850 
3851  if z3_debug():
3852  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
3853  r = args[0]
3854  for i in range(sz - 1):
3855  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3856  return r
3857 
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
def is_re(s)
Definition: z3py.py:10307
def z3_debug()
Definition: z3py.py:56
def is_expr(a)
Definition: z3py.py:1115
def is_bv(a)
Definition: z3py.py:3683
def Concat(args)
Definition: z3py.py:3813
def is_seq(a)
Definition: z3py.py:10052

◆ Cond()

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

Referenced by If().

8164 def Cond(p, t1, t2, ctx=None):
8165  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8166 
8167  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8168  """
8169  p = _to_probe(p, ctx)
8170  t1 = _to_tactic(t1, ctx)
8171  t2 = _to_tactic(t2, ctx)
8172  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8173 
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8164
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, 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...

◆ Const()

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

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

Definition at line 1301 of file z3py.py.

Referenced by BitVecSort(), Consts(), FPSort(), IntSort(), IsMember(), IsSubset(), RealSort(), DatatypeSortRef.recognizer(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().

1301 def Const(name, sort):
1302  """Create a constant of the given sort.
1303 
1304  >>> Const('x', IntSort())
1305  x
1306  """
1307  if z3_debug():
1308  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1309  ctx = sort.ctx
1310  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1311 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def Const(name, sort)
Definition: z3py.py:1301
def z3_debug()
Definition: z3py.py:56

◆ Consts()

def z3py.Consts (   names,
  sort 
)
Create 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 1312 of file z3py.py.

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

1312 def Consts(names, sort):
1313  """Create several constants of the given sort.
1314 
1315  `names` is a string containing the names of all constants to be created.
1316  Blank spaces separate the names of different constants.
1317 
1318  >>> x, y, z = Consts('x y z', IntSort())
1319  >>> x + y + z
1320  x + y + z
1321  """
1322  if isinstance(names, str):
1323  names = names.split(" ")
1324  return [Const(name, sort) for name in names]
1325 
def Consts(names, sort)
Definition: z3py.py:1312
def Const(name, sort)
Definition: z3py.py:1301

◆ Contains()

def z3py.Contains (   a,
  b 
)
Check if 'a' contains 'b'
>>> s1 = Contains("abc", "ab")
>>> simplify(s1)
True
>>> s2 = Contains("abc", "bc")
>>> simplify(s2)
True
>>> x, y, z = Strings('x y z')
>>> s3 = Contains(Concat(x,y,z), y)
>>> simplify(s3)
True

Definition at line 10178 of file z3py.py.

10178 def Contains(a, b):
10179  """Check if 'a' contains 'b'
10180  >>> s1 = Contains("abc", "ab")
10181  >>> simplify(s1)
10182  True
10183  >>> s2 = Contains("abc", "bc")
10184  >>> simplify(s2)
10185  True
10186  >>> x, y, z = Strings('x y z')
10187  >>> s3 = Contains(Concat(x,y,z), y)
10188  >>> simplify(s3)
10189  True
10190  """
10191  ctx = _get_ctx2(a, b)
10192  a = _coerce_seq(a, ctx)
10193  b = _coerce_seq(b, ctx)
10194  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10195 
10196 
def Contains(a, b)
Definition: z3py.py:10178
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.

◆ CreateDatatypes()

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

Referenced by Datatype.create().

4782 def CreateDatatypes(*ds):
4783  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4784 
4785  In the following example we define a Tree-List using two mutually recursive datatypes.
4786 
4787  >>> TreeList = Datatype('TreeList')
4788  >>> Tree = Datatype('Tree')
4789  >>> # Tree has two constructors: leaf and node
4790  >>> Tree.declare('leaf', ('val', IntSort()))
4791  >>> # a node contains a list of trees
4792  >>> Tree.declare('node', ('children', TreeList))
4793  >>> TreeList.declare('nil')
4794  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4795  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4796  >>> Tree.val(Tree.leaf(10))
4797  val(leaf(10))
4798  >>> simplify(Tree.val(Tree.leaf(10)))
4799  10
4800  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4801  >>> n1
4802  node(cons(leaf(10), cons(leaf(20), nil)))
4803  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4804  >>> simplify(n2 == n1)
4805  False
4806  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4807  True
4808  """
4809  ds = _get_args(ds)
4810  if z3_debug():
4811  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4812  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
4813  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
4814  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
4815  ctx = ds[0].ctx
4816  num = len(ds)
4817  names = (Symbol * num)()
4818  out = (Sort * num)()
4819  clists = (ConstructorList * num)()
4820  to_delete = []
4821  for i in range(num):
4822  d = ds[i]
4823  names[i] = to_symbol(d.name, ctx)
4824  num_cs = len(d.constructors)
4825  cs = (Constructor * num_cs)()
4826  for j in range(num_cs):
4827  c = d.constructors[j]
4828  cname = to_symbol(c[0], ctx)
4829  rname = to_symbol(c[1], ctx)
4830  fs = c[2]
4831  num_fs = len(fs)
4832  fnames = (Symbol * num_fs)()
4833  sorts = (Sort * num_fs)()
4834  refs = (ctypes.c_uint * num_fs)()
4835  for k in range(num_fs):
4836  fname = fs[k][0]
4837  ftype = fs[k][1]
4838  fnames[k] = to_symbol(fname, ctx)
4839  if isinstance(ftype, Datatype):
4840  if z3_debug():
4841  _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4842  sorts[k] = None
4843  refs[k] = ds.index(ftype)
4844  else:
4845  if z3_debug():
4846  _z3_assert(is_sort(ftype), "Z3 sort expected")
4847  sorts[k] = ftype.ast
4848  refs[k] = 0
4849  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4850  to_delete.append(ScopedConstructor(cs[j], ctx))
4851  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4852  to_delete.append(ScopedConstructorList(clists[i], ctx))
4853  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4854  result = []
4855 
4856  for i in range(num):
4857  dref = DatatypeSortRef(out[i], ctx)
4858  num_cs = dref.num_constructors()
4859  for j in range(num_cs):
4860  cref = dref.constructor(j)
4861  cref_name = cref.name()
4862  cref_arity = cref.arity()
4863  if cref.arity() == 0:
4864  cref = cref()
4865  setattr(dref, cref_name, cref)
4866  rref = dref.recognizer(j)
4867  setattr(dref, "is_" + cref_name, rref)
4868  for k in range(cref_arity):
4869  aref = dref.accessor(j, k)
4870  setattr(dref, aref.name(), aref)
4871  result.append(dref)
4872  return tuple(result)
4873 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def to_symbol(s, ctx=None)
Definition: z3py.py:109
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
def CreateDatatypes(ds)
Definition: z3py.py:4782
def is_sort(s)
Definition: z3py.py:596
def z3_debug()
Definition: z3py.py:56
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.

◆ DeclareSort()

def z3py.DeclareSort (   name,
  ctx = None 
)
Create a new uninterpreted 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 637 of file z3py.py.

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

637 def DeclareSort(name, ctx=None):
638  """Create a new uninterpreted sort named `name`.
639 
640  If `ctx=None`, then the new sort is declared in the global Z3Py context.
641 
642  >>> A = DeclareSort('A')
643  >>> a = Const('a', A)
644  >>> b = Const('b', A)
645  >>> a.sort() == A
646  True
647  >>> b.sort() == A
648  True
649  >>> a == b
650  a == b
651  """
652  ctx = _get_ctx(ctx)
653  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
654 
def to_symbol(s, ctx=None)
Definition: z3py.py:109
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
def DeclareSort(name, ctx=None)
Definition: z3py.py:637

◆ Default()

def z3py.Default (   a)
Return a default value for array expression.
>>> b = K(IntSort(), 1)
>>> prove(Default(b) == 1)
proved

Definition at line 4437 of file z3py.py.

Referenced by is_default().

4437 def Default(a):
4438  """ Return a default value for array expression.
4439  >>> b = K(IntSort(), 1)
4440  >>> prove(Default(b) == 1)
4441  proved
4442  """
4443  if z3_debug():
4444  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4445  return a.default()
4446 
4447 
def is_array_sort(a)
Definition: z3py.py:4290
def Default(a)
Definition: z3py.py:4437
def z3_debug()
Definition: z3py.py:56

◆ describe_probes()

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

Definition at line 8094 of file z3py.py.

8094 def describe_probes():
8095  """Display a (tabular) description of all available probes in Z3."""
8096  if in_html_mode():
8097  even = True
8098  print('<table border="1" cellpadding="2" cellspacing="0">')
8099  for p in probes():
8100  if even:
8101  print('<tr style="background-color:#CFCFCF">')
8102  even = False
8103  else:
8104  print('<tr>')
8105  even = True
8106  print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
8107  print('</table>')
8108  else:
8109  for p in probes():
8110  print('%s : %s' % (p, probe_description(p)))
8111 
def probes(ctx=None)
Definition: z3py.py:8076
def probe_description(name, ctx=None)
Definition: z3py.py:8086
def describe_probes()
Definition: z3py.py:8094

◆ describe_tactics()

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

Definition at line 7903 of file z3py.py.

7903 def describe_tactics():
7904  """Display a (tabular) description of all available tactics in Z3."""
7905  if in_html_mode():
7906  even = True
7907  print('<table border="1" cellpadding="2" cellspacing="0">')
7908  for t in tactics():
7909  if even:
7910  print('<tr style="background-color:#CFCFCF">')
7911  even = False
7912  else:
7913  print('<tr>')
7914  even = True
7915  print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
7916  print('</table>')
7917  else:
7918  for t in tactics():
7919  print('%s : %s' % (t, tactic_description(t)))
7920 
def tactics(ctx=None)
Definition: z3py.py:7885
def tactic_description(name, ctx=None)
Definition: z3py.py:7895
def describe_tactics()
Definition: z3py.py:7903

◆ disable_trace()

def z3py.disable_trace (   msg)

Definition at line 70 of file z3py.py.

70 def disable_trace(msg):
71  Z3_disable_trace(msg)
72 
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def disable_trace(msg)
Definition: z3py.py:70

◆ DisjointSum()

def z3py.DisjointSum (   name,
  sorts,
  ctx = None 
)
Create a named tagged union sort base on a set of underlying sorts
Example:
    >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])

Definition at line 4982 of file z3py.py.

4982 def DisjointSum(name, sorts, ctx=None):
4983  """Create a named tagged union sort base on a set of underlying sorts
4984  Example:
4985  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
4986  """
4987  sum = Datatype(name, ctx)
4988  for i in range(len(sorts)):
4989  sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
4990  sum = sum.create()
4991  return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
4992 
4993 
def DisjointSum(name, sorts, ctx=None)
Definition: z3py.py:4982
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370

◆ Distinct()

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

1270 def Distinct(*args):
1271  """Create a Z3 distinct expression.
1272 
1273  >>> x = Int('x')
1274  >>> y = Int('y')
1275  >>> Distinct(x, y)
1276  x != y
1277  >>> z = Int('z')
1278  >>> Distinct(x, y, z)
1279  Distinct(x, y, z)
1280  >>> simplify(Distinct(x, y, z))
1281  Distinct(x, y, z)
1282  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1283  And(Not(x == y), Not(x == z), Not(y == z))
1284  """
1285  args = _get_args(args)
1286  ctx = _ctx_from_ast_arg_list(args)
1287  if z3_debug():
1288  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
1289  args = _coerce_expr_list(args, ctx)
1290  _args, sz = _to_ast_array(args)
1291  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1292 
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
def z3_debug()
Definition: z3py.py:56
def Distinct(args)
Definition: z3py.py:1270

◆ Empty()

def z3py.Empty (   s)
Create the empty sequence of the given sort
>>> e = Empty(StringSort())
>>> e2 = StringVal("")
>>> print(e.eq(e2))
True
>>> e3 = Empty(SeqSort(IntSort()))
>>> print(e3)
Empty(Seq(Int))
>>> e4 = Empty(ReSort(SeqSort(IntSort())))
>>> print(e4)
Empty(ReSort(Seq(Int)))

Definition at line 10113 of file z3py.py.

10113 def Empty(s):
10114  """Create the empty sequence of the given sort
10115  >>> e = Empty(StringSort())
10116  >>> e2 = StringVal("")
10117  >>> print(e.eq(e2))
10118  True
10119  >>> e3 = Empty(SeqSort(IntSort()))
10120  >>> print(e3)
10121  Empty(Seq(Int))
10122  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10123  >>> print(e4)
10124  Empty(ReSort(Seq(Int)))
10125  """
10126  if isinstance(s, SeqSortRef):
10127  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10128  if isinstance(s, ReSortRef):
10129  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10130  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10131 
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
def Empty(s)
Definition: z3py.py:10113

◆ EmptySet()

def z3py.EmptySet (   s)
Create the empty set
>>> EmptySet(IntSort())
K(Int, False)

Definition at line 4572 of file z3py.py.

4572 def EmptySet(s):
4573  """Create the empty set
4574  >>> EmptySet(IntSort())
4575  K(Int, False)
4576  """
4577  ctx = s.ctx
4578  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4579 
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
def EmptySet(s)
Definition: z3py.py:4572

◆ enable_trace()

def z3py.enable_trace (   msg)

Definition at line 67 of file z3py.py.

67 def enable_trace(msg):
68  Z3_enable_trace(msg)
69 
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def enable_trace(msg)
Definition: z3py.py:67

◆ EnumSort()

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

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

4994 def EnumSort(name, values, ctx=None):
4995  """Return a new enumeration sort named `name` containing the given values.
4996 
4997  The result is a pair (sort, list of constants).
4998  Example:
4999  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5000  """
5001  if z3_debug():
5002  _z3_assert(isinstance(name, str), "Name must be a string")
5003  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
5004  _z3_assert(len(values) > 0, "At least one value expected")
5005  ctx = _get_ctx(ctx)
5006  num = len(values)
5007  _val_names = (Symbol * num)()
5008  for i in range(num):
5009  _val_names[i] = to_symbol(values[i])
5010  _values = (FuncDecl * num)()
5011  _testers = (FuncDecl * num)()
5012  name = to_symbol(name)
5013  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5014  V = []
5015  for i in range(num):
5016  V.append(FuncDeclRef(_values[i], ctx))
5017  V = [a() for a in V]
5018  return S, V
5019 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def z3_debug()
Definition: z3py.py:56
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4994
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.

◆ eq()

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

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

432 def eq(a, b):
433  """Return `True` if `a` and `b` are structurally identical AST nodes.
434 
435  >>> x = Int('x')
436  >>> y = Int('y')
437  >>> eq(x, y)
438  False
439  >>> eq(x + 1, x + 1)
440  True
441  >>> eq(x + 1, 1 + x)
442  False
443  >>> eq(simplify(x + 1), simplify(1 + x))
444  True
445  """
446  if z3_debug():
447  _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
448  return a.eq(b)
449 
def eq(a, b)
Definition: z3py.py:432
def z3_debug()
Definition: z3py.py:56
def is_ast(a)
Definition: z3py.py:412

◆ Exists()

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.


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

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

2061 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2062  """Create a Z3 exists formula.
2063 
2064  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2065 
2066 
2067  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2068  >>> x = Int('x')
2069  >>> y = Int('y')
2070  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2071  >>> q
2072  Exists([x, y], f(x, y) >= x)
2073  >>> is_quantifier(q)
2074  True
2075  >>> r = Tactic('nnf')(q).as_expr()
2076  >>> is_quantifier(r)
2077  False
2078  """
2079  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2080 
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2061

◆ Ext()

def z3py.Ext (   a,
  b 
)
Return extensionality index for one-dimensional arrays.
>> a, b = Consts('a b', SetSort(IntSort()))
>> Ext(a, b)
Ext(a, b)

Definition at line 4522 of file z3py.py.

4522 def Ext(a, b):
4523  """Return extensionality index for one-dimensional arrays.
4524  >> a, b = Consts('a b', SetSort(IntSort()))
4525  >> Ext(a, b)
4526  Ext(a, b)
4527  """
4528  ctx = a.ctx
4529  if z3_debug():
4530  _z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays")
4531  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4532 
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
def is_array_sort(a)
Definition: z3py.py:4290
def is_array(a)
Definition: z3py.py:4294
def z3_debug()
Definition: z3py.py:56
def Ext(a, b)
Definition: z3py.py:4522

◆ Extract()

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

>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)
>>> simplify(Extract(StringVal("abcd"),2,1))
"c"

Definition at line 3858 of file z3py.py.

3858 def Extract(high, low, a):
3859  """Create a Z3 bit-vector extraction expression, or create a string extraction expression.
3860 
3861  >>> x = BitVec('x', 8)
3862  >>> Extract(6, 2, x)
3863  Extract(6, 2, x)
3864  >>> Extract(6, 2, x).sort()
3865  BitVec(5)
3866  >>> simplify(Extract(StringVal("abcd"),2,1))
3867  "c"
3868  """
3869  if isinstance(high, str):
3870  high = StringVal(high)
3871  if is_seq(high):
3872  s = high
3873  offset, length = _coerce_exprs(low, a, s.ctx)
3874  return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
3875  if z3_debug():
3876  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3877  _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")
3878  _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
3879  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
3880 
def Extract(high, low, a)
Definition: z3py.py:3858
def StringVal(s, ctx=None)
Definition: z3py.py:10078
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
def z3_debug()
Definition: z3py.py:56
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n...
def is_bv(a)
Definition: z3py.py:3683
def is_seq(a)
Definition: z3py.py:10052

◆ FailIf()

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

8127 def FailIf(p, ctx=None):
8128  """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8129 
8130  In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
8131 
8132  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8133  >>> x, y = Ints('x y')
8134  >>> g = Goal()
8135  >>> g.add(x > 0)
8136  >>> g.add(y > 0)
8137  >>> t(g)
8138  [[x > 0, y > 0]]
8139  >>> g.add(x == y + 1)
8140  >>> t(g)
8141  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8142  """
8143  p = _to_probe(p, ctx)
8144  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8145 
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
def FailIf(p, ctx=None)
Definition: z3py.py:8127

◆ FiniteDomainSort()

def z3py.FiniteDomainSort (   name,
  sz,
  ctx = None 
)
Create a named finite domain sort of a given size sz

Definition at line 7219 of file z3py.py.

Referenced by Context.mkFiniteDomainSort(), Context.MkFiniteDomainSort(), Sort.translate(), and Sort.Translate().

7219 def FiniteDomainSort(name, sz, ctx=None):
7220  """Create a named finite domain sort of a given size sz"""
7221  if not isinstance(name, Symbol):
7222  name = to_symbol(name)
7223  ctx = _get_ctx(ctx)
7224  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7225 
def to_symbol(s, ctx=None)
Definition: z3py.py:109
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)
Create a named finite domain sort.
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7219

◆ FiniteDomainVal()

def z3py.FiniteDomainVal (   val,
  sort,
  ctx = None 
)
Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.

>>> s = FiniteDomainSort('S', 256)
>>> FiniteDomainVal(255, s)
255
>>> FiniteDomainVal('100', s)
100

Definition at line 7287 of file z3py.py.

7287 def FiniteDomainVal(val, sort, ctx=None):
7288  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7289 
7290  >>> s = FiniteDomainSort('S', 256)
7291  >>> FiniteDomainVal(255, s)
7292  255
7293  >>> FiniteDomainVal('100', s)
7294  100
7295  """
7296  if z3_debug():
7297  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" )
7298  ctx = sort.ctx
7299  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7300 
def is_finite_domain_sort(s)
Definition: z3py.py:7226
def FiniteDomainVal(val, sort, ctx=None)
Definition: z3py.py:7287
def z3_debug()
Definition: z3py.py:56
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ Float128()

def z3py.Float128 (   ctx = None)
Floating-point 128-bit (quadruple) sort.

Definition at line 8757 of file z3py.py.

8757 def Float128(ctx=None):
8758  """Floating-point 128-bit (quadruple) sort."""
8759  ctx = _get_ctx(ctx)
8760  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
8761 
def Float128(ctx=None)
Definition: z3py.py:8757
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.

◆ Float16()

def z3py.Float16 (   ctx = None)
Floating-point 16-bit (half) sort.

Definition at line 8727 of file z3py.py.

8727 def Float16(ctx=None):
8728  """Floating-point 16-bit (half) sort."""
8729  ctx = _get_ctx(ctx)
8730  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
8731 
def Float16(ctx=None)
Definition: z3py.py:8727
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.

◆ Float32()

def z3py.Float32 (   ctx = None)
Floating-point 32-bit (single) sort.

Definition at line 8737 of file z3py.py.

Referenced by FPRef.__neg__(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), and fpUnsignedToFP().

8737 def Float32(ctx=None):
8738  """Floating-point 32-bit (single) sort."""
8739  ctx = _get_ctx(ctx)
8740  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
8741 
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
def Float32(ctx=None)
Definition: z3py.py:8737

◆ Float64()

def z3py.Float64 (   ctx = None)
Floating-point 64-bit (double) sort.

Definition at line 8747 of file z3py.py.

Referenced by fpFPToFP(), and fpToFP().

8747 def Float64(ctx=None):
8748  """Floating-point 64-bit (double) sort."""
8749  ctx = _get_ctx(ctx)
8750  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
8751 
def Float64(ctx=None)
Definition: z3py.py:8747
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.

◆ FloatDouble()

def z3py.FloatDouble (   ctx = None)
Floating-point 64-bit (double) sort.

Definition at line 8752 of file z3py.py.

8752 def FloatDouble(ctx=None):
8753  """Floating-point 64-bit (double) sort."""
8754  ctx = _get_ctx(ctx)
8755  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
8756 
def FloatDouble(ctx=None)
Definition: z3py.py:8752
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.

◆ FloatHalf()

def z3py.FloatHalf (   ctx = None)
Floating-point 16-bit (half) sort.

Definition at line 8732 of file z3py.py.

8732 def FloatHalf(ctx=None):
8733  """Floating-point 16-bit (half) sort."""
8734  ctx = _get_ctx(ctx)
8735  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
8736 
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
def FloatHalf(ctx=None)
Definition: z3py.py:8732

◆ FloatQuadruple()

def z3py.FloatQuadruple (   ctx = None)
Floating-point 128-bit (quadruple) sort.

Definition at line 8762 of file z3py.py.

8762 def FloatQuadruple(ctx=None):
8763  """Floating-point 128-bit (quadruple) sort."""
8764  ctx = _get_ctx(ctx)
8765  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
8766 
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
def FloatQuadruple(ctx=None)
Definition: z3py.py:8762

◆ FloatSingle()

def z3py.FloatSingle (   ctx = None)
Floating-point 32-bit (single) sort.

Definition at line 8742 of file z3py.py.

8742 def FloatSingle(ctx=None):
8743  """Floating-point 32-bit (single) sort."""
8744  ctx = _get_ctx(ctx)
8745  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
8746 
def FloatSingle(ctx=None)
Definition: z3py.py:8742
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.

◆ ForAll()

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

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

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

Referenced by Fixedpoint.abstract(), QuantifierRef.body(), QuantifierRef.children(), QuantifierRef.is_exists(), 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().

2044 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2045  """Create a Z3 forall formula.
2046 
2047  The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2048 
2049  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2050  >>> x = Int('x')
2051  >>> y = Int('y')
2052  >>> ForAll([x, y], f(x, y) >= x)
2053  ForAll([x, y], f(x, y) >= x)
2054  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2055  ForAll([x, y], f(x, y) >= x)
2056  >>> ForAll([x, y], f(x, y) >= x, weight=10)
2057  ForAll([x, y], f(x, y) >= x)
2058  """
2059  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2060 
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2044

◆ FP()

def z3py.FP (   name,
  fpsort,
  ctx = None 
)
Return a floating-point constant named `name`.
`fpsort` is the floating-point sort.
If `ctx=None`, then the global context is used.

>>> x  = FP('x', FPSort(8, 24))
>>> is_fp(x)
True
>>> x.ebits()
8
>>> x.sort()
FPSort(8, 24)
>>> word = FPSort(8, 24)
>>> x2 = FP('x', word)
>>> eq(x, x2)
True

Definition at line 9342 of file z3py.py.

Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__neg__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), fpAdd(), fpDiv(), fpIsInf(), fpIsNaN(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), FPSort(), fpSub(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and FPRef.sort().

9342 def FP(name, fpsort, ctx=None):
9343  """Return a floating-point constant named `name`.
9344  `fpsort` is the floating-point sort.
9345  If `ctx=None`, then the global context is used.
9346 
9347  >>> x = FP('x', FPSort(8, 24))
9348  >>> is_fp(x)
9349  True
9350  >>> x.ebits()
9351  8
9352  >>> x.sort()
9353  FPSort(8, 24)
9354  >>> word = FPSort(8, 24)
9355  >>> x2 = FP('x', word)
9356  >>> eq(x, x2)
9357  True
9358  """
9359  if isinstance(fpsort, FPSortRef) and ctx is None:
9360  ctx = fpsort.ctx
9361  else:
9362  ctx = _get_ctx(ctx)
9363  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
9364 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def FP(name, fpsort, ctx=None)
Definition: z3py.py:9342

◆ fpAbs()

def z3py.fpAbs (   a,
  ctx = None 
)
Create a Z3 floating-point absolute value expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FPVal(1.0, s)
>>> fpAbs(x)
fpAbs(1)
>>> y = FPVal(-20.0, s)
>>> y
-1.25*(2**4)
>>> fpAbs(y)
fpAbs(-1.25*(2**4))
>>> fpAbs(-1.25*(2**4))
fpAbs(-1.25*(2**4))
>>> fpAbs(x).sort()
FPSort(8, 24)

Definition at line 9383 of file z3py.py.

9383 def fpAbs(a, ctx=None):
9384  """Create a Z3 floating-point absolute value expression.
9385 
9386  >>> s = FPSort(8, 24)
9387  >>> rm = RNE()
9388  >>> x = FPVal(1.0, s)
9389  >>> fpAbs(x)
9390  fpAbs(1)
9391  >>> y = FPVal(-20.0, s)
9392  >>> y
9393  -1.25*(2**4)
9394  >>> fpAbs(y)
9395  fpAbs(-1.25*(2**4))
9396  >>> fpAbs(-1.25*(2**4))
9397  fpAbs(-1.25*(2**4))
9398  >>> fpAbs(x).sort()
9399  FPSort(8, 24)
9400  """
9401  ctx = _get_ctx(ctx)
9402  [a] = _coerce_fp_expr_list([a], ctx)
9403  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
9404 
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
def fpAbs(a, ctx=None)
Definition: z3py.py:9383

◆ fpAdd()

def z3py.fpAdd (   rm,
  a,
  b,
  ctx = None 
)
Create a Z3 floating-point addition expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpAdd(rm, x, y)
fpAdd(RNE(), x, y)
>>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
x + y
>>> fpAdd(rm, x, y).sort()
FPSort(8, 24)

Definition at line 9465 of file z3py.py.

Referenced by FPs().

9465 def fpAdd(rm, a, b, ctx=None):
9466  """Create a Z3 floating-point addition expression.
9467 
9468  >>> s = FPSort(8, 24)
9469  >>> rm = RNE()
9470  >>> x = FP('x', s)
9471  >>> y = FP('y', s)
9472  >>> fpAdd(rm, x, y)
9473  fpAdd(RNE(), x, y)
9474  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
9475  x + y
9476  >>> fpAdd(rm, x, y).sort()
9477  FPSort(8, 24)
9478  """
9479  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
9480 
def fpAdd(rm, a, b, ctx=None)
Definition: z3py.py:9465

◆ fpBVToFP()

def z3py.fpBVToFP (   v,
  sort,
  ctx = None 
)
Create a Z3 floating-point conversion expression that represents the
conversion from a bit-vector term to a floating-point term.

>>> x_bv = BitVecVal(0x3F800000, 32)
>>> x_fp = fpBVToFP(x_bv, Float32())
>>> x_fp
fpToFP(1065353216)
>>> simplify(x_fp)
1

Definition at line 9761 of file z3py.py.

9761 def fpBVToFP(v, sort, ctx=None):
9762  """Create a Z3 floating-point conversion expression that represents the
9763  conversion from a bit-vector term to a floating-point term.
9764 
9765  >>> x_bv = BitVecVal(0x3F800000, 32)
9766  >>> x_fp = fpBVToFP(x_bv, Float32())
9767  >>> x_fp
9768  fpToFP(1065353216)
9769  >>> simplify(x_fp)
9770  1
9771  """
9772  _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.")
9773  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
9774  ctx = _get_ctx(ctx)
9775  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
9776 
def fpBVToFP(v, sort, ctx=None)
Definition: z3py.py:9761
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
def is_fp_sort(s)
Definition: z3py.py:8771
def is_bv(a)
Definition: z3py.py:3683

◆ fpDiv()

def z3py.fpDiv (   rm,
  a,
  b,
  ctx = None 
)
Create a Z3 floating-point division expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpDiv(rm, x, y)
fpDiv(RNE(), x, y)
>>> fpDiv(rm, x, y).sort()
FPSort(8, 24)

Definition at line 9509 of file z3py.py.

9509 def fpDiv(rm, a, b, ctx=None):
9510  """Create a Z3 floating-point division expression.
9511 
9512  >>> s = FPSort(8, 24)
9513  >>> rm = RNE()
9514  >>> x = FP('x', s)
9515  >>> y = FP('y', s)
9516  >>> fpDiv(rm, x, y)
9517  fpDiv(RNE(), x, y)
9518  >>> fpDiv(rm, x, y).sort()
9519  FPSort(8, 24)
9520  """
9521  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
9522 
def fpDiv(rm, a, b, ctx=None)
Definition: z3py.py:9509

◆ fpEQ()

def z3py.fpEQ (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `fpEQ(other, self)`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpEQ(x, y)
fpEQ(x, y)
>>> fpEQ(x, y).sexpr()
'(fp.eq x y)'

Definition at line 9673 of file z3py.py.

Referenced by fpFP(), and fpNEQ().

9673 def fpEQ(a, b, ctx=None):
9674  """Create the Z3 floating-point expression `fpEQ(other, self)`.
9675 
9676  >>> x, y = FPs('x y', FPSort(8, 24))
9677  >>> fpEQ(x, y)
9678  fpEQ(x, y)
9679  >>> fpEQ(x, y).sexpr()
9680  '(fp.eq x y)'
9681  """
9682  return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
9683 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:9673

◆ fpFMA()

def z3py.fpFMA (   rm,
  a,
  b,
  c,
  ctx = None 
)
Create a Z3 floating-point fused multiply-add expression.

Definition at line 9564 of file z3py.py.

9564 def fpFMA(rm, a, b, c, ctx=None):
9565  """Create a Z3 floating-point fused multiply-add expression.
9566  """
9567  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
9568 
def fpFMA(rm, a, b, c, ctx=None)
Definition: z3py.py:9564

◆ fpFP()

def z3py.fpFP (   sgn,
  exp,
  sig,
  ctx = None 
)
Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.

>>> s = FPSort(8, 24)
>>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
>>> print(x)
fpFP(1, 127, 4194304)
>>> xv = FPVal(-1.5, s)
>>> print(xv)
-1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
sat
>>> xv = FPVal(+1.5, s)
>>> print(xv)
1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
unsat

Definition at line 9695 of file z3py.py.

9695 def fpFP(sgn, exp, sig, ctx=None):
9696  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
9697 
9698  >>> s = FPSort(8, 24)
9699  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
9700  >>> print(x)
9701  fpFP(1, 127, 4194304)
9702  >>> xv = FPVal(-1.5, s)
9703  >>> print(xv)
9704  -1.5
9705  >>> slvr = Solver()
9706  >>> slvr.add(fpEQ(x, xv))
9707  >>> slvr.check()
9708  sat
9709  >>> xv = FPVal(+1.5, s)
9710  >>> print(xv)
9711  1.5
9712  >>> slvr = Solver()
9713  >>> slvr.add(fpEQ(x, xv))
9714  >>> slvr.check()
9715  unsat
9716  """
9717  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
9718  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
9719  ctx = _get_ctx(ctx)
9720  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
9721  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
9722 
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
def fpFP(sgn, exp, sig, ctx=None)
Definition: z3py.py:9695
def is_bv(a)
Definition: z3py.py:3683

◆ fpFPToFP()

def z3py.fpFPToFP (   rm,
  v,
  sort,
  ctx = None 
)
Create a Z3 floating-point conversion expression that represents the
conversion from a floating-point term to a floating-point term of different precision.

>>> x_sgl = FPVal(1.0, Float32())
>>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
>>> x_dbl
fpToFP(RNE(), 1)
>>> simplify(x_dbl)
1
>>> x_dbl.sort()
FPSort(11, 53)

Definition at line 9777 of file z3py.py.

9777 def fpFPToFP(rm, v, sort, ctx=None):
9778  """Create a Z3 floating-point conversion expression that represents the
9779  conversion from a floating-point term to a floating-point term of different precision.
9780 
9781  >>> x_sgl = FPVal(1.0, Float32())
9782  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
9783  >>> x_dbl
9784  fpToFP(RNE(), 1)
9785  >>> simplify(x_dbl)
9786  1
9787  >>> x_dbl.sort()
9788  FPSort(11, 53)
9789  """
9790  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9791  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
9792  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9793  ctx = _get_ctx(ctx)
9794  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9795 
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
def is_fp_sort(s)
Definition: z3py.py:8771
def fpFPToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9777
def is_fprm(a)
Definition: z3py.py:9018
def is_fp(a)
Definition: z3py.py:9154

◆ fpGEQ()

def z3py.fpGEQ (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `other >= self`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGEQ(x, y)
x >= y
>>> (x >= y).sexpr()
'(fp.geq x y)'

Definition at line 9662 of file z3py.py.

9662 def fpGEQ(a, b, ctx=None):
9663  """Create the Z3 floating-point expression `other >= self`.
9664 
9665  >>> x, y = FPs('x y', FPSort(8, 24))
9666  >>> fpGEQ(x, y)
9667  x >= y
9668  >>> (x >= y).sexpr()
9669  '(fp.geq x y)'
9670  """
9671  return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
9672 
def fpGEQ(a, b, ctx=None)
Definition: z3py.py:9662

◆ fpGT()

def z3py.fpGT (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `other > self`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGT(x, y)
x > y
>>> (x > y).sexpr()
'(fp.gt x y)'

Definition at line 9651 of file z3py.py.

9651 def fpGT(a, b, ctx=None):
9652  """Create the Z3 floating-point expression `other > self`.
9653 
9654  >>> x, y = FPs('x y', FPSort(8, 24))
9655  >>> fpGT(x, y)
9656  x > y
9657  >>> (x > y).sexpr()
9658  '(fp.gt x y)'
9659  """
9660  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
9661 
def fpGT(a, b, ctx=None)
Definition: z3py.py:9651

◆ fpInfinity()

def z3py.fpInfinity (   s,
  negative 
)
Create a Z3 floating-point +oo or -oo term.

Definition at line 9276 of file z3py.py.

9276 def fpInfinity(s, negative):
9277  """Create a Z3 floating-point +oo or -oo term."""
9278  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9279  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9280  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
9281 
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
def fpInfinity(s, negative)
Definition: z3py.py:9276

◆ fpIsInf()

def z3py.fpIsInf (   a,
  ctx = None 
)
Create a Z3 floating-point isInfinite expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> fpIsInf(x)
fpIsInf(x)

Definition at line 9590 of file z3py.py.

9590 def fpIsInf(a, ctx=None):
9591  """Create a Z3 floating-point isInfinite expression.
9592 
9593  >>> s = FPSort(8, 24)
9594  >>> x = FP('x', s)
9595  >>> fpIsInf(x)
9596  fpIsInf(x)
9597  """
9598  return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
9599 
def fpIsInf(a, ctx=None)
Definition: z3py.py:9590

◆ fpIsNaN()

def z3py.fpIsNaN (   a,
  ctx = None 
)
Create a Z3 floating-point isNaN expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpIsNaN(x)
fpIsNaN(x)

Definition at line 9579 of file z3py.py.

9579 def fpIsNaN(a, ctx=None):
9580  """Create a Z3 floating-point isNaN expression.
9581 
9582  >>> s = FPSort(8, 24)
9583  >>> x = FP('x', s)
9584  >>> y = FP('y', s)
9585  >>> fpIsNaN(x)
9586  fpIsNaN(x)
9587  """
9588  return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
9589 
def fpIsNaN(a, ctx=None)
Definition: z3py.py:9579

◆ fpIsNegative()

def z3py.fpIsNegative (   a,
  ctx = None 
)
Create a Z3 floating-point isNegative expression.

Definition at line 9615 of file z3py.py.

9615 def fpIsNegative(a, ctx=None):
9616  """Create a Z3 floating-point isNegative expression.
9617  """
9618  return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
9619 
def fpIsNegative(a, ctx=None)
Definition: z3py.py:9615

◆ fpIsNormal()

def z3py.fpIsNormal (   a,
  ctx = None 
)
Create a Z3 floating-point isNormal expression.

Definition at line 9605 of file z3py.py.

9605 def fpIsNormal(a, ctx=None):
9606  """Create a Z3 floating-point isNormal expression.
9607  """
9608  return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
9609 
def fpIsNormal(a, ctx=None)
Definition: z3py.py:9605

◆ fpIsPositive()

def z3py.fpIsPositive (   a,
  ctx = None 
)
Create a Z3 floating-point isPositive expression.

Definition at line 9620 of file z3py.py.

9620 def fpIsPositive(a, ctx=None):
9621  """Create a Z3 floating-point isPositive expression.
9622  """
9623  return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
9624 
def fpIsPositive(a, ctx=None)
Definition: z3py.py:9620

◆ fpIsSubnormal()

def z3py.fpIsSubnormal (   a,
  ctx = None 
)
Create a Z3 floating-point isSubnormal expression.

Definition at line 9610 of file z3py.py.

9610 def fpIsSubnormal(a, ctx=None):
9611  """Create a Z3 floating-point isSubnormal expression.
9612  """
9613  return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
9614 
def fpIsSubnormal(a, ctx=None)
Definition: z3py.py:9610

◆ fpIsZero()

def z3py.fpIsZero (   a,
  ctx = None 
)
Create a Z3 floating-point isZero expression.

Definition at line 9600 of file z3py.py.

9600 def fpIsZero(a, ctx=None):
9601  """Create a Z3 floating-point isZero expression.
9602  """
9603  return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
9604 
def fpIsZero(a, ctx=None)
Definition: z3py.py:9600

◆ fpLEQ()

def z3py.fpLEQ (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `other <= self`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLEQ(x, y)
x <= y
>>> (x <= y).sexpr()
'(fp.leq x y)'

Definition at line 9640 of file z3py.py.

9640 def fpLEQ(a, b, ctx=None):
9641  """Create the Z3 floating-point expression `other <= self`.
9642 
9643  >>> x, y = FPs('x y', FPSort(8, 24))
9644  >>> fpLEQ(x, y)
9645  x <= y
9646  >>> (x <= y).sexpr()
9647  '(fp.leq x y)'
9648  """
9649  return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
9650 
def fpLEQ(a, b, ctx=None)
Definition: z3py.py:9640

◆ fpLT()

def z3py.fpLT (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `other < self`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLT(x, y)
x < y
>>> (x < y).sexpr()
'(fp.lt x y)'

Definition at line 9629 of file z3py.py.

9629 def fpLT(a, b, ctx=None):
9630  """Create the Z3 floating-point expression `other < self`.
9631 
9632  >>> x, y = FPs('x y', FPSort(8, 24))
9633  >>> fpLT(x, y)
9634  x < y
9635  >>> (x < y).sexpr()
9636  '(fp.lt x y)'
9637  """
9638  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
9639 
def fpLT(a, b, ctx=None)
Definition: z3py.py:9629

◆ fpMax()

def z3py.fpMax (   a,
  b,
  ctx = None 
)
Create a Z3 floating-point maximum expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMax(x, y)
fpMax(x, y)
>>> fpMax(x, y).sort()
FPSort(8, 24)

Definition at line 9550 of file z3py.py.

9550 def fpMax(a, b, ctx=None):
9551  """Create a Z3 floating-point maximum expression.
9552 
9553  >>> s = FPSort(8, 24)
9554  >>> rm = RNE()
9555  >>> x = FP('x', s)
9556  >>> y = FP('y', s)
9557  >>> fpMax(x, y)
9558  fpMax(x, y)
9559  >>> fpMax(x, y).sort()
9560  FPSort(8, 24)
9561  """
9562  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
9563 
def fpMax(a, b, ctx=None)
Definition: z3py.py:9550

◆ fpMin()

def z3py.fpMin (   a,
  b,
  ctx = None 
)
Create a Z3 floating-point minimum expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMin(x, y)
fpMin(x, y)
>>> fpMin(x, y).sort()
FPSort(8, 24)

Definition at line 9536 of file z3py.py.

9536 def fpMin(a, b, ctx=None):
9537  """Create a Z3 floating-point minimum expression.
9538 
9539  >>> s = FPSort(8, 24)
9540  >>> rm = RNE()
9541  >>> x = FP('x', s)
9542  >>> y = FP('y', s)
9543  >>> fpMin(x, y)
9544  fpMin(x, y)
9545  >>> fpMin(x, y).sort()
9546  FPSort(8, 24)
9547  """
9548  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
9549 
def fpMin(a, b, ctx=None)
Definition: z3py.py:9536

◆ fpMinusInfinity()

def z3py.fpMinusInfinity (   s)
Create a Z3 floating-point -oo term.

Definition at line 9271 of file z3py.py.

9271 def fpMinusInfinity(s):
9272  """Create a Z3 floating-point -oo term."""
9273  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9274  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9275 
def fpMinusInfinity(s)
Definition: z3py.py:9271
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.

◆ fpMinusZero()

def z3py.fpMinusZero (   s)
Create a Z3 floating-point -0.0 term.

Definition at line 9287 of file z3py.py.

9287 def fpMinusZero(s):
9288  """Create a Z3 floating-point -0.0 term."""
9289  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9290  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
9291 
def fpMinusZero(s)
Definition: z3py.py:9287
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.

◆ fpMul()

def z3py.fpMul (   rm,
  a,
  b,
  ctx = None 
)
Create a Z3 floating-point multiplication expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMul(rm, x, y)
fpMul(RNE(), x, y)
>>> fpMul(rm, x, y).sort()
FPSort(8, 24)

Definition at line 9495 of file z3py.py.

Referenced by FPs().

9495 def fpMul(rm, a, b, ctx=None):
9496  """Create a Z3 floating-point multiplication expression.
9497 
9498  >>> s = FPSort(8, 24)
9499  >>> rm = RNE()
9500  >>> x = FP('x', s)
9501  >>> y = FP('y', s)
9502  >>> fpMul(rm, x, y)
9503  fpMul(RNE(), x, y)
9504  >>> fpMul(rm, x, y).sort()
9505  FPSort(8, 24)
9506  """
9507  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
9508 
def fpMul(rm, a, b, ctx=None)
Definition: z3py.py:9495

◆ fpNaN()

def z3py.fpNaN (   s)
Create a Z3 floating-point NaN term.

>>> s = FPSort(8, 24)
>>> set_fpa_pretty(True)
>>> fpNaN(s)
NaN
>>> pb = get_fpa_pretty()
>>> set_fpa_pretty(False)
>>> fpNaN(s)
fpNaN(FPSort(8, 24))
>>> set_fpa_pretty(pb)

Definition at line 9239 of file z3py.py.

9239 def fpNaN(s):
9240  """Create a Z3 floating-point NaN term.
9241 
9242  >>> s = FPSort(8, 24)
9243  >>> set_fpa_pretty(True)
9244  >>> fpNaN(s)
9245  NaN
9246  >>> pb = get_fpa_pretty()
9247  >>> set_fpa_pretty(False)
9248  >>> fpNaN(s)
9249  fpNaN(FPSort(8, 24))
9250  >>> set_fpa_pretty(pb)
9251  """
9252  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9253  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9254 
def fpNaN(s)
Definition: z3py.py:9239
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.

◆ fpNeg()

def z3py.fpNeg (   a,
  ctx = None 
)
Create a Z3 floating-point addition expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> fpNeg(x)
-x
>>> fpNeg(x).sort()
FPSort(8, 24)

Definition at line 9405 of file z3py.py.

9405 def fpNeg(a, ctx=None):
9406  """Create a Z3 floating-point addition expression.
9407 
9408  >>> s = FPSort(8, 24)
9409  >>> rm = RNE()
9410  >>> x = FP('x', s)
9411  >>> fpNeg(x)
9412  -x
9413  >>> fpNeg(x).sort()
9414  FPSort(8, 24)
9415  """
9416  ctx = _get_ctx(ctx)
9417  [a] = _coerce_fp_expr_list([a], ctx)
9418  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
9419 
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
def fpNeg(a, ctx=None)
Definition: z3py.py:9405

◆ fpNEQ()

def z3py.fpNEQ (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `Not(fpEQ(other, self))`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpNEQ(x, y)
Not(fpEQ(x, y))
>>> (x != y).sexpr()
'(distinct x y)'

Definition at line 9684 of file z3py.py.

9684 def fpNEQ(a, b, ctx=None):
9685  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
9686 
9687  >>> x, y = FPs('x y', FPSort(8, 24))
9688  >>> fpNEQ(x, y)
9689  Not(fpEQ(x, y))
9690  >>> (x != y).sexpr()
9691  '(distinct x y)'
9692  """
9693  return Not(fpEQ(a, b, ctx))
9694 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:9673
def Not(a, ctx=None)
Definition: z3py.py:1649
def fpNEQ(a, b, ctx=None)
Definition: z3py.py:9684

◆ fpPlusInfinity()

def z3py.fpPlusInfinity (   s)
Create a Z3 floating-point +oo term.

>>> s = FPSort(8, 24)
>>> pb = get_fpa_pretty()
>>> set_fpa_pretty(True)
>>> fpPlusInfinity(s)
+oo
>>> set_fpa_pretty(False)
>>> fpPlusInfinity(s)
fpPlusInfinity(FPSort(8, 24))
>>> set_fpa_pretty(pb)

Definition at line 9255 of file z3py.py.

9255 def fpPlusInfinity(s):
9256  """Create a Z3 floating-point +oo term.
9257 
9258  >>> s = FPSort(8, 24)
9259  >>> pb = get_fpa_pretty()
9260  >>> set_fpa_pretty(True)
9261  >>> fpPlusInfinity(s)
9262  +oo
9263  >>> set_fpa_pretty(False)
9264  >>> fpPlusInfinity(s)
9265  fpPlusInfinity(FPSort(8, 24))
9266  >>> set_fpa_pretty(pb)
9267  """
9268  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9269  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9270 
def fpPlusInfinity(s)
Definition: z3py.py:9255
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.

◆ fpPlusZero()

def z3py.fpPlusZero (   s)
Create a Z3 floating-point +0.0 term.

Definition at line 9282 of file z3py.py.

9282 def fpPlusZero(s):
9283  """Create a Z3 floating-point +0.0 term."""
9284  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9285  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
9286 
def fpPlusZero(s)
Definition: z3py.py:9282
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.

◆ fpRealToFP()

def z3py.fpRealToFP (   rm,
  v,
  sort,
  ctx = None 
)
Create a Z3 floating-point conversion expression that represents the
conversion from a real term to a floating-point term.

>>> x_r = RealVal(1.5)
>>> x_fp = fpRealToFP(RNE(), x_r, Float32())
>>> x_fp
fpToFP(RNE(), 3/2)
>>> simplify(x_fp)
1.5

Definition at line 9796 of file z3py.py.

9796 def fpRealToFP(rm, v, sort, ctx=None):
9797  """Create a Z3 floating-point conversion expression that represents the
9798  conversion from a real term to a floating-point term.
9799 
9800  >>> x_r = RealVal(1.5)
9801  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
9802  >>> x_fp
9803  fpToFP(RNE(), 3/2)
9804  >>> simplify(x_fp)
9805  1.5
9806  """
9807  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9808  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
9809  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9810  ctx = _get_ctx(ctx)
9811  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9812 
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
def is_real(a)
Definition: z3py.py:2515
def is_fp_sort(s)
Definition: z3py.py:8771
def fpRealToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9796
def is_fprm(a)
Definition: z3py.py:9018

◆ fpRem()

def z3py.fpRem (   a,
  b,
  ctx = None 
)
Create a Z3 floating-point remainder expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpRem(x, y)
fpRem(x, y)
>>> fpRem(x, y).sort()
FPSort(8, 24)

Definition at line 9523 of file z3py.py.

9523 def fpRem(a, b, ctx=None):
9524  """Create a Z3 floating-point remainder expression.
9525 
9526  >>> s = FPSort(8, 24)
9527  >>> x = FP('x', s)
9528  >>> y = FP('y', s)
9529  >>> fpRem(x, y)
9530  fpRem(x, y)
9531  >>> fpRem(x, y).sort()
9532  FPSort(8, 24)
9533  """
9534  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
9535 
def fpRem(a, b, ctx=None)
Definition: z3py.py:9523

◆ fpRoundToIntegral()

def z3py.fpRoundToIntegral (   rm,
  a,
  ctx = None 
)
Create a Z3 floating-point roundToIntegral expression.

Definition at line 9574 of file z3py.py.

9574 def fpRoundToIntegral(rm, a, ctx=None):
9575  """Create a Z3 floating-point roundToIntegral expression.
9576  """
9577  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
9578 
def fpRoundToIntegral(rm, a, ctx=None)
Definition: z3py.py:9574

◆ FPs()

def z3py.FPs (   names,
  fpsort,
  ctx = None 
)
Return an array of floating-point constants.

>>> x, y, z = FPs('x y z', FPSort(8, 24))
>>> x.sort()
FPSort(8, 24)
>>> x.sbits()
24
>>> x.ebits()
8
>>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
fpMul(RNE(), fpAdd(RNE(), x, y), z)

Definition at line 9365 of file z3py.py.

Referenced by fpEQ(), fpGEQ(), fpGT(), fpLEQ(), fpLT(), and fpNEQ().

9365 def FPs(names, fpsort, ctx=None):
9366  """Return an array of floating-point constants.
9367 
9368  >>> x, y, z = FPs('x y z', FPSort(8, 24))
9369  >>> x.sort()
9370  FPSort(8, 24)
9371  >>> x.sbits()
9372  24
9373  >>> x.ebits()
9374  8
9375  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9376  fpMul(RNE(), fpAdd(RNE(), x, y), z)
9377  """
9378  ctx = _get_ctx(ctx)
9379  if isinstance(names, str):
9380  names = names.split(" ")
9381  return [FP(name, fpsort, ctx) for name in names]
9382 
def FPs(names, fpsort, ctx=None)
Definition: z3py.py:9365
def FP(name, fpsort, ctx=None)
Definition: z3py.py:9342

◆ fpSignedToFP()

def z3py.fpSignedToFP (   rm,
  v,
  sort,
  ctx = None 
)
Create a Z3 floating-point conversion expression that represents the
conversion from a signed bit-vector term (encoding an integer) to a floating-point term.

>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
>>> x_fp
fpToFP(RNE(), 4294967291)
>>> simplify(x_fp)
-1.25*(2**2)

Definition at line 9813 of file z3py.py.

9813 def fpSignedToFP(rm, v, sort, ctx=None):
9814  """Create a Z3 floating-point conversion expression that represents the
9815  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
9816 
9817  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9818  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
9819  >>> x_fp
9820  fpToFP(RNE(), 4294967291)
9821  >>> simplify(x_fp)
9822  -1.25*(2**2)
9823  """
9824  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9825  _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.")
9826  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9827  ctx = _get_ctx(ctx)
9828  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9829 
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement signed bit-vector term into a term of FloatingPoint sort...
def fpSignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9813
def is_fp_sort(s)
Definition: z3py.py:8771
def is_bv(a)
Definition: z3py.py:3683
def is_fprm(a)
Definition: z3py.py:9018

◆ FPSort()

def z3py.FPSort (   ebits,
  sbits,
  ctx = None 
)
Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.

>>> Single = FPSort(8, 24)
>>> Double = FPSort(11, 53)
>>> Single
FPSort(8, 24)
>>> x = Const('x', Single)
>>> eq(x, FP('x', FPSort(8, 24)))
True

Definition at line 9181 of file z3py.py.

Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FPSortRef.cast(), FPSortRef.ebits(), FPRef.ebits(), FPNumRef.exponent(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpFP(), fpFPToFP(), fpGEQ(), fpGT(), fpIsInf(), fpIsNaN(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNaN(), fpNeg(), fpNEQ(), fpPlusInfinity(), fpRem(), FPs(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), is_fp(), is_fp_sort(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), Context.MkFPRTZ(), Context.mkFPSort(), Context.mkFPSort128(), Context.MkFPSort128(), Context.mkFPSort16(), Context.MkFPSort16(), Context.mkFPSort32(), Context.MkFPSort32(), Context.mkFPSort64(), Context.MkFPSort64(), Context.mkFPSortDouble(), Context.MkFPSortDouble(), Context.mkFPSortHalf(), Context.MkFPSortHalf(), Context.mkFPSortQuadruple(), Context.MkFPSortQuadruple(), Context.mkFPSortSingle(), Context.MkFPSortSingle(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPRef.sort(), Sort.translate(), and Sort.Translate().

9181 def FPSort(ebits, sbits, ctx=None):
9182  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9183 
9184  >>> Single = FPSort(8, 24)
9185  >>> Double = FPSort(11, 53)
9186  >>> Single
9187  FPSort(8, 24)
9188  >>> x = Const('x', Single)
9189  >>> eq(x, FP('x', FPSort(8, 24)))
9190  True
9191  """
9192  ctx = _get_ctx(ctx)
9193  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9194 
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9181

◆ fpSqrt()

def z3py.fpSqrt (   rm,
  a,
  ctx = None 
)
Create a Z3 floating-point square root expression.

Definition at line 9569 of file z3py.py.

9569 def fpSqrt(rm, a, ctx=None):
9570  """Create a Z3 floating-point square root expression.
9571  """
9572  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
9573 
def fpSqrt(rm, a, ctx=None)
Definition: z3py.py:9569

◆ fpSub()

def z3py.fpSub (   rm,
  a,
  b,
  ctx = None 
)
Create a Z3 floating-point subtraction expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpSub(rm, x, y)
fpSub(RNE(), x, y)
>>> fpSub(rm, x, y).sort()
FPSort(8, 24)

Definition at line 9481 of file z3py.py.

9481 def fpSub(rm, a, b, ctx=None):
9482  """Create a Z3 floating-point subtraction expression.
9483 
9484  >>> s = FPSort(8, 24)
9485  >>> rm = RNE()
9486  >>> x = FP('x', s)
9487  >>> y = FP('y', s)
9488  >>> fpSub(rm, x, y)
9489  fpSub(RNE(), x, y)
9490  >>> fpSub(rm, x, y).sort()
9491  FPSort(8, 24)
9492  """
9493  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
9494 
def fpSub(rm, a, b, ctx=None)
Definition: z3py.py:9481

◆ fpToFP()

def z3py.fpToFP (   a1,
  a2 = None,
  a3 = None,
  ctx = None 
)
Create a Z3 floating-point conversion expression from other term sorts
to floating-point.

From a bit-vector term in IEEE 754-2008 format:
>>> x = FPVal(1.0, Float32())
>>> x_bv = fpToIEEEBV(x)
>>> simplify(fpToFP(x_bv, Float32()))
1

From a floating-point term with different precision:
>>> x = FPVal(1.0, Float32())
>>> x_db = fpToFP(RNE(), x, Float64())
>>> x_db.sort()
FPSort(11, 53)

From a real term:
>>> x_r = RealVal(1.5)
>>> simplify(fpToFP(RNE(), x_r, Float32()))
1.5

From a signed bit-vector term:
>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> simplify(fpToFP(RNE(), x_signed, Float32()))
-1.25*(2**2)

Definition at line 9723 of file z3py.py.

Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), and fpSignedToFP().

9723 def fpToFP(a1, a2=None, a3=None, ctx=None):
9724  """Create a Z3 floating-point conversion expression from other term sorts
9725  to floating-point.
9726 
9727  From a bit-vector term in IEEE 754-2008 format:
9728  >>> x = FPVal(1.0, Float32())
9729  >>> x_bv = fpToIEEEBV(x)
9730  >>> simplify(fpToFP(x_bv, Float32()))
9731  1
9732 
9733  From a floating-point term with different precision:
9734  >>> x = FPVal(1.0, Float32())
9735  >>> x_db = fpToFP(RNE(), x, Float64())
9736  >>> x_db.sort()
9737  FPSort(11, 53)
9738 
9739  From a real term:
9740  >>> x_r = RealVal(1.5)
9741  >>> simplify(fpToFP(RNE(), x_r, Float32()))
9742  1.5
9743 
9744  From a signed bit-vector term:
9745  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9746  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
9747  -1.25*(2**2)
9748  """
9749  ctx = _get_ctx(ctx)
9750  if is_bv(a1) and is_fp_sort(a2):
9751  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
9752  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
9753  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9754  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
9755  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9756  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
9757  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9758  else:
9759  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
9760 
def fpToFP(a1, a2=None, a3=None, ctx=None)
Definition: z3py.py:9723
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement signed bit-vector term into a term of FloatingPoint sort...
def is_real(a)
Definition: z3py.py:2515
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
def is_fp_sort(s)
Definition: z3py.py:8771
def is_bv(a)
Definition: z3py.py:3683
def is_fprm(a)
Definition: z3py.py:9018
def is_fp(a)
Definition: z3py.py:9154

◆ fpToFPUnsigned()

def z3py.fpToFPUnsigned (   rm,
  x,
  s,
  ctx = None 
)
Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.

Definition at line 9847 of file z3py.py.

Referenced by fpUnsignedToFP().

9847 def fpToFPUnsigned(rm, x, s, ctx=None):
9848  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
9849  if z3_debug():
9850  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9851  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
9852  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
9853  ctx = _get_ctx(ctx)
9854  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
9855 
def fpToFPUnsigned(rm, x, s, ctx=None)
Definition: z3py.py:9847
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement unsigned bit-vector term into a term of FloatingPoint sort...
def z3_debug()
Definition: z3py.py:56
def is_fp_sort(s)
Definition: z3py.py:8771
def is_bv(a)
Definition: z3py.py:3683
def is_fprm(a)
Definition: z3py.py:9018

◆ fpToIEEEBV()

def z3py.fpToIEEEBV (   x,
  ctx = None 
)
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

The size of the resulting bit-vector is automatically determined.

Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
knows only one NaN and it will always produce the same bit-vector representation of
that NaN.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToIEEEBV(x)
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False

Definition at line 9917 of file z3py.py.

Referenced by fpToFP().

9917 def fpToIEEEBV(x, ctx=None):
9918  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
9919 
9920  The size of the resulting bit-vector is automatically determined.
9921 
9922  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9923  knows only one NaN and it will always produce the same bit-vector representation of
9924  that NaN.
9925 
9926  >>> x = FP('x', FPSort(8, 24))
9927  >>> y = fpToIEEEBV(x)
9928  >>> print(is_fp(x))
9929  True
9930  >>> print(is_bv(y))
9931  True
9932  >>> print(is_fp(y))
9933  False
9934  >>> print(is_bv(x))
9935  False
9936  """
9937  if z3_debug():
9938  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
9939  ctx = _get_ctx(ctx)
9940  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
9941 
9942 
9943 
def fpToIEEEBV(x, ctx=None)
Definition: z3py.py:9917
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
def z3_debug()
Definition: z3py.py:56
def is_fp(a)
Definition: z3py.py:9154

◆ fpToReal()

def z3py.fpToReal (   x,
  ctx = None 
)
Create a Z3 floating-point conversion expression, from floating-point expression to real.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToReal(x)
>>> print(is_fp(x))
True
>>> print(is_real(y))
True
>>> print(is_fp(y))
False
>>> print(is_real(x))
False

Definition at line 9898 of file z3py.py.

9898 def fpToReal(x, ctx=None):
9899  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
9900 
9901  >>> x = FP('x', FPSort(8, 24))
9902  >>> y = fpToReal(x)
9903  >>> print(is_fp(x))
9904  True
9905  >>> print(is_real(y))
9906  True
9907  >>> print(is_fp(y))
9908  False
9909  >>> print(is_real(x))
9910  False
9911  """
9912  if z3_debug():
9913  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
9914  ctx = _get_ctx(ctx)
9915  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
9916 
Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a real-numbered term.
def z3_debug()
Definition: z3py.py:56
def fpToReal(x, ctx=None)
Definition: z3py.py:9898
def is_fp(a)
Definition: z3py.py:9154

◆ fpToSBV()

def z3py.fpToSBV (   rm,
  x,
  s,
  ctx = None 
)
Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToSBV(RTZ(), x, BitVecSort(32))
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False

Definition at line 9856 of file z3py.py.

9856 def fpToSBV(rm, x, s, ctx=None):
9857  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
9858 
9859  >>> x = FP('x', FPSort(8, 24))
9860  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
9861  >>> print(is_fp(x))
9862  True
9863  >>> print(is_bv(y))
9864  True
9865  >>> print(is_fp(y))
9866  False
9867  >>> print(is_bv(x))
9868  False
9869  """
9870  if z3_debug():
9871  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9872  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
9873  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
9874  ctx = _get_ctx(ctx)
9875  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
9876 
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
def fpToSBV(rm, x, s, ctx=None)
Definition: z3py.py:9856
def z3_debug()
Definition: z3py.py:56
def is_bv_sort(s)
Definition: z3py.py:3222
def is_fprm(a)
Definition: z3py.py:9018
def is_fp(a)
Definition: z3py.py:9154

◆ fpToUBV()

def z3py.fpToUBV (   rm,
  x,
  s,
  ctx = None 
)
Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToUBV(RTZ(), x, BitVecSort(32))
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False

Definition at line 9877 of file z3py.py.

9877 def fpToUBV(rm, x, s, ctx=None):
9878  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
9879 
9880  >>> x = FP('x', FPSort(8, 24))
9881  >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
9882  >>> print(is_fp(x))
9883  True
9884  >>> print(is_bv(y))
9885  True
9886  >>> print(is_fp(y))
9887  False
9888  >>> print(is_bv(x))
9889  False
9890  """
9891  if z3_debug():
9892  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9893  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
9894  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
9895  ctx = _get_ctx(ctx)
9896  return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
9897 
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
def fpToUBV(rm, x, s, ctx=None)
Definition: z3py.py:9877
def z3_debug()
Definition: z3py.py:56
def is_bv_sort(s)
Definition: z3py.py:3222
def is_fprm(a)
Definition: z3py.py:9018
def is_fp(a)
Definition: z3py.py:9154

◆ fpUnsignedToFP()

def z3py.fpUnsignedToFP (   rm,
  v,
  sort,
  ctx = None 
)
Create a Z3 floating-point conversion expression that represents the
conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.

>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
>>> x_fp
fpToFPUnsigned(RNE(), 4294967291)
>>> simplify(x_fp)
1*(2**32)

Definition at line 9830 of file z3py.py.

9830 def fpUnsignedToFP(rm, v, sort, ctx=None):
9831  """Create a Z3 floating-point conversion expression that represents the
9832  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9833 
9834  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9835  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
9836  >>> x_fp
9837  fpToFPUnsigned(RNE(), 4294967291)
9838  >>> simplify(x_fp)
9839  1*(2**32)
9840  """
9841  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9842  _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.")
9843  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9844  ctx = _get_ctx(ctx)
9845  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9846 
def fpUnsignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9830
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement unsigned bit-vector term into a term of FloatingPoint sort...
def is_fp_sort(s)
Definition: z3py.py:8771
def is_bv(a)
Definition: z3py.py:3683
def is_fprm(a)
Definition: z3py.py:9018

◆ FPVal()

def z3py.FPVal (   sig,
  exp = None,
  fps = None,
  ctx = None 
)
Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.

>>> v = FPVal(20.0, FPSort(8, 24))
>>> v
1.25*(2**4)
>>> print("0x%.8x" % v.exponent_as_long(False))
0x00000004
>>> v = FPVal(2.25, FPSort(8, 24))
>>> v
1.125*(2**1)
>>> v = FPVal(-2.25, FPSort(8, 24))
>>> v
-1.125*(2**1)
>>> FPVal(-0.0, FPSort(8, 24))
-0.0
>>> FPVal(0.0, FPSort(8, 24))
+0.0
>>> FPVal(+0.0, FPSort(8, 24))
+0.0

Definition at line 9298 of file z3py.py.

Referenced by FPNumRef.exponent(), fpAbs(), fpFP(), fpFPToFP(), fpToFP(), is_fp_value(), FPNumRef.isNegative(), FPNumRef.sign_as_bv(), FPNumRef.significand(), and FPNumRef.significand_as_bv().

9298 def FPVal(sig, exp=None, fps=None, ctx=None):
9299  """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
9300 
9301  >>> v = FPVal(20.0, FPSort(8, 24))
9302  >>> v
9303  1.25*(2**4)
9304  >>> print("0x%.8x" % v.exponent_as_long(False))
9305  0x00000004
9306  >>> v = FPVal(2.25, FPSort(8, 24))
9307  >>> v
9308  1.125*(2**1)
9309  >>> v = FPVal(-2.25, FPSort(8, 24))
9310  >>> v
9311  -1.125*(2**1)
9312  >>> FPVal(-0.0, FPSort(8, 24))
9313  -0.0
9314  >>> FPVal(0.0, FPSort(8, 24))
9315  +0.0
9316  >>> FPVal(+0.0, FPSort(8, 24))
9317  +0.0
9318  """
9319  ctx = _get_ctx(ctx)
9320  if is_fp_sort(exp):
9321  fps = exp
9322  exp = None
9323  elif fps is None:
9324  fps = _dflt_fps(ctx)
9325  _z3_assert(is_fp_sort(fps), "sort mismatch")
9326  if exp is None:
9327  exp = 0
9328  val = _to_float_str(sig)
9329  if val == "NaN" or val == "nan":
9330  return fpNaN(fps)
9331  elif val == "-0.0":
9332  return fpMinusZero(fps)
9333  elif val == "0.0" or val == "+0.0":
9334  return fpPlusZero(fps)
9335  elif val == "+oo" or val == "+inf" or val == "+Inf":
9336  return fpPlusInfinity(fps)
9337  elif val == "-oo" or val == "-inf" or val == "-Inf":
9338  return fpMinusInfinity(fps)
9339  else:
9340  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
9341 
def FPVal(sig, exp=None, fps=None, ctx=None)
Definition: z3py.py:9298
def fpMinusInfinity(s)
Definition: z3py.py:9271
def fpMinusZero(s)
Definition: z3py.py:9287
def fpPlusZero(s)
Definition: z3py.py:9282
def fpPlusInfinity(s)
Definition: z3py.py:9255
def fpNaN(s)
Definition: z3py.py:9239
def is_fp_sort(s)
Definition: z3py.py:8771
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ fpZero()

def z3py.fpZero (   s,
  negative 
)
Create a Z3 floating-point +0.0 or -0.0 term.

Definition at line 9292 of file z3py.py.

9292 def fpZero(s, negative):
9293  """Create a Z3 floating-point +0.0 or -0.0 term."""
9294  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9295  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9296  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
9297 
def fpZero(s, negative)
Definition: z3py.py:9292
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.

◆ FreshBool()

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

1608 def FreshBool(prefix='b', ctx=None):
1609  """Return a fresh Boolean constant in the given context using the given prefix.
1610 
1611  If `ctx=None`, then the global context is used.
1612 
1613  >>> b1 = FreshBool()
1614  >>> b2 = FreshBool()
1615  >>> eq(b1, b2)
1616  False
1617  """
1618  ctx = _get_ctx(ctx)
1619  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1620 
def FreshBool(prefix='b', ctx=None)
Definition: z3py.py:1608
def BoolSort(ctx=None)
Definition: z3py.py:1533
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshConst()

def z3py.FreshConst (   sort,
  prefix = 'c' 
)
Create a fresh constant of a specified sort

Definition at line 1326 of file z3py.py.

1326 def FreshConst(sort, prefix='c'):
1327  """Create a fresh constant of a specified sort"""
1328  ctx = _get_ctx(sort.ctx)
1329  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1330 
def FreshConst(sort, prefix='c')
Definition: z3py.py:1326
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshInt()

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

3045 def FreshInt(prefix='x', ctx=None):
3046  """Return a fresh integer constant in the given context using the given prefix.
3047 
3048  >>> x = FreshInt()
3049  >>> y = FreshInt()
3050  >>> eq(x, y)
3051  False
3052  >>> x.sort()
3053  Int
3054  """
3055  ctx = _get_ctx(ctx)
3056  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3057 
def IntSort(ctx=None)
Definition: z3py.py:2907
def FreshInt(prefix='x', ctx=None)
Definition: z3py.py:3045
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshReal()

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

3097 def FreshReal(prefix='b', ctx=None):
3098  """Return a fresh real constant in the given context using the given prefix.
3099 
3100  >>> x = FreshReal()
3101  >>> y = FreshReal()
3102  >>> eq(x, y)
3103  False
3104  >>> x.sort()
3105  Real
3106  """
3107  ctx = _get_ctx(ctx)
3108  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3109 
def FreshReal(prefix='b', ctx=None)
Definition: z3py.py:3097
def RealSort(ctx=None)
Definition: z3py.py:2923
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ Full()

def z3py.Full (   s)
Create the regular expression that accepts the universal language
>>> e = Full(ReSort(SeqSort(IntSort())))
>>> print(e)
Full(ReSort(Seq(Int)))
>>> e1 = Full(ReSort(StringSort()))
>>> print(e1)
Full(ReSort(String))

Definition at line 10132 of file z3py.py.

10132 def Full(s):
10133  """Create the regular expression that accepts the universal language
10134  >>> e = Full(ReSort(SeqSort(IntSort())))
10135  >>> print(e)
10136  Full(ReSort(Seq(Int)))
10137  >>> e1 = Full(ReSort(StringSort()))
10138  >>> print(e1)
10139  Full(ReSort(String))
10140  """
10141  if isinstance(s, ReSortRef):
10142  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10143  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10144 
10145 
def Full(s)
Definition: z3py.py:10132
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.

◆ FullSet()

def z3py.FullSet (   s)
Create the full set
>>> FullSet(IntSort())
K(Int, True)

Definition at line 4580 of file z3py.py.

4580 def FullSet(s):
4581  """Create the full set
4582  >>> FullSet(IntSort())
4583  K(Int, True)
4584  """
4585  ctx = s.ctx
4586  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4587 
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
def FullSet(s)
Definition: z3py.py:4580

◆ Function()

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 799 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_exists(), QuantifierRef.is_forall(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), Lambda(), 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().

799 def Function(name, *sig):
800  """Create a new Z3 uninterpreted function with the given sorts.
801 
802  >>> f = Function('f', IntSort(), IntSort())
803  >>> f(f(0))
804  f(f(0))
805  """
806  sig = _get_args(sig)
807  if z3_debug():
808  _z3_assert(len(sig) > 0, "At least two arguments expected")
809  arity = len(sig) - 1
810  rng = sig[arity]
811  if z3_debug():
812  _z3_assert(is_sort(rng), "Z3 sort expected")
813  dom = (Sort * arity)()
814  for i in range(arity):
815  if z3_debug():
816  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
817  dom[i] = sig[i].ast
818  ctx = rng.ctx
819  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
820 
def Function(name, sig)
Definition: z3py.py:799
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def to_symbol(s, ctx=None)
Definition: z3py.py:109
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
def is_sort(s)
Definition: z3py.py:596
def z3_debug()
Definition: z3py.py:56

◆ get_as_array_func()

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

6244 def get_as_array_func(n):
6245  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6246  if z3_debug():
6247  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6248  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6249 
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
def get_as_array_func(n)
Definition: z3py.py:6244
def z3_debug()
Definition: z3py.py:56
def is_as_array(n)
Definition: z3py.py:6240

◆ get_ctx()

def z3py.get_ctx (   ctx)

Definition at line 237 of file z3py.py.

237 def get_ctx(ctx):
238  return _get_ctx(ctx)
239 
def get_ctx(ctx)
Definition: z3py.py:237

◆ get_default_fp_sort()

def z3py.get_default_fp_sort (   ctx = None)

Definition at line 8651 of file z3py.py.

8651 def get_default_fp_sort(ctx=None):
8652  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
8653 
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9181
def get_default_fp_sort(ctx=None)
Definition: z3py.py:8651

◆ get_default_rounding_mode()

def z3py.get_default_rounding_mode (   ctx = None)
Retrieves the global default rounding mode.

Definition at line 8624 of file z3py.py.

8624 def get_default_rounding_mode(ctx=None):
8625  """Retrieves the global default rounding mode."""
8626  global _dflt_rounding_mode
8627  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
8628  return RTZ(ctx)
8629  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
8630  return RTN(ctx)
8631  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
8632  return RTP(ctx)
8633  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
8634  return RNE(ctx)
8635  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
8636  return RNA(ctx)
8637 
def RTN(ctx=None)
Definition: z3py.py:9006
def RTZ(ctx=None)
Definition: z3py.py:9014
def RTP(ctx=None)
Definition: z3py.py:8998
def RNA(ctx=None)
Definition: z3py.py:8990
def get_default_rounding_mode(ctx=None)
Definition: z3py.py:8624
def RNE(ctx=None)
Definition: z3py.py:8982

◆ get_full_version()

def z3py.get_full_version ( )

Definition at line 89 of file z3py.py.

89 def get_full_version():
90  return Z3_get_full_version()
91 
92 # We use _z3_assert instead of the assert command because we want to
93 # produce nice error messages in Z3Py at rise4fun.com
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
def get_full_version()
Definition: z3py.py:89

◆ get_map_func()

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

4354 def get_map_func(a):
4355  """Return the function declaration associated with a Z3 map array expression.
4356 
4357  >>> f = Function('f', IntSort(), IntSort())
4358  >>> b = Array('b', IntSort(), IntSort())
4359  >>> a = Map(f, b)
4360  >>> eq(f, get_map_func(a))
4361  True
4362  >>> get_map_func(a)
4363  f
4364  >>> get_map_func(a)(0)
4365  f(0)
4366  """
4367  if z3_debug():
4368  _z3_assert(is_map(a), "Z3 array map expression expected.")
4369  return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
4370 
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
def is_map(a)
Definition: z3py.py:4331
def get_map_func(a)
Definition: z3py.py:4354
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def z3_debug()
Definition: z3py.py:56

◆ get_param()

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

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

Definition at line 273 of file z3py.py.

273 def get_param(name):
274  """Return the value of a Z3 global (or module) parameter
275 
276  >>> get_param('nlsat.reorder')
277  'true'
278  """
279  ptr = (ctypes.c_char_p * 1)()
280  if Z3_global_param_get(str(name), ptr):
281  r = z3core._to_pystr(ptr[0])
282  return r
283  raise Z3Exception("failed to retrieve value for '%s'" % name)
284 
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
def get_param(name)
Definition: z3py.py:273

◆ get_var_index()

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

1204 def get_var_index(a):
1205  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1206 
1207  >>> x = Int('x')
1208  >>> y = Int('y')
1209  >>> is_var(x)
1210  False
1211  >>> is_const(x)
1212  True
1213  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1214  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1215  >>> q = ForAll([x, y], f(x, y) == x + y)
1216  >>> q.body()
1217  f(Var(1), Var(0)) == Var(1) + Var(0)
1218  >>> b = q.body()
1219  >>> b.arg(0)
1220  f(Var(1), Var(0))
1221  >>> v1 = b.arg(0).arg(0)
1222  >>> v2 = b.arg(0).arg(1)
1223  >>> v1
1224  Var(1)
1225  >>> v2
1226  Var(0)
1227  >>> get_var_index(v1)
1228  1
1229  >>> get_var_index(v2)
1230  0
1231  """
1232  if z3_debug():
1233  _z3_assert(is_var(a), "Z3 bound variable expected")
1234  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1235 
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
def z3_debug()
Definition: z3py.py:56
def get_var_index(a)
Definition: z3py.py:1204
def is_var(a)
Definition: z3py.py:1180

◆ get_version()

def z3py.get_version ( )

Definition at line 81 of file z3py.py.

81 def get_version():
82  major = ctypes.c_uint(0)
83  minor = ctypes.c_uint(0)
84  build = ctypes.c_uint(0)
85  rev = ctypes.c_uint(0)
86  Z3_get_version(major, minor, build, rev)
87  return (major.value, minor.value, build.value, rev.value)
88 
def get_version()
Definition: z3py.py:81
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.

◆ get_version_string()

def z3py.get_version_string ( )

Definition at line 73 of file z3py.py.

73 def get_version_string():
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 "%s.%s.%s" % (major.value, minor.value, build.value)
80 
def get_version_string()
Definition: z3py.py:73
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.

◆ help_simplify()

def z3py.help_simplify ( )
Return a string describing all options available for Z3 `simplify` procedure.

Definition at line 8204 of file z3py.py.

8204 def help_simplify():
8205  """Return a string describing all options available for Z3 `simplify` procedure."""
8206  print(Z3_simplify_get_help(main_ctx().ref()))
8207 
def main_ctx()
Definition: z3py.py:211
def help_simplify()
Definition: z3py.py:8204
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.

◆ If()

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

Referenced by BoolRef.__mul__(), BV2Int(), and Lambda().

1248 def If(a, b, c, ctx=None):
1249  """Create a Z3 if-then-else expression.
1250 
1251  >>> x = Int('x')
1252  >>> y = Int('y')
1253  >>> max = If(x > y, x, y)
1254  >>> max
1255  If(x > y, x, y)
1256  >>> simplify(max)
1257  If(x <= y, y, x)
1258  """
1259  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1260  return Cond(a, b, c, ctx)
1261  else:
1262  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1263  s = BoolSort(ctx)
1264  a = s.cast(a)
1265  b, c = _coerce_exprs(b, c, ctx)
1266  if z3_debug():
1267  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1268  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1269 
def If(a, b, c, ctx=None)
Definition: z3py.py:1248
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8164
def z3_debug()
Definition: z3py.py:56
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
def BoolSort(ctx=None)
Definition: z3py.py:1533

◆ Implies()

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

>>> p, q = Bools('p q')
>>> Implies(p, q)
Implies(p, q)

Definition at line 1621 of file z3py.py.

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

1621 def Implies(a, b, ctx=None):
1622  """Create a Z3 implies expression.
1623 
1624  >>> p, q = Bools('p q')
1625  >>> Implies(p, q)
1626  Implies(p, q)
1627  """
1628  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1629  s = BoolSort(ctx)
1630  a = s.cast(a)
1631  b = s.cast(b)
1632  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1633 
def Implies(a, b, ctx=None)
Definition: z3py.py:1621
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
def BoolSort(ctx=None)
Definition: z3py.py:1533

◆ IndexOf() [1/2]

def z3py.IndexOf (   s,
  substr 
)

Definition at line 10211 of file z3py.py.

Referenced by IndexOf().

10211 def IndexOf(s, substr):
10212  return IndexOf(s, substr, IntVal(0))
10213 
def IntVal(val, ctx=None)
Definition: z3py.py:2954
def IndexOf(s, substr)
Definition: z3py.py:10211

◆ IndexOf() [2/2]

def z3py.IndexOf (   s,
  substr,
  offset 
)
Retrieve the index of substring within a string starting at a specified offset.
>>> simplify(IndexOf("abcabc", "bc", 0))
1
>>> simplify(IndexOf("abcabc", "bc", 2))
4

Definition at line 10214 of file z3py.py.

10214 def IndexOf(s, substr, offset):
10215  """Retrieve the index of substring within a string starting at a specified offset.
10216  >>> simplify(IndexOf("abcabc", "bc", 0))
10217  1
10218  >>> simplify(IndexOf("abcabc", "bc", 2))
10219  4
10220  """
10221  ctx = None
10222  if is_expr(offset):
10223  ctx = offset.ctx
10224  ctx = _get_ctx2(s, substr, ctx)
10225  s = _coerce_seq(s, ctx)
10226  substr = _coerce_seq(substr, ctx)
10227  if _is_int(offset):
10228  offset = IntVal(offset, ctx)
10229  return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
10230 
def IntVal(val, ctx=None)
Definition: z3py.py:2954
def IndexOf(s, substr)
Definition: z3py.py:10211
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
def is_expr(a)
Definition: z3py.py:1115

◆ InRe()

def z3py.InRe (   s,
  re 
)
Create regular expression membership test
>>> re = Union(Re("a"),Re("b"))
>>> print (simplify(InRe("a", re)))
True
>>> print (simplify(InRe("b", re)))
True
>>> print (simplify(InRe("c", re)))
False

Definition at line 10311 of file z3py.py.

Referenced by Loop(), Option(), Plus(), Range(), Star(), and Union().

10311 def InRe(s, re):
10312  """Create regular expression membership test
10313  >>> re = Union(Re("a"),Re("b"))
10314  >>> print (simplify(InRe("a", re)))
10315  True
10316  >>> print (simplify(InRe("b", re)))
10317  True
10318  >>> print (simplify(InRe("c", re)))
10319  False
10320  """
10321  s = _coerce_seq(s, re.ctx)
10322  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
10323 
def InRe(s, re)
Definition: z3py.py:10311
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.

◆ Int()

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

Referenced by ArithRef.__add__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ArithRef.__mod__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), QuantifierRef.body(), BV2Int(), Solver.check(), QuantifierRef.children(), ModelRef.decls(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), Goal.insert(), Solver.insert(), is_arith(), is_arith_sort(), is_bv(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_fp(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_int_value(), QuantifierRef.is_lambda(), 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(), Solver.sexpr(), Goal.simplify(), ArithRef.sort(), Solver.statistics(), Store(), ToReal(), Goal.translate(), AstVector.translate(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

3010 def Int(name, ctx=None):
3011  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3012 
3013  >>> x = Int('x')
3014  >>> is_int(x)
3015  True
3016  >>> is_int(x + 1)
3017  True
3018  """
3019  ctx = _get_ctx(ctx)
3020  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3021 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def Int(name, ctx=None)
Definition: z3py.py:3010
def IntSort(ctx=None)
Definition: z3py.py:2907

◆ Int2BV()

def z3py.Int2BV (   a,
  num_bits 
)
Return the z3 expression Int2BV(a, num_bits).
It is a bit-vector of width num_bits and represents the
modulo of a by 2^num_bits

Definition at line 3732 of file z3py.py.

3732 def Int2BV(a, num_bits):
3733  """Return the z3 expression Int2BV(a, num_bits).
3734  It is a bit-vector of width num_bits and represents the
3735  modulo of a by 2^num_bits
3736  """
3737  ctx = a.ctx
3738  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
3739 
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
def Int2BV(a, num_bits)
Definition: z3py.py:3732

◆ Intersect()

def z3py.Intersect (   args)
Create intersection of regular expressions.
>>> re = Intersect(Re("a"), Re("b"), Re("c"))

Definition at line 10343 of file z3py.py.

10343 def Intersect(*args):
10344  """Create intersection of regular expressions.
10345  >>> re = Intersect(Re("a"), Re("b"), Re("c"))
10346  """
10347  args = _get_args(args)
10348  sz = len(args)
10349  if z3_debug():
10350  _z3_assert(sz > 0, "At least one argument expected.")
10351  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
10352  if sz == 1:
10353  return args[0]
10354  ctx = args[0].ctx
10355  v = (Ast * sz)()
10356  for i in range(sz):
10357  v[i] = args[i].as_ast()
10358  return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
10359 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def Intersect(args)
Definition: z3py.py:10343
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
def is_re(s)
Definition: z3py.py:10307
def z3_debug()
Definition: z3py.py:56

◆ Ints()

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

Referenced by ArithRef.__ge__(), Goal.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ArithRef.__lt__(), Goal.convert_model(), 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(), Lambda(), Goal.prec(), Goal.size(), Store(), Solver.unsat_core(), and Update().

3022 def Ints(names, ctx=None):
3023  """Return a tuple of Integer constants.
3024 
3025  >>> x, y, z = Ints('x y z')
3026  >>> Sum(x, y, z)
3027  x + y + z
3028  """
3029  ctx = _get_ctx(ctx)
3030  if isinstance(names, str):
3031  names = names.split(" ")
3032  return [Int(name, ctx) for name in names]
3033 
def Int(name, ctx=None)
Definition: z3py.py:3010
def Ints(names, ctx=None)
Definition: z3py.py:3022

◆ IntSort()

def z3py.IntSort (   ctx = None)
Return the integer 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 2907 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(), Default(), DisjointSum(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), Full(), FullSet(), ModelRef.get_interp(), get_map_func(), Context.getIntSort(), is_arith_sort(), is_array(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_fp_sort(), is_K(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_select(), is_store(), SeqSortRef.is_string(), IsMember(), IsSubset(), K(), Lambda(), Map(), 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(), SeqSort(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), ArrayRef.sort(), Store(), Sort.translate(), Sort.Translate(), TupleSort(), Update(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

2907 def IntSort(ctx=None):
2908  """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
2909 
2910  >>> IntSort()
2911  Int
2912  >>> x = Const('x', IntSort())
2913  >>> is_int(x)
2914  True
2915  >>> x.sort() == IntSort()
2916  True
2917  >>> x.sort() == BoolSort()
2918  False
2919  """
2920  ctx = _get_ctx(ctx)
2921  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
2922 
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
def IntSort(ctx=None)
Definition: z3py.py:2907

◆ IntToStr()

def z3py.IntToStr (   s)
Convert integer expression to string

Definition at line 10265 of file z3py.py.

Referenced by StrToInt().

10265 def IntToStr(s):
10266  """Convert integer expression to string"""
10267  if not is_expr(s):
10268  s = _py2expr(s)
10269  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
10270 
10271 
def IntToStr(s)
Definition: z3py.py:10265
def is_expr(a)
Definition: z3py.py:1115
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.

◆ IntVal()

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 2954 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(), is_seq(), AstMap.keys(), AstMap.reset(), and SeqSort().

2954 def IntVal(val, ctx=None):
2955  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
2956 
2957  >>> IntVal(1)
2958  1
2959  >>> IntVal("100")
2960  100
2961  """
2962  ctx = _get_ctx(ctx)
2963  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
2964 
def IntVal(val, ctx=None)
Definition: z3py.py:2954
def IntSort(ctx=None)
Definition: z3py.py:2907
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ IntVector()

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

3034 def IntVector(prefix, sz, ctx=None):
3035  """Return a list of integer constants of size `sz`.
3036 
3037  >>> X = IntVector('x', 3)
3038  >>> X
3039  [x__0, x__1, x__2]
3040  >>> Sum(X)
3041  x__0 + x__1 + x__2
3042  """
3043  return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
3044 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
def Int(name, ctx=None)
Definition: z3py.py:3010
def IntVector(prefix, sz, ctx=None)
Definition: z3py.py:3034

◆ is_add()

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

2596 def is_add(a):
2597  """Return `True` if `a` is an expression of the form b + c.
2598 
2599  >>> x, y = Ints('x y')
2600  >>> is_add(x + y)
2601  True
2602  >>> is_add(x - y)
2603  False
2604  """
2605  return is_app_of(a, Z3_OP_ADD)
2606 
def is_app_of(a, k)
Definition: z3py.py:1236
def is_add(a)
Definition: z3py.py:2596

◆ is_algebraic_value()

def z3py.is_algebraic_value (   a)
Return `True` if `a` is an algebraic 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 2583 of file z3py.py.

2583 def is_algebraic_value(a):
2584  """Return `True` if `a` is an algebraic value of sort Real.
2585 
2586  >>> is_algebraic_value(RealVal("3/5"))
2587  False
2588  >>> n = simplify(Sqrt(2))
2589  >>> n
2590  1.4142135623?
2591  >>> is_algebraic_value(n)
2592  True
2593  """
2594  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2595 
def is_arith(a)
Definition: z3py.py:2477
def is_algebraic_value(a)
Definition: z3py.py:2583

◆ is_and()

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

1469 def is_and(a):
1470  """Return `True` if `a` is a Z3 and expression.
1471 
1472  >>> p, q = Bools('p q')
1473  >>> is_and(And(p, q))
1474  True
1475  >>> is_and(Or(p, q))
1476  False
1477  """
1478  return is_app_of(a, Z3_OP_AND)
1479 
def is_and(a)
Definition: z3py.py:1469
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_app()

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

Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), expr.hi(), expr.is_and(), is_app_of(), expr.is_const(), is_const(), expr.is_distinct(), expr.is_eq(), expr.is_false(), expr.is_implies(), expr.is_ite(), expr.is_not(), expr.is_or(), expr.is_true(), expr.is_xor(), expr.lo(), ExprRef.num_args(), expr.operator Z3_app(), and RecAddDefinition().

1137 def is_app(a):
1138  """Return `True` if `a` is a Z3 function application.
1139 
1140  Note that, constants are function applications with 0 arguments.
1141 
1142  >>> a = Int('a')
1143  >>> is_app(a)
1144  True
1145  >>> is_app(a + 1)
1146  True
1147  >>> is_app(IntSort())
1148  False
1149  >>> is_app(1)
1150  False
1151  >>> is_app(IntVal(1))
1152  True
1153  >>> x = Int('x')
1154  >>> is_app(ForAll(x, x >= 0))
1155  False
1156  """
1157  if not isinstance(a, ExprRef):
1158  return False
1159  k = _ast_kind(a.ctx, a)
1160  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
1161 
def is_app(a)
Definition: z3py.py:1137

◆ is_app_of()

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

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

1236 def is_app_of(a, k):
1237  """Return `True` if `a` is an application of the given kind `k`.
1238 
1239  >>> x = Int('x')
1240  >>> n = x + 1
1241  >>> is_app_of(n, Z3_OP_ADD)
1242  True
1243  >>> is_app_of(n, Z3_OP_MUL)
1244  False
1245  """
1246  return is_app(a) and a.decl().kind() == k
1247 
def is_app(a)
Definition: z3py.py:1137
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_arith()

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

2477 def is_arith(a):
2478  """Return `True` if `a` is an arithmetical expression.
2479 
2480  >>> x = Int('x')
2481  >>> is_arith(x)
2482  True
2483  >>> is_arith(x + 1)
2484  True
2485  >>> is_arith(1)
2486  False
2487  >>> is_arith(IntVal(1))
2488  True
2489  >>> y = Real('y')
2490  >>> is_arith(y)
2491  True
2492  >>> is_arith(y + 1)
2493  True
2494  """
2495  return isinstance(a, ArithRef)
2496 
def is_arith(a)
Definition: z3py.py:2477

◆ is_arith_sort()

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

2178 def is_arith_sort(s):
2179  """Return `True` if s is an arithmetical sort (type).
2180 
2181  >>> is_arith_sort(IntSort())
2182  True
2183  >>> is_arith_sort(RealSort())
2184  True
2185  >>> is_arith_sort(BoolSort())
2186  False
2187  >>> n = Int('x') + 1
2188  >>> is_arith_sort(n.sort())
2189  True
2190  """
2191  return isinstance(s, ArithSortRef)
2192 
def is_arith_sort(s)
Definition: z3py.py:2178

◆ is_array()

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

Referenced by sort.array_domain(), sort.array_range(), and expr.operator[]().

4294 def is_array(a):
4295  """Return `True` if `a` is a Z3 array expression.
4296 
4297  >>> a = Array('a', IntSort(), IntSort())
4298  >>> is_array(a)
4299  True
4300  >>> is_array(Store(a, 0, 1))
4301  True
4302  >>> is_array(a[0])
4303  False
4304  """
4305  return isinstance(a, ArrayRef)
4306 
def is_array(a)
Definition: z3py.py:4294

◆ is_array_sort()

def z3py.is_array_sort (   a)

Definition at line 4290 of file z3py.py.

4290 def is_array_sort(a):
4291  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4292 
4293 
def is_array_sort(a)
Definition: z3py.py:4290
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

◆ is_as_array()

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

Definition at line 6240 of file z3py.py.

6240 def is_as_array(n):
6241  """Return true if n is a Z3 expression of the form (_ as-array f)."""
6242  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6243 
def is_as_array(n)
Definition: z3py.py:6240
bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3...

◆ is_ast()

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

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

Definition at line 412 of file z3py.py.

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

412 def is_ast(a):
413  """Return `True` if `a` is an AST node.
414 
415  >>> is_ast(10)
416  False
417  >>> is_ast(IntVal(10))
418  True
419  >>> is_ast(Int('x'))
420  True
421  >>> is_ast(BoolSort())
422  True
423  >>> is_ast(Function('f', IntSort(), IntSort()))
424  True
425  >>> is_ast("x")
426  False
427  >>> is_ast(Solver())
428  False
429  """
430  return isinstance(a, AstRef)
431 
def is_ast(a)
Definition: z3py.py:412

◆ is_bool()

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

Referenced by BoolSort(), and prove().

1422 def is_bool(a):
1423  """Return `True` if `a` is a Z3 Boolean expression.
1424 
1425  >>> p = Bool('p')
1426  >>> is_bool(p)
1427  True
1428  >>> q = Bool('q')
1429  >>> is_bool(And(p, q))
1430  True
1431  >>> x = Real('x')
1432  >>> is_bool(x)
1433  False
1434  >>> is_bool(x == 0)
1435  True
1436  """
1437  return isinstance(a, BoolRef)
1438 
def is_bool(a)
Definition: z3py.py:1422

◆ is_bv()

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

Referenced by BitVec(), sort.bv_size(), fpToIEEEBV(), fpToSBV(), fpToUBV(), Product(), and Sum().

3683 def is_bv(a):
3684  """Return `True` if `a` is a Z3 bit-vector expression.
3685 
3686  >>> b = BitVec('b', 32)
3687  >>> is_bv(b)
3688  True
3689  >>> is_bv(b + 10)
3690  True
3691  >>> is_bv(Int('x'))
3692  False
3693  """
3694  return isinstance(a, BitVecRef)
3695 
def is_bv(a)
Definition: z3py.py:3683

◆ is_bv_sort()

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

3222 def is_bv_sort(s):
3223  """Return True if `s` is a Z3 bit-vector sort.
3224 
3225  >>> is_bv_sort(BitVecSort(32))
3226  True
3227  >>> is_bv_sort(IntSort())
3228  False
3229  """
3230  return isinstance(s, BitVecSortRef)
3231 
def is_bv_sort(s)
Definition: z3py.py:3222

◆ is_bv_value()

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

3696 def is_bv_value(a):
3697  """Return `True` if `a` is a Z3 bit-vector numeral value.
3698 
3699  >>> b = BitVec('b', 32)
3700  >>> is_bv_value(b)
3701  False
3702  >>> b = BitVecVal(10, 32)
3703  >>> b
3704  10
3705  >>> is_bv_value(b)
3706  True
3707  """
3708  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3709 
def is_bv_value(a)
Definition: z3py.py:3696
def is_bv(a)
Definition: z3py.py:3683

◆ is_const()

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

Referenced by Optimize.assert_and_track(), and prove().

1162 def is_const(a):
1163  """Return `True` if `a` is Z3 constant/variable expression.
1164 
1165  >>> a = Int('a')
1166  >>> is_const(a)
1167  True
1168  >>> is_const(a + 1)
1169  False
1170  >>> is_const(1)
1171  False
1172  >>> is_const(IntVal(1))
1173  True
1174  >>> x = Int('x')
1175  >>> is_const(ForAll(x, x >= 0))
1176  False
1177  """
1178  return is_app(a) and a.num_args() == 0
1179 
def is_app(a)
Definition: z3py.py:1137
def is_const(a)
Definition: z3py.py:1162

◆ is_const_array()

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

4307 def is_const_array(a):
4308  """Return `True` if `a` is a Z3 constant array.
4309 
4310  >>> a = K(IntSort(), 10)
4311  >>> is_const_array(a)
4312  True
4313  >>> a = Array('a', IntSort(), IntSort())
4314  >>> is_const_array(a)
4315  False
4316  """
4317  return is_app_of(a, Z3_OP_CONST_ARRAY)
4318 
def is_const_array(a)
Definition: z3py.py:4307
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_default()

def z3py.is_default (   a)
Return `True` if `a` is a Z3 default array expression.
>>> d = Default(K(IntSort(), 10))
>>> is_default(d)
True

Definition at line 4346 of file z3py.py.

4346 def is_default(a):
4347  """Return `True` if `a` is a Z3 default array expression.
4348  >>> d = Default(K(IntSort(), 10))
4349  >>> is_default(d)
4350  True
4351  """
4352  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4353 
def is_default(a)
Definition: z3py.py:4346
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_distinct()

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

1522 def is_distinct(a):
1523  """Return `True` if `a` is a Z3 distinct expression.
1524 
1525  >>> x, y, z = Ints('x y z')
1526  >>> is_distinct(x == y)
1527  False
1528  >>> is_distinct(Distinct(x, y, z))
1529  True
1530  """
1531  return is_app_of(a, Z3_OP_DISTINCT)
1532 
def is_distinct(a)
Definition: z3py.py:1522
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_div()

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

2629 def is_div(a):
2630  """Return `True` if `a` is an expression of the form b / c.
2631 
2632  >>> x, y = Reals('x y')
2633  >>> is_div(x / y)
2634  True
2635  >>> is_div(x + y)
2636  False
2637  >>> x, y = Ints('x y')
2638  >>> is_div(x / y)
2639  False
2640  >>> is_idiv(x / y)
2641  True
2642  """
2643  return is_app_of(a, Z3_OP_DIV)
2644 
def is_div(a)
Definition: z3py.py:2629
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_eq()

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

Referenced by AstRef.__bool__().

1513 def is_eq(a):
1514  """Return `True` if `a` is a Z3 equality expression.
1515 
1516  >>> x, y = Ints('x y')
1517  >>> is_eq(x == y)
1518  True
1519  """
1520  return is_app_of(a, Z3_OP_EQ)
1521 
def is_eq(a)
Definition: z3py.py:1513
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_expr()

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
>>> is_expr(FPVal(1.0))
True

Definition at line 1115 of file z3py.py.

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

1115 def is_expr(a):
1116  """Return `True` if `a` is a Z3 expression.
1117 
1118  >>> a = Int('a')
1119  >>> is_expr(a)
1120  True
1121  >>> is_expr(a + 1)
1122  True
1123  >>> is_expr(IntSort())
1124  False
1125  >>> is_expr(1)
1126  False
1127  >>> is_expr(IntVal(1))
1128  True
1129  >>> x = Int('x')
1130  >>> is_expr(ForAll(x, x >= 0))
1131  True
1132  >>> is_expr(FPVal(1.0))
1133  True
1134  """
1135  return isinstance(a, ExprRef)
1136 
def is_expr(a)
Definition: z3py.py:1115

◆ is_false()

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

Referenced by AstRef.__bool__(), and BoolVal().

1456 def is_false(a):
1457  """Return `True` if `a` is the Z3 false expression.
1458 
1459  >>> p = Bool('p')
1460  >>> is_false(p)
1461  False
1462  >>> is_false(False)
1463  False
1464  >>> is_false(BoolVal(False))
1465  True
1466  """
1467  return is_app_of(a, Z3_OP_FALSE)
1468 
def is_app_of(a, k)
Definition: z3py.py:1236
def is_false(a)
Definition: z3py.py:1456

◆ is_finite_domain()

def z3py.is_finite_domain (   a)
Return `True` if `a` is a Z3 finite-domain expression.

>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain(b)
True
>>> is_finite_domain(Int('x'))
False

Definition at line 7248 of file z3py.py.

Referenced by is_finite_domain_value().

7248 def is_finite_domain(a):
7249  """Return `True` if `a` is a Z3 finite-domain expression.
7250 
7251  >>> s = FiniteDomainSort('S', 100)
7252  >>> b = Const('b', s)
7253  >>> is_finite_domain(b)
7254  True
7255  >>> is_finite_domain(Int('x'))
7256  False
7257  """
7258  return isinstance(a, FiniteDomainRef)
7259 
7260 
def is_finite_domain(a)
Definition: z3py.py:7248

◆ is_finite_domain_sort()

def z3py.is_finite_domain_sort (   s)
Return True if `s` is a Z3 finite-domain sort.

>>> is_finite_domain_sort(FiniteDomainSort('S', 100))
True
>>> is_finite_domain_sort(IntSort())
False

Definition at line 7226 of file z3py.py.

Referenced by FiniteDomainVal().

7226 def is_finite_domain_sort(s):
7227  """Return True if `s` is a Z3 finite-domain sort.
7228 
7229  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7230  True
7231  >>> is_finite_domain_sort(IntSort())
7232  False
7233  """
7234  return isinstance(s, FiniteDomainSortRef)
7235 
7236 
def is_finite_domain_sort(s)
Definition: z3py.py:7226

◆ is_finite_domain_value()

def z3py.is_finite_domain_value (   a)
Return `True` if `a` is a Z3 finite-domain value.

>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain_value(b)
False
>>> b = FiniteDomainVal(10, s)
>>> b
10
>>> is_finite_domain_value(b)
True

Definition at line 7301 of file z3py.py.

7301 def is_finite_domain_value(a):
7302  """Return `True` if `a` is a Z3 finite-domain value.
7303 
7304  >>> s = FiniteDomainSort('S', 100)
7305  >>> b = Const('b', s)
7306  >>> is_finite_domain_value(b)
7307  False
7308  >>> b = FiniteDomainVal(10, s)
7309  >>> b
7310  10
7311  >>> is_finite_domain_value(b)
7312  True
7313  """
7314  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7315 
7316 
def is_finite_domain_value(a)
Definition: z3py.py:7301
def is_finite_domain(a)
Definition: z3py.py:7248

◆ is_fp()

def z3py.is_fp (   a)
Return `True` if `a` is a Z3 floating-point expression.

>>> b = FP('b', FPSort(8, 24))
>>> is_fp(b)
True
>>> is_fp(b + 1.0)
True
>>> is_fp(Int('x'))
False

Definition at line 9154 of file z3py.py.

Referenced by FP(), fpToIEEEBV(), fpToReal(), fpToSBV(), and fpToUBV().

9154 def is_fp(a):
9155  """Return `True` if `a` is a Z3 floating-point expression.
9156 
9157  >>> b = FP('b', FPSort(8, 24))
9158  >>> is_fp(b)
9159  True
9160  >>> is_fp(b + 1.0)
9161  True
9162  >>> is_fp(Int('x'))
9163  False
9164  """
9165  return isinstance(a, FPRef)
9166 
def is_fp(a)
Definition: z3py.py:9154

◆ is_fp_sort()

def z3py.is_fp_sort (   s)
Return True if `s` is a Z3 floating-point sort.

>>> is_fp_sort(FPSort(8, 24))
True
>>> is_fp_sort(IntSort())
False

Definition at line 8771 of file z3py.py.

8771 def is_fp_sort(s):
8772  """Return True if `s` is a Z3 floating-point sort.
8773 
8774  >>> is_fp_sort(FPSort(8, 24))
8775  True
8776  >>> is_fp_sort(IntSort())
8777  False
8778  """
8779  return isinstance(s, FPSortRef)
8780 
def is_fp_sort(s)
Definition: z3py.py:8771

◆ is_fp_value()

def z3py.is_fp_value (   a)
Return `True` if `a` is a Z3 floating-point numeral value.

>>> b = FP('b', FPSort(8, 24))
>>> is_fp_value(b)
False
>>> b = FPVal(1.0, FPSort(8, 24))
>>> b
1
>>> is_fp_value(b)
True

Definition at line 9167 of file z3py.py.

9167 def is_fp_value(a):
9168  """Return `True` if `a` is a Z3 floating-point numeral value.
9169 
9170  >>> b = FP('b', FPSort(8, 24))
9171  >>> is_fp_value(b)
9172  False
9173  >>> b = FPVal(1.0, FPSort(8, 24))
9174  >>> b
9175  1
9176  >>> is_fp_value(b)
9177  True
9178  """
9179  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9180 
def is_fp_value(a)
Definition: z3py.py:9167
def is_fp(a)
Definition: z3py.py:9154

◆ is_fprm()

def z3py.is_fprm (   a)
Return `True` if `a` is a Z3 floating-point rounding mode expression.

>>> rm = RNE()
>>> is_fprm(rm)
True
>>> rm = 1.0
>>> is_fprm(rm)
False

Definition at line 9018 of file z3py.py.

9018 def is_fprm(a):
9019  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9020 
9021  >>> rm = RNE()
9022  >>> is_fprm(rm)
9023  True
9024  >>> rm = 1.0
9025  >>> is_fprm(rm)
9026  False
9027  """
9028  return isinstance(a, FPRMRef)
9029 
def is_fprm(a)
Definition: z3py.py:9018

◆ is_fprm_sort()

def z3py.is_fprm_sort (   s)
Return True if `s` is a Z3 floating-point rounding mode sort.

>>> is_fprm_sort(FPSort(8, 24))
False
>>> is_fprm_sort(RNE().sort())
True

Definition at line 8781 of file z3py.py.

8781 def is_fprm_sort(s):
8782  """Return True if `s` is a Z3 floating-point rounding mode sort.
8783 
8784  >>> is_fprm_sort(FPSort(8, 24))
8785  False
8786  >>> is_fprm_sort(RNE().sort())
8787  True
8788  """
8789  return isinstance(s, FPRMSortRef)
8790 
def is_fprm_sort(s)
Definition: z3py.py:8781

◆ is_fprm_value()

def z3py.is_fprm_value (   a)
Return `True` if `a` is a Z3 floating-point rounding mode numeral value.

Definition at line 9030 of file z3py.py.

9030 def is_fprm_value(a):
9031  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9032  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9033 
def is_fprm_value(a)
Definition: z3py.py:9030
def is_fprm(a)
Definition: z3py.py:9018

◆ is_func_decl()

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

Referenced by prove().

787 def is_func_decl(a):
788  """Return `True` if `a` is a Z3 function declaration.
789 
790  >>> f = Function('f', IntSort(), IntSort())
791  >>> is_func_decl(f)
792  True
793  >>> x = Real('x')
794  >>> is_func_decl(x)
795  False
796  """
797  return isinstance(a, FuncDeclRef)
798 
def is_func_decl(a)
Definition: z3py.py:787

◆ is_ge()

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

2689 def is_ge(a):
2690  """Return `True` if `a` is an expression of the form b >= c.
2691 
2692  >>> x, y = Ints('x y')
2693  >>> is_ge(x >= y)
2694  True
2695  >>> is_ge(x == y)
2696  False
2697  """
2698  return is_app_of(a, Z3_OP_GE)
2699 
def is_ge(a)
Definition: z3py.py:2689
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_gt()

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

2700 def is_gt(a):
2701  """Return `True` if `a` is an expression of the form b > c.
2702 
2703  >>> x, y = Ints('x y')
2704  >>> is_gt(x > y)
2705  True
2706  >>> is_gt(x == y)
2707  False
2708  """
2709  return is_app_of(a, Z3_OP_GT)
2710 
def is_gt(a)
Definition: z3py.py:2700
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_idiv()

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

Referenced by is_div().

2645 def is_idiv(a):
2646  """Return `True` if `a` is an expression of the form b div c.
2647 
2648  >>> x, y = Ints('x y')
2649  >>> is_idiv(x / y)
2650  True
2651  >>> is_idiv(x + y)
2652  False
2653  """
2654  return is_app_of(a, Z3_OP_IDIV)
2655 
def is_idiv(a)
Definition: z3py.py:2645
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_implies()

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

>>> p, q = Bools('p q')
>>> is_implies(Implies(p, q))
True
>>> is_implies(And(p, q))
False

Definition at line 1491 of file z3py.py.

1491 def is_implies(a):
1492  """Return `True` if `a` is a Z3 implication expression.
1493 
1494  >>> p, q = Bools('p q')
1495  >>> is_implies(Implies(p, q))
1496  True
1497  >>> is_implies(And(p, q))
1498  False
1499  """
1500  return is_app_of(a, Z3_OP_IMPLIES)
1501 
def is_implies(a)
Definition: z3py.py:1491
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_int()

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

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

2497 def is_int(a):
2498  """Return `True` if `a` is an integer expression.
2499 
2500  >>> x = Int('x')
2501  >>> is_int(x + 1)
2502  True
2503  >>> is_int(1)
2504  False
2505  >>> is_int(IntVal(1))
2506  True
2507  >>> y = Real('y')
2508  >>> is_int(y)
2509  False
2510  >>> is_int(y + 1)
2511  False
2512  """
2513  return is_arith(a) and a.is_int()
2514 
def is_arith(a)
Definition: z3py.py:2477
def is_int(a)
Definition: z3py.py:2497

◆ is_int_value()

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

2539 def is_int_value(a):
2540  """Return `True` if `a` is an integer value of sort Int.
2541 
2542  >>> is_int_value(IntVal(1))
2543  True
2544  >>> is_int_value(1)
2545  False
2546  >>> is_int_value(Int('x'))
2547  False
2548  >>> n = Int('x') + 1
2549  >>> n
2550  x + 1
2551  >>> n.arg(1)
2552  1
2553  >>> is_int_value(n.arg(1))
2554  True
2555  >>> is_int_value(RealVal("1/3"))
2556  False
2557  >>> is_int_value(RealVal(1))
2558  False
2559  """
2560  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2561 
def is_int_value(a)
Definition: z3py.py:2539
def is_arith(a)
Definition: z3py.py:2477

◆ is_is_int()

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

2711 def is_is_int(a):
2712  """Return `True` if `a` is an expression of the form IsInt(b).
2713 
2714  >>> x = Real('x')
2715  >>> is_is_int(IsInt(x))
2716  True
2717  >>> is_is_int(x)
2718  False
2719  """
2720  return is_app_of(a, Z3_OP_IS_INT)
2721 
def is_app_of(a, k)
Definition: z3py.py:1236
def is_is_int(a)
Definition: z3py.py:2711

◆ is_K()

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

4319 def is_K(a):
4320  """Return `True` if `a` is a Z3 constant array.
4321 
4322  >>> a = K(IntSort(), 10)
4323  >>> is_K(a)
4324  True
4325  >>> a = Array('a', IntSort(), IntSort())
4326  >>> is_K(a)
4327  False
4328  """
4329  return is_app_of(a, Z3_OP_CONST_ARRAY)
4330 
def is_K(a)
Definition: z3py.py:4319
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_le()

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

2667 def is_le(a):
2668  """Return `True` if `a` is an expression of the form b <= c.
2669 
2670  >>> x, y = Ints('x y')
2671  >>> is_le(x <= y)
2672  True
2673  >>> is_le(x < y)
2674  False
2675  """
2676  return is_app_of(a, Z3_OP_LE)
2677 
def is_le(a)
Definition: z3py.py:2667
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_lt()

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

2678 def is_lt(a):
2679  """Return `True` if `a` is an expression of the form b < c.
2680 
2681  >>> x, y = Ints('x y')
2682  >>> is_lt(x < y)
2683  True
2684  >>> is_lt(x == y)
2685  False
2686  """
2687  return is_app_of(a, Z3_OP_LT)
2688 
def is_lt(a)
Definition: z3py.py:2678
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_map()

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

4331 def is_map(a):
4332  """Return `True` if `a` is a Z3 map array expression.
4333 
4334  >>> f = Function('f', IntSort(), IntSort())
4335  >>> b = Array('b', IntSort(), IntSort())
4336  >>> a = Map(f, b)
4337  >>> a
4338  Map(f, b)
4339  >>> is_map(a)
4340  True
4341  >>> is_map(b)
4342  False
4343  """
4344  return is_app_of(a, Z3_OP_ARRAY_MAP)
4345 
def is_map(a)
Definition: z3py.py:4331
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_mod()

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

2656 def is_mod(a):
2657  """Return `True` if `a` is an expression of the form b % c.
2658 
2659  >>> x, y = Ints('x y')
2660  >>> is_mod(x % y)
2661  True
2662  >>> is_mod(x + y)
2663  False
2664  """
2665  return is_app_of(a, Z3_OP_MOD)
2666 
def is_mod(a)
Definition: z3py.py:2656
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_mul()

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

2607 def is_mul(a):
2608  """Return `True` if `a` is an expression of the form b * c.
2609 
2610  >>> x, y = Ints('x y')
2611  >>> is_mul(x * y)
2612  True
2613  >>> is_mul(x - y)
2614  False
2615  """
2616  return is_app_of(a, Z3_OP_MUL)
2617 
def is_app_of(a, k)
Definition: z3py.py:1236
def is_mul(a)
Definition: z3py.py:2607

◆ is_not()

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

1502 def is_not(a):
1503  """Return `True` if `a` is a Z3 not expression.
1504 
1505  >>> p = Bool('p')
1506  >>> is_not(p)
1507  False
1508  >>> is_not(Not(p))
1509  True
1510  """
1511  return is_app_of(a, Z3_OP_NOT)
1512 
def is_not(a)
Definition: z3py.py:1502
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_or()

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

1480 def is_or(a):
1481  """Return `True` if `a` is a Z3 or expression.
1482 
1483  >>> p, q = Bools('p q')
1484  >>> is_or(Or(p, q))
1485  True
1486  >>> is_or(And(p, q))
1487  False
1488  """
1489  return is_app_of(a, Z3_OP_OR)
1490 
def is_or(a)
Definition: z3py.py:1480
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_pattern()

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

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

Referenced by MultiPattern().

1759 def is_pattern(a):
1760  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1761 
1762  >>> f = Function('f', IntSort(), IntSort())
1763  >>> x = Int('x')
1764  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1765  >>> q
1766  ForAll(x, f(x) == 0)
1767  >>> q.num_patterns()
1768  1
1769  >>> is_pattern(q.pattern(0))
1770  True
1771  >>> q.pattern(0)
1772  f(Var(0))
1773  """
1774  return isinstance(a, PatternRef)
1775 
def is_pattern(a)
Definition: z3py.py:1759

◆ is_probe()

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

Referenced by eq().

8060 def is_probe(p):
8061  """Return `True` if `p` is a Z3 probe.
8062 
8063  >>> is_probe(Int('x'))
8064  False
8065  >>> is_probe(Probe('memory'))
8066  True
8067  """
8068  return isinstance(p, Probe)
8069 
def is_probe(p)
Definition: z3py.py:8060

◆ is_quantifier()

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

Referenced by expr.body(), and Exists().

1997 def is_quantifier(a):
1998  """Return `True` if `a` is a Z3 quantifier.
1999 
2000  >>> f = Function('f', IntSort(), IntSort())
2001  >>> x = Int('x')
2002  >>> q = ForAll(x, f(x) == 0)
2003  >>> is_quantifier(q)
2004  True
2005  >>> is_quantifier(f(x))
2006  False
2007  """
2008  return isinstance(a, QuantifierRef)
2009 
def is_quantifier(a)
Definition: z3py.py:1997

◆ is_rational_value()

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

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

2562 def is_rational_value(a):
2563  """Return `True` if `a` is rational value of sort Real.
2564 
2565  >>> is_rational_value(RealVal(1))
2566  True
2567  >>> is_rational_value(RealVal("3/5"))
2568  True
2569  >>> is_rational_value(IntVal(1))
2570  False
2571  >>> is_rational_value(1)
2572  False
2573  >>> n = Real('x') + 1
2574  >>> n.arg(1)
2575  1
2576  >>> is_rational_value(n.arg(1))
2577  True
2578  >>> is_rational_value(Real('x'))
2579  False
2580  """
2581  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2582 
def is_arith(a)
Definition: z3py.py:2477
def is_rational_value(a)
Definition: z3py.py:2562

◆ is_re()

def z3py.is_re (   s)

Definition at line 10307 of file z3py.py.

10307 def is_re(s):
10308  return isinstance(s, ReRef)
10309 
10310 
def is_re(s)
Definition: z3py.py:10307

◆ is_real()

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

Referenced by fpToReal(), sort.is_arith(), Real(), and RealSort().

2515 def is_real(a):
2516  """Return `True` if `a` is a real expression.
2517 
2518  >>> x = Int('x')
2519  >>> is_real(x + 1)
2520  False
2521  >>> y = Real('y')
2522  >>> is_real(y)
2523  True
2524  >>> is_real(y + 1)
2525  True
2526  >>> is_real(1)
2527  False
2528  >>> is_real(RealVal(1))
2529  True
2530  """
2531  return is_arith(a) and a.is_real()
2532 
def is_real(a)
Definition: z3py.py:2515
def is_arith(a)
Definition: z3py.py:2477

◆ is_select()

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

4538 def is_select(a):
4539  """Return `True` if `a` is a Z3 array select application.
4540 
4541  >>> a = Array('a', IntSort(), IntSort())
4542  >>> is_select(a)
4543  False
4544  >>> i = Int('i')
4545  >>> is_select(a[i])
4546  True
4547  """
4548  return is_app_of(a, Z3_OP_SELECT)
4549 
def is_select(a)
Definition: z3py.py:4538
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_seq()

def z3py.is_seq (   a)
Return `True` if `a` is a Z3 sequence expression.
>>> print (is_seq(Unit(IntVal(0))))
True
>>> print (is_seq(StringVal("abc")))
True

Definition at line 10052 of file z3py.py.

Referenced by expr.operator[]().

10052 def is_seq(a):
10053  """Return `True` if `a` is a Z3 sequence expression.
10054  >>> print (is_seq(Unit(IntVal(0))))
10055  True
10056  >>> print (is_seq(StringVal("abc")))
10057  True
10058  """
10059  return isinstance(a, SeqRef)
10060 
def is_seq(a)
Definition: z3py.py:10052

◆ is_sort()

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

Referenced by Function(), prove(), RecFunction(), and Var().

596 def is_sort(s):
597  """Return `True` if `s` is a Z3 sort.
598 
599  >>> is_sort(IntSort())
600  True
601  >>> is_sort(Int('x'))
602  False
603  >>> is_expr(Int('x'))
604  True
605  """
606  return isinstance(s, SortRef)
607 
def is_sort(s)
Definition: z3py.py:596

◆ is_store()

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

4550 def is_store(a):
4551  """Return `True` if `a` is a Z3 array store application.
4552 
4553  >>> a = Array('a', IntSort(), IntSort())
4554  >>> is_store(a)
4555  False
4556  >>> is_store(Store(a, 0, 1))
4557  True
4558  """
4559  return is_app_of(a, Z3_OP_STORE)
4560 
def is_store(a)
Definition: z3py.py:4550
def is_app_of(a, k)
Definition: z3py.py:1236

◆ is_string()

def z3py.is_string (   a)
Return `True` if `a` is a Z3 string expression.
>>> print (is_string(StringVal("ab")))
True

Definition at line 10061 of file z3py.py.

10061 def