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  PropClosures
 
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  UserPropagateBase
 
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 FreshFunction (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, logFile=None)
 
def SimpleSolver (ctx=None, logFile=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)
 
def ensure_prop_closures ()
 
def user_prop_push (ctx)
 
def user_prop_pop (ctx, num_scopes)
 
def user_prop_fresh (id, ctx)
 
def user_prop_fixed (ctx, cb, id, value)
 
def user_prop_final (ctx, cb)
 
def user_prop_eq (ctx, cb, x, y)
 
def user_prop_diseq (ctx, cb, x, y)
 

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

1708 def And(*args):
1709  """Create a Z3 and-expression or and-probe.
1710 
1711  >>> p, q, r = Bools('p q r')
1712  >>> And(p, q, r)
1713  And(p, q, r)
1714  >>> P = BoolVector('p', 5)
1715  >>> And(P)
1716  And(p__0, p__1, p__2, p__3, p__4)
1717  """
1718  last_arg = None
1719  if len(args) > 0:
1720  last_arg = args[len(args)-1]
1721  if isinstance(last_arg, Context):
1722  ctx = args[len(args)-1]
1723  args = args[:len(args)-1]
1724  elif len(args) == 1 and isinstance(args[0], AstVector):
1725  ctx = args[0].ctx
1726  args = [a for a in args[0]]
1727  else:
1728  ctx = None
1729  args = _get_args(args)
1730  ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1731  if z3_debug():
1732  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1733  if _has_probe(args):
1734  return _probe_and(args, ctx)
1735  else:
1736  args = _coerce_expr_list(args, ctx)
1737  _args, sz = _to_ast_array(args)
1738  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1739 
def And(args)
Definition: z3py.py:1708
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 7803 of file z3py.py.

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

7803 def AndThen(*ts, **ks):
7804  """Return a tactic that applies the tactics in `*ts` in sequence.
7805 
7806  >>> x, y = Ints('x y')
7807  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
7808  >>> t(And(x == 0, y > x + 1))
7809  [[Not(y <= 1)]]
7810  >>> t(And(x == 0, y > x + 1)).as_expr()
7811  Not(y <= 1)
7812  """
7813  if z3_debug():
7814  _z3_assert(len(ts) >= 2, "At least two arguments expected")
7815  ctx = ks.get('ctx', None)
7816  num = len(ts)
7817  r = ts[0]
7818  for i in range(num - 1):
7819  r = _and_then(r, ts[i+1], ctx)
7820  return r
7821 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
def AndThen(ts, ks)
Definition: z3py.py:7803
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 5121 of file z3py.py.

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

5121 def args2params(arguments, keywords, ctx=None):
5122  """Convert python arguments into a Z3_params object.
5123  A ':' is added to the keywords, and '_' is replaced with '-'
5124 
5125  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5126  (params model true relevancy 2 elim_and true)
5127  """
5128  if z3_debug():
5129  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5130  prev = None
5131  r = ParamsRef(ctx)
5132  for a in arguments:
5133  if prev is None:
5134  prev = a
5135  else:
5136  r.set(prev, a)
5137  prev = None
5138  for k in keywords:
5139  v = keywords[k]
5140  r.set(k, v)
5141  return r
5142 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5121
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 4454 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().

4454 def Array(name, dom, rng):
4455  """Return an array constant named `name` with the given domain and range sorts.
4456 
4457  >>> a = Array('a', IntSort(), IntSort())
4458  >>> a.sort()
4459  Array(Int, Int)
4460  >>> a[0]
4461  a[0]
4462  """
4463  s = ArraySort(dom, rng)
4464  ctx = s.ctx
4465  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4466 
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:4422
def to_symbol(s, ctx=None)
Definition: z3py.py:109
def Array(name, dom, rng)
Definition: z3py.py:4454

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

Referenced by ArraySortRef.domain(), ArraySort< D, BoolSort >.getRange(), Context.MkArraySort(), ArraySortRef.range(), and Sort.Translate().

4422 def ArraySort(*sig):
4423  """Return the Z3 array sort with the given domain and range sorts.
4424 
4425  >>> A = ArraySort(IntSort(), BoolSort())
4426  >>> A
4427  Array(Int, Bool)
4428  >>> A.domain()
4429  Int
4430  >>> A.range()
4431  Bool
4432  >>> AA = ArraySort(IntSort(), A)
4433  >>> AA
4434  Array(Int, Array(Int, Bool))
4435  """
4436  sig = _get_args(sig)
4437  if z3_debug():
4438  _z3_assert(len(sig) > 1, "At least two arguments expected")
4439  arity = len(sig) - 1
4440  r = sig[arity]
4441  d = sig[0]
4442  if z3_debug():
4443  for s in sig:
4444  _z3_assert(is_sort(s), "Z3 sort expected")
4445  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4446  ctx = d.ctx
4447  if len(sig) == 2:
4448  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4449  dom = (Sort * arity)()
4450  for i in range(arity):
4451  dom[i] = sig[i].ast
4452  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4453 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
def ArraySort(sig)
Definition: z3py.py:4422
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 8384 of file z3py.py.

8384 def AtLeast(*args):
8385  """Create an at-most Pseudo-Boolean k constraint.
8386 
8387  >>> a, b, c = Bools('a b c')
8388  >>> f = AtLeast(a, b, c, 2)
8389  """
8390  args = _get_args(args)
8391  if z3_debug():
8392  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8393  ctx = _ctx_from_ast_arg_list(args)
8394  if z3_debug():
8395  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8396  args1 = _coerce_expr_list(args[:-1], ctx)
8397  k = args[-1]
8398  _args, sz = _to_ast_array(args1)
8399  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8400 
def AtLeast(args)
Definition: z3py.py:8384
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 8367 of file z3py.py.

8367 def AtMost(*args):
8368  """Create an at-most Pseudo-Boolean k constraint.
8369 
8370  >>> a, b, c = Bools('a b c')
8371  >>> f = AtMost(a, b, c, 2)
8372  """
8373  args = _get_args(args)
8374  if z3_debug():
8375  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8376  ctx = _ctx_from_ast_arg_list(args)
8377  if z3_debug():
8378  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8379  args1 = _coerce_expr_list(args[:-1], ctx)
8380  k = args[-1]
8381  _args, sz = _to_ast_array(args1)
8382  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8383 
def AtMost(args)
Definition: z3py.py:8367
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 3821 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().

3821 def BitVec(name, bv, ctx=None):
3822  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3823  If `ctx=None`, then the global context is used.
3824 
3825  >>> x = BitVec('x', 16)
3826  >>> is_bv(x)
3827  True
3828  >>> x.size()
3829  16
3830  >>> x.sort()
3831  BitVec(16)
3832  >>> word = BitVecSort(16)
3833  >>> x2 = BitVec('x', word)
3834  >>> eq(x, x2)
3835  True
3836  """
3837  if isinstance(bv, BitVecSortRef):
3838  ctx = bv.ctx
3839  else:
3840  ctx = _get_ctx(ctx)
3841  bv = BitVecSort(bv, ctx)
3842  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
3843 
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:3821
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3791

◆ 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 3844 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().

3844 def BitVecs(names, bv, ctx=None):
3845  """Return a tuple of bit-vector constants of size bv.
3846 
3847  >>> x, y, z = BitVecs('x y z', 16)
3848  >>> x.size()
3849  16
3850  >>> x.sort()
3851  BitVec(16)
3852  >>> Sum(x, y, z)
3853  0 + x + y + z
3854  >>> Product(x, y, z)
3855  1*x*y*z
3856  >>> simplify(Product(x, y, z))
3857  x*y*z
3858  """
3859  ctx = _get_ctx(ctx)
3860  if isinstance(names, str):
3861  names = names.split(" ")
3862  return [BitVec(name, bv, ctx) for name in names]
3863 
def BitVec(name, bv, ctx=None)
Definition: z3py.py:3821
def BitVecs(names, bv, ctx=None)
Definition: z3py.py:3844

◆ 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 3791 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().

3791 def BitVecSort(sz, ctx=None):
3792  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3793 
3794  >>> Byte = BitVecSort(8)
3795  >>> Word = BitVecSort(16)
3796  >>> Byte
3797  BitVec(8)
3798  >>> x = Const('x', Byte)
3799  >>> eq(x, BitVec('x', 8))
3800  True
3801  """
3802  ctx = _get_ctx(ctx)
3803  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
3804 
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:3791

◆ 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 3805 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().

3805 def BitVecVal(val, bv, ctx=None):
3806  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3807 
3808  >>> v = BitVecVal(10, 32)
3809  >>> v
3810  10
3811  >>> print("0x%.8x" % v.as_long())
3812  0x0000000a
3813  """
3814  if is_bv_sort(bv):
3815  ctx = bv.ctx
3816  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3817  else:
3818  ctx = _get_ctx(ctx)
3819  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3820 
def BitVecVal(val, bv, ctx=None)
Definition: z3py.py:3805
def is_bv_sort(s)
Definition: z3py.py:3269
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3791
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 1596 of file z3py.py.

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

1596 def Bool(name, ctx=None):
1597  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1598 
1599  >>> p = Bool('p')
1600  >>> q = Bool('q')
1601  >>> And(p, q)
1602  And(p, q)
1603  """
1604  ctx = _get_ctx(ctx)
1605  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1606 
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:1596
def BoolSort(ctx=None)
Definition: z3py.py:1561

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

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

1607 def Bools(names, ctx=None):
1608  """Return a tuple of Boolean constants.
1609 
1610  `names` is a single string containing all names separated by blank spaces.
1611  If `ctx=None`, then the global context is used.
1612 
1613  >>> p, q, r = Bools('p q r')
1614  >>> And(p, Or(q, r))
1615  And(p, Or(q, r))
1616  """
1617  ctx = _get_ctx(ctx)
1618  if isinstance(names, str):
1619  names = names.split(" ")
1620  return [Bool(name, ctx) for name in names]
1621 
def Bools(names, ctx=None)
Definition: z3py.py:1607
def Bool(name, ctx=None)
Definition: z3py.py:1596

◆ 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 1561 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().

1561 def BoolSort(ctx=None):
1562  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1563 
1564  >>> BoolSort()
1565  Bool
1566  >>> p = Const('p', BoolSort())
1567  >>> is_bool(p)
1568  True
1569  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1570  >>> r(0, 1)
1571  r(0, 1)
1572  >>> is_bool(r(0, 1))
1573  True
1574  """
1575  ctx = _get_ctx(ctx)
1576  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1577 
def is_bool(a)
Definition: z3py.py:1450
def BoolSort(ctx=None)
Definition: z3py.py:1561

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

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

1578 def BoolVal(val, ctx=None):
1579  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1580 
1581  >>> BoolVal(True)
1582  True
1583  >>> is_true(BoolVal(True))
1584  True
1585  >>> is_true(True)
1586  False
1587  >>> is_false(BoolVal(False))
1588  True
1589  """
1590  ctx = _get_ctx(ctx)
1591  if val == False:
1592  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1593  else:
1594  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1595 
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:1578

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

Referenced by And(), and Or().

1622 def BoolVector(prefix, sz, ctx=None):
1623  """Return a list of Boolean constants of size `sz`.
1624 
1625  The constants are named using the given prefix.
1626  If `ctx=None`, then the global context is used.
1627 
1628  >>> P = BoolVector('p', 3)
1629  >>> P
1630  [p__0, p__1, p__2]
1631  >>> And(P)
1632  And(p__0, p__1, p__2)
1633  """
1634  return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
1635 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
def BoolVector(prefix, sz, ctx=None)
Definition: z3py.py:1622
def Bool(name, ctx=None)
Definition: z3py.py:1596

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

3761 def BV2Int(a, is_signed=False):
3762  """Return the Z3 expression BV2Int(a).
3763 
3764  >>> b = BitVec('b', 3)
3765  >>> BV2Int(b).sort()
3766  Int
3767  >>> x = Int('x')
3768  >>> x > BV2Int(b)
3769  x > BV2Int(b)
3770  >>> x > BV2Int(b, is_signed=False)
3771  x > BV2Int(b)
3772  >>> x > BV2Int(b, is_signed=True)
3773  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3774  >>> solve(x > BV2Int(b), b == 1, x < 3)
3775  [x = 2, b = 1]
3776  """
3777  if z3_debug():
3778  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
3779  ctx = a.ctx
3780 
3781  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3782 
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:3761
def is_bv(a)
Definition: z3py.py:3734

◆ BVAddNoOverflow()

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

Definition at line 4216 of file z3py.py.

4216 def BVAddNoOverflow(a, b, signed):
4217  """A predicate the determines that bit-vector addition does not overflow"""
4218  _check_bv_args(a, b)
4219  a, b = _coerce_exprs(a, b)
4220  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4221 
def BVAddNoOverflow(a, b, signed)
Definition: z3py.py:4216
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 4222 of file z3py.py.

