Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

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

Functions

def z3_debug ()
 
def enable_trace (msg)
 
def disable_trace (msg)
 
def get_version_string ()
 
def get_version ()
 
def get_full_version ()
 
def open_log (fname)
 
def append_log (s)
 
def to_symbol (s, ctx=None)
 
def z3_error_handler (c, e)
 
def main_ctx ()
 
def get_ctx (ctx)
 
def set_param (*args, **kws)
 
def reset_params ()
 
def set_option (*args, **kws)
 
def get_param (name)
 
def is_ast (a)
 
def eq (a, b)
 
def is_sort (s)
 
def DeclareSort (name, ctx=None)
 
def is_func_decl (a)
 
def Function (name, *sig)
 
def FreshFunction (*sig)
 
def RecFunction (name, *sig)
 
def RecAddDefinition (f, args, body)
 
def deserialize (st)
 
def is_expr (a)
 
def is_app (a)
 
def is_const (a)
 
def is_var (a)
 
def get_var_index (a)
 
def is_app_of (a, k)
 
def If (a, b, c, ctx=None)
 
def Distinct (*args)
 
def Const (name, sort)
 
def Consts (names, sort)
 
def FreshConst (sort, prefix="c")
 
def Var (idx, s)
 
def RealVar (idx, ctx=None)
 
def RealVarVector (n, ctx=None)
 
def is_bool (a)
 
def is_true (a)
 
def is_false (a)
 
def is_and (a)
 
def is_or (a)
 
def is_implies (a)
 
def is_not (a)
 
def is_eq (a)
 
def is_distinct (a)
 
def BoolSort (ctx=None)
 
def BoolVal (val, ctx=None)
 
def Bool (name, ctx=None)
 
def Bools (names, ctx=None)
 
def BoolVector (prefix, sz, ctx=None)
 
def FreshBool (prefix="b", ctx=None)
 
def Implies (a, b, ctx=None)
 
def Xor (a, b, ctx=None)
 
def Not (a, ctx=None)
 
def mk_not (a)
 
def And (*args)
 
def Or (*args)
 
def is_pattern (a)
 
def MultiPattern (*args)
 
def is_quantifier (a)
 
def ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Lambda (vs, body)
 
def is_arith_sort (s)
 
def is_arith (a)
 
def is_int (a)
 
def is_real (a)
 
def is_int_value (a)
 
def is_rational_value (a)
 
def is_algebraic_value (a)
 
def is_add (a)
 
def is_mul (a)
 
def is_sub (a)
 
def is_div (a)
 
def is_idiv (a)
 
def is_mod (a)
 
def is_le (a)
 
def is_lt (a)
 
def is_ge (a)
 
def is_gt (a)
 
def is_is_int (a)
 
def is_to_real (a)
 
def is_to_int (a)
 
def IntSort (ctx=None)
 
def RealSort (ctx=None)
 
def IntVal (val, ctx=None)
 
def RealVal (val, ctx=None)
 
def RatVal (a, b, ctx=None)
 
def Q (a, b, ctx=None)
 
def Int (name, ctx=None)
 
def Ints (names, ctx=None)
 
def IntVector (prefix, sz, ctx=None)
 
def FreshInt (prefix="x", ctx=None)
 
def Real (name, ctx=None)
 
def Reals (names, ctx=None)
 
def RealVector (prefix, sz, ctx=None)
 
def FreshReal (prefix="b", ctx=None)
 
def ToReal (a)
 
def ToInt (a)
 
def IsInt (a)
 
def Sqrt (a, ctx=None)
 
def Cbrt (a, ctx=None)
 
def is_bv_sort (s)
 
def is_bv (a)
 
def is_bv_value (a)
 
def BV2Int (a, is_signed=False)
 
def Int2BV (a, num_bits)
 
def BitVecSort (sz, ctx=None)
 
def BitVecVal (val, bv, ctx=None)
 
def BitVec (name, bv, ctx=None)
 
def BitVecs (names, bv, ctx=None)
 
def Concat (*args)
 
def Extract (high, low, a)
 
def ULE (a, b)
 
def ULT (a, b)
 
def UGE (a, b)
 
def UGT (a, b)
 
def UDiv (a, b)
 
def URem (a, b)
 
def SRem (a, b)
 
def LShR (a, b)
 
def RotateLeft (a, b)
 
def RotateRight (a, b)
 
def SignExt (n, a)
 
def ZeroExt (n, a)
 
def RepeatBitVec (n, a)
 
def BVRedAnd (a)
 
def BVRedOr (a)
 
def BVAddNoOverflow (a, b, signed)
 
def BVAddNoUnderflow (a, b)
 
def BVSubNoOverflow (a, b)
 
def BVSubNoUnderflow (a, b, signed)
 
def BVSDivNoOverflow (a, b)
 
def BVSNegNoOverflow (a)
 
def BVMulNoOverflow (a, b, signed)
 
def BVMulNoUnderflow (a, b)
 
def is_array_sort (a)
 
def is_array (a)
 
def is_const_array (a)
 
def is_K (a)
 
def is_map (a)
 
def is_default (a)
 
def get_map_func (a)
 
def ArraySort (*sig)
 
def Array (name, *sorts)
 
def Update (a, *args)
 
def Default (a)
 
def Store (a, *args)
 
def Select (a, *args)
 
def Map (f, *args)
 
def K (dom, v)
 
def Ext (a, b)
 
def SetHasSize (a, k)
 
def is_select (a)
 
def is_store (a)
 
def SetSort (s)
 Sets. More...
 
def EmptySet (s)
 
def FullSet (s)
 
def SetUnion (*args)
 
def SetIntersect (*args)
 
def SetAdd (s, e)
 
def SetDel (s, e)
 
def SetComplement (s)
 
def SetDifference (a, b)
 
def IsMember (e, s)
 
def IsSubset (a, b)
 
def CreateDatatypes (*ds)
 
def DatatypeSort (name, ctx=None)
 
def TupleSort (name, sorts, ctx=None)
 
def DisjointSum (name, sorts, ctx=None)
 
def EnumSort (name, values, ctx=None)
 
def args2params (arguments, keywords, ctx=None)
 
def Model (ctx=None)
 
def is_as_array (n)
 
def get_as_array_func (n)
 
def SolverFor (logic, ctx=None, logFile=None)
 
def SimpleSolver (ctx=None, logFile=None)
 
def FiniteDomainSort (name, sz, ctx=None)
 
def is_finite_domain_sort (s)
 
def is_finite_domain (a)
 
def FiniteDomainVal (val, sort, ctx=None)
 
def is_finite_domain_value (a)
 
def AndThen (*ts, **ks)
 
def Then (*ts, **ks)
 
def OrElse (*ts, **ks)
 
def ParOr (*ts, **ks)
 
def ParThen (t1, t2, ctx=None)
 
def ParAndThen (t1, t2, ctx=None)
 
def With (t, *args, **keys)
 
def WithParams (t, p)
 
def Repeat (t, max=4294967295, ctx=None)
 
def TryFor (t, ms, ctx=None)
 
def tactics (ctx=None)
 
def tactic_description (name, ctx=None)
 
def describe_tactics ()
 
def is_probe (p)
 
def probes (ctx=None)
 
def probe_description (name, ctx=None)
 
def describe_probes ()
 
def FailIf (p, ctx=None)
 
def When (p, t, ctx=None)
 
def Cond (p, t1, t2, ctx=None)
 
def simplify (a, *arguments, **keywords)
 Utils. More...
 
def help_simplify ()
 
def simplify_param_descrs ()
 
def substitute (t, *m)
 
def substitute_vars (t, *m)
 
def substitute_funs (t, *m)
 
def Sum (*args)
 
def Product (*args)
 
def Abs (arg)
 
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, show=False, **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 CharSort (ctx=None)
 
def SeqSort (s)
 
def CharVal (ch, ctx=None)
 
def CharFromBv (ch, ctx=None)
 
def CharToBv (ch, ctx=None)
 
def CharToInt (ch, ctx=None)
 
def CharIsDigit (ch, ctx=None)
 
def is_seq (a)
 
def is_string (a)
 
def is_string_value (a)
 
def StringVal (s, ctx=None)
 
def String (name, ctx=None)
 
def Strings (names, ctx=None)
 
def SubString (s, offset, length)
 
def SubSeq (s, offset, length)
 
def Empty (s)
 
def Full (s)
 
def Unit (a)
 
def PrefixOf (a, b)
 
def SuffixOf (a, b)
 
def Contains (a, b)
 
def Replace (s, src, dst)
 
def IndexOf (s, substr, offset=None)
 
def LastIndexOf (s, substr)
 
def Length (s)
 
def StrToInt (s)
 
def IntToStr (s)
 
def StrToCode (s)
 
def StrFromCode (c)
 
def Re (s, ctx=None)
 
def ReSort (s)
 
def is_re (s)
 
def InRe (s, re)
 
def Union (*args)
 
def Intersect (*args)
 
def Plus (re)
 
def Option (re)
 
def Complement (re)
 
def Star (re)
 
def Loop (re, lo, hi=0)
 
def Range (lo, hi, ctx=None)
 
def Diff (a, b, ctx=None)
 
def AllChar (regex_sort, ctx=None)
 
def PartialOrder (a, index)
 
def LinearOrder (a, index)
 
def TreeOrder (a, index)
 
def PiecewiseLinearOrder (a, index)
 
def TransitiveClosure (f)
 
def to_Ast (ptr)
 
def to_ContextObj (ptr)
 
def to_AstVectorObj (ptr)
 
def on_clause_eh (ctx, p, clause)
 
def ensure_prop_closures ()
 
def user_prop_push (ctx, cb)
 
def user_prop_pop (ctx, cb, num_scopes)
 
def user_prop_fresh (ctx, _new_ctx)
 
def user_prop_fixed (ctx, cb, id, value)
 
def user_prop_created (ctx, cb, id)
 
def user_prop_final (ctx, cb)
 
def user_prop_eq (ctx, cb, x, y)
 
def user_prop_diseq (ctx, cb, x, y)
 
def user_prop_decide (ctx, cb, t_ref, idx_ref, phase_ref)
 
def PropagateFunction (name, *sig)
 

Variables

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

Function Documentation

◆ Abs()

def z3py.Abs (   arg)
Create the absolute value of an arithmetic expression

Definition at line 8932 of file z3py.py.

8932 def Abs(arg):
8933  """Create the absolute value of an arithmetic expression"""
8934  return If(arg > 0, arg, -arg)
8935 
8936 
def Abs(arg)
Definition: z3py.py:8932
def If(a, b, c, ctx=None)
Definition: z3py.py:1381

◆ AllChar()

def z3py.AllChar (   regex_sort,
  ctx = None 
)
Create a regular expression that accepts all single character strings

Definition at line 11298 of file z3py.py.

11298 def AllChar(regex_sort, ctx=None):
11299  """Create a regular expression that accepts all single character strings
11300  """
11301  return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
11302 
11303 # Special Relations
11304 
11305 
Z3_ast Z3_API Z3_mk_re_allchar(Z3_context c, Z3_sort regex_sort)
Create a regular expression that accepts all singleton sequences of the regular expression sort.
def AllChar(regex_sort, ctx=None)
Definition: z3py.py:11298

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

1849 def And(*args):
1850  """Create a Z3 and-expression or and-probe.
1851 
1852  >>> p, q, r = Bools('p q r')
1853  >>> And(p, q, r)
1854  And(p, q, r)
1855  >>> P = BoolVector('p', 5)
1856  >>> And(P)
1857  And(p__0, p__1, p__2, p__3, p__4)
1858  """
1859  last_arg = None
1860  if len(args) > 0:
1861  last_arg = args[len(args) - 1]
1862  if isinstance(last_arg, Context):
1863  ctx = args[len(args) - 1]
1864  args = args[:len(args) - 1]
1865  elif len(args) == 1 and isinstance(args[0], AstVector):
1866  ctx = args[0].ctx
1867  args = [a for a in args[0]]
1868  else:
1869  ctx = None
1870  args = _get_args(args)
1871  ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1872  if z3_debug():
1873  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1874  if _has_probe(args):
1875  return _probe_and(args, ctx)
1876  else:
1877  args = _coerce_expr_list(args, ctx)
1878  _args, sz = _to_ast_array(args)
1879  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1880 
1881 
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
def z3_debug()
Definition: z3py.py:62
def And(*args)
Definition: z3py.py:1849

