Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

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

Functions

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

Variables

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

1662 def And(*args):
1663  """Create a Z3 and-expression or and-probe.
1664 
1665  >>> p, q, r = Bools('p q r')
1666  >>> And(p, q, r)
1667  And(p, q, r)
1668  >>> P = BoolVector('p', 5)
1669  >>> And(P)
1670  And(p__0, p__1, p__2, p__3, p__4)
1671  """
1672  last_arg = None
1673  if len(args) > 0:
1674  last_arg = args[len(args)-1]
1675  if isinstance(last_arg, Context):
1676  ctx = args[len(args)-1]
1677  args = args[:len(args)-1]
1678  elif len(args) == 1 and isinstance(args[0], AstVector):
1679  ctx = args[0].ctx
1680  args = [a for a in args[0]]
1681  else:
1682  ctx = main_ctx()
1683  args = _get_args(args)
1684  ctx_args = _ctx_from_ast_arg_list(args, ctx)
1685  if __debug__:
1686  _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch")
1687  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1688  if _has_probe(args):
1689  return _probe_and(args, ctx)
1690  else:
1691  args = _coerce_expr_list(args, ctx)
1692  _args, sz = _to_ast_array(args)
1693  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1694 
def And(args)
Definition: z3py.py:1662
def main_ctx()
Definition: z3py.py:207
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].

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

Referenced by Then().

7684 def AndThen(*ts, **ks):
7685  """Return a tactic that applies the tactics in `*ts` in sequence.
7686 
7687  >>> x, y = Ints('x y')
7688  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
7689  >>> t(And(x == 0, y > x + 1))
7690  [[Not(y <= 1)]]
7691  >>> t(And(x == 0, y > x + 1)).as_expr()
7692  Not(y <= 1)
7693  """
7694  if __debug__:
7695  _z3_assert(len(ts) >= 2, "At least two arguments expected")
7696  ctx = ks.get('ctx', None)
7697  num = len(ts)
7698  r = ts[0]
7699  for i in range(num - 1):
7700  r = _and_then(r, ts[i+1], ctx)
7701  return r
7702 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3286
def AndThen(ts, ks)
Definition: z3py.py:7684

◆ append_log()

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

Definition at line 101 of file z3py.py.

101 def append_log(s):
102  """Append user-defined string to interaction log. """
103  Z3_append_log(s)
104 
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
def append_log(s)
Definition: z3py.py:101

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

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

5012 def args2params(arguments, keywords, ctx=None):
5013  """Convert python arguments into a Z3_params object.
5014  A ':' is added to the keywords, and '_' is replaced with '-'
5015 
5016  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5017  (params model true relevancy 2 elim_and true)
5018  """
5019  if __debug__:
5020  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5021  prev = None
5022  r = ParamsRef(ctx)
5023  for a in arguments:
5024  if prev is None:
5025  prev = a
5026  else:
5027  r.set(prev, a)
5028  prev = None
5029  for k in keywords:
5030  v = keywords[k]
5031  r.set(k, v)
5032  return r
5033 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5012

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

4373 def Array(name, dom, rng):
4374  """Return an array constant named `name` with the given domain and range sorts.
4375 
4376  >>> a = Array('a', IntSort(), IntSort())
4377  >>> a.sort()
4378  Array(Int, Int)
4379  >>> a[0]
4380  a[0]
4381  """
4382  s = ArraySort(dom, rng)
4383  ctx = s.ctx
4384  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4385 
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:4341
def to_symbol(s, ctx=None)
Definition: z3py.py:105
def Array(name, dom, rng)
Definition: z3py.py:4373

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

Referenced by ArraySortRef.domain(), and ArraySortRef.range().

4341 def ArraySort(*sig):
4342  """Return the Z3 array sort with the given domain and range sorts.
4343 
4344  >>> A = ArraySort(IntSort(), BoolSort())
4345  >>> A
4346  Array(Int, Bool)
4347  >>> A.domain()
4348  Int
4349  >>> A.range()
4350  Bool
4351  >>> AA = ArraySort(IntSort(), A)
4352  >>> AA
4353  Array(Int, Array(Int, Bool))
4354  """
4355  sig = _get_args(sig)
4356  if __debug__:
4357  _z3_assert(len(sig) > 1, "At least two arguments expected")
4358  arity = len(sig) - 1
4359  r = sig[arity]
4360  d = sig[0]
4361  if __debug__:
4362  for s in sig:
4363  _z3_assert(is_sort(s), "Z3 sort expected")
4364  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4365  ctx = d.ctx
4366  if len(sig) == 2:
4367  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4368  dom = (Sort * arity)()
4369  for i in range(arity):
4370  dom[i] = sig[i].ast
4371  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4372 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3286
def ArraySort(sig)
Definition: z3py.py:4341
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:580

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

8265 def AtLeast(*args):
8266  """Create an at-most Pseudo-Boolean k constraint.
8267 
8268  >>> a, b, c = Bools('a b c')
8269  >>> f = AtLeast(a, b, c, 2)
8270  """
8271  args = _get_args(args)
8272  if __debug__:
8273  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8274  ctx = _ctx_from_ast_arg_list(args)
8275  if __debug__:
8276  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8277  args1 = _coerce_expr_list(args[:-1], ctx)
8278  k = args[-1]
8279  _args, sz = _to_ast_array(args1)
8280  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8281 
8282 
def AtLeast(args)
Definition: z3py.py:8265
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 8248 of file z3py.py.

8248 def AtMost(*args):
8249  """Create an at-most Pseudo-Boolean k constraint.
8250 
8251  >>> a, b, c = Bools('a b c')
8252  >>> f = AtMost(a, b, c, 2)
8253  """
8254  args = _get_args(args)
8255  if __debug__:
8256  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8257  ctx = _ctx_from_ast_arg_list(args)
8258  if __debug__:
8259  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8260  args1 = _coerce_expr_list(args[:-1], ctx)
8261  k = args[-1]
8262  _args, sz = _to_ast_array(args1)
8263  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8264 
def AtMost(args)
Definition: z3py.py:8248
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 3743 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().

3743 def BitVec(name, bv, ctx=None):
3744  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3745  If `ctx=None`, then the global context is used.
3746 
3747  >>> x = BitVec('x', 16)
3748  >>> is_bv(x)
3749  True
3750  >>> x.size()
3751  16
3752  >>> x.sort()
3753  BitVec(16)
3754  >>> word = BitVecSort(16)
3755  >>> x2 = BitVec('x', word)
3756  >>> eq(x, x2)
3757  True
3758  """
3759  if isinstance(bv, BitVecSortRef):
3760  ctx = bv.ctx
3761  else:
3762  ctx = _get_ctx(ctx)
3763  bv = BitVecSort(bv, ctx)
3764  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
3765 
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:105
def BitVec(name, bv, ctx=None)
Definition: z3py.py:3743
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3713

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

3766 def BitVecs(names, bv, ctx=None):
3767  """Return a tuple of bit-vector constants of size bv.
3768 
3769  >>> x, y, z = BitVecs('x y z', 16)
3770  >>> x.size()
3771  16
3772  >>> x.sort()
3773  BitVec(16)
3774  >>> Sum(x, y, z)
3775  0 + x + y + z
3776  >>> Product(x, y, z)
3777  1*x*y*z
3778  >>> simplify(Product(x, y, z))
3779  x*y*z
3780  """
3781  ctx = _get_ctx(ctx)
3782  if isinstance(names, str):
3783  names = names.split(" ")
3784  return [BitVec(name, bv, ctx) for name in names]
3785 
def BitVec(name, bv, ctx=None)
Definition: z3py.py:3743
def BitVecs(names, bv, ctx=None)
Definition: z3py.py:3766

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

Referenced by BitVec(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), BitVecSortRef.size(), and BitVecRef.sort().

3713 def BitVecSort(sz, ctx=None):
3714  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3715 
3716  >>> Byte = BitVecSort(8)
3717  >>> Word = BitVecSort(16)
3718  >>> Byte
3719  BitVec(8)
3720  >>> x = Const('x', Byte)
3721  >>> eq(x, BitVec('x', 8))
3722  True
3723  """
3724  ctx = _get_ctx(ctx)
3725  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
3726 
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:3713

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

3727 def BitVecVal(val, bv, ctx=None):
3728  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3729 
3730  >>> v = BitVecVal(10, 32)
3731  >>> v
3732  10
3733  >>> print("0x%.8x" % v.as_long())
3734  0x0000000a
3735  """
3736  if is_bv_sort(bv):
3737  ctx = bv.ctx
3738  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3739  else:
3740  ctx = _get_ctx(ctx)
3741  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3742 
def BitVecVal(val, bv, ctx=None)
Definition: z3py.py:3727
def is_bv_sort(s)
Definition: z3py.py:3195
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3713
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 1548 of file z3py.py.

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

1548 def Bool(name, ctx=None):
1549  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1550 
1551  >>> p = Bool('p')
1552  >>> q = Bool('q')
1553  >>> And(p, q)
1554  And(p, q)
1555  """
1556  ctx = _get_ctx(ctx)
1557  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1558 
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:105
def Bool(name, ctx=None)
Definition: z3py.py:1548
def BoolSort(ctx=None)
Definition: z3py.py:1513

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

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

1559 def Bools(names, ctx=None):
1560  """Return a tuple of Boolean constants.
1561 
1562  `names` is a single string containing all names separated by blank spaces.
1563  If `ctx=None`, then the global context is used.
1564 
1565  >>> p, q, r = Bools('p q r')
1566  >>> And(p, Or(q, r))
1567  And(p, Or(q, r))
1568  """
1569  ctx = _get_ctx(ctx)
1570  if isinstance(names, str):
1571  names = names.split(" ")
1572  return [Bool(name, ctx) for name in names]
1573 
def Bools(names, ctx=None)
Definition: z3py.py:1559
def Bool(name, ctx=None)
Definition: z3py.py:1548

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

Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), ArraySortRef.domain(), ArrayRef.domain(), If(), IntSort(), is_arith_sort(), ArraySortRef.range(), ArrayRef.range(), and ArrayRef.sort().

1513 def BoolSort(ctx=None):
1514  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1515 
1516  >>> BoolSort()
1517  Bool
1518  >>> p = Const('p', BoolSort())
1519  >>> is_bool(p)
1520  True
1521  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1522  >>> r(0, 1)
1523  r(0, 1)
1524  >>> is_bool(r(0, 1))
1525  True
1526  """
1527  ctx = _get_ctx(ctx)
1528  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1529 
def is_bool(a)
Definition: z3py.py:1402
def BoolSort(ctx=None)
Definition: z3py.py:1513

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

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

1530 def BoolVal(val, ctx=None):
1531  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1532 
1533  >>> BoolVal(True)
1534  True
1535  >>> is_true(BoolVal(True))
1536  True
1537  >>> is_true(True)
1538  False
1539  >>> is_false(BoolVal(False))
1540  True
1541  """
1542  ctx = _get_ctx(ctx)
1543  if val == False:
1544  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1545  else:
1546  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1547 
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:1530

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

Referenced by And(), and Or().

1574 def BoolVector(prefix, sz, ctx=None):
1575  """Return a list of Boolean constants of size `sz`.
1576 
1577  The constants are named using the given prefix.
1578  If `ctx=None`, then the global context is used.
1579 
1580  >>> P = BoolVector('p', 3)
1581  >>> P
1582  [p__0, p__1, p__2]
1583  >>> And(P)
1584  And(p__0, p__1, p__2)
1585  """
1586  return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
1587 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3286
def BoolVector(prefix, sz, ctx=None)
Definition: z3py.py:1574
def Bool(name, ctx=None)
Definition: z3py.py:1548

◆ 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)
[b = 1, x = 2]

Definition at line 3683 of file z3py.py.

3683 def BV2Int(a, is_signed=False):
3684  """Return the Z3 expression BV2Int(a).
3685 
3686  >>> b = BitVec('b', 3)
3687  >>> BV2Int(b).sort()
3688  Int
3689  >>> x = Int('x')
3690  >>> x > BV2Int(b)
3691  x > BV2Int(b)
3692  >>> x > BV2Int(b, is_signed=False)
3693  x > BV2Int(b)
3694  >>> x > BV2Int(b, is_signed=True)
3695  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3696  >>> solve(x > BV2Int(b), b == 1, x < 3)
3697  [b = 1, x = 2]
3698  """
3699  if __debug__:
3700  _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
3701  ctx = a.ctx
3702 
3703  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3704 
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 BV2Int(a, is_signed=False)
Definition: z3py.py:3683
def is_bv(a)
Definition: z3py.py:3656

◆ BVAddNoOverflow()

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

Definition at line 4138 of file z3py.py.

4138 def BVAddNoOverflow(a, b, signed):
4139  """A predicate the determines that bit-vector addition does not overflow"""
4140  _check_bv_args(a, b)
4141  a, b = _coerce_exprs(a, b)
4142  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4143 
def BVAddNoOverflow(a, b, signed)
Definition: z3py.py:4138
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 4144 of file z3py.py.

4144 def BVAddNoUnderflow(a, b):
4145  """A predicate the determines that signed bit-vector addition does not underflow"""
4146  _check_bv_args(a, b)
4147  a, b = _coerce_exprs(a, b)
4148  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4149 
def BVAddNoUnderflow(a, b)
Definition: z3py.py:4144
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 4175 of file z3py.py.

4175 def BVMulNoOverflow(a, b, signed):
4176  """A predicate the determines that bit-vector multiplication does not overflow"""
4177  _check_bv_args(a, b)
4178  a, b = _coerce_exprs(a, b)
4179  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4180 
4181 
def BVMulNoOverflow(a, b, signed)
Definition: z3py.py:4175
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 4182 of file z3py.py.

4182 def BVMulNoUnderflow(a, b):
4183  """A predicate the determines that bit-vector signed multiplication does not underflow"""
4184  _check_bv_args(a, b)
4185  a, b = _coerce_exprs(a, b)
4186  return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4187 
4188 
4189 
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:4182

◆ BVRedAnd()

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

Definition at line 4126 of file z3py.py.

4126 def BVRedAnd(a):
4127  """Return the reduction-and expression of `a`."""
4128  if __debug__:
4129  _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
4130  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4131 
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:4126
def is_bv(a)
Definition: z3py.py:3656