4222 def BVAddNoUnderflow(a, b):
4223  """A predicate the determines that signed bit-vector addition does not underflow"""
4224  _check_bv_args(a, b)
4225  a, b = _coerce_exprs(a, b)
4226  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4227 
def BVAddNoUnderflow(a, b)
Definition: z3py.py:4222
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 4253 of file z3py.py.

4253 def BVMulNoOverflow(a, b, signed):
4254  """A predicate the determines that bit-vector multiplication does not overflow"""
4255  _check_bv_args(a, b)
4256  a, b = _coerce_exprs(a, b)
4257  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4258 
4259 
def BVMulNoOverflow(a, b, signed)
Definition: z3py.py:4253
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 4260 of file z3py.py.

4260 def BVMulNoUnderflow(a, b):
4261  """A predicate the determines that bit-vector signed multiplication does not underflow"""
4262  _check_bv_args(a, b)
4263  a, b = _coerce_exprs(a, b)
4264  return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4265 
4266 
4267 
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:4260

◆ BVRedAnd()

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

Definition at line 4204 of file z3py.py.

4204 def BVRedAnd(a):
4205  """Return the reduction-and expression of `a`."""
4206  if z3_debug():
4207  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4208  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4209 
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:4204
def z3_debug()
Definition: z3py.py:56
def is_bv(a)
Definition: z3py.py:3734

◆ BVRedOr()

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

Definition at line 4210 of file z3py.py.

4210 def BVRedOr(a):
4211  """Return the reduction-or expression of `a`."""
4212  if z3_debug():
4213  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4214  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4215 
def BVRedOr(a)
Definition: z3py.py:4210
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:3734

◆ BVSDivNoOverflow()

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

Definition at line 4241 of file z3py.py.

4241 def BVSDivNoOverflow(a, b):
4242  """A predicate the determines that bit-vector signed division does not overflow"""
4243  _check_bv_args(a, b)
4244  a, b = _coerce_exprs(a, b)
4245  return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4246 
def BVSDivNoOverflow(a, b)
Definition: z3py.py:4241
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 4247 of file z3py.py.

4247 def BVSNegNoOverflow(a):
4248  """A predicate the determines that bit-vector unary negation does not overflow"""
4249  if z3_debug():
4250  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4251  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4252 
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:4247
def is_bv(a)
Definition: z3py.py:3734

◆ BVSubNoOverflow()

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

Definition at line 4228 of file z3py.py.

4228 def BVSubNoOverflow(a, b):
4229  """A predicate the determines that bit-vector subtraction does not overflow"""
4230  _check_bv_args(a, b)
4231  a, b = _coerce_exprs(a, b)
4232  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4233 
4234 
def BVSubNoOverflow(a, b)
Definition: z3py.py:4228
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 4235 of file z3py.py.

4235 def BVSubNoUnderflow(a, b, signed):
4236  """A predicate the determines that bit-vector subtraction does not underflow"""
4237  _check_bv_args(a, b)
4238  a, b = _coerce_exprs(a, b)
4239  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4240 
def BVSubNoUnderflow(a, b, signed)
Definition: z3py.py:4235
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 3219 of file z3py.py.

3219 def Cbrt(a, ctx=None):
3220  """ Return a Z3 expression which represents the cubic root of a.
3221 
3222  >>> x = Real('x')
3223  >>> Cbrt(x)
3224  x**(1/3)
3225  """
3226  if not is_expr(a):
3227  ctx = _get_ctx(ctx)
3228  a = RealVal(a, ctx)
3229  return a ** "1/3"
3230 
def Cbrt(a, ctx=None)
Definition: z3py.py:3219
def RealVal(val, ctx=None)
Definition: z3py.py:3010
def is_expr(a)
Definition: z3py.py:1143

◆ Complement()

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

Definition at line 10446 of file z3py.py.

10446 def Complement(re):
10447  """Create the complement regular expression."""
10448  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
10449 
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:10446

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

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

3864 def Concat(*args):
3865  """Create a Z3 bit-vector concatenation expression.
3866 
3867  >>> v = BitVecVal(1, 4)
3868  >>> Concat(v, v+1, v)
3869  Concat(Concat(1, 1 + 1), 1)
3870  >>> simplify(Concat(v, v+1, v))
3871  289
3872  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3873  121
3874  """
3875  args = _get_args(args)
3876  sz = len(args)
3877  if z3_debug():
3878  _z3_assert(sz >= 2, "At least two arguments expected.")
3879 
3880  ctx = None
3881  for a in args:
3882  if is_expr(a):
3883  ctx = a.ctx
3884  break
3885  if is_seq(args[0]) or isinstance(args[0], str):
3886  args = [_coerce_seq(s, ctx) for s in args]
3887  if z3_debug():
3888  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
3889  v = (Ast * sz)()
3890  for i in range(sz):
3891  v[i] = args[i].as_ast()
3892  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
3893 
3894  if is_re(args[0]):
3895  if z3_debug():
3896  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
3897  v = (Ast * sz)()
3898  for i in range(sz):
3899  v[i] = args[i].as_ast()
3900  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
3901 
3902  if z3_debug():
3903  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
3904  r = args[0]
3905  for i in range(sz - 1):
3906  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3907  return r
3908 
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:3515
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:10369
def z3_debug()
Definition: z3py.py:56
def is_expr(a)
Definition: z3py.py:1143
def is_bv(a)
Definition: z3py.py:3734
def Concat(args)
Definition: z3py.py:3864
def is_seq(a)
Definition: z3py.py:10113

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

Referenced by If().

8222 def Cond(p, t1, t2, ctx=None):
8223  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8224 
8225  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8226  """
8227  p = _to_probe(p, ctx)
8228  t1 = _to_tactic(t1, ctx)
8229  t2 = _to_tactic(t2, ctx)
8230  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8231 
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8222
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 1329 of file z3py.py.

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

1329 def Const(name, sort):
1330  """Create a constant of the given sort.
1331 
1332  >>> Const('x', IntSort())
1333  x
1334  """
1335  if z3_debug():
1336  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1337  ctx = sort.ctx
1338  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1339 
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:1329
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 1340 of file z3py.py.

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

1340 def Consts(names, sort):
1341  """Create several constants of the given sort.
1342 
1343  `names` is a string containing the names of all constants to be created.
1344  Blank spaces separate the names of different constants.
1345 
1346  >>> x, y, z = Consts('x y z', IntSort())
1347  >>> x + y + z
1348  x + y + z
1349  """
1350  if isinstance(names, str):
1351  names = names.split(" ")
1352  return [Const(name, sort) for name in names]
1353 
def Consts(names, sort)
Definition: z3py.py:1340
def Const(name, sort)
Definition: z3py.py:1329

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

10240 def Contains(a, b):
10241  """Check if 'a' contains 'b'
10242  >>> s1 = Contains("abc", "ab")
10243  >>> simplify(s1)
10244  True
10245  >>> s2 = Contains("abc", "bc")
10246  >>> simplify(s2)
10247  True
10248  >>> x, y, z = Strings('x y z')
10249  >>> s3 = Contains(Concat(x,y,z), y)
10250  >>> simplify(s3)
10251  True
10252  """
10253  ctx = _get_ctx2(a, b)
10254  a = _coerce_seq(a, ctx)
10255  b = _coerce_seq(b, ctx)
10256  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10257 
10258 
def Contains(a, b)
Definition: z3py.py:10240
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 4833 of file z3py.py.

Referenced by Datatype.create().

4833 def CreateDatatypes(*ds):
4834  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4835 
4836  In the following example we define a Tree-List using two mutually recursive datatypes.
4837 
4838  >>> TreeList = Datatype('TreeList')
4839  >>> Tree = Datatype('Tree')
4840  >>> # Tree has two constructors: leaf and node
4841  >>> Tree.declare('leaf', ('val', IntSort()))
4842  >>> # a node contains a list of trees
4843  >>> Tree.declare('node', ('children', TreeList))
4844  >>> TreeList.declare('nil')
4845  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4846  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4847  >>> Tree.val(Tree.leaf(10))
4848  val(leaf(10))
4849  >>> simplify(Tree.val(Tree.leaf(10)))
4850  10
4851  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4852  >>> n1
4853  node(cons(leaf(10), cons(leaf(20), nil)))
4854  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4855  >>> simplify(n2 == n1)
4856  False
4857  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4858  True
4859  """
4860  ds = _get_args(ds)
4861  if z3_debug():
4862  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4863  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
4864  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
4865  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
4866  ctx = ds[0].ctx
4867  num = len(ds)
4868  names = (Symbol * num)()
4869  out = (Sort * num)()
4870  clists = (ConstructorList * num)()
4871  to_delete = []
4872  for i in range(num):
4873  d = ds[i]
4874  names[i] = to_symbol(d.name, ctx)
4875  num_cs = len(d.constructors)
4876  cs = (Constructor * num_cs)()
4877  for j in range(num_cs):
4878  c = d.constructors[j]
4879  cname = to_symbol(c[0], ctx)
4880  rname = to_symbol(c[1], ctx)
4881  fs = c[2]
4882  num_fs = len(fs)
4883  fnames = (Symbol * num_fs)()
4884  sorts = (Sort * num_fs)()
4885  refs = (ctypes.c_uint * num_fs)()
4886  for k in range(num_fs):
4887  fname = fs[k][0]
4888  ftype = fs[k][1]
4889  fnames[k] = to_symbol(fname, ctx)
4890  if isinstance(ftype, Datatype):
4891  if z3_debug():
4892  _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4893  sorts[k] = None
4894  refs[k] = ds.index(ftype)
4895  else:
4896  if z3_debug():
4897  _z3_assert(is_sort(ftype), "Z3 sort expected")
4898  sorts[k] = ftype.ast
4899  refs[k] = 0
4900  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4901  to_delete.append(ScopedConstructor(cs[j], ctx))
4902  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4903  to_delete.append(ScopedConstructorList(clists[i], ctx))
4904  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4905  result = []
4906 
4907  for i in range(num):
4908  dref = DatatypeSortRef(out[i], ctx)
4909  num_cs = dref.num_constructors()
4910  for j in range(num_cs):
4911  cref = dref.constructor(j)
4912  cref_name = cref.name()
4913  cref_arity = cref.arity()
4914  if cref.arity() == 0:
4915  cref = cref()
4916  setattr(dref, cref_name, cref)
4917  rref = dref.recognizer(j)
4918  setattr(dref, "is_" + cref_name, rref)
4919  for k in range(cref_arity):
4920  aref = dref.accessor(j, k)
4921  setattr(dref, aref.name(), aref)
4922  result.append(dref)
4923  return tuple(result)
4924 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
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:4833
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 4488 of file z3py.py.

Referenced by is_default().

4488 def Default(a):
4489  """ Return a default value for array expression.
4490  >>> b = K(IntSort(), 1)
4491  >>> prove(Default(b) == 1)
4492  proved
4493  """
4494  if z3_debug():
4495  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4496  return a.default()
4497 
4498 
def is_array_sort(a)
Definition: z3py.py:4341
def Default(a)
Definition: z3py.py:4488
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 8152 of file z3py.py.

8152 def describe_probes():
8153  """Display a (tabular) description of all available probes in Z3."""
8154  if in_html_mode():
8155  even = True
8156  print('<table border="1" cellpadding="2" cellspacing="0">')
8157  for p in probes():
8158  if even:
8159  print('<tr style="background-color:#CFCFCF">')
8160  even = False
8161  else:
8162  print('<tr>')
8163  even = True
8164  print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
8165  print('</table>')
8166  else:
8167  for p in probes():
8168  print('%s : %s' % (p, probe_description(p)))
8169 
def probes(ctx=None)
Definition: z3py.py:8134
def probe_description(name, ctx=None)
Definition: z3py.py:8144
def describe_probes()
Definition: z3py.py:8152

◆ describe_tactics()

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

Definition at line 7961 of file z3py.py.

7961 def describe_tactics():
7962  """Display a (tabular) description of all available tactics in Z3."""
7963  if in_html_mode():
7964  even = True
7965  print('<table border="1" cellpadding="2" cellspacing="0">')
7966  for t in tactics():
7967  if even:
7968  print('<tr style="background-color:#CFCFCF">')
7969  even = False
7970  else:
7971  print('<tr>')
7972  even = True
7973  print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
7974  print('</table>')
7975  else:
7976  for t in tactics():
7977  print('%s : %s' % (t, tactic_description(t)))
7978 
def tactics(ctx=None)
Definition: z3py.py:7943
def tactic_description(name, ctx=None)
Definition: z3py.py:7953
def describe_tactics()
Definition: z3py.py:7961

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