Referenced by Fixedpoint.add_rule(), Goal.as_expr(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().

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

8297 def AndThen(*ts, **ks):
8298  """Return a tactic that applies the tactics in `*ts` in sequence.
8299 
8300  >>> x, y = Ints('x y')
8301  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
8302  >>> t(And(x == 0, y > x + 1))
8303  [[Not(y <= 1)]]
8304  >>> t(And(x == 0, y > x + 1)).as_expr()
8305  Not(y <= 1)
8306  """
8307  if z3_debug():
8308  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8309  ctx = ks.get("ctx", None)
8310  num = len(ts)
8311  r = ts[0]
8312  for i in range(num - 1):
8313  r = _and_then(r, ts[i + 1], ctx)
8314  return r
8315 
8316 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3970
def AndThen(*ts, **ks)
Definition: z3py.py:8297

Referenced by Then().

◆ append_log()

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

Definition at line 119 of file z3py.py.

119 def append_log(s):
120  """Append user-defined string to interaction log. """
121  Z3_append_log(s)
122 
123 
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
def append_log(s)
Definition: z3py.py:119

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

5466 def args2params(arguments, keywords, ctx=None):
5467  """Convert python arguments into a Z3_params object.
5468  A ':' is added to the keywords, and '_' is replaced with '-'
5469 
5470  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5471  (params model true relevancy 2 elim_and true)
5472  """
5473  if z3_debug():
5474  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5475  prev = None
5476  r = ParamsRef(ctx)
5477  for a in arguments:
5478  if prev is None:
5479  prev = a
5480  else:
5481  r.set(prev, a)
5482  prev = None
5483  for k in keywords:
5484  v = keywords[k]
5485  r.set(k, v)
5486  return r
5487 
5488 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5466

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

◆ Array()

def z3py.Array (   name,
sorts 
)
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 4733 of file z3py.py.

4733 def Array(name, *sorts):
4734  """Return an array constant named `name` with the given domain and range sorts.
4735 
4736  >>> a = Array('a', IntSort(), IntSort())
4737  >>> a.sort()
4738  Array(Int, Int)
4739  >>> a[0]
4740  a[0]
4741  """
4742  s = ArraySort(sorts)
4743  ctx = s.ctx
4744  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4745 
4746 
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:4700
def Array(name, *sorts)
Definition: z3py.py:4733
def to_symbol(s, ctx=None)
Definition: z3py.py:124

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

4700 def ArraySort(*sig):
4701  """Return the Z3 array sort with the given domain and range sorts.
4702 
4703  >>> A = ArraySort(IntSort(), BoolSort())
4704  >>> A
4705  Array(Int, Bool)
4706  >>> A.domain()
4707  Int
4708  >>> A.range()
4709  Bool
4710  >>> AA = ArraySort(IntSort(), A)
4711  >>> AA
4712  Array(Int, Array(Int, Bool))
4713  """
4714  sig = _get_args(sig)
4715  if z3_debug():
4716  _z3_assert(len(sig) > 1, "At least two arguments expected")
4717  arity = len(sig) - 1
4718  r = sig[arity]
4719  d = sig[0]
4720  if z3_debug():
4721  for s in sig:
4722  _z3_assert(is_sort(s), "Z3 sort expected")
4723  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4724  ctx = d.ctx
4725  if len(sig) == 2:
4726  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4727  dom = (Sort * arity)()
4728  for i in range(arity):
4729  dom[i] = sig[i].ast
4730  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4731 
4732 
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.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
def is_sort(s)
Definition: z3py.py:647

Referenced by Array(), Context.MkArraySort(), and SetSort().

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

8955 def AtLeast(*args):
8956  """Create an at-most Pseudo-Boolean k constraint.
8957 
8958  >>> a, b, c = Bools('a b c')
8959  >>> f = AtLeast(a, b, c, 2)
8960  """
8961  args = _get_args(args)
8962  if z3_debug():
8963  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8964  ctx = _ctx_from_ast_arg_list(args)
8965  if z3_debug():
8966  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8967  args1 = _coerce_expr_list(args[:-1], ctx)
8968  k = args[-1]
8969  _args, sz = _to_ast_array(args1)
8970  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8971 
8972 
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
def AtLeast(*args)
Definition: z3py.py:8955

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

8937 def AtMost(*args):
8938  """Create an at-most Pseudo-Boolean k constraint.
8939 
8940  >>> a, b, c = Bools('a b c')
8941  >>> f = AtMost(a, b, c, 2)
8942  """
8943  args = _get_args(args)
8944  if z3_debug():
8945  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8946  ctx = _ctx_from_ast_arg_list(args)
8947  if z3_debug():
8948  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8949  args1 = _coerce_expr_list(args[:-1], ctx)
8950  k = args[-1]
8951  _args, sz = _to_ast_array(args1)
8952  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8953 
8954 
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
def AtMost(*args)
Definition: z3py.py:8937

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

4037 def BitVec(name, bv, ctx=None):
4038  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4039  If `ctx=None`, then the global context is used.
4040 
4041  >>> x = BitVec('x', 16)
4042  >>> is_bv(x)
4043  True
4044  >>> x.size()
4045  16
4046  >>> x.sort()
4047  BitVec(16)
4048  >>> word = BitVecSort(16)
4049  >>> x2 = BitVec('x', word)
4050  >>> eq(x, x2)
4051  True
4052  """
4053  if isinstance(bv, BitVecSortRef):
4054  ctx = bv.ctx
4055  else:
4056  ctx = _get_ctx(ctx)
4057  bv = BitVecSort(bv, ctx)
4058  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
4059 
4060 
def BitVec(name, bv, ctx=None)
Definition: z3py.py:4037
def BitVecSort(sz, ctx=None)
Definition: z3py.py:4005

Referenced by BitVecs().

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

4061 def BitVecs(names, bv, ctx=None):
4062  """Return a tuple of bit-vector constants of size bv.
4063 
4064  >>> x, y, z = BitVecs('x y z', 16)
4065  >>> x.size()
4066  16
4067  >>> x.sort()
4068  BitVec(16)
4069  >>> Sum(x, y, z)
4070  0 + x + y + z
4071  >>> Product(x, y, z)
4072  1*x*y*z
4073  >>> simplify(Product(x, y, z))
4074  x*y*z
4075  """
4076  ctx = _get_ctx(ctx)
4077  if isinstance(names, str):
4078  names = names.split(" ")
4079  return [BitVec(name, bv, ctx) for name in names]
4080 
4081 
def BitVecs(names, bv, ctx=None)
Definition: z3py.py:4061

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

4005 def BitVecSort(sz, ctx=None):
4006  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
4007 
4008  >>> Byte = BitVecSort(8)
4009  >>> Word = BitVecSort(16)
4010  >>> Byte
4011  BitVec(8)
4012  >>> x = Const('x', Byte)
4013  >>> eq(x, BitVec('x', 8))
4014  True
4015  """
4016  ctx = _get_ctx(ctx)
4017  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
4018 
4019 
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.

Referenced by BitVec(), BitVecVal(), Context.mkBitVecSort(), and Context.MkBitVecSort().

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

4020 def BitVecVal(val, bv, ctx=None):
4021  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
4022 
4023  >>> v = BitVecVal(10, 32)
4024  >>> v
4025  10
4026  >>> print("0x%.8x" % v.as_long())
4027  0x0000000a
4028  """
4029  if is_bv_sort(bv):
4030  ctx = bv.ctx
4031  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
4032  else:
4033  ctx = _get_ctx(ctx)
4034  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
4035 
4036 
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
def is_bv_sort(s)
Definition: z3py.py:3476
def BitVecVal(val, bv, ctx=None)
Definition: z3py.py:4020

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

1728 def Bool(name, ctx=None):
1729  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1730 
1731  >>> p = Bool('p')
1732  >>> q = Bool('q')
1733  >>> And(p, q)
1734  And(p, q)
1735  """
1736  ctx = _get_ctx(ctx)
1737  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1738 
1739 
def BoolSort(ctx=None)
Definition: z3py.py:1691
def Bool(name, ctx=None)
Definition: z3py.py:1728

Referenced by Solver.assert_and_track(), Optimize.assert_and_track(), Bools(), and BoolVector().

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

1740 def Bools(names, ctx=None):
1741  """Return a tuple of Boolean constants.
1742 
1743  `names` is a single string containing all names separated by blank spaces.
1744  If `ctx=None`, then the global context is used.
1745 
1746  >>> p, q, r = Bools('p q r')
1747  >>> And(p, Or(q, r))
1748  And(p, Or(q, r))
1749  """
1750  ctx = _get_ctx(ctx)
1751  if isinstance(names, str):
1752  names = names.split(" ")
1753  return [Bool(name, ctx) for name in names]
1754 
1755 
def Bools(names, ctx=None)
Definition: z3py.py:1740

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

1691 def BoolSort(ctx=None):
1692  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1693 
1694  >>> BoolSort()
1695  Bool
1696  >>> p = Const('p', BoolSort())
1697  >>> is_bool(p)
1698  True
1699  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1700  >>> r(0, 1)
1701  r(0, 1)
1702  >>> is_bool(r(0, 1))
1703  True
1704  """
1705  ctx = _get_ctx(ctx)
1706  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1707 
1708 
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.

Referenced by Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), Solver.check(), FreshBool(), Context.getBoolSort(), If(), Implies(), Context.mkBoolSort(), Not(), SetSort(), QuantifierRef.sort(), and Xor().

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

1709 def BoolVal(val, ctx=None):
1710  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1711 
1712  >>> BoolVal(True)
1713  True
1714  >>> is_true(BoolVal(True))
1715  True
1716  >>> is_true(True)
1717  False
1718  >>> is_false(BoolVal(False))
1719  True
1720  """
1721  ctx = _get_ctx(ctx)
1722  if val:
1723  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1724  else:
1725  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1726 
1727 
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:1709

Referenced by Goal.as_expr(), ApplyResult.as_expr(), BoolSortRef.cast(), UserPropagateBase.conflict(), AlgebraicNumRef.index(), is_quantifier(), and Solver.to_smt2().

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

1756 def BoolVector(prefix, sz, ctx=None):
1757  """Return a list of Boolean constants of size `sz`.
1758 
1759  The constants are named using the given prefix.
1760  If `ctx=None`, then the global context is used.
1761 
1762  >>> P = BoolVector('p', 3)
1763  >>> P
1764  [p__0, p__1, p__2]
1765  >>> And(P)
1766  And(p__0, p__1, p__2)
1767  """
1768  return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]
1769 
1770 
def BoolVector(prefix, sz, ctx=None)
Definition: z3py.py:1756

◆ BV2Int()

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

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

Definition at line 3973 of file z3py.py.

3973 def BV2Int(a, is_signed=False):
3974  """Return the Z3 expression BV2Int(a).
3975 
3976  >>> b = BitVec('b', 3)
3977  >>> BV2Int(b).sort()
3978  Int
3979  >>> x = Int('x')
3980  >>> x > BV2Int(b)
3981  x > BV2Int(b)
3982  >>> x > BV2Int(b, is_signed=False)
3983  x > BV2Int(b)
3984  >>> x > BV2Int(b, is_signed=True)
3985  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3986  >>> solve(x > BV2Int(b), b == 1, x < 3)
3987  [x = 2, b = 1]
3988  """
3989  if z3_debug():
3990  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
3991  ctx = a.ctx
3992  # investigate problem with bv2int
3993  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3994 
3995 
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 is_bv(a)
Definition: z3py.py:3944
def BV2Int(a, is_signed=False)
Definition: z3py.py:3973

◆ BVAddNoOverflow()

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

Definition at line 4459 of file z3py.py.

4459 def BVAddNoOverflow(a, b, signed):
4460  """A predicate the determines that bit-vector addition does not overflow"""
4461  _check_bv_args(a, b)
4462  a, b = _coerce_exprs(a, b)
4463  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4464 
4465 
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.
def BVAddNoOverflow(a, b, signed)
Definition: z3py.py:4459

◆ BVAddNoUnderflow()

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

Definition at line 4466 of file z3py.py.

4466 def BVAddNoUnderflow(a, b):
4467  """A predicate the determines that signed bit-vector addition does not underflow"""
4468  _check_bv_args(a, b)
4469  a, b = _coerce_exprs(a, b)
4470  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4471 
4472 
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.
def BVAddNoUnderflow(a, b)
Definition: z3py.py:4466

◆ BVMulNoOverflow()

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

Definition at line 4501 of file z3py.py.

4501 def BVMulNoOverflow(a, b, signed):
4502  """A predicate the determines that bit-vector multiplication does not overflow"""
4503  _check_bv_args(a, b)
4504  a, b = _coerce_exprs(a, b)
4505  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4506 
4507 
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.
def BVMulNoOverflow(a, b, signed)
Definition: z3py.py:4501

◆ BVMulNoUnderflow()

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

Definition at line 4508 of file z3py.py.

4508 def BVMulNoUnderflow(a, b):
4509  """A predicate the determines that bit-vector signed multiplication does not underflow"""
4510  _check_bv_args(a, b)
4511  a, b = _coerce_exprs(a, b)
4512  return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4513 
4514 
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:4508

◆ BVRedAnd()

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

Definition at line 4445 of file z3py.py.

4445 def BVRedAnd(a):
4446  """Return the reduction-and expression of `a`."""
4447  if z3_debug():
4448  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4449  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4450 
4451 
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:4445

◆ BVRedOr()

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

Definition at line 4452 of file z3py.py.

4452 def BVRedOr(a):
4453  """Return the reduction-or expression of `a`."""
4454  if z3_debug():
4455  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4456  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4457 
4458 
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 BVRedOr(a)
Definition: z3py.py:4452

◆ BVSDivNoOverflow()

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

Definition at line 4487 of file z3py.py.

4487 def BVSDivNoOverflow(a, b):
4488  """A predicate the determines that bit-vector signed division does not overflow"""
4489  _check_bv_args(a, b)
4490  a, b = _coerce_exprs(a, b)
4491  return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4492 
4493 
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.
def BVSDivNoOverflow(a, b)
Definition: z3py.py:4487

◆ BVSNegNoOverflow()

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

Definition at line 4494 of file z3py.py.

4494 def BVSNegNoOverflow(a):
4495  """A predicate the determines that bit-vector unary negation does not overflow"""
4496  if z3_debug():
4497  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4498  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4499 
4500 
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:4494

◆ BVSubNoOverflow()

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

Definition at line 4473 of file z3py.py.

4473 def BVSubNoOverflow(a, b):
4474  """A predicate the determines that bit-vector subtraction does not overflow"""
4475  _check_bv_args(a, b)
4476  a, b = _coerce_exprs(a, b)
4477  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4478 
4479 
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.
def BVSubNoOverflow(a, b)
Definition: z3py.py:4473

◆ BVSubNoUnderflow()

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

Definition at line 4480 of file z3py.py.

4480 def BVSubNoUnderflow(a, b, signed):
4481  """A predicate the determines that bit-vector subtraction does not underflow"""
4482  _check_bv_args(a, b)
4483  a, b = _coerce_exprs(a, b)
4484  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4485 
4486 
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.
def BVSubNoUnderflow(a, b, signed)
Definition: z3py.py:4480

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

3424 def Cbrt(a, ctx=None):
3425  """ Return a Z3 expression which represents the cubic root of a.
3426 
3427  >>> x = Real('x')
3428  >>> Cbrt(x)
3429  x**(1/3)
3430  """
3431  if not is_expr(a):
3432  ctx = _get_ctx(ctx)
3433  a = RealVal(a, ctx)
3434  return a ** "1/3"
3435 
def is_expr(a)
Definition: z3py.py:1242
def Cbrt(a, ctx=None)
Definition: z3py.py:3424
def RealVal(val, ctx=None)
Definition: z3py.py:3200

◆ CharFromBv()

def z3py.CharFromBv (   ch,
  ctx = None 
)

Definition at line 10856 of file z3py.py.

10856 def CharFromBv(ch, ctx=None):
10857  if not is_expr(ch):
10858  raise Z3Expression("Bit-vector expression needed")
10859  return _to_expr_ref(Z3_mk_char_from_bv(ch.ctx_ref(), ch.as_ast()), ch.ctx)
10860 
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).
def CharFromBv(ch, ctx=None)
Definition: z3py.py:10856

◆ CharIsDigit()

def z3py.CharIsDigit (   ch,
  ctx = None 
)

Definition at line 10869 of file z3py.py.

10869 def CharIsDigit(ch, ctx=None):
10870  ch = _coerce_char(ch, ctx)
10871  return ch.is_digit()
10872 
def CharIsDigit(ch, ctx=None)
Definition: z3py.py:10869

◆ CharSort()

def z3py.CharSort (   ctx = None)
Create a character sort
>>> ch = CharSort()
>>> print(ch)
Char

Definition at line 10755 of file z3py.py.

10755 def CharSort(ctx=None):
10756  """Create a character sort
10757  >>> ch = CharSort()
10758  >>> print(ch)
10759  Char
10760  """
10761  ctx = _get_ctx(ctx)
10762  return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
10763 
10764 
Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
def CharSort(ctx=None)
Definition: z3py.py:10755

Referenced by Context.mkCharSort().

◆ CharToBv()

def z3py.CharToBv (   ch,
  ctx = None 
)

Definition at line 10861 of file z3py.py.

10861 def CharToBv(ch, ctx=None):
10862  ch = _coerce_char(ch, ctx)
10863  return ch.to_bv()
10864 
def CharToBv(ch, ctx=None)
Definition: z3py.py:10861

◆ CharToInt()

def z3py.CharToInt (   ch,
  ctx = None 
)

Definition at line 10865 of file z3py.py.

10865 def CharToInt(ch, ctx=None):
10866  ch = _coerce_char(ch, ctx)
10867  return ch.to_int()
10868 
def CharToInt(ch, ctx=None)
Definition: z3py.py:10865

◆ CharVal()

def z3py.CharVal (   ch,
  ctx = None 
)

Definition at line 10848 of file z3py.py.

10848 def CharVal(ch, ctx=None):
10849  ctx = _get_ctx(ctx)
10850  if isinstance(ch, str):
10851  ch = ord(ch)
10852  if not isinstance(ch, int):
10853  raise Z3Exception("character value should be an ordinal")
10854  return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
10855 
Z3_ast Z3_API Z3_mk_char(Z3_context c, unsigned ch)
Create a character literal.
def CharVal(ch, ctx=None)
Definition: z3py.py:10848

Referenced by SeqRef.__gt__().

◆ Complement()

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

Definition at line 11250 of file z3py.py.

11250 def Complement(re):
11251  """Create the complement regular expression."""
11252  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
11253 
11254 
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:11250

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

4082 def Concat(*args):
4083  """Create a Z3 bit-vector concatenation expression.
4084 
4085  >>> v = BitVecVal(1, 4)
4086  >>> Concat(v, v+1, v)
4087  Concat(Concat(1, 1 + 1), 1)
4088  >>> simplify(Concat(v, v+1, v))
4089  289
4090  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
4091  121
4092  """
4093  args = _get_args(args)
4094  sz = len(args)
4095  if z3_debug():
4096  _z3_assert(sz >= 2, "At least two arguments expected.")
4097 
4098  ctx = None
4099  for a in args:
4100  if is_expr(a):
4101  ctx = a.ctx
4102  break
4103  if is_seq(args[0]) or isinstance(args[0], str):
4104  args = [_coerce_seq(s, ctx) for s in args]
4105  if z3_debug():
4106  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
4107  v = (Ast * sz)()
4108  for i in range(sz):
4109  v[i] = args[i].as_ast()
4110  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
4111 
4112  if is_re(args[0]):
4113  if z3_debug():
4114  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
4115  v = (Ast * sz)()
4116  for i in range(sz):
4117  v[i] = args[i].as_ast()
4118  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
4119 
4120  if z3_debug():
4121  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
4122  r = args[0]
4123  for i in range(sz - 1):
4124  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
4125  return r
4126 
4127 
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
def Concat(*args)
Definition: z3py.py:4082
def is_seq(a)
Definition: z3py.py:10894
def is_re(s)
Definition: z3py.py:11168

