Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

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

Functions

def z3_debug ()
 
def enable_trace (msg)
 
def disable_trace (msg)
 
def get_version_string ()
 
def get_version ()
 
def get_full_version ()
 
def open_log (fname)
 
def append_log (s)
 
def to_symbol (s, ctx=None)
 
def z3_error_handler (c, e)
 
def main_ctx ()
 
def get_ctx (ctx)
 
def set_param (*args, **kws)
 
def reset_params ()
 
def set_option (*args, **kws)
 
def get_param (name)
 
def is_ast (a)
 
def eq (a, b)
 
def is_sort (s)
 
def DeclareSort (name, ctx=None)
 
def is_func_decl (a)
 
def Function (name, *sig)
 
def FreshFunction (*sig)
 
def RecFunction (name, *sig)
 
def RecAddDefinition (f, args, body)
 
def 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 ensure_prop_closures ()
 
def user_prop_push (ctx, cb)
 
def user_prop_pop (ctx, cb, num_scopes)
 
def to_ContextObj (ptr)
 
def user_prop_fresh (ctx, _new_ctx)
 
def to_Ast (ptr)
 
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 8907 of file z3py.py.

8907 def Abs(arg):
8908  """Create the absolute value of an arithmetic expression"""
8909  return If(arg > 0, arg, -arg)
8910 
8911 

◆ AllChar()

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

Definition at line 11273 of file z3py.py.

11273 def AllChar(regex_sort, ctx=None):
11274  """Create a regular expression that accepts all single character strings
11275  """
11276  return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
11277 
11278 # Special Relations
11279 
11280 

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

1840 def And(*args):
1841  """Create a Z3 and-expression or and-probe.
1842 
1843  >>> p, q, r = Bools('p q r')
1844  >>> And(p, q, r)
1845  And(p, q, r)
1846  >>> P = BoolVector('p', 5)
1847  >>> And(P)
1848  And(p__0, p__1, p__2, p__3, p__4)
1849  """
1850  last_arg = None
1851  if len(args) > 0:
1852  last_arg = args[len(args) - 1]
1853  if isinstance(last_arg, Context):
1854  ctx = args[len(args) - 1]
1855  args = args[:len(args) - 1]
1856  elif len(args) == 1 and isinstance(args[0], AstVector):
1857  ctx = args[0].ctx
1858  args = [a for a in args[0]]
1859  else:
1860  ctx = None
1861  args = _get_args(args)
1862  ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1863  if z3_debug():
1864  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1865  if _has_probe(args):
1866  return _probe_and(args, ctx)
1867  else:
1868  args = _coerce_expr_list(args, ctx)
1869  _args, sz = _to_ast_array(args)
1870  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1871 
1872 

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

8272 def AndThen(*ts, **ks):
8273  """Return a tactic that applies the tactics in `*ts` in sequence.
8274 
8275  >>> x, y = Ints('x y')
8276  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
8277  >>> t(And(x == 0, y > x + 1))
8278  [[Not(y <= 1)]]
8279  >>> t(And(x == 0, y > x + 1)).as_expr()
8280  Not(y <= 1)
8281  """
8282  if z3_debug():
8283  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8284  ctx = ks.get("ctx", None)
8285  num = len(ts)
8286  r = ts[0]
8287  for i in range(num - 1):
8288  r = _and_then(r, ts[i + 1], ctx)
8289  return r
8290 
8291 

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 

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

5457 def args2params(arguments, keywords, ctx=None):
5458  """Convert python arguments into a Z3_params object.
5459  A ':' is added to the keywords, and '_' is replaced with '-'
5460 
5461  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5462  (params model true relevancy 2 elim_and true)
5463  """
5464  if z3_debug():
5465  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5466  prev = None
5467  r = ParamsRef(ctx)
5468  for a in arguments:
5469  if prev is None:
5470  prev = a
5471  else:
5472  r.set(prev, a)
5473  prev = None
5474  for k in keywords:
5475  v = keywords[k]
5476  r.set(k, v)
5477  return r
5478 
5479 

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

4724 def Array(name, *sorts):
4725  """Return an array constant named `name` with the given domain and range sorts.
4726 
4727  >>> a = Array('a', IntSort(), IntSort())
4728  >>> a.sort()
4729  Array(Int, Int)
4730  >>> a[0]
4731  a[0]
4732  """
4733  s = ArraySort(sorts)
4734  ctx = s.ctx
4735  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4736 
4737 

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

4691 def ArraySort(*sig):
4692  """Return the Z3 array sort with the given domain and range sorts.
4693 
4694  >>> A = ArraySort(IntSort(), BoolSort())
4695  >>> A
4696  Array(Int, Bool)
4697  >>> A.domain()
4698  Int
4699  >>> A.range()
4700  Bool
4701  >>> AA = ArraySort(IntSort(), A)
4702  >>> AA
4703  Array(Int, Array(Int, Bool))
4704  """
4705  sig = _get_args(sig)
4706  if z3_debug():
4707  _z3_assert(len(sig) > 1, "At least two arguments expected")
4708  arity = len(sig) - 1
4709  r = sig[arity]
4710  d = sig[0]
4711  if z3_debug():
4712  for s in sig:
4713  _z3_assert(is_sort(s), "Z3 sort expected")
4714  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4715  ctx = d.ctx
4716  if len(sig) == 2:
4717  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4718  dom = (Sort * arity)()
4719  for i in range(arity):
4720  dom[i] = sig[i].ast
4721  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4722 
4723 

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

8930 def AtLeast(*args):
8931  """Create an at-most Pseudo-Boolean k constraint.
8932 
8933  >>> a, b, c = Bools('a b c')
8934  >>> f = AtLeast(a, b, c, 2)
8935  """
8936  args = _get_args(args)
8937  if z3_debug():
8938  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8939  ctx = _ctx_from_ast_arg_list(args)
8940  if z3_debug():
8941  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8942  args1 = _coerce_expr_list(args[:-1], ctx)
8943  k = args[-1]
8944  _args, sz = _to_ast_array(args1)
8945  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8946 
8947 

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

8912 def AtMost(*args):
8913  """Create an at-most Pseudo-Boolean k constraint.
8914 
8915  >>> a, b, c = Bools('a b c')
8916  >>> f = AtMost(a, b, c, 2)
8917  """
8918  args = _get_args(args)
8919  if z3_debug():
8920  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8921  ctx = _ctx_from_ast_arg_list(args)
8922  if z3_debug():
8923  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8924  args1 = _coerce_expr_list(args[:-1], ctx)
8925  k = args[-1]
8926  _args, sz = _to_ast_array(args1)
8927  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8928 
8929 

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

4028 def BitVec(name, bv, ctx=None):
4029  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4030  If `ctx=None`, then the global context is used.
4031 
4032  >>> x = BitVec('x', 16)
4033  >>> is_bv(x)
4034  True
4035  >>> x.size()
4036  16
4037  >>> x.sort()
4038  BitVec(16)
4039  >>> word = BitVecSort(16)
4040  >>> x2 = BitVec('x', word)
4041  >>> eq(x, x2)
4042  True
4043  """
4044  if isinstance(bv, BitVecSortRef):
4045  ctx = bv.ctx
4046  else:
4047  ctx = _get_ctx(ctx)
4048  bv = BitVecSort(bv, ctx)
4049  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
4050 
4051 

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

4052 def BitVecs(names, bv, ctx=None):
4053  """Return a tuple of bit-vector constants of size bv.
4054 
4055  >>> x, y, z = BitVecs('x y z', 16)
4056  >>> x.size()
4057  16
4058  >>> x.sort()
4059  BitVec(16)
4060  >>> Sum(x, y, z)
4061  0 + x + y + z
4062  >>> Product(x, y, z)
4063  1*x*y*z
4064  >>> simplify(Product(x, y, z))
4065  x*y*z
4066  """
4067  ctx = _get_ctx(ctx)
4068  if isinstance(names, str):
4069  names = names.split(" ")
4070  return [BitVec(name, bv, ctx) for name in names]
4071 
4072 

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

3996 def BitVecSort(sz, ctx=None):
3997  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3998 
3999  >>> Byte = BitVecSort(8)
4000  >>> Word = BitVecSort(16)
4001  >>> Byte
4002  BitVec(8)
4003  >>> x = Const('x', Byte)
4004  >>> eq(x, BitVec('x', 8))
4005  True
4006  """
4007  ctx = _get_ctx(ctx)
4008  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
4009 
4010 

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

4011 def BitVecVal(val, bv, ctx=None):
4012  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
4013 
4014  >>> v = BitVecVal(10, 32)
4015  >>> v
4016  10
4017  >>> print("0x%.8x" % v.as_long())
4018  0x0000000a
4019  """
4020  if is_bv_sort(bv):
4021  ctx = bv.ctx
4022  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
4023  else:
4024  ctx = _get_ctx(ctx)
4025  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
4026 
4027 

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

1719 def Bool(name, ctx=None):
1720  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1721 
1722  >>> p = Bool('p')
1723  >>> q = Bool('q')
1724  >>> And(p, q)
1725  And(p, q)
1726  """
1727  ctx = _get_ctx(ctx)
1728  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1729 
1730 

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

1731 def Bools(names, ctx=None):
1732  """Return a tuple of Boolean constants.
1733 
1734  `names` is a single string containing all names separated by blank spaces.
1735  If `ctx=None`, then the global context is used.
1736 
1737  >>> p, q, r = Bools('p q r')
1738  >>> And(p, Or(q, r))
1739  And(p, Or(q, r))
1740  """
1741  ctx = _get_ctx(ctx)
1742  if isinstance(names, str):
1743  names = names.split(" ")
1744  return [Bool(name, ctx) for name in names]
1745 
1746 

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

1682 def BoolSort(ctx=None):
1683  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1684 
1685  >>> BoolSort()
1686  Bool
1687  >>> p = Const('p', BoolSort())
1688  >>> is_bool(p)
1689  True
1690  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1691  >>> r(0, 1)
1692  r(0, 1)
1693  >>> is_bool(r(0, 1))
1694  True
1695  """
1696  ctx = _get_ctx(ctx)
1697  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1698 
1699 

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

1700 def BoolVal(val, ctx=None):
1701  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1702 
1703  >>> BoolVal(True)
1704  True
1705  >>> is_true(BoolVal(True))
1706  True
1707  >>> is_true(True)
1708  False
1709  >>> is_false(BoolVal(False))
1710  True
1711  """
1712  ctx = _get_ctx(ctx)
1713  if val:
1714  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1715  else:
1716  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1717 
1718 

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

1747 def BoolVector(prefix, sz, ctx=None):
1748  """Return a list of Boolean constants of size `sz`.
1749 
1750  The constants are named using the given prefix.
1751  If `ctx=None`, then the global context is used.
1752 
1753  >>> P = BoolVector('p', 3)
1754  >>> P
1755  [p__0, p__1, p__2]
1756  >>> And(P)
1757  And(p__0, p__1, p__2)
1758  """
1759  return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]
1760 
1761 

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

3964 def BV2Int(a, is_signed=False):
3965  """Return the Z3 expression BV2Int(a).
3966 
3967  >>> b = BitVec('b', 3)
3968  >>> BV2Int(b).sort()
3969  Int
3970  >>> x = Int('x')
3971  >>> x > BV2Int(b)
3972  x > BV2Int(b)
3973  >>> x > BV2Int(b, is_signed=False)
3974  x > BV2Int(b)
3975  >>> x > BV2Int(b, is_signed=True)
3976  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3977  >>> solve(x > BV2Int(b), b == 1, x < 3)
3978  [x = 2, b = 1]
3979  """
3980  if z3_debug():
3981  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
3982  ctx = a.ctx
3983  # investigate problem with bv2int
3984  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3985 
3986 

◆ BVAddNoOverflow()

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

Definition at line 4450 of file z3py.py.

4450 def BVAddNoOverflow(a, b, signed):
4451  """A predicate the determines that bit-vector addition does not overflow"""
4452  _check_bv_args(a, b)
4453  a, b = _coerce_exprs(a, b)
4454  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4455 
4456 

◆ BVAddNoUnderflow()

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

Definition at line 4457 of file z3py.py.

4457 def BVAddNoUnderflow(a, b):
4458  """A predicate the determines that signed bit-vector addition does not underflow"""
4459  _check_bv_args(a, b)
4460  a, b = _coerce_exprs(a, b)
4461  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4462 
4463 

◆ BVMulNoOverflow()

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

Definition at line 4492 of file z3py.py.

4492 def BVMulNoOverflow(a, b, signed):
4493  """A predicate the determines that bit-vector multiplication does not overflow"""
4494  _check_bv_args(a, b)
4495  a, b = _coerce_exprs(a, b)
4496  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4497 
4498 

◆ BVMulNoUnderflow()

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

Definition at line 4499 of file z3py.py.

4499 def BVMulNoUnderflow(a, b):
4500  """A predicate the determines that bit-vector signed multiplication does not underflow"""
4501  _check_bv_args(a, b)
4502  a, b = _coerce_exprs(a, b)
4503  return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4504 
4505 

◆ BVRedAnd()

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

Definition at line 4436 of file z3py.py.

4436 def BVRedAnd(a):
4437  """Return the reduction-and expression of `a`."""
4438  if z3_debug():
4439  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4440  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4441 
4442 

◆ BVRedOr()

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