5033 def DisjointSum(name, sorts, ctx=None):
5034  """Create a named tagged union sort base on a set of underlying sorts
5035  Example:
5036  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5037  """
5038  sum = Datatype(name, ctx)
5039  for i in range(len(sorts)):
5040  sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
5041  sum = sum.create()
5042  return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
5043 
5044 
def DisjointSum(name, sorts, ctx=None)
Definition: z3py.py:5033
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515

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

1298 def Distinct(*args):
1299  """Create a Z3 distinct expression.
1300 
1301  >>> x = Int('x')
1302  >>> y = Int('y')
1303  >>> Distinct(x, y)
1304  x != y
1305  >>> z = Int('z')
1306  >>> Distinct(x, y, z)
1307  Distinct(x, y, z)
1308  >>> simplify(Distinct(x, y, z))
1309  Distinct(x, y, z)
1310  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1311  And(Not(x == y), Not(x == z), Not(y == z))
1312  """
1313  args = _get_args(args)
1314  ctx = _ctx_from_ast_arg_list(args)
1315  if z3_debug():
1316  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
1317  args = _coerce_expr_list(args, ctx)
1318  _args, sz = _to_ast_array(args)
1319  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1320 
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:1298

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

10175 def Empty(s):
10176  """Create the empty sequence of the given sort
10177  >>> e = Empty(StringSort())
10178  >>> e2 = StringVal("")
10179  >>> print(e.eq(e2))
10180  True
10181  >>> e3 = Empty(SeqSort(IntSort()))
10182  >>> print(e3)
10183  Empty(Seq(Int))
10184  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10185  >>> print(e4)
10186  Empty(ReSort(Seq(Int)))
10187  """
10188  if isinstance(s, SeqSortRef):
10189  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10190  if isinstance(s, ReSortRef):
10191  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10192  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10193 
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:10175

◆ EmptySet()

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

Definition at line 4623 of file z3py.py.

4623 def EmptySet(s):
4624  """Create the empty set
4625  >>> EmptySet(IntSort())
4626  K(Int, False)
4627  """
4628  ctx = s.ctx
4629  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4630 
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
def EmptySet(s)
Definition: z3py.py:4623

◆ 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

◆ ensure_prop_closures()

def z3py.ensure_prop_closures ( )

Definition at line 10538 of file z3py.py.

10538 def ensure_prop_closures():
10539  global _prop_closures
10540  if _prop_closures is None:
10541  _prop_closures = PropClosures()
10542 
def ensure_prop_closures()
Definition: z3py.py:10538

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

Referenced by EnumSort< R >.getTesterDecl(), Context.MkEnumSort(), and EnumSort.TesterDecl().

5045 def EnumSort(name, values, ctx=None):
5046  """Return a new enumeration sort named `name` containing the given values.
5047 
5048  The result is a pair (sort, list of constants).
5049  Example:
5050  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5051  """
5052  if z3_debug():
5053  _z3_assert(isinstance(name, str), "Name must be a string")
5054  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
5055  _z3_assert(len(values) > 0, "At least one value expected")
5056  ctx = _get_ctx(ctx)
5057  num = len(values)
5058  _val_names = (Symbol * num)()
5059  for i in range(num):
5060  _val_names[i] = to_symbol(values[i])
5061  _values = (FuncDecl * num)()
5062  _testers = (FuncDecl * num)()
5063  name = to_symbol(name)
5064  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5065  V = []
5066  for i in range(num):
5067  V.append(FuncDeclRef(_values[i], ctx))
5068  V = [a() for a in V]
5069  return S, V
5070 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
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:5045
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 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 2090 of file z3py.py.

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

2090 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2091  """Create a Z3 exists formula.
2092 
2093  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2094 
2095 
2096  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2097  >>> x = Int('x')
2098  >>> y = Int('y')
2099  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2100  >>> q
2101  Exists([x, y], f(x, y) >= x)
2102  >>> is_quantifier(q)
2103  True
2104  >>> r = Tactic('nnf')(q).as_expr()
2105  >>> is_quantifier(r)
2106  False
2107  """
2108  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2109 
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2090

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

4573 def Ext(a, b):
4574  """Return extensionality index for one-dimensional arrays.
4575  >> a, b = Consts('a b', SetSort(IntSort()))
4576  >> Ext(a, b)
4577  Ext(a, b)
4578  """
4579  ctx = a.ctx
4580  if z3_debug():
4581  _z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays")
4582  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4583 
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:4341
def is_array(a)
Definition: z3py.py:4345
def z3_debug()
Definition: z3py.py:56
def Ext(a, b)
Definition: z3py.py:4573

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

3909 def Extract(high, low, a):
3910  """Create a Z3 bit-vector extraction expression, or create a string extraction expression.
3911 
3912  >>> x = BitVec('x', 8)
3913  >>> Extract(6, 2, x)
3914  Extract(6, 2, x)
3915  >>> Extract(6, 2, x).sort()
3916  BitVec(5)
3917  >>> simplify(Extract(StringVal("abcd"),2,1))
3918  "c"
3919  """
3920  if isinstance(high, str):
3921  high = StringVal(high)
3922  if is_seq(high):
3923  s = high
3924  offset, length = _coerce_exprs(low, a, s.ctx)
3925  return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
3926  if z3_debug():
3927  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3928  _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")
3929  _z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
3930  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
3931 
def Extract(high, low, a)
Definition: z3py.py:3909
def StringVal(s, ctx=None)
Definition: z3py.py:10139
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:3734
def is_seq(a)
Definition: z3py.py:10113

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

8185 def FailIf(p, ctx=None):
8186  """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8187 
8188  In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
8189 
8190  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8191  >>> x, y = Ints('x y')
8192  >>> g = Goal()
8193  >>> g.add(x > 0)
8194  >>> g.add(y > 0)
8195  >>> t(g)
8196  [[x > 0, y > 0]]
8197  >>> g.add(x == y + 1)
8198  >>> t(g)
8199  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8200  """
8201  p = _to_probe(p, ctx)
8202  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8203 
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:8185

◆ FiniteDomainSort()

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

Definition at line 7273 of file z3py.py.

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

7273 def FiniteDomainSort(name, sz, ctx=None):
7274  """Create a named finite domain sort of a given size sz"""
7275  if not isinstance(name, Symbol):
7276  name = to_symbol(name)
7277  ctx = _get_ctx(ctx)
7278  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7279 
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:7273

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

7341 def FiniteDomainVal(val, sort, ctx=None):
7342  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7343 
7344  >>> s = FiniteDomainSort('S', 256)
7345  >>> FiniteDomainVal(255, s)
7346  255
7347  >>> FiniteDomainVal('100', s)
7348  100
7349  """
7350  if z3_debug():
7351  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" )
7352  ctx = sort.ctx
7353  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7354 
def is_finite_domain_sort(s)
Definition: z3py.py:7280
def FiniteDomainVal(val, sort, ctx=None)
Definition: z3py.py:7341
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 8815 of file z3py.py.

8815 def Float128(ctx=None):
8816  """Floating-point 128-bit (quadruple) sort."""
8817  ctx = _get_ctx(ctx)
8818  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
8819 
def Float128(ctx=None)
Definition: z3py.py:8815
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 8785 of file z3py.py.

8785 def Float16(ctx=None):
8786  """Floating-point 16-bit (half) sort."""
8787  ctx = _get_ctx(ctx)
8788  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
8789 
def Float16(ctx=None)
Definition: z3py.py:8785
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 8795 of file z3py.py.

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

8795 def Float32(ctx=None):
8796  """Floating-point 32-bit (single) sort."""
8797  ctx = _get_ctx(ctx)
8798  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
8799 
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:8795

◆ Float64()

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

Definition at line 8805 of file z3py.py.

Referenced by fpFPToFP(), and fpToFP().

8805 def Float64(ctx=None):
8806  """Floating-point 64-bit (double) sort."""
8807  ctx = _get_ctx(ctx)
8808  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
8809 
def Float64(ctx=None)
Definition: z3py.py:8805
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 8810 of file z3py.py.

8810 def FloatDouble(ctx=None):
8811  """Floating-point 64-bit (double) sort."""
8812  ctx = _get_ctx(ctx)
8813  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
8814 
def FloatDouble(ctx=None)
Definition: z3py.py:8810
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 8790 of file z3py.py.

8790 def FloatHalf(ctx=None):
8791  """Floating-point 16-bit (half) sort."""
8792  ctx = _get_ctx(ctx)
8793  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
8794 
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:8790

◆ FloatQuadruple()

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

Definition at line 8820 of file z3py.py.

8820 def FloatQuadruple(ctx=None):
8821  """Floating-point 128-bit (quadruple) sort."""
8822  ctx = _get_ctx(ctx)
8823  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
8824 
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:8820

◆ FloatSingle()

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

Definition at line 8800 of file z3py.py.

8800 def FloatSingle(ctx=None):
8801  """Floating-point 32-bit (single) sort."""
8802  ctx = _get_ctx(ctx)
8803  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
8804 
def FloatSingle(ctx=None)
Definition: z3py.py:8800
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 2073 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().

2073 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2074  """Create a Z3 forall formula.
2075 
2076  The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2077 
2078  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2079  >>> x = Int('x')
2080  >>> y = Int('y')
2081  >>> ForAll([x, y], f(x, y) >= x)
2082  ForAll([x, y], f(x, y) >= x)
2083  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2084  ForAll([x, y], f(x, y) >= x)
2085  >>> ForAll([x, y], f(x, y) >= x, weight=10)
2086  ForAll([x, y], f(x, y) >= x)
2087  """
2088  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2089 
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2073

◆ 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 9400 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().

9400 def FP(name, fpsort, ctx=None):
9401  """Return a floating-point constant named `name`.
9402  `fpsort` is the floating-point sort.
9403  If `ctx=None`, then the global context is used.
9404 
9405  >>> x = FP('x', FPSort(8, 24))
9406  >>> is_fp(x)
9407  True
9408  >>> x.ebits()
9409  8
9410  >>> x.sort()
9411  FPSort(8, 24)
9412  >>> word = FPSort(8, 24)
9413  >>> x2 = FP('x', word)
9414  >>> eq(x, x2)
9415  True
9416  """
9417  if isinstance(fpsort, FPSortRef) and ctx is None:
9418  ctx = fpsort.ctx
9419  else:
9420  ctx = _get_ctx(ctx)
9421  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
9422 
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:9400

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

9441 def fpAbs(a, ctx=None):
9442  """Create a Z3 floating-point absolute value expression.
9443 
9444  >>> s = FPSort(8, 24)
9445  >>> rm = RNE()
9446  >>> x = FPVal(1.0, s)
9447  >>> fpAbs(x)
9448  fpAbs(1)
9449  >>> y = FPVal(-20.0, s)
9450  >>> y
9451  -1.25*(2**4)
9452  >>> fpAbs(y)
9453  fpAbs(-1.25*(2**4))
9454  >>> fpAbs(-1.25*(2**4))
9455  fpAbs(-1.25*(2**4))
9456  >>> fpAbs(x).sort()
9457  FPSort(8, 24)
9458  """
9459  ctx = _get_ctx(ctx)
9460  [a] = _coerce_fp_expr_list([a], ctx)
9461  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
9462 
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:9441

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

Referenced by FPs().

9523 def fpAdd(rm, a, b, ctx=None):
9524  """Create a Z3 floating-point addition expression.
9525 
9526  >>> s = FPSort(8, 24)
9527  >>> rm = RNE()
9528  >>> x = FP('x', s)
9529  >>> y = FP('y', s)
9530  >>> fpAdd(rm, x, y)
9531  fpAdd(RNE(), x, y)
9532  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
9533  x + y
9534  >>> fpAdd(rm, x, y).sort()
9535  FPSort(8, 24)
9536  """
9537  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
9538 
def fpAdd(rm, a, b, ctx=None)
Definition: z3py.py:9523

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

9819 def fpBVToFP(v, sort, ctx=None):
9820  """Create a Z3 floating-point conversion expression that represents the
9821  conversion from a bit-vector term to a floating-point term.
9822 
9823  >>> x_bv = BitVecVal(0x3F800000, 32)
9824  >>> x_fp = fpBVToFP(x_bv, Float32())
9825  >>> x_fp
9826  fpToFP(1065353216)
9827  >>> simplify(x_fp)
9828  1
9829  """
9830  _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
9831  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
9832  ctx = _get_ctx(ctx)
9833  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
9834 
def fpBVToFP(v, sort, ctx=None)
Definition: z3py.py:9819
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:8829
def is_bv(a)
Definition: z3py.py:3734

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

9567 def fpDiv(rm, a, b, ctx=None):
9568  """Create a Z3 floating-point division expression.
9569 
9570  >>> s = FPSort(8, 24)
9571  >>> rm = RNE()
9572  >>> x = FP('x', s)
9573  >>> y = FP('y', s)
9574  >>> fpDiv(rm, x, y)
9575  fpDiv(RNE(), x, y)
9576  >>> fpDiv(rm, x, y).sort()
9577  FPSort(8, 24)
9578  """
9579  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
9580 
def fpDiv(rm, a, b, ctx=None)
Definition: z3py.py:9567

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

Referenced by fpFP(), and fpNEQ().

9731 def fpEQ(a, b, ctx=None):
9732  """Create the Z3 floating-point expression `fpEQ(other, self)`.
9733 
9734  >>> x, y = FPs('x y', FPSort(8, 24))
9735  >>> fpEQ(x, y)
9736  fpEQ(x, y)
9737  >>> fpEQ(x, y).sexpr()
9738  '(fp.eq x y)'
9739  """
9740  return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
9741 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:9731

◆ fpFMA()

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

Definition at line 9622 of file z3py.py.

9622 def fpFMA(rm, a, b, c, ctx=None):
9623  """Create a Z3 floating-point fused multiply-add expression.
9624  """
9625  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
9626 
def fpFMA(rm, a, b, c, ctx=None)
Definition: z3py.py:9622

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

9753 def fpFP(sgn, exp, sig, ctx=None):
9754  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
9755 
9756  >>> s = FPSort(8, 24)
9757  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
9758  >>> print(x)
9759  fpFP(1, 127, 4194304)
9760  >>> xv = FPVal(-1.5, s)
9761  >>> print(xv)
9762  -1.5
9763  >>> slvr = Solver()
9764  >>> slvr.add(fpEQ(x, xv))
9765  >>> slvr.check()
9766  sat
9767  >>> xv = FPVal(+1.5, s)
9768  >>> print(xv)
9769  1.5
9770  >>> slvr = Solver()
9771  >>> slvr.add(fpEQ(x, xv))
9772  >>> slvr.check()
9773  unsat
9774  """
9775  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
9776  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
9777  ctx = _get_ctx(ctx)
9778  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
9779  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
9780 
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:9753
def is_bv(a)
Definition: z3py.py:3734

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