Referenced by SeqRef.__add__(), and SeqRef.__radd__().

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

8754 def Cond(p, t1, t2, ctx=None):
8755  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8756 
8757  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8758  """
8759  p = _to_probe(p, ctx)
8760  t1 = _to_tactic(t1, ctx)
8761  t2 = _to_tactic(t2, ctx)
8762  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8763 
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...
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8754

Referenced by If().

◆ Const()

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

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

Definition at line 1437 of file z3py.py.

1437 def Const(name, sort):
1438  """Create a constant of the given sort.
1439 
1440  >>> Const('x', IntSort())
1441  x
1442  """
1443  if z3_debug():
1444  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1445  ctx = sort.ctx
1446  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1447 
1448 
def Const(name, sort)
Definition: z3py.py:1437

Referenced by Consts().

◆ Consts()

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

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

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

Definition at line 1449 of file z3py.py.

1449 def Consts(names, sort):
1450  """Create several constants of the given sort.
1451 
1452  `names` is a string containing the names of all constants to be created.
1453  Blank spaces separate the names of different constants.
1454 
1455  >>> x, y, z = Consts('x y z', IntSort())
1456  >>> x + y + z
1457  x + y + z
1458  """
1459  if isinstance(names, str):
1460  names = names.split(" ")
1461  return [Const(name, sort) for name in names]
1462 
1463 
def Consts(names, sort)
Definition: z3py.py:1449

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

11025 def Contains(a, b):
11026  """Check if 'a' contains 'b'
11027  >>> s1 = Contains("abc", "ab")
11028  >>> simplify(s1)
11029  True
11030  >>> s2 = Contains("abc", "bc")
11031  >>> simplify(s2)
11032  True
11033  >>> x, y, z = Strings('x y z')
11034  >>> s3 = Contains(Concat(x,y,z), y)
11035  >>> simplify(s3)
11036  True
11037  """
11038  ctx = _get_ctx2(a, b)
11039  a = _coerce_seq(a, ctx)
11040  b = _coerce_seq(b, ctx)
11041  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11042 
11043 
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
def Contains(a, b)
Definition: z3py.py:11025

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

5158 def CreateDatatypes(*ds):
5159  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
5160 
5161  In the following example we define a Tree-List using two mutually recursive datatypes.
5162 
5163  >>> TreeList = Datatype('TreeList')
5164  >>> Tree = Datatype('Tree')
5165  >>> # Tree has two constructors: leaf and node
5166  >>> Tree.declare('leaf', ('val', IntSort()))
5167  >>> # a node contains a list of trees
5168  >>> Tree.declare('node', ('children', TreeList))
5169  >>> TreeList.declare('nil')
5170  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
5171  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
5172  >>> Tree.val(Tree.leaf(10))
5173  val(leaf(10))
5174  >>> simplify(Tree.val(Tree.leaf(10)))
5175  10
5176  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
5177  >>> n1
5178  node(cons(leaf(10), cons(leaf(20), nil)))
5179  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
5180  >>> simplify(n2 == n1)
5181  False
5182  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
5183  True
5184  """
5185  ds = _get_args(ds)
5186  if z3_debug():
5187  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
5188  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
5189  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
5190  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
5191  ctx = ds[0].ctx
5192  num = len(ds)
5193  names = (Symbol * num)()
5194  out = (Sort * num)()
5195  clists = (ConstructorList * num)()
5196  to_delete = []
5197  for i in range(num):
5198  d = ds[i]
5199  names[i] = to_symbol(d.name, ctx)
5200  num_cs = len(d.constructors)
5201  cs = (Constructor * num_cs)()
5202  for j in range(num_cs):
5203  c = d.constructors[j]
5204  cname = to_symbol(c[0], ctx)
5205  rname = to_symbol(c[1], ctx)
5206  fs = c[2]
5207  num_fs = len(fs)
5208  fnames = (Symbol * num_fs)()
5209  sorts = (Sort * num_fs)()
5210  refs = (ctypes.c_uint * num_fs)()
5211  for k in range(num_fs):
5212  fname = fs[k][0]
5213  ftype = fs[k][1]
5214  fnames[k] = to_symbol(fname, ctx)
5215  if isinstance(ftype, Datatype):
5216  if z3_debug():
5217  _z3_assert(
5218  ds.count(ftype) == 1,
5219  "One and only one occurrence of each datatype is expected",
5220  )
5221  sorts[k] = None
5222  refs[k] = ds.index(ftype)
5223  else:
5224  if z3_debug():
5225  _z3_assert(is_sort(ftype), "Z3 sort expected")
5226  sorts[k] = ftype.ast
5227  refs[k] = 0
5228  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
5229  to_delete.append(ScopedConstructor(cs[j], ctx))
5230  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
5231  to_delete.append(ScopedConstructorList(clists[i], ctx))
5232  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
5233  result = []
5234  # Create a field for every constructor, recognizer and accessor
5235  for i in range(num):
5236  dref = DatatypeSortRef(out[i], ctx)
5237  num_cs = dref.num_constructors()
5238  for j in range(num_cs):
5239  cref = dref.constructor(j)
5240  cref_name = cref.name()
5241  cref_arity = cref.arity()
5242  if cref.arity() == 0:
5243  cref = cref()
5244  setattr(dref, cref_name, cref)
5245  rref = dref.recognizer(j)
5246  setattr(dref, "is_" + cref_name, rref)
5247  for k in range(cref_arity):
5248  aref = dref.accessor(j, k)
5249  setattr(dref, aref.name(), aref)
5250  result.append(dref)
5251  return tuple(result)
5252 
5253 
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.
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.
def CreateDatatypes(*ds)
Definition: z3py.py:5158

Referenced by Datatype.create().

◆ DatatypeSort()

def z3py.DatatypeSort (   name,
  ctx = None 
)
Create a reference to a sort that was declared, or will be declared, as a recursive datatype

Definition at line 5358 of file z3py.py.

5358 def DatatypeSort(name, ctx = None):
5359  """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
5360  ctx = _get_ctx(ctx)
5361  return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
5362 
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
def DatatypeSort(name, ctx=None)
Definition: z3py.py:5358

Referenced by Context.MkDatatypeSort(), and Context.MkDatatypeSorts().

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

693 def DeclareSort(name, ctx=None):
694  """Create a new uninterpreted sort named `name`.
695 
696  If `ctx=None`, then the new sort is declared in the global Z3Py context.
697 
698  >>> A = DeclareSort('A')
699  >>> a = Const('a', A)
700  >>> b = Const('b', A)
701  >>> a.sort() == A
702  True
703  >>> b.sort() == A
704  True
705  >>> a == b
706  a == b
707  """
708  ctx = _get_ctx(ctx)
709  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
710 
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:693

◆ Default()

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

Definition at line 4779 of file z3py.py.

4779 def Default(a):
4780  """ Return a default value for array expression.
4781  >>> b = K(IntSort(), 1)
4782  >>> prove(Default(b) == 1)
4783  proved
4784  """
4785  if z3_debug():
4786  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4787  return a.default()
4788 
4789 
def is_array_sort(a)
Definition: z3py.py:4607
def Default(a)
Definition: z3py.py:4779

◆ describe_probes()

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

Definition at line 8675 of file z3py.py.

8675 def describe_probes():
8676  """Display a (tabular) description of all available probes in Z3."""
8677  if in_html_mode():
8678  even = True
8679  print('<table border="1" cellpadding="2" cellspacing="0">')
8680  for p in probes():
8681  if even:
8682  print('<tr style="background-color:#CFCFCF">')
8683  even = False
8684  else:
8685  print("<tr>")
8686  even = True
8687  print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
8688  print("</table>")
8689  else:
8690  for p in probes():
8691  print("%s : %s" % (p, probe_description(p)))
8692 
8693 
def probe_description(name, ctx=None)
Definition: z3py.py:8666
def describe_probes()
Definition: z3py.py:8675
def probes(ctx=None)
Definition: z3py.py:8655

◆ describe_tactics()

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

Definition at line 8469 of file z3py.py.

8469 def describe_tactics():
8470  """Display a (tabular) description of all available tactics in Z3."""
8471  if in_html_mode():
8472  even = True
8473  print('<table border="1" cellpadding="2" cellspacing="0">')
8474  for t in tactics():
8475  if even:
8476  print('<tr style="background-color:#CFCFCF">')
8477  even = False
8478  else:
8479  print("<tr>")
8480  even = True
8481  print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
8482  print("</table>")
8483  else:
8484  for t in tactics():
8485  print("%s : %s" % (t, tactic_description(t)))
8486 
8487 
def tactics(ctx=None)
Definition: z3py.py:8449
def tactic_description(name, ctx=None)
Definition: z3py.py:8460
def describe_tactics()
Definition: z3py.py:8469

◆ deserialize()

def z3py.deserialize (   st)
inverse function to the serialize method on ExprRef.
It is made available to make it easier for users to serialize expressions back and forth between
strings. Solvers can be serialized using the 'sexpr()' method.

Definition at line 1119 of file z3py.py.

1119 def deserialize(st):
1120  """inverse function to the serialize method on ExprRef.
1121  It is made available to make it easier for users to serialize expressions back and forth between
1122  strings. Solvers can be serialized using the 'sexpr()' method.
1123  """
1124  s = Solver()
1125  s.from_string(st)
1126  if len(s.assertions()) != 1:
1127  raise Z3Exception("single assertion expected")
1128  fml = s.assertions()[0]
1129  if fml.num_args() != 1:
1130  raise Z3Exception("dummy function 'F' expected")
1131  return fml.arg(0)
1132 
def deserialize(st)
Definition: z3py.py:1119

◆ Diff()

def z3py.Diff (   a,
  b,
  ctx = None 
)
Create the difference regular epression

Definition at line 11293 of file z3py.py.

11293 def Diff(a, b, ctx=None):
11294  """Create the difference regular epression
11295  """
11296  return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)
11297 
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
def Diff(a, b, ctx=None)
Definition: z3py.py:11293

◆ disable_trace()

def z3py.disable_trace (   msg)

Definition at line 79 of file z3py.py.

79 def disable_trace(msg):
80  Z3_disable_trace(msg)
81 
82 
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:79

◆ DisjointSum()

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

Definition at line 5375 of file z3py.py.

5375 def DisjointSum(name, sorts, ctx=None):
5376  """Create a named tagged union sort base on a set of underlying sorts
5377  Example:
5378  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5379  """
5380  sum = Datatype(name, ctx)
5381  for i in range(len(sorts)):
5382  sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
5383  sum = sum.create()
5384  return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
5385 
5386 
def DisjointSum(name, sorts, ctx=None)
Definition: z3py.py:5375

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

1404 def Distinct(*args):
1405  """Create a Z3 distinct expression.
1406 
1407  >>> x = Int('x')
1408  >>> y = Int('y')
1409  >>> Distinct(x, y)
1410  x != y
1411  >>> z = Int('z')
1412  >>> Distinct(x, y, z)
1413  Distinct(x, y, z)
1414  >>> simplify(Distinct(x, y, z))
1415  Distinct(x, y, z)
1416  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1417  And(Not(x == y), Not(x == z), Not(y == z))
1418  """
1419  args = _get_args(args)
1420  ctx = _ctx_from_ast_arg_list(args)
1421  if z3_debug():
1422  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
1423  args = _coerce_expr_list(args, ctx)
1424  _args, sz = _to_ast_array(args)
1425  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1426 
1427 
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:1404

◆ Empty()

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

Definition at line 10955 of file z3py.py.

10955 def Empty(s):
10956  """Create the empty sequence of the given sort
10957  >>> e = Empty(StringSort())
10958  >>> e2 = StringVal("")
10959  >>> print(e.eq(e2))
10960  True
10961  >>> e3 = Empty(SeqSort(IntSort()))
10962  >>> print(e3)
10963  Empty(Seq(Int))
10964  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10965  >>> print(e4)
10966  Empty(ReSort(Seq(Int)))
10967  """
10968  if isinstance(s, SeqSortRef):
10969  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10970  if isinstance(s, ReSortRef):
10971  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10972  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10973 
10974 
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
def Empty(s)
Definition: z3py.py:10955

◆ EmptySet()

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

Definition at line 4922 of file z3py.py.

4922 def EmptySet(s):
4923  """Create the empty set
4924  >>> EmptySet(IntSort())
4925  K(Int, False)
4926  """
4927  ctx = s.ctx
4928  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4929 
4930 
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
def EmptySet(s)
Definition: z3py.py:4922

◆ enable_trace()

def z3py.enable_trace (   msg)

Definition at line 75 of file z3py.py.

75 def enable_trace(msg):
76  Z3_enable_trace(msg)
77 
78 
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:75

◆ ensure_prop_closures()

def z3py.ensure_prop_closures ( )

Definition at line 11408 of file z3py.py.

11408 def ensure_prop_closures():
11409  global _prop_closures
11410  if _prop_closures is None:
11411  _prop_closures = PropClosures()
11412 
11413 
def ensure_prop_closures()
Definition: z3py.py:11408

Referenced by UserPropagateBase.__init__().

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

5387 def EnumSort(name, values, ctx=None):
5388  """Return a new enumeration sort named `name` containing the given values.
5389 
5390  The result is a pair (sort, list of constants).
5391  Example:
5392  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5393  """
5394  if z3_debug():
5395  _z3_assert(isinstance(name, str), "Name must be a string")
5396  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
5397  _z3_assert(len(values) > 0, "At least one value expected")
5398  ctx = _get_ctx(ctx)
5399  num = len(values)
5400  _val_names = (Symbol * num)()
5401  for i in range(num):
5402  _val_names[i] = to_symbol(values[i])
5403  _values = (FuncDecl * num)()
5404  _testers = (FuncDecl * num)()
5405  name = to_symbol(name)
5406  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5407  V = []
5408  for i in range(num):
5409  V.append(FuncDeclRef(_values[i], ctx))
5410  V = [a() for a in V]
5411  return S, V
5412 
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.
def EnumSort(name, values, ctx=None)
Definition: z3py.py:5387

Referenced by Context.MkEnumSort().

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

472 def eq(a, b):
473  """Return `True` if `a` and `b` are structurally identical AST nodes.
474 
475  >>> x = Int('x')
476  >>> y = Int('y')
477  >>> eq(x, y)
478  False
479  >>> eq(x + 1, x + 1)
480  True
481  >>> eq(x + 1, 1 + x)
482  False
483  >>> eq(simplify(x + 1), simplify(1 + x))
484  True
485  """
486  if z3_debug():
487  _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
488  return a.eq(b)
489 
490 
def is_ast(a)
Definition: z3py.py:451
def eq(a, b)
Definition: z3py.py:472

Referenced by substitute().

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

2240 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2241  """Create a Z3 exists formula.
2242 
2243  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2244 
2245 
2246  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2247  >>> x = Int('x')
2248  >>> y = Int('y')
2249  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2250  >>> q
2251  Exists([x, y], f(x, y) >= x)
2252  >>> is_quantifier(q)
2253  True
2254  >>> r = Tactic('nnf')(q).as_expr()
2255  >>> is_quantifier(r)
2256  False
2257  """
2258  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2259 
2260 
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2240

Referenced by Fixedpoint.abstract().

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

4868 def Ext(a, b):
4869  """Return extensionality index for one-dimensional arrays.
4870  >> a, b = Consts('a b', SetSort(IntSort()))
4871  >> Ext(a, b)
4872  Ext(a, b)
4873  """
4874  ctx = a.ctx
4875  if z3_debug():
4876  _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
4877  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4878 
4879 
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:4611
def Ext(a, b)
Definition: z3py.py:4868

◆ Extract()

def z3py.Extract (   high,
  low,
  a 
)
Create a Z3 bit-vector extraction expression.
Extract is overloaded to also work on sequence extraction.
The functions SubString and SubSeq are redirected to Extract.
For this case, the arguments are reinterpreted as:
    high - is a sequence (string)
    low  - is an offset
    a    - is the length to be extracted

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

4128 def Extract(high, low, a):
4129  """Create a Z3 bit-vector extraction expression.
4130  Extract is overloaded to also work on sequence extraction.
4131  The functions SubString and SubSeq are redirected to Extract.
4132  For this case, the arguments are reinterpreted as:
4133  high - is a sequence (string)
4134  low - is an offset
4135  a - is the length to be extracted
4136 
4137  >>> x = BitVec('x', 8)
4138  >>> Extract(6, 2, x)
4139  Extract(6, 2, x)
4140  >>> Extract(6, 2, x).sort()
4141  BitVec(5)
4142  >>> simplify(Extract(StringVal("abcd"),2,1))
4143  "c"
4144  """
4145  if isinstance(high, str):
4146  high = StringVal(high)
4147  if is_seq(high):
4148  s = high
4149  offset, length = _coerce_exprs(low, a, s.ctx)
4150  return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
4151  if z3_debug():
4152  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
4153  _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0,
4154  "First and second arguments must be non negative integers")
4155  _z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
4156  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
4157 
4158 
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,...
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
def Extract(high, low, a)
Definition: z3py.py:4128
def StringVal(s, ctx=None)
Definition: z3py.py:10921

Referenced by SubSeq(), and SubString().

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

8712 def FailIf(p, ctx=None):
8713  """Return a tactic that fails if the probe `p` evaluates to true.
8714  Otherwise, it returns the input goal unmodified.
8715 
8716  In the following example, the tactic applies 'simplify' if and only if there are
8717  more than 2 constraints in the goal.
8718 
8719  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8720  >>> x, y = Ints('x y')
8721  >>> g = Goal()
8722  >>> g.add(x > 0)
8723  >>> g.add(y > 0)
8724  >>> t(g)
8725  [[x > 0, y > 0]]
8726  >>> g.add(x == y + 1)
8727  >>> t(g)
8728  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8729  """
8730  p = _to_probe(p, ctx)
8731  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8732 
8733 
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:8712

◆ FiniteDomainSort()

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

Definition at line 7716 of file z3py.py.

7716 def FiniteDomainSort(name, sz, ctx=None):
7717  """Create a named finite domain sort of a given size sz"""
7718  if not isinstance(name, Symbol):
7719  name = to_symbol(name)
7720  ctx = _get_ctx(ctx)
7721  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7722 
7723 
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:7716

Referenced by Context.MkFiniteDomainSort().

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

7786 def FiniteDomainVal(val, sort, ctx=None):
7787  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7788 
7789  >>> s = FiniteDomainSort('S', 256)
7790  >>> FiniteDomainVal(255, s)
7791  255
7792  >>> FiniteDomainVal('100', s)
7793  100
7794  """
7795  if z3_debug():
7796  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
7797  ctx = sort.ctx
7798  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7799 
7800 
def FiniteDomainVal(val, sort, ctx=None)
Definition: z3py.py:7786
def is_finite_domain_sort(s)
Definition: z3py.py:7724