Definition at line 4443 of file z3py.py.

4443 def BVRedOr(a):
4444  """Return the reduction-or expression of `a`."""
4445  if z3_debug():
4446  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4447  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4448 
4449 

◆ BVSDivNoOverflow()

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

Definition at line 4478 of file z3py.py.

4478 def BVSDivNoOverflow(a, b):
4479  """A predicate the determines that bit-vector signed division does not overflow"""
4480  _check_bv_args(a, b)
4481  a, b = _coerce_exprs(a, b)
4482  return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4483 
4484 

◆ BVSNegNoOverflow()

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

Definition at line 4485 of file z3py.py.

4485 def BVSNegNoOverflow(a):
4486  """A predicate the determines that bit-vector unary negation does not overflow"""
4487  if z3_debug():
4488  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4489  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4490 
4491 

◆ BVSubNoOverflow()

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

Definition at line 4464 of file z3py.py.

4464 def BVSubNoOverflow(a, b):
4465  """A predicate the determines that bit-vector subtraction does not overflow"""
4466  _check_bv_args(a, b)
4467  a, b = _coerce_exprs(a, b)
4468  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4469 
4470 

◆ BVSubNoUnderflow()

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

Definition at line 4471 of file z3py.py.

4471 def BVSubNoUnderflow(a, b, signed):
4472  """A predicate the determines that bit-vector subtraction does not underflow"""
4473  _check_bv_args(a, b)
4474  a, b = _coerce_exprs(a, b)
4475  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4476 
4477 

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

3415 def Cbrt(a, ctx=None):
3416  """ Return a Z3 expression which represents the cubic root of a.
3417 
3418  >>> x = Real('x')
3419  >>> Cbrt(x)
3420  x**(1/3)
3421  """
3422  if not is_expr(a):
3423  ctx = _get_ctx(ctx)
3424  a = RealVal(a, ctx)
3425  return a ** "1/3"
3426 

◆ CharFromBv()

def z3py.CharFromBv (   ch,
  ctx = None 
)

Definition at line 10831 of file z3py.py.

10831 def CharFromBv(ch, ctx=None):
10832  if not is_expr(ch):
10833  raise Z3Expression("Bit-vector expression needed")
10834  return _to_expr_ref(Z3_mk_char_from_bv(ch.ctx_ref(), ch.as_ast()), ch.ctx)
10835 

◆ CharIsDigit()

def z3py.CharIsDigit (   ch,
  ctx = None 
)

Definition at line 10844 of file z3py.py.

10844 def CharIsDigit(ch, ctx=None):
10845  ch = _coerce_char(ch, ctx)
10846  return ch.is_digit()
10847 

◆ CharSort()

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

Definition at line 10730 of file z3py.py.

10730 def CharSort(ctx=None):
10731  """Create a character sort
10732  >>> ch = CharSort()
10733  >>> print(ch)
10734  Char
10735  """
10736  ctx = _get_ctx(ctx)
10737  return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
10738 
10739 

Referenced by Context.mkCharSort().

◆ CharToBv()

def z3py.CharToBv (   ch,
  ctx = None 
)

Definition at line 10836 of file z3py.py.

10836 def CharToBv(ch, ctx=None):
10837  ch = _coerce_char(ch, ctx)
10838  return ch.to_bv()
10839 

◆ CharToInt()

def z3py.CharToInt (   ch,
  ctx = None 
)

Definition at line 10840 of file z3py.py.

10840 def CharToInt(ch, ctx=None):
10841  ch = _coerce_char(ch, ctx)
10842  return ch.to_int()
10843 

◆ CharVal()

def z3py.CharVal (   ch,
  ctx = None 
)

Definition at line 10823 of file z3py.py.

10823 def CharVal(ch, ctx=None):
10824  ctx = _get_ctx(ctx)
10825  if isinstance(ch, str):
10826  ch = ord(ch)
10827  if not isinstance(ch, int):
10828  raise Z3Exception("character value should be an ordinal")
10829  return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
10830 

Referenced by SeqRef.__gt__().

◆ Complement()

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

Definition at line 11225 of file z3py.py.

11225 def Complement(re):
11226  """Create the complement regular expression."""
11227  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
11228 
11229 

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

4073 def Concat(*args):
4074  """Create a Z3 bit-vector concatenation expression.
4075 
4076  >>> v = BitVecVal(1, 4)
4077  >>> Concat(v, v+1, v)
4078  Concat(Concat(1, 1 + 1), 1)
4079  >>> simplify(Concat(v, v+1, v))
4080  289
4081  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
4082  121
4083  """
4084  args = _get_args(args)
4085  sz = len(args)
4086  if z3_debug():
4087  _z3_assert(sz >= 2, "At least two arguments expected.")
4088 
4089  ctx = None
4090  for a in args:
4091  if is_expr(a):
4092  ctx = a.ctx
4093  break
4094  if is_seq(args[0]) or isinstance(args[0], str):
4095  args = [_coerce_seq(s, ctx) for s in args]
4096  if z3_debug():
4097  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
4098  v = (Ast * sz)()
4099  for i in range(sz):
4100  v[i] = args[i].as_ast()
4101  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
4102 
4103  if is_re(args[0]):
4104  if z3_debug():
4105  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
4106  v = (Ast * sz)()
4107  for i in range(sz):
4108  v[i] = args[i].as_ast()
4109  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
4110 
4111  if z3_debug():
4112  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
4113  r = args[0]
4114  for i in range(sz - 1):
4115  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
4116  return r
4117 
4118 

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

8729 def Cond(p, t1, t2, ctx=None):
8730  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8731 
8732  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8733  """
8734  p = _to_probe(p, ctx)
8735  t1 = _to_tactic(t1, ctx)
8736  t2 = _to_tactic(t2, ctx)
8737  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8738 

Referenced by If().

◆ Const()

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

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

Definition at line 1432 of file z3py.py.

1432 def Const(name, sort):
1433  """Create a constant of the given sort.
1434 
1435  >>> Const('x', IntSort())
1436  x
1437  """
1438  if z3_debug():
1439  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1440  ctx = sort.ctx
1441  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1442 
1443 

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

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

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

11000 def Contains(a, b):
11001  """Check if 'a' contains 'b'
11002  >>> s1 = Contains("abc", "ab")
11003  >>> simplify(s1)
11004  True
11005  >>> s2 = Contains("abc", "bc")
11006  >>> simplify(s2)
11007  True
11008  >>> x, y, z = Strings('x y z')
11009  >>> s3 = Contains(Concat(x,y,z), y)
11010  >>> simplify(s3)
11011  True
11012  """
11013  ctx = _get_ctx2(a, b)
11014  a = _coerce_seq(a, ctx)
11015  b = _coerce_seq(b, ctx)
11016  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11017 
11018 

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

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

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

5349 def DatatypeSort(name, ctx = None):
5350  """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
5351  ctx = _get_ctx(ctx)
5352  return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
5353 

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 

◆ Default()

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

Definition at line 4770 of file z3py.py.

4770 def Default(a):
4771  """ Return a default value for array expression.
4772  >>> b = K(IntSort(), 1)
4773  >>> prove(Default(b) == 1)
4774  proved
4775  """
4776  if z3_debug():
4777  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4778  return a.default()
4779 
4780 

◆ describe_probes()

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

Definition at line 8650 of file z3py.py.

8650 def describe_probes():
8651  """Display a (tabular) description of all available probes in Z3."""
8652  if in_html_mode():
8653  even = True
8654  print('<table border="1" cellpadding="2" cellspacing="0">')
8655  for p in probes():
8656  if even:
8657  print('<tr style="background-color:#CFCFCF">')
8658  even = False
8659  else:
8660  print("<tr>")
8661  even = True
8662  print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
8663  print("</table>")
8664  else:
8665  for p in probes():
8666  print("%s : %s" % (p, probe_description(p)))
8667 
8668 

◆ describe_tactics()

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

Definition at line 8444 of file z3py.py.

8444 def describe_tactics():
8445  """Display a (tabular) description of all available tactics in Z3."""
8446  if in_html_mode():
8447  even = True
8448  print('<table border="1" cellpadding="2" cellspacing="0">')
8449  for t in tactics():
8450  if even:
8451  print('<tr style="background-color:#CFCFCF">')
8452  even = False
8453  else:
8454  print("<tr>")
8455  even = True
8456  print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
8457  print("</table>")
8458  else:
8459  for t in tactics():
8460  print("%s : %s" % (t, tactic_description(t)))
8461 
8462 

◆ 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 

◆ Diff()

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

Definition at line 11268 of file z3py.py.

11268 def Diff(a, b, ctx=None):
11269  """Create the difference regular epression
11270  """
11271  return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)
11272 

◆ 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 

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

5366 def DisjointSum(name, sorts, ctx=None):
5367  """Create a named tagged union sort base on a set of underlying sorts
5368  Example:
5369  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5370  """
5371  sum = Datatype(name, ctx)
5372  for i in range(len(sorts)):
5373  sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
5374  sum = sum.create()
5375  return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
5376 
5377 

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

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

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

10930 def Empty(s):
10931  """Create the empty sequence of the given sort
10932  >>> e = Empty(StringSort())
10933  >>> e2 = StringVal("")
10934  >>> print(e.eq(e2))
10935  True
10936  >>> e3 = Empty(SeqSort(IntSort()))
10937  >>> print(e3)
10938  Empty(Seq(Int))
10939  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10940  >>> print(e4)
10941  Empty(ReSort(Seq(Int)))
10942  """
10943  if isinstance(s, SeqSortRef):
10944  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10945  if isinstance(s, ReSortRef):
10946  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10947  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10948 
10949 

◆ EmptySet()

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

Definition at line 4913 of file z3py.py.

4913 def EmptySet(s):
4914  """Create the empty set
4915  >>> EmptySet(IntSort())
4916  K(Int, False)
4917  """
4918  ctx = s.ctx
4919  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4920 
4921 

◆ 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 

◆ ensure_prop_closures()

def z3py.ensure_prop_closures ( )

Definition at line 11344 of file z3py.py.

11344 def ensure_prop_closures():
11345  global _prop_closures
11346  if _prop_closures is None:
11347  _prop_closures = PropClosures()
11348 
11349 

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

5378 def EnumSort(name, values, ctx=None):
5379  """Return a new enumeration sort named `name` containing the given values.
5380 
5381  The result is a pair (sort, list of constants).
5382  Example:
5383  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5384  """
5385  if z3_debug():
5386  _z3_assert(isinstance(name, str), "Name must be a string")
5387  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
5388  _z3_assert(len(values) > 0, "At least one value expected")
5389  ctx = _get_ctx(ctx)
5390  num = len(values)
5391  _val_names = (Symbol * num)()
5392  for i in range(num):
5393  _val_names[i] = to_symbol(values[i])
5394  _values = (FuncDecl * num)()
5395  _testers = (FuncDecl * num)()
5396  name = to_symbol(name)
5397  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5398  V = []
5399  for i in range(num):
5400  V.append(FuncDeclRef(_values[i], ctx))
5401  V = [a() for a in V]
5402  return S, V
5403 

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 

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

2231 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2232  """Create a Z3 exists formula.
2233 
2234  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2235 
2236 
2237  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2238  >>> x = Int('x')
2239  >>> y = Int('y')
2240  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2241  >>> q
2242  Exists([x, y], f(x, y) >= x)
2243  >>> is_quantifier(q)
2244  True
2245  >>> r = Tactic('nnf')(q).as_expr()
2246  >>> is_quantifier(r)
2247  False
2248  """
2249  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2250 
2251 

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

4859 def Ext(a, b):
4860  """Return extensionality index for one-dimensional arrays.
4861  >> a, b = Consts('a b', SetSort(IntSort()))
4862  >> Ext(a, b)
4863  Ext(a, b)
4864  """
4865  ctx = a.ctx
4866  if z3_debug():
4867  _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
4868  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4869 
4870 

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

4119 def Extract(high, low, a):
4120  """Create a Z3 bit-vector extraction expression.
4121  Extract is overloaded to also work on sequence extraction.
4122  The functions SubString and SubSeq are redirected to Extract.
4123  For this case, the arguments are reinterpreted as:
4124  high - is a sequence (string)
4125  low - is an offset
4126  a - is the length to be extracted
4127 
4128  >>> x = BitVec('x', 8)
4129  >>> Extract(6, 2, x)
4130  Extract(6, 2, x)
4131  >>> Extract(6, 2, x).sort()
4132  BitVec(5)
4133  >>> simplify(Extract(StringVal("abcd"),2,1))
4134  "c"
4135  """
4136  if isinstance(high, str):
4137  high = StringVal(high)
4138  if is_seq(high):
4139  s = high
4140  offset, length = _coerce_exprs(low, a, s.ctx)
4141  return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
4142  if z3_debug():
4143  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
4144  _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0,
4145  "First and second arguments must be non negative integers")
4146  _z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
4147  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
4148 
4149 

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

8687 def FailIf(p, ctx=None):
8688  """Return a tactic that fails if the probe `p` evaluates to true.
8689  Otherwise, it returns the input goal unmodified.
8690 
8691  In the following example, the tactic applies 'simplify' if and only if there are
8692  more than 2 constraints in the goal.
8693 
8694  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8695  >>> x, y = Ints('x y')
8696  >>> g = Goal()
8697  >>> g.add(x > 0)
8698  >>> g.add(y > 0)
8699  >>> t(g)
8700  [[x > 0, y > 0]]
8701  >>> g.add(x == y + 1)
8702  >>> t(g)
8703  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8704  """
8705  p = _to_probe(p, ctx)
8706  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8707 
8708 