9835 def fpFPToFP(rm, v, sort, ctx=None):
9836  """Create a Z3 floating-point conversion expression that represents the
9837  conversion from a floating-point term to a floating-point term of different precision.
9838 
9839  >>> x_sgl = FPVal(1.0, Float32())
9840  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
9841  >>> x_dbl
9842  fpToFP(RNE(), 1)
9843  >>> simplify(x_dbl)
9844  1
9845  >>> x_dbl.sort()
9846  FPSort(11, 53)
9847  """
9848  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9849  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
9850  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9851  ctx = _get_ctx(ctx)
9852  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9853 
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:8829
def fpFPToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9835
def is_fprm(a)
Definition: z3py.py:9076
def is_fp(a)
Definition: z3py.py:9212

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

9720 def fpGEQ(a, b, ctx=None):
9721  """Create the Z3 floating-point expression `other >= self`.
9722 
9723  >>> x, y = FPs('x y', FPSort(8, 24))
9724  >>> fpGEQ(x, y)
9725  x >= y
9726  >>> (x >= y).sexpr()
9727  '(fp.geq x y)'
9728  """
9729  return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
9730 
def fpGEQ(a, b, ctx=None)
Definition: z3py.py:9720

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

9709 def fpGT(a, b, ctx=None):
9710  """Create the Z3 floating-point expression `other > self`.
9711 
9712  >>> x, y = FPs('x y', FPSort(8, 24))
9713  >>> fpGT(x, y)
9714  x > y
9715  >>> (x > y).sexpr()
9716  '(fp.gt x y)'
9717  """
9718  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
9719 
def fpGT(a, b, ctx=None)
Definition: z3py.py:9709

◆ fpInfinity()

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

Definition at line 9334 of file z3py.py.

9334 def fpInfinity(s, negative):
9335  """Create a Z3 floating-point +oo or -oo term."""
9336  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9337  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9338  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
9339 
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:9334

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

9648 def fpIsInf(a, ctx=None):
9649  """Create a Z3 floating-point isInfinite expression.
9650 
9651  >>> s = FPSort(8, 24)
9652  >>> x = FP('x', s)
9653  >>> fpIsInf(x)
9654  fpIsInf(x)
9655  """
9656  return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
9657 
def fpIsInf(a, ctx=None)
Definition: z3py.py:9648

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

9637 def fpIsNaN(a, ctx=None):
9638  """Create a Z3 floating-point isNaN expression.
9639 
9640  >>> s = FPSort(8, 24)
9641  >>> x = FP('x', s)
9642  >>> y = FP('y', s)
9643  >>> fpIsNaN(x)
9644  fpIsNaN(x)
9645  """
9646  return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
9647 
def fpIsNaN(a, ctx=None)
Definition: z3py.py:9637

◆ fpIsNegative()

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

Definition at line 9673 of file z3py.py.

9673 def fpIsNegative(a, ctx=None):
9674  """Create a Z3 floating-point isNegative expression.
9675  """
9676  return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
9677 
def fpIsNegative(a, ctx=None)
Definition: z3py.py:9673

◆ fpIsNormal()

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

Definition at line 9663 of file z3py.py.

9663 def fpIsNormal(a, ctx=None):
9664  """Create a Z3 floating-point isNormal expression.
9665  """
9666  return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
9667 
def fpIsNormal(a, ctx=None)
Definition: z3py.py:9663

◆ fpIsPositive()

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

Definition at line 9678 of file z3py.py.

9678 def fpIsPositive(a, ctx=None):
9679  """Create a Z3 floating-point isPositive expression.
9680  """
9681  return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
9682 
def fpIsPositive(a, ctx=None)
Definition: z3py.py:9678

◆ fpIsSubnormal()

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

Definition at line 9668 of file z3py.py.

9668 def fpIsSubnormal(a, ctx=None):
9669  """Create a Z3 floating-point isSubnormal expression.
9670  """
9671  return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
9672 
def fpIsSubnormal(a, ctx=None)
Definition: z3py.py:9668

◆ fpIsZero()

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

Definition at line 9658 of file z3py.py.

9658 def fpIsZero(a, ctx=None):
9659  """Create a Z3 floating-point isZero expression.
9660  """
9661  return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
9662 
def fpIsZero(a, ctx=None)
Definition: z3py.py:9658

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

9698 def fpLEQ(a, b, ctx=None):
9699  """Create the Z3 floating-point expression `other <= self`.
9700 
9701  >>> x, y = FPs('x y', FPSort(8, 24))
9702  >>> fpLEQ(x, y)
9703  x <= y
9704  >>> (x <= y).sexpr()
9705  '(fp.leq x y)'
9706  """
9707  return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
9708 
def fpLEQ(a, b, ctx=None)
Definition: z3py.py:9698

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

9687 def fpLT(a, b, ctx=None):
9688  """Create the Z3 floating-point expression `other < self`.
9689 
9690  >>> x, y = FPs('x y', FPSort(8, 24))
9691  >>> fpLT(x, y)
9692  x < y
9693  >>> (x < y).sexpr()
9694  '(fp.lt x y)'
9695  """
9696  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
9697 
def fpLT(a, b, ctx=None)
Definition: z3py.py:9687

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

9608 def fpMax(a, b, ctx=None):
9609  """Create a Z3 floating-point maximum expression.
9610 
9611  >>> s = FPSort(8, 24)
9612  >>> rm = RNE()
9613  >>> x = FP('x', s)
9614  >>> y = FP('y', s)
9615  >>> fpMax(x, y)
9616  fpMax(x, y)
9617  >>> fpMax(x, y).sort()
9618  FPSort(8, 24)
9619  """
9620  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
9621 
def fpMax(a, b, ctx=None)
Definition: z3py.py:9608

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

9594 def fpMin(a, b, ctx=None):
9595  """Create a Z3 floating-point minimum expression.
9596 
9597  >>> s = FPSort(8, 24)
9598  >>> rm = RNE()
9599  >>> x = FP('x', s)
9600  >>> y = FP('y', s)
9601  >>> fpMin(x, y)
9602  fpMin(x, y)
9603  >>> fpMin(x, y).sort()
9604  FPSort(8, 24)
9605  """
9606  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
9607 
def fpMin(a, b, ctx=None)
Definition: z3py.py:9594

◆ fpMinusInfinity()

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

Definition at line 9329 of file z3py.py.

9329 def fpMinusInfinity(s):
9330  """Create a Z3 floating-point -oo term."""
9331  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9332  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9333 
def fpMinusInfinity(s)
Definition: z3py.py:9329
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 9345 of file z3py.py.

9345 def fpMinusZero(s):
9346  """Create a Z3 floating-point -0.0 term."""
9347  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9348  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
9349 
def fpMinusZero(s)
Definition: z3py.py:9345
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 9553 of file z3py.py.

Referenced by FPs().

9553 def fpMul(rm, a, b, ctx=None):
9554  """Create a Z3 floating-point multiplication expression.
9555 
9556  >>> s = FPSort(8, 24)
9557  >>> rm = RNE()
9558  >>> x = FP('x', s)
9559  >>> y = FP('y', s)
9560  >>> fpMul(rm, x, y)
9561  fpMul(RNE(), x, y)
9562  >>> fpMul(rm, x, y).sort()
9563  FPSort(8, 24)
9564  """
9565  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
9566 
def fpMul(rm, a, b, ctx=None)
Definition: z3py.py:9553

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

9297 def fpNaN(s):
9298  """Create a Z3 floating-point NaN term.
9299 
9300  >>> s = FPSort(8, 24)
9301  >>> set_fpa_pretty(True)
9302  >>> fpNaN(s)
9303  NaN
9304  >>> pb = get_fpa_pretty()
9305  >>> set_fpa_pretty(False)
9306  >>> fpNaN(s)
9307  fpNaN(FPSort(8, 24))
9308  >>> set_fpa_pretty(pb)
9309  """
9310  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9311  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9312 
def fpNaN(s)
Definition: z3py.py:9297
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 9463 of file z3py.py.

9463 def fpNeg(a, ctx=None):
9464  """Create a Z3 floating-point addition expression.
9465 
9466  >>> s = FPSort(8, 24)
9467  >>> rm = RNE()
9468  >>> x = FP('x', s)
9469  >>> fpNeg(x)
9470  -x
9471  >>> fpNeg(x).sort()
9472  FPSort(8, 24)
9473  """
9474  ctx = _get_ctx(ctx)
9475  [a] = _coerce_fp_expr_list([a], ctx)
9476  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
9477 
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:9463

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