◆ Float128()

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

Definition at line 9440 of file z3py.py.

9440 def Float128(ctx=None):
9441  """Floating-point 128-bit (quadruple) sort."""
9442  ctx = _get_ctx(ctx)
9443  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
9444 
9445 
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
def Float128(ctx=None)
Definition: z3py.py:9440

◆ Float16()

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

Definition at line 9404 of file z3py.py.

9404 def Float16(ctx=None):
9405  """Floating-point 16-bit (half) sort."""
9406  ctx = _get_ctx(ctx)
9407  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
9408 
9409 
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
def Float16(ctx=None)
Definition: z3py.py:9404

◆ Float32()

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

Definition at line 9416 of file z3py.py.

9416 def Float32(ctx=None):
9417  """Floating-point 32-bit (single) sort."""
9418  ctx = _get_ctx(ctx)
9419  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
9420 
9421 
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:9416

◆ Float64()

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

Definition at line 9428 of file z3py.py.

9428 def Float64(ctx=None):
9429  """Floating-point 64-bit (double) sort."""
9430  ctx = _get_ctx(ctx)
9431  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
9432 
9433 
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
def Float64(ctx=None)
Definition: z3py.py:9428

◆ FloatDouble()

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

Definition at line 9434 of file z3py.py.

9434 def FloatDouble(ctx=None):
9435  """Floating-point 64-bit (double) sort."""
9436  ctx = _get_ctx(ctx)
9437  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
9438 
9439 
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
def FloatDouble(ctx=None)
Definition: z3py.py:9434

◆ FloatHalf()

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

Definition at line 9410 of file z3py.py.

9410 def FloatHalf(ctx=None):
9411  """Floating-point 16-bit (half) sort."""
9412  ctx = _get_ctx(ctx)
9413  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
9414 
9415 
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:9410

◆ FloatQuadruple()

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

Definition at line 9446 of file z3py.py.

9446 def FloatQuadruple(ctx=None):
9447  """Floating-point 128-bit (quadruple) sort."""
9448  ctx = _get_ctx(ctx)
9449  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
9450 
9451 
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:9446

◆ FloatSingle()

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

Definition at line 9422 of file z3py.py.

9422 def FloatSingle(ctx=None):
9423  """Floating-point 32-bit (single) sort."""
9424  ctx = _get_ctx(ctx)
9425  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
9426 
9427 
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
def FloatSingle(ctx=None)
Definition: z3py.py:9422

◆ ForAll()

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

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

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

Definition at line 2222 of file z3py.py.

2222 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2223  """Create a Z3 forall formula.
2224 
2225  The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2226 
2227  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2228  >>> x = Int('x')
2229  >>> y = Int('y')
2230  >>> ForAll([x, y], f(x, y) >= x)
2231  ForAll([x, y], f(x, y) >= x)
2232  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2233  ForAll([x, y], f(x, y) >= x)
2234  >>> ForAll([x, y], f(x, y) >= x, weight=10)
2235  ForAll([x, y], f(x, y) >= x)
2236  """
2237  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2238 
2239 
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2222

Referenced by Fixedpoint.abstract().

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

10072 def FP(name, fpsort, ctx=None):
10073  """Return a floating-point constant named `name`.
10074  `fpsort` is the floating-point sort.
10075  If `ctx=None`, then the global context is used.
10076 
10077  >>> x = FP('x', FPSort(8, 24))
10078  >>> is_fp(x)
10079  True
10080  >>> x.ebits()
10081  8
10082  >>> x.sort()
10083  FPSort(8, 24)
10084  >>> word = FPSort(8, 24)
10085  >>> x2 = FP('x', word)
10086  >>> eq(x, x2)
10087  True
10088  """
10089  if isinstance(fpsort, FPSortRef) and ctx is None:
10090  ctx = fpsort.ctx
10091  else:
10092  ctx = _get_ctx(ctx)
10093  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
10094 
10095 
def FP(name, fpsort, ctx=None)
Definition: z3py.py:10072

Referenced by FPs().

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

10115 def fpAbs(a, ctx=None):
10116  """Create a Z3 floating-point absolute value expression.
10117 
10118  >>> s = FPSort(8, 24)
10119  >>> rm = RNE()
10120  >>> x = FPVal(1.0, s)
10121  >>> fpAbs(x)
10122  fpAbs(1)
10123  >>> y = FPVal(-20.0, s)
10124  >>> y
10125  -1.25*(2**4)
10126  >>> fpAbs(y)
10127  fpAbs(-1.25*(2**4))
10128  >>> fpAbs(-1.25*(2**4))
10129  fpAbs(-1.25*(2**4))
10130  >>> fpAbs(x).sort()
10131  FPSort(8, 24)
10132  """
10133  ctx = _get_ctx(ctx)
10134  [a] = _coerce_fp_expr_list([a], ctx)
10135  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
10136 
10137 
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:10115

◆ 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)
x + y
>>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
fpAdd(RTZ(), x, y)
>>> fpAdd(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10206 of file z3py.py.

10206 def fpAdd(rm, a, b, ctx=None):
10207  """Create a Z3 floating-point addition expression.
10208 
10209  >>> s = FPSort(8, 24)
10210  >>> rm = RNE()
10211  >>> x = FP('x', s)
10212  >>> y = FP('y', s)
10213  >>> fpAdd(rm, x, y)
10214  x + y
10215  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
10216  fpAdd(RTZ(), x, y)
10217  >>> fpAdd(rm, x, y).sort()
10218  FPSort(8, 24)
10219  """
10220  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
10221 
10222 
def fpAdd(rm, a, b, ctx=None)
Definition: z3py.py:10206

Referenced by FPRef.__add__(), and FPRef.__radd__().

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

10528 def fpBVToFP(v, sort, ctx=None):
10529  """Create a Z3 floating-point conversion expression that represents the
10530  conversion from a bit-vector term to a floating-point term.
10531 
10532  >>> x_bv = BitVecVal(0x3F800000, 32)
10533  >>> x_fp = fpBVToFP(x_bv, Float32())
10534  >>> x_fp
10535  fpToFP(1065353216)
10536  >>> simplify(x_fp)
10537  1
10538  """
10539  _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
10540  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
10541  ctx = _get_ctx(ctx)
10542  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
10543 
10544 
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:9456
def fpBVToFP(v, sort, ctx=None)
Definition: z3py.py:10528

◆ 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)
x / y
>>> fpDiv(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10253 of file z3py.py.

10253 def fpDiv(rm, a, b, ctx=None):
10254  """Create a Z3 floating-point division expression.
10255 
10256  >>> s = FPSort(8, 24)
10257  >>> rm = RNE()
10258  >>> x = FP('x', s)
10259  >>> y = FP('y', s)
10260  >>> fpDiv(rm, x, y)
10261  x / y
10262  >>> fpDiv(rm, x, y).sort()
10263  FPSort(8, 24)
10264  """
10265  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
10266 
10267 
def fpDiv(rm, a, b, ctx=None)
Definition: z3py.py:10253

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

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

10436 def fpEQ(a, b, ctx=None):
10437  """Create the Z3 floating-point expression `fpEQ(other, self)`.
10438 
10439  >>> x, y = FPs('x y', FPSort(8, 24))
10440  >>> fpEQ(x, y)
10441  fpEQ(x, y)
10442  >>> fpEQ(x, y).sexpr()
10443  '(fp.eq x y)'
10444  """
10445  return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
10446 
10447 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:10436

Referenced by fpNEQ().

◆ fpFMA()

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

Definition at line 10312 of file z3py.py.

10312 def fpFMA(rm, a, b, c, ctx=None):
10313  """Create a Z3 floating-point fused multiply-add expression.
10314  """
10315  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
10316 
10317 
def fpFMA(rm, a, b, c, ctx=None)
Definition: z3py.py:10312

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

10460 def fpFP(sgn, exp, sig, ctx=None):
10461  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
10462 
10463  >>> s = FPSort(8, 24)
10464  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
10465  >>> print(x)
10466  fpFP(1, 127, 4194304)
10467  >>> xv = FPVal(-1.5, s)
10468  >>> print(xv)
10469  -1.5
10470  >>> slvr = Solver()
10471  >>> slvr.add(fpEQ(x, xv))
10472  >>> slvr.check()
10473  sat
10474  >>> xv = FPVal(+1.5, s)
10475  >>> print(xv)
10476  1.5
10477  >>> slvr = Solver()
10478  >>> slvr.add(fpEQ(x, xv))
10479  >>> slvr.check()
10480  unsat
10481  """
10482  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
10483  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
10484  ctx = _get_ctx(ctx)
10485  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
10486  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
10487 
10488 
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:10460

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

10545 def fpFPToFP(rm, v, sort, ctx=None):
10546  """Create a Z3 floating-point conversion expression that represents the
10547  conversion from a floating-point term to a floating-point term of different precision.
10548 
10549  >>> x_sgl = FPVal(1.0, Float32())
10550  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
10551  >>> x_dbl
10552  fpToFP(RNE(), 1)
10553  >>> simplify(x_dbl)
10554  1
10555  >>> x_dbl.sort()
10556  FPSort(11, 53)
10557  """
10558  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10559  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
10560  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10561  ctx = _get_ctx(ctx)
10562  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10563 
10564 
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 fpFPToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10545
def is_fprm(a)
Definition: z3py.py:9716
def is_fp(a)
Definition: z3py.py:9872

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

10424 def fpGEQ(a, b, ctx=None):
10425  """Create the Z3 floating-point expression `other >= self`.
10426 
10427  >>> x, y = FPs('x y', FPSort(8, 24))
10428  >>> fpGEQ(x, y)
10429  x >= y
10430  >>> (x >= y).sexpr()
10431  '(fp.geq x y)'
10432  """
10433  return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
10434 
10435 
def fpGEQ(a, b, ctx=None)
Definition: z3py.py:10424

Referenced by FPRef.__ge__().

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

10412 def fpGT(a, b, ctx=None):
10413  """Create the Z3 floating-point expression `other > self`.
10414 
10415  >>> x, y = FPs('x y', FPSort(8, 24))
10416  >>> fpGT(x, y)
10417  x > y
10418  >>> (x > y).sexpr()
10419  '(fp.gt x y)'
10420  """
10421  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
10422 
10423 
def fpGT(a, b, ctx=None)
Definition: z3py.py:10412

Referenced by FPRef.__gt__().

◆ fpInfinity()

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

Definition at line 10000 of file z3py.py.

10000 def fpInfinity(s, negative):
10001  """Create a Z3 floating-point +oo or -oo term."""
10002  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10003  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
10004  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
10005 
10006 
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:10000

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

10342 def fpIsInf(a, ctx=None):
10343  """Create a Z3 floating-point isInfinite expression.
10344 
10345  >>> s = FPSort(8, 24)
10346  >>> x = FP('x', s)
10347  >>> fpIsInf(x)
10348  fpIsInf(x)
10349  """
10350  return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
10351 
10352 
def fpIsInf(a, ctx=None)
Definition: z3py.py:10342

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

10330 def fpIsNaN(a, ctx=None):
10331  """Create a Z3 floating-point isNaN expression.
10332 
10333  >>> s = FPSort(8, 24)
10334  >>> x = FP('x', s)
10335  >>> y = FP('y', s)
10336  >>> fpIsNaN(x)
10337  fpIsNaN(x)
10338  """
10339  return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
10340 
10341 
def fpIsNaN(a, ctx=None)
Definition: z3py.py:10330

◆ fpIsNegative()

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

Definition at line 10371 of file z3py.py.

10371 def fpIsNegative(a, ctx=None):
10372  """Create a Z3 floating-point isNegative expression.
10373  """
10374  return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
10375 
10376 
def fpIsNegative(a, ctx=None)
Definition: z3py.py:10371

◆ fpIsNormal()

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

Definition at line 10359 of file z3py.py.

10359 def fpIsNormal(a, ctx=None):
10360  """Create a Z3 floating-point isNormal expression.
10361  """
10362  return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
10363 
10364 
def fpIsNormal(a, ctx=None)
Definition: z3py.py:10359

◆ fpIsPositive()

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

Definition at line 10377 of file z3py.py.

10377 def fpIsPositive(a, ctx=None):
10378  """Create a Z3 floating-point isPositive expression.
10379  """
10380  return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
10381 
10382 
def fpIsPositive(a, ctx=None)
Definition: z3py.py:10377

◆ fpIsSubnormal()

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

Definition at line 10365 of file z3py.py.

10365 def fpIsSubnormal(a, ctx=None):
10366  """Create a Z3 floating-point isSubnormal expression.
10367  """
10368  return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
10369 
10370 
def fpIsSubnormal(a, ctx=None)
Definition: z3py.py:10365

◆ fpIsZero()

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

Definition at line 10353 of file z3py.py.

10353 def fpIsZero(a, ctx=None):
10354  """Create a Z3 floating-point isZero expression.
10355  """
10356  return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
10357 
10358 
def fpIsZero(a, ctx=None)
Definition: z3py.py:10353

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

10400 def fpLEQ(a, b, ctx=None):
10401  """Create the Z3 floating-point expression `other <= self`.
10402 
10403  >>> x, y = FPs('x y', FPSort(8, 24))
10404  >>> fpLEQ(x, y)
10405  x <= y
10406  >>> (x <= y).sexpr()
10407  '(fp.leq x y)'
10408  """
10409  return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
10410 
10411 
def fpLEQ(a, b, ctx=None)
Definition: z3py.py:10400

Referenced by FPRef.__le__().

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

10388 def fpLT(a, b, ctx=None):
10389  """Create the Z3 floating-point expression `other < self`.
10390 
10391  >>> x, y = FPs('x y', FPSort(8, 24))
10392  >>> fpLT(x, y)
10393  x < y
10394  >>> (x < y).sexpr()
10395  '(fp.lt x y)'
10396  """
10397  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
10398 
10399 
def fpLT(a, b, ctx=None)
Definition: z3py.py:10388

Referenced by FPRef.__lt__().

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

10297 def fpMax(a, b, ctx=None):
10298  """Create a Z3 floating-point maximum expression.
10299 
10300  >>> s = FPSort(8, 24)
10301  >>> rm = RNE()
10302  >>> x = FP('x', s)
10303  >>> y = FP('y', s)
10304  >>> fpMax(x, y)
10305  fpMax(x, y)
10306  >>> fpMax(x, y).sort()
10307  FPSort(8, 24)
10308  """
10309  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
10310 
10311 
def fpMax(a, b, ctx=None)
Definition: z3py.py:10297

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

10282 def fpMin(a, b, ctx=None):
10283  """Create a Z3 floating-point minimum expression.
10284 
10285  >>> s = FPSort(8, 24)
10286  >>> rm = RNE()
10287  >>> x = FP('x', s)
10288  >>> y = FP('y', s)
10289  >>> fpMin(x, y)
10290  fpMin(x, y)
10291  >>> fpMin(x, y).sort()
10292  FPSort(8, 24)
10293  """
10294  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
10295 
10296 
def fpMin(a, b, ctx=None)
Definition: z3py.py:10282

◆ fpMinusInfinity()

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

Definition at line 9994 of file z3py.py.

9994 def fpMinusInfinity(s):
9995  """Create a Z3 floating-point -oo term."""
9996  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9997  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9998 
9999 
def fpMinusInfinity(s)
Definition: z3py.py:9994

Referenced by FPVal().

◆ fpMinusZero()

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

Definition at line 10013 of file z3py.py.

10013 def fpMinusZero(s):
10014  """Create a Z3 floating-point -0.0 term."""
10015  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10016  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
10017 
10018 
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.
def fpMinusZero(s)
Definition: z3py.py:10013

Referenced by FPVal().

◆ 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)
x * y
>>> fpMul(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10238 of file z3py.py.

10238 def fpMul(rm, a, b, ctx=None):
10239  """Create a Z3 floating-point multiplication expression.
10240 
10241  >>> s = FPSort(8, 24)
10242  >>> rm = RNE()
10243  >>> x = FP('x', s)
10244  >>> y = FP('y', s)
10245  >>> fpMul(rm, x, y)
10246  x * y
10247  >>> fpMul(rm, x, y).sort()
10248  FPSort(8, 24)
10249  """
10250  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
10251 
10252 
def fpMul(rm, a, b, ctx=None)
Definition: z3py.py:10238

Referenced by FPRef.__mul__(), and FPRef.__rmul__().

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

9960 def fpNaN(s):
9961  """Create a Z3 floating-point NaN term.
9962 
9963  >>> s = FPSort(8, 24)
9964  >>> set_fpa_pretty(True)
9965  >>> fpNaN(s)
9966  NaN
9967  >>> pb = get_fpa_pretty()
9968  >>> set_fpa_pretty(False)
9969  >>> fpNaN(s)
9970  fpNaN(FPSort(8, 24))
9971  >>> set_fpa_pretty(pb)
9972  """
9973  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9974  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9975 
9976 
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
def fpNaN(s)
Definition: z3py.py:9960

Referenced by FPVal().

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

10138 def fpNeg(a, ctx=None):
10139  """Create a Z3 floating-point addition expression.
10140 
10141  >>> s = FPSort(8, 24)
10142  >>> rm = RNE()
10143  >>> x = FP('x', s)
10144  >>> fpNeg(x)
10145  -x
10146  >>> fpNeg(x).sort()
10147  FPSort(8, 24)
10148  """
10149  ctx = _get_ctx(ctx)
10150  [a] = _coerce_fp_expr_list([a], ctx)
10151  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
10152 
10153 
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:10138

Referenced by FPRef.__neg__().

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

10448 def fpNEQ(a, b, ctx=None):
10449  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
10450 
10451  >>> x, y = FPs('x y', FPSort(8, 24))
10452  >>> fpNEQ(x, y)
10453  Not(fpEQ(x, y))
10454  >>> (x != y).sexpr()
10455  '(distinct x y)'
10456  """
10457  return Not(fpEQ(a, b, ctx))
10458 
10459 
def Not(a, ctx=None)
Definition: z3py.py:1815
def fpNEQ(a, b, ctx=None)
Definition: z3py.py:10448

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

9977 def fpPlusInfinity(s):
9978  """Create a Z3 floating-point +oo term.
9979 
9980  >>> s = FPSort(8, 24)
9981  >>> pb = get_fpa_pretty()
9982  >>> set_fpa_pretty(True)
9983  >>> fpPlusInfinity(s)
9984  +oo
9985  >>> set_fpa_pretty(False)
9986  >>> fpPlusInfinity(s)
9987  fpPlusInfinity(FPSort(8, 24))
9988  >>> set_fpa_pretty(pb)
9989  """
9990  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9991  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9992 
9993 
def fpPlusInfinity(s)
Definition: z3py.py:9977

Referenced by FPVal().

◆ fpPlusZero()

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

Definition at line 10007 of file z3py.py.

10007 def fpPlusZero(s):
10008  """Create a Z3 floating-point +0.0 term."""
10009  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10010  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
10011 
10012 
def fpPlusZero(s)
Definition: z3py.py:10007

Referenced by FPVal().

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

10565 def fpRealToFP(rm, v, sort, ctx=None):
10566  """Create a Z3 floating-point conversion expression that represents the
10567  conversion from a real term to a floating-point term.
10568 
10569  >>> x_r = RealVal(1.5)
10570  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
10571  >>> x_fp
10572  fpToFP(RNE(), 3/2)
10573  >>> simplify(x_fp)
10574  1.5
10575  """
10576  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10577  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
10578  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10579  ctx = _get_ctx(ctx)
10580  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10581 
10582 
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 fpRealToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10565
def is_real(a)
Definition: z3py.py:2705

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

10268 def fpRem(a, b, ctx=None):
10269  """Create a Z3 floating-point remainder expression.
10270 
10271  >>> s = FPSort(8, 24)
10272  >>> x = FP('x', s)
10273  >>> y = FP('y', s)
10274  >>> fpRem(x, y)
10275  fpRem(x, y)
10276  >>> fpRem(x, y).sort()
10277  FPSort(8, 24)
10278  """
10279  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
10280 
10281 
def fpRem(a, b, ctx=None)
Definition: z3py.py:10268

Referenced by FPRef.__mod__(), and FPRef.__rmod__().

◆ fpRoundToIntegral()

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

Definition at line 10324 of file z3py.py.

10324 def fpRoundToIntegral(rm, a, ctx=None):
10325  """Create a Z3 floating-point roundToIntegral expression.
10326  """
10327  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
10328 
10329 
def fpRoundToIntegral(rm, a, ctx=None)
Definition: z3py.py:10324

◆ 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)
x + y * z