◆ FiniteDomainSort()

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

Definition at line 7691 of file z3py.py.

7691 def FiniteDomainSort(name, sz, ctx=None):
7692  """Create a named finite domain sort of a given size sz"""
7693  if not isinstance(name, Symbol):
7694  name = to_symbol(name)
7695  ctx = _get_ctx(ctx)
7696  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7697 
7698 

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

7761 def FiniteDomainVal(val, sort, ctx=None):
7762  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7763 
7764  >>> s = FiniteDomainSort('S', 256)
7765  >>> FiniteDomainVal(255, s)
7766  255
7767  >>> FiniteDomainVal('100', s)
7768  100
7769  """
7770  if z3_debug():
7771  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
7772  ctx = sort.ctx
7773  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7774 
7775 

◆ Float128()

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

Definition at line 9415 of file z3py.py.

9415 def Float128(ctx=None):
9416  """Floating-point 128-bit (quadruple) sort."""
9417  ctx = _get_ctx(ctx)
9418  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
9419 
9420 

◆ Float16()

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

Definition at line 9379 of file z3py.py.

9379 def Float16(ctx=None):
9380  """Floating-point 16-bit (half) sort."""
9381  ctx = _get_ctx(ctx)
9382  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
9383 
9384 

◆ Float32()

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

Definition at line 9391 of file z3py.py.

9391 def Float32(ctx=None):
9392  """Floating-point 32-bit (single) sort."""
9393  ctx = _get_ctx(ctx)
9394  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
9395 
9396 

◆ Float64()

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

Definition at line 9403 of file z3py.py.

9403 def Float64(ctx=None):
9404  """Floating-point 64-bit (double) sort."""
9405  ctx = _get_ctx(ctx)
9406  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
9407 
9408 

◆ FloatDouble()

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

Definition at line 9409 of file z3py.py.

9409 def FloatDouble(ctx=None):
9410  """Floating-point 64-bit (double) sort."""
9411  ctx = _get_ctx(ctx)
9412  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
9413 
9414 

◆ FloatHalf()

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

Definition at line 9385 of file z3py.py.

9385 def FloatHalf(ctx=None):
9386  """Floating-point 16-bit (half) sort."""
9387  ctx = _get_ctx(ctx)
9388  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
9389 
9390 

◆ FloatQuadruple()

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

Definition at line 9421 of file z3py.py.

9421 def FloatQuadruple(ctx=None):
9422  """Floating-point 128-bit (quadruple) sort."""
9423  ctx = _get_ctx(ctx)
9424  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
9425 
9426 

◆ FloatSingle()

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

Definition at line 9397 of file z3py.py.

9397 def FloatSingle(ctx=None):
9398  """Floating-point 32-bit (single) sort."""
9399  ctx = _get_ctx(ctx)
9400  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
9401 
9402 

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

2213 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2214  """Create a Z3 forall formula.
2215 
2216  The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2217 
2218  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2219  >>> x = Int('x')
2220  >>> y = Int('y')
2221  >>> ForAll([x, y], f(x, y) >= x)
2222  ForAll([x, y], f(x, y) >= x)
2223  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2224  ForAll([x, y], f(x, y) >= x)
2225  >>> ForAll([x, y], f(x, y) >= x, weight=10)
2226  ForAll([x, y], f(x, y) >= x)
2227  """
2228  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2229 
2230 

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

10047 def FP(name, fpsort, ctx=None):
10048  """Return a floating-point constant named `name`.
10049  `fpsort` is the floating-point sort.
10050  If `ctx=None`, then the global context is used.
10051 
10052  >>> x = FP('x', FPSort(8, 24))
10053  >>> is_fp(x)
10054  True
10055  >>> x.ebits()
10056  8
10057  >>> x.sort()
10058  FPSort(8, 24)
10059  >>> word = FPSort(8, 24)
10060  >>> x2 = FP('x', word)
10061  >>> eq(x, x2)
10062  True
10063  """
10064  if isinstance(fpsort, FPSortRef) and ctx is None:
10065  ctx = fpsort.ctx
10066  else:
10067  ctx = _get_ctx(ctx)
10068  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
10069 
10070 

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

10090 def fpAbs(a, ctx=None):
10091  """Create a Z3 floating-point absolute value expression.
10092 
10093  >>> s = FPSort(8, 24)
10094  >>> rm = RNE()
10095  >>> x = FPVal(1.0, s)
10096  >>> fpAbs(x)
10097  fpAbs(1)
10098  >>> y = FPVal(-20.0, s)
10099  >>> y
10100  -1.25*(2**4)
10101  >>> fpAbs(y)
10102  fpAbs(-1.25*(2**4))
10103  >>> fpAbs(-1.25*(2**4))
10104  fpAbs(-1.25*(2**4))
10105  >>> fpAbs(x).sort()
10106  FPSort(8, 24)
10107  """
10108  ctx = _get_ctx(ctx)
10109  [a] = _coerce_fp_expr_list([a], ctx)
10110  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
10111 
10112 

◆ fpAdd()

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

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

Definition at line 10181 of file z3py.py.

10181 def fpAdd(rm, a, b, ctx=None):
10182  """Create a Z3 floating-point addition expression.
10183 
10184  >>> s = FPSort(8, 24)
10185  >>> rm = RNE()
10186  >>> x = FP('x', s)
10187  >>> y = FP('y', s)
10188  >>> fpAdd(rm, x, y)
10189  fpAdd(RNE(), x, y)
10190  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
10191  x + y
10192  >>> fpAdd(rm, x, y).sort()
10193  FPSort(8, 24)
10194  """
10195  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
10196 
10197 

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

10503 def fpBVToFP(v, sort, ctx=None):
10504  """Create a Z3 floating-point conversion expression that represents the
10505  conversion from a bit-vector term to a floating-point term.
10506 
10507  >>> x_bv = BitVecVal(0x3F800000, 32)
10508  >>> x_fp = fpBVToFP(x_bv, Float32())
10509  >>> x_fp
10510  fpToFP(1065353216)
10511  >>> simplify(x_fp)
10512  1
10513  """
10514  _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
10515  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
10516  ctx = _get_ctx(ctx)
10517  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
10518 
10519 

◆ fpDiv()

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

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

Definition at line 10228 of file z3py.py.

10228 def fpDiv(rm, a, b, ctx=None):
10229  """Create a Z3 floating-point division expression.
10230 
10231  >>> s = FPSort(8, 24)
10232  >>> rm = RNE()
10233  >>> x = FP('x', s)
10234  >>> y = FP('y', s)
10235  >>> fpDiv(rm, x, y)
10236  fpDiv(RNE(), x, y)
10237  >>> fpDiv(rm, x, y).sort()
10238  FPSort(8, 24)
10239  """
10240  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
10241 
10242 

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

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

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

10287 def fpFMA(rm, a, b, c, ctx=None):
10288  """Create a Z3 floating-point fused multiply-add expression.
10289  """
10290  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
10291 
10292 

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

10435 def fpFP(sgn, exp, sig, ctx=None):
10436  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
10437 
10438  >>> s = FPSort(8, 24)
10439  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
10440  >>> print(x)
10441  fpFP(1, 127, 4194304)
10442  >>> xv = FPVal(-1.5, s)
10443  >>> print(xv)
10444  -1.5
10445  >>> slvr = Solver()
10446  >>> slvr.add(fpEQ(x, xv))
10447  >>> slvr.check()
10448  sat
10449  >>> xv = FPVal(+1.5, s)
10450  >>> print(xv)
10451  1.5
10452  >>> slvr = Solver()
10453  >>> slvr.add(fpEQ(x, xv))
10454  >>> slvr.check()
10455  unsat
10456  """
10457  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
10458  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
10459  ctx = _get_ctx(ctx)
10460  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
10461  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
10462 
10463 

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

10520 def fpFPToFP(rm, v, sort, ctx=None):
10521  """Create a Z3 floating-point conversion expression that represents the
10522  conversion from a floating-point term to a floating-point term of different precision.
10523 
10524  >>> x_sgl = FPVal(1.0, Float32())
10525  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
10526  >>> x_dbl
10527  fpToFP(RNE(), 1)
10528  >>> simplify(x_dbl)
10529  1
10530  >>> x_dbl.sort()
10531  FPSort(11, 53)
10532  """
10533  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10534  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
10535  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10536  ctx = _get_ctx(ctx)
10537  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10538 
10539 

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

10399 def fpGEQ(a, b, ctx=None):
10400  """Create the Z3 floating-point expression `other >= self`.
10401 
10402  >>> x, y = FPs('x y', FPSort(8, 24))
10403  >>> fpGEQ(x, y)
10404  x >= y
10405  >>> (x >= y).sexpr()
10406  '(fp.geq x y)'
10407  """
10408  return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
10409 
10410 

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

10387 def fpGT(a, b, ctx=None):
10388  """Create the Z3 floating-point expression `other > self`.
10389 
10390  >>> x, y = FPs('x y', FPSort(8, 24))
10391  >>> fpGT(x, y)
10392  x > y
10393  >>> (x > y).sexpr()
10394  '(fp.gt x y)'
10395  """
10396  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
10397 
10398 

Referenced by FPRef.__gt__().

◆ fpInfinity()

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

Definition at line 9975 of file z3py.py.

9975 def fpInfinity(s, negative):
9976  """Create a Z3 floating-point +oo or -oo term."""
9977  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9978  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9979  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
9980 
9981 

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

10317 def fpIsInf(a, ctx=None):
10318  """Create a Z3 floating-point isInfinite expression.
10319 
10320  >>> s = FPSort(8, 24)
10321  >>> x = FP('x', s)
10322  >>> fpIsInf(x)
10323  fpIsInf(x)
10324  """
10325  return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
10326 
10327 

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

10305 def fpIsNaN(a, ctx=None):
10306  """Create a Z3 floating-point isNaN expression.
10307 
10308  >>> s = FPSort(8, 24)
10309  >>> x = FP('x', s)
10310  >>> y = FP('y', s)
10311  >>> fpIsNaN(x)
10312  fpIsNaN(x)
10313  """
10314  return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
10315 
10316 

◆ fpIsNegative()

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

Definition at line 10346 of file z3py.py.

10346 def fpIsNegative(a, ctx=None):
10347  """Create a Z3 floating-point isNegative expression.
10348  """
10349  return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
10350 
10351 

◆ fpIsNormal()

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

Definition at line 10334 of file z3py.py.

10334 def fpIsNormal(a, ctx=None):
10335  """Create a Z3 floating-point isNormal expression.
10336  """
10337  return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
10338 
10339 

◆ fpIsPositive()

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

Definition at line 10352 of file z3py.py.

10352 def fpIsPositive(a, ctx=None):
10353  """Create a Z3 floating-point isPositive expression.
10354  """
10355  return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
10356 
10357 

◆ fpIsSubnormal()

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

Definition at line 10340 of file z3py.py.

10340 def fpIsSubnormal(a, ctx=None):
10341  """Create a Z3 floating-point isSubnormal expression.
10342  """
10343  return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
10344 
10345 

◆ fpIsZero()

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

Definition at line 10328 of file z3py.py.

10328 def fpIsZero(a, ctx=None):
10329  """Create a Z3 floating-point isZero expression.
10330  """
10331  return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
10332 
10333 

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

10375 def fpLEQ(a, b, ctx=None):
10376  """Create the Z3 floating-point expression `other <= self`.
10377 
10378  >>> x, y = FPs('x y', FPSort(8, 24))
10379  >>> fpLEQ(x, y)
10380  x <= y
10381  >>> (x <= y).sexpr()
10382  '(fp.leq x y)'
10383  """
10384  return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
10385 
10386 

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

10363 def fpLT(a, b, ctx=None):
10364  """Create the Z3 floating-point expression `other < self`.
10365 
10366  >>> x, y = FPs('x y', FPSort(8, 24))
10367  >>> fpLT(x, y)
10368  x < y
10369  >>> (x < y).sexpr()
10370  '(fp.lt x y)'
10371  """
10372  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
10373 
10374 

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

10272 def fpMax(a, b, ctx=None):
10273  """Create a Z3 floating-point maximum expression.
10274 
10275  >>> s = FPSort(8, 24)
10276  >>> rm = RNE()
10277  >>> x = FP('x', s)
10278  >>> y = FP('y', s)
10279  >>> fpMax(x, y)
10280  fpMax(x, y)
10281  >>> fpMax(x, y).sort()
10282  FPSort(8, 24)
10283  """
10284  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
10285 
10286 

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

10257 def fpMin(a, b, ctx=None):
10258  """Create a Z3 floating-point minimum expression.
10259 
10260  >>> s = FPSort(8, 24)
10261  >>> rm = RNE()
10262  >>> x = FP('x', s)
10263  >>> y = FP('y', s)
10264  >>> fpMin(x, y)
10265  fpMin(x, y)
10266  >>> fpMin(x, y).sort()
10267  FPSort(8, 24)
10268  """
10269  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
10270 
10271 

◆ fpMinusInfinity()

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