9742 def fpNEQ(a, b, ctx=None):
9743  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
9744 
9745  >>> x, y = FPs('x y', FPSort(8, 24))
9746  >>> fpNEQ(x, y)
9747  Not(fpEQ(x, y))
9748  >>> (x != y).sexpr()
9749  '(distinct x y)'
9750  """
9751  return Not(fpEQ(a, b, ctx))
9752 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:9731
def Not(a, ctx=None)
Definition: z3py.py:1677
def fpNEQ(a, b, ctx=None)
Definition: z3py.py:9742

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

9313 def fpPlusInfinity(s):
9314  """Create a Z3 floating-point +oo term.
9315 
9316  >>> s = FPSort(8, 24)
9317  >>> pb = get_fpa_pretty()
9318  >>> set_fpa_pretty(True)
9319  >>> fpPlusInfinity(s)
9320  +oo
9321  >>> set_fpa_pretty(False)
9322  >>> fpPlusInfinity(s)
9323  fpPlusInfinity(FPSort(8, 24))
9324  >>> set_fpa_pretty(pb)
9325  """
9326  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9327  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9328 
def fpPlusInfinity(s)
Definition: z3py.py:9313
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 9340 of file z3py.py.

9340 def fpPlusZero(s):
9341  """Create a Z3 floating-point +0.0 term."""
9342  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9343  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
9344 
def fpPlusZero(s)
Definition: z3py.py:9340
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 9854 of file z3py.py.

9854 def fpRealToFP(rm, v, sort, ctx=None):
9855  """Create a Z3 floating-point conversion expression that represents the
9856  conversion from a real term to a floating-point term.
9857 
9858  >>> x_r = RealVal(1.5)
9859  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
9860  >>> x_fp
9861  fpToFP(RNE(), 3/2)
9862  >>> simplify(x_fp)
9863  1.5
9864  """
9865  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9866  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
9867  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9868  ctx = _get_ctx(ctx)
9869  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9870 
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:2544
def is_fp_sort(s)
Definition: z3py.py:8829
def fpRealToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9854
def is_fprm(a)
Definition: z3py.py:9076

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

9581 def fpRem(a, b, ctx=None):
9582  """Create a Z3 floating-point remainder expression.
9583 
9584  >>> s = FPSort(8, 24)
9585  >>> x = FP('x', s)
9586  >>> y = FP('y', s)
9587  >>> fpRem(x, y)
9588  fpRem(x, y)
9589  >>> fpRem(x, y).sort()
9590  FPSort(8, 24)
9591  """
9592  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
9593 
def fpRem(a, b, ctx=None)
Definition: z3py.py:9581

◆ fpRoundToIntegral()

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

Definition at line 9632 of file z3py.py.

9632 def fpRoundToIntegral(rm, a, ctx=None):
9633  """Create a Z3 floating-point roundToIntegral expression.
9634  """
9635  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
9636 
def fpRoundToIntegral(rm, a, ctx=None)
Definition: z3py.py:9632

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

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

9423 def FPs(names, fpsort, ctx=None):
9424  """Return an array of floating-point constants.
9425 
9426  >>> x, y, z = FPs('x y z', FPSort(8, 24))
9427  >>> x.sort()
9428  FPSort(8, 24)
9429  >>> x.sbits()
9430  24
9431  >>> x.ebits()
9432  8
9433  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9434  fpMul(RNE(), fpAdd(RNE(), x, y), z)
9435  """
9436  ctx = _get_ctx(ctx)
9437  if isinstance(names, str):
9438  names = names.split(" ")
9439  return [FP(name, fpsort, ctx) for name in names]
9440 
def FPs(names, fpsort, ctx=None)
Definition: z3py.py:9423
def FP(name, fpsort, ctx=None)
Definition: z3py.py:9400

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

9871 def fpSignedToFP(rm, v, sort, ctx=None):
9872  """Create a Z3 floating-point conversion expression that represents the
9873  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
9874 
9875  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9876  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
9877  >>> x_fp
9878  fpToFP(RNE(), 4294967291)
9879  >>> simplify(x_fp)
9880  -1.25*(2**2)
9881  """
9882  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9883  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
9884  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9885  ctx = _get_ctx(ctx)
9886  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9887 
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:9871
def is_fp_sort(s)
Definition: z3py.py:8829
def is_bv(a)
Definition: z3py.py:3734
def is_fprm(a)
Definition: z3py.py:9076

◆ 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 9239 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().

9239 def FPSort(ebits, sbits, ctx=None):
9240  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9241 
9242  >>> Single = FPSort(8, 24)
9243  >>> Double = FPSort(11, 53)
9244  >>> Single
9245  FPSort(8, 24)
9246  >>> x = Const('x', Single)
9247  >>> eq(x, FP('x', FPSort(8, 24)))
9248  True
9249  """
9250  ctx = _get_ctx(ctx)
9251  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9252 
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:9239

◆ fpSqrt()

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

Definition at line 9627 of file z3py.py.

9627 def fpSqrt(rm, a, ctx=None):
9628  """Create a Z3 floating-point square root expression.
9629  """
9630  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
9631 
def fpSqrt(rm, a, ctx=None)
Definition: z3py.py:9627

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

9539 def fpSub(rm, a, b, ctx=None):
9540  """Create a Z3 floating-point subtraction expression.
9541 
9542  >>> s = FPSort(8, 24)
9543  >>> rm = RNE()
9544  >>> x = FP('x', s)
9545  >>> y = FP('y', s)
9546  >>> fpSub(rm, x, y)
9547  fpSub(RNE(), x, y)
9548  >>> fpSub(rm, x, y).sort()
9549  FPSort(8, 24)
9550  """
9551  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
9552 
def fpSub(rm, a, b, ctx=None)
Definition: z3py.py:9539

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

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

9781 def fpToFP(a1, a2=None, a3=None, ctx=None):
9782  """Create a Z3 floating-point conversion expression from other term sorts
9783  to floating-point.
9784 
9785  From a bit-vector term in IEEE 754-2008 format:
9786  >>> x = FPVal(1.0, Float32())
9787  >>> x_bv = fpToIEEEBV(x)
9788  >>> simplify(fpToFP(x_bv, Float32()))
9789  1
9790 
9791  From a floating-point term with different precision:
9792  >>> x = FPVal(1.0, Float32())
9793  >>> x_db = fpToFP(RNE(), x, Float64())
9794  >>> x_db.sort()
9795  FPSort(11, 53)
9796 
9797  From a real term:
9798  >>> x_r = RealVal(1.5)
9799  >>> simplify(fpToFP(RNE(), x_r, Float32()))
9800  1.5
9801 
9802  From a signed bit-vector term:
9803  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9804  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
9805  -1.25*(2**2)
9806  """
9807  ctx = _get_ctx(ctx)
9808  if is_bv(a1) and is_fp_sort(a2):
9809  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
9810  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
9811  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9812  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
9813  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9814  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
9815  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9816  else:
9817  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
9818 
def fpToFP(a1, a2=None, a3=None, ctx=None)
Definition: z3py.py:9781
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:2544
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:8829
def is_bv(a)
Definition: z3py.py:3734
def is_fprm(a)
Definition: z3py.py:9076
def is_fp(a)
Definition: z3py.py:9212

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

Referenced by fpUnsignedToFP().

9905 def fpToFPUnsigned(rm, x, s, ctx=None):
9906  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
9907  if z3_debug():
9908  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9909  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
9910  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
9911  ctx = _get_ctx(ctx)
9912  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
9913 
def fpToFPUnsigned(rm, x, s, ctx=None)
Definition: z3py.py:9905
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:8829
def is_bv(a)
Definition: z3py.py:3734
def is_fprm(a)
Definition: z3py.py:9076

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

Referenced by fpToFP().

9975 def fpToIEEEBV(x, ctx=None):
9976  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
9977 
9978  The size of the resulting bit-vector is automatically determined.
9979 
9980  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9981  knows only one NaN and it will always produce the same bit-vector representation of
9982  that NaN.
9983 
9984  >>> x = FP('x', FPSort(8, 24))
9985  >>> y = fpToIEEEBV(x)
9986  >>> print(is_fp(x))
9987  True
9988  >>> print(is_bv(y))
9989  True
9990  >>> print(is_fp(y))
9991  False
9992  >>> print(is_bv(x))
9993  False
9994  """
9995  if z3_debug():
9996  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
9997  ctx = _get_ctx(ctx)
9998  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
9999 
10000 
10001 
def fpToIEEEBV(x, ctx=None)
Definition: z3py.py:9975
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:9212

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

9956 def fpToReal(x, ctx=None):
9957  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
9958 
9959  >>> x = FP('x', FPSort(8, 24))
9960  >>> y = fpToReal(x)
9961  >>> print(is_fp(x))
9962  True
9963  >>> print(is_real(y))
9964  True
9965  >>> print(is_fp(y))
9966  False
9967  >>> print(is_real(x))
9968  False
9969  """
9970  if z3_debug():
9971  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
9972  ctx = _get_ctx(ctx)
9973  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
9974 
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:9956
def is_fp(a)
Definition: z3py.py:9212

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

9914 def fpToSBV(rm, x, s, ctx=None):
9915  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
9916 
9917  >>> x = FP('x', FPSort(8, 24))
9918  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
9919  >>> print(is_fp(x))
9920  True
9921  >>> print(is_bv(y))
9922  True
9923  >>> print(is_fp(y))
9924  False
9925  >>> print(is_bv(x))
9926  False
9927  """
9928  if z3_debug():
9929  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9930  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
9931  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
9932  ctx = _get_ctx(ctx)
9933  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
9934 
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:9914
def z3_debug()
Definition: z3py.py:56
def is_bv_sort(s)
Definition: z3py.py:3269
def is_fprm(a)
Definition: z3py.py:9076
def is_fp(a)
Definition: z3py.py:9212

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

9935 def fpToUBV(rm, x, s, ctx=None):
9936  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
9937 
9938  >>> x = FP('x', FPSort(8, 24))
9939  >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
9940  >>> print(is_fp(x))
9941  True
9942  >>> print(is_bv(y))
9943  True
9944  >>> print(is_fp(y))
9945  False
9946  >>> print(is_bv(x))
9947  False
9948  """
9949  if z3_debug():
9950  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9951  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
9952  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
9953  ctx = _get_ctx(ctx)
9954  return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
9955 
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:9935
def z3_debug()
Definition: z3py.py:56
def is_bv_sort(s)
Definition: z3py.py:3269
def is_fprm(a)
Definition: z3py.py:9076
def is_fp(a)
Definition: z3py.py:9212

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

9888 def fpUnsignedToFP(rm, v, sort, ctx=None):
9889  """Create a Z3 floating-point conversion expression that represents the
9890  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9891 
9892  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9893  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
9894  >>> x_fp
9895  fpToFPUnsigned(RNE(), 4294967291)
9896  >>> simplify(x_fp)
9897  1*(2**32)
9898  """
9899  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9900  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
9901  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9902  ctx = _get_ctx(ctx)
9903  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9904 
def fpUnsignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9888
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:8829
def is_bv(a)
Definition: z3py.py:3734
def is_fprm(a)
Definition: z3py.py:9076

◆ 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 9356 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().

9356 def FPVal(sig, exp=None, fps=None, ctx=None):
9357  """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
9358 
9359  >>> v = FPVal(20.0, FPSort(8, 24))
9360  >>> v
9361  1.25*(2**4)
9362  >>> print("0x%.8x" % v.exponent_as_long(False))
9363  0x00000004
9364  >>> v = FPVal(2.25, FPSort(8, 24))
9365  >>> v
9366  1.125*(2**1)
9367  >>> v = FPVal(-2.25, FPSort(8, 24))
9368  >>> v
9369  -1.125*(2**1)
9370  >>> FPVal(-0.0, FPSort(8, 24))
9371  -0.0
9372  >>> FPVal(0.0, FPSort(8, 24))
9373  +0.0
9374  >>> FPVal(+0.0, FPSort(8, 24))
9375  +0.0
9376  """
9377  ctx = _get_ctx(ctx)
9378  if is_fp_sort(exp):
9379  fps = exp
9380  exp = None
9381  elif fps is None:
9382  fps = _dflt_fps(ctx)
9383  _z3_assert(is_fp_sort(fps), "sort mismatch")
9384  if exp is None:
9385  exp = 0
9386  val = _to_float_str(sig)
9387  if val == "NaN" or val == "nan":
9388  return fpNaN(fps)
9389  elif val == "-0.0":
9390  return fpMinusZero(fps)
9391  elif val == "0.0" or val == "+0.0":
9392  return fpPlusZero(fps)
9393  elif val == "+oo" or val == "+inf" or val == "+Inf":
9394  return fpPlusInfinity(fps)
9395  elif val == "-oo" or val == "-inf" or val == "-Inf":
9396  return fpMinusInfinity(fps)
9397  else:
9398  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
9399 
def FPVal(sig, exp=None, fps=None, ctx=None)
Definition: z3py.py:9356
def fpMinusInfinity(s)
Definition: z3py.py:9329
def fpMinusZero(s)
Definition: z3py.py:9345
def fpPlusZero(s)
Definition: z3py.py:9340
def fpPlusInfinity(s)
Definition: z3py.py:9313
def fpNaN(s)
Definition: z3py.py:9297
def is_fp_sort(s)
Definition: z3py.py:8829
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 9350 of file z3py.py.

9350 def fpZero(s, negative):
9351  """Create a Z3 floating-point +0.0 or -0.0 term."""
9352  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9353  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9354  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
9355 
def fpZero(s, negative)
Definition: z3py.py:9350
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 1636 of file z3py.py.

1636 def FreshBool(prefix='b', ctx=None):
1637  """Return a fresh Boolean constant in the given context using the given prefix.
1638 
1639  If `ctx=None`, then the global context is used.
1640 
1641  >>> b1 = FreshBool()
1642  >>> b2 = FreshBool()
1643  >>> eq(b1, b2)
1644  False
1645  """
1646  ctx = _get_ctx(ctx)
1647  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1648 
def FreshBool(prefix='b', ctx=None)
Definition: z3py.py:1636
def BoolSort(ctx=None)
Definition: z3py.py:1561
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 1354 of file z3py.py.

1354 def FreshConst(sort, prefix='c'):
1355  """Create a fresh constant of a specified sort"""
1356  ctx = _get_ctx(sort.ctx)
1357  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1358 
def FreshConst(sort, prefix='c')
Definition: z3py.py:1354
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshFunction()

def z3py.FreshFunction (   sig)
Create a new fresh Z3 uninterpreted function with the given sorts.

Definition at line 821 of file z3py.py.