Definition at line 10096 of file z3py.py.

10096 def FPs(names, fpsort, ctx=None):
10097  """Return an array of floating-point constants.
10098 
10099  >>> x, y, z = FPs('x y z', FPSort(8, 24))
10100  >>> x.sort()
10101  FPSort(8, 24)
10102  >>> x.sbits()
10103  24
10104  >>> x.ebits()
10105  8
10106  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
10107  x + y * z
10108  """
10109  ctx = _get_ctx(ctx)
10110  if isinstance(names, str):
10111  names = names.split(" ")
10112  return [FP(name, fpsort, ctx) for name in names]
10113 
10114 
def FPs(names, fpsort, ctx=None)
Definition: z3py.py:10096

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

10583 def fpSignedToFP(rm, v, sort, ctx=None):
10584  """Create a Z3 floating-point conversion expression that represents the
10585  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
10586 
10587  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10588  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
10589  >>> x_fp
10590  fpToFP(RNE(), 4294967291)
10591  >>> simplify(x_fp)
10592  -1.25*(2**2)
10593  """
10594  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10595  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10596  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10597  ctx = _get_ctx(ctx)
10598  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10599 
10600 
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's complement signed bit-vector term into a term of FloatingPoint sort.
def fpSignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10583

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

9901 def FPSort(ebits, sbits, ctx=None):
9902  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9903 
9904  >>> Single = FPSort(8, 24)
9905  >>> Double = FPSort(11, 53)
9906  >>> Single
9907  FPSort(8, 24)
9908  >>> x = Const('x', Single)
9909  >>> eq(x, FP('x', FPSort(8, 24)))
9910  True
9911  """
9912  ctx = _get_ctx(ctx)
9913  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9914 
9915 
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:9901

Referenced by get_default_fp_sort(), Context.mkFPSort(), Context.MkFPSort(), Context.MkFPSort128(), Context.mkFPSort128(), Context.MkFPSort16(), Context.mkFPSort16(), Context.MkFPSort32(), Context.mkFPSort32(), Context.MkFPSort64(), Context.mkFPSort64(), Context.MkFPSortDouble(), Context.mkFPSortDouble(), Context.MkFPSortHalf(), Context.mkFPSortHalf(), Context.MkFPSortQuadruple(), Context.mkFPSortQuadruple(), Context.MkFPSortSingle(), and Context.mkFPSortSingle().

◆ fpSqrt()

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

Definition at line 10318 of file z3py.py.

10318 def fpSqrt(rm, a, ctx=None):
10319  """Create a Z3 floating-point square root expression.
10320  """
10321  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
10322 
10323 
def fpSqrt(rm, a, ctx=None)
Definition: z3py.py:10318

◆ 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)
x - y
>>> fpSub(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10223 of file z3py.py.

10223 def fpSub(rm, a, b, ctx=None):
10224  """Create a Z3 floating-point subtraction expression.
10225 
10226  >>> s = FPSort(8, 24)
10227  >>> rm = RNE()
10228  >>> x = FP('x', s)
10229  >>> y = FP('y', s)
10230  >>> fpSub(rm, x, y)
10231  x - y
10232  >>> fpSub(rm, x, y).sort()
10233  FPSort(8, 24)
10234  """
10235  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
10236 
10237 
def fpSub(rm, a, b, ctx=None)
Definition: z3py.py:10223

Referenced by FPRef.__rsub__(), and FPRef.__sub__().

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

10489 def fpToFP(a1, a2=None, a3=None, ctx=None):
10490  """Create a Z3 floating-point conversion expression from other term sorts
10491  to floating-point.
10492 
10493  From a bit-vector term in IEEE 754-2008 format:
10494  >>> x = FPVal(1.0, Float32())
10495  >>> x_bv = fpToIEEEBV(x)
10496  >>> simplify(fpToFP(x_bv, Float32()))
10497  1
10498 
10499  From a floating-point term with different precision:
10500  >>> x = FPVal(1.0, Float32())
10501  >>> x_db = fpToFP(RNE(), x, Float64())
10502  >>> x_db.sort()
10503  FPSort(11, 53)
10504 
10505  From a real term:
10506  >>> x_r = RealVal(1.5)
10507  >>> simplify(fpToFP(RNE(), x_r, Float32()))
10508  1.5
10509 
10510  From a signed bit-vector term:
10511  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10512  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
10513  -1.25*(2**2)
10514  """
10515  ctx = _get_ctx(ctx)
10516  if is_bv(a1) and is_fp_sort(a2):
10517  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
10518  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
10519  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10520  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
10521  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10522  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
10523  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10524  else:
10525  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
10526 
10527 
def fpToFP(a1, a2=None, a3=None, ctx=None)
Definition: z3py.py:10489

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

10619 def fpToFPUnsigned(rm, x, s, ctx=None):
10620  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
10621  if z3_debug():
10622  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10623  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
10624  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
10625  ctx = _get_ctx(ctx)
10626  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
10627 
10628 
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's complement unsigned bit-vector term into a term of FloatingPoint sort.
def fpToFPUnsigned(rm, x, s, ctx=None)
Definition: z3py.py:10619

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

10693 def fpToIEEEBV(x, ctx=None):
10694  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
10695 
10696  The size of the resulting bit-vector is automatically determined.
10697 
10698  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
10699  knows only one NaN and it will always produce the same bit-vector representation of
10700  that NaN.
10701 
10702  >>> x = FP('x', FPSort(8, 24))
10703  >>> y = fpToIEEEBV(x)
10704  >>> print(is_fp(x))
10705  True
10706  >>> print(is_bv(y))
10707  True
10708  >>> print(is_fp(y))
10709  False
10710  >>> print(is_bv(x))
10711  False
10712  """
10713  if z3_debug():
10714  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10715  ctx = _get_ctx(ctx)
10716  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
10717 
10718 
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 fpToIEEEBV(x, ctx=None)
Definition: z3py.py:10693

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

10673 def fpToReal(x, ctx=None):
10674  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
10675 
10676  >>> x = FP('x', FPSort(8, 24))
10677  >>> y = fpToReal(x)
10678  >>> print(is_fp(x))
10679  True
10680  >>> print(is_real(y))
10681  True
10682  >>> print(is_fp(y))
10683  False
10684  >>> print(is_real(x))
10685  False
10686  """
10687  if z3_debug():
10688  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10689  ctx = _get_ctx(ctx)
10690  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
10691 
10692 
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:10673

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

10629 def fpToSBV(rm, x, s, ctx=None):
10630  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
10631 
10632  >>> x = FP('x', FPSort(8, 24))
10633  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
10634  >>> print(is_fp(x))
10635  True
10636  >>> print(is_bv(y))
10637  True
10638  >>> print(is_fp(y))
10639  False
10640  >>> print(is_bv(x))
10641  False
10642  """
10643  if z3_debug():
10644  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10645  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10646  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10647  ctx = _get_ctx(ctx)
10648  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10649 
10650 
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:10629

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