◆ BVRedOr()

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

Definition at line 4132 of file z3py.py.

4132 def BVRedOr(a):
4133  """Return the reduction-or expression of `a`."""
4134  if __debug__:
4135  _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
4136  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4137 
def BVRedOr(a)
Definition: z3py.py:4132
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:3656

◆ BVSDivNoOverflow()

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

Definition at line 4163 of file z3py.py.

4163 def BVSDivNoOverflow(a, b):
4164  """A predicate the determines that bit-vector signed division does not overflow"""
4165  _check_bv_args(a, b)
4166  a, b = _coerce_exprs(a, b)
4167  return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4168 
def BVSDivNoOverflow(a, b)
Definition: z3py.py:4163
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 4169 of file z3py.py.

4169 def BVSNegNoOverflow(a):
4170  """A predicate the determines that bit-vector unary negation does not overflow"""
4171  if __debug__:
4172  _z3_assert(is_bv(a), "Argument should be a bit-vector")
4173  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4174 
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 BVSNegNoOverflow(a)
Definition: z3py.py:4169
def is_bv(a)
Definition: z3py.py:3656

◆ BVSubNoOverflow()

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

Definition at line 4150 of file z3py.py.

4150 def BVSubNoOverflow(a, b):
4151  """A predicate the determines that bit-vector subtraction does not overflow"""
4152  _check_bv_args(a, b)
4153  a, b = _coerce_exprs(a, b)
4154  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4155 
4156 
def BVSubNoOverflow(a, b)
Definition: z3py.py:4150
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 4157 of file z3py.py.

4157 def BVSubNoUnderflow(a, b, signed):
4158  """A predicate the determines that bit-vector subtraction does not underflow"""
4159  _check_bv_args(a, b)
4160  a, b = _coerce_exprs(a, b)
4161  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4162 
def BVSubNoUnderflow(a, b, signed)
Definition: z3py.py:4157
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 3145 of file z3py.py.

3145 def Cbrt(a, ctx=None):
3146  """ Return a Z3 expression which represents the cubic root of a.
3147 
3148  >>> x = Real('x')
3149  >>> Cbrt(x)
3150  x**(1/3)
3151  """
3152  if not is_expr(a):
3153  ctx = _get_ctx(ctx)
3154  a = RealVal(a, ctx)
3155  return a ** "1/3"
3156 
def Cbrt(a, ctx=None)
Definition: z3py.py:3145
def RealVal(val, ctx=None)
Definition: z3py.py:2938
def is_expr(a)
Definition: z3py.py:1095

◆ Complement()

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

Definition at line 10272 of file z3py.py.

10272 def Complement(re):
10273  """Create the complement regular expression."""
10274  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
10275 
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:10272

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

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

3786 def Concat(*args):
3787  """Create a Z3 bit-vector concatenation expression.
3788 
3789  >>> v = BitVecVal(1, 4)
3790  >>> Concat(v, v+1, v)
3791  Concat(Concat(1, 1 + 1), 1)
3792  >>> simplify(Concat(v, v+1, v))
3793  289
3794  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3795  121
3796  """
3797  args = _get_args(args)
3798  sz = len(args)
3799  if __debug__:
3800  _z3_assert(sz >= 2, "At least two arguments expected.")
3801 
3802  ctx = None
3803  for a in args:
3804  if is_expr(a):
3805  ctx = a.ctx
3806  break
3807  if is_seq(args[0]) or isinstance(args[0], str):
3808  args = [_coerce_seq(s, ctx) for s in args]
3809  if __debug__:
3810  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
3811  v = (Ast * sz)()
3812  for i in range(sz):
3813  v[i] = args[i].as_ast()
3814  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
3815 
3816  if is_re(args[0]):
3817  if __debug__:
3818  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
3819  v = (Ast * sz)()
3820  for i in range(sz):
3821  v[i] = args[i].as_ast()
3822  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
3823 
3824  if __debug__:
3825  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
3826  r = args[0]
3827  for i in range(sz - 1):
3828  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3829  return r
3830 
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:3286
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:10212
def is_expr(a)
Definition: z3py.py:1095
def is_bv(a)
Definition: z3py.py:3656
def Concat(args)
Definition: z3py.py:3786
def is_seq(a)
Definition: z3py.py:9974

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

Referenced by If().

8103 def Cond(p, t1, t2, ctx=None):
8104  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8105 
8106  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8107  """
8108  p = _to_probe(p, ctx)
8109  t1 = _to_tactic(t1, ctx)
8110  t2 = _to_tactic(t2, ctx)
8111  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8112 
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8103
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 1281 of file z3py.py.

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

1281 def Const(name, sort):
1282  """Create a constant of the given sort.
1283 
1284  >>> Const('x', IntSort())
1285  x
1286  """
1287  if __debug__:
1288  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1289  ctx = sort.ctx
1290  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1291 
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:105
def Const(name, sort)
Definition: z3py.py:1281

◆ Consts()

def z3py.Consts (   names,
  sort 
)
Create a several constants of the given sort.

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

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

Definition at line 1292 of file z3py.py.

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

1292 def Consts(names, sort):
1293  """Create a several constants of the given sort.
1294 
1295  `names` is a string containing the names of all constants to be created.
1296  Blank spaces separate the names of different constants.
1297 
1298  >>> x, y, z = Consts('x y z', IntSort())
1299  >>> x + y + z
1300  x + y + z
1301  """
1302  if isinstance(names, str):
1303  names = names.split(" ")
1304  return [Const(name, sort) for name in names]
1305 
def Consts(names, sort)
Definition: z3py.py:1292
def Const(name, sort)
Definition: z3py.py:1281

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

10093 def Contains(a, b):
10094  """Check if 'a' contains 'b'
10095  >>> s1 = Contains("abc", "ab")
10096  >>> simplify(s1)
10097  True
10098  >>> s2 = Contains("abc", "bc")
10099  >>> simplify(s2)
10100  True
10101  >>> x, y, z = Strings('x y z')
10102  >>> s3 = Contains(Concat(x,y,z), y)
10103  >>> simplify(s3)
10104  True
10105  """
10106  ctx = _get_ctx2(a, b)
10107  a = _coerce_seq(a, ctx)
10108  b = _coerce_seq(b, ctx)
10109  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10110 
10111 
def Contains(a, b)
Definition: z3py.py:10093
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 4747 of file z3py.py.

Referenced by Datatype.create().

4747 def CreateDatatypes(*ds):
4748  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4749 
4750  In the following example we define a Tree-List using two mutually recursive datatypes.
4751 
4752  >>> TreeList = Datatype('TreeList')
4753  >>> Tree = Datatype('Tree')
4754  >>> # Tree has two constructors: leaf and node
4755  >>> Tree.declare('leaf', ('val', IntSort()))
4756  >>> # a node contains a list of trees
4757  >>> Tree.declare('node', ('children', TreeList))
4758  >>> TreeList.declare('nil')
4759  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4760  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4761  >>> Tree.val(Tree.leaf(10))
4762  val(leaf(10))
4763  >>> simplify(Tree.val(Tree.leaf(10)))
4764  10
4765  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4766  >>> n1
4767  node(cons(leaf(10), cons(leaf(20), nil)))
4768  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4769  >>> simplify(n2 == n1)
4770  False
4771  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4772  True
4773  """
4774  ds = _get_args(ds)
4775  if __debug__:
4776  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4777  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
4778  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
4779  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
4780  ctx = ds[0].ctx
4781  num = len(ds)
4782  names = (Symbol * num)()
4783  out = (Sort * num)()
4784  clists = (ConstructorList * num)()
4785  to_delete = []
4786  for i in range(num):
4787  d = ds[i]
4788  names[i] = to_symbol(d.name, ctx)
4789  num_cs = len(d.constructors)
4790  cs = (Constructor * num_cs)()
4791  for j in range(num_cs):
4792  c = d.constructors[j]
4793  cname = to_symbol(c[0], ctx)
4794  rname = to_symbol(c[1], ctx)
4795  fs = c[2]
4796  num_fs = len(fs)
4797  fnames = (Symbol * num_fs)()
4798  sorts = (Sort * num_fs)()
4799  refs = (ctypes.c_uint * num_fs)()
4800  for k in range(num_fs):
4801  fname = fs[k][0]
4802  ftype = fs[k][1]
4803  fnames[k] = to_symbol(fname, ctx)
4804  if isinstance(ftype, Datatype):
4805  if __debug__:
4806  _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4807  sorts[k] = None
4808  refs[k] = ds.index(ftype)
4809  else:
4810  if __debug__:
4811  _z3_assert(is_sort(ftype), "Z3 sort expected")
4812  sorts[k] = ftype.ast
4813  refs[k] = 0
4814  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4815  to_delete.append(ScopedConstructor(cs[j], ctx))
4816  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4817  to_delete.append(ScopedConstructorList(clists[i], ctx))
4818  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4819  result = []
4820 
4821  for i in range(num):
4822  dref = DatatypeSortRef(out[i], ctx)
4823  num_cs = dref.num_constructors()
4824  for j in range(num_cs):
4825  cref = dref.constructor(j)
4826  cref_name = cref.name()
4827  cref_arity = cref.arity()
4828  if cref.arity() == 0:
4829  cref = cref()
4830  setattr(dref, cref_name, cref)
4831  rref = dref.recognizer(j)
4832  setattr(dref, "is_" + cref_name, rref)
4833  for k in range(cref_arity):
4834  aref = dref.accessor(j, k)
4835  setattr(dref, aref.name(), aref)
4836  result.append(dref)
4837  return tuple(result)
4838 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3286
def to_symbol(s, ctx=None)
Definition: z3py.py:105
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:4747
def is_sort(s)
Definition: z3py.py:580
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 617 of file z3py.py.

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

617 def DeclareSort(name, ctx=None):
618  """Create a new uninterpreted sort named `name`.
619 
620  If `ctx=None`, then the new sort is declared in the global Z3Py context.
621 
622  >>> A = DeclareSort('A')
623  >>> a = Const('a', A)
624  >>> b = Const('b', A)
625  >>> a.sort() == A
626  True
627  >>> b.sort() == A
628  True
629  >>> a == b
630  a == b
631  """
632  ctx = _get_ctx(ctx)
633  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
634 
def to_symbol(s, ctx=None)
Definition: z3py.py:105
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:617

◆ Default()

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

Definition at line 4407 of file z3py.py.

Referenced by is_default().

4407 def Default(a):
4408  """ Return a default value for array expression.
4409  >>> b = K(IntSort(), 1)
4410  >>> prove(Default(b) == 1)
4411  proved
4412  """
4413  if __debug__:
4414  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
4415  return a.default()
4416 
4417 
def is_array(a)
Definition: z3py.py:4264
def Default(a)
Definition: z3py.py:4407

◆ describe_probes()

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

Definition at line 8033 of file z3py.py.

8033 def describe_probes():
8034  """Display a (tabular) description of all available probes in Z3."""
8035  if in_html_mode():
8036  even = True
8037  print('<table border="1" cellpadding="2" cellspacing="0">')
8038  for p in probes():
8039  if even:
8040  print('<tr style="background-color:#CFCFCF">')
8041  even = False
8042  else:
8043  print('<tr>')
8044  even = True
8045  print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
8046  print('</table>')
8047  else:
8048  for p in probes():
8049  print('%s : %s' % (p, probe_description(p)))
8050 
def probes(ctx=None)
Definition: z3py.py:8015
def probe_description(name, ctx=None)
Definition: z3py.py:8025
def describe_probes()
Definition: z3py.py:8033

◆ describe_tactics()

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

Definition at line 7842 of file z3py.py.

7842 def describe_tactics():
7843  """Display a (tabular) description of all available tactics in Z3."""
7844  if in_html_mode():
7845  even = True
7846  print('<table border="1" cellpadding="2" cellspacing="0">')
7847  for t in tactics():
7848  if even:
7849  print('<tr style="background-color:#CFCFCF">')
7850  even = False
7851  else:
7852  print('<tr>')
7853  even = True
7854  print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
7855  print('</table>')
7856  else:
7857  for t in tactics():
7858  print('%s : %s' % (t, tactic_description(t)))
7859 
def tactics(ctx=None)
Definition: z3py.py:7824
def tactic_description(name, ctx=None)
Definition: z3py.py:7834
def describe_tactics()
Definition: z3py.py:7842

◆ disable_trace()

def z3py.disable_trace (   msg)

Definition at line 66 of file z3py.py.

66 def disable_trace(msg):
67  Z3_disable_trace(msg)
68 
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:66

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

1250 def Distinct(*args):
1251  """Create a Z3 distinct expression.
1252 
1253  >>> x = Int('x')
1254  >>> y = Int('y')
1255  >>> Distinct(x, y)
1256  x != y
1257  >>> z = Int('z')
1258  >>> Distinct(x, y, z)
1259  Distinct(x, y, z)
1260  >>> simplify(Distinct(x, y, z))
1261  Distinct(x, y, z)
1262  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1263  And(Not(x == y), Not(x == z), Not(y == z))
1264  """
1265  args = _get_args(args)
1266  ctx = _ctx_from_ast_arg_list(args)
1267  if __debug__:
1268  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
1269  args = _coerce_expr_list(args, ctx)
1270  _args, sz = _to_ast_array(args)
1271  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1272 
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 Distinct(args)
Definition: z3py.py:1250

◆ 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)
seq.empty
>>> e4 = Empty(ReSort(SeqSort(IntSort())))
>>> print(e4)
re.empty

Definition at line 10028 of file z3py.py.

10028 def Empty(s):
10029  """Create the empty sequence of the given sort
10030  >>> e = Empty(StringSort())
10031  >>> e2 = StringVal("")
10032  >>> print(e.eq(e2))
10033  True
10034  >>> e3 = Empty(SeqSort(IntSort()))
10035  >>> print(e3)
10036  seq.empty
10037  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10038  >>> print(e4)
10039  re.empty
10040  """
10041  if isinstance(s, SeqSortRef):
10042  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10043  if isinstance(s, ReSortRef):
10044  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10045  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10046 
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:10028

◆ EmptySet()

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

Definition at line 4537 of file z3py.py.