Definition at line 9969 of file z3py.py.

9969 def fpMinusInfinity(s):
9970  """Create a Z3 floating-point -oo term."""
9971  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9972  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9973 
9974 

Referenced by FPVal().

◆ fpMinusZero()

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

Definition at line 9988 of file z3py.py.

9988 def fpMinusZero(s):
9989  """Create a Z3 floating-point -0.0 term."""
9990  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9991  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
9992 
9993 

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

Definition at line 10213 of file z3py.py.

10213 def fpMul(rm, a, b, ctx=None):
10214  """Create a Z3 floating-point multiplication expression.
10215 
10216  >>> s = FPSort(8, 24)
10217  >>> rm = RNE()
10218  >>> x = FP('x', s)
10219  >>> y = FP('y', s)
10220  >>> fpMul(rm, x, y)
10221  fpMul(RNE(), x, y)
10222  >>> fpMul(rm, x, y).sort()
10223  FPSort(8, 24)
10224  """
10225  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
10226 
10227 

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

9935 def fpNaN(s):
9936  """Create a Z3 floating-point NaN term.
9937 
9938  >>> s = FPSort(8, 24)
9939  >>> set_fpa_pretty(True)
9940  >>> fpNaN(s)
9941  NaN
9942  >>> pb = get_fpa_pretty()
9943  >>> set_fpa_pretty(False)
9944  >>> fpNaN(s)
9945  fpNaN(FPSort(8, 24))
9946  >>> set_fpa_pretty(pb)
9947  """
9948  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9949  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9950 
9951 

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

10113 def fpNeg(a, ctx=None):
10114  """Create a Z3 floating-point addition expression.
10115 
10116  >>> s = FPSort(8, 24)
10117  >>> rm = RNE()
10118  >>> x = FP('x', s)
10119  >>> fpNeg(x)
10120  -x
10121  >>> fpNeg(x).sort()
10122  FPSort(8, 24)
10123  """
10124  ctx = _get_ctx(ctx)
10125  [a] = _coerce_fp_expr_list([a], ctx)
10126  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
10127 
10128 

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

10423 def fpNEQ(a, b, ctx=None):
10424  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
10425 
10426  >>> x, y = FPs('x y', FPSort(8, 24))
10427  >>> fpNEQ(x, y)
10428  Not(fpEQ(x, y))
10429  >>> (x != y).sexpr()
10430  '(distinct x y)'
10431  """
10432  return Not(fpEQ(a, b, ctx))
10433 
10434 

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

9952 def fpPlusInfinity(s):
9953  """Create a Z3 floating-point +oo term.
9954 
9955  >>> s = FPSort(8, 24)
9956  >>> pb = get_fpa_pretty()
9957  >>> set_fpa_pretty(True)
9958  >>> fpPlusInfinity(s)
9959  +oo
9960  >>> set_fpa_pretty(False)
9961  >>> fpPlusInfinity(s)
9962  fpPlusInfinity(FPSort(8, 24))
9963  >>> set_fpa_pretty(pb)
9964  """
9965  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9966  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9967 
9968 

Referenced by FPVal().

◆ fpPlusZero()

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

Definition at line 9982 of file z3py.py.

9982 def fpPlusZero(s):
9983  """Create a Z3 floating-point +0.0 term."""
9984  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9985  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
9986 
9987 

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

10540 def fpRealToFP(rm, v, sort, ctx=None):
10541  """Create a Z3 floating-point conversion expression that represents the
10542  conversion from a real term to a floating-point term.
10543 
10544  >>> x_r = RealVal(1.5)
10545  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
10546  >>> x_fp
10547  fpToFP(RNE(), 3/2)
10548  >>> simplify(x_fp)
10549  1.5
10550  """
10551  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10552  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
10553  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10554  ctx = _get_ctx(ctx)
10555  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10556 
10557 

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

10243 def fpRem(a, b, ctx=None):
10244  """Create a Z3 floating-point remainder expression.
10245 
10246  >>> s = FPSort(8, 24)
10247  >>> x = FP('x', s)
10248  >>> y = FP('y', s)
10249  >>> fpRem(x, y)
10250  fpRem(x, y)
10251  >>> fpRem(x, y).sort()
10252  FPSort(8, 24)
10253  """
10254  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
10255 
10256 

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

10299 def fpRoundToIntegral(rm, a, ctx=None):
10300  """Create a Z3 floating-point roundToIntegral expression.
10301  """
10302  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
10303 
10304 

◆ FPs()

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

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

Definition at line 10071 of file z3py.py.

10071 def FPs(names, fpsort, ctx=None):
10072  """Return an array of floating-point constants.
10073 
10074  >>> x, y, z = FPs('x y z', FPSort(8, 24))
10075  >>> x.sort()
10076  FPSort(8, 24)
10077  >>> x.sbits()
10078  24
10079  >>> x.ebits()
10080  8
10081  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
10082  fpMul(RNE(), fpAdd(RNE(), x, y), z)
10083  """
10084  ctx = _get_ctx(ctx)
10085  if isinstance(names, str):
10086  names = names.split(" ")
10087  return [FP(name, fpsort, ctx) for name in names]
10088 
10089 

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

10558 def fpSignedToFP(rm, v, sort, ctx=None):
10559  """Create a Z3 floating-point conversion expression that represents the
10560  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
10561 
10562  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10563  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
10564  >>> x_fp
10565  fpToFP(RNE(), 4294967291)
10566  >>> simplify(x_fp)
10567  -1.25*(2**2)
10568  """
10569  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10570  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10571  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10572  ctx = _get_ctx(ctx)
10573  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10574 
10575 

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

9876 def FPSort(ebits, sbits, ctx=None):
9877  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9878 
9879  >>> Single = FPSort(8, 24)
9880  >>> Double = FPSort(11, 53)
9881  >>> Single
9882  FPSort(8, 24)
9883  >>> x = Const('x', Single)
9884  >>> eq(x, FP('x', FPSort(8, 24)))
9885  True
9886  """
9887  ctx = _get_ctx(ctx)
9888  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9889 
9890 

Referenced by get_default_fp_sort(), 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 10293 of file z3py.py.

10293 def fpSqrt(rm, a, ctx=None):
10294  """Create a Z3 floating-point square root expression.
10295  """
10296  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
10297 
10298 

◆ fpSub()

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

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

Definition at line 10198 of file z3py.py.

10198 def fpSub(rm, a, b, ctx=None):
10199  """Create a Z3 floating-point subtraction expression.
10200 
10201  >>> s = FPSort(8, 24)
10202  >>> rm = RNE()
10203  >>> x = FP('x', s)
10204  >>> y = FP('y', s)
10205  >>> fpSub(rm, x, y)
10206  fpSub(RNE(), x, y)
10207  >>> fpSub(rm, x, y).sort()
10208  FPSort(8, 24)
10209  """
10210  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
10211 
10212 

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

10464 def fpToFP(a1, a2=None, a3=None, ctx=None):
10465  """Create a Z3 floating-point conversion expression from other term sorts
10466  to floating-point.
10467 
10468  From a bit-vector term in IEEE 754-2008 format:
10469  >>> x = FPVal(1.0, Float32())
10470  >>> x_bv = fpToIEEEBV(x)
10471  >>> simplify(fpToFP(x_bv, Float32()))
10472  1
10473 
10474  From a floating-point term with different precision:
10475  >>> x = FPVal(1.0, Float32())
10476  >>> x_db = fpToFP(RNE(), x, Float64())
10477  >>> x_db.sort()
10478  FPSort(11, 53)
10479 
10480  From a real term:
10481  >>> x_r = RealVal(1.5)
10482  >>> simplify(fpToFP(RNE(), x_r, Float32()))
10483  1.5
10484 
10485  From a signed bit-vector term:
10486  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10487  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
10488  -1.25*(2**2)
10489  """
10490  ctx = _get_ctx(ctx)
10491  if is_bv(a1) and is_fp_sort(a2):
10492  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
10493  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
10494  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10495  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
10496  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10497  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
10498  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10499  else:
10500  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
10501 
10502 

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

10594 def fpToFPUnsigned(rm, x, s, ctx=None):
10595  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
10596  if z3_debug():
10597  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10598  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
10599  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
10600  ctx = _get_ctx(ctx)
10601  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
10602 
10603 

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

10668 def fpToIEEEBV(x, ctx=None):
10669  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
10670 
10671  The size of the resulting bit-vector is automatically determined.
10672 
10673  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
10674  knows only one NaN and it will always produce the same bit-vector representation of
10675  that NaN.
10676 
10677  >>> x = FP('x', FPSort(8, 24))
10678  >>> y = fpToIEEEBV(x)
10679  >>> print(is_fp(x))
10680  True
10681  >>> print(is_bv(y))
10682  True
10683  >>> print(is_fp(y))
10684  False
10685  >>> print(is_bv(x))
10686  False
10687  """
10688  if z3_debug():
10689  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10690  ctx = _get_ctx(ctx)
10691  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
10692 
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 10648 of file z3py.py.

10648 def fpToReal(x, ctx=None):
10649  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
10650 
10651  >>> x = FP('x', FPSort(8, 24))
10652  >>> y = fpToReal(x)
10653  >>> print(is_fp(x))
10654  True
10655  >>> print(is_real(y))
10656  True
10657  >>> print(is_fp(y))
10658  False
10659  >>> print(is_real(x))
10660  False
10661  """
10662  if z3_debug():
10663  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10664  ctx = _get_ctx(ctx)
10665  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
10666 
10667 

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