10651 def fpToUBV(rm, x, s, ctx=None):
10652  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
10653 
10654  >>> x = FP('x', FPSort(8, 24))
10655  >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
10656  >>> print(is_fp(x))
10657  True
10658  >>> print(is_bv(y))
10659  True
10660  >>> print(is_fp(y))
10661  False
10662  >>> print(is_bv(x))
10663  False
10664  """
10665  if z3_debug():
10666  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10667  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10668  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10669  ctx = _get_ctx(ctx)
10670  return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10671 
10672 
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:10651

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

10601 def fpUnsignedToFP(rm, v, sort, ctx=None):
10602  """Create a Z3 floating-point conversion expression that represents the
10603  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
10604 
10605  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10606  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
10607  >>> x_fp
10608  fpToFPUnsigned(RNE(), 4294967291)
10609  >>> simplify(x_fp)
10610  1*(2**32)
10611  """
10612  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10613  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10614  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10615  ctx = _get_ctx(ctx)
10616  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10617 
10618 
def fpUnsignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10601

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

10026 def FPVal(sig, exp=None, fps=None, ctx=None):
10027  """Return a floating-point value of value `val` and sort `fps`.
10028  If `ctx=None`, then the global context is used.
10029 
10030  >>> v = FPVal(20.0, FPSort(8, 24))
10031  >>> v
10032  1.25*(2**4)
10033  >>> print("0x%.8x" % v.exponent_as_long(False))
10034  0x00000004
10035  >>> v = FPVal(2.25, FPSort(8, 24))
10036  >>> v
10037  1.125*(2**1)
10038  >>> v = FPVal(-2.25, FPSort(8, 24))
10039  >>> v
10040  -1.125*(2**1)
10041  >>> FPVal(-0.0, FPSort(8, 24))
10042  -0.0
10043  >>> FPVal(0.0, FPSort(8, 24))
10044  +0.0
10045  >>> FPVal(+0.0, FPSort(8, 24))
10046  +0.0
10047  """
10048  ctx = _get_ctx(ctx)
10049  if is_fp_sort(exp):
10050  fps = exp
10051  exp = None
10052  elif fps is None:
10053  fps = _dflt_fps(ctx)
10054  _z3_assert(is_fp_sort(fps), "sort mismatch")
10055  if exp is None:
10056  exp = 0
10057  val = _to_float_str(sig)
10058  if val == "NaN" or val == "nan":
10059  return fpNaN(fps)
10060  elif val == "-0.0":
10061  return fpMinusZero(fps)
10062  elif val == "0.0" or val == "+0.0":
10063  return fpPlusZero(fps)
10064  elif val == "+oo" or val == "+inf" or val == "+Inf":
10065  return fpPlusInfinity(fps)
10066  elif val == "-oo" or val == "-inf" or val == "-Inf":
10067  return fpMinusInfinity(fps)
10068  else:
10069  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
10070 
10071 
def FPVal(sig, exp=None, fps=None, ctx=None)
Definition: z3py.py:10026

Referenced by set_default_fp_sort().

◆ fpZero()

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

Definition at line 10019 of file z3py.py.

10019 def fpZero(s, negative):
10020  """Create a Z3 floating-point +0.0 or -0.0 term."""
10021  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10022  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
10023  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
10024 
10025 
def fpZero(s, negative)
Definition: z3py.py:10019

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

1771 def FreshBool(prefix="b", ctx=None):
1772  """Return a fresh Boolean constant in the given context using the given prefix.
1773 
1774  If `ctx=None`, then the global context is used.
1775 
1776  >>> b1 = FreshBool()
1777  >>> b2 = FreshBool()
1778  >>> eq(b1, b2)
1779  False
1780  """
1781  ctx = _get_ctx(ctx)
1782  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1783 
1784 
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.
def FreshBool(prefix="b", ctx=None)
Definition: z3py.py:1771

◆ FreshConst()

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

Definition at line 1464 of file z3py.py.

1464 def FreshConst(sort, prefix="c"):
1465  """Create a fresh constant of a specified sort"""
1466  ctx = _get_ctx(sort.ctx)
1467  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1468 
1469 
def FreshConst(sort, prefix="c")
Definition: z3py.py:1464

◆ FreshFunction()

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

Definition at line 886 of file z3py.py.

886 def FreshFunction(*sig):
887  """Create a new fresh Z3 uninterpreted function with the given sorts.
888  """
889  sig = _get_args(sig)
890  if z3_debug():
891  _z3_assert(len(sig) > 0, "At least two arguments expected")
892  arity = len(sig) - 1
893  rng = sig[arity]
894  if z3_debug():
895  _z3_assert(is_sort(rng), "Z3 sort expected")
896  dom = (z3.Sort * arity)()
897  for i in range(arity):
898  if z3_debug():
899  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
900  dom[i] = sig[i].ast
901  ctx = rng.ctx
902  return FuncDeclRef(Z3_mk_fresh_func_decl(ctx.ref(), "f", arity, dom, rng.ast), ctx)
903 
904 
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
def FreshFunction(*sig)
Definition: z3py.py:886

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

3287 def FreshInt(prefix="x", ctx=None):
3288  """Return a fresh integer constant in the given context using the given prefix.
3289 
3290  >>> x = FreshInt()
3291  >>> y = FreshInt()
3292  >>> eq(x, y)
3293  False
3294  >>> x.sort()
3295  Int
3296  """
3297  ctx = _get_ctx(ctx)
3298  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3299 
3300 
def IntSort(ctx=None)
Definition: z3py.py:3138
def FreshInt(prefix="x", ctx=None)
Definition: z3py.py:3287

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

3344 def FreshReal(prefix="b", ctx=None):
3345  """Return a fresh real constant in the given context using the given prefix.
3346 
3347  >>> x = FreshReal()
3348  >>> y = FreshReal()
3349  >>> eq(x, y)
3350  False
3351  >>> x.sort()
3352  Real
3353  """
3354  ctx = _get_ctx(ctx)
3355  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3356 
3357 
def RealSort(ctx=None)
Definition: z3py.py:3155
def FreshReal(prefix="b", ctx=None)
Definition: z3py.py:3344

◆ Full()

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

Definition at line 10975 of file z3py.py.

10975 def Full(s):
10976  """Create the regular expression that accepts the universal language
10977  >>> e = Full(ReSort(SeqSort(IntSort())))
10978  >>> print(e)
10979  Full(ReSort(Seq(Int)))
10980  >>> e1 = Full(ReSort(StringSort()))
10981  >>> print(e1)
10982  Full(ReSort(String))
10983  """
10984  if isinstance(s, ReSortRef):
10985  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10986  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10987 
10988 
10989 
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
def Full(s)
Definition: z3py.py:10975

◆ FullSet()

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

Definition at line 4931 of file z3py.py.

4931 def FullSet(s):
4932  """Create the full set
4933  >>> FullSet(IntSort())
4934  K(Int, True)
4935  """
4936  ctx = s.ctx
4937  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4938 
4939 
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
def FullSet(s)
Definition: z3py.py:4931

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

863 def Function(name, *sig):
864  """Create a new Z3 uninterpreted function with the given sorts.
865 
866  >>> f = Function('f', IntSort(), IntSort())
867  >>> f(f(0))
868  f(f(0))
869  """
870  sig = _get_args(sig)
871  if z3_debug():
872  _z3_assert(len(sig) > 0, "At least two arguments expected")
873  arity = len(sig) - 1
874  rng = sig[arity]
875  if z3_debug():
876  _z3_assert(is_sort(rng), "Z3 sort expected")
877  dom = (Sort * arity)()
878  for i in range(arity):
879  if z3_debug():
880  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
881  dom[i] = sig[i].ast
882  ctx = rng.ctx
883  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
884 
885 
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 Function(name, *sig)
Definition: z3py.py:863

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

6699 def get_as_array_func(n):
6700  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6701  if z3_debug():
6702  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6703  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6704 
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 is_as_array(n)
Definition: z3py.py:6694
def get_as_array_func(n)
Definition: z3py.py:6699

Referenced by ModelRef.get_interp().

◆ get_ctx()

def z3py.get_ctx (   ctx)

Definition at line 267 of file z3py.py.

267 def get_ctx(ctx):
268  return _get_ctx(ctx)
269 
270 
def get_ctx(ctx)
Definition: z3py.py:267

◆ get_default_fp_sort()

def z3py.get_default_fp_sort (   ctx = None)

Definition at line 9323 of file z3py.py.

9323 def get_default_fp_sort(ctx=None):
9324  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
9325 
9326 
def get_default_fp_sort(ctx=None)
Definition: z3py.py:9323

Referenced by set_default_fp_sort().

◆ get_default_rounding_mode()

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

Definition at line 9290 of file z3py.py.

9290 def get_default_rounding_mode(ctx=None):
9291  """Retrieves the global default rounding mode."""
9292  global _dflt_rounding_mode
9293  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
9294  return RTZ(ctx)
9295  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
9296  return RTN(ctx)
9297  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
9298  return RTP(ctx)
9299  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
9300  return RNE(ctx)
9301  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
9302  return RNA(ctx)
9303 
9304 
def RNE(ctx=None)
Definition: z3py.py:9671
def get_default_rounding_mode(ctx=None)
Definition: z3py.py:9290
def RTZ(ctx=None)
Definition: z3py.py:9711
def RTN(ctx=None)
Definition: z3py.py:9701
def RTP(ctx=None)
Definition: z3py.py:9691
def RNA(ctx=None)
Definition: z3py.py:9681

Referenced by set_default_fp_sort().

◆ get_full_version()

def z3py.get_full_version ( )

Definition at line 101 of file z3py.py.

101 def get_full_version():
102  return Z3_get_full_version()
103 
104 
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:101

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

4676 def get_map_func(a):
4677  """Return the function declaration associated with a Z3 map array expression.
4678 
4679  >>> f = Function('f', IntSort(), IntSort())
4680  >>> b = Array('b', IntSort(), IntSort())
4681  >>> a = Map(f, b)
4682  >>> eq(f, get_map_func(a))
4683  True
4684  >>> get_map_func(a)
4685  f
4686  >>> get_map_func(a)(0)
4687  f(0)
4688  """
4689  if z3_debug():
4690  _z3_assert(is_map(a), "Z3 array map expression expected.")
4691  return FuncDeclRef(
4693  a.ctx_ref(),
4694  Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
4695  ),
4696  ctx=a.ctx,
4697  )
4698 
4699 
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.
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def is_map(a)
Definition: z3py.py:4651
def get_map_func(a)
Definition: z3py.py:4676

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

307 def get_param(name):
308  """Return the value of a Z3 global (or module) parameter
309 
310  >>> get_param('nlsat.reorder')
311  'true'
312  """
313  ptr = (ctypes.c_char_p * 1)()
314  if Z3_global_param_get(str(name), ptr):
315  r = z3core._to_pystr(ptr[0])
316  return r
317  raise Z3Exception("failed to retrieve value for '%s'" % name)
318 
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:307

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

1335 def get_var_index(a):
1336  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1337 
1338  >>> x = Int('x')
1339  >>> y = Int('y')
1340  >>> is_var(x)
1341  False
1342  >>> is_const(x)
1343  True
1344  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1345  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1346  >>> q = ForAll([x, y], f(x, y) == x + y)
1347  >>> q.body()
1348  f(Var(1), Var(0)) == Var(1) + Var(0)
1349  >>> b = q.body()
1350  >>> b.arg(0)
1351  f(Var(1), Var(0))
1352  >>> v1 = b.arg(0).arg(0)
1353  >>> v2 = b.arg(0).arg(1)
1354  >>> v1
1355  Var(1)
1356  >>> v2
1357  Var(0)
1358  >>> get_var_index(v1)
1359  1
1360  >>> get_var_index(v2)
1361  0
1362  """
1363  if z3_debug():
1364  _z3_assert(is_var(a), "Z3 bound variable expected")
1365  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1366 
1367 
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
def is_var(a)
Definition: z3py.py:1310
def get_var_index(a)
Definition: z3py.py:1335

◆ get_version()

def z3py.get_version ( )

Definition at line 92 of file z3py.py.

92 def get_version():
93  major = ctypes.c_uint(0)
94  minor = ctypes.c_uint(0)
95  build = ctypes.c_uint(0)
96  rev = ctypes.c_uint(0)
97  Z3_get_version(major, minor, build, rev)
98  return (major.value, minor.value, build.value, rev.value)
99 
100 
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
def get_version()
Definition: z3py.py:92

◆ get_version_string()

def z3py.get_version_string ( )

Definition at line 83 of file z3py.py.

83 def get_version_string():
84  major = ctypes.c_uint(0)
85  minor = ctypes.c_uint(0)
86  build = ctypes.c_uint(0)
87  rev = ctypes.c_uint(0)
88  Z3_get_version(major, minor, build, rev)
89  return "%s.%s.%s" % (major.value, minor.value, build.value)
90 
91 
def get_version_string()
Definition: z3py.py:83

◆ help_simplify()

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

Definition at line 8796 of file z3py.py.

8796 def help_simplify():
8797  """Return a string describing all options available for Z3 `simplify` procedure."""
8798  print(Z3_simplify_get_help(main_ctx().ref()))
8799 
8800 
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
def help_simplify()
Definition: z3py.py:8796
def main_ctx()
Definition: z3py.py:239

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

1381 def If(a, b, c, ctx=None):
1382  """Create a Z3 if-then-else expression.
1383 
1384  >>> x = Int('x')
1385  >>> y = Int('y')
1386  >>> max = If(x > y, x, y)
1387  >>> max
1388  If(x > y, x, y)
1389  >>> simplify(max)
1390  If(x <= y, y, x)
1391  """
1392  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1393  return Cond(a, b, c, ctx)
1394  else:
1395  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1396  s = BoolSort(ctx)
1397  a = s.cast(a)
1398  b, c = _coerce_exprs(b, c, ctx)
1399  if z3_debug():
1400  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1401  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1402 
1403 
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).

Referenced by BoolRef.__mul__(), ArithRef.__mul__(), and Abs().

◆ Implies()

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

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

Definition at line 1785 of file z3py.py.

1785 def Implies(a, b, ctx=None):
1786  """Create a Z3 implies expression.
1787 
1788  >>> p, q = Bools('p q')
1789  >>> Implies(p, q)
1790  Implies(p, q)
1791  """
1792  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1793  s = BoolSort(ctx)
1794  a = s.cast(a)
1795  b = s.cast(b)
1796  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1797 
1798 
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 Implies(a, b, ctx=None)
Definition: z3py.py:1785

Referenced by Fixedpoint.add_rule(), and Fixedpoint.update_rule().

◆ IndexOf()

def z3py.IndexOf (   s,
  substr,
  offset = None 
)
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 11059 of file z3py.py.

11059 def IndexOf(s, substr, offset=None):
11060  """Retrieve the index of substring within a string starting at a specified offset.
11061  >>> simplify(IndexOf("abcabc", "bc", 0))
11062  1
11063  >>> simplify(IndexOf("abcabc", "bc", 2))
11064  4
11065  """
11066  if offset is None:
11067  offset = IntVal(0)
11068  ctx = None
11069  if is_expr(offset):
11070  ctx = offset.ctx
11071  ctx = _get_ctx2(s, substr, ctx)
11072  s = _coerce_seq(s, ctx)
11073  substr = _coerce_seq(substr, ctx)
11074  if _is_int(offset):
11075  offset = IntVal(offset, ctx)
11076  return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
11077 
11078 
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...
def IndexOf(s, substr, offset=None)
Definition: z3py.py:11059
def IntVal(val, ctx=None)
Definition: z3py.py:3188

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

11172 def InRe(s, re):
11173  """Create regular expression membership test
11174  >>> re = Union(Re("a"),Re("b"))
11175  >>> print (simplify(InRe("a", re)))
11176  True
11177  >>> print (simplify(InRe("b", re)))
11178  True
11179  >>> print (simplify(InRe("c", re)))
11180  False
11181  """
11182  s = _coerce_seq(s, re.ctx)
11183  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
11184 
11185 
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.
def InRe(s, re)
Definition: z3py.py:11172

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

3248 def Int(name, ctx=None):
3249  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3250 
3251  >>> x = Int('x')
3252  >>> is_int(x)
3253  True
3254  >>> is_int(x + 1)
3255  True
3256  """
3257  ctx = _get_ctx(ctx)
3258  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3259 
3260 
def Int(name, ctx=None)
Definition: z3py.py:3248

Referenced by Ints(), and IntVector().

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

3996 def Int2BV(a, num_bits):
3997  """Return the z3 expression Int2BV(a, num_bits).
3998  It is a bit-vector of width num_bits and represents the
3999  modulo of a by 2^num_bits
4000  """
4001  ctx = a.ctx
4002  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
4003 
4004 
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:3996

◆ Intersect()

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

Definition at line 11206 of file z3py.py.

11206 def Intersect(*args):
11207  """Create intersection of regular expressions.
11208  >>> re = Intersect(Re("a"), Re("b"), Re("c"))
11209  """
11210  args = _get_args(args)
11211  sz = len(args)
11212  if z3_debug():
11213  _z3_assert(sz > 0, "At least one argument expected.")
11214  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
11215  if sz == 1:
11216  return args[0]
11217  ctx = args[0].ctx
11218  v = (Ast * sz)()
11219  for i in range(sz):
11220  v[i] = args[i].as_ast()
11221  return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
11222 
11223 
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
def Intersect(*args)
Definition: z3py.py:11206

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

3261 def Ints(names, ctx=None):
3262  """Return a tuple of Integer constants.
3263 
3264  >>> x, y, z = Ints('x y z')
3265  >>> Sum(x, y, z)
3266  x + y + z
3267  """
3268  ctx = _get_ctx(ctx)
3269  if isinstance(names, str):
3270  names = names.split(" ")
3271  return [Int(name, ctx) for name in names]
3272 
3273 
def Ints(names, ctx=None)
Definition: z3py.py:3261

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

3138 def IntSort(ctx=None):
3139  """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
3140 
3141  >>> IntSort()
3142  Int
3143  >>> x = Const('x', IntSort())
3144  >>> is_int(x)
3145  True
3146  >>> x.sort() == IntSort()
3147  True
3148  >>> x.sort() == BoolSort()
3149  False
3150  """
3151  ctx = _get_ctx(ctx)
3152  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
3153 
3154 
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.

Referenced by FreshInt(), Context.getIntSort(), Int(), IntVal(), and Context.mkIntSort().

◆ IntToStr()

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

Definition at line 11114 of file z3py.py.

11114 def IntToStr(s):
11115  """Convert integer expression to string"""
11116  if not is_expr(s):
11117  s = _py2expr(s)
11118  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
11119 
11120 
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
def IntToStr(s)
Definition: z3py.py:11114

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

3188 def IntVal(val, ctx=None):
3189  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3190 
3191  >>> IntVal(1)
3192  1
3193  >>> IntVal("100")
3194  100
3195  """
3196  ctx = _get_ctx(ctx)
3197  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3198 
3199 