4537 def EmptySet(s):
4538  """Create the empty set
4539  >>> EmptySet(IntSort())
4540  K(Int, False)
4541  """
4542  ctx = s.ctx
4543  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4544 
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
def EmptySet(s)
Definition: z3py.py:4537

◆ enable_trace()

def z3py.enable_trace (   msg)

Definition at line 63 of file z3py.py.

63 def enable_trace(msg):
64  Z3_enable_trace(msg)
65 
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:63

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

4936 def EnumSort(name, values, ctx=None):
4937  """Return a new enumeration sort named `name` containing the given values.
4938 
4939  The result is a pair (sort, list of constants).
4940  Example:
4941  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
4942  """
4943  if __debug__:
4944  _z3_assert(isinstance(name, str), "Name must be a string")
4945  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
4946  _z3_assert(len(values) > 0, "At least one value expected")
4947  ctx = _get_ctx(ctx)
4948  num = len(values)
4949  _val_names = (Symbol * num)()
4950  for i in range(num):
4951  _val_names[i] = to_symbol(values[i])
4952  _values = (FuncDecl * num)()
4953  _testers = (FuncDecl * num)()
4954  name = to_symbol(name)
4955  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
4956  V = []
4957  for i in range(num):
4958  V.append(FuncDeclRef(_values[i], ctx))
4959  V = [a() for a in V]
4960  return S, V
4961 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3286
def to_symbol(s, ctx=None)
Definition: z3py.py:105
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4936
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 416 of file z3py.py.

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

416 def eq(a, b):
417  """Return `True` if `a` and `b` are structurally identical AST nodes.
418 
419  >>> x = Int('x')
420  >>> y = Int('y')
421  >>> eq(x, y)
422  False
423  >>> eq(x + 1, x + 1)
424  True
425  >>> eq(x + 1, 1 + x)
426  False
427  >>> eq(simplify(x + 1), simplify(1 + x))
428  True
429  """
430  if __debug__:
431  _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
432  return a.eq(b)
433 
def eq(a, b)
Definition: z3py.py:416
def is_ast(a)
Definition: z3py.py:396

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

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

2034 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2035  """Create a Z3 exists formula.
2036 
2037  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2038 
2039 
2040  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2041  >>> x = Int('x')
2042  >>> y = Int('y')
2043  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2044  >>> q
2045  Exists([x, y], f(x, y) >= x)
2046  >>> is_quantifier(q)
2047  True
2048  >>> r = Tactic('nnf')(q).as_expr()
2049  >>> is_quantifier(r)
2050  False
2051  """
2052  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2053 
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2034

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

4492 def Ext(a, b):
4493  """Return extensionality index for one-dimensional arrays.
4494  >> a, b = Consts('a b', SetSort(IntSort()))
4495  >> Ext(a, b)
4496  Ext(a, b)
4497  """
4498  ctx = a.ctx
4499  if __debug__:
4500  _z3_assert(is_array(a) and is_array(b), "arguments must be arrays")
4501  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4502 
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(a)
Definition: z3py.py:4264
def Ext(a, b)
Definition: z3py.py:4492

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

3831 def Extract(high, low, a):
3832  """Create a Z3 bit-vector extraction expression, or create a string extraction expression.
3833 
3834  >>> x = BitVec('x', 8)
3835  >>> Extract(6, 2, x)
3836  Extract(6, 2, x)
3837  >>> Extract(6, 2, x).sort()
3838  BitVec(5)
3839  >>> simplify(Extract(StringVal("abcd"),2,1))
3840  c
3841  """
3842  if isinstance(high, str):
3843  high = StringVal(high)
3844  if is_seq(high):
3845  s = high
3846  offset, length = _coerce_exprs(low, a, s.ctx)
3847  return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
3848  if __debug__:
3849  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3850  _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")
3851  _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
3852  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
3853 
def Extract(high, low, a)
Definition: z3py.py:3831
def StringVal(s, ctx=None)
Definition: z3py.py:10000
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.
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:3656
def is_seq(a)
Definition: z3py.py:9974

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

8066 def FailIf(p, ctx=None):
8067  """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8068 
8069  In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
8070 
8071  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8072  >>> x, y = Ints('x y')
8073  >>> g = Goal()
8074  >>> g.add(x > 0)
8075  >>> g.add(y > 0)
8076  >>> t(g)
8077  [[x > 0, y > 0]]
8078  >>> g.add(x == y + 1)
8079  >>> t(g)
8080  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8081  """
8082  p = _to_probe(p, ctx)
8083  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8084 
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:8066

◆ FiniteDomainSort()

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

Definition at line 7158 of file z3py.py.

7158 def FiniteDomainSort(name, sz, ctx=None):
7159  """Create a named finite domain sort of a given size sz"""
7160  if not isinstance(name, Symbol):
7161  name = to_symbol(name)
7162  ctx = _get_ctx(ctx)
7163  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7164 
def to_symbol(s, ctx=None)
Definition: z3py.py:105
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:7158

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

7226 def FiniteDomainVal(val, sort, ctx=None):
7227  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7228 
7229  >>> s = FiniteDomainSort('S', 256)
7230  >>> FiniteDomainVal(255, s)
7231  255
7232  >>> FiniteDomainVal('100', s)
7233  100
7234  """
7235  if __debug__:
7236  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" )
7237  ctx = sort.ctx
7238  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7239 
def is_finite_domain_sort(s)
Definition: z3py.py:7165
def FiniteDomainVal(val, sort, ctx=None)
Definition: z3py.py:7226
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 8690 of file z3py.py.

8690 def Float128(ctx=None):
8691  """Floating-point 128-bit (quadruple) sort."""
8692  ctx = _get_ctx(ctx)
8693  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
8694 
def Float128(ctx=None)
Definition: z3py.py:8690
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 8660 of file z3py.py.

8660 def Float16(ctx=None):
8661  """Floating-point 16-bit (half) sort."""
8662  ctx = _get_ctx(ctx)
8663  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
8664 
def Float16(ctx=None)
Definition: z3py.py:8660
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 8670 of file z3py.py.

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

8670 def Float32(ctx=None):
8671  """Floating-point 32-bit (single) sort."""
8672  ctx = _get_ctx(ctx)
8673  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
8674 
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:8670

◆ Float64()

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

Definition at line 8680 of file z3py.py.

Referenced by fpFPToFP(), and fpToFP().

8680 def Float64(ctx=None):
8681  """Floating-point 64-bit (double) sort."""
8682  ctx = _get_ctx(ctx)
8683  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
8684 
def Float64(ctx=None)
Definition: z3py.py:8680
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 8685 of file z3py.py.

8685 def FloatDouble(ctx=None):
8686  """Floating-point 64-bit (double) sort."""
8687  ctx = _get_ctx(ctx)
8688  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
8689 
def FloatDouble(ctx=None)
Definition: z3py.py:8685
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 8665 of file z3py.py.

8665 def FloatHalf(ctx=None):
8666  """Floating-point 16-bit (half) sort."""
8667  ctx = _get_ctx(ctx)
8668  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
8669 
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:8665

◆ FloatQuadruple()

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

Definition at line 8695 of file z3py.py.

8695 def FloatQuadruple(ctx=None):
8696  """Floating-point 128-bit (quadruple) sort."""
8697  ctx = _get_ctx(ctx)
8698  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
8699 
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:8695

◆ FloatSingle()

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

Definition at line 8675 of file z3py.py.

8675 def FloatSingle(ctx=None):
8676  """Floating-point 32-bit (single) sort."""
8677  ctx = _get_ctx(ctx)
8678  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
8679 
def FloatSingle(ctx=None)
Definition: z3py.py:8675
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`, `qif`, `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 2017 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().

2017 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2018  """Create a Z3 forall formula.
2019 
2020  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2021 
2022  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2023  >>> x = Int('x')
2024  >>> y = Int('y')
2025  >>> ForAll([x, y], f(x, y) >= x)
2026  ForAll([x, y], f(x, y) >= x)
2027  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2028  ForAll([x, y], f(x, y) >= x)
2029  >>> ForAll([x, y], f(x, y) >= x, weight=10)
2030  ForAll([x, y], f(x, y) >= x)
2031  """
2032  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2033 
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2017

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

9276 def FP(name, fpsort, ctx=None):
9277  """Return a floating-point constant named `name`.
9278  `fpsort` is the floating-point sort.
9279  If `ctx=None`, then the global context is used.
9280 
9281  >>> x = FP('x', FPSort(8, 24))
9282  >>> is_fp(x)
9283  True
9284  >>> x.ebits()
9285  8
9286  >>> x.sort()
9287  FPSort(8, 24)
9288  >>> word = FPSort(8, 24)
9289  >>> x2 = FP('x', word)
9290  >>> eq(x, x2)
9291  True
9292  """
9293  if isinstance(fpsort, FPSortRef) and ctx is None:
9294  ctx = fpsort.ctx
9295  else:
9296  ctx = _get_ctx(ctx)
9297  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
9298 
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:105
def FP(name, fpsort, ctx=None)
Definition: z3py.py:9276

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

9317 def fpAbs(a, ctx=None):
9318  """Create a Z3 floating-point absolute value expression.
9319 
9320  >>> s = FPSort(8, 24)
9321  >>> rm = RNE()
9322  >>> x = FPVal(1.0, s)
9323  >>> fpAbs(x)
9324  fpAbs(1)
9325  >>> y = FPVal(-20.0, s)
9326  >>> y
9327  -1.25*(2**4)
9328  >>> fpAbs(y)
9329  fpAbs(-1.25*(2**4))
9330  >>> fpAbs(-1.25*(2**4))
9331  fpAbs(-1.25*(2**4))
9332  >>> fpAbs(x).sort()
9333  FPSort(8, 24)
9334  """
9335  ctx = _get_ctx(ctx)
9336  [a] = _coerce_fp_expr_list([a], ctx)
9337  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
9338 
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:9317

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

Referenced by FPs().

9406 def fpAdd(rm, a, b, ctx=None):
9407  """Create a Z3 floating-point addition expression.
9408 
9409  >>> s = FPSort(8, 24)
9410  >>> rm = RNE()
9411  >>> x = FP('x', s)
9412  >>> y = FP('y', s)
9413  >>> fpAdd(rm, x, y)
9414  fpAdd(RNE(), x, y)
9415  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
9416  x + y
9417  >>> fpAdd(rm, x, y).sort()
9418  FPSort(8, 24)
9419  """
9420  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
9421 
def fpAdd(rm, a, b, ctx=None)
Definition: z3py.py:9406

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

9703 def fpBVToFP(v, sort, ctx=None):
9704  """Create a Z3 floating-point conversion expression that represents the
9705  conversion from a bit-vector term to a floating-point term.
9706 
9707  >>> x_bv = BitVecVal(0x3F800000, 32)
9708  >>> x_fp = fpBVToFP(x_bv, Float32())
9709  >>> x_fp
9710  fpToFP(1065353216)
9711  >>> simplify(x_fp)
9712  1
9713  """
9714  _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.")
9715  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
9716  ctx = _get_ctx(ctx)
9717  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
9718 
def fpBVToFP(v, sort, ctx=None)
Definition: z3py.py:9703
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:8704
def is_bv(a)
Definition: z3py.py:3656

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

9450 def fpDiv(rm, a, b, ctx=None):
9451  """Create a Z3 floating-point division expression.
9452 
9453  >>> s = FPSort(8, 24)
9454  >>> rm = RNE()
9455  >>> x = FP('x', s)
9456  >>> y = FP('y', s)
9457  >>> fpDiv(rm, x, y)
9458  fpDiv(RNE(), x, y)
9459  >>> fpDiv(rm, x, y).sort()
9460  FPSort(8, 24)
9461  """
9462  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
9463 
def fpDiv(rm, a, b, ctx=None)
Definition: z3py.py:9450

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

Referenced by fpFP(), and fpNEQ().

9615 def fpEQ(a, b, ctx=None):
9616  """Create the Z3 floating-point expression `fpEQ(other, self)`.
9617 
9618  >>> x, y = FPs('x y', FPSort(8, 24))
9619  >>> fpEQ(x, y)
9620  fpEQ(x, y)
9621  >>> fpEQ(x, y).sexpr()
9622  '(fp.eq x y)'
9623  """
9624  return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
9625 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:9615

◆ fpFMA()

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

Definition at line 9505 of file z3py.py.

9505 def fpFMA(rm, a, b, c, ctx=None):
9506  """Create a Z3 floating-point fused multiply-add expression.
9507  """
9508  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
9509 
def fpFMA(rm, a, b, c, ctx=None)
Definition: z3py.py:9505

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

9637 def fpFP(sgn, exp, sig, ctx=None):
9638  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
9639 
9640  >>> s = FPSort(8, 24)
9641  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
9642  >>> print(x)
9643  fpFP(1, 127, 4194304)
9644  >>> xv = FPVal(-1.5, s)
9645  >>> print(xv)
9646  -1.5
9647  >>> slvr = Solver()
9648  >>> slvr.add(fpEQ(x, xv))
9649  >>> slvr.check()
9650  sat
9651  >>> xv = FPVal(+1.5, s)
9652  >>> print(xv)
9653  1.5
9654  >>> slvr = Solver()
9655  >>> slvr.add(fpEQ(x, xv))
9656  >>> slvr.check()
9657  unsat
9658  """
9659  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
9660  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
9661  ctx = _get_ctx(ctx)
9662  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
9663  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
9664 
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:9637
def is_bv(a)
Definition: z3py.py:3656

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

9719 def fpFPToFP(rm, v, sort, ctx=None):
9720  """Create a Z3 floating-point conversion expression that represents the
9721  conversion from a floating-point term to a floating-point term of different precision.
9722 
9723  >>> x_sgl = FPVal(1.0, Float32())
9724  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
9725  >>> x_dbl
9726  fpToFP(RNE(), 1)
9727  >>> simplify(x_dbl)
9728  1
9729  >>> x_dbl.sort()
9730  FPSort(11, 53)
9731  """
9732  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9733  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
9734  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9735  ctx = _get_ctx(ctx)
9736  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9737 
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:8704
def fpFPToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9719
def is_fprm(a)
Definition: z3py.py:8952
def is_fp(a)
Definition: z3py.py:9088

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