821 def FreshFunction(*sig):
822  """Create a new fresh Z3 uninterpreted function with the given sorts.
823  """
824  sig = _get_args(sig)
825  if z3_debug():
826  _z3_assert(len(sig) > 0, "At least two arguments expected")
827  arity = len(sig) - 1
828  rng = sig[arity]
829  if z3_debug():
830  _z3_assert(is_sort(rng), "Z3 sort expected")
831  dom = (z3.Sort * arity)()
832  for i in range(arity):
833  if z3_debug():
834  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
835  dom[i] = sig[i].ast
836  ctx = rng.ctx
837  return FuncDeclRef(Z3_mk_fresh_func_decl(ctx.ref(), 'f', arity, dom, rng.ast), ctx)
838 
839 
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
def is_sort(s)
Definition: z3py.py:596
def z3_debug()
Definition: z3py.py:56
def FreshFunction(sig)
Definition: z3py.py:821

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

3091 def FreshInt(prefix='x', ctx=None):
3092  """Return a fresh integer constant in the given context using the given prefix.
3093 
3094  >>> x = FreshInt()
3095  >>> y = FreshInt()
3096  >>> eq(x, y)
3097  False
3098  >>> x.sort()
3099  Int
3100  """
3101  ctx = _get_ctx(ctx)
3102  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3103 
def IntSort(ctx=None)
Definition: z3py.py:2952
def FreshInt(prefix='x', ctx=None)
Definition: z3py.py:3091
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 3144 of file z3py.py.

3144 def FreshReal(prefix='b', ctx=None):
3145  """Return a fresh real constant in the given context using the given prefix.
3146 
3147  >>> x = FreshReal()
3148  >>> y = FreshReal()
3149  >>> eq(x, y)
3150  False
3151  >>> x.sort()
3152  Real
3153  """
3154  ctx = _get_ctx(ctx)
3155  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3156 
def FreshReal(prefix='b', ctx=None)
Definition: z3py.py:3144
def RealSort(ctx=None)
Definition: z3py.py:2968
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 10194 of file z3py.py.

10194 def Full(s):
10195  """Create the regular expression that accepts the universal language
10196  >>> e = Full(ReSort(SeqSort(IntSort())))
10197  >>> print(e)
10198  Full(ReSort(Seq(Int)))
10199  >>> e1 = Full(ReSort(StringSort()))
10200  >>> print(e1)
10201  Full(ReSort(String))
10202  """
10203  if isinstance(s, ReSortRef):
10204  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10205  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10206 
10207 
def Full(s)
Definition: z3py.py:10194
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 4631 of file z3py.py.

4631 def FullSet(s):
4632  """Create the full set
4633  >>> FullSet(IntSort())
4634  K(Int, True)
4635  """
4636  ctx = s.ctx
4637  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4638 
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
def FullSet(s)
Definition: z3py.py:4631

◆ 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:3515
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 6295 of file z3py.py.

6295 def get_as_array_func(n):
6296  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6297  if z3_debug():
6298  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6299  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6300 
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:6295
def z3_debug()
Definition: z3py.py:56
def is_as_array(n)
Definition: z3py.py:6291

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

8709 def get_default_fp_sort(ctx=None):
8710  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
8711 
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9239
def get_default_fp_sort(ctx=None)
Definition: z3py.py:8709

◆ get_default_rounding_mode()

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

Definition at line 8682 of file z3py.py.

8682 def get_default_rounding_mode(ctx=None):
8683  """Retrieves the global default rounding mode."""
8684  global _dflt_rounding_mode
8685  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
8686  return RTZ(ctx)
8687  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
8688  return RTN(ctx)
8689  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
8690  return RTP(ctx)
8691  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
8692  return RNE(ctx)
8693  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
8694  return RNA(ctx)
8695 
def RTN(ctx=None)
Definition: z3py.py:9064
def RTZ(ctx=None)
Definition: z3py.py:9072
def RTP(ctx=None)
Definition: z3py.py:9056
def RNA(ctx=None)
Definition: z3py.py:9048
def get_default_rounding_mode(ctx=None)
Definition: z3py.py:8682
def RNE(ctx=None)
Definition: z3py.py:9040

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

4405 def get_map_func(a):
4406  """Return the function declaration associated with a Z3 map array expression.
4407 
4408  >>> f = Function('f', IntSort(), IntSort())
4409  >>> b = Array('b', IntSort(), IntSort())
4410  >>> a = Map(f, b)
4411  >>> eq(f, get_map_func(a))
4412  True
4413  >>> get_map_func(a)
4414  f
4415  >>> get_map_func(a)(0)
4416  f(0)
4417  """
4418  if z3_debug():
4419  _z3_assert(is_map(a), "Z3 array map expression expected.")
4420  return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
4421 
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:4382
def get_map_func(a)
Definition: z3py.py:4405
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 1232 of file z3py.py.

1232 def get_var_index(a):
1233  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1234 
1235  >>> x = Int('x')
1236  >>> y = Int('y')
1237  >>> is_var(x)
1238  False
1239  >>> is_const(x)
1240  True
1241  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1242  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1243  >>> q = ForAll([x, y], f(x, y) == x + y)
1244  >>> q.body()
1245  f(Var(1), Var(0)) == Var(1) + Var(0)
1246  >>> b = q.body()
1247  >>> b.arg(0)
1248  f(Var(1), Var(0))
1249  >>> v1 = b.arg(0).arg(0)
1250  >>> v2 = b.arg(0).arg(1)
1251  >>> v1
1252  Var(1)
1253  >>> v2
1254  Var(0)
1255  >>> get_var_index(v1)
1256  1
1257  >>> get_var_index(v2)
1258  0
1259  """
1260  if z3_debug():
1261  _z3_assert(is_var(a), "Z3 bound variable expected")
1262  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1263 
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:1232
def is_var(a)
Definition: z3py.py:1208

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

8262 def help_simplify():
8263  """Return a string describing all options available for Z3 `simplify` procedure."""
8264  print(Z3_simplify_get_help(main_ctx().ref()))
8265 
def main_ctx()
Definition: z3py.py:211
def help_simplify()
Definition: z3py.py:8262
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 1276 of file z3py.py.

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

1276 def If(a, b, c, ctx=None):
1277  """Create a Z3 if-then-else expression.
1278 
1279  >>> x = Int('x')
1280  >>> y = Int('y')
1281  >>> max = If(x > y, x, y)
1282  >>> max
1283  If(x > y, x, y)
1284  >>> simplify(max)
1285  If(x <= y, y, x)
1286  """
1287  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1288  return Cond(a, b, c, ctx)
1289  else:
1290  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1291  s = BoolSort(ctx)
1292  a = s.cast(a)
1293  b, c = _coerce_exprs(b, c, ctx)
1294  if z3_debug():
1295  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1296  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1297 
def If(a, b, c, ctx=None)
Definition: z3py.py:1276
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8222
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:1561

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

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

1649 def Implies(a, b, ctx=None):
1650  """Create a Z3 implies expression.
1651 
1652  >>> p, q = Bools('p q')
1653  >>> Implies(p, q)
1654  Implies(p, q)
1655  """
1656  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1657  s = BoolSort(ctx)
1658  a = s.cast(a)
1659  b = s.cast(b)
1660  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1661 
def Implies(a, b, ctx=None)
Definition: z3py.py:1649
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:1561

◆ IndexOf() [1/2]

def z3py.IndexOf (   s,
  substr 
)

Definition at line 10273 of file z3py.py.

Referenced by IndexOf().

10273 def IndexOf(s, substr):
10274  return IndexOf(s, substr, IntVal(0))
10275 
def IntVal(val, ctx=None)
Definition: z3py.py:2999
def IndexOf(s, substr)
Definition: z3py.py:10273

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

10276 def IndexOf(s, substr, offset):
10277  """Retrieve the index of substring within a string starting at a specified offset.
10278  >>> simplify(IndexOf("abcabc", "bc", 0))
10279  1
10280  >>> simplify(IndexOf("abcabc", "bc", 2))
10281  4
10282  """
10283  ctx = None
10284  if is_expr(offset):
10285  ctx = offset.ctx
10286  ctx = _get_ctx2(s, substr, ctx)
10287  s = _coerce_seq(s, ctx)
10288  substr = _coerce_seq(substr, ctx)
10289  if _is_int(offset):
10290  offset = IntVal(offset, ctx)
10291  return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
10292 
def IntVal(val, ctx=None)
Definition: z3py.py:2999
def IndexOf(s, substr)
Definition: z3py.py:10273
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:1143

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

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

10373 def InRe(s, re):
10374  """Create regular expression membership test
10375  >>> re = Union(Re("a"),Re("b"))
10376  >>> print (simplify(InRe("a", re)))
10377  True
10378  >>> print (simplify(InRe("b", re)))
10379  True
10380  >>> print (simplify(InRe("c", re)))
10381  False
10382  """
10383  s = _coerce_seq(s, re.ctx)
10384  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
10385 
def InRe(s, re)
Definition: z3py.py:10373
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 3055 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().

3055 def Int(name, ctx=None):
3056  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3057 
3058  >>> x = Int('x')
3059  >>> is_int(x)
3060  True
3061  >>> is_int(x + 1)
3062  True
3063  """
3064  ctx = _get_ctx(ctx)
3065  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3066 
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:3055
def IntSort(ctx=None)
Definition: z3py.py:2952

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

3783 def Int2BV(a, num_bits):
3784  """Return the z3 expression Int2BV(a, num_bits).
3785  It is a bit-vector of width num_bits and represents the
3786  modulo of a by 2^num_bits
3787  """
3788  ctx = a.ctx
3789  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
3790 
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:3783

◆ Intersect()

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

Definition at line 10405 of file z3py.py.

10405 def Intersect(*args):
10406  """Create intersection of regular expressions.
10407  >>> re = Intersect(Re("a"), Re("b"), Re("c"))
10408  """
10409  args = _get_args(args)
10410  sz = len(args)
10411  if z3_debug():
10412  _z3_assert(sz > 0, "At least one argument expected.")
10413  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
10414  if sz == 1:
10415  return args[0]
10416  ctx = args[0].ctx
10417  v = (Ast * sz)()
10418  for i in range(sz):
10419  v[i] = args[i].as_ast()
10420  return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
10421 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
def Intersect(args)
Definition: z3py.py:10405
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:10369
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 3067 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().

3067 def Ints(names, ctx=None):
3068  """Return a tuple of Integer constants.
3069 
3070  >>> x, y, z = Ints('x y z')
3071  >>> Sum(x, y, z)
3072  x + y + z
3073  """
3074  ctx = _get_ctx(ctx)
3075  if isinstance(names, str):
3076  names = names.split(" ")
3077  return [Int(name, ctx) for name in names]
3078 
def Int(name, ctx=None)
Definition: z3py.py:3055
def Ints(names, ctx=None)
Definition: z3py.py:3067

◆ 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 2952 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().

2952 def IntSort(ctx=None):
2953  """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
2954 
2955  >>> IntSort()
2956  Int
2957  >>> x = Const('x', IntSort())
2958  >>> is_int(x)
2959  True
2960  >>> x.sort() == IntSort()
2961  True
2962  >>> x.sort() == BoolSort()
2963  False
2964  """
2965  ctx = _get_ctx(ctx)
2966  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
2967 
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
def IntSort(ctx=None)
Definition: z3py.py:2952

◆ IntToStr()

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

Definition at line 10327 of file z3py.py.

Referenced by StrToInt().

10327 def IntToStr(s):
10328  """Convert integer expression to string"""
10329  if not is_expr(s):
10330  s = _py2expr(s)
10331  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
10332 
10333 
def IntToStr(s)
Definition: z3py.py:10327
def is_expr(a)
Definition: z3py.py:1143
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 2999 of file z3py.py.

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