Referenced by SeqRef.__getitem__(), BoolRef.__mul__(), SeqRef.at(), AlgebraicNumRef.index(), and IndexOf().

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

3274 def IntVector(prefix, sz, ctx=None):
3275  """Return a list of integer constants of size `sz`.
3276 
3277  >>> X = IntVector('x', 3)
3278  >>> X
3279  [x__0, x__1, x__2]
3280  >>> Sum(X)
3281  x__0 + x__1 + x__2
3282  """
3283  ctx = _get_ctx(ctx)
3284  return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3285 
3286 
def IntVector(prefix, sz, ctx=None)
Definition: z3py.py:3274

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

2792 def is_add(a):
2793  """Return `True` if `a` is an expression of the form b + c.
2794 
2795  >>> x, y = Ints('x y')
2796  >>> is_add(x + y)
2797  True
2798  >>> is_add(x - y)
2799  False
2800  """
2801  return is_app_of(a, Z3_OP_ADD)
2802 
2803 
def is_add(a)
Definition: z3py.py:2792
def is_app_of(a, k)
Definition: z3py.py:1368

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

2778 def is_algebraic_value(a):
2779  """Return `True` if `a` is an algebraic value of sort Real.
2780 
2781  >>> is_algebraic_value(RealVal("3/5"))
2782  False
2783  >>> n = simplify(Sqrt(2))
2784  >>> n
2785  1.4142135623?
2786  >>> is_algebraic_value(n)
2787  True
2788  """
2789  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2790 
2791 
def is_algebraic_value(a)
Definition: z3py.py:2778
def is_arith(a)
Definition: z3py.py:2665

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

1621 def is_and(a):
1622  """Return `True` if `a` is a Z3 and expression.
1623 
1624  >>> p, q = Bools('p q')
1625  >>> is_and(And(p, q))
1626  True
1627  >>> is_and(Or(p, q))
1628  False
1629  """
1630  return is_app_of(a, Z3_OP_AND)
1631 
1632 
def is_and(a)
Definition: z3py.py:1621

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

1265 def is_app(a):
1266  """Return `True` if `a` is a Z3 function application.
1267 
1268  Note that, constants are function applications with 0 arguments.
1269 
1270  >>> a = Int('a')
1271  >>> is_app(a)
1272  True
1273  >>> is_app(a + 1)
1274  True
1275  >>> is_app(IntSort())
1276  False
1277  >>> is_app(1)
1278  False
1279  >>> is_app(IntVal(1))
1280  True
1281  >>> x = Int('x')
1282  >>> is_app(ForAll(x, x >= 0))
1283  False
1284  """
1285  if not isinstance(a, ExprRef):
1286  return False
1287  k = _ast_kind(a.ctx, a)
1288  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
1289 
1290 
def is_app(a)
Definition: z3py.py:1265

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

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

1368 def is_app_of(a, k):
1369  """Return `True` if `a` is an application of the given kind `k`.
1370 
1371  >>> x = Int('x')
1372  >>> n = x + 1
1373  >>> is_app_of(n, Z3_OP_ADD)
1374  True
1375  >>> is_app_of(n, Z3_OP_MUL)
1376  False
1377  """
1378  return is_app(a) and a.decl().kind() == k
1379 
1380 

Referenced by is_add(), is_and(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().

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

2665 def is_arith(a):
2666  """Return `True` if `a` is an arithmetical expression.
2667 
2668  >>> x = Int('x')
2669  >>> is_arith(x)
2670  True
2671  >>> is_arith(x + 1)
2672  True
2673  >>> is_arith(1)
2674  False
2675  >>> is_arith(IntVal(1))
2676  True
2677  >>> y = Real('y')
2678  >>> is_arith(y)
2679  True
2680  >>> is_arith(y + 1)
2681  True
2682  """
2683  return isinstance(a, ArithRef)
2684 
2685 

Referenced by is_algebraic_value(), is_int(), is_int_value(), is_rational_value(), and is_real().

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

2364 def is_arith_sort(s):
2365  """Return `True` if s is an arithmetical sort (type).
2366 
2367  >>> is_arith_sort(IntSort())
2368  True
2369  >>> is_arith_sort(RealSort())
2370  True
2371  >>> is_arith_sort(BoolSort())
2372  False
2373  >>> n = Int('x') + 1
2374  >>> is_arith_sort(n.sort())
2375  True
2376  """
2377  return isinstance(s, ArithSortRef)
2378 
2379 
def is_arith_sort(s)
Definition: z3py.py:2364

Referenced by ArithSortRef.subsort().

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

4611 def is_array(a):
4612  """Return `True` if `a` is a Z3 array expression.
4613 
4614  >>> a = Array('a', IntSort(), IntSort())
4615  >>> is_array(a)
4616  True
4617  >>> is_array(Store(a, 0, 1))
4618  True
4619  >>> is_array(a[0])
4620  False
4621  """
4622  return isinstance(a, ArrayRef)
4623 
4624 

Referenced by Ext(), and Map().

◆ is_array_sort()

def z3py.is_array_sort (   a)

Definition at line 4607 of file z3py.py.

4607 def is_array_sort(a):
4608  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4609 
4610 
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

Referenced by Default(), Ext(), Select(), and Update().

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

6694 def is_as_array(n):
6695  """Return true if n is a Z3 expression of the form (_ as-array f)."""
6696  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6697 
6698 
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....

Referenced by get_as_array_func(), and ModelRef.get_interp().

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

451 def is_ast(a):
452  """Return `True` if `a` is an AST node.
453 
454  >>> is_ast(10)
455  False
456  >>> is_ast(IntVal(10))
457  True
458  >>> is_ast(Int('x'))
459  True
460  >>> is_ast(BoolSort())
461  True
462  >>> is_ast(Function('f', IntSort(), IntSort()))
463  True
464  >>> is_ast("x")
465  False
466  >>> is_ast(Solver())
467  False
468  """
469  return isinstance(a, AstRef)
470 
471 

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

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

1571 def is_bool(a):
1572  """Return `True` if `a` is a Z3 Boolean expression.
1573 
1574  >>> p = Bool('p')
1575  >>> is_bool(p)
1576  True
1577  >>> q = Bool('q')
1578  >>> is_bool(And(p, q))
1579  True
1580  >>> x = Real('x')
1581  >>> is_bool(x)
1582  False
1583  >>> is_bool(x == 0)
1584  True
1585  """
1586  return isinstance(a, BoolRef)
1587 
1588 
def is_bool(a)
Definition: z3py.py:1571

Referenced by is_quantifier(), and prove().

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

3944 def is_bv(a):
3945  """Return `True` if `a` is a Z3 bit-vector expression.
3946 
3947  >>> b = BitVec('b', 32)
3948  >>> is_bv(b)
3949  True
3950  >>> is_bv(b + 10)
3951  True
3952  >>> is_bv(Int('x'))
3953  False
3954  """
3955  return isinstance(a, BitVecRef)
3956 
3957 

Referenced by BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), is_bv_value(), Product(), RepeatBitVec(), SignExt(), Sum(), and ZeroExt().

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

3476 def is_bv_sort(s):
3477  """Return True if `s` is a Z3 bit-vector sort.
3478 
3479  >>> is_bv_sort(BitVecSort(32))
3480  True
3481  >>> is_bv_sort(IntSort())
3482  False
3483  """
3484  return isinstance(s, BitVecSortRef)
3485 
3486 

Referenced by BitVecVal(), fpToSBV(), fpToUBV(), and BitVecSortRef.subsort().

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

3958 def is_bv_value(a):
3959  """Return `True` if `a` is a Z3 bit-vector numeral value.
3960 
3961  >>> b = BitVec('b', 32)
3962  >>> is_bv_value(b)
3963  False
3964  >>> b = BitVecVal(10, 32)
3965  >>> b
3966  10
3967  >>> is_bv_value(b)
3968  True
3969  """
3970  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3971 
3972 
def is_bv_value(a)
Definition: z3py.py:3958

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

1291 def is_const(a):
1292  """Return `True` if `a` is Z3 constant/variable expression.
1293 
1294  >>> a = Int('a')
1295  >>> is_const(a)
1296  True
1297  >>> is_const(a + 1)
1298  False
1299  >>> is_const(1)
1300  False
1301  >>> is_const(IntVal(1))
1302  True
1303  >>> x = Int('x')
1304  >>> is_const(ForAll(x, x >= 0))
1305  False
1306  """
1307  return is_app(a) and a.num_args() == 0
1308 
1309 
def is_const(a)
Definition: z3py.py:1291

Referenced by ModelRef.__getitem__(), Solver.assert_and_track(), Optimize.assert_and_track(), ModelRef.get_interp(), is_quantifier(), and prove().

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

4625 def is_const_array(a):
4626  """Return `True` if `a` is a Z3 constant array.
4627 
4628  >>> a = K(IntSort(), 10)
4629  >>> is_const_array(a)
4630  True
4631  >>> a = Array('a', IntSort(), IntSort())
4632  >>> is_const_array(a)
4633  False
4634  """
4635  return is_app_of(a, Z3_OP_CONST_ARRAY)
4636 
4637 
def is_const_array(a)
Definition: z3py.py:4625

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

4667 def is_default(a):
4668  """Return `True` if `a` is a Z3 default array expression.
4669  >>> d = Default(K(IntSort(), 10))
4670  >>> is_default(d)
4671  True
4672  """
4673  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4674 
4675 
def is_default(a)
Definition: z3py.py:4667

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

1679 def is_distinct(a):
1680  """Return `True` if `a` is a Z3 distinct expression.
1681 
1682  >>> x, y, z = Ints('x y z')
1683  >>> is_distinct(x == y)
1684  False
1685  >>> is_distinct(Distinct(x, y, z))
1686  True
1687  """
1688  return is_app_of(a, Z3_OP_DISTINCT)
1689 
1690 
def is_distinct(a)
Definition: z3py.py:1679

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

2828 def is_div(a):
2829  """Return `True` if `a` is an expression of the form b / c.
2830 
2831  >>> x, y = Reals('x y')
2832  >>> is_div(x / y)
2833  True
2834  >>> is_div(x + y)
2835  False
2836  >>> x, y = Ints('x y')
2837  >>> is_div(x / y)
2838  False
2839  >>> is_idiv(x / y)
2840  True
2841  """
2842  return is_app_of(a, Z3_OP_DIV)
2843 
2844 
def is_div(a)
Definition: z3py.py:2828

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

1669 def is_eq(a):
1670  """Return `True` if `a` is a Z3 equality expression.
1671 
1672  >>> x, y = Ints('x y')
1673  >>> is_eq(x == y)
1674  True
1675  """
1676  return is_app_of(a, Z3_OP_EQ)
1677 
1678 
def is_eq(a)
Definition: z3py.py:1669

Referenced by AstRef.__bool__().

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

1242 def is_expr(a):
1243  """Return `True` if `a` is a Z3 expression.
1244 
1245  >>> a = Int('a')
1246  >>> is_expr(a)
1247  True
1248  >>> is_expr(a + 1)
1249  True
1250  >>> is_expr(IntSort())
1251  False
1252  >>> is_expr(1)
1253  False
1254  >>> is_expr(IntVal(1))
1255  True
1256  >>> x = Int('x')
1257  >>> is_expr(ForAll(x, x >= 0))
1258  True
1259  >>> is_expr(FPVal(1.0))
1260  True
1261  """
1262  return isinstance(a, ExprRef)
1263 
1264 

Referenced by SeqRef.__gt__(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), CharFromBv(), CharIsDigit(), Concat(), deserialize(), AlgebraicNumRef.index(), IndexOf(), IntToStr(), is_quantifier(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), StrFromCode(), StrToCode(), substitute(), substitute_funs(), substitute_vars(), and ModelRef.update_value().

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

1607 def is_false(a):
1608  """Return `True` if `a` is the Z3 false expression.
1609 
1610  >>> p = Bool('p')
1611  >>> is_false(p)
1612  False
1613  >>> is_false(False)
1614  False
1615  >>> is_false(BoolVal(False))
1616  True
1617  """
1618  return is_app_of(a, Z3_OP_FALSE)
1619 
1620 
def is_false(a)
Definition: z3py.py:1607

Referenced by AstRef.__bool__().

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

7747 def is_finite_domain(a):
7748  """Return `True` if `a` is a Z3 finite-domain expression.
7749 
7750  >>> s = FiniteDomainSort('S', 100)
7751  >>> b = Const('b', s)
7752  >>> is_finite_domain(b)
7753  True
7754  >>> is_finite_domain(Int('x'))
7755  False
7756  """
7757  return isinstance(a, FiniteDomainRef)
7758 
7759 
def is_finite_domain(a)
Definition: z3py.py:7747

Referenced by is_finite_domain_value().

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

7724 def is_finite_domain_sort(s):
7725  """Return True if `s` is a Z3 finite-domain sort.
7726 
7727  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7728  True
7729  >>> is_finite_domain_sort(IntSort())
7730  False
7731  """
7732  return isinstance(s, FiniteDomainSortRef)
7733 
7734 

Referenced by FiniteDomainVal().

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

7801 def is_finite_domain_value(a):
7802  """Return `True` if `a` is a Z3 finite-domain value.
7803 
7804  >>> s = FiniteDomainSort('S', 100)
7805  >>> b = Const('b', s)
7806  >>> is_finite_domain_value(b)
7807  False
7808  >>> b = FiniteDomainVal(10, s)
7809  >>> b
7810  10
7811  >>> is_finite_domain_value(b)
7812  True
7813  """
7814  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7815 
7816 
def is_finite_domain_value(a)
Definition: z3py.py:7801

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

9872 def is_fp(a):
9873  """Return `True` if `a` is a Z3 floating-point expression.
9874 
9875  >>> b = FP('b', FPSort(8, 24))
9876  >>> is_fp(b)
9877  True
9878  >>> is_fp(b + 1.0)
9879  True
9880  >>> is_fp(Int('x'))
9881  False
9882  """
9883  return isinstance(a, FPRef)
9884 
9885 

Referenced by fpFPToFP(), fpIsPositive(), fpNeg(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp_value(), and set_default_fp_sort().

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

9456 def is_fp_sort(s):
9457  """Return True if `s` is a Z3 floating-point sort.
9458 
9459  >>> is_fp_sort(FPSort(8, 24))
9460  True
9461  >>> is_fp_sort(IntSort())
9462  False
9463  """
9464  return isinstance(s, FPSortRef)
9465 
9466 

Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), and FPVal().

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

9886 def is_fp_value(a):
9887  """Return `True` if `a` is a Z3 floating-point numeral value.
9888 
9889  >>> b = FP('b', FPSort(8, 24))
9890  >>> is_fp_value(b)
9891  False
9892  >>> b = FPVal(1.0, FPSort(8, 24))
9893  >>> b
9894  1
9895  >>> is_fp_value(b)
9896  True
9897  """
9898  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9899 
9900 
def is_fp_value(a)
Definition: z3py.py:9886

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