9604 def fpGEQ(a, b, ctx=None):
9605  """Create the Z3 floating-point expression `other >= self`.
9606 
9607  >>> x, y = FPs('x y', FPSort(8, 24))
9608  >>> fpGEQ(x, y)
9609  x >= y
9610  >>> (x >= y).sexpr()
9611  '(fp.geq x y)'
9612  """
9613  return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
9614 
def fpGEQ(a, b, ctx=None)
Definition: z3py.py:9604

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

9593 def fpGT(a, b, ctx=None):
9594  """Create the Z3 floating-point expression `other > self`.
9595 
9596  >>> x, y = FPs('x y', FPSort(8, 24))
9597  >>> fpGT(x, y)
9598  x > y
9599  >>> (x > y).sexpr()
9600  '(fp.gt x y)'
9601  """
9602  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
9603 
def fpGT(a, b, ctx=None)
Definition: z3py.py:9593

◆ fpInfinity()

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

Definition at line 9210 of file z3py.py.

9210 def fpInfinity(s, negative):
9211  """Create a Z3 floating-point +oo or -oo term."""
9212  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9213  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9214  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
9215 
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:9210

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

9531 def fpIsInf(a, ctx=None):
9532  """Create a Z3 floating-point isInfinite expression.
9533 
9534  >>> s = FPSort(8, 24)
9535  >>> x = FP('x', s)
9536  >>> fpIsInf(x)
9537  fpIsInf(x)
9538  """
9539  return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx)
9540 
def fpIsInf(a, ctx=None)
Definition: z3py.py:9531

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

9520 def fpIsNaN(a, ctx=None):
9521  """Create a Z3 floating-point isNaN expression.
9522 
9523  >>> s = FPSort(8, 24)
9524  >>> x = FP('x', s)
9525  >>> y = FP('y', s)
9526  >>> fpIsNaN(x)
9527  fpIsNaN(x)
9528  """
9529  return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx)
9530 
def fpIsNaN(a, ctx=None)
Definition: z3py.py:9520

◆ fpIsNegative()

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

Definition at line 9556 of file z3py.py.

9556 def fpIsNegative(a, ctx=None):
9557  """Create a Z3 floating-point isNegative expression.
9558  """
9559  return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx)
9560 
def fpIsNegative(a, ctx=None)
Definition: z3py.py:9556

◆ fpIsNormal()

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

Definition at line 9546 of file z3py.py.

9546 def fpIsNormal(a, ctx=None):
9547  """Create a Z3 floating-point isNormal expression.
9548  """
9549  return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx)
9550 
def fpIsNormal(a, ctx=None)
Definition: z3py.py:9546

◆ fpIsPositive()

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

Definition at line 9561 of file z3py.py.

9561 def fpIsPositive(a, ctx=None):
9562  """Create a Z3 floating-point isPositive expression.
9563  """
9564  return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx)
9565  return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx)
9566 
Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t)
Predicate indicating whether t is a positive floating-point number.
def fpIsPositive(a, ctx=None)
Definition: z3py.py:9561

◆ fpIsSubnormal()

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

Definition at line 9551 of file z3py.py.

9551 def fpIsSubnormal(a, ctx=None):
9552  """Create a Z3 floating-point isSubnormal expression.
9553  """
9554  return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx)
9555 
def fpIsSubnormal(a, ctx=None)
Definition: z3py.py:9551

◆ fpIsZero()

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

Definition at line 9541 of file z3py.py.

9541 def fpIsZero(a, ctx=None):
9542  """Create a Z3 floating-point isZero expression.
9543  """
9544  return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx)
9545 
def fpIsZero(a, ctx=None)
Definition: z3py.py:9541

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

9582 def fpLEQ(a, b, ctx=None):
9583  """Create the Z3 floating-point expression `other <= self`.
9584 
9585  >>> x, y = FPs('x y', FPSort(8, 24))
9586  >>> fpLEQ(x, y)
9587  x <= y
9588  >>> (x <= y).sexpr()
9589  '(fp.leq x y)'
9590  """
9591  return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
9592 
def fpLEQ(a, b, ctx=None)
Definition: z3py.py:9582

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

9571 def fpLT(a, b, ctx=None):
9572  """Create the Z3 floating-point expression `other < self`.
9573 
9574  >>> x, y = FPs('x y', FPSort(8, 24))
9575  >>> fpLT(x, y)
9576  x < y
9577  >>> (x < y).sexpr()
9578  '(fp.lt x y)'
9579  """
9580  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
9581 
def fpLT(a, b, ctx=None)
Definition: z3py.py:9571

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

9491 def fpMax(a, b, ctx=None):
9492  """Create a Z3 floating-point maximum expression.
9493 
9494  >>> s = FPSort(8, 24)
9495  >>> rm = RNE()
9496  >>> x = FP('x', s)
9497  >>> y = FP('y', s)
9498  >>> fpMax(x, y)
9499  fpMax(x, y)
9500  >>> fpMax(x, y).sort()
9501  FPSort(8, 24)
9502  """
9503  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
9504 
def fpMax(a, b, ctx=None)
Definition: z3py.py:9491

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

9477 def fpMin(a, b, ctx=None):
9478  """Create a Z3 floating-point minimum expression.
9479 
9480  >>> s = FPSort(8, 24)
9481  >>> rm = RNE()
9482  >>> x = FP('x', s)
9483  >>> y = FP('y', s)
9484  >>> fpMin(x, y)
9485  fpMin(x, y)
9486  >>> fpMin(x, y).sort()
9487  FPSort(8, 24)
9488  """
9489  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
9490 
def fpMin(a, b, ctx=None)
Definition: z3py.py:9477

◆ fpMinusInfinity()

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

Definition at line 9205 of file z3py.py.

9205 def fpMinusInfinity(s):
9206  """Create a Z3 floating-point -oo term."""
9207  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9208  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9209 
def fpMinusInfinity(s)
Definition: z3py.py:9205
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 9221 of file z3py.py.

9221 def fpMinusZero(s):
9222  """Create a Z3 floating-point -0.0 term."""
9223  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9224  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
9225 
def fpMinusZero(s)
Definition: z3py.py:9221
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 9436 of file z3py.py.

Referenced by FPs().

9436 def fpMul(rm, a, b, ctx=None):
9437  """Create a Z3 floating-point multiplication expression.
9438 
9439  >>> s = FPSort(8, 24)
9440  >>> rm = RNE()
9441  >>> x = FP('x', s)
9442  >>> y = FP('y', s)
9443  >>> fpMul(rm, x, y)
9444  fpMul(RNE(), x, y)
9445  >>> fpMul(rm, x, y).sort()
9446  FPSort(8, 24)
9447  """
9448  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
9449 
def fpMul(rm, a, b, ctx=None)
Definition: z3py.py:9436

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

9173 def fpNaN(s):
9174  """Create a Z3 floating-point NaN term.
9175 
9176  >>> s = FPSort(8, 24)
9177  >>> set_fpa_pretty(True)
9178  >>> fpNaN(s)
9179  NaN
9180  >>> pb = get_fpa_pretty()
9181  >>> set_fpa_pretty(False)
9182  >>> fpNaN(s)
9183  fpNaN(FPSort(8, 24))
9184  >>> set_fpa_pretty(pb)
9185  """
9186  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9187  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9188 
def fpNaN(s)
Definition: z3py.py:9173
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 9339 of file z3py.py.

9339 def fpNeg(a, ctx=None):
9340  """Create a Z3 floating-point addition expression.
9341 
9342  >>> s = FPSort(8, 24)
9343  >>> rm = RNE()
9344  >>> x = FP('x', s)
9345  >>> fpNeg(x)
9346  -x
9347  >>> fpNeg(x).sort()
9348  FPSort(8, 24)
9349  """
9350  ctx = _get_ctx(ctx)
9351  [a] = _coerce_fp_expr_list([a], ctx)
9352  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
9353 
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:9339

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

9626 def fpNEQ(a, b, ctx=None):
9627  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
9628 
9629  >>> x, y = FPs('x y', FPSort(8, 24))
9630  >>> fpNEQ(x, y)
9631  Not(fpEQ(x, y))
9632  >>> (x != y).sexpr()
9633  '(distinct x y)'
9634  """
9635  return Not(fpEQ(a, b, ctx))
9636 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:9615
def Not(a, ctx=None)
Definition: z3py.py:1631
def fpNEQ(a, b, ctx=None)
Definition: z3py.py:9626

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

9189 def fpPlusInfinity(s):
9190  """Create a Z3 floating-point +oo term.
9191 
9192  >>> s = FPSort(8, 24)
9193  >>> pb = get_fpa_pretty()
9194  >>> set_fpa_pretty(True)
9195  >>> fpPlusInfinity(s)
9196  +oo
9197  >>> set_fpa_pretty(False)
9198  >>> fpPlusInfinity(s)
9199  fpPlusInfinity(FPSort(8, 24))
9200  >>> set_fpa_pretty(pb)
9201  """
9202  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9203  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9204 
def fpPlusInfinity(s)
Definition: z3py.py:9189
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 9216 of file z3py.py.

9216 def fpPlusZero(s):
9217  """Create a Z3 floating-point +0.0 term."""
9218  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9219  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
9220 
def fpPlusZero(s)
Definition: z3py.py:9216
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 9738 of file z3py.py.

9738 def fpRealToFP(rm, v, sort, ctx=None):
9739  """Create a Z3 floating-point conversion expression that represents the
9740  conversion from a real term to a floating-point term.
9741 
9742  >>> x_r = RealVal(1.5)
9743  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
9744  >>> x_fp
9745  fpToFP(RNE(), 3/2)
9746  >>> simplify(x_fp)
9747  1.5
9748  """
9749  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9750  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
9751  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9752  ctx = _get_ctx(ctx)
9753  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9754 
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:2488
def is_fp_sort(s)
Definition: z3py.py:8704
def fpRealToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9738
def is_fprm(a)
Definition: z3py.py:8952

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

9464 def fpRem(a, b, ctx=None):
9465  """Create a Z3 floating-point remainder expression.
9466 
9467  >>> s = FPSort(8, 24)
9468  >>> x = FP('x', s)
9469  >>> y = FP('y', s)
9470  >>> fpRem(x, y)
9471  fpRem(x, y)
9472  >>> fpRem(x, y).sort()
9473  FPSort(8, 24)
9474  """
9475  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
9476 
def fpRem(a, b, ctx=None)
Definition: z3py.py:9464

◆ fpRoundToIntegral()

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

Definition at line 9515 of file z3py.py.

9515 def fpRoundToIntegral(rm, a, ctx=None):
9516  """Create a Z3 floating-point roundToIntegral expression.
9517  """
9518  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
9519 
def fpRoundToIntegral(rm, a, ctx=None)
Definition: z3py.py:9515

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

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

9299 def FPs(names, fpsort, ctx=None):
9300  """Return an array of floating-point constants.
9301 
9302  >>> x, y, z = FPs('x y z', FPSort(8, 24))
9303  >>> x.sort()
9304  FPSort(8, 24)
9305  >>> x.sbits()
9306  24
9307  >>> x.ebits()
9308  8
9309  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9310  fpMul(RNE(), fpAdd(RNE(), x, y), z)
9311  """
9312  ctx = _get_ctx(ctx)
9313  if isinstance(names, str):
9314  names = names.split(" ")
9315  return [FP(name, fpsort, ctx) for name in names]
9316 
def FPs(names, fpsort, ctx=None)
Definition: z3py.py:9299
def FP(name, fpsort, ctx=None)
Definition: z3py.py:9276

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

9755 def fpSignedToFP(rm, v, sort, ctx=None):
9756  """Create a Z3 floating-point conversion expression that represents the
9757  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
9758 
9759  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9760  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
9761  >>> x_fp
9762  fpToFP(RNE(), 4294967291)
9763  >>> simplify(x_fp)
9764  -1.25*(2**2)
9765  """
9766  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9767  _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.")
9768  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9769  ctx = _get_ctx(ctx)
9770  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9771 
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:9755
def is_fp_sort(s)
Definition: z3py.py:8704
def is_bv(a)
Definition: z3py.py:3656
def is_fprm(a)
Definition: z3py.py:8952

◆ 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 9115 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(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), and FPRef.sort().

9115 def FPSort(ebits, sbits, ctx=None):
9116  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9117 
9118  >>> Single = FPSort(8, 24)
9119  >>> Double = FPSort(11, 53)
9120  >>> Single
9121  FPSort(8, 24)
9122  >>> x = Const('x', Single)
9123  >>> eq(x, FP('x', FPSort(8, 24)))
9124  True
9125  """
9126  ctx = _get_ctx(ctx)
9127  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9128 
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:9115

◆ fpSqrt()

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

Definition at line 9510 of file z3py.py.

9510 def fpSqrt(rm, a, ctx=None):
9511  """Create a Z3 floating-point square root expression.
9512  """
9513  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
9514 
def fpSqrt(rm, a, ctx=None)
Definition: z3py.py:9510

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

9422 def fpSub(rm, a, b, ctx=None):
9423  """Create a Z3 floating-point subtraction expression.
9424 
9425  >>> s = FPSort(8, 24)
9426  >>> rm = RNE()
9427  >>> x = FP('x', s)
9428  >>> y = FP('y', s)
9429  >>> fpSub(rm, x, y)
9430  fpSub(RNE(), x, y)
9431  >>> fpSub(rm, x, y).sort()
9432  FPSort(8, 24)
9433  """
9434  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
9435 
def fpSub(rm, a, b, ctx=None)
Definition: z3py.py:9422

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

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