10604 def fpToSBV(rm, x, s, ctx=None):
10605  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
10606 
10607  >>> x = FP('x', FPSort(8, 24))
10608  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
10609  >>> print(is_fp(x))
10610  True
10611  >>> print(is_bv(y))
10612  True
10613  >>> print(is_fp(y))
10614  False
10615  >>> print(is_bv(x))
10616  False
10617  """
10618  if z3_debug():
10619  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10620  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10621  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10622  ctx = _get_ctx(ctx)
10623  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10624 
10625 

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

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

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

10576 def fpUnsignedToFP(rm, v, sort, ctx=None):
10577  """Create a Z3 floating-point conversion expression that represents the
10578  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
10579 
10580  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10581  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
10582  >>> x_fp
10583  fpToFPUnsigned(RNE(), 4294967291)
10584  >>> simplify(x_fp)
10585  1*(2**32)
10586  """
10587  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10588  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10589  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10590  ctx = _get_ctx(ctx)
10591  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10592 
10593 

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

10001 def FPVal(sig, exp=None, fps=None, ctx=None):
10002  """Return a floating-point value of value `val` and sort `fps`.
10003  If `ctx=None`, then the global context is used.
10004 
10005  >>> v = FPVal(20.0, FPSort(8, 24))
10006  >>> v
10007  1.25*(2**4)
10008  >>> print("0x%.8x" % v.exponent_as_long(False))
10009  0x00000004
10010  >>> v = FPVal(2.25, FPSort(8, 24))
10011  >>> v
10012  1.125*(2**1)
10013  >>> v = FPVal(-2.25, FPSort(8, 24))
10014  >>> v
10015  -1.125*(2**1)
10016  >>> FPVal(-0.0, FPSort(8, 24))
10017  -0.0
10018  >>> FPVal(0.0, FPSort(8, 24))
10019  +0.0
10020  >>> FPVal(+0.0, FPSort(8, 24))
10021  +0.0
10022  """
10023  ctx = _get_ctx(ctx)
10024  if is_fp_sort(exp):
10025  fps = exp
10026  exp = None
10027  elif fps is None:
10028  fps = _dflt_fps(ctx)
10029  _z3_assert(is_fp_sort(fps), "sort mismatch")
10030  if exp is None:
10031  exp = 0
10032  val = _to_float_str(sig)
10033  if val == "NaN" or val == "nan":
10034  return fpNaN(fps)
10035  elif val == "-0.0":
10036  return fpMinusZero(fps)
10037  elif val == "0.0" or val == "+0.0":
10038  return fpPlusZero(fps)
10039  elif val == "+oo" or val == "+inf" or val == "+Inf":
10040  return fpPlusInfinity(fps)
10041  elif val == "-oo" or val == "-inf" or val == "-Inf":
10042  return fpMinusInfinity(fps)
10043  else:
10044  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
10045 
10046 

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

9994 def fpZero(s, negative):
9995  """Create a Z3 floating-point +0.0 or -0.0 term."""
9996  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9997  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9998  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
9999 
10000 

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

1762 def FreshBool(prefix="b", ctx=None):
1763  """Return a fresh Boolean constant in the given context using the given prefix.
1764 
1765  If `ctx=None`, then the global context is used.
1766 
1767  >>> b1 = FreshBool()
1768  >>> b2 = FreshBool()
1769  >>> eq(b1, b2)
1770  False
1771  """
1772  ctx = _get_ctx(ctx)
1773  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1774 
1775 

◆ FreshConst()

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

Definition at line 1459 of file z3py.py.

1459 def FreshConst(sort, prefix="c"):
1460  """Create a fresh constant of a specified sort"""
1461  ctx = _get_ctx(sort.ctx)
1462  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1463 
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 

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

3278 def FreshInt(prefix="x", ctx=None):
3279  """Return a fresh integer constant in the given context using the given prefix.
3280 
3281  >>> x = FreshInt()
3282  >>> y = FreshInt()
3283  >>> eq(x, y)
3284  False
3285  >>> x.sort()
3286  Int
3287  """
3288  ctx = _get_ctx(ctx)
3289  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3290 
3291 

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

3335 def FreshReal(prefix="b", ctx=None):
3336  """Return a fresh real constant in the given context using the given prefix.
3337 
3338  >>> x = FreshReal()
3339  >>> y = FreshReal()
3340  >>> eq(x, y)
3341  False
3342  >>> x.sort()
3343  Real
3344  """
3345  ctx = _get_ctx(ctx)
3346  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3347 
3348 

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

10950 def Full(s):
10951  """Create the regular expression that accepts the universal language
10952  >>> e = Full(ReSort(SeqSort(IntSort())))
10953  >>> print(e)
10954  Full(ReSort(Seq(Int)))
10955  >>> e1 = Full(ReSort(StringSort()))
10956  >>> print(e1)
10957  Full(ReSort(String))
10958  """
10959  if isinstance(s, ReSortRef):
10960  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10961  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10962 
10963 
10964 

◆ FullSet()

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

Definition at line 4922 of file z3py.py.

4922 def FullSet(s):
4923  """Create the full set
4924  >>> FullSet(IntSort())
4925  K(Int, True)
4926  """
4927  ctx = s.ctx
4928  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4929 
4930 

◆ 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 

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

6690 def get_as_array_func(n):
6691  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6692  if z3_debug():
6693  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6694  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6695 

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 

◆ get_default_fp_sort()

def z3py.get_default_fp_sort (   ctx = None)

Definition at line 9298 of file z3py.py.

9298 def get_default_fp_sort(ctx=None):
9299  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
9300 
9301 

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

9265 def get_default_rounding_mode(ctx=None):
9266  """Retrieves the global default rounding mode."""
9267  global _dflt_rounding_mode
9268  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
9269  return RTZ(ctx)
9270  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
9271  return RTN(ctx)
9272  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
9273  return RTP(ctx)
9274  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
9275  return RNE(ctx)
9276  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
9277  return RNA(ctx)
9278 
9279 

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 

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

4667 def get_map_func(a):
4668  """Return the function declaration associated with a Z3 map array expression.
4669 
4670  >>> f = Function('f', IntSort(), IntSort())
4671  >>> b = Array('b', IntSort(), IntSort())
4672  >>> a = Map(f, b)
4673  >>> eq(f, get_map_func(a))
4674  True
4675  >>> get_map_func(a)
4676  f
4677  >>> get_map_func(a)(0)
4678  f(0)
4679  """
4680  if z3_debug():
4681  _z3_assert(is_map(a), "Z3 array map expression expected.")
4682  return FuncDeclRef(
4684  a.ctx_ref(),
4685  Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
4686  ),
4687  ctx=a.ctx,
4688  )
4689 
4690 

◆ 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 

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

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

◆ 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 

◆ 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 

◆ help_simplify()

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

Definition at line 8771 of file z3py.py.

8771 def help_simplify():
8772  """Return a string describing all options available for Z3 `simplify` procedure."""
8773  print(Z3_simplify_get_help(main_ctx().ref()))
8774 
8775 

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

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

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

1776 def Implies(a, b, ctx=None):
1777  """Create a Z3 implies expression.
1778 
1779  >>> p, q = Bools('p q')
1780  >>> Implies(p, q)
1781  Implies(p, q)
1782  """
1783  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1784  s = BoolSort(ctx)
1785  a = s.cast(a)
1786  b = s.cast(b)
1787  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1788 
1789 

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

11034 def IndexOf(s, substr, offset=None):
11035  """Retrieve the index of substring within a string starting at a specified offset.
11036  >>> simplify(IndexOf("abcabc", "bc", 0))
11037  1
11038  >>> simplify(IndexOf("abcabc", "bc", 2))
11039  4
11040  """
11041  if offset is None:
11042  offset = IntVal(0)
11043  ctx = None
11044  if is_expr(offset):
11045  ctx = offset.ctx
11046  ctx = _get_ctx2(s, substr, ctx)
11047  s = _coerce_seq(s, ctx)
11048  substr = _coerce_seq(substr, ctx)
11049  if _is_int(offset):
11050  offset = IntVal(offset, ctx)
11051  return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
11052 
11053 

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

11147 def InRe(s, re):
11148  """Create regular expression membership test
11149  >>> re = Union(Re("a"),Re("b"))
11150  >>> print (simplify(InRe("a", re)))
11151  True
11152  >>> print (simplify(InRe("b", re)))
11153  True
11154  >>> print (simplify(InRe("c", re)))
11155  False
11156  """
11157  s = _coerce_seq(s, re.ctx)
11158  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
11159 
11160 

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

3239 def Int(name, ctx=None):
3240  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3241 
3242  >>> x = Int('x')
3243  >>> is_int(x)
3244  True
3245  >>> is_int(x + 1)
3246  True
3247  """
3248  ctx = _get_ctx(ctx)
3249  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3250 
3251 

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

3987 def Int2BV(a, num_bits):
3988  """Return the z3 expression Int2BV(a, num_bits).
3989  It is a bit-vector of width num_bits and represents the
3990  modulo of a by 2^num_bits
3991  """
3992  ctx = a.ctx
3993  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
3994 
3995 

◆ Intersect()

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

Definition at line 11181 of file z3py.py.

11181 def Intersect(*args):
11182  """Create intersection of regular expressions.
11183  >>> re = Intersect(Re("a"), Re("b"), Re("c"))
11184  """
11185  args = _get_args(args)
11186  sz = len(args)
11187  if z3_debug():
11188  _z3_assert(sz > 0, "At least one argument expected.")
11189  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
11190  if sz == 1:
11191  return args[0]
11192  ctx = args[0].ctx
11193  v = (Ast * sz)()
11194  for i in range(sz):
11195  v[i] = args[i].as_ast()
11196  return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
11197 
11198 

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

3252 def Ints(names, ctx=None):
3253  """Return a tuple of Integer constants.
3254 
3255  >>> x, y, z = Ints('x y z')
3256  >>> Sum(x, y, z)
3257  x + y + z
3258  """
3259  ctx = _get_ctx(ctx)
3260  if isinstance(names, str):
3261  names = names.split(" ")
3262  return [Int(name, ctx) for name in names]
3263 
3264 

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

3129 def IntSort(ctx=None):
3130  """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
3131 
3132  >>> IntSort()
3133  Int
3134  >>> x = Const('x', IntSort())
3135  >>> is_int(x)
3136  True
3137  >>> x.sort() == IntSort()
3138  True
3139  >>> x.sort() == BoolSort()
3140  False
3141  """
3142  ctx = _get_ctx(ctx)
3143  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
3144 
3145 

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

◆ IntToStr()

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

Definition at line 11089 of file z3py.py.

11089 def IntToStr(s):
11090  """Convert integer expression to string"""
11091  if not is_expr(s):
11092  s = _py2expr(s)
11093  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
11094 
11095 

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

3179 def IntVal(val, ctx=None):
3180  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3181 
3182  >>> IntVal(1)
3183  1
3184  >>> IntVal("100")
3185  100
3186  """
3187  ctx = _get_ctx(ctx)
3188  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3189 
3190 

Referenced by SeqRef.__getitem__(), 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 3265 of file z3py.py.

3265 def IntVector(prefix, sz, ctx=None):
3266  """Return a list of integer constants of size `sz`.
3267 
3268  >>> X = IntVector('x', 3)
3269  >>> X
3270  [x__0, x__1, x__2]
3271  >>> Sum(X)
3272  x__0 + x__1 + x__2
3273  """
3274  ctx = _get_ctx(ctx)
3275  return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3276 
3277 

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

2783 def is_add(a):
2784  """Return `True` if `a` is an expression of the form b + c.
2785 
2786  >>> x, y = Ints('x y')
2787  >>> is_add(x + y)
2788  True
2789  >>> is_add(x - y)
2790  False
2791  """
2792  return is_app_of(a, Z3_OP_ADD)
2793 
2794 

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

2769 def is_algebraic_value(a):
2770  """Return `True` if `a` is an algebraic value of sort Real.
2771 
2772  >>> is_algebraic_value(RealVal("3/5"))
2773  False
2774  >>> n = simplify(Sqrt(2))
2775  >>> n
2776  1.4142135623?
2777  >>> is_algebraic_value(n)
2778  True
2779  """
2780  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2781 
2782 

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

1612 def is_and(a):
1613  """Return `True` if `a` is a Z3 and expression.
1614 
1615  >>> p, q = Bools('p q')
1616  >>> is_and(And(p, q))
1617  True
1618  >>> is_and(Or(p, q))
1619  False
1620  """
1621  return is_app_of(a, Z3_OP_AND)
1622 
1623 

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

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

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

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

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

2656 def is_arith(a):
2657  """Return `True` if `a` is an arithmetical expression.
2658 
2659  >>> x = Int('x')
2660  >>> is_arith(x)
2661  True
2662  >>> is_arith(x + 1)
2663  True
2664  >>> is_arith(1)
2665  False
2666  >>> is_arith(IntVal(1))
2667  True
2668  >>> y = Real('y')
2669  >>> is_arith(y)
2670  True
2671  >>> is_arith(y + 1)
2672  True
2673  """
2674  return isinstance(a, ArithRef)
2675 
2676 

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

2355 def is_arith_sort(s):
2356  """Return `True` if s is an arithmetical sort (type).
2357 
2358  >>> is_arith_sort(IntSort())
2359  True
2360  >>> is_arith_sort(RealSort())
2361  True
2362  >>> is_arith_sort(BoolSort())
2363  False
2364  >>> n = Int('x') + 1
2365  >>> is_arith_sort(n.sort())
2366  True
2367  """
2368  return isinstance(s, ArithSortRef)
2369 
2370 

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

4602 def is_array(a):
4603  """Return `True` if `a` is a Z3 array expression.
4604 
4605  >>> a = Array('a', IntSort(), IntSort())
4606  >>> is_array(a)
4607  True
4608  >>> is_array(Store(a, 0, 1))
4609  True
4610  >>> is_array(a[0])
4611  False
4612  """
4613  return isinstance(a, ArrayRef)
4614 
4615 

Referenced by Ext(), and Map().

◆ is_array_sort()

def z3py.is_array_sort (   a)

Definition at line 4598 of file z3py.py.

4598 def is_array_sort(a):
4599  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4600 
4601 

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

6685 def is_as_array(n):
6686  """Return true if n is a Z3 expression of the form (_ as-array f)."""
6687  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6688 
6689 

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 AstRef.eq(), 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 1562 of file z3py.py.

1562 def is_bool(a):
1563  """Return `True` if `a` is a Z3 Boolean expression.
1564 
1565  >>> p = Bool('p')
1566  >>> is_bool(p)
1567  True
1568  >>> q = Bool('q')
1569  >>> is_bool(And(p, q))
1570  True
1571  >>> x = Real('x')
1572  >>> is_bool(x)
1573  False
1574  >>> is_bool(x == 0)
1575  True
1576  """
1577  return isinstance(a, BoolRef)
1578 
1579 

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

3935 def is_bv(a):
3936  """Return `True` if `a` is a Z3 bit-vector expression.
3937 
3938  >>> b = BitVec('b', 32)
3939  >>> is_bv(b)
3940  True
3941  >>> is_bv(b + 10)
3942  True
3943  >>> is_bv(Int('x'))
3944  False
3945  """
3946  return isinstance(a, BitVecRef)
3947 
3948 

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

3467 def is_bv_sort(s):
3468  """Return True if `s` is a Z3 bit-vector sort.
3469 
3470  >>> is_bv_sort(BitVecSort(32))
3471  True
3472  >>> is_bv_sort(IntSort())
3473  False
3474  """
3475  return isinstance(s, BitVecSortRef)
3476 
3477 

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

3949 def is_bv_value(a):
3950  """Return `True` if `a` is a Z3 bit-vector numeral value.
3951 
3952  >>> b = BitVec('b', 32)
3953  >>> is_bv_value(b)
3954  False
3955  >>> b = BitVecVal(10, 32)
3956  >>> b
3957  10
3958  >>> is_bv_value(b)
3959  True
3960  """
3961  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3962 
3963 

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

1286 def is_const(a):
1287  """Return `True` if `a` is Z3 constant/variable expression.
1288 
1289  >>> a = Int('a')
1290  >>> is_const(a)
1291  True
1292  >>> is_const(a + 1)
1293  False
1294  >>> is_const(1)
1295  False
1296  >>> is_const(IntVal(1))
1297  True
1298  >>> x = Int('x')
1299  >>> is_const(ForAll(x, x >= 0))
1300  False
1301  """
1302  return is_app(a) and a.num_args() == 0
1303 
1304 

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

4616 def is_const_array(a):
4617  """Return `True` if `a` is a Z3 constant array.
4618 
4619  >>> a = K(IntSort(), 10)
4620  >>> is_const_array(a)
4621  True
4622  >>> a = Array('a', IntSort(), IntSort())
4623  >>> is_const_array(a)
4624  False
4625  """
4626  return is_app_of(a, Z3_OP_CONST_ARRAY)
4627 
4628 

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

4658 def is_default(a):
4659  """Return `True` if `a` is a Z3 default array expression.
4660  >>> d = Default(K(IntSort(), 10))
4661  >>> is_default(d)
4662  True
4663  """
4664  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4665 
4666 

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

1670 def is_distinct(a):
1671  """Return `True` if `a` is a Z3 distinct expression.
1672 
1673  >>> x, y, z = Ints('x y z')
1674  >>> is_distinct(x == y)
1675  False
1676  >>> is_distinct(Distinct(x, y, z))
1677  True
1678  """
1679  return is_app_of(a, Z3_OP_DISTINCT)
1680 
1681 

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

2819 def is_div(a):
2820  """Return `True` if `a` is an expression of the form b / c.
2821 
2822  >>> x, y = Reals('x y')
2823  >>> is_div(x / y)
2824  True
2825  >>> is_div(x + y)
2826  False
2827  >>> x, y = Ints('x y')
2828  >>> is_div(x / y)
2829  False
2830  >>> is_idiv(x / y)
2831  True
2832  """
2833  return is_app_of(a, Z3_OP_DIV)
2834 
2835 

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

1660 def is_eq(a):
1661  """Return `True` if `a` is a Z3 equality expression.
1662 
1663  >>> x, y = Ints('x y')
1664  >>> is_eq(x == y)
1665  True
1666  """
1667  return is_app_of(a, Z3_OP_EQ)
1668 
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 1237 of file z3py.py.

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

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

1598 def is_false(a):
1599  """Return `True` if `a` is the Z3 false expression.
1600 
1601  >>> p = Bool('p')
1602  >>> is_false(p)
1603  False
1604  >>> is_false(False)
1605  False
1606  >>> is_false(BoolVal(False))
1607  True
1608  """
1609  return is_app_of(a, Z3_OP_FALSE)
1610 
1611 

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

7722 def is_finite_domain(a):
7723  """Return `True` if `a` is a Z3 finite-domain expression.
7724 
7725  >>> s = FiniteDomainSort('S', 100)
7726  >>> b = Const('b', s)
7727  >>> is_finite_domain(b)
7728  True
7729  >>> is_finite_domain(Int('x'))
7730  False
7731  """
7732  return isinstance(a, FiniteDomainRef)
7733 
7734 

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

7699 def is_finite_domain_sort(s):
7700  """Return True if `s` is a Z3 finite-domain sort.
7701 
7702  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7703  True
7704  >>> is_finite_domain_sort(IntSort())
7705  False
7706  """
7707  return isinstance(s, FiniteDomainSortRef)
7708 
7709 

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

7776 def is_finite_domain_value(a):
7777  """Return `True` if `a` is a Z3 finite-domain value.
7778 
7779  >>> s = FiniteDomainSort('S', 100)
7780  >>> b = Const('b', s)
7781  >>> is_finite_domain_value(b)
7782  False
7783  >>> b = FiniteDomainVal(10, s)
7784  >>> b
7785  10
7786  >>> is_finite_domain_value(b)
7787  True
7788  """
7789  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7790 
7791 

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

9847 def is_fp(a):
9848  """Return `True` if `a` is a Z3 floating-point expression.
9849 
9850  >>> b = FP('b', FPSort(8, 24))
9851  >>> is_fp(b)
9852  True
9853  >>> is_fp(b + 1.0)
9854  True
9855  >>> is_fp(Int('x'))
9856  False
9857  """
9858  return isinstance(a, FPRef)
9859 
9860 

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

9431 def is_fp_sort(s):
9432  """Return True if `s` is a Z3 floating-point sort.
9433 
9434  >>> is_fp_sort(FPSort(8, 24))
9435  True
9436  >>> is_fp_sort(IntSort())
9437  False
9438  """
9439  return isinstance(s, FPSortRef)
9440 
9441 

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

9861 def is_fp_value(a):
9862  """Return `True` if `a` is a Z3 floating-point numeral value.
9863 
9864  >>> b = FP('b', FPSort(8, 24))
9865  >>> is_fp_value(b)
9866  False
9867  >>> b = FPVal(1.0, FPSort(8, 24))
9868  >>> b
9869  1
9870  >>> is_fp_value(b)
9871  True
9872  """
9873  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9874 
9875 

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

9691 def is_fprm(a):
9692  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9693 
9694  >>> rm = RNE()
9695  >>> is_fprm(rm)
9696  True
9697  >>> rm = 1.0
9698  >>> is_fprm(rm)
9699  False
9700  """
9701  return isinstance(a, FPRMRef)
9702 
9703 

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