2999 def IntVal(val, ctx=None):
3000  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3001 
3002  >>> IntVal(1)
3003  1
3004  >>> IntVal("100")
3005  100
3006  """
3007  ctx = _get_ctx(ctx)
3008  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3009 
def IntVal(val, ctx=None)
Definition: z3py.py:2999
def IntSort(ctx=None)
Definition: z3py.py:2952
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 3079 of file z3py.py.

3079 def IntVector(prefix, sz, ctx=None):
3080  """Return a list of integer constants of size `sz`.
3081 
3082  >>> X = IntVector('x', 3)
3083  >>> X
3084  [x__0, x__1, x__2]
3085  >>> Sum(X)
3086  x__0 + x__1 + x__2
3087  """
3088  ctx = _get_ctx(ctx)
3089  return [ Int('%s__%s' % (prefix, i), ctx) for i in range(sz) ]
3090 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
def Int(name, ctx=None)
Definition: z3py.py:3055
def IntVector(prefix, sz, ctx=None)
Definition: z3py.py:3079

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

2625 def is_add(a):
2626  """Return `True` if `a` is an expression of the form b + c.
2627 
2628  >>> x, y = Ints('x y')
2629  >>> is_add(x + y)
2630  True
2631  >>> is_add(x - y)
2632  False
2633  """
2634  return is_app_of(a, Z3_OP_ADD)
2635 
def is_app_of(a, k)
Definition: z3py.py:1264
def is_add(a)
Definition: z3py.py:2625

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

2612 def is_algebraic_value(a):
2613  """Return `True` if `a` is an algebraic value of sort Real.
2614 
2615  >>> is_algebraic_value(RealVal("3/5"))
2616  False
2617  >>> n = simplify(Sqrt(2))
2618  >>> n
2619  1.4142135623?
2620  >>> is_algebraic_value(n)
2621  True
2622  """
2623  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2624 
def is_arith(a)
Definition: z3py.py:2506
def is_algebraic_value(a)
Definition: z3py.py:2612

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

1497 def is_and(a):
1498  """Return `True` if `a` is a Z3 and expression.
1499 
1500  >>> p, q = Bools('p q')
1501  >>> is_and(And(p, q))
1502  True
1503  >>> is_and(Or(p, q))
1504  False
1505  """
1506  return is_app_of(a, Z3_OP_AND)
1507 
def is_and(a)
Definition: z3py.py:1497
def is_app_of(a, k)
Definition: z3py.py:1264

◆ 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 1165 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().

1165 def is_app(a):
1166  """Return `True` if `a` is a Z3 function application.
1167 
1168  Note that, constants are function applications with 0 arguments.
1169 
1170  >>> a = Int('a')
1171  >>> is_app(a)
1172  True
1173  >>> is_app(a + 1)
1174  True
1175  >>> is_app(IntSort())
1176  False
1177  >>> is_app(1)
1178  False
1179  >>> is_app(IntVal(1))
1180  True
1181  >>> x = Int('x')
1182  >>> is_app(ForAll(x, x >= 0))
1183  False
1184  """
1185  if not isinstance(a, ExprRef):
1186  return False
1187  k = _ast_kind(a.ctx, a)
1188  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
1189 
def is_app(a)
Definition: z3py.py:1165

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

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

1264 def is_app_of(a, k):
1265  """Return `True` if `a` is an application of the given kind `k`.
1266 
1267  >>> x = Int('x')
1268  >>> n = x + 1
1269  >>> is_app_of(n, Z3_OP_ADD)
1270  True
1271  >>> is_app_of(n, Z3_OP_MUL)
1272  False
1273  """
1274  return is_app(a) and a.decl().kind() == k
1275 
def is_app(a)
Definition: z3py.py:1165
def is_app_of(a, k)
Definition: z3py.py:1264

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

2506 def is_arith(a):
2507  """Return `True` if `a` is an arithmetical expression.
2508 
2509  >>> x = Int('x')
2510  >>> is_arith(x)
2511  True
2512  >>> is_arith(x + 1)
2513  True
2514  >>> is_arith(1)
2515  False
2516  >>> is_arith(IntVal(1))
2517  True
2518  >>> y = Real('y')
2519  >>> is_arith(y)
2520  True
2521  >>> is_arith(y + 1)
2522  True
2523  """
2524  return isinstance(a, ArithRef)
2525 
def is_arith(a)
Definition: z3py.py:2506

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

2207 def is_arith_sort(s):
2208  """Return `True` if s is an arithmetical sort (type).
2209 
2210  >>> is_arith_sort(IntSort())
2211  True
2212  >>> is_arith_sort(RealSort())
2213  True
2214  >>> is_arith_sort(BoolSort())
2215  False
2216  >>> n = Int('x') + 1
2217  >>> is_arith_sort(n.sort())
2218  True
2219  """
2220  return isinstance(s, ArithSortRef)
2221 
def is_arith_sort(s)
Definition: z3py.py:2207

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

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

4345 def is_array(a):
4346  """Return `True` if `a` is a Z3 array expression.
4347 
4348  >>> a = Array('a', IntSort(), IntSort())
4349  >>> is_array(a)
4350  True
4351  >>> is_array(Store(a, 0, 1))
4352  True
4353  >>> is_array(a[0])
4354  False
4355  """
4356  return isinstance(a, ArrayRef)
4357 
def is_array(a)
Definition: z3py.py:4345

◆ is_array_sort()

def z3py.is_array_sort (   a)

Definition at line 4341 of file z3py.py.

4341 def is_array_sort(a):
4342  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4343 
4344 
def is_array_sort(a)
Definition: z3py.py:4341
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 6291 of file z3py.py.

6291 def is_as_array(n):
6292  """Return true if n is a Z3 expression of the form (_ as-array f)."""
6293  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6294 
def is_as_array(n)
Definition: z3py.py:6291
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 1450 of file z3py.py.

Referenced by BoolSort(), and prove().

1450 def is_bool(a):
1451  """Return `True` if `a` is a Z3 Boolean expression.
1452 
1453  >>> p = Bool('p')
1454  >>> is_bool(p)
1455  True
1456  >>> q = Bool('q')
1457  >>> is_bool(And(p, q))
1458  True
1459  >>> x = Real('x')
1460  >>> is_bool(x)
1461  False
1462  >>> is_bool(x == 0)
1463  True
1464  """
1465  return isinstance(a, BoolRef)
1466 
def is_bool(a)
Definition: z3py.py:1450

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

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

3734 def is_bv(a):
3735  """Return `True` if `a` is a Z3 bit-vector expression.
3736 
3737  >>> b = BitVec('b', 32)
3738  >>> is_bv(b)
3739  True
3740  >>> is_bv(b + 10)
3741  True
3742  >>> is_bv(Int('x'))
3743  False
3744  """
3745  return isinstance(a, BitVecRef)
3746 
def is_bv(a)
Definition: z3py.py:3734

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

3269 def is_bv_sort(s):
3270  """Return True if `s` is a Z3 bit-vector sort.
3271 
3272  >>> is_bv_sort(BitVecSort(32))
3273  True
3274  >>> is_bv_sort(IntSort())
3275  False
3276  """
3277  return isinstance(s, BitVecSortRef)
3278 
def is_bv_sort(s)
Definition: z3py.py:3269

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

3747 def is_bv_value(a):
3748  """Return `True` if `a` is a Z3 bit-vector numeral value.
3749 
3750  >>> b = BitVec('b', 32)
3751  >>> is_bv_value(b)
3752  False
3753  >>> b = BitVecVal(10, 32)
3754  >>> b
3755  10
3756  >>> is_bv_value(b)
3757  True
3758  """
3759  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3760 
def is_bv_value(a)
Definition: z3py.py:3747
def is_bv(a)
Definition: z3py.py:3734

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

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

1190 def is_const(a):
1191  """Return `True` if `a` is Z3 constant/variable expression.
1192 
1193  >>> a = Int('a')
1194  >>> is_const(a)
1195  True
1196  >>> is_const(a + 1)
1197  False
1198  >>> is_const(1)
1199  False
1200  >>> is_const(IntVal(1))
1201  True
1202  >>> x = Int('x')
1203  >>> is_const(ForAll(x, x >= 0))
1204  False
1205  """
1206  return is_app(a) and a.num_args() == 0
1207 
def is_app(a)
Definition: z3py.py:1165
def is_const(a)
Definition: z3py.py:1190

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

4358 def is_const_array(a):
4359  """Return `True` if `a` is a Z3 constant array.
4360 
4361  >>> a = K(IntSort(), 10)
4362  >>> is_const_array(a)
4363  True
4364  >>> a = Array('a', IntSort(), IntSort())
4365  >>> is_const_array(a)
4366  False
4367  """
4368  return is_app_of(a, Z3_OP_CONST_ARRAY)
4369 
def is_const_array(a)
Definition: z3py.py:4358
def is_app_of(a, k)
Definition: z3py.py:1264

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

4397 def is_default(a):
4398  """Return `True` if `a` is a Z3 default array expression.
4399  >>> d = Default(K(IntSort(), 10))
4400  >>> is_default(d)
4401  True
4402  """
4403  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4404 
def is_default(a)
Definition: z3py.py:4397
def is_app_of(a, k)
Definition: z3py.py:1264

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

1550 def is_distinct(a):
1551  """Return `True` if `a` is a Z3 distinct expression.
1552 
1553  >>> x, y, z = Ints('x y z')
1554  >>> is_distinct(x == y)
1555  False
1556  >>> is_distinct(Distinct(x, y, z))
1557  True
1558  """
1559  return is_app_of(a, Z3_OP_DISTINCT)
1560 
def is_distinct(a)
Definition: z3py.py:1550
def is_app_of(a, k)
Definition: z3py.py:1264

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

2658 def is_div(a):
2659  """Return `True` if `a` is an expression of the form b / c.
2660 
2661  >>> x, y = Reals('x y')
2662  >>> is_div(x / y)
2663  True
2664  >>> is_div(x + y)
2665  False
2666  >>> x, y = Ints('x y')
2667  >>> is_div(x / y)
2668  False
2669  >>> is_idiv(x / y)
2670  True
2671  """
2672  return is_app_of(a, Z3_OP_DIV)
2673 
def is_div(a)
Definition: z3py.py:2658
def is_app_of(a, k)
Definition: z3py.py:1264

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

Referenced by AstRef.__bool__().

1541 def is_eq(a):
1542  """Return `True` if `a` is a Z3 equality expression.
1543 
1544  >>> x, y = Ints('x y')
1545  >>> is_eq(x == y)
1546  True
1547  """
1548  return is_app_of(a, Z3_OP_EQ)
1549 
def is_eq(a)
Definition: z3py.py:1541
def is_app_of(a, k)
Definition: z3py.py:1264

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

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

1143 def is_expr(a):
1144  """Return `True` if `a` is a Z3 expression.
1145 
1146  >>> a = Int('a')
1147  >>> is_expr(a)
1148  True
1149  >>> is_expr(a + 1)
1150  True
1151  >>> is_expr(IntSort())
1152  False
1153  >>> is_expr(1)
1154  False
1155  >>> is_expr(IntVal(1))
1156  True
1157  >>> x = Int('x')
1158  >>> is_expr(ForAll(x, x >= 0))
1159  True
1160  >>> is_expr(FPVal(1.0))
1161  True
1162  """
1163  return isinstance(a, ExprRef)
1164 
def is_expr(a)
Definition: z3py.py:1143

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

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

1484 def is_false(a):
1485  """Return `True` if `a` is the Z3 false expression.
1486 
1487  >>> p = Bool('p')
1488  >>> is_false(p)
1489  False
1490  >>> is_false(False)
1491  False
1492  >>> is_false(BoolVal(False))
1493  True
1494  """
1495  return is_app_of(a, Z3_OP_FALSE)
1496 
def is_app_of(a, k)
Definition: z3py.py:1264
def is_false(a)
Definition: z3py.py:1484

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

Referenced by is_finite_domain_value().

7302 def is_finite_domain(a):
7303  """Return `True` if `a` is a Z3 finite-domain expression.
7304 
7305  >>> s = FiniteDomainSort('S', 100)
7306  >>> b = Const('b', s)
7307  >>> is_finite_domain(b)
7308  True
7309  >>> is_finite_domain(Int('x'))
7310  False
7311  """
7312  return isinstance(a, FiniteDomainRef)
7313 
7314 
def is_finite_domain(a)
Definition: z3py.py:7302

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

Referenced by FiniteDomainVal().

7280 def is_finite_domain_sort(s):
7281  """Return True if `s` is a Z3 finite-domain sort.
7282 
7283  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7284  True
7285  >>> is_finite_domain_sort(IntSort())
7286  False
7287  """
7288  return isinstance(s, FiniteDomainSortRef)
7289 
7290 
def is_finite_domain_sort(s)
Definition: z3py.py:7280

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

7355 def is_finite_domain_value(a):
7356  """Return `True` if `a` is a Z3 finite-domain value.
7357 
7358  >>> s = FiniteDomainSort('S', 100)
7359  >>> b = Const('b', s)
7360  >>> is_finite_domain_value(b)
7361  False
7362  >>> b = FiniteDomainVal(10, s)
7363  >>> b
7364  10
7365  >>> is_finite_domain_value(b)
7366  True
7367  """
7368  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7369 
7370 
def is_finite_domain_value(a)
Definition: z3py.py:7355
def is_finite_domain(a)
Definition: z3py.py:7302

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

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

9212 def is_fp(a):
9213  """Return `True` if `a` is a Z3 floating-point expression.
9214 
9215  >>> b = FP('b', FPSort(8, 24))
9216  >>> is_fp(b)
9217  True
9218  >>> is_fp(b + 1.0)
9219  True
9220  >>> is_fp(Int('x'))
9221  False
9222  """
9223  return isinstance(a, FPRef)
9224 
def is_fp(a)
Definition: z3py.py:9212

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

8829 def is_fp_sort(s):
8830  """Return True if `s` is a Z3 floating-point sort.
8831 
8832  >>> is_fp_sort(FPSort(8, 24))
8833  True
8834  >>> is_fp_sort(IntSort())
8835  False
8836  """
8837  return isinstance(s, FPSortRef)
8838 
def is_fp_sort(s)
Definition: z3py.py:8829

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

9225 def is_fp_value(a):
9226  """Return `True` if `a` is a Z3 floating-point numeral value.
9227 
9228  >>> b = FP('b', FPSort(8, 24))
9229  >>> is_fp_value(b)
9230  False
9231  >>> b = FPVal(1.0, FPSort(8, 24))
9232  >>> b
9233  1
9234  >>> is_fp_value(b)
9235  True
9236  """
9237  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9238 
def is_fp_value(a)
Definition: z3py.py:9225
def is_fp(a)
Definition: z3py.py:9212

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

9076 def is_fprm(a):
9077  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9078 
9079  >>> rm = RNE()
9080  >>> is_fprm(rm)
9081  True
9082  >>> rm = 1.0
9083  >>> is_fprm(rm)
9084  False
9085  """
9086  return isinstance(a, FPRMRef)
9087 
def is_fprm(a)
Definition: z3py.py:9076

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