9665 def fpToFP(a1, a2=None, a3=None, ctx=None):
9666  """Create a Z3 floating-point conversion expression from other term sorts
9667  to floating-point.
9668 
9669  From a bit-vector term in IEEE 754-2008 format:
9670  >>> x = FPVal(1.0, Float32())
9671  >>> x_bv = fpToIEEEBV(x)
9672  >>> simplify(fpToFP(x_bv, Float32()))
9673  1
9674 
9675  From a floating-point term with different precision:
9676  >>> x = FPVal(1.0, Float32())
9677  >>> x_db = fpToFP(RNE(), x, Float64())
9678  >>> x_db.sort()
9679  FPSort(11, 53)
9680 
9681  From a real term:
9682  >>> x_r = RealVal(1.5)
9683  >>> simplify(fpToFP(RNE(), x_r, Float32()))
9684  1.5
9685 
9686  From a signed bit-vector term:
9687  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9688  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
9689  -1.25*(2**2)
9690  """
9691  ctx = _get_ctx(ctx)
9692  if is_bv(a1) and is_fp_sort(a2):
9693  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
9694  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
9695  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9696  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
9697  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9698  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
9699  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
9700  else:
9701  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
9702 
def fpToFP(a1, a2=None, a3=None, ctx=None)
Definition: z3py.py:9665
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:2488
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:8704
def is_bv(a)
Definition: z3py.py:3656
def is_fprm(a)
Definition: z3py.py:8952
def is_fp(a)
Definition: z3py.py:9088

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

Referenced by fpUnsignedToFP().

9789 def fpToFPUnsigned(rm, x, s, ctx=None):
9790  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
9791  if __debug__:
9792  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9793  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
9794  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
9795  ctx = _get_ctx(ctx)
9796  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
9797 
def fpToFPUnsigned(rm, x, s, ctx=None)
Definition: z3py.py:9789
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:8704
def is_bv(a)
Definition: z3py.py:3656
def is_fprm(a)
Definition: z3py.py:8952

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

Referenced by fpToFP().

9859 def fpToIEEEBV(x, ctx=None):
9860  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
9861 
9862  The size of the resulting bit-vector is automatically determined.
9863 
9864  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9865  knows only one NaN and it will always produce the same bit-vector representation of
9866  that NaN.
9867 
9868  >>> x = FP('x', FPSort(8, 24))
9869  >>> y = fpToIEEEBV(x)
9870  >>> print(is_fp(x))
9871  True
9872  >>> print(is_bv(y))
9873  True
9874  >>> print(is_fp(y))
9875  False
9876  >>> print(is_bv(x))
9877  False
9878  """
9879  if __debug__:
9880  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
9881  ctx = _get_ctx(ctx)
9882  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
9883 
9884 
9885 
def fpToIEEEBV(x, ctx=None)
Definition: z3py.py:9859
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 is_fp(a)
Definition: z3py.py:9088

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

9840 def fpToReal(x, ctx=None):
9841  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
9842 
9843  >>> x = FP('x', FPSort(8, 24))
9844  >>> y = fpToReal(x)
9845  >>> print(is_fp(x))
9846  True
9847  >>> print(is_real(y))
9848  True
9849  >>> print(is_fp(y))
9850  False
9851  >>> print(is_real(x))
9852  False
9853  """
9854  if __debug__:
9855  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
9856  ctx = _get_ctx(ctx)
9857  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
9858 
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 fpToReal(x, ctx=None)
Definition: z3py.py:9840
def is_fp(a)
Definition: z3py.py:9088

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

9798 def fpToSBV(rm, x, s, ctx=None):
9799  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
9800 
9801  >>> x = FP('x', FPSort(8, 24))
9802  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
9803  >>> print(is_fp(x))
9804  True
9805  >>> print(is_bv(y))
9806  True
9807  >>> print(is_fp(y))
9808  False
9809  >>> print(is_bv(x))
9810  False
9811  """
9812  if __debug__:
9813  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9814  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
9815  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
9816  ctx = _get_ctx(ctx)
9817  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
9818 
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:9798
def is_bv_sort(s)
Definition: z3py.py:3195
def is_fprm(a)
Definition: z3py.py:8952
def is_fp(a)
Definition: z3py.py:9088

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

9819 def fpToUBV(rm, x, s, ctx=None):
9820  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
9821 
9822  >>> x = FP('x', FPSort(8, 24))
9823  >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
9824  >>> print(is_fp(x))
9825  True
9826  >>> print(is_bv(y))
9827  True
9828  >>> print(is_fp(y))
9829  False
9830  >>> print(is_bv(x))
9831  False
9832  """
9833  if __debug__:
9834  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
9835  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
9836  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
9837  ctx = _get_ctx(ctx)
9838  return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
9839 
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:9819
def is_bv_sort(s)
Definition: z3py.py:3195
def is_fprm(a)
Definition: z3py.py:8952
def is_fp(a)
Definition: z3py.py:9088

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

9772 def fpUnsignedToFP(rm, v, sort, ctx=None):
9773  """Create a Z3 floating-point conversion expression that represents the
9774  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9775 
9776  >>> x_signed = BitVecVal(-5, BitVecSort(32))
9777  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
9778  >>> x_fp
9779  fpToFPUnsigned(RNE(), 4294967291)
9780  >>> simplify(x_fp)
9781  1*(2**32)
9782  """
9783  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
9784  _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.")
9785  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
9786  ctx = _get_ctx(ctx)
9787  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
9788 
def fpUnsignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:9772
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:8704
def is_bv(a)
Definition: z3py.py:3656
def is_fprm(a)
Definition: z3py.py:8952

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

9232 def FPVal(sig, exp=None, fps=None, ctx=None):
9233  """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
9234 
9235  >>> v = FPVal(20.0, FPSort(8, 24))
9236  >>> v
9237  1.25*(2**4)
9238  >>> print("0x%.8x" % v.exponent_as_long(False))
9239  0x00000004
9240  >>> v = FPVal(2.25, FPSort(8, 24))
9241  >>> v
9242  1.125*(2**1)
9243  >>> v = FPVal(-2.25, FPSort(8, 24))
9244  >>> v
9245  -1.125*(2**1)
9246  >>> FPVal(-0.0, FPSort(8, 24))
9247  -0.0
9248  >>> FPVal(0.0, FPSort(8, 24))
9249  +0.0
9250  >>> FPVal(+0.0, FPSort(8, 24))
9251  +0.0
9252  """
9253  ctx = _get_ctx(ctx)
9254  if is_fp_sort(exp):
9255  fps = exp
9256  exp = None
9257  elif fps is None:
9258  fps = _dflt_fps(ctx)
9259  _z3_assert(is_fp_sort(fps), "sort mismatch")
9260  if exp is None:
9261  exp = 0
9262  val = _to_float_str(sig)
9263  if val == "NaN" or val == "nan":
9264  return fpNaN(fps)
9265  elif val == "-0.0":
9266  return fpMinusZero(fps)
9267  elif val == "0.0" or val == "+0.0":
9268  return fpPlusZero(fps)
9269  elif val == "+oo" or val == "+inf" or val == "+Inf":
9270  return fpPlusInfinity(fps)
9271  elif val == "-oo" or val == "-inf" or val == "-Inf":
9272  return fpMinusInfinity(fps)
9273  else:
9274  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
9275 
def FPVal(sig, exp=None, fps=None, ctx=None)
Definition: z3py.py:9232
def fpMinusInfinity(s)
Definition: z3py.py:9205
def fpMinusZero(s)
Definition: z3py.py:9221
def fpPlusZero(s)
Definition: z3py.py:9216
def fpPlusInfinity(s)
Definition: z3py.py:9189
def fpNaN(s)
Definition: z3py.py:9173
def is_fp_sort(s)
Definition: z3py.py:8704
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 9226 of file z3py.py.

9226 def fpZero(s, negative):
9227  """Create a Z3 floating-point +0.0 or -0.0 term."""
9228  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9229  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9230  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
9231 
def fpZero(s, negative)
Definition: z3py.py:9226
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 1588 of file z3py.py.

1588 def FreshBool(prefix='b', ctx=None):
1589  """Return a fresh Boolean constant in the given context using the given prefix.
1590 
1591  If `ctx=None`, then the global context is used.
1592 
1593  >>> b1 = FreshBool()
1594  >>> b2 = FreshBool()
1595  >>> eq(b1, b2)
1596  False
1597  """
1598  ctx = _get_ctx(ctx)
1599  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1600 
def FreshBool(prefix='b', ctx=None)
Definition: z3py.py:1588
def BoolSort(ctx=None)
Definition: z3py.py:1513
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 1306 of file z3py.py.

1306 def FreshConst(sort, prefix='c'):
1307  """Create a fresh constant of a specified sort"""
1308  ctx = _get_ctx(sort.ctx)
1309  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1310 
def FreshConst(sort, prefix='c')
Definition: z3py.py:1306
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshInt()

def z3py.FreshInt (   prefix = 'x',
  ctx = None 
)
Return a fresh integer constant in the given context using the given prefix.

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

Definition at line 3018 of file z3py.py.

3018 def FreshInt(prefix='x', ctx=None):
3019  """Return a fresh integer constant in the given context using the given prefix.
3020 
3021  >>> x = FreshInt()
3022  >>> y = FreshInt()
3023  >>> eq(x, y)
3024  False
3025  >>> x.sort()
3026  Int
3027  """
3028  ctx = _get_ctx(ctx)
3029  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3030 
def IntSort(ctx=None)
Definition: z3py.py:2880
def FreshInt(prefix='x', ctx=None)
Definition: z3py.py:3018
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 3070 of file z3py.py.

3070 def FreshReal(prefix='b', ctx=None):
3071  """Return a fresh real constant in the given context using the given prefix.
3072 
3073  >>> x = FreshReal()
3074  >>> y = FreshReal()
3075  >>> eq(x, y)
3076  False
3077  >>> x.sort()
3078  Real
3079  """
3080  ctx = _get_ctx(ctx)
3081  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3082 
def FreshReal(prefix='b', ctx=None)
Definition: z3py.py:3070
def RealSort(ctx=None)
Definition: z3py.py:2896
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)
re.all
>>> e1 = Full(ReSort(StringSort()))
>>> print(e1)
re.all

Definition at line 10047 of file z3py.py.

10047 def Full(s):
10048  """Create the regular expression that accepts the universal language
10049  >>> e = Full(ReSort(SeqSort(IntSort())))
10050  >>> print(e)
10051  re.all
10052  >>> e1 = Full(ReSort(StringSort()))
10053  >>> print(e1)
10054  re.all
10055  """
10056  if isinstance(s, ReSortRef):
10057  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10058  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10059 
10060 
def Full(s)
Definition: z3py.py:10047
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 4545 of file z3py.py.

4545 def FullSet(s):
4546  """Create the full set
4547  >>> FullSet(IntSort())
4548  K(Int, True)
4549  """
4550  ctx = s.ctx
4551  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4552 
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
def FullSet(s)
Definition: z3py.py:4545

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

779 def Function(name, *sig):
780  """Create a new Z3 uninterpreted function with the given sorts.
781 
782  >>> f = Function('f', IntSort(), IntSort())
783  >>> f(f(0))
784  f(f(0))
785  """
786  sig = _get_args(sig)
787  if __debug__:
788  _z3_assert(len(sig) > 0, "At least two arguments expected")
789  arity = len(sig) - 1
790  rng = sig[arity]
791  if __debug__:
792  _z3_assert(is_sort(rng), "Z3 sort expected")
793  dom = (Sort * arity)()
794  for i in range(arity):
795  if __debug__:
796  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
797  dom[i] = sig[i].ast
798  ctx = rng.ctx
799  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
800 
def Function(name, sig)
Definition: z3py.py:779
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3286
def to_symbol(s, ctx=None)
Definition: z3py.py:105
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:580

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

6186 def get_as_array_func(n):
6187  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6188  if __debug__:
6189  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6190  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6191 
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:6186
def is_as_array(n)
Definition: z3py.py:6182

◆ get_default_fp_sort()

def z3py.get_default_fp_sort (   ctx = None)

Definition at line 8584 of file z3py.py.

8584 def get_default_fp_sort(ctx=None):
8585  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
8586 
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9115
def get_default_fp_sort(ctx=None)
Definition: z3py.py:8584

◆ get_default_rounding_mode()

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

Definition at line 8557 of file z3py.py.

8557 def get_default_rounding_mode(ctx=None):
8558  """Retrieves the global default rounding mode."""
8559  global _dflt_rounding_mode
8560  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
8561  return RTZ(ctx)
8562  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
8563  return RTN(ctx)
8564  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
8565  return RTP(ctx)
8566  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
8567  return RNE(ctx)
8568  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
8569  return RNA(ctx)
8570 
def RTN(ctx=None)
Definition: z3py.py:8940
def RTZ(ctx=None)
Definition: z3py.py:8948
def RTP(ctx=None)
Definition: z3py.py:8932
def RNA(ctx=None)
Definition: z3py.py:8924
def get_default_rounding_mode(ctx=None)
Definition: z3py.py:8557
def RNE(ctx=None)
Definition: z3py.py:8916

◆ get_full_version()

def z3py.get_full_version ( )

Definition at line 85 of file z3py.py.

85 def get_full_version():
86  return Z3_get_full_version()
87 
88 # We use _z3_assert instead of the assert command because we want to
89 # 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:85

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

4324 def get_map_func(a):
4325  """Return the function declaration associated with a Z3 map array expression.
4326 
4327  >>> f = Function('f', IntSort(), IntSort())
4328  >>> b = Array('b', IntSort(), IntSort())
4329  >>> a = Map(f, b)
4330  >>> eq(f, get_map_func(a))
4331  True
4332  >>> get_map_func(a)
4333  f
4334  >>> get_map_func(a)(0)
4335  f(0)
4336  """
4337  if __debug__:
4338  _z3_assert(is_map(a), "Z3 array map expression expected.")
4339  return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
4340 
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:4301
def get_map_func(a)
Definition: z3py.py:4324
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.

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

266 def get_param(name):
267  """Return the value of a Z3 global (or module) parameter
268 
269  >>> get_param('nlsat.reorder')
270  'true'
271  """
272  ptr = (ctypes.c_char_p * 1)()
273  if Z3_global_param_get(str(name), ptr):
274  r = z3core._to_pystr(ptr[0])
275  return r
276  raise Z3Exception("failed to retrieve value for '%s'" % name)
277 
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:266

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