9442 def is_fprm_sort(s):
9443  """Return True if `s` is a Z3 floating-point rounding mode sort.
9444 
9445  >>> is_fprm_sort(FPSort(8, 24))
9446  False
9447  >>> is_fprm_sort(RNE().sort())
9448  True
9449  """
9450  return isinstance(s, FPRMSortRef)
9451 
9452 # FP Expressions
9453 
9454 

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

9704 def is_fprm_value(a):
9705  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9706  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9707 
9708 # FP Numerals
9709 
9710 

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 

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

2884 def is_ge(a):
2885  """Return `True` if `a` is an expression of the form b >= c.
2886 
2887  >>> x, y = Ints('x y')
2888  >>> is_ge(x >= y)
2889  True
2890  >>> is_ge(x == y)
2891  False
2892  """
2893  return is_app_of(a, Z3_OP_GE)
2894 
2895 

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

2896 def is_gt(a):
2897  """Return `True` if `a` is an expression of the form b > c.
2898 
2899  >>> x, y = Ints('x y')
2900  >>> is_gt(x > y)
2901  True
2902  >>> is_gt(x == y)
2903  False
2904  """
2905  return is_app_of(a, Z3_OP_GT)
2906 
2907 

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

2836 def is_idiv(a):
2837  """Return `True` if `a` is an expression of the form b div c.
2838 
2839  >>> x, y = Ints('x y')
2840  >>> is_idiv(x / y)
2841  True
2842  >>> is_idiv(x + y)
2843  False
2844  """
2845  return is_app_of(a, Z3_OP_IDIV)
2846 
2847 

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

1636 def is_implies(a):
1637  """Return `True` if `a` is a Z3 implication expression.
1638 
1639  >>> p, q = Bools('p q')
1640  >>> is_implies(Implies(p, q))
1641  True
1642  >>> is_implies(And(p, q))
1643  False
1644  """
1645  return is_app_of(a, Z3_OP_IMPLIES)
1646 
1647 

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

2677 def is_int(a):
2678  """Return `True` if `a` is an integer expression.
2679 
2680  >>> x = Int('x')
2681  >>> is_int(x + 1)
2682  True
2683  >>> is_int(1)
2684  False
2685  >>> is_int(IntVal(1))
2686  True
2687  >>> y = Real('y')
2688  >>> is_int(y)
2689  False
2690  >>> is_int(y + 1)
2691  False
2692  """
2693  return is_arith(a) and a.is_int()
2694 
2695 

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

2723 def is_int_value(a):
2724  """Return `True` if `a` is an integer value of sort Int.
2725 
2726  >>> is_int_value(IntVal(1))
2727  True
2728  >>> is_int_value(1)
2729  False
2730  >>> is_int_value(Int('x'))
2731  False
2732  >>> n = Int('x') + 1
2733  >>> n
2734  x + 1
2735  >>> n.arg(1)
2736  1
2737  >>> is_int_value(n.arg(1))
2738  True
2739  >>> is_int_value(RealVal("1/3"))
2740  False
2741  >>> is_int_value(RealVal(1))
2742  False
2743  """
2744  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2745 
2746 

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

2908 def is_is_int(a):
2909  """Return `True` if `a` is an expression of the form IsInt(b).
2910 
2911  >>> x = Real('x')
2912  >>> is_is_int(IsInt(x))
2913  True
2914  >>> is_is_int(x)
2915  False
2916  """
2917  return is_app_of(a, Z3_OP_IS_INT)
2918 
2919 

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

4629 def is_K(a):
4630  """Return `True` if `a` is a Z3 constant array.
4631 
4632  >>> a = K(IntSort(), 10)
4633  >>> is_K(a)
4634  True
4635  >>> a = Array('a', IntSort(), IntSort())
4636  >>> is_K(a)
4637  False
4638  """
4639  return is_app_of(a, Z3_OP_CONST_ARRAY)
4640 
4641 

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

2860 def is_le(a):
2861  """Return `True` if `a` is an expression of the form b <= c.
2862 
2863  >>> x, y = Ints('x y')
2864  >>> is_le(x <= y)
2865  True
2866  >>> is_le(x < y)
2867  False
2868  """
2869  return is_app_of(a, Z3_OP_LE)
2870 
2871 

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

2872 def is_lt(a):
2873  """Return `True` if `a` is an expression of the form b < c.
2874 
2875  >>> x, y = Ints('x y')
2876  >>> is_lt(x < y)
2877  True
2878  >>> is_lt(x == y)
2879  False
2880  """
2881  return is_app_of(a, Z3_OP_LT)
2882 
2883 

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

4642 def is_map(a):
4643  """Return `True` if `a` is a Z3 map array expression.
4644 
4645  >>> f = Function('f', IntSort(), IntSort())
4646  >>> b = Array('b', IntSort(), IntSort())
4647  >>> a = Map(f, b)
4648  >>> a
4649  Map(f, b)
4650  >>> is_map(a)
4651  True
4652  >>> is_map(b)
4653  False
4654  """
4655  return is_app_of(a, Z3_OP_ARRAY_MAP)
4656 
4657 

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

2848 def is_mod(a):
2849  """Return `True` if `a` is an expression of the form b % c.
2850 
2851  >>> x, y = Ints('x y')
2852  >>> is_mod(x % y)
2853  True
2854  >>> is_mod(x + y)
2855  False
2856  """
2857  return is_app_of(a, Z3_OP_MOD)
2858 
2859 

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

2795 def is_mul(a):
2796  """Return `True` if `a` is an expression of the form b * c.
2797 
2798  >>> x, y = Ints('x y')
2799  >>> is_mul(x * y)
2800  True
2801  >>> is_mul(x - y)
2802  False
2803  """
2804  return is_app_of(a, Z3_OP_MUL)
2805 
2806 

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

1648 def is_not(a):
1649  """Return `True` if `a` is a Z3 not expression.
1650 
1651  >>> p = Bool('p')
1652  >>> is_not(p)
1653  False
1654  >>> is_not(Not(p))
1655  True
1656  """
1657  return is_app_of(a, Z3_OP_NOT)
1658 
1659 

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

1624 def is_or(a):
1625  """Return `True` if `a` is a Z3 or expression.
1626 
1627  >>> p, q = Bools('p q')
1628  >>> is_or(Or(p, q))
1629  True
1630  >>> is_or(And(p, q))
1631  False
1632  """
1633  return is_app_of(a, Z3_OP_OR)
1634 
1635 

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