9716 def is_fprm(a):
9717  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9718 
9719  >>> rm = RNE()
9720  >>> is_fprm(rm)
9721  True
9722  >>> rm = 1.0
9723  >>> is_fprm(rm)
9724  False
9725  """
9726  return isinstance(a, FPRMRef)
9727 
9728 

Referenced by fpFPToFP(), fpNeg(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), and is_fprm_value().

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

9467 def is_fprm_sort(s):
9468  """Return True if `s` is a Z3 floating-point rounding mode sort.
9469 
9470  >>> is_fprm_sort(FPSort(8, 24))
9471  False
9472  >>> is_fprm_sort(RNE().sort())
9473  True
9474  """
9475  return isinstance(s, FPRMSortRef)
9476 
9477 # FP Expressions
9478 
9479 
def is_fprm_sort(s)
Definition: z3py.py:9467

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

9729 def is_fprm_value(a):
9730  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9731  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9732 
9733 # FP Numerals
9734 
9735 
def is_fprm_value(a)
Definition: z3py.py:9729

Referenced by set_default_rounding_mode().

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

850 def is_func_decl(a):
851  """Return `True` if `a` is a Z3 function declaration.
852 
853  >>> f = Function('f', IntSort(), IntSort())
854  >>> is_func_decl(f)
855  True
856  >>> x = Real('x')
857  >>> is_func_decl(x)
858  False
859  """
860  return isinstance(a, FuncDeclRef)
861 
862 
def is_func_decl(a)
Definition: z3py.py:850

Referenced by Map(), prove(), substitute_funs(), and ModelRef.update_value().

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

2893 def is_ge(a):
2894  """Return `True` if `a` is an expression of the form b >= c.
2895 
2896  >>> x, y = Ints('x y')
2897  >>> is_ge(x >= y)
2898  True
2899  >>> is_ge(x == y)
2900  False
2901  """
2902  return is_app_of(a, Z3_OP_GE)
2903 
2904 
def is_ge(a)
Definition: z3py.py:2893

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

2905 def is_gt(a):
2906  """Return `True` if `a` is an expression of the form b > c.
2907 
2908  >>> x, y = Ints('x y')
2909  >>> is_gt(x > y)
2910  True
2911  >>> is_gt(x == y)
2912  False
2913  """
2914  return is_app_of(a, Z3_OP_GT)
2915 
2916 
def is_gt(a)
Definition: z3py.py:2905

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

2845 def is_idiv(a):
2846  """Return `True` if `a` is an expression of the form b div c.
2847 
2848  >>> x, y = Ints('x y')
2849  >>> is_idiv(x / y)
2850  True
2851  >>> is_idiv(x + y)
2852  False
2853  """
2854  return is_app_of(a, Z3_OP_IDIV)
2855 
2856 
def is_idiv(a)
Definition: z3py.py:2845

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

1645 def is_implies(a):
1646  """Return `True` if `a` is a Z3 implication expression.
1647 
1648  >>> p, q = Bools('p q')
1649  >>> is_implies(Implies(p, q))
1650  True
1651  >>> is_implies(And(p, q))
1652  False
1653  """
1654  return is_app_of(a, Z3_OP_IMPLIES)
1655 
1656 
def is_implies(a)
Definition: z3py.py:1645

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

2686 def is_int(a):
2687  """Return `True` if `a` is an integer expression.
2688 
2689  >>> x = Int('x')
2690  >>> is_int(x + 1)
2691  True
2692  >>> is_int(1)
2693  False
2694  >>> is_int(IntVal(1))
2695  True
2696  >>> y = Real('y')
2697  >>> is_int(y)
2698  False
2699  >>> is_int(y + 1)
2700  False
2701  """
2702  return is_arith(a) and a.is_int()
2703 
2704 
def is_int(a)
Definition: z3py.py:2686

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

2732 def is_int_value(a):
2733  """Return `True` if `a` is an integer value of sort Int.
2734 
2735  >>> is_int_value(IntVal(1))
2736  True
2737  >>> is_int_value(1)
2738  False
2739  >>> is_int_value(Int('x'))
2740  False
2741  >>> n = Int('x') + 1
2742  >>> n
2743  x + 1
2744  >>> n.arg(1)
2745  1
2746  >>> is_int_value(n.arg(1))
2747  True
2748  >>> is_int_value(RealVal("1/3"))
2749  False
2750  >>> is_int_value(RealVal(1))
2751  False
2752  """
2753  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2754 
2755 
def is_int_value(a)
Definition: z3py.py:2732

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

2917 def is_is_int(a):
2918  """Return `True` if `a` is an expression of the form IsInt(b).
2919 
2920  >>> x = Real('x')
2921  >>> is_is_int(IsInt(x))
2922  True
2923  >>> is_is_int(x)
2924  False
2925  """
2926  return is_app_of(a, Z3_OP_IS_INT)
2927 
2928 
def is_is_int(a)
Definition: z3py.py:2917

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

4638 def is_K(a):
4639  """Return `True` if `a` is a Z3 constant array.
4640 
4641  >>> a = K(IntSort(), 10)
4642  >>> is_K(a)
4643  True
4644  >>> a = Array('a', IntSort(), IntSort())
4645  >>> is_K(a)
4646  False
4647  """
4648  return is_app_of(a, Z3_OP_CONST_ARRAY)
4649 
4650 
def is_K(a)
Definition: z3py.py:4638

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

2869 def is_le(a):
2870  """Return `True` if `a` is an expression of the form b <= c.
2871 
2872  >>> x, y = Ints('x y')
2873  >>> is_le(x <= y)
2874  True
2875  >>> is_le(x < y)
2876  False
2877  """
2878  return is_app_of(a, Z3_OP_LE)
2879 
2880 
def is_le(a)
Definition: z3py.py:2869

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

2881 def is_lt(a):
2882  """Return `True` if `a` is an expression of the form b < c.
2883 
2884  >>> x, y = Ints('x y')
2885  >>> is_lt(x < y)
2886  True
2887  >>> is_lt(x == y)
2888  False
2889  """
2890  return is_app_of(a, Z3_OP_LT)
2891 
2892 
def is_lt(a)
Definition: z3py.py:2881

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

4651 def is_map(a):
4652  """Return `True` if `a` is a Z3 map array expression.
4653 
4654  >>> f = Function('f', IntSort(), IntSort())
4655  >>> b = Array('b', IntSort(), IntSort())
4656  >>> a = Map(f, b)
4657  >>> a
4658  Map(f, b)
4659  >>> is_map(a)
4660  True
4661  >>> is_map(b)
4662  False
4663  """
4664  return is_app_of(a, Z3_OP_ARRAY_MAP)
4665 
4666 

Referenced by get_map_func().

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

2857 def is_mod(a):
2858  """Return `True` if `a` is an expression of the form b % c.
2859 
2860  >>> x, y = Ints('x y')
2861  >>> is_mod(x % y)
2862  True
2863  >>> is_mod(x + y)
2864  False
2865  """
2866  return is_app_of(a, Z3_OP_MOD)
2867 
2868 
def is_mod(a)
Definition: z3py.py:2857

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

2804 def is_mul(a):
2805  """Return `True` if `a` is an expression of the form b * c.
2806 
2807  >>> x, y = Ints('x y')
2808  >>> is_mul(x * y)
2809  True
2810  >>> is_mul(x - y)
2811  False
2812  """
2813  return is_app_of(a, Z3_OP_MUL)
2814 
2815 
def is_mul(a)
Definition: z3py.py:2804

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

1657 def is_not(a):
1658  """Return `True` if `a` is a Z3 not expression.
1659 
1660  >>> p = Bool('p')
1661  >>> is_not(p)
1662  False
1663  >>> is_not(Not(p))
1664  True
1665  """
1666  return is_app_of(a, Z3_OP_NOT)
1667 
1668 
def is_not(a)
Definition: z3py.py:1657

Referenced by mk_not().

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

1633 def is_or(a):
1634  """Return `True` if `a` is a Z3 or expression.
1635 
1636  >>> p, q = Bools('p q')
1637  >>> is_or(Or(p, q))
1638  True
1639  >>> is_or(And(p, q))
1640  False
1641  """
1642  return is_app_of(a, Z3_OP_OR)
1643 
1644 
def is_or(a)
Definition: z3py.py:1633

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

1933 def is_pattern(a):
1934  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1935 
1936  >>> f = Function('f', IntSort(), IntSort())
1937  >>> x = Int('x')
1938  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1939  >>> q
1940  ForAll(x, f(x) == 0)
1941  >>> q.num_patterns()
1942  1
1943  >>> is_pattern(q.pattern(0))
1944  True
1945  >>> q.pattern(0)
1946  f(Var(0))
1947  """
1948  return isinstance(a, PatternRef)
1949 
1950 
def is_pattern(a)
Definition: z3py.py:1933

Referenced by is_quantifier(), and MultiPattern().

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

8637 def is_probe(p):
8638  """Return `True` if `p` is a Z3 probe.
8639 
8640  >>> is_probe(Int('x'))
8641  False
8642  >>> is_probe(Probe('memory'))
8643  True
8644  """
8645  return isinstance(p, Probe)
8646 
8647 
def is_probe(p)
Definition: z3py.py:8637

Referenced by eq(), mk_not(), and Not().

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

2173 def is_quantifier(a):
2174  """Return `True` if `a` is a Z3 quantifier.
2175 
2176  >>> f = Function('f', IntSort(), IntSort())
2177  >>> x = Int('x')
2178  >>> q = ForAll(x, f(x) == 0)
2179  >>> is_quantifier(q)
2180  True
2181  >>> is_quantifier(f(x))
2182  False
2183  """
2184  return isinstance(a, QuantifierRef)
2185 
2186 
def is_quantifier(a)
Definition: z3py.py:2173

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

2756 def is_rational_value(a):
2757  """Return `True` if `a` is rational value of sort Real.
2758 
2759  >>> is_rational_value(RealVal(1))
2760  True
2761  >>> is_rational_value(RealVal("3/5"))
2762  True
2763  >>> is_rational_value(IntVal(1))
2764  False
2765  >>> is_rational_value(1)
2766  False
2767  >>> n = Real('x') + 1
2768  >>> n.arg(1)
2769  1
2770  >>> is_rational_value(n.arg(1))
2771  True
2772  >>> is_rational_value(Real('x'))
2773  False
2774  """
2775  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2776 
2777 
def is_rational_value(a)
Definition: z3py.py:2756

◆ is_re()

def z3py.is_re (   s)

Definition at line 11168 of file z3py.py.

11168 def is_re(s):
11169  return isinstance(s, ReRef)
11170 
11171 

Referenced by Concat(), Intersect(), and Union().

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

2705 def is_real(a):
2706  """Return `True` if `a` is a real expression.
2707 
2708  >>> x = Int('x')
2709  >>> is_real(x + 1)
2710  False
2711  >>> y = Real('y')
2712  >>> is_real(y)
2713  True
2714  >>> is_real(y + 1)
2715  True
2716  >>> is_real(1)
2717  False
2718  >>> is_real(RealVal(1))
2719  True
2720  """
2721  return is_arith(a) and a.is_real()
2722 
2723 

Referenced by fpRealToFP(), and fpToFP().

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

4886 def is_select(a):
4887  """Return `True` if `a` is a Z3 array select application.
4888 
4889  >>> a = Array('a', IntSort(), IntSort())
4890  >>> is_select(a)
4891  False
4892  >>> i = Int('i')
4893  >>> is_select(a[i])
4894  True
4895  """
4896  return is_app_of(a, Z3_OP_SELECT)
4897 
4898 
def is_select(a)
Definition: z3py.py:4886

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

10894 def is_seq(a):
10895  """Return `True` if `a` is a Z3 sequence expression.
10896  >>> print (is_seq(Unit(IntVal(0))))
10897  True
10898  >>> print (is_seq(StringVal("abc")))
10899  True
10900  """
10901  return isinstance(a, SeqRef)
10902 
10903 

Referenced by CharIsDigit(), Concat(), and Extract().

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

647 def is_sort(s):
648  """Return `True` if `s` is a Z3 sort.
649 
650  >>> is_sort(IntSort())
651  True
652  >>> is_sort(Int('x'))
653  False
654  >>> is_expr(Int('x'))
655  True
656  """
657  return isinstance(s, SortRef)
658 
659 

Referenced by ArraySort(), CreateDatatypes(), FreshFunction(), Function(), IsSubset(), K(), PropagateFunction(), prove(), RecFunction(), and Var().

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

4899 def is_store(a):
4900  """Return `True` if `a` is a Z3 array store application.
4901 
4902  >>> a = Array('a', IntSort(), IntSort())
4903  >>> is_store(a)
4904  False
4905  >>> is_store(Store(a, 0, 1))
4906  True
4907  """
4908  return is_app_of(a, Z3_OP_STORE)
4909 
def is_store(a)
Definition: z3py.py:4899

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

10904 def is_string(a):
10905  """Return `True` if `a` is a Z3 string expression.
10906  >>> print (is_string(StringVal("ab")))
10907  True
10908  """
10909  return isinstance(a, SeqRef) and a.is_string()
10910 
10911 
def is_string(a)
Definition: z3py.py:10904

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

10912 def is_string_value(a):
10913  """return 'True' if 'a' is a Z3 string constant expression.
10914  >>> print (is_string_value(StringVal("a")))
10915  True
10916  >>> print (is_string_value(StringVal("a") + StringVal("b")))
10917  False
10918  """
10919  return isinstance(a, SeqRef) and a.is_string_value()
10920 
def is_string_value(a)
Definition: z3py.py:10912

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

2816 def is_sub(a):
2817  """Return `True` if `a` is an expression of the form b - c.
2818 
2819  >>> x, y = Ints('x y')
2820  >>> is_sub(x - y)
2821  True
2822  >>> is_sub(x + y)
2823  False
2824  """
2825  return is_app_of(a, Z3_OP_SUB)
2826 
2827 
def is_sub(a)
Definition: z3py.py:2816

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

2944 def is_to_int(a):
2945  """Return `True` if `a` is an expression of the form ToInt(b).
2946 
2947  >>> x = Real('x')
2948  >>> n = ToInt(x)
2949  >>> n
2950  ToInt(x)
2951  >>> is_to_int(n)
2952  True
2953  >>> is_to_int(x)
2954  False
2955  """
2956  return is_app_of(a, Z3_OP_TO_INT)
2957 
2958 
def is_to_int(a)
Definition: z3py.py:2944

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

2929 def is_to_real(a):
2930  """Return `True` if `a` is an expression of the form ToReal(b).
2931 
2932  >>> x = Int('x')
2933  >>> n = ToReal(x)
2934  >>> n
2935  ToReal(x)
2936  >>> is_to_real(n)
2937  True
2938  >>> is_to_real(x)
2939  False
2940  """
2941  return is_app_of(a, Z3_OP_TO_REAL)
2942 
2943 
def is_to_real(a)
Definition: z3py.py:2929

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

1589 def is_true(a):
1590  """Return `True` if `a` is the Z3 true expression.
1591 
1592  >>> p = Bool('p')
1593  >>> is_true(p)
1594  False
1595  >>> is_true(simplify(p == p))
1596  True
1597  >>> x = Real('x')
1598  >>> is_true(x == 0)
1599  False
1600  >>> # True is a Python Boolean expression
1601  >>> is_true(True)
1602  False
1603  """
1604  return is_app_of(a, Z3_OP_TRUE)
1605 
1606 
def is_true(a)
Definition: z3py.py:1589

Referenced by AstRef.__bool__().

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

1310 def is_var(a):
1311  """Return `True` if `a` is variable.
1312 
1313  Z3 uses de-Bruijn indices for representing bound variables in
1314  quantifiers.
1315 
1316  >>> x = Int('x')
1317  >>> is_var(x)
1318  False
1319  >>> is_const(x)
1320  True
1321  >>> f = Function('f', IntSort(), IntSort())
1322  >>> # Z3 replaces x with bound variables when ForAll is executed.
1323  >>> q = ForAll(x, f(x) == x)
1324  >>> b = q.body()
1325  >>> b
1326  f(Var(0)) == Var(0)
1327  >>> b.arg(1)
1328  Var(0)
1329  >>> is_var(b.arg(1))
1330  True
1331  """</