1184 def get_var_index(a):
1185  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1186 
1187  >>> x = Int('x')
1188  >>> y = Int('y')
1189  >>> is_var(x)
1190  False
1191  >>> is_const(x)
1192  True
1193  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1194  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1195  >>> q = ForAll([x, y], f(x, y) == x + y)
1196  >>> q.body()
1197  f(Var(1), Var(0)) == Var(1) + Var(0)
1198  >>> b = q.body()
1199  >>> b.arg(0)
1200  f(Var(1), Var(0))
1201  >>> v1 = b.arg(0).arg(0)
1202  >>> v2 = b.arg(0).arg(1)
1203  >>> v1
1204  Var(1)
1205  >>> v2
1206  Var(0)
1207  >>> get_var_index(v1)
1208  1
1209  >>> get_var_index(v2)
1210  0
1211  """
1212  if __debug__:
1213  _z3_assert(is_var(a), "Z3 bound variable expected")
1214  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1215 
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
def get_var_index(a)
Definition: z3py.py:1184
def is_var(a)
Definition: z3py.py:1160

◆ get_version()

def z3py.get_version ( )

Definition at line 77 of file z3py.py.

77 def get_version():
78  major = ctypes.c_uint(0)
79  minor = ctypes.c_uint(0)
80  build = ctypes.c_uint(0)
81  rev = ctypes.c_uint(0)
82  Z3_get_version(major, minor, build, rev)
83  return (major.value, minor.value, build.value, rev.value)
84 
def get_version()
Definition: z3py.py:77
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 69 of file z3py.py.

69 def get_version_string():
70  major = ctypes.c_uint(0)
71  minor = ctypes.c_uint(0)
72  build = ctypes.c_uint(0)
73  rev = ctypes.c_uint(0)
74  Z3_get_version(major, minor, build, rev)
75  return "%s.%s.%s" % (major.value, minor.value, build.value)
76 
def get_version_string()
Definition: z3py.py:69
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 8143 of file z3py.py.

8143 def help_simplify():
8144  """Return a string describing all options available for Z3 `simplify` procedure."""
8145  print(Z3_simplify_get_help(main_ctx().ref()))
8146 
def main_ctx()
Definition: z3py.py:207
def help_simplify()
Definition: z3py.py:8143
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 1228 of file z3py.py.

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

1228 def If(a, b, c, ctx=None):
1229  """Create a Z3 if-then-else expression.
1230 
1231  >>> x = Int('x')
1232  >>> y = Int('y')
1233  >>> max = If(x > y, x, y)
1234  >>> max
1235  If(x > y, x, y)
1236  >>> simplify(max)
1237  If(x <= y, y, x)
1238  """
1239  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1240  return Cond(a, b, c, ctx)
1241  else:
1242  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1243  s = BoolSort(ctx)
1244  a = s.cast(a)
1245  b, c = _coerce_exprs(b, c, ctx)
1246  if __debug__:
1247  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1248  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1249 
def If(a, b, c, ctx=None)
Definition: z3py.py:1228
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8103
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:1513

◆ Implies()

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

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

Definition at line 1601 of file z3py.py.

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

1601 def Implies(a, b, ctx=None):
1602  """Create a Z3 implies expression.
1603 
1604  >>> p, q = Bools('p q')
1605  >>> Implies(p, q)
1606  Implies(p, q)
1607  >>> simplify(Implies(p, q))
1608  Or(Not(p), q)
1609  """
1610  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1611  s = BoolSort(ctx)
1612  a = s.cast(a)
1613  b = s.cast(b)
1614  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1615 
def Implies(a, b, ctx=None)
Definition: z3py.py:1601
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:1513

◆ IndexOf() [1/2]

def z3py.IndexOf (   s,
  substr 
)

Definition at line 10126 of file z3py.py.

Referenced by IndexOf().

10126 def IndexOf(s, substr):
10127  return IndexOf(s, substr, IntVal(0))
10128 
def IntVal(val, ctx=None)
Definition: z3py.py:2927
def IndexOf(s, substr)
Definition: z3py.py:10126

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

10129 def IndexOf(s, substr, offset):
10130  """Retrieve the index of substring within a string starting at a specified offset.
10131  >>> simplify(IndexOf("abcabc", "bc", 0))
10132  1
10133  >>> simplify(IndexOf("abcabc", "bc", 2))
10134  4
10135  """
10136  ctx = None
10137  if is_expr(offset):
10138  ctx = offset.ctx
10139  ctx = _get_ctx2(s, substr, ctx)
10140  s = _coerce_seq(s, ctx)
10141  substr = _coerce_seq(substr, ctx)
10142  if _is_int(offset):
10143  offset = IntVal(offset, ctx)
10144  return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
10145 
def IntVal(val, ctx=None)
Definition: z3py.py:2927
def IndexOf(s, substr)
Definition: z3py.py:10126
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:1095

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

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

10216 def InRe(s, re):
10217  """Create regular expression membership test
10218  >>> re = Union(Re("a"),Re("b"))
10219  >>> print (simplify(InRe("a", re)))
10220  True
10221  >>> print (simplify(InRe("b", re)))
10222  True
10223  >>> print (simplify(InRe("c", re)))
10224  False
10225  """
10226  s = _coerce_seq(s, re.ctx)
10227  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
10228 
def InRe(s, re)
Definition: z3py.py:10216
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 2983 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().

2983 def Int(name, ctx=None):
2984  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
2985 
2986  >>> x = Int('x')
2987  >>> is_int(x)
2988  True
2989  >>> is_int(x + 1)
2990  True
2991  """
2992  ctx = _get_ctx(ctx)
2993  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
2994 
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:105
def Int(name, ctx=None)
Definition: z3py.py:2983
def IntSort(ctx=None)
Definition: z3py.py:2880

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

3705 def Int2BV(a, num_bits):
3706  """Return the z3 expression Int2BV(a, num_bits).
3707  It is a bit-vector of width num_bits and represents the
3708  modulo of a by 2^num_bits
3709  """
3710  ctx = a.ctx
3711  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
3712 
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:3705

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

2995 def Ints(names, ctx=None):
2996  """Return a tuple of Integer constants.
2997 
2998  >>> x, y, z = Ints('x y z')
2999  >>> Sum(x, y, z)
3000  x + y + z
3001  """
3002  ctx = _get_ctx(ctx)
3003  if isinstance(names, str):
3004  names = names.split(" ")
3005  return [Int(name, ctx) for name in names]
3006 
def Int(name, ctx=None)
Definition: z3py.py:2983
def Ints(names, ctx=None)
Definition: z3py.py:2995