8839 def is_fprm_sort(s):
8840  """Return True if `s` is a Z3 floating-point rounding mode sort.
8841 
8842  >>> is_fprm_sort(FPSort(8, 24))
8843  False
8844  >>> is_fprm_sort(RNE().sort())
8845  True
8846  """
8847  return isinstance(s, FPRMSortRef)
8848 
def is_fprm_sort(s)
Definition: z3py.py:8839

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

9088 def is_fprm_value(a):
9089  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9090  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9091 
def is_fprm_value(a)
Definition: z3py.py:9088
def is_fprm(a)
Definition: z3py.py:9076

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

2718 def is_ge(a):
2719  """Return `True` if `a` is an expression of the form b >= c.
2720 
2721  >>> x, y = Ints('x y')
2722  >>> is_ge(x >= y)
2723  True
2724  >>> is_ge(x == y)
2725  False
2726  """
2727  return is_app_of(a, Z3_OP_GE)
2728 
def is_ge(a)
Definition: z3py.py:2718
def is_app_of(a, k)
Definition: z3py.py:1264

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

2729 def is_gt(a):
2730  """Return `True` if `a` is an expression of the form b > c.
2731 
2732  >>> x, y = Ints('x y')
2733  >>> is_gt(x > y)
2734  True
2735  >>> is_gt(x == y)
2736  False
2737  """
2738  return is_app_of(a, Z3_OP_GT)
2739 
def is_gt(a)
Definition: z3py.py:2729
def is_app_of(a, k)
Definition: z3py.py:1264

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

Referenced by is_div().

2674 def is_idiv(a):
2675  """Return `True` if `a` is an expression of the form b div c.
2676 
2677  >>> x, y = Ints('x y')
2678  >>> is_idiv(x / y)
2679  True
2680  >>> is_idiv(x + y)
2681  False
2682  """
2683  return is_app_of(a, Z3_OP_IDIV)
2684 
def is_idiv(a)
Definition: z3py.py:2674
def is_app_of(a, k)
Definition: z3py.py:1264

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

1519 def is_implies(a):
1520  """Return `True` if `a` is a Z3 implication expression.
1521 
1522  >>> p, q = Bools('p q')
1523  >>> is_implies(Implies(p, q))
1524  True
1525  >>> is_implies(And(p, q))
1526  False
1527  """
1528  return is_app_of(a, Z3_OP_IMPLIES)
1529 
def is_implies(a)
Definition: z3py.py:1519
def is_app_of(a, k)
Definition: z3py.py:1264

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

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

2526 def is_int(a):
2527  """Return `True` if `a` is an integer expression.
2528 
2529  >>> x = Int('x')
2530  >>> is_int(x + 1)
2531  True
2532  >>> is_int(1)
2533  False
2534  >>> is_int(IntVal(1))
2535  True
2536  >>> y = Real('y')
2537  >>> is_int(y)
2538  False
2539  >>> is_int(y + 1)
2540  False
2541  """
2542  return is_arith(a) and a.is_int()
2543 
def is_arith(a)
Definition: z3py.py:2506
def is_int(a)
Definition: z3py.py:2526

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

2568 def is_int_value(a):
2569  """Return `True` if `a` is an integer value of sort Int.
2570 
2571  >>> is_int_value(IntVal(1))
2572  True
2573  >>> is_int_value(1)
2574  False
2575  >>> is_int_value(Int('x'))
2576  False
2577  >>> n = Int('x') + 1
2578  >>> n
2579  x + 1
2580  >>> n.arg(1)
2581  1
2582  >>> is_int_value(n.arg(1))
2583  True
2584  >>> is_int_value(RealVal("1/3"))
2585  False
2586  >>> is_int_value(RealVal(1))
2587  False
2588  """
2589  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2590 
def is_int_value(a)
Definition: z3py.py:2568
def is_arith(a)
Definition: z3py.py:2506

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

2740 def is_is_int(a):
2741  """Return `True` if `a` is an expression of the form IsInt(b).
2742 
2743  >>> x = Real('x')
2744  >>> is_is_int(IsInt(x))
2745  True
2746  >>> is_is_int(x)
2747  False
2748  """
2749  return is_app_of(a, Z3_OP_IS_INT)
2750 
def is_app_of(a, k)
Definition: z3py.py:1264
def is_is_int(a)
Definition: z3py.py:2740

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

4370 def is_K(a):
4371  """Return `True` if `a` is a Z3 constant array.
4372 
4373  >>> a = K(IntSort(), 10)
4374  >>> is_K(a)
4375  True
4376  >>> a = Array('a', IntSort(), IntSort())
4377  >>> is_K(a)
4378  False
4379  """
4380  return is_app_of(a, Z3_OP_CONST_ARRAY)
4381 
def is_K(a)
Definition: z3py.py:4370
def is_app_of(a, k)
Definition: z3py.py:1264

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

2696 def is_le(a):
2697  """Return `True` if `a` is an expression of the form b <= c.
2698 
2699  >>> x, y = Ints('x y')
2700  >>> is_le(x <= y)
2701  True
2702  >>> is_le(x < y)
2703  False
2704  """
2705  return is_app_of(a, Z3_OP_LE)
2706 
def is_le(a)
Definition: z3py.py:2696
def is_app_of(a, k)
Definition: z3py.py:1264

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

2707 def is_lt(a):
2708  """Return `True` if `a` is an expression of the form b < c.
2709 
2710  >>> x, y = Ints('x y')
2711  >>> is_lt(x < y)
2712  True
2713  >>> is_lt(x == y)
2714  False
2715  """
2716  return is_app_of(a, Z3_OP_LT)
2717 
def is_lt(a)
Definition: z3py.py:2707
def is_app_of(a, k)
Definition: z3py.py:1264

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

4382 def is_map(a):
4383  """Return `True` if `a` is a Z3 map array expression.
4384 
4385  >>> f = Function('f', IntSort(), IntSort())
4386  >>> b = Array('b', IntSort(), IntSort())
4387  >>> a = Map(f, b)
4388  >>> a
4389  Map(f, b)
4390  >>> is_map(a)
4391  True
4392  >>> is_map(b)
4393  False
4394  """
4395  return is_app_of(a, Z3_OP_ARRAY_MAP)
4396 
def is_map(a)
Definition: z3py.py:4382
def is_app_of(a, k)
Definition: z3py.py:1264

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

2685 def is_mod(a):
2686  """Return `True` if `a` is an expression of the form b % c.
2687 
2688  >>> x, y = Ints('x y')
2689  >>> is_mod(x % y)
2690  True
2691  >>> is_mod(x + y)
2692  False
2693  """
2694  return is_app_of(a, Z3_OP_MOD)
2695 
def is_mod(a)
Definition: z3py.py:2685
def is_app_of(a, k)
Definition: z3py.py:1264

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

2636 def is_mul(a):
2637  """Return `True` if `a` is an expression of the form b * c.
2638 
2639  >>> x, y = Ints('x y')
2640  >>> is_mul(x * y)
2641  True
2642  >>> is_mul(x - y)
2643  False
2644  """
2645  return is_app_of(a, Z3_OP_MUL)
2646 
def is_app_of(a, k)
Definition: z3py.py:1264
def is_mul(a)
Definition: z3py.py:2636

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

1530 def is_not(a):
1531  """Return `True` if `a` is a Z3 not expression.
1532 
1533  >>> p = Bool('p')
1534  >>> is_not(p)
1535  False
1536  >>> is_not(Not(p))
1537  True
1538  """
1539  return is_app_of(a, Z3_OP_NOT)
1540 
def is_not(a)
Definition: z3py.py:1530
def is_app_of(a, k)
Definition: z3py.py:1264

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

1508 def is_or(a):
1509  """Return `True` if `a` is a Z3 or expression.
1510 
1511  >>> p, q = Bools('p q')
1512  >>> is_or(Or(p, q))
1513  True
1514  >>> is_or(And(p, q))
1515  False
1516  """
1517  return is_app_of(a, Z3_OP_OR)
1518 
def is_or(a)
Definition: z3py.py:1508
def is_app_of(a, k)
Definition: z3py.py:1264

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

Referenced by MultiPattern().

1788 def is_pattern(a):
1789  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1790 
1791  >>> f = Function('f', IntSort(), IntSort())
1792  >>> x = Int('x')
1793  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1794  >>> q
1795  ForAll(x, f(x) == 0)
1796  >>> q.num_patterns()
1797  1
1798  >>> is_pattern(q.pattern(0))
1799  True
1800  >>> q.pattern(0)
1801  f(Var(0))
1802  """
1803  return isinstance(a, PatternRef)
1804 
def is_pattern(a)
Definition: z3py.py:1788

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

Referenced by eq().

8118 def is_probe(p):
8119  """Return `True` if `p` is a Z3 probe.
8120 
8121  >>> is_probe(Int('x'))
8122  False
8123  >>> is_probe(Probe('memory'))
8124  True
8125  """
8126  return isinstance(p, Probe)
8127 
def is_probe(p)
Definition: z3py.py:8118

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

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

2026 def is_quantifier(a):
2027  """Return `True` if `a` is a Z3 quantifier.
2028 
2029  >>> f = Function('f', IntSort(), IntSort())
2030  >>> x = Int('x')
2031  >>> q = ForAll(x, f(x) == 0)
2032  >>> is_quantifier(q)
2033  True
2034  >>> is_quantifier(f(x))
2035  False
2036  """
2037  return isinstance(a, QuantifierRef)
2038 
def is_quantifier(a)
Definition: z3py.py:2026

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

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

2591 def is_rational_value(a):
2592  """Return `True` if `a` is rational value of sort Real.
2593 
2594  >>> is_rational_value(RealVal(1))
2595  True
2596  >>> is_rational_value(RealVal("3/5"))
2597  True
2598  >>> is_rational_value(IntVal(1))
2599  False
2600  >>> is_rational_value(1)
2601  False
2602  >>> n = Real('x') + 1
2603  >>> n.arg(1)
2604  1
2605  >>> is_rational_value(n.arg(1))
2606  True
2607  >>> is_rational_value(Real('x'))
2608  False
2609  """
2610  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2611 
def is_arith(a)
Definition: z3py.py:2506
def is_rational_value(a)
Definition: z3py.py:2591

◆ is_re()

def z3py.is_re (   s)

Definition at line 10369 of file z3py.py.

10369 def is_re(s):
10370  return isinstance(s, ReRef)
10371 
10372 
def is_re(s)
Definition: z3py.py:10369

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

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

2544 def is_real(a):
2545  """Return `True` if `a` is a real expression.
2546 
2547  >>> x = Int('x')
2548  >>> is_real(x + 1)
2549  False
2550  >>> y = Real('y')
2551  >>> is_real(y)
2552  True
2553  >>> is_real(y + 1)
2554  True
2555  >>> is_real(1)
2556  False
2557  >>> is_real(RealVal(1))
2558  True
2559  """
2560  return is_arith(a) and a.is_real()
2561 
def is_real(a)
Definition: z3py.py:2544
def is_arith(a)
Definition: z3py.py:2506

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

4589 def is_select(a):
4590  """Return `True` if `a` is a Z3 array select application.
4591 
4592  >>> a = Array('a', IntSort(), IntSort())
4593  >>> is_select(a)
4594  False
4595  >>> i = Int('i')
4596  >>> is_select(a[i])
4597  True
4598  """