1924 def is_pattern(a):
1925  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1926 
1927  >>> f = Function('f', IntSort(), IntSort())
1928  >>> x = Int('x')
1929  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1930  >>> q
1931  ForAll(x, f(x) == 0)
1932  >>> q.num_patterns()
1933  1
1934  >>> is_pattern(q.pattern(0))
1935  True
1936  >>> q.pattern(0)
1937  f(Var(0))
1938  """
1939  return isinstance(a, PatternRef)
1940 
1941 

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

8612 def is_probe(p):
8613  """Return `True` if `p` is a Z3 probe.
8614 
8615  >>> is_probe(Int('x'))
8616  False
8617  >>> is_probe(Probe('memory'))
8618  True
8619  """
8620  return isinstance(p, Probe)
8621 
8622 

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

2164 def is_quantifier(a):
2165  """Return `True` if `a` is a Z3 quantifier.
2166 
2167  >>> f = Function('f', IntSort(), IntSort())
2168  >>> x = Int('x')
2169  >>> q = ForAll(x, f(x) == 0)
2170  >>> is_quantifier(q)
2171  True
2172  >>> is_quantifier(f(x))
2173  False
2174  """
2175  return isinstance(a, QuantifierRef)
2176 
2177 

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

2747 def is_rational_value(a):
2748  """Return `True` if `a` is rational value of sort Real.
2749 
2750  >>> is_rational_value(RealVal(1))
2751  True
2752  >>> is_rational_value(RealVal("3/5"))
2753  True
2754  >>> is_rational_value(IntVal(1))
2755  False
2756  >>> is_rational_value(1)
2757  False
2758  >>> n = Real('x') + 1
2759  >>> n.arg(1)
2760  1
2761  >>> is_rational_value(n.arg(1))
2762  True
2763  >>> is_rational_value(Real('x'))
2764  False
2765  """
2766  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2767 
2768 

◆ is_re()

def z3py.is_re (   s)

Definition at line 11143 of file z3py.py.

11143 def is_re(s):
11144  return isinstance(s, ReRef)
11145 
11146 

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

2696 def is_real(a):
2697  """Return `True` if `a` is a real expression.
2698 
2699  >>> x = Int('x')
2700  >>> is_real(x + 1)
2701  False
2702  >>> y = Real('y')
2703  >>> is_real(y)
2704  True
2705  >>> is_real(y + 1)
2706  True
2707  >>> is_real(1)
2708  False
2709  >>> is_real(RealVal(1))
2710  True
2711  """
2712  return is_arith(a) and a.is_real()
2713 
2714 

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

4877 def is_select(a):
4878  """Return `True` if `a` is a Z3 array select application.
4879 
4880  >>> a = Array('a', IntSort(), IntSort())
4881  >>> is_select(a)
4882  False
4883  >>> i = Int('i')
4884  >>> is_select(a[i])
4885  True
4886  """
4887  return is_app_of(a, Z3_OP_SELECT)
4888 
4889 

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

10869 def is_seq(a):
10870  """Return `True` if `a` is a Z3 sequence expression.
10871  >>> print (is_seq(Unit(IntVal(0))))
10872  True
10873  >>> print (is_seq(StringVal("abc")))
10874  True
10875  """
10876  return isinstance(a, SeqRef)
10877 
10878 

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

4890 def is_store(a):
4891  """Return `True` if `a` is a Z3 array store application.
4892 
4893  >>> a = Array('a', IntSort(), IntSort())
4894  >>> is_store(a)
4895  False
4896  >>> is_store(Store(a, 0, 1))
4897  True
4898  """
4899  return is_app_of(a, Z3_OP_STORE)
4900 

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

10879 def is_string(a):
10880  """Return `True` if `a` is a Z3 string expression.
10881  >>> print (is_string(StringVal("ab")))
10882  True
10883  """
10884  return isinstance(a, SeqRef) and a.is_string()
10885 
10886 

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

10887 def is_string_value(a):
10888  """return 'True' if 'a' is a Z3 string constant expression.
10889  >>> print (is_string_value(StringVal("a")))
10890  True
10891  >>> print (is_string_value(StringVal("a") + StringVal("b")))
10892  False
10893  """
10894  return isinstance(a, SeqRef) and a.is_string_value()
10895 

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

2807 def is_sub(a):
2808  """Return `True` if `a` is an expression of the form b - c.
2809 
2810  >>> x, y = Ints('x y')
2811  >>> is_sub(x - y)
2812  True
2813  >>> is_sub(x + y)
2814  False
2815  """
2816  return is_app_of(a, Z3_OP_SUB)
2817 
2818 

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

2935 def is_to_int(a):
2936  """Return `True` if `a` is an expression of the form ToInt(b).
2937 
2938  >>> x = Real('x')
2939  >>> n = ToInt(x)
2940  >>> n
2941  ToInt(x)
2942  >>> is_to_int(n)
2943  True
2944  >>> is_to_int(x)
2945  False
2946  """
2947  return is_app_of(a, Z3_OP_TO_INT)
2948 
2949 

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

2920 def is_to_real(a):
2921  """Return `True` if `a` is an expression of the form ToReal(b).
2922 
2923  >>> x = Int('x')
2924  >>> n = ToReal(x)
2925  >>> n
2926  ToReal(x)
2927  >>> is_to_real(n)
2928  True
2929  >>> is_to_real(x)
2930  False
2931  """
2932  return is_app_of(a, Z3_OP_TO_REAL)
2933 
2934 

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

1580 def is_true(a):
1581  """Return `True` if `a` is the Z3 true expression.
1582 
1583  >>> p = Bool('p')
1584  >>> is_true(p)
1585  False
1586  >>> is_true(simplify(p == p))
1587  True
1588  >>> x = Real('x')
1589  >>> is_true(x == 0)
1590  False
1591  >>> # True is a Python Boolean expression
1592  >>> is_true(True)
1593  False
1594  """
1595  return is_app_of(a, Z3_OP_TRUE)
1596 
1597 

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

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

Referenced by get_var_index().

◆ IsInt()

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

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

Definition at line 3385 of file z3py.py.

3385 def IsInt(a):
3386  """ Return the Z3 predicate IsInt(a).
3387 
3388  >>> x = Real('x')
3389  >>> IsInt(x + "1/2")
3390  IsInt(x + 1/2)
3391  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3392  [x = 1/2]
3393  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3394  no solution
3395  """
3396  if z3_debug():
3397  _z3_assert(a.is_real(), "Z3 real expression expected.")
3398  ctx = a.ctx
3399  return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
3400 
3401 

◆ IsMember()

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

Definition at line 5000 of file z3py.py.

5000 def IsMember(e, s):
5001  """ Check if e is a member of set s
5002  >>> a = Const('a', SetSort(IntSort()))
5003  >>> IsMember(1, a)
5004  a[1]
5005  """
5006  ctx = _ctx_from_ast_arg_list([s, e])
5007  e = _py2expr(e, ctx)
5008  return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
5009 
5010 

◆ IsSubset()

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

Definition at line 5011 of file z3py.py.

5011 def IsSubset(a, b):
5012  """ Check if a is a subset of b
5013  >>> a = Const('a', SetSort(IntSort()))
5014  >>> b = Const('b', SetSort(IntSort()))
5015  >>> IsSubset(a, b)
5016  subset(a, b)
5017  """
5018  ctx = _ctx_from_ast_arg_list([a, b])
5019  return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
5020 
5021 

◆ K()

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

>>> a = K(IntSort(), 10)
>>> a
K(Int, 10)
>>> a.sort()
Array(Int, Int)
>>> i = Int('i')
>>> a[i]
K(Int, 10)[i]
>>> simplify(a[i])
10

Definition at line 4837 of file z3py.py.

4837 def K(dom, v):
4838  """Return a Z3 constant array expression.
4839 
4840  >>> a = K(IntSort(), 10)
4841  >>> a
4842  K(Int, 10)
4843  >>> a.sort()
4844  Array(Int, Int)
4845  >>> i = Int('i')
4846  >>> a[i]
4847  K(Int, 10)[i]
4848  >>> simplify(a[i])
4849  10
4850  """
4851  if z3_debug():
4852  _z3_assert(is_sort(dom), "Z3 sort expected")
4853  ctx = dom.ctx
4854  if not is_expr(v):
4855  v = _py2expr(v, ctx)
4856  return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
4857 
4858 

Referenced by ModelRef.get_interp().

◆ Lambda()

def z3py.Lambda (   vs,
  body 
)
Create a Z3 lambda expression.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> mem0 = Array('mem0', IntSort(), IntSort())
>>> lo, hi, e, i = Ints('lo hi e i')
>>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
>>> mem1
Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))

Definition at line 2252 of file z3py.py.

2252 def Lambda(vs, body):
2253  """Create a Z3 lambda expression.
2254 
2255  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2256  >>> mem0 = Array('mem0', IntSort(), IntSort())
2257  >>> lo, hi, e, i = Ints('lo hi e i')
2258  >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2259  >>> mem1
2260  Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2261  """
2262  ctx = body.ctx
2263  if is_app(vs):
2264  vs = [vs]
2265  num_vars = len(vs)
2266  _vs = (Ast * num_vars)()
2267  for i in range(num_vars):
2268  # TODO: Check if is constant
2269  _vs[i] = vs[i].as_ast()
2270  return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)
2271 

Referenced by Context.MkLambda().

◆ LastIndexOf()

def z3py.LastIndexOf (   s,
  substr 
)
Retrieve the last index of substring within a string

Definition at line 11054 of file z3py.py.

11054 def LastIndexOf(s, substr):
11055  """Retrieve the last index of substring within a string"""
11056  ctx = None
11057  ctx = _get_ctx2(s, substr, ctx)
11058  s = _coerce_seq(s, ctx)
11059  substr = _coerce_seq(substr, ctx)
11060  return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx)
11061 
11062 

◆ Length()

def z3py.Length (   s)
Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))
>>> simplify(l)
3

Definition at line 11063 of file z3py.py.

11063 def Length(s):
11064  """Obtain the length of a sequence 's'
11065  >>> l = Length(StringVal("abc"))
11066  >>> simplify(l)
11067  3
11068  """
11069  s = _coerce_seq(s)
11070  return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
11071 
11072 

Referenced by NativeContext.MkAdd(), NativeContext.MkAnd(), NativeContext.MkFreshFuncDecl(), NativeContext.MkFuncDecl(), NativeContext.MkMul(), NativeContext.MkOr(), NativeContext.MkSub(), and NativeContext.MkTupleSort().

◆ LinearOrder()

def z3py.LinearOrder (   a,
  index 
)

Definition at line 11285 of file z3py.py.

11285 def LinearOrder(a, index):
11286  return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11287 
11288 

◆ Loop()

def z3py.Loop (   re,
  lo,
  hi = 0 
)
Create the regular expression accepting between a lower and upper bound repetitions
>>> re = Loop(Re("a"), 1, 3)
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("aaaa", re)))
False
>>> print(simplify(InRe("", re)))
False

Definition at line 11243 of file z3py.py.

11243 def Loop(re, lo, hi=0):
11244  """Create the regular expression accepting between a lower and upper bound repetitions
11245  >>> re = Loop(Re("a"), 1, 3)
11246  >>> print(simplify(InRe("aa", re)))
11247  True
11248  >>> print(simplify(InRe("aaaa", re)))
11249  False
11250  >>> print(simplify(InRe("", re)))
11251  False
11252  """
11253  return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
11254 
11255 

◆ LShR()

def z3py.LShR (   a,
  b 
)
Create the Z3 expression logical right shift.

Use the operator >> for the arithmetical right shift.

>>> x, y = BitVecs('x y', 32)
>>> LShR(x, y)
LShR(x, y)
>>> (x >> y).sexpr()
'(bvashr x y)'
>>> LShR(x, y).sexpr()
'(bvlshr x y)'
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> simplify(BitVecVal(4, 3) >> 1)
6
>>> simplify(LShR(BitVecVal(4, 3), 1))
2
>>> simplify(BitVecVal(2, 3) >> 1)
1
>>> simplify(LShR(BitVecVal(2, 3), 1))
1

Definition at line 4290 of file z3py.py.

4290 def LShR(a, b):
4291  """Create the Z3 expression logical right shift.
4292 
4293  Use the operator >> for the arithmetical right shift.
4294 
4295  >>> x, y = BitVecs('x y', 32)
4296  >>> LShR(x, y)
4297  LShR(x, y)
4298  >>> (x >> y).sexpr()
4299  '(bvashr x y)'
4300  >>> LShR(x, y).sexpr()
4301  '(bvlshr x y)'
4302  >>> BitVecVal(4, 3)
4303  4
4304  >>> BitVecVal(4, 3).as_signed_long()
4305  -4
4306  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4307  -2
4308  >>> simplify(BitVecVal(4, 3) >> 1)
4309  6
4310  >>> simplify(LShR(BitVecVal(4, 3), 1))
4311  2
4312  >>> simplify(BitVecVal(2, 3) >> 1)
4313  1
4314  >>> simplify(LShR(BitVecVal(2, 3), 1))
4315  1
4316  """
4317  _check_bv_args(a, b)
4318  a, b = _coerce_exprs(a, b)
4319  return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4320 
4321 

◆ main_ctx()

def z3py.main_ctx ( )
Return a reference to the global Z3 context.

>>> x = Real('x')
>>> x.ctx == main_ctx()
True
>>> c = Context()
>>> c == main_ctx()
False
>>> x2 = Real('x', c)
>>> x2.ctx == c
True
>>> eq(x, x2)
False

Definition at line 239 of file z3py.py.

239 def main_ctx():
240  """Return a reference to the global Z3 context.
241 
242  >>> x = Real('x')
243  >>> x.ctx == main_ctx()
244  True
245  >>> c = Context()
246  >>> c == main_ctx()
247  False
248  >>> x2 = Real('x', c)
249  >>> x2.ctx == c
250  True
251  >>> eq(x, x2)
252  False
253  """
254  global _main_ctx
255  if _main_ctx is None:
256  _main_ctx = Context()
257  return _main_ctx
258 
259 

Referenced by CharIsDigit(), help_simplify(), and simplify_param_descrs().

◆ Map()

def z3py.Map (   f,
args 
)
Return a Z3 map array expression.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> a1 = Array('a1', IntSort(), IntSort())
>>> a2 = Array('a2', IntSort(), IntSort())
>>> b  = Map(f, a1, a2)
>>> b
Map(f, a1, a2)
>>> prove(b[0] == f(a1[0], a2[0]))
proved

Definition at line 4814 of file z3py.py.

4814 def Map(f, *args):
4815  """Return a Z3 map array expression.
4816 
4817  >>> f = Function('f', IntSort(), IntSort(), IntSort())
4818  >>> a1 = Array('a1', IntSort(), IntSort())
4819  >>> a2 = Array('a2', IntSort(), IntSort())
4820  >>> b = Map(f, a1, a2)
4821  >>> b
4822  Map(f, a1, a2)
4823  >>> prove(b[0] == f(a1[0], a2[0]))
4824  proved
4825  """
4826  args = _get_args(args)
4827  if z3_debug():
4828  _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
4829  _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
4830  _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
4831  _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
4832  _args, sz = _to_ast_array(args)
4833  ctx = f.ctx
4834  return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
4835 
4836 

Referenced by Context.Context().

◆ mk_not()

def z3py.mk_not (   a)

Definition at line 1825 of file z3py.py.

1825 def mk_not(a):
1826  if is_not(a):
1827  return a.arg(0)
1828  else:
1829  return Not(a)
1830 
1831 

◆ Model()

def z3py.Model (   ctx = None)

Definition at line 6680 of file z3py.py.

6680 def Model(ctx=None):
6681  ctx = _get_ctx(ctx)
6682  return ModelRef(Z3_mk_model(ctx.ref()), ctx)
6683 
6684 

Referenced by Goal.ConvertModel(), Goal.convertModel(), Optimize.getModel(), Solver.getModel(), and Optimize.set_on_model().

◆ MultiPattern()

def z3py.MultiPattern ( args)
Create a Z3 multi-pattern using the given expressions `*args`

>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
>>> q
ForAll(x, f(x) != g(x))
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
MultiPattern(f(Var(0)), g(Var(0)))

Definition at line 1942 of file z3py.py.

1942 def MultiPattern(*args):
1943  """Create a Z3 multi-pattern using the given expressions `*args`
1944 
1945  >>> f = Function('f', IntSort(), IntSort())
1946  >>> g = Function('g', IntSort(), IntSort())
1947  >>> x = Int('x')
1948  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1949  >>> q
1950  ForAll(x, f(x) != g(x))
1951  >>> q.num_patterns()
1952  1
1953  >>> is_pattern(q.pattern(0))
1954  True
1955  >>> q.pattern(0)
1956  MultiPattern(f(Var(0)), g(Var(0)))
1957  """
1958  if z3_debug():
1959  _z3_assert(len(args) > 0, "At least one argument expected")
1960  _z3_assert(all([is_expr(a) for a in args]), "Z3 expressions expected")
1961  ctx = args[0].ctx
1962  args, sz = _to_ast_array(args)
1963  return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
1964 
1965 

◆ Not()

def z3py.Not (   a,
  ctx = None 
)
Create a Z3 not expression or probe.

>>> p = Bool('p')
>>> Not(Not(p))
Not(Not(p))
>>> simplify(Not(Not(p)))
p

Definition at line 1806 of file z3py.py.

1806 def Not(a, ctx=None):
1807  """Create a Z3 not expression or probe.
1808 
1809  >>> p = Bool('p')
1810  >>> Not(Not(p))
1811  Not(Not(p))
1812  >>> simplify(Not(Not(p)))
1813  p
1814  """
1815  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1816  if is_probe(a):
1817  # Not is also used to build probes
1818  return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1819  else:
1820  s = BoolSort(ctx)
1821  a = s.cast(a)
1822  return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
1823 
1824 

Referenced by fpNEQ(), mk_not(), and prove().

◆ open_log()

def z3py.open_log (   fname)
Log interaction to a file. This function must be invoked immediately after init(). 

Definition at line 114 of file z3py.py.

114 def open_log(fname):
115  """Log interaction to a file. This function must be invoked immediately after init(). """
116  Z3_open_log(fname)
117 
118 

◆ Option()

def z3py.Option (   re)
Create the regular expression that optionally accepts the argument.
>>> re = Option(Re("a"))
>>> print(simplify(InRe("a", re)))
True
>>> print(simplify(InRe("", re)))
True
>>> print(simplify(InRe("aa", re)))
False

Definition at line 11212 of file z3py.py.

11212 def Option(re):
11213  """Create the regular expression that optionally accepts the argument.
11214  >>> re = Option(Re("a"))
11215  >>> print(simplify(InRe("a", re)))
11216  True
11217  >>> print(simplify(InRe("", re)))
11218  True
11219  >>> print(simplify(InRe("aa", re)))
11220  False
11221  """
11222  return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
11223 
11224 

◆ Or()

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

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

Definition at line 1873 of file z3py.py.

1873 def Or(*args):
1874  """Create a Z3 or-expression or or-probe.
1875 
1876  >>> p, q, r = Bools('p q r')
1877  >>> Or(p, q, r)
1878  Or(p, q, r)
1879  >>> P = BoolVector('p', 5)
1880  >>> Or(P)
1881  Or(p__0, p__1, p__2, p__3, p__4)
1882  """
1883  last_arg = None
1884  if len(args) > 0:
1885  last_arg = args[len(args) - 1]
1886  if isinstance(last_arg, Context):
1887  ctx = args[len(args) - 1]
1888  args = args[:len(args) - 1]
1889  elif len(args) == 1 and isinstance(args[0], AstVector):
1890  ctx = args[0].ctx
1891  args = [a for a in args[0]]
1892  else:
1893  ctx = None
1894  args = _get_args(args)
1895  ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1896  if z3_debug():
1897  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1898  if _has_probe(args):
1899  return _probe_or(args, ctx)
1900  else:
1901  args = _coerce_expr_list(args, ctx)
1902  _args, sz = _to_ast_array(args)
1903  return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
1904 

Referenced by ApplyResult.as_expr().

◆ OrElse()

def z3py.OrElse ( ts,
**  ks 
)
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).

>>> x = Int('x')
>>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
>>> # Tactic split-clause fails if there is no clause in the given goal.
>>> t(x == 0)
[[x == 0]]
>>> t(Or(x == 0, x == 1))
[[x == 0], [x == 1]]

Definition at line 8305 of file z3py.py.

8305 def OrElse(*ts, **ks):
8306  """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
8307 
8308  >>> x = Int('x')
8309  >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
8310  >>> # Tactic split-clause fails if there is no clause in the given goal.
8311  >>> t(x == 0)
8312  [[x == 0]]
8313  >>> t(Or(x == 0, x == 1))
8314  [[x == 0], [x == 1]]
8315  """
8316  if z3_debug():
8317  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8318  ctx = ks.get("ctx", None)
8319  num = len(ts)
8320  r = ts[0]
8321  for i in range(num - 1):
8322  r = _or_else(r, ts[i + 1], ctx)
8323  return r
8324 
8325 

◆ ParAndThen()

def z3py.ParAndThen (   t1,
  t2,
  ctx = None 
)
Alias for ParThen(t1, t2, ctx).

Definition at line 8361 of file z3py.py.

8361 def ParAndThen(t1, t2, ctx=None):
8362  """Alias for ParThen(t1, t2, ctx)."""
8363  return ParThen(t1, t2, ctx)
8364 
8365 

◆ ParOr()

def z3py.ParOr ( ts,
**  ks 
)
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).

>>> x = Int('x')
>>> t = ParOr(Tactic('simplify'), Tactic('fail'))
>>> t(x + 1 == 2)
[[x == 1]]

Definition at line 8326 of file z3py.py.

8326 def ParOr(*ts, **ks):
8327  """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
8328 
8329  >>> x = Int('x')
8330  >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
8331  >>> t(x + 1 == 2)
8332  [[x == 1]]
8333  """
8334  if z3_debug():
8335  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8336  ctx = _get_ctx(ks.get("ctx", None))
8337  ts = [_to_tactic(t, ctx) for t in ts]
8338  sz = len(ts)
8339  _args = (TacticObj * sz)()
8340  for i in range(sz):
8341  _args[i] = ts[i].tactic
8342  return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
8343 
8344 

◆ parse_smt2_file()

def z3py.parse_smt2_file (   f,
  sorts = {},
  decls = {},
  ctx = None 
)
Parse a file in SMT 2.0 format using the given sorts and decls.

This function is similar to parse_smt2_string().

Definition at line 9241 of file z3py.py.

9241 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
9242  """Parse a file in SMT 2.0 format using the given sorts and decls.
9243 
9244  This function is similar to parse_smt2_string().
9245  """
9246  ctx = _get_ctx(ctx)
9247  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9248  dsz, dnames, ddecls = _dict2darray(decls, ctx)
9249  return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9250 
9251 

◆ parse_smt2_string()

def z3py.parse_smt2_string (   s,
  sorts = {},
  decls = {},
  ctx = None 
)
Parse a string in SMT 2.0 format using the given sorts and decls.

The arguments sorts and decls are Python dictionaries used to initialize
the symbol table used for the SMT 2.0 parser.

>>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
[x > 0, x < 10]
>>> x, y = Ints('x y')
>>> f = Function('f', IntSort(), IntSort())
>>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
[x + f(y) > 0]
>>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
[a > 0]

Definition at line 9220 of file z3py.py.

9220 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
9221  """Parse a string in SMT 2.0 format using the given sorts and decls.
9222 
9223  The arguments sorts and decls are Python dictionaries used to initialize
9224  the symbol table used for the SMT 2.0 parser.
9225 
9226  >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
9227  [x > 0, x < 10]
9228  >>> x, y = Ints('x y')
9229  >>> f = Function('f', IntSort(), IntSort())
9230  >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
9231  [x + f(y) > 0]
9232  >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
9233  [a > 0]
9234  """
9235  ctx = _get_ctx(ctx)
9236  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9237  dsz, dnames, ddecls = _dict2darray(decls, ctx)
9238  return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9239 
9240 

◆ ParThen()

def z3py.ParThen (   t1,
  t2,
  ctx = None 
)
Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
The subgoals are processed in parallel.

>>> x, y = Ints('x y')
>>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
>>> t(And(Or(x == 1, x == 2), y == x + 1))
[[x == 1, y == 2], [x == 2, y == 3]]

Definition at line 8345 of file z3py.py.

8345 def ParThen(t1, t2, ctx=None):
8346  """Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
8347  The subgoals are processed in parallel.
8348 
8349  >>> x, y = Ints('x y')
8350  >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
8351  >>> t(And(Or(x == 1, x == 2), y == x + 1))
8352  [[x == 1, y == 2], [x == 2, y == 3]]
8353  """
8354  t1 = _to_tactic(t1, ctx)
8355  t2 = _to_tactic(t2, ctx)
8356  if z3_debug():
8357  _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
8358  return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
8359 
8360 

Referenced by ParAndThen().

◆ PartialOrder()

def z3py.PartialOrder (   a,
  index 
)

Definition at line 11281 of file z3py.py.

11281 def PartialOrder(a, index):
11282  return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx)
11283 
11284 

◆ PbEq()

def z3py.PbEq (   args,
  k,
  ctx = None 
)
Create a Pseudo-Boolean inequality k constraint.

>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)

Definition at line 8997 of file z3py.py.

8997 def PbEq(args, k, ctx=None):
8998  """Create a Pseudo-Boolean inequality k constraint.
8999 
9000  >>> a, b, c = Bools('a b c')
9001  >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
9002  """
9003  _z3_check_cint_overflow(k, "k")
9004  ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
9005  return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
9006 
9007 

◆ PbGe()

def z3py.PbGe (   args,
  k 
)
Create a Pseudo-Boolean inequality k constraint.

>>> a, b, c = Bools('a b c')
>>> f = PbGe(((a,1),(b,3),(c,2)), 3)

Definition at line 8986 of file z3py.py.

8986 def PbGe(args, k):
8987  """Create a Pseudo-Boolean inequality k constraint.
8988 
8989  >>> a, b, c = Bools('a b c')
8990  >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
8991  """
8992  _z3_check_cint_overflow(k, "k")
8993  ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
8994  return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
8995 
8996 

◆ PbLe()

def z3py.PbLe (   args,
  k 
)
Create a Pseudo-Boolean inequality k constraint.

>>> a, b, c = Bools('a b c')
>>> f = PbLe(((a,1),(b,3),(c,2)), 3)

Definition at line 8975 of file z3py.py.

8975 def PbLe(args, k):
8976  """Create a Pseudo-Boolean inequality k constraint.
8977 
8978  >>> a, b, c = Bools('a b c')
8979  >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
8980  """
8981  _z3_check_cint_overflow(k, "k")
8982  ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
8983  return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
8984 
8985 

◆ PiecewiseLinearOrder()

def z3py.PiecewiseLinearOrder (   a,
  index 
)

Definition at line 11293 of file z3py.py.

11293 def PiecewiseLinearOrder(a, index):
11294  return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11295 
11296 

◆ Plus()

def z3py.Plus (   re)
Create the regular expression accepting one or more repetitions of argument.
>>> re = Plus(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
False

Definition at line 11199 of file z3py.py.

11199 def Plus(re):
11200  """Create the regular expression accepting one or more repetitions of argument.
11201  >>> re = Plus(Re("a"))
11202  >>> print(simplify(InRe("aa", re)))
11203  True
11204  >>> print(simplify(InRe("ab", re)))
11205  False
11206  >>> print(simplify(InRe("", re)))
11207  False
11208  """
11209  return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
11210 
11211 

◆ PrefixOf()

def z3py.PrefixOf (   a,
  b 
)
Check if 'a' is a prefix of 'b'
>>> s1 = PrefixOf("ab", "abc")
>>> simplify(s1)
True
>>> s2 = PrefixOf("bc", "abc")
>>> simplify(s2)
False

Definition at line 10970 of file z3py.py.

10970 def PrefixOf(a, b):
10971  """Check if 'a' is a prefix of 'b'
10972  >>> s1 = PrefixOf("ab", "abc")
10973  >>> simplify(s1)
10974  True
10975  >>> s2 = PrefixOf("bc", "abc")
10976  >>> simplify(s2)
10977  False
10978  """
10979  ctx = _get_ctx2(a, b)
10980  a = _coerce_seq(a, ctx)
10981  b = _coerce_seq(b, ctx)
10982  return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10983 
10984 

◆ probe_description()

def z3py.probe_description (   name,
  ctx = None 
)
Return a short description for the probe named `name`.

>>> d = probe_description('memory')

Definition at line 8641 of file z3py.py.

8641 def probe_description(name, ctx=None):
8642  """Return a short description for the probe named `name`.
8643 
8644  >>> d = probe_description('memory')
8645  """
8646  ctx = _get_ctx(ctx)
8647  return Z3_probe_get_descr(ctx.ref(), name)
8648 
8649 

Referenced by describe_probes().

◆ probes()