◆ 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 2880 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(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), Full(), FullSet(), ModelRef.get_interp(), get_map_func(), 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(), 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(), Update(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

2880 def IntSort(ctx=None):
2881  """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
2882 
2883  >>> IntSort()
2884  Int
2885  >>> x = Const('x', IntSort())
2886  >>> is_int(x)
2887  True
2888  >>> x.sort() == IntSort()
2889  True
2890  >>> x.sort() == BoolSort()
2891  False
2892  """
2893  ctx = _get_ctx(ctx)
2894  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
2895 
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
def IntSort(ctx=None)
Definition: z3py.py:2880

◆ IntToStr()

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

Definition at line 10171 of file z3py.py.

Referenced by StrToInt().

10171 def IntToStr(s):
10172  """Convert integer expression to string"""
10173  if not is_expr(s):
10174  s = _py2expr(s)
10175  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
10176 
10177 
def IntToStr(s)
Definition: z3py.py:10171
def is_expr(a)
Definition: z3py.py:1095
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 2927 of file z3py.py.

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

2927 def IntVal(val, ctx=None):
2928  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
2929 
2930  >>> IntVal(1)
2931  1
2932  >>> IntVal("100")
2933  100
2934  """
2935  ctx = _get_ctx(ctx)
2936  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
2937 
def IntVal(val, ctx=None)
Definition: z3py.py:2927
def IntSort(ctx=None)
Definition: z3py.py:2880
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 3007 of file z3py.py.

3007 def IntVector(prefix, sz, ctx=None):
3008  """Return a list of integer constants of size `sz`.
3009 
3010  >>> X = IntVector('x', 3)
3011  >>> X
3012  [x__0, x__1, x__2]
3013  >>> Sum(X)
3014  x__0 + x__1 + x__2
3015  """
3016  return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
3017 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3286
def Int(name, ctx=None)
Definition: z3py.py:2983
def IntVector(prefix, sz, ctx=None)
Definition: z3py.py:3007

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

2569 def is_add(a):
2570  """Return `True` if `a` is an expression of the form b + c.
2571 
2572  >>> x, y = Ints('x y')
2573  >>> is_add(x + y)
2574  True
2575  >>> is_add(x - y)
2576  False
2577  """
2578  return is_app_of(a, Z3_OP_ADD)
2579 
def is_app_of(a, k)
Definition: z3py.py:1216
def is_add(a)
Definition: z3py.py:2569

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

2556 def is_algebraic_value(a):
2557  """Return `True` if `a` is an algebraic value of sort Real.
2558 
2559  >>> is_algebraic_value(RealVal("3/5"))
2560  False
2561  >>> n = simplify(Sqrt(2))
2562  >>> n
2563  1.4142135623?
2564  >>> is_algebraic_value(n)
2565  True
2566  """
2567  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2568 
def is_arith(a)
Definition: z3py.py:2450
def is_algebraic_value(a)
Definition: z3py.py:2556

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

1449 def is_and(a):
1450  """Return `True` if `a` is a Z3 and expression.
1451 
1452  >>> p, q = Bools('p q')
1453  >>> is_and(And(p, q))
1454  True
1455  >>> is_and(Or(p, q))
1456  False
1457  """
1458  return is_app_of(a, Z3_OP_AND)
1459 
def is_and(a)
Definition: z3py.py:1449
def is_app_of(a, k)
Definition: z3py.py:1216

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

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

1117 def is_app(a):
1118  """Return `True` if `a` is a Z3 function application.
1119 
1120  Note that, constants are function applications with 0 arguments.
1121 
1122  >>> a = Int('a')
1123  >>> is_app(a)
1124  True
1125  >>> is_app(a + 1)
1126  True
1127  >>> is_app(IntSort())
1128  False
1129  >>> is_app(1)
1130  False
1131  >>> is_app(IntVal(1))
1132  True
1133  >>> x = Int('x')
1134  >>> is_app(ForAll(x, x >= 0))
1135  False
1136  """
1137  if not isinstance(a, ExprRef):
1138  return False
1139  k = _ast_kind(a.ctx, a)
1140  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
1141 
def is_app(a)
Definition: z3py.py:1117

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

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

1216 def is_app_of(a, k):
1217  """Return `True` if `a` is an application of the given kind `k`.
1218 
1219  >>> x = Int('x')
1220  >>> n = x + 1
1221  >>> is_app_of(n, Z3_OP_ADD)
1222  True
1223  >>> is_app_of(n, Z3_OP_MUL)
1224  False
1225  """
1226  return is_app(a) and a.decl().kind() == k
1227 
def is_app(a)
Definition: z3py.py:1117
def is_app_of(a, k)
Definition: z3py.py:1216

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

2450 def is_arith(a):
2451  """Return `True` if `a` is an arithmetical expression.
2452 
2453  >>> x = Int('x')
2454  >>> is_arith(x)
2455  True
2456  >>> is_arith(x + 1)
2457  True
2458  >>> is_arith(1)
2459  False
2460  >>> is_arith(IntVal(1))
2461  True
2462  >>> y = Real('y')
2463  >>> is_arith(y)
2464  True
2465  >>> is_arith(y + 1)
2466  True
2467  """
2468  return isinstance(a, ArithRef)
2469 
def is_arith(a)
Definition: z3py.py:2450

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

2151 def is_arith_sort(s):
2152  """Return `True` if s is an arithmetical sort (type).
2153 
2154  >>> is_arith_sort(IntSort())
2155  True
2156  >>> is_arith_sort(RealSort())
2157  True
2158  >>> is_arith_sort(BoolSort())
2159  False
2160  >>> n = Int('x') + 1
2161  >>> is_arith_sort(n.sort())
2162  True
2163  """
2164  return isinstance(s, ArithSortRef)
2165 
def is_arith_sort(s)
Definition: z3py.py:2151

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

4264 def is_array(a):
4265  """Return `True` if `a` is a Z3 array expression.
4266 
4267  >>> a = Array('a', IntSort(), IntSort())
4268  >>> is_array(a)
4269  True
4270  >>> is_array(Store(a, 0, 1))
4271  True
4272  >>> is_array(a[0])
4273  False
4274  """
4275  return isinstance(a, ArrayRef)
4276 
def is_array(a)
Definition: z3py.py:4264

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

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

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

396 def is_ast(a):
397  """Return `True` if `a` is an AST node.
398 
399  >>> is_ast(10)
400  False
401  >>> is_ast(IntVal(10))
402  True
403  >>> is_ast(Int('x'))
404  True
405  >>> is_ast(BoolSort())
406  True
407  >>> is_ast(Function('f', IntSort(), IntSort()))
408  True
409  >>> is_ast("x")
410  False
411  >>> is_ast(Solver())
412  False
413  """
414  return isinstance(a, AstRef)
415 
def is_ast(a)
Definition: z3py.py:396

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

Referenced by BoolSort(), and prove().

1402 def is_bool(a):
1403  """Return `True` if `a` is a Z3 Boolean expression.
1404 
1405  >>> p = Bool('p')
1406  >>> is_bool(p)
1407  True
1408  >>> q = Bool('q')
1409  >>> is_bool(And(p, q))
1410  True
1411  >>> x = Real('x')
1412  >>> is_bool(x)
1413  False
1414  >>> is_bool(x == 0)
1415  True
1416  """
1417  return isinstance(a, BoolRef)
1418 
def is_bool(a)
Definition: z3py.py:1402

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

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

3656 def is_bv(a):
3657  """Return `True` if `a` is a Z3 bit-vector expression.
3658 
3659  >>> b = BitVec('b', 32)
3660  >>> is_bv(b)
3661  True
3662  >>> is_bv(b + 10)
3663  True
3664  >>> is_bv(Int('x'))
3665  False
3666  """
3667  return isinstance(a, BitVecRef)
3668 
def is_bv(a)
Definition: z3py.py:3656

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

3195 def is_bv_sort(s):
3196  """Return True if `s` is a Z3 bit-vector sort.
3197 
3198  >>> is_bv_sort(BitVecSort(32))
3199  True
3200  >>> is_bv_sort(IntSort())
3201  False
3202  """
3203  return isinstance(s, BitVecSortRef)
3204 
def is_bv_sort(s)
Definition: z3py.py:3195

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

3669 def is_bv_value(a):
3670  """Return `True` if `a` is a Z3 bit-vector numeral value.
3671 
3672  >>> b = BitVec('b', 32)
3673  >>> is_bv_value(b)
3674  False
3675  >>> b = BitVecVal(10, 32)
3676  >>> b
3677  10
3678  >>> is_bv_value(b)
3679  True
3680  """
3681  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3682 
def is_bv_value(a)
Definition: z3py.py:3669
def is_bv(a)
Definition: z3py.py:3656

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

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

1142 def is_const(a):
1143  """Return `True` if `a` is Z3 constant/variable expression.
1144 
1145  >>> a = Int('a')
1146  >>> is_const(a)
1147  True
1148  >>> is_const(a + 1)
1149  False
1150  >>> is_const(1)
1151  False
1152  >>> is_const(IntVal(1))
1153  True
1154  >>> x = Int('x')
1155  >>> is_const(ForAll(x, x >= 0))
1156  False
1157  """
1158  return is_app(a) and a.num_args() == 0
1159 
def is_app(a)
Definition: z3py.py:1117
def is_const(a)
Definition: z3py.py:1142

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

4277 def is_const_array(a):
4278  """Return `True` if `a` is a Z3 constant array.
4279 
4280  >>> a = K(IntSort(), 10)
4281  >>> is_const_array(a)
4282  True
4283  >>> a = Array('a', IntSort(), IntSort())
4284  >>> is_const_array(a)
4285  False
4286  """
4287  return is_app_of(a, Z3_OP_CONST_ARRAY)
4288 
def is_const_array(a)
Definition: z3py.py:4277
def is_app_of(a, k)
Definition: z3py.py:1216

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

4316 def is_default(a):
4317  """Return `True` if `a` is a Z3 default array expression.
4318  >>> d = Default(K(IntSort(), 10))
4319  >>> is_default(d)
4320  True
4321  """
4322  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4323 
def is_default(a)
Definition: z3py.py:4316
def is_app_of(a, k)
Definition: z3py.py:1216

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

1502 def is_distinct(a):
1503  """Return `True` if `a` is a Z3 distinct expression.
1504 
1505  >>> x, y, z = Ints('x y z')
1506  >>> is_distinct(x == y)
1507  False
1508  >>> is_distinct(Distinct(x, y, z))
1509  True
1510  """
1511  return is_app_of(a, Z3_OP_DISTINCT)
1512 
def is_distinct(a)
Definition: z3py.py:1502
def is_app_of(a, k)
Definition: z3py.py:1216

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

2602 def is_div(a):
2603  """Return `True` if `a` is an expression of the form b / c.
2604 
2605  >>> x, y = Reals('x y')
2606  >>> is_div(x / y)
2607  True
2608  >>> is_div(x + y)
2609  False
2610  >>> x, y = Ints('x y')
2611  >>> is_div(x / y)
2612  False
2613  >>> is_idiv(x / y)
2614  True
2615  """
2616  return is_app_of(a, Z3_OP_DIV)
2617 
def is_div(a)
Definition: z3py.py:2602
def is_app_of(a, k)
Definition: z3py.py:1216

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

Referenced by AstRef.__bool__().

1493 def is_eq(a):
1494  """Return `True` if `a` is a Z3 equality expression.
1495 
1496  >>> x, y = Ints('x y')
1497  >>> is_eq(x == y)
1498  True
1499  """
1500  return is_app_of(a, Z3_OP_EQ)
1501 
def is_eq(a)
Definition: z3py.py:1493
def is_app_of(a, k)
Definition: z3py.py:1216

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

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

1095 def is_expr(a):
1096  """Return `True` if `a` is a Z3 expression.
1097 
1098  >>> a = Int('a')
1099  >>> is_expr(a)
1100  True
1101  >>> is_expr(a + 1)
1102  True
1103  >>> is_expr(IntSort())
1104  False
1105  >>> is_expr(1)
1106  False
1107  >>> is_expr(IntVal(1))
1108  True
1109  >>> x = Int('x')
1110  >>> is_expr(ForAll(x, x >= 0))
1111  True
1112  >>> is_expr(FPVal(1.0))
1113  True
1114  """
1115  return isinstance(a, ExprRef)
1116 
def is_expr(a)
Definition: z3py.py:1095

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

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

1436 def is_false(a):
1437  """Return `True` if `a` is the Z3 false expression.
1438 
1439  >>> p = Bool('p')
1440  >>> is_false(p)
1441  False
1442  >>> is_false(False)
1443  False
1444  >>> is_false(BoolVal(False))
1445  True
1446  """
1447  return is_app_of(a, Z3_OP_FALSE)
1448 
def is_app_of(a, k)
Definition: z3py.py:1216
def is_false(a)
Definition: z3py.py:1436

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

Referenced by is_finite_domain_value().

7187 def is_finite_domain(a):
7188  """Return `True` if `a` is a Z3 finite-domain expression.
7189 
7190  >>> s = FiniteDomainSort('S', 100)
7191  >>> b = Const('b', s)
7192  >>> is_finite_domain(b)
7193  True
7194  >>> is_finite_domain(Int('x'))
7195  False
7196  """
7197  return isinstance(a, FiniteDomainRef)
7198 
7199 
def is_finite_domain(a)
Definition: z3py.py:7187

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

Referenced by FiniteDomainVal().

7165 def is_finite_domain_sort(s):
7166  """Return True if `s` is a Z3 finite-domain sort.
7167 
7168  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7169  True
7170  >>> is_finite_domain_sort(IntSort())
7171  False
7172  """
7173  return isinstance(s, FiniteDomainSortRef)
7174 
7175 
def is_finite_domain_sort(s)
Definition: z3py.py:7165

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

7240 def is_finite_domain_value(a):
7241  """Return `True` if `a` is a Z3 finite-domain value.
7242 
7243  >>> s = FiniteDomainSort('S', 100)
7244  >>> b = Const('b', s)
7245  >>> is_finite_domain_value(b)
7246  False
7247  >>> b = FiniteDomainVal(10, s)
7248  >>> b
7249  10
7250  >>> is_finite_domain_value(b)
7251  True
7252  """
7253  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7254 
7255 
def is_finite_domain_value(a)
Definition: z3py.py:7240
def is_finite_domain(a)
Definition: z3py.py:7187

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

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

9088 def is_fp(a):
9089  """Return `True` if `a` is a Z3 floating-point expression.
9090 
9091  >>> b = FP('b', FPSort(8, 24))
9092  >>> is_fp(b)
9093  True
9094  >>> is_fp(b + 1.0)
9095  True
9096  >>> is_fp(Int('x'))
9097  False
9098  """
9099  return isinstance(a, FPRef)
9100 
def is_fp(a)
Definition: z3py.py:9088

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

8704 def is_fp_sort(s):
8705  """Return True if `s` is a Z3 floating-point sort.
8706 
8707  >>> is_fp_sort(FPSort(8, 24))
8708  True
8709  >>> is_fp_sort(IntSort())
8710  False
8711  """
8712  return isinstance(s, FPSortRef)
8713 
def is_fp_sort(s)
Definition: z3py.py:8704

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

9101 def is_fp_value(a):
9102  """Return `True` if `a` is a Z3 floating-point numeral value.
9103 
9104  >>> b = FP('b', FPSort(8, 24))
9105  >>> is_fp_value(b)
9106  False
9107  >>> b = FPVal(1.0, FPSort(8, 24))
9108  >>> b
9109  1
9110  >>> is_fp_value(b)
9111  True
9112  """
9113  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9114 
def is_fp_value(a)
Definition: z3py.py:9101
def is_fp(a)
Definition: z3py.py:9088

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

8952 def is_fprm(a):
8953  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
8954 
8955  >>> rm = RNE()
8956  >>> is_fprm(rm)
8957  True
8958  >>> rm = 1.0
8959  >>> is_fprm(rm)
8960  False
8961  """
8962  return isinstance(a, FPRMRef)
8963 
def is_fprm(a)
Definition: z3py.py:8952

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

8714 def is_fprm_sort(s):
8715  """Return True if `s` is a Z3 floating-point rounding mode sort.
8716 
8717  >>> is_fprm_sort(FPSort(8, 24))
8718  False
8719  >>> is_fprm_sort(RNE().sort())
8720  True
8721  """
8722  return isinstance(s, FPRMSortRef)
8723 
def is_fprm_sort(s)
Definition: z3py.py:8714

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

8964 def is_fprm_value(a):
8965  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
8966  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
8967 
def is_fprm_value(a)
Definition: z3py.py:8964
def is_fprm(a)
Definition: z3py.py:8952

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

Referenced by prove().

767 def is_func_decl(a):
768  """Return `True` if `a` is a Z3 function declaration.
769 
770  >>> f = Function('f', IntSort(), IntSort())
771  >>> is_func_decl(f)
772  True
773  >>> x = Real('x')
774  >>> is_func_decl(x)
775  False
776  """
777  return isinstance(a, FuncDeclRef)
778 
def is_func_decl(a)
Definition: z3py.py:767

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

2662 def is_ge(a):
2663  """Return `True` if `a` is an expression of the form b >= c.
2664 
2665  >>> x, y = Ints('x y')
2666  >>> is_ge(x >= y)
2667  True
2668  >>> is_ge(x == y)
2669  False
2670  """
2671  return is_app_of(a, Z3_OP_GE)
2672 
def is_ge(a)
Definition: z3py.py:2662
def is_app_of(a, k)
Definition: z3py.py:1216

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

2673 def is_gt(a):
2674  """Return `True` if `a` is an expression of the form b > c.
2675 
2676  >>> x, y = Ints('x y')
2677  >>> is_gt(x > y)
2678  True
2679  >>> is_gt(x == y)
2680  False
2681  """
2682  return is_app_of(a, Z3_OP_GT)
2683 
def is_gt(a)
Definition: z3py.py:2673
def is_app_of(a, k)
Definition: z3py.py:1216

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

Referenced by is_div().

2618 def is_idiv(a):
2619  """Return `True` if `a` is an expression of the form b div c.
2620 
2621  >>> x, y = Ints('x y')
2622  >>> is_idiv(x / y)
2623  True
2624  >>> is_idiv(x + y)
2625  False
2626  """
2627  return is_app_of(a, Z3_OP_IDIV)
2628 
def is_idiv(a)
Definition: z3py.py:2618
def is_app_of(a, k)
Definition: z3py.py:1216

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

1471 def is_implies(a):
1472  """Return `True` if `a` is a Z3 implication expression.
1473 
1474  >>> p, q = Bools('p q')
1475  >>> is_implies(Implies(p, q))
1476  True
1477  >>> is_implies(And(p, q))
1478  False
1479  """
1480  return is_app_of(a, Z3_OP_IMPLIES)
1481 
def is_implies(a)
Definition: z3py.py:1471
def is_app_of(a, k)
Definition: z3py.py:1216

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

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

2470 def is_int(a):
2471  """Return `True` if `a` is an integer expression.
2472 
2473  >>> x = Int('x')
2474  >>> is_int(x + 1)
2475  True
2476  >>> is_int(1)
2477  False
2478  >>> is_int(IntVal(1))
2479  True
2480  >>> y = Real('y')
2481  >>> is_int(y)
2482  False
2483  >>> is_int(y + 1)
2484  False
2485  """
2486  return is_arith(a) and a.is_int()
2487 
def is_arith(a)
Definition: z3py.py:2450
def is_int(a)
Definition: z3py.py:2470

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

2512 def is_int_value(a):
2513  """Return `True` if `a` is an integer value of sort Int.
2514 
2515  >>> is_int_value(IntVal(1))
2516  True
2517  >>> is_int_value(1)
2518  False
2519  >>> is_int_value(Int('x'))
2520  False
2521  >>> n = Int('x') + 1
2522  >>> n
2523  x + 1
2524  >>> n.arg(1)
2525  1
2526  >>> is_int_value(n.arg(1))
2527  True
2528  >>> is_int_value(RealVal("1/3"))
2529  False
2530  >>> is_int_value(RealVal(1))
2531  False
2532  """
2533  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2534 
def is_int_value(a)
Definition: z3py.py:2512
def is_arith(a)
Definition: z3py.py:2450

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

2684 def is_is_int(a):
2685  """Return `True` if `a` is an expression of the form IsInt(b).
2686 
2687  >>> x = Real('x')
2688  >>> is_is_int(IsInt(x))
2689  True
2690  >>> is_is_int(x)
2691  False
2692  """
2693  return is_app_of(a, Z3_OP_IS_INT)
2694 
def is_app_of(a, k)
Definition: z3py.py:1216
def is_is_int(a)
Definition: z3py.py:2684

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

4289 def is_K(a):
4290  """Return `True` if `a` is a Z3 constant array.
4291 
4292  >>> a = K(IntSort(), 10)
4293  >>> is_K(a)
4294  True
4295  >>> a = Array('a', IntSort(), IntSort())
4296  >>> is_K(a)
4297  False
4298  """
4299  return is_app_of(a, Z3_OP_CONST_ARRAY)
4300 
def is_K(a)
Definition: z3py.py:4289
def is_app_of(a, k)
Definition: z3py.py:1216

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

2640 def is_le(a):
2641  """Return `True` if `a` is an expression of the form b <= c.
2642 
2643  >>> x, y = Ints('x y')
2644  >>> is_le(x <= y)
2645  True
2646  >>> is_le(x < y)
2647  False
2648  """
2649  return is_app_of(a, Z3_OP_LE)
2650 
def is_le(a)
Definition: z3py.py:2640
def is_app_of(a, k)
Definition: z3py.py:1216

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

2651 def is_lt(a):
2652  """Return `True` if `a` is an expression of the form b < c.
2653 
2654  >>> x, y = Ints('x y')
2655  >>> is_lt(x < y)
2656  True
2657  >>> is_lt(x == y)
2658  False
2659  """
2660  return is_app_of(a, Z3_OP_LT)
2661 
def is_lt(a)
Definition: z3py.py:2651
def is_app_of(a, k)
Definition: z3py.py:1216

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

4301 def is_map(a):
4302  """Return `True` if `a` is a Z3 map array expression.
4303 
4304  >>> f = Function('f', IntSort(), IntSort())
4305  >>> b = Array('b', IntSort(), IntSort())
4306  >>> a = Map(f, b)
4307  >>> a
4308  Map(f, b)
4309  >>> is_map(a)
4310  True
4311  >>> is_map(b)
4312  False
4313  """
4314  return is_app_of(a, Z3_OP_ARRAY_MAP)
4315 
def is_map(a)
Definition: z3py.py:4301
def is_app_of(a, k)
Definition: z3py.py:1216

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

2629 def is_mod(a):
2630  """Return `True` if `a` is an expression of the form b % c.
2631 
2632  >>> x, y = Ints('x y')
2633  >>> is_mod(x % y)
2634  True
2635  >>> is_mod(x + y)
2636  False
2637  """
2638  return is_app_of(a, Z3_OP_MOD)
2639 
def is_mod(a)
Definition: z3py.py:2629
def is_app_of(a, k)
Definition: z3py.py:1216

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

2580 def is_mul(a):
2581  """Return `True` if `a` is an expression of the form b * c.
2582 
2583  >>> x, y = Ints('x y')
2584  >>> is_mul(x * y)
2585  True
2586  >>> is_mul(x - y)
2587  False
2588  """
2589  return is_app_of(a, Z3_OP_MUL)
2590 
def is_app_of(a, k)
Definition: z3py.py:1216
def is_mul(a)
Definition: z3py.py:2580

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

1482 def is_not(a):
1483  """Return `True` if `a` is a Z3 not expression.
1484 
1485  >>> p = Bool('p')
1486  >>> is_not(p)
1487  False
1488  >>> is_not(Not(p))
1489  True
1490  """
1491  return is_app_of(a, Z3_OP_NOT)
1492 
def is_not(a)
Definition: z3py.py:1482
def is_app_of(a, k)
Definition: z3py.py:1216

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

1460 def is_or(a):
1461  """Return `True` if `a` is a Z3 or expression.
1462 
1463  >>> p, q = Bools('p q')
1464  >>> is_or(Or(p, q))
1465  True
1466  >>> is_or(And(p, q))
1467  False
1468  """
1469  return is_app_of(a, Z3_OP_OR)
1470 
def is_or(a)
Definition: z3py.py:1460
def is_app_of(a, k)
Definition: z3py.py:1216

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

Referenced by MultiPattern().

1741 def is_pattern(a):
1742  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1743 
1744  >>> f = Function('f', IntSort(), IntSort())
1745  >>> x = Int('x')
1746  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1747  >>> q
1748  ForAll(x, f(x) == 0)
1749  >>> q.num_patterns()
1750  1
1751  >>> is_pattern(q.pattern(0))
1752  True
1753  >>> q.pattern(0)
1754  f(Var(0))
1755  """
1756  return isinstance(a, PatternRef)
1757 
def is_pattern(a)
Definition: z3py.py:1741

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

Referenced by eq().

7999 def is_probe(p):
8000  """Return `True` if `p` is a Z3 probe.
8001 
8002  >>> is_probe(Int('x'))
8003  False
8004  >>> is_probe(Probe('memory'))
8005  True
8006  """
8007  return isinstance(p, Probe)
8008 
def is_probe(p)
Definition: z3py.py:7999

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

Referenced by Exists().

1970 def is_quantifier(a):
1971  """Return `True` if `a` is a Z3 quantifier.
1972 
1973  >>> f = Function('f', IntSort(), IntSort())
1974  >>> x = Int('x')
1975  >>> q = ForAll(x, f(x) == 0)
1976  >>> is_quantifier(q)
1977  True
1978  >>> is_quantifier(f(x))
1979  False
1980  """
1981  return isinstance(a, QuantifierRef)
1982 
def is_quantifier(a)
Definition: z3py.py:1970

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

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

2535 def is_rational_value(a):
2536  """Return `True` if `a` is rational value of sort Real.
2537 
2538  >>> is_rational_value(RealVal(1))
2539  True
2540  >>> is_rational_value(RealVal("3/5"))
2541  True
2542  >>> is_rational_value(IntVal(1))
2543  False
2544  >>> is_rational_value(1)
2545  False
2546  >>> n = Real('x') + 1
2547  >>> n.arg(1)
2548  1
2549  >>> is_rational_value(n.arg(1))
2550  True
2551  >>> is_rational_value(Real('x'))
2552  False
2553  """
2554  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2555 
def is_arith(a)
Definition: z3py.py:2450
def is_rational_value(a)
Definition: z3py.py:2535

◆ is_re()

def z3py.is_re (   s)

Definition at line 10212 of file z3py.py.

10212 def is_re(s):
10213  return isinstance(s, ReRef)
10214 
10215 
def is_re(s)
Definition: z3py.py:10212

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

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

2488 def is_real(a):
2489  """Return `True` if `a` is a real expression.
2490 
2491  >>> x = Int('x')
2492  >>> is_real(x + 1)
2493  False
2494  >>> y = Real('y')
2495  >>> is_real(y)
2496  True
2497  >>> is_real(y + 1)
2498  True
2499  >>> is_real(1)
2500  False
2501  >>> is_real(RealVal(1))
2502  True
2503  """
2504  return is_arith(a) and a.is_real()
2505 
def is_real(a)
Definition: z3py.py:2488
def is_arith(a)
Definition: z3py.py:2450

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

4503 def is_select(a):
4504  """Return `True` if `a` is a Z3 array select application.
4505 
4506  >>> a = Array('a', IntSort(), IntSort())
4507  >>> is_select(a)
4508  False
4509  >>> i = Int('i')
4510  >>> is_select(a[i])
4511  True
4512  """
4513  return is_app_of(a, Z3_OP_SELECT)
4514 
def is_select(a)
Definition: z3py.py:4503
def is_app_of(a, k)
Definition: z3py.py:1216

◆ is_seq()

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

Definition at line 9974 of file z3py.py.

9974 def is_seq(a):
9975  """Return `True` if `a` is a Z3 sequence expression.
9976  >>> print (is_seq(Unit(IntVal(0))))
9977  True
9978  >>> print (is_seq(StringVal("abc")))
9979  True
9980  """
9981  return isinstance(a, SeqRef)
9982 
def is_seq(a)
Definition: z3py.py:9974

◆ is_sort()

def z3py.is_sort (   s)
Return `True` if `s` is a Z3 sort.

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

Definition at line 580 of file z3py.py.

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

580 def is_sort(s):
581  """Return `True` if `s` is a Z3 sort.
582 
583  >>> is_sort(IntSort())
584  True
585  >>> is_sort(Int('x'))
586  False
587  >>> is_expr(Int('x'))
588  True
589  """
590  return isinstance(s, SortRef)
591 
def is_sort(s)
Definition: z3py.py:580

◆ is_store()

def z3py.is_store (   a)
Return `True` if `a` is a Z3 array store application.

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

Definition at line 4515 of file z3py.py.

4515 def is_store(a):
4516  """Return `True` if `a` is a Z3 array store application.
4517 
4518  >>> a = Array('a', IntSort(), IntSort())
4519  >>> is_store(a)
4520  False
4521  >>> is_store(Store(a, 0, 1))
4522  True
4523  """
4524  return is_app_of(a, Z3_OP_STORE)
4525 
def is_store(a)
Definition: z3py.py:4515
def is_app_of(a, k)
Definition: z3py.py:1216

◆ is_string()

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

Definition at line 9983 of file z3py.py.

9983 def is_string(a):
9984  """Return `True` if `a` is a Z3 string expression.
9985  >>> print (is_string(StringVal("ab")))
9986  True
9987  """
9988  return isinstance(a, SeqRef) and a.is_string()
9989 
def is_string(a)
Definition: z3py.py:9983

◆ is_string_value()

def z3py.is_string_value (   a)
return 'True' if 'a' is a Z3 string constant expression.
>>> print (is_string_value(StringVal("a")))
True
>>> print (is_string_value(StringVal("a") + StringVal("b")))
False

Definition at line 9990 of file z3py.py.

9990 def is_string_value(a):
9991  """return 'True' if 'a' is a Z3 string constant expression.
9992  >>> print (is_string_value(StringVal("a")))
9993  True
9994  >>> print (is_string_value(StringVal("a") + StringVal("b")))
9995  False
9996  """
9997  return isinstance(a, SeqRef) and a.is_string_value()
9998 
9999 
def is_string_value(a)
Definition: z3py.py:9990

◆ is_sub()

def z3py.is_sub (   a)
Return `True` if `a` is an expression of the form b - c.

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

Definition at line 2591 of file z3py.py.

2591 def is_sub(a):
2592  """Return `True` if `a` is an expression of the form b - c.
2593 
2594  >>> x, y = Ints('x y')
2595  >>> is_sub(x - y)
2596  True
2597  >>> is_sub(x + y)
2598  False
2599  """
2600  return is_app_of(a, Z3_OP_SUB)
2601 
def is_app_of(a, k)
Definition: z3py.py:1216
def is_sub(a)
Definition: z3py.py:2591

◆ is_to_int()

def z3py.is_to_int (   a)
Return `True` if `a` is an expression of the form ToInt(b).

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

Definition at line 2709 of file z3py.py.

2709 def is_to_int(a):
2710  """Return `True` if `a` is an expression of the form ToInt(b).
2711 
2712  >>> x = Real('x')
2713  >>> n = ToInt(x)
2714  >>> n
2715  ToInt(x)
2716  >>> is_to_int(n)
2717  True
2718  >>> is_to_int(x)
2719  False
2720  """
2721  return is_app_of(a, Z3_OP_TO_INT)
2722 
def is_app_of(a, k)
Definition: z3py.py:1216
def is_to_int(a)
Definition: z3py.py:2709

◆ is_to_real()

def z3py.is_to_real (   a)
Return `True` if `a` is an expression of the form ToReal(b).

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

Definition at line 2695 of file z3py.py.

2695 def is_to_real(a):
2696  """Return `True` if `a` is an expression of the form ToReal(b).
2697 
2698  >>> x = Int('x')
2699  >>> n = ToReal(x)
2700  >>> n
2701  ToReal(x)
2702  >>> is_to_real(n)
2703  True
2704  >>> is_to_real(x)
2705  False
2706  """
2707  return is_app_of(a, Z3_OP_TO_REAL)
2708 
def is_to_real(a)
Definition: z3py.py:2695
def is_app_of(a, k)
Definition: z3py.py:1216

◆ is_true()

def z3py.is_true (   a)
Return `True` if `a` is the Z3 true expression.

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

Definition at line 1419 of file z3py.py.

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

1419 def is_true(a):
1420  """Return `True` if `a` is the Z3 true expression.
1421 
1422  >>> p = Bool('p')
1423  >>> is_true(p)
1424  False
1425  >>> is_true(simplify(p == p))
1426  True
1427  >>> x = Real('x')
1428  >>> is_true(x == 0)
1429  False
1430  >>> # True is a Python Boolean expression
1431  >>> is_true(True)
1432  False
1433  """
1434  return is_app_of(a, Z3_OP_TRUE)
1435 
def is_true(a)
Definition: z3py.py:1419
def is_app_of(a, k)
Definition: z3py.py:1216

◆ is_var()

def z3py.is_var (   a)
Return `True` if `a` is variable.

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

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

Definition at line 1160 of file z3py.py.

Referenced by get_var_index().

1160 def is_var(a):
1161  """Return `True` if `a` is variable.
1162 
1163  Z3 uses de-Bruijn indices for representing bound variables in
1164  quantifiers.
1165 
1166  >>> x = Int('x')
1167  >>> is_var(x)
1168  False
1169  >>> is_const(x)
1170  True
1171  >>> f = Function('f', IntSort(), IntSort())
1172  >>> # Z3 replaces x with bound variables when ForAll is executed.
1173  >>> q = ForAll(x, f(x) == x)
1174  >>> b = q.body()
1175  >>> b
1176  f(Var(0)) == Var(0)
1177  >>> b.arg(1)
1178  Var(0)
1179  >>> is_var(b.arg(1))
1180  True
1181  """
1182  return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
1183 
def is_expr(a)
Definition: z3py.py:1095
def is_var(a)
Definition: z3py.py:1160

◆ IsInt()

def z3py.IsInt (   a)
Return the Z3 predicate IsInt(a).

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

Definition at line 3117 of file z3py.py.

Referenced by is_is_int().

3117 def IsInt(a):
3118  """ Return the Z3 predicate IsInt(a).
3119 
3120  >>> x = Real('x')
3121  >>> IsInt(x + "1/2")
3122  IsInt(x + 1/2)
3123  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3124  [x = 1/2]
3125  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3126  no solution
3127  """
3128  if __debug__:
3129  _z3_assert(a.is_real(), "Z3 real expression expected.")
3130  ctx = a.ctx
3131  return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
3132 
def IsInt(a)
Definition: z3py.py:3117
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.

◆ IsMember()

def z3py.IsMember (   e,
  s 
)
Check if e is a member of set s
>>> a = Const('a', SetSort(IntSort()))
>>> IsMember(1, a)
a[1]

Definition at line 4616 of file z3py.py.

4616 def IsMember(e, s):
4617  """ Check if e is a member of set s
4618  >>> a = Const('a', SetSort(IntSort()))
4619  >>> IsMember(1, a)
4620  a[1]
4621  """
4622  ctx = _ctx_from_ast_arg_list([s,e])
4623  e = _py2expr(e, ctx)
4624  return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
4625 
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
def IsMember(e, s)
Definition: z3py.py:4616

◆ IsSubset()

def z3py.IsSubset (   a,
  b 
)
Check if a is a subset of b
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> IsSubset(a, b)
subset(a, b)

Definition at line 4626 of file z3py.py.

4626 def IsSubset(a, b):
4627  """ Check if a is a subset of b
4628  >>> a = Const('a', SetSort(IntSort()))
4629  >>> b = Const('b', SetSort(IntSort()))
4630  >>> IsSubset(a, b)
4631  subset(a, b)
4632  """
4633  ctx = _ctx_from_ast_arg_list([a, b])
4634  return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4635 
4636 
def IsSubset(a, b)
Definition: z3py.py:4626
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.

◆ K()

def z3py.K (   dom,
  v 
)
Return a Z3 constant