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  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  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 is_expr (a)
 
def is_app (a)
 
def is_const (a)
 
def is_var (a)
 
def get_var_index (a)
 
def is_app_of (a, k)
 
def If (a, b, c, ctx=None)
 
def Distinct (*args)
 
def Const (name, sort)
 
def Consts (names, sort)
 
def FreshConst (sort, prefix="c")
 
def Var (idx, s)
 
def RealVar (idx, ctx=None)
 
def RealVarVector (n, ctx=None)
 
def is_bool (a)
 
def is_true (a)
 
def is_false (a)
 
def is_and (a)
 
def is_or (a)
 
def is_implies (a)
 
def is_not (a)
 
def is_eq (a)
 
def is_distinct (a)
 
def BoolSort (ctx=None)
 
def BoolVal (val, ctx=None)
 
def Bool (name, ctx=None)
 
def Bools (names, ctx=None)
 
def BoolVector (prefix, sz, ctx=None)
 
def FreshBool (prefix="b", ctx=None)
 
def Implies (a, b, ctx=None)
 
def Xor (a, b, ctx=None)
 
def Not (a, ctx=None)
 
def mk_not (a)
 
def And (*args)
 
def Or (*args)
 
def is_pattern (a)
 
def MultiPattern (*args)
 
def is_quantifier (a)
 
def ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Lambda (vs, body)
 
def is_arith_sort (s)
 
def is_arith (a)
 
def is_int (a)
 
def is_real (a)
 
def is_int_value (a)
 
def is_rational_value (a)
 
def is_algebraic_value (a)
 
def is_add (a)
 
def is_mul (a)
 
def is_sub (a)
 
def is_div (a)
 
def is_idiv (a)
 
def is_mod (a)
 
def is_le (a)
 
def is_lt (a)
 
def is_ge (a)
 
def is_gt (a)
 
def is_is_int (a)
 
def is_to_real (a)
 
def is_to_int (a)
 
def IntSort (ctx=None)
 
def RealSort (ctx=None)
 
def IntVal (val, ctx=None)
 
def RealVal (val, ctx=None)
 
def RatVal (a, b, ctx=None)
 
def Q (a, b, ctx=None)
 
def Int (name, ctx=None)
 
def Ints (names, ctx=None)
 
def IntVector (prefix, sz, ctx=None)
 
def FreshInt (prefix="x", ctx=None)
 
def Real (name, ctx=None)
 
def Reals (names, ctx=None)
 
def RealVector (prefix, sz, ctx=None)
 
def FreshReal (prefix="b", ctx=None)
 
def ToReal (a)
 
def ToInt (a)
 
def IsInt (a)
 
def Sqrt (a, ctx=None)
 
def Cbrt (a, ctx=None)
 
def is_bv_sort (s)
 
def is_bv (a)
 
def is_bv_value (a)
 
def BV2Int (a, is_signed=False)
 
def Int2BV (a, num_bits)
 
def BitVecSort (sz, ctx=None)
 
def BitVecVal (val, bv, ctx=None)
 
def BitVec (name, bv, ctx=None)
 
def BitVecs (names, bv, ctx=None)
 
def Concat (*args)
 
def Extract (high, low, a)
 
def ULE (a, b)
 
def ULT (a, b)
 
def UGE (a, b)
 
def UGT (a, b)
 
def UDiv (a, b)
 
def URem (a, b)
 
def SRem (a, b)
 
def LShR (a, b)
 
def RotateLeft (a, b)
 
def RotateRight (a, b)
 
def SignExt (n, a)
 
def ZeroExt (n, a)
 
def RepeatBitVec (n, a)
 
def BVRedAnd (a)
 
def BVRedOr (a)
 
def BVAddNoOverflow (a, b, signed)
 
def BVAddNoUnderflow (a, b)
 
def BVSubNoOverflow (a, b)
 
def BVSubNoUnderflow (a, b, signed)
 
def BVSDivNoOverflow (a, b)
 
def BVSNegNoOverflow (a)
 
def BVMulNoOverflow (a, b, signed)
 
def BVMulNoUnderflow (a, b)
 
def is_array_sort (a)
 
def is_array (a)
 
def is_const_array (a)
 
def is_K (a)
 
def is_map (a)
 
def is_default (a)
 
def get_map_func (a)
 
def ArraySort (*sig)
 
def Array (name, dom, rng)
 
def Update (a, i, v)
 
def Default (a)
 
def Store (a, i, v)
 
def Select (a, i)
 
def Map (f, *args)
 
def K (dom, v)
 
def Ext (a, b)
 
def SetHasSize (a, k)
 
def is_select (a)
 
def is_store (a)
 
def SetSort (s)
 Sets. More...
 
def EmptySet (s)
 
def FullSet (s)
 
def SetUnion (*args)
 
def SetIntersect (*args)
 
def SetAdd (s, e)
 
def SetDel (s, e)
 
def SetComplement (s)
 
def SetDifference (a, b)
 
def IsMember (e, s)
 
def IsSubset (a, b)
 
def CreateDatatypes (*ds)
 
def TupleSort (name, sorts, ctx=None)
 
def DisjointSum (name, sorts, ctx=None)
 
def EnumSort (name, values, ctx=None)
 
def args2params (arguments, keywords, ctx=None)
 
def Model (ctx=None)
 
def is_as_array (n)
 
def get_as_array_func (n)
 
def SolverFor (logic, ctx=None, logFile=None)
 
def SimpleSolver (ctx=None, logFile=None)
 
def FiniteDomainSort (name, sz, ctx=None)
 
def is_finite_domain_sort (s)
 
def is_finite_domain (a)
 
def FiniteDomainVal (val, sort, ctx=None)
 
def is_finite_domain_value (a)
 
def AndThen (*ts, **ks)
 
def Then (*ts, **ks)
 
def OrElse (*ts, **ks)
 
def ParOr (*ts, **ks)
 
def ParThen (t1, t2, ctx=None)
 
def ParAndThen (t1, t2, ctx=None)
 
def With (t, *args, **keys)
 
def WithParams (t, p)
 
def Repeat (t, max=4294967295, ctx=None)
 
def TryFor (t, ms, ctx=None)
 
def tactics (ctx=None)
 
def tactic_description (name, ctx=None)
 
def describe_tactics ()
 
def is_probe (p)
 
def probes (ctx=None)
 
def probe_description (name, ctx=None)
 
def describe_probes ()
 
def FailIf (p, ctx=None)
 
def When (p, t, ctx=None)
 
def Cond (p, t1, t2, ctx=None)
 
def simplify (a, *arguments, **keywords)
 Utils. More...
 
def help_simplify ()
 
def simplify_param_descrs ()
 
def substitute (t, *m)
 
def substitute_vars (t, *m)
 
def Sum (*args)
 
def Product (*args)
 
def AtMost (*args)
 
def AtLeast (*args)
 
def PbLe (args, k)
 
def PbGe (args, k)
 
def PbEq (args, k, ctx=None)
 
def solve (*args, **keywords)
 
def solve_using (s, *args, **keywords)
 
def prove (claim, 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 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 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)
 
def user_prop_pop (ctx, num_scopes)
 
def user_prop_fresh (id, ctx)
 
def user_prop_fixed (ctx, cb, id, value)
 
def user_prop_final (ctx, cb)
 
def user_prop_eq (ctx, cb, x, y)
 
def user_prop_diseq (ctx, cb, x, y)
 

Variables

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

Function Documentation

◆ AllChar()

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

Definition at line 11073 of file z3py.py.

11073 def AllChar(regex_sort, ctx=None):
11074  """Create a regular expression that accepts all single character strings
11075  """
11076  return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
11077 
11078 # Special Relations
11079 
11080 

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

1815 def And(*args):
1816  """Create a Z3 and-expression or and-probe.
1817 
1818  >>> p, q, r = Bools('p q r')
1819  >>> And(p, q, r)
1820  And(p, q, r)
1821  >>> P = BoolVector('p', 5)
1822  >>> And(P)
1823  And(p__0, p__1, p__2, p__3, p__4)
1824  """
1825  last_arg = None
1826  if len(args) > 0:
1827  last_arg = args[len(args) - 1]
1828  if isinstance(last_arg, Context):
1829  ctx = args[len(args) - 1]
1830  args = args[:len(args) - 1]
1831  elif len(args) == 1 and isinstance(args[0], AstVector):
1832  ctx = args[0].ctx
1833  args = [a for a in args[0]]
1834  else:
1835  ctx = None
1836  args = _get_args(args)
1837  ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1838  if z3_debug():
1839  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1840  if _has_probe(args):
1841  return _probe_and(args, ctx)
1842  else:
1843  args = _coerce_expr_list(args, ctx)
1844  _args, sz = _to_ast_array(args)
1845  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1846 
1847 

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

8182 def AndThen(*ts, **ks):
8183  """Return a tactic that applies the tactics in `*ts` in sequence.
8184 
8185  >>> x, y = Ints('x y')
8186  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
8187  >>> t(And(x == 0, y > x + 1))
8188  [[Not(y <= 1)]]
8189  >>> t(And(x == 0, y > x + 1)).as_expr()
8190  Not(y <= 1)
8191  """
8192  if z3_debug():
8193  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8194  ctx = ks.get("ctx", None)
8195  num = len(ts)
8196  r = ts[0]
8197  for i in range(num - 1):
8198  r = _and_then(r, ts[i + 1], ctx)
8199  return r
8200 
8201 

Referenced by Then().

◆ append_log()

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

Definition at line 124 of file z3py.py.

124 def append_log(s):
125  """Append user-defined string to interaction log. """
126  Z3_append_log(s)
127 
128 

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

5398 def args2params(arguments, keywords, ctx=None):
5399  """Convert python arguments into a Z3_params object.
5400  A ':' is added to the keywords, and '_' is replaced with '-'
5401 
5402  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5403  (params model true relevancy 2 elim_and true)
5404  """
5405  if z3_debug():
5406  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5407  prev = None
5408  r = ParamsRef(ctx)
5409  for a in arguments:
5410  if prev is None:
5411  prev = a
5412  else:
5413  r.set(prev, a)
5414  prev = None
5415  for k in keywords:
5416  v = keywords[k]
5417  r.set(k, v)
5418  return r
5419 
5420 

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

◆ Array()

def z3py.Array (   name,
  dom,
  rng 
)
Return an array constant named `name` with the given domain and range sorts.

>>> a = Array('a', IntSort(), IntSort())
>>> a.sort()
Array(Int, Int)
>>> a[0]
a[0]

Definition at line 4680 of file z3py.py.

4680 def Array(name, dom, rng):
4681  """Return an array constant named `name` with the given domain and range sorts.
4682 
4683  >>> a = Array('a', IntSort(), IntSort())
4684  >>> a.sort()
4685  Array(Int, Int)
4686  >>> a[0]
4687  a[0]
4688  """
4689  s = ArraySort(dom, rng)
4690  ctx = s.ctx
4691  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4692 
4693 

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

4647 def ArraySort(*sig):
4648  """Return the Z3 array sort with the given domain and range sorts.
4649 
4650  >>> A = ArraySort(IntSort(), BoolSort())
4651  >>> A
4652  Array(Int, Bool)
4653  >>> A.domain()
4654  Int
4655  >>> A.range()
4656  Bool
4657  >>> AA = ArraySort(IntSort(), A)
4658  >>> AA
4659  Array(Int, Array(Int, Bool))
4660  """
4661  sig = _get_args(sig)
4662  if z3_debug():
4663  _z3_assert(len(sig) > 1, "At least two arguments expected")
4664  arity = len(sig) - 1
4665  r = sig[arity]
4666  d = sig[0]
4667  if z3_debug():
4668  for s in sig:
4669  _z3_assert(is_sort(s), "Z3 sort expected")
4670  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4671  ctx = d.ctx
4672  if len(sig) == 2:
4673  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4674  dom = (Sort * arity)()
4675  for i in range(arity):
4676  dom[i] = sig[i].ast
4677  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4678 
4679 

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

8811 def AtLeast(*args):
8812  """Create an at-most Pseudo-Boolean k constraint.
8813 
8814  >>> a, b, c = Bools('a b c')
8815  >>> f = AtLeast(a, b, c, 2)
8816  """
8817  args = _get_args(args)
8818  if z3_debug():
8819  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8820  ctx = _ctx_from_ast_arg_list(args)
8821  if z3_debug():
8822  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8823  args1 = _coerce_expr_list(args[:-1], ctx)
8824  k = args[-1]
8825  _args, sz = _to_ast_array(args1)
8826  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8827 
8828 

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

8793 def AtMost(*args):
8794  """Create an at-most Pseudo-Boolean k constraint.
8795 
8796  >>> a, b, c = Bools('a b c')
8797  >>> f = AtMost(a, b, c, 2)
8798  """
8799  args = _get_args(args)
8800  if z3_debug():
8801  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8802  ctx = _ctx_from_ast_arg_list(args)
8803  if z3_debug():
8804  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8805  args1 = _coerce_expr_list(args[:-1], ctx)
8806  k = args[-1]
8807  _args, sz = _to_ast_array(args1)
8808  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8809 
8810 

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

4001 def BitVec(name, bv, ctx=None):
4002  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4003  If `ctx=None`, then the global context is used.
4004 
4005  >>> x = BitVec('x', 16)
4006  >>> is_bv(x)
4007  True
4008  >>> x.size()
4009  16
4010  >>> x.sort()
4011  BitVec(16)
4012  >>> word = BitVecSort(16)
4013  >>> x2 = BitVec('x', word)
4014  >>> eq(x, x2)
4015  True
4016  """
4017  if isinstance(bv, BitVecSortRef):
4018  ctx = bv.ctx
4019  else:
4020  ctx = _get_ctx(ctx)
4021  bv = BitVecSort(bv, ctx)
4022  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
4023 
4024 

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

4025 def BitVecs(names, bv, ctx=None):
4026  """Return a tuple of bit-vector constants of size bv.
4027 
4028  >>> x, y, z = BitVecs('x y z', 16)
4029  >>> x.size()
4030  16
4031  >>> x.sort()
4032  BitVec(16)
4033  >>> Sum(x, y, z)
4034  0 + x + y + z
4035  >>> Product(x, y, z)
4036  1*x*y*z
4037  >>> simplify(Product(x, y, z))
4038  x*y*z
4039  """
4040  ctx = _get_ctx(ctx)
4041  if isinstance(names, str):
4042  names = names.split(" ")
4043  return [BitVec(name, bv, ctx) for name in names]
4044 
4045 

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

3969 def BitVecSort(sz, ctx=None):
3970  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3971 
3972  >>> Byte = BitVecSort(8)
3973  >>> Word = BitVecSort(16)
3974  >>> Byte
3975  BitVec(8)
3976  >>> x = Const('x', Byte)
3977  >>> eq(x, BitVec('x', 8))
3978  True
3979  """
3980  ctx = _get_ctx(ctx)
3981  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
3982 
3983 

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

3984 def BitVecVal(val, bv, ctx=None):
3985  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3986 
3987  >>> v = BitVecVal(10, 32)
3988  >>> v
3989  10
3990  >>> print("0x%.8x" % v.as_long())
3991  0x0000000a
3992  """
3993  if is_bv_sort(bv):
3994  ctx = bv.ctx
3995  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3996  else:
3997  ctx = _get_ctx(ctx)
3998  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3999 
4000 

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

1694 def Bool(name, ctx=None):
1695  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1696 
1697  >>> p = Bool('p')
1698  >>> q = Bool('q')
1699  >>> And(p, q)
1700  And(p, q)
1701  """
1702  ctx = _get_ctx(ctx)
1703  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1704 
1705 

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

1706 def Bools(names, ctx=None):
1707  """Return a tuple of Boolean constants.
1708 
1709  `names` is a single string containing all names separated by blank spaces.
1710  If `ctx=None`, then the global context is used.
1711 
1712  >>> p, q, r = Bools('p q r')
1713  >>> And(p, Or(q, r))
1714  And(p, Or(q, r))
1715  """
1716  ctx = _get_ctx(ctx)
1717  if isinstance(names, str):
1718  names = names.split(" ")
1719  return [Bool(name, ctx) for name in names]
1720 
1721 

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

1657 def BoolSort(ctx=None):
1658  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1659 
1660  >>> BoolSort()
1661  Bool
1662  >>> p = Const('p', BoolSort())
1663  >>> is_bool(p)
1664  True
1665  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1666  >>> r(0, 1)
1667  r(0, 1)
1668  >>> is_bool(r(0, 1))
1669  True
1670  """
1671  ctx = _get_ctx(ctx)
1672  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1673 
1674 

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

1675 def BoolVal(val, ctx=None):
1676  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1677 
1678  >>> BoolVal(True)
1679  True
1680  >>> is_true(BoolVal(True))
1681  True
1682  >>> is_true(True)
1683  False
1684  >>> is_false(BoolVal(False))
1685  True
1686  """
1687  ctx = _get_ctx(ctx)
1688  if val:
1689  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1690  else:
1691  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1692 
1693 

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

1722 def BoolVector(prefix, sz, ctx=None):
1723  """Return a list of Boolean constants of size `sz`.
1724 
1725  The constants are named using the given prefix.
1726  If `ctx=None`, then the global context is used.
1727 
1728  >>> P = BoolVector('p', 3)
1729  >>> P
1730  [p__0, p__1, p__2]
1731  >>> And(P)
1732  And(p__0, p__1, p__2)
1733  """
1734  return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]
1735 
1736 

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

3937 def BV2Int(a, is_signed=False):
3938  """Return the Z3 expression BV2Int(a).
3939 
3940  >>> b = BitVec('b', 3)
3941  >>> BV2Int(b).sort()
3942  Int
3943  >>> x = Int('x')
3944  >>> x > BV2Int(b)
3945  x > BV2Int(b)
3946  >>> x > BV2Int(b, is_signed=False)
3947  x > BV2Int(b)
3948  >>> x > BV2Int(b, is_signed=True)
3949  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3950  >>> solve(x > BV2Int(b), b == 1, x < 3)
3951  [x = 2, b = 1]
3952  """
3953  if z3_debug():
3954  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
3955  ctx = a.ctx
3956  # investigate problem with bv2int
3957  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3958 
3959 

◆ BVAddNoOverflow()

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

Definition at line 4423 of file z3py.py.

4423 def BVAddNoOverflow(a, b, signed):
4424  """A predicate the determines that bit-vector addition does not overflow"""
4425  _check_bv_args(a, b)
4426  a, b = _coerce_exprs(a, b)
4427  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4428 
4429 

◆ BVAddNoUnderflow()

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

Definition at line 4430 of file z3py.py.

4430 def BVAddNoUnderflow(a, b):
4431  """A predicate the determines that signed bit-vector addition does not underflow"""
4432  _check_bv_args(a, b)
4433  a, b = _coerce_exprs(a, b)
4434  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4435 
4436 

◆ BVMulNoOverflow()

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

Definition at line 4465 of file z3py.py.

4465 def BVMulNoOverflow(a, b, signed):
4466  """A predicate the determines that bit-vector multiplication does not overflow"""
4467  _check_bv_args(a, b)
4468  a, b = _coerce_exprs(a, b)
4469  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4470 
4471 

◆ BVMulNoUnderflow()

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

Definition at line 4472 of file z3py.py.

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

◆ BVRedAnd()

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

Definition at line 4409 of file z3py.py.

4409 def BVRedAnd(a):
4410  """Return the reduction-and expression of `a`."""
4411  if z3_debug():
4412  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4413  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4414 
4415 

◆ BVRedOr()

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

Definition at line 4416 of file z3py.py.

4416 def BVRedOr(a):
4417  """Return the reduction-or expression of `a`."""
4418  if z3_debug():
4419  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4420  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4421 
4422 

◆ BVSDivNoOverflow()

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

Definition at line 4451 of file z3py.py.

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

◆ BVSNegNoOverflow()

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

Definition at line 4458 of file z3py.py.

4458 def BVSNegNoOverflow(a):
4459  """A predicate the determines that bit-vector unary negation does not overflow"""
4460  if z3_debug():
4461  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4462  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4463 
4464 

◆ BVSubNoOverflow()

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

Definition at line 4437 of file z3py.py.

4437 def BVSubNoOverflow(a, b):
4438  """A predicate the determines that bit-vector subtraction does not overflow"""
4439  _check_bv_args(a, b)
4440  a, b = _coerce_exprs(a, b)
4441  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4442 
4443 

◆ BVSubNoUnderflow()

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

Definition at line 4444 of file z3py.py.

4444 def BVSubNoUnderflow(a, b, signed):
4445  """A predicate the determines that bit-vector subtraction does not underflow"""
4446  _check_bv_args(a, b)
4447  a, b = _coerce_exprs(a, b)
4448  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4449 
4450 

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

3388 def Cbrt(a, ctx=None):
3389  """ Return a Z3 expression which represents the cubic root of a.
3390 
3391  >>> x = Real('x')
3392  >>> Cbrt(x)
3393  x**(1/3)
3394  """
3395  if not is_expr(a):
3396  ctx = _get_ctx(ctx)
3397  a = RealVal(a, ctx)
3398  return a ** "1/3"
3399 

◆ CharSort()

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

Definition at line 10593 of file z3py.py.

10593 def CharSort(ctx=None):
10594  """Create a character sort
10595  >>> ch = CharSort()
10596  >>> print(ch)
10597  Char
10598  """
10599  ctx = _get_ctx(ctx)
10600  return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
10601 
10602 

Referenced by Context.mkCharSort().

◆ Complement()

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

Definition at line 11025 of file z3py.py.

11025 def Complement(re):
11026  """Create the complement regular expression."""
11027  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
11028 
11029 

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

4046 def Concat(*args):
4047  """Create a Z3 bit-vector concatenation expression.
4048 
4049  >>> v = BitVecVal(1, 4)
4050  >>> Concat(v, v+1, v)
4051  Concat(Concat(1, 1 + 1), 1)
4052  >>> simplify(Concat(v, v+1, v))
4053  289
4054  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
4055  121
4056  """
4057  args = _get_args(args)
4058  sz = len(args)
4059  if z3_debug():
4060  _z3_assert(sz >= 2, "At least two arguments expected.")
4061 
4062  ctx = None
4063  for a in args:
4064  if is_expr(a):
4065  ctx = a.ctx
4066  break
4067  if is_seq(args[0]) or isinstance(args[0], str):
4068  args = [_coerce_seq(s, ctx) for s in args]
4069  if z3_debug():
4070  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
4071  v = (Ast * sz)()
4072  for i in range(sz):
4073  v[i] = args[i].as_ast()
4074  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
4075 
4076  if is_re(args[0]):
4077  if z3_debug():
4078  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
4079  v = (Ast * sz)()
4080  for i in range(sz):
4081  v[i] = args[i].as_ast()
4082  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
4083 
4084  if z3_debug():
4085  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
4086  r = args[0]
4087  for i in range(sz - 1):
4088  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
4089  return r
4090 
4091 

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

8639 def Cond(p, t1, t2, ctx=None):
8640  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8641 
8642  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8643  """
8644  p = _to_probe(p, ctx)
8645  t1 = _to_tactic(t1, ctx)
8646  t2 = _to_tactic(t2, ctx)
8647  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8648 

Referenced by If().

◆ Const()

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

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

Definition at line 1407 of file z3py.py.

1407 def Const(name, sort):
1408  """Create a constant of the given sort.
1409 
1410  >>> Const('x', IntSort())
1411  x
1412  """
1413  if z3_debug():
1414  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1415  ctx = sort.ctx
1416  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1417 
1418 

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

1419 def Consts(names, sort):
1420  """Create several constants of the given sort.
1421 
1422  `names` is a string containing the names of all constants to be created.
1423  Blank spaces separate the names of different constants.
1424 
1425  >>> x, y, z = Consts('x y z', IntSort())
1426  >>> x + y + z
1427  x + y + z
1428  """
1429  if isinstance(names, str):
1430  names = names.split(" ")
1431  return [Const(name, sort) for name in names]
1432 
1433 

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

10812 def Contains(a, b):
10813  """Check if 'a' contains 'b'
10814  >>> s1 = Contains("abc", "ab")
10815  >>> simplify(s1)
10816  True
10817  >>> s2 = Contains("abc", "bc")
10818  >>> simplify(s2)
10819  True
10820  >>> x, y, z = Strings('x y z')
10821  >>> s3 = Contains(Concat(x,y,z), y)
10822  >>> simplify(s3)
10823  True
10824  """
10825  ctx = _get_ctx2(a, b)
10826  a = _coerce_seq(a, ctx)
10827  b = _coerce_seq(b, ctx)
10828  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10829 
10830 

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

5094 def CreateDatatypes(*ds):
5095  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
5096 
5097  In the following example we define a Tree-List using two mutually recursive datatypes.
5098 
5099  >>> TreeList = Datatype('TreeList')
5100  >>> Tree = Datatype('Tree')
5101  >>> # Tree has two constructors: leaf and node
5102  >>> Tree.declare('leaf', ('val', IntSort()))
5103  >>> # a node contains a list of trees
5104  >>> Tree.declare('node', ('children', TreeList))
5105  >>> TreeList.declare('nil')
5106  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
5107  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
5108  >>> Tree.val(Tree.leaf(10))
5109  val(leaf(10))
5110  >>> simplify(Tree.val(Tree.leaf(10)))
5111  10
5112  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
5113  >>> n1
5114  node(cons(leaf(10), cons(leaf(20), nil)))
5115  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
5116  >>> simplify(n2 == n1)
5117  False
5118  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
5119  True
5120  """
5121  ds = _get_args(ds)
5122  if z3_debug():
5123  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
5124  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
5125  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
5126  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
5127  ctx = ds[0].ctx
5128  num = len(ds)
5129  names = (Symbol * num)()
5130  out = (Sort * num)()
5131  clists = (ConstructorList * num)()
5132  to_delete = []
5133  for i in range(num):
5134  d = ds[i]
5135  names[i] = to_symbol(d.name, ctx)
5136  num_cs = len(d.constructors)
5137  cs = (Constructor * num_cs)()
5138  for j in range(num_cs):
5139  c = d.constructors[j]
5140  cname = to_symbol(c[0], ctx)
5141  rname = to_symbol(c[1], ctx)
5142  fs = c[2]
5143  num_fs = len(fs)
5144  fnames = (Symbol * num_fs)()
5145  sorts = (Sort * num_fs)()
5146  refs = (ctypes.c_uint * num_fs)()
5147  for k in range(num_fs):
5148  fname = fs[k][0]
5149  ftype = fs[k][1]
5150  fnames[k] = to_symbol(fname, ctx)
5151  if isinstance(ftype, Datatype):
5152  if z3_debug():
5153  _z3_assert(
5154  ds.count(ftype) == 1,
5155  "One and only one occurrence of each datatype is expected",
5156  )
5157  sorts[k] = None
5158  refs[k] = ds.index(ftype)
5159  else:
5160  if z3_debug():
5161  _z3_assert(is_sort(ftype), "Z3 sort expected")
5162  sorts[k] = ftype.ast
5163  refs[k] = 0
5164  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
5165  to_delete.append(ScopedConstructor(cs[j], ctx))
5166  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
5167  to_delete.append(ScopedConstructorList(clists[i], ctx))
5168  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
5169  result = []
5170  # Create a field for every constructor, recognizer and accessor
5171  for i in range(num):
5172  dref = DatatypeSortRef(out[i], ctx)
5173  num_cs = dref.num_constructors()
5174  for j in range(num_cs):
5175  cref = dref.constructor(j)
5176  cref_name = cref.name()
5177  cref_arity = cref.arity()
5178  if cref.arity() == 0:
5179  cref = cref()
5180  setattr(dref, cref_name, cref)
5181  rref = dref.recognizer(j)
5182  setattr(dref, "is_" + cref_name, rref)
5183  for k in range(cref_arity):
5184  aref = dref.accessor(j, k)
5185  setattr(dref, aref.name(), aref)
5186  result.append(dref)
5187  return tuple(result)
5188 
5189 

Referenced by Datatype.create().

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

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

◆ Default()

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

Definition at line 4716 of file z3py.py.

4716 def Default(a):
4717  """ Return a default value for array expression.
4718  >>> b = K(IntSort(), 1)
4719  >>> prove(Default(b) == 1)
4720  proved
4721  """
4722  if z3_debug():
4723  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4724  return a.default()
4725 
4726 

◆ describe_probes()

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

Definition at line 8560 of file z3py.py.

8560 def describe_probes():
8561  """Display a (tabular) description of all available probes in Z3."""
8562  if in_html_mode():
8563  even = True
8564  print('<table border="1" cellpadding="2" cellspacing="0">')
8565  for p in probes():
8566  if even:
8567  print('<tr style="background-color:#CFCFCF">')
8568  even = False
8569  else:
8570  print("<tr>")
8571  even = True
8572  print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
8573  print("</table>")
8574  else:
8575  for p in probes():
8576  print("%s : %s" % (p, probe_description(p)))
8577 
8578 

◆ describe_tactics()

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

Definition at line 8354 of file z3py.py.

8354 def describe_tactics():
8355  """Display a (tabular) description of all available tactics in Z3."""
8356  if in_html_mode():
8357  even = True
8358  print('<table border="1" cellpadding="2" cellspacing="0">')
8359  for t in tactics():
8360  if even:
8361  print('<tr style="background-color:#CFCFCF">')
8362  even = False
8363  else:
8364  print("<tr>")
8365  even = True
8366  print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
8367  print("</table>")
8368  else:
8369  for t in tactics():
8370  print("%s : %s" % (t, tactic_description(t)))
8371 
8372 

◆ Diff()

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

Definition at line 11068 of file z3py.py.

11068 def Diff(a, b, ctx=None):
11069  """Create the difference regular epression
11070  """
11071  return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)
11072 

◆ disable_trace()

def z3py.disable_trace (   msg)

Definition at line 81 of file z3py.py.

81 def disable_trace(msg):
82  Z3_disable_trace(msg)
83 
84 

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

5307 def DisjointSum(name, sorts, ctx=None):
5308  """Create a named tagged union sort base on a set of underlying sorts
5309  Example:
5310  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5311  """
5312  sum = Datatype(name, ctx)
5313  for i in range(len(sorts)):
5314  sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
5315  sum = sum.create()
5316  return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
5317 
5318 

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

1374 def Distinct(*args):
1375  """Create a Z3 distinct expression.
1376 
1377  >>> x = Int('x')
1378  >>> y = Int('y')
1379  >>> Distinct(x, y)
1380  x != y
1381  >>> z = Int('z')
1382  >>> Distinct(x, y, z)
1383  Distinct(x, y, z)
1384  >>> simplify(Distinct(x, y, z))
1385  Distinct(x, y, z)
1386  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1387  And(Not(x == y), Not(x == z), Not(y == z))
1388  """
1389  args = _get_args(args)
1390  ctx = _ctx_from_ast_arg_list(args)
1391  if z3_debug():
1392  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
1393  args = _coerce_expr_list(args, ctx)
1394  _args, sz = _to_ast_array(args)
1395  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1396 
1397 

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

10743 def Empty(s):
10744  """Create the empty sequence of the given sort
10745  >>> e = Empty(StringSort())
10746  >>> e2 = StringVal("")
10747  >>> print(e.eq(e2))
10748  True
10749  >>> e3 = Empty(SeqSort(IntSort()))
10750  >>> print(e3)
10751  Empty(Seq(Int))
10752  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10753  >>> print(e4)
10754  Empty(ReSort(Seq(Int)))
10755  """
10756  if isinstance(s, SeqSortRef):
10757  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10758  if isinstance(s, ReSortRef):
10759  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10760  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10761 
10762 

◆ EmptySet()

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

Definition at line 4858 of file z3py.py.

4858 def EmptySet(s):
4859  """Create the empty set
4860  >>> EmptySet(IntSort())
4861  K(Int, False)
4862  """
4863  ctx = s.ctx
4864  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4865 
4866 

◆ enable_trace()

def z3py.enable_trace (   msg)

Definition at line 77 of file z3py.py.

77 def enable_trace(msg):
78  Z3_enable_trace(msg)
79 
80 

◆ ensure_prop_closures()

def z3py.ensure_prop_closures ( )

Definition at line 11144 of file z3py.py.

11144 def ensure_prop_closures():
11145  global _prop_closures
11146  if _prop_closures is None:
11147  _prop_closures = PropClosures()
11148 
11149 

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

5319 def EnumSort(name, values, ctx=None):
5320  """Return a new enumeration sort named `name` containing the given values.
5321 
5322  The result is a pair (sort, list of constants).
5323  Example:
5324  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5325  """
5326  if z3_debug():
5327  _z3_assert(isinstance(name, str), "Name must be a string")
5328  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
5329  _z3_assert(len(values) > 0, "At least one value expected")
5330  ctx = _get_ctx(ctx)
5331  num = len(values)
5332  _val_names = (Symbol * num)()
5333  for i in range(num):
5334  _val_names[i] = to_symbol(values[i])
5335  _values = (FuncDecl * num)()
5336  _testers = (FuncDecl * num)()
5337  name = to_symbol(name)
5338  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5339  V = []
5340  for i in range(num):
5341  V.append(FuncDeclRef(_values[i], ctx))
5342  V = [a() for a in V]
5343  return S, V
5344 

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

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

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

2207 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2208  """Create a Z3 exists formula.
2209 
2210  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2211 
2212 
2213  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2214  >>> x = Int('x')
2215  >>> y = Int('y')
2216  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2217  >>> q
2218  Exists([x, y], f(x, y) >= x)
2219  >>> is_quantifier(q)
2220  True
2221  >>> r = Tactic('nnf')(q).as_expr()
2222  >>> is_quantifier(r)
2223  False
2224  """
2225  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2226 
2227 

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

4804 def Ext(a, b):
4805  """Return extensionality index for one-dimensional arrays.
4806  >> a, b = Consts('a b', SetSort(IntSort()))
4807  >> Ext(a, b)
4808  Ext(a, b)
4809  """
4810  ctx = a.ctx
4811  if z3_debug():
4812  _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
4813  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4814 
4815 

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

4092 def Extract(high, low, a):
4093  """Create a Z3 bit-vector extraction expression.
4094  Extract is overloaded to also work on sequence extraction.
4095  The functions SubString and SubSeq are redirected to Extract.
4096  For this case, the arguments are reinterpreted as:
4097  high - is a sequence (string)
4098  low - is an offset
4099  a - is the length to be extracted
4100 
4101  >>> x = BitVec('x', 8)
4102  >>> Extract(6, 2, x)
4103  Extract(6, 2, x)
4104  >>> Extract(6, 2, x).sort()
4105  BitVec(5)
4106  >>> simplify(Extract(StringVal("abcd"),2,1))
4107  "c"
4108  """
4109  if isinstance(high, str):
4110  high = StringVal(high)
4111  if is_seq(high):
4112  s = high
4113  offset, length = _coerce_exprs(low, a, s.ctx)
4114  return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
4115  if z3_debug():
4116  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
4117  _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0,
4118  "First and second arguments must be non negative integers")
4119  _z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
4120  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
4121 
4122 

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

8597 def FailIf(p, ctx=None):
8598  """Return a tactic that fails if the probe `p` evaluates to true.
8599  Otherwise, it returns the input goal unmodified.
8600 
8601  In the following example, the tactic applies 'simplify' if and only if there are
8602  more than 2 constraints in the goal.
8603 
8604  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8605  >>> x, y = Ints('x y')
8606  >>> g = Goal()
8607  >>> g.add(x > 0)
8608  >>> g.add(y > 0)
8609  >>> t(g)
8610  [[x > 0, y > 0]]
8611  >>> g.add(x == y + 1)
8612  >>> t(g)
8613  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8614  """
8615  p = _to_probe(p, ctx)
8616  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8617 
8618 

◆ FiniteDomainSort()

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

Definition at line 7601 of file z3py.py.

7601 def FiniteDomainSort(name, sz, ctx=None):
7602  """Create a named finite domain sort of a given size sz"""
7603  if not isinstance(name, Symbol):
7604  name = to_symbol(name)
7605  ctx = _get_ctx(ctx)
7606  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7607 
7608 

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

7671 def FiniteDomainVal(val, sort, ctx=None):
7672  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7673 
7674  >>> s = FiniteDomainSort('S', 256)
7675  >>> FiniteDomainVal(255, s)
7676  255
7677  >>> FiniteDomainVal('100', s)
7678  100
7679  """
7680  if z3_debug():
7681  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
7682  ctx = sort.ctx
7683  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7684 
7685 

◆ Float128()

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

Definition at line 9277 of file z3py.py.

9277 def Float128(ctx=None):
9278  """Floating-point 128-bit (quadruple) sort."""
9279  ctx = _get_ctx(ctx)
9280  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
9281 
9282 

◆ Float16()

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

Definition at line 9241 of file z3py.py.

9241 def Float16(ctx=None):
9242  """Floating-point 16-bit (half) sort."""
9243  ctx = _get_ctx(ctx)
9244  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
9245 
9246 

◆ Float32()

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

Definition at line 9253 of file z3py.py.

9253 def Float32(ctx=None):
9254  """Floating-point 32-bit (single) sort."""
9255  ctx = _get_ctx(ctx)
9256  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
9257 
9258 

◆ Float64()

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

Definition at line 9265 of file z3py.py.

9265 def Float64(ctx=None):
9266  """Floating-point 64-bit (double) sort."""
9267  ctx = _get_ctx(ctx)
9268  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
9269 
9270 

◆ FloatDouble()

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

Definition at line 9271 of file z3py.py.

9271 def FloatDouble(ctx=None):
9272  """Floating-point 64-bit (double) sort."""
9273  ctx = _get_ctx(ctx)
9274  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
9275 
9276 

◆ FloatHalf()

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

Definition at line 9247 of file z3py.py.

9247 def FloatHalf(ctx=None):
9248  """Floating-point 16-bit (half) sort."""
9249  ctx = _get_ctx(ctx)
9250  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
9251 
9252 

◆ FloatQuadruple()

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

Definition at line 9283 of file z3py.py.

9283 def FloatQuadruple(ctx=None):
9284  """Floating-point 128-bit (quadruple) sort."""
9285  ctx = _get_ctx(ctx)
9286  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
9287 
9288 

◆ FloatSingle()

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

Definition at line 9259 of file z3py.py.

9259 def FloatSingle(ctx=None):
9260  """Floating-point 32-bit (single) sort."""
9261  ctx = _get_ctx(ctx)
9262  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
9263 
9264 

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

2189 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2190  """Create a Z3 forall formula.
2191 
2192  The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2193 
2194  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2195  >>> x = Int('x')
2196  >>> y = Int('y')
2197  >>> ForAll([x, y], f(x, y) >= x)
2198  ForAll([x, y], f(x, y) >= x)
2199  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2200  ForAll([x, y], f(x, y) >= x)
2201  >>> ForAll([x, y], f(x, y) >= x, weight=10)
2202  ForAll([x, y], f(x, y) >= x)
2203  """
2204  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2205 
2206 

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

9909 def FP(name, fpsort, ctx=None):
9910  """Return a floating-point constant named `name`.
9911  `fpsort` is the floating-point sort.
9912  If `ctx=None`, then the global context is used.
9913 
9914  >>> x = FP('x', FPSort(8, 24))
9915  >>> is_fp(x)
9916  True
9917  >>> x.ebits()
9918  8
9919  >>> x.sort()
9920  FPSort(8, 24)
9921  >>> word = FPSort(8, 24)
9922  >>> x2 = FP('x', word)
9923  >>> eq(x, x2)
9924  True
9925  """
9926  if isinstance(fpsort, FPSortRef) and ctx is None:
9927  ctx = fpsort.ctx
9928  else:
9929  ctx = _get_ctx(ctx)
9930  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
9931 
9932 

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

9952 def fpAbs(a, ctx=None):
9953  """Create a Z3 floating-point absolute value expression.
9954 
9955  >>> s = FPSort(8, 24)
9956  >>> rm = RNE()
9957  >>> x = FPVal(1.0, s)
9958  >>> fpAbs(x)
9959  fpAbs(1)
9960  >>> y = FPVal(-20.0, s)
9961  >>> y
9962  -1.25*(2**4)
9963  >>> fpAbs(y)
9964  fpAbs(-1.25*(2**4))
9965  >>> fpAbs(-1.25*(2**4))
9966  fpAbs(-1.25*(2**4))
9967  >>> fpAbs(x).sort()
9968  FPSort(8, 24)
9969  """
9970  ctx = _get_ctx(ctx)
9971  [a] = _coerce_fp_expr_list([a], ctx)
9972  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
9973 
9974 

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

10043 def fpAdd(rm, a, b, ctx=None):
10044  """Create a Z3 floating-point addition expression.
10045 
10046  >>> s = FPSort(8, 24)
10047  >>> rm = RNE()
10048  >>> x = FP('x', s)
10049  >>> y = FP('y', s)
10050  >>> fpAdd(rm, x, y)
10051  fpAdd(RNE(), x, y)
10052  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
10053  x + y
10054  >>> fpAdd(rm, x, y).sort()
10055  FPSort(8, 24)
10056  """
10057  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
10058 
10059 

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

10365 def fpBVToFP(v, sort, ctx=None):
10366  """Create a Z3 floating-point conversion expression that represents the
10367  conversion from a bit-vector term to a floating-point term.
10368 
10369  >>> x_bv = BitVecVal(0x3F800000, 32)
10370  >>> x_fp = fpBVToFP(x_bv, Float32())
10371  >>> x_fp
10372  fpToFP(1065353216)
10373  >>> simplify(x_fp)
10374  1
10375  """
10376  _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
10377  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
10378  ctx = _get_ctx(ctx)
10379  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
10380 
10381 

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

10090 def fpDiv(rm, a, b, ctx=None):
10091  """Create a Z3 floating-point division expression.
10092 
10093  >>> s = FPSort(8, 24)
10094  >>> rm = RNE()
10095  >>> x = FP('x', s)
10096  >>> y = FP('y', s)
10097  >>> fpDiv(rm, x, y)
10098  fpDiv(RNE(), x, y)
10099  >>> fpDiv(rm, x, y).sort()
10100  FPSort(8, 24)
10101  """
10102  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
10103 
10104 

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

10273 def fpEQ(a, b, ctx=None):
10274  """Create the Z3 floating-point expression `fpEQ(other, self)`.
10275 
10276  >>> x, y = FPs('x y', FPSort(8, 24))
10277  >>> fpEQ(x, y)
10278  fpEQ(x, y)
10279  >>> fpEQ(x, y).sexpr()
10280  '(fp.eq x y)'
10281  """
10282  return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
10283 
10284 

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

10149 def fpFMA(rm, a, b, c, ctx=None):
10150  """Create a Z3 floating-point fused multiply-add expression.
10151  """
10152  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
10153 
10154 

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

10297 def fpFP(sgn, exp, sig, ctx=None):
10298  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
10299 
10300  >>> s = FPSort(8, 24)
10301  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
10302  >>> print(x)
10303  fpFP(1, 127, 4194304)
10304  >>> xv = FPVal(-1.5, s)
10305  >>> print(xv)
10306  -1.5
10307  >>> slvr = Solver()
10308  >>> slvr.add(fpEQ(x, xv))
10309  >>> slvr.check()
10310  sat
10311  >>> xv = FPVal(+1.5, s)
10312  >>> print(xv)
10313  1.5
10314  >>> slvr = Solver()
10315  >>> slvr.add(fpEQ(x, xv))
10316  >>> slvr.check()
10317  unsat
10318  """
10319  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
10320  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
10321  ctx = _get_ctx(ctx)
10322  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
10323  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
10324 
10325 

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

10382 def fpFPToFP(rm, v, sort, ctx=None):
10383  """Create a Z3 floating-point conversion expression that represents the
10384  conversion from a floating-point term to a floating-point term of different precision.
10385 
10386  >>> x_sgl = FPVal(1.0, Float32())
10387  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
10388  >>> x_dbl
10389  fpToFP(RNE(), 1)
10390  >>> simplify(x_dbl)
10391  1
10392  >>> x_dbl.sort()
10393  FPSort(11, 53)
10394  """
10395  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10396  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
10397  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10398  ctx = _get_ctx(ctx)
10399  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10400 
10401 

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

10261 def fpGEQ(a, b, ctx=None):
10262  """Create the Z3 floating-point expression `other >= self`.
10263 
10264  >>> x, y = FPs('x y', FPSort(8, 24))
10265  >>> fpGEQ(x, y)
10266  x >= y
10267  >>> (x >= y).sexpr()
10268  '(fp.geq x y)'
10269  """
10270  return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
10271 
10272 

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

10249 def fpGT(a, b, ctx=None):
10250  """Create the Z3 floating-point expression `other > self`.
10251 
10252  >>> x, y = FPs('x y', FPSort(8, 24))
10253  >>> fpGT(x, y)
10254  x > y
10255  >>> (x > y).sexpr()
10256  '(fp.gt x y)'
10257  """
10258  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
10259 
10260 

Referenced by FPRef.__gt__().

◆ fpInfinity()

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

Definition at line 9837 of file z3py.py.

9837 def fpInfinity(s, negative):
9838  """Create a Z3 floating-point +oo or -oo term."""
9839  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9840  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9841  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
9842 
9843 

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

10179 def fpIsInf(a, ctx=None):
10180  """Create a Z3 floating-point isInfinite expression.
10181 
10182  >>> s = FPSort(8, 24)
10183  >>> x = FP('x', s)
10184  >>> fpIsInf(x)
10185  fpIsInf(x)
10186  """
10187  return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
10188 
10189 

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

10167 def fpIsNaN(a, ctx=None):
10168  """Create a Z3 floating-point isNaN expression.
10169 
10170  >>> s = FPSort(8, 24)
10171  >>> x = FP('x', s)
10172  >>> y = FP('y', s)
10173  >>> fpIsNaN(x)
10174  fpIsNaN(x)
10175  """
10176  return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
10177 
10178 

◆ fpIsNegative()

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

Definition at line 10208 of file z3py.py.

10208 def fpIsNegative(a, ctx=None):
10209  """Create a Z3 floating-point isNegative expression.
10210  """
10211  return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
10212 
10213 

◆ fpIsNormal()

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

Definition at line 10196 of file z3py.py.

10196 def fpIsNormal(a, ctx=None):
10197  """Create a Z3 floating-point isNormal expression.
10198  """
10199  return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
10200 
10201 

◆ fpIsPositive()

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

Definition at line 10214 of file z3py.py.

10214 def fpIsPositive(a, ctx=None):
10215  """Create a Z3 floating-point isPositive expression.
10216  """
10217  return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
10218 
10219 

◆ fpIsSubnormal()

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

Definition at line 10202 of file z3py.py.

10202 def fpIsSubnormal(a, ctx=None):
10203  """Create a Z3 floating-point isSubnormal expression.
10204  """
10205  return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
10206 
10207 

◆ fpIsZero()

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

Definition at line 10190 of file z3py.py.

10190 def fpIsZero(a, ctx=None):
10191  """Create a Z3 floating-point isZero expression.
10192  """
10193  return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
10194 
10195 

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

10237 def fpLEQ(a, b, ctx=None):
10238  """Create the Z3 floating-point expression `other <= self`.
10239 
10240  >>> x, y = FPs('x y', FPSort(8, 24))
10241  >>> fpLEQ(x, y)
10242  x <= y
10243  >>> (x <= y).sexpr()
10244  '(fp.leq x y)'
10245  """
10246  return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
10247 
10248 

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

10225 def fpLT(a, b, ctx=None):
10226  """Create the Z3 floating-point expression `other < self`.
10227 
10228  >>> x, y = FPs('x y', FPSort(8, 24))
10229  >>> fpLT(x, y)
10230  x < y
10231  >>> (x < y).sexpr()
10232  '(fp.lt x y)'
10233  """
10234  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
10235 
10236 

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

10134 def fpMax(a, b, ctx=None):
10135  """Create a Z3 floating-point maximum expression.
10136 
10137  >>> s = FPSort(8, 24)
10138  >>> rm = RNE()
10139  >>> x = FP('x', s)
10140  >>> y = FP('y', s)
10141  >>> fpMax(x, y)
10142  fpMax(x, y)
10143  >>> fpMax(x, y).sort()
10144  FPSort(8, 24)
10145  """
10146  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
10147 
10148 

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

10119 def fpMin(a, b, ctx=None):
10120  """Create a Z3 floating-point minimum expression.
10121 
10122  >>> s = FPSort(8, 24)
10123  >>> rm = RNE()
10124  >>> x = FP('x', s)
10125  >>> y = FP('y', s)
10126  >>> fpMin(x, y)
10127  fpMin(x, y)
10128  >>> fpMin(x, y).sort()
10129  FPSort(8, 24)
10130  """
10131  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
10132 
10133 

◆ fpMinusInfinity()

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

Definition at line 9831 of file z3py.py.

9831 def fpMinusInfinity(s):
9832  """Create a Z3 floating-point -oo term."""
9833  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9834  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9835 
9836 

Referenced by FPVal().

◆ fpMinusZero()

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

Definition at line 9850 of file z3py.py.

9850 def fpMinusZero(s):
9851  """Create a Z3 floating-point -0.0 term."""
9852  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9853  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
9854 
9855 

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

10075 def fpMul(rm, a, b, ctx=None):
10076  """Create a Z3 floating-point multiplication expression.
10077 
10078  >>> s = FPSort(8, 24)
10079  >>> rm = RNE()
10080  >>> x = FP('x', s)
10081  >>> y = FP('y', s)
10082  >>> fpMul(rm, x, y)
10083  fpMul(RNE(), x, y)
10084  >>> fpMul(rm, x, y).sort()
10085  FPSort(8, 24)
10086  """
10087  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
10088 
10089 

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

9797 def fpNaN(s):
9798  """Create a Z3 floating-point NaN term.
9799 
9800  >>> s = FPSort(8, 24)
9801  >>> set_fpa_pretty(True)
9802  >>> fpNaN(s)
9803  NaN
9804  >>> pb = get_fpa_pretty()
9805  >>> set_fpa_pretty(False)
9806  >>> fpNaN(s)
9807  fpNaN(FPSort(8, 24))
9808  >>> set_fpa_pretty(pb)
9809  """
9810  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9811  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9812 
9813 

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

9975 def fpNeg(a, ctx=None):
9976  """Create a Z3 floating-point addition expression.
9977 
9978  >>> s = FPSort(8, 24)
9979  >>> rm = RNE()
9980  >>> x = FP('x', s)
9981  >>> fpNeg(x)
9982  -x
9983  >>> fpNeg(x).sort()
9984  FPSort(8, 24)
9985  """
9986  ctx = _get_ctx(ctx)
9987  [a] = _coerce_fp_expr_list([a], ctx)
9988  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
9989 
9990 

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

10285 def fpNEQ(a, b, ctx=None):
10286  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
10287 
10288  >>> x, y = FPs('x y', FPSort(8, 24))
10289  >>> fpNEQ(x, y)
10290  Not(fpEQ(x, y))
10291  >>> (x != y).sexpr()
10292  '(distinct x y)'
10293  """
10294  return Not(fpEQ(a, b, ctx))
10295 
10296 

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

9814 def fpPlusInfinity(s):
9815  """Create a Z3 floating-point +oo term.
9816 
9817  >>> s = FPSort(8, 24)
9818  >>> pb = get_fpa_pretty()
9819  >>> set_fpa_pretty(True)
9820  >>> fpPlusInfinity(s)
9821  +oo
9822  >>> set_fpa_pretty(False)
9823  >>> fpPlusInfinity(s)
9824  fpPlusInfinity(FPSort(8, 24))
9825  >>> set_fpa_pretty(pb)
9826  """
9827  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9828  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9829 
9830 

Referenced by FPVal().

◆ fpPlusZero()

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

Definition at line 9844 of file z3py.py.

9844 def fpPlusZero(s):
9845  """Create a Z3 floating-point +0.0 term."""
9846  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9847  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
9848 
9849 

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

10402 def fpRealToFP(rm, v, sort, ctx=None):
10403  """Create a Z3 floating-point conversion expression that represents the
10404  conversion from a real term to a floating-point term.
10405 
10406  >>> x_r = RealVal(1.5)
10407  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
10408  >>> x_fp
10409  fpToFP(RNE(), 3/2)
10410  >>> simplify(x_fp)
10411  1.5
10412  """
10413  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10414  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
10415  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10416  ctx = _get_ctx(ctx)
10417  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10418 
10419 

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

10105 def fpRem(a, b, ctx=None):
10106  """Create a Z3 floating-point remainder expression.
10107 
10108  >>> s = FPSort(8, 24)
10109  >>> x = FP('x', s)
10110  >>> y = FP('y', s)
10111  >>> fpRem(x, y)
10112  fpRem(x, y)
10113  >>> fpRem(x, y).sort()
10114  FPSort(8, 24)
10115  """
10116  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
10117 
10118 

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

10161 def fpRoundToIntegral(rm, a, ctx=None):
10162  """Create a Z3 floating-point roundToIntegral expression.
10163  """
10164  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
10165 
10166 

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

9933 def FPs(names, fpsort, ctx=None):
9934  """Return an array of floating-point constants.
9935 
9936  >>> x, y, z = FPs('x y z', FPSort(8, 24))
9937  >>> x.sort()
9938  FPSort(8, 24)
9939  >>> x.sbits()
9940  24
9941  >>> x.ebits()
9942  8
9943  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9944  fpMul(RNE(), fpAdd(RNE(), x, y), z)
9945  """
9946  ctx = _get_ctx(ctx)
9947  if isinstance(names, str):
9948  names = names.split(" ")
9949  return [FP(name, fpsort, ctx) for name in names]
9950 
9951 

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

10420 def fpSignedToFP(rm, v, sort, ctx=None):
10421  """Create a Z3 floating-point conversion expression that represents the
10422  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
10423 
10424  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10425  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
10426  >>> x_fp
10427  fpToFP(RNE(), 4294967291)
10428  >>> simplify(x_fp)
10429  -1.25*(2**2)
10430  """
10431  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10432  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10433  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10434  ctx = _get_ctx(ctx)
10435  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10436 
10437 

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

9738 def FPSort(ebits, sbits, ctx=None):
9739  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9740 
9741  >>> Single = FPSort(8, 24)
9742  >>> Double = FPSort(11, 53)
9743  >>> Single
9744  FPSort(8, 24)
9745  >>> x = Const('x', Single)
9746  >>> eq(x, FP('x', FPSort(8, 24)))
9747  True
9748  """
9749  ctx = _get_ctx(ctx)
9750  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9751 
9752 

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

10155 def fpSqrt(rm, a, ctx=None):
10156  """Create a Z3 floating-point square root expression.
10157  """
10158  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
10159 
10160 

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

10060 def fpSub(rm, a, b, ctx=None):
10061  """Create a Z3 floating-point subtraction expression.
10062 
10063  >>> s = FPSort(8, 24)
10064  >>> rm = RNE()
10065  >>> x = FP('x', s)
10066  >>> y = FP('y', s)
10067  >>> fpSub(rm, x, y)
10068  fpSub(RNE(), x, y)
10069  >>> fpSub(rm, x, y).sort()
10070  FPSort(8, 24)
10071  """
10072  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
10073 
10074 

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

10326 def fpToFP(a1, a2=None, a3=None, ctx=None):
10327  """Create a Z3 floating-point conversion expression from other term sorts
10328  to floating-point.
10329 
10330  From a bit-vector term in IEEE 754-2008 format:
10331  >>> x = FPVal(1.0, Float32())
10332  >>> x_bv = fpToIEEEBV(x)
10333  >>> simplify(fpToFP(x_bv, Float32()))
10334  1
10335 
10336  From a floating-point term with different precision:
10337  >>> x = FPVal(1.0, Float32())
10338  >>> x_db = fpToFP(RNE(), x, Float64())
10339  >>> x_db.sort()
10340  FPSort(11, 53)
10341 
10342  From a real term:
10343  >>> x_r = RealVal(1.5)
10344  >>> simplify(fpToFP(RNE(), x_r, Float32()))
10345  1.5
10346 
10347  From a signed bit-vector term:
10348  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10349  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
10350  -1.25*(2**2)
10351  """
10352  ctx = _get_ctx(ctx)
10353  if is_bv(a1) and is_fp_sort(a2):
10354  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
10355  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
10356  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10357  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
10358  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10359  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
10360  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10361  else:
10362  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
10363 
10364 

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

10456 def fpToFPUnsigned(rm, x, s, ctx=None):
10457  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
10458  if z3_debug():
10459  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10460  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
10461  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
10462  ctx = _get_ctx(ctx)
10463  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
10464 
10465 

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

10530 def fpToIEEEBV(x, ctx=None):
10531  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
10532 
10533  The size of the resulting bit-vector is automatically determined.
10534 
10535  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
10536  knows only one NaN and it will always produce the same bit-vector representation of
10537  that NaN.
10538 
10539  >>> x = FP('x', FPSort(8, 24))
10540  >>> y = fpToIEEEBV(x)
10541  >>> print(is_fp(x))
10542  True
10543  >>> print(is_bv(y))
10544  True
10545  >>> print(is_fp(y))
10546  False
10547  >>> print(is_bv(x))
10548  False
10549  """
10550  if z3_debug():
10551  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10552  ctx = _get_ctx(ctx)
10553  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
10554 
10555 

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

10510 def fpToReal(x, ctx=None):
10511  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
10512 
10513  >>> x = FP('x', FPSort(8, 24))
10514  >>> y = fpToReal(x)
10515  >>> print(is_fp(x))
10516  True
10517  >>> print(is_real(y))
10518  True
10519  >>> print(is_fp(y))
10520  False
10521  >>> print(is_real(x))
10522  False
10523  """
10524  if z3_debug():
10525  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10526  ctx = _get_ctx(ctx)
10527  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
10528 
10529 

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

10466 def fpToSBV(rm, x, s, ctx=None):
10467  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
10468 
10469  >>> x = FP('x', FPSort(8, 24))
10470  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
10471  >>> print(is_fp(x))
10472  True
10473  >>> print(is_bv(y))
10474  True
10475  >>> print(is_fp(y))
10476  False
10477  >>> print(is_bv(x))
10478  False
10479  """
10480  if z3_debug():
10481  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10482  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10483  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10484  ctx = _get_ctx(ctx)
10485  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10486 
10487 

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

10488 def fpToUBV(rm, x, s, ctx=None):
10489  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
10490 
10491  >>> x = FP('x', FPSort(8, 24))
10492  >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
10493  >>> print(is_fp(x))
10494  True
10495  >>> print(is_bv(y))
10496  True
10497  >>> print(is_fp(y))
10498  False
10499  >>> print(is_bv(x))
10500  False
10501  """
10502  if z3_debug():
10503  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10504  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10505  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10506  ctx = _get_ctx(ctx)
10507  return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10508 
10509 

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

10438 def fpUnsignedToFP(rm, v, sort, ctx=None):
10439  """Create a Z3 floating-point conversion expression that represents the
10440  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
10441 
10442  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10443  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
10444  >>> x_fp
10445  fpToFPUnsigned(RNE(), 4294967291)
10446  >>> simplify(x_fp)
10447  1*(2**32)
10448  """
10449  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10450  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10451  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10452  ctx = _get_ctx(ctx)
10453  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10454 
10455 

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

9863 def FPVal(sig, exp=None, fps=None, ctx=None):
9864  """Return a floating-point value of value `val` and sort `fps`.
9865  If `ctx=None`, then the global context is used.
9866 
9867  >>> v = FPVal(20.0, FPSort(8, 24))
9868  >>> v
9869  1.25*(2**4)
9870  >>> print("0x%.8x" % v.exponent_as_long(False))
9871  0x00000004
9872  >>> v = FPVal(2.25, FPSort(8, 24))
9873  >>> v
9874  1.125*(2**1)
9875  >>> v = FPVal(-2.25, FPSort(8, 24))
9876  >>> v
9877  -1.125*(2**1)
9878  >>> FPVal(-0.0, FPSort(8, 24))
9879  -0.0
9880  >>> FPVal(0.0, FPSort(8, 24))
9881  +0.0
9882  >>> FPVal(+0.0, FPSort(8, 24))
9883  +0.0
9884  """
9885  ctx = _get_ctx(ctx)
9886  if is_fp_sort(exp):
9887  fps = exp
9888  exp = None
9889  elif fps is None:
9890  fps = _dflt_fps(ctx)
9891  _z3_assert(is_fp_sort(fps), "sort mismatch")
9892  if exp is None:
9893  exp = 0
9894  val = _to_float_str(sig)
9895  if val == "NaN" or val == "nan":
9896  return fpNaN(fps)
9897  elif val == "-0.0":
9898  return fpMinusZero(fps)
9899  elif val == "0.0" or val == "+0.0":
9900  return fpPlusZero(fps)
9901  elif val == "+oo" or val == "+inf" or val == "+Inf":
9902  return fpPlusInfinity(fps)
9903  elif val == "-oo" or val == "-inf" or val == "-Inf":
9904  return fpMinusInfinity(fps)
9905  else:
9906  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
9907 
9908 

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

9856 def fpZero(s, negative):
9857  """Create a Z3 floating-point +0.0 or -0.0 term."""
9858  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9859  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9860  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
9861 
9862 

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

1737 def FreshBool(prefix="b", ctx=None):
1738  """Return a fresh Boolean constant in the given context using the given prefix.
1739 
1740  If `ctx=None`, then the global context is used.
1741 
1742  >>> b1 = FreshBool()
1743  >>> b2 = FreshBool()
1744  >>> eq(b1, b2)
1745  False
1746  """
1747  ctx = _get_ctx(ctx)
1748  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1749 
1750 

◆ FreshConst()

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

Definition at line 1434 of file z3py.py.

1434 def FreshConst(sort, prefix="c"):
1435  """Create a fresh constant of a specified sort"""
1436  ctx = _get_ctx(sort.ctx)
1437  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1438 
1439 

◆ FreshFunction()

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

Definition at line 885 of file z3py.py.

885 def FreshFunction(*sig):
886  """Create a new fresh Z3 uninterpreted function with the given sorts.
887  """
888  sig = _get_args(sig)
889  if z3_debug():
890  _z3_assert(len(sig) > 0, "At least two arguments expected")
891  arity = len(sig) - 1
892  rng = sig[arity]
893  if z3_debug():
894  _z3_assert(is_sort(rng), "Z3 sort expected")
895  dom = (z3.Sort * arity)()
896  for i in range(arity):
897  if z3_debug():
898  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
899  dom[i] = sig[i].ast
900  ctx = rng.ctx
901  return FuncDeclRef(Z3_mk_fresh_func_decl(ctx.ref(), "f", arity, dom, rng.ast), ctx)
902 
903 

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

3251 def FreshInt(prefix="x", ctx=None):
3252  """Return a fresh integer constant in the given context using the given prefix.
3253 
3254  >>> x = FreshInt()
3255  >>> y = FreshInt()
3256  >>> eq(x, y)
3257  False
3258  >>> x.sort()
3259  Int
3260  """
3261  ctx = _get_ctx(ctx)
3262  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3263 
3264 

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

3308 def FreshReal(prefix="b", ctx=None):
3309  """Return a fresh real constant in the given context using the given prefix.
3310 
3311  >>> x = FreshReal()
3312  >>> y = FreshReal()
3313  >>> eq(x, y)
3314  False
3315  >>> x.sort()
3316  Real
3317  """
3318  ctx = _get_ctx(ctx)
3319  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3320 
3321 

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

10763 def Full(s):
10764  """Create the regular expression that accepts the universal language
10765  >>> e = Full(ReSort(SeqSort(IntSort())))
10766  >>> print(e)
10767  Full(ReSort(Seq(Int)))
10768  >>> e1 = Full(ReSort(StringSort()))
10769  >>> print(e1)
10770  Full(ReSort(String))
10771  """
10772  if isinstance(s, ReSortRef):
10773  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10774  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10775 
10776 

◆ FullSet()

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

Definition at line 4867 of file z3py.py.

4867 def FullSet(s):
4868  """Create the full set
4869  >>> FullSet(IntSort())
4870  K(Int, True)
4871  """
4872  ctx = s.ctx
4873  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4874 
4875 

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

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

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

6600 def get_as_array_func(n):
6601  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6602  if z3_debug():
6603  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6604  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6605 

Referenced by ModelRef.get_interp().

◆ get_ctx()

def z3py.get_ctx (   ctx)

Definition at line 266 of file z3py.py.

266 def get_ctx(ctx):
267  return _get_ctx(ctx)
268 
269 

◆ get_default_fp_sort()

def z3py.get_default_fp_sort (   ctx = None)

Definition at line 9160 of file z3py.py.

9160 def get_default_fp_sort(ctx=None):
9161  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
9162 
9163 

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

9127 def get_default_rounding_mode(ctx=None):
9128  """Retrieves the global default rounding mode."""
9129  global _dflt_rounding_mode
9130  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
9131  return RTZ(ctx)
9132  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
9133  return RTN(ctx)
9134  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
9135  return RTP(ctx)
9136  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
9137  return RNE(ctx)
9138  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
9139  return RNA(ctx)
9140 
9141 

Referenced by set_default_fp_sort().

◆ get_full_version()

def z3py.get_full_version ( )

Definition at line 103 of file z3py.py.

103 def get_full_version():
104  return Z3_get_full_version()
105 
106 # We use _z3_assert instead of the assert command because we want to
107 # produce nice error messages in Z3Py at rise4fun.com
108 
109 

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

4623 def get_map_func(a):
4624  """Return the function declaration associated with a Z3 map array expression.
4625 
4626  >>> f = Function('f', IntSort(), IntSort())
4627  >>> b = Array('b', IntSort(), IntSort())
4628  >>> a = Map(f, b)
4629  >>> eq(f, get_map_func(a))
4630  True
4631  >>> get_map_func(a)
4632  f
4633  >>> get_map_func(a)(0)
4634  f(0)
4635  """
4636  if z3_debug():
4637  _z3_assert(is_map(a), "Z3 array map expression expected.")
4638  return FuncDeclRef(
4640  a.ctx_ref(),
4641  Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
4642  ),
4643  ctx=a.ctx,
4644  )
4645 
4646 

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

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

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

1305 def get_var_index(a):
1306  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1307 
1308  >>> x = Int('x')
1309  >>> y = Int('y')
1310  >>> is_var(x)
1311  False
1312  >>> is_const(x)
1313  True
1314  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1315  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1316  >>> q = ForAll([x, y], f(x, y) == x + y)
1317  >>> q.body()
1318  f(Var(1), Var(0)) == Var(1) + Var(0)
1319  >>> b = q.body()
1320  >>> b.arg(0)
1321  f(Var(1), Var(0))
1322  >>> v1 = b.arg(0).arg(0)
1323  >>> v2 = b.arg(0).arg(1)
1324  >>> v1
1325  Var(1)
1326  >>> v2
1327  Var(0)
1328  >>> get_var_index(v1)
1329  1
1330  >>> get_var_index(v2)
1331  0
1332  """
1333  if z3_debug():
1334  _z3_assert(is_var(a), "Z3 bound variable expected")
1335  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1336 
1337 

◆ get_version()

def z3py.get_version ( )

Definition at line 94 of file z3py.py.

94 def get_version():
95  major = ctypes.c_uint(0)
96  minor = ctypes.c_uint(0)
97  build = ctypes.c_uint(0)
98  rev = ctypes.c_uint(0)
99  Z3_get_version(major, minor, build, rev)
100  return (major.value, minor.value, build.value, rev.value)
101 
102 

◆ get_version_string()

def z3py.get_version_string ( )

Definition at line 85 of file z3py.py.

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

◆ help_simplify()

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

Definition at line 8681 of file z3py.py.

8681 def help_simplify():
8682  """Return a string describing all options available for Z3 `simplify` procedure."""
8683  print(Z3_simplify_get_help(main_ctx().ref()))
8684 
8685 

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

1351 def If(a, b, c, ctx=None):
1352  """Create a Z3 if-then-else expression.
1353 
1354  >>> x = Int('x')
1355  >>> y = Int('y')
1356  >>> max = If(x > y, x, y)
1357  >>> max
1358  If(x > y, x, y)
1359  >>> simplify(max)
1360  If(x <= y, y, x)
1361  """
1362  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1363  return Cond(a, b, c, ctx)
1364  else:
1365  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1366  s = BoolSort(ctx)
1367  a = s.cast(a)
1368  b, c = _coerce_exprs(b, c, ctx)
1369  if z3_debug():
1370  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1371  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1372 
1373 

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

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

1751 def Implies(a, b, ctx=None):
1752  """Create a Z3 implies expression.
1753 
1754  >>> p, q = Bools('p q')
1755  >>> Implies(p, q)
1756  Implies(p, q)
1757  """
1758  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1759  s = BoolSort(ctx)
1760  a = s.cast(a)
1761  b = s.cast(b)
1762  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1763 
1764 

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

10846 def IndexOf(s, substr, offset=None):
10847  """Retrieve the index of substring within a string starting at a specified offset.
10848  >>> simplify(IndexOf("abcabc", "bc", 0))
10849  1
10850  >>> simplify(IndexOf("abcabc", "bc", 2))
10851  4
10852  """
10853  if offset is None:
10854  offset = IntVal(0)
10855  ctx = None
10856  if is_expr(offset):
10857  ctx = offset.ctx
10858  ctx = _get_ctx2(s, substr, ctx)
10859  s = _coerce_seq(s, ctx)
10860  substr = _coerce_seq(substr, ctx)
10861  if _is_int(offset):
10862  offset = IntVal(offset, ctx)
10863  return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
10864 
10865 

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

10947 def InRe(s, re):
10948  """Create regular expression membership test
10949  >>> re = Union(Re("a"),Re("b"))
10950  >>> print (simplify(InRe("a", re)))
10951  True
10952  >>> print (simplify(InRe("b", re)))
10953  True
10954  >>> print (simplify(InRe("c", re)))
10955  False
10956  """
10957  s = _coerce_seq(s, re.ctx)
10958  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
10959 
10960 

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

3212 def Int(name, ctx=None):
3213  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3214 
3215  >>> x = Int('x')
3216  >>> is_int(x)
3217  True
3218  >>> is_int(x + 1)
3219  True
3220  """
3221  ctx = _get_ctx(ctx)
3222  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3223 
3224 

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

3960 def Int2BV(a, num_bits):
3961  """Return the z3 expression Int2BV(a, num_bits).
3962  It is a bit-vector of width num_bits and represents the
3963  modulo of a by 2^num_bits
3964  """
3965  ctx = a.ctx
3966  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
3967 
3968 

◆ Intersect()

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

Definition at line 10981 of file z3py.py.

10981 def Intersect(*args):
10982  """Create intersection of regular expressions.
10983  >>> re = Intersect(Re("a"), Re("b"), Re("c"))
10984  """
10985  args = _get_args(args)
10986  sz = len(args)
10987  if z3_debug():
10988  _z3_assert(sz > 0, "At least one argument expected.")
10989  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
10990  if sz == 1:
10991  return args[0]
10992  ctx = args[0].ctx
10993  v = (Ast * sz)()
10994  for i in range(sz):
10995  v[i] = args[i].as_ast()
10996  return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
10997 
10998 

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

3225 def Ints(names, ctx=None):
3226  """Return a tuple of Integer constants.
3227 
3228  >>> x, y, z = Ints('x y z')
3229  >>> Sum(x, y, z)
3230  x + y + z
3231  """
3232  ctx = _get_ctx(ctx)
3233  if isinstance(names, str):
3234  names = names.split(" ")
3235  return [Int(name, ctx) for name in names]
3236 
3237 

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

3102 def IntSort(ctx=None):
3103  """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
3104 
3105  >>> IntSort()
3106  Int
3107  >>> x = Const('x', IntSort())
3108  >>> is_int(x)
3109  True
3110  >>> x.sort() == IntSort()
3111  True
3112  >>> x.sort() == BoolSort()
3113  False
3114  """
3115  ctx = _get_ctx(ctx)
3116  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
3117 
3118 

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

◆ IntToStr()

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

Definition at line 10901 of file z3py.py.

10901 def IntToStr(s):
10902  """Convert integer expression to string"""
10903  if not is_expr(s):
10904  s = _py2expr(s)
10905  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
10906 
10907 

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

3152 def IntVal(val, ctx=None):
3153  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3154 
3155  >>> IntVal(1)
3156  1
3157  >>> IntVal("100")
3158  100
3159  """
3160  ctx = _get_ctx(ctx)
3161  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3162 
3163 

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

3238 def IntVector(prefix, sz, ctx=None):
3239  """Return a list of integer constants of size `sz`.
3240 
3241  >>> X = IntVector('x', 3)
3242  >>> X
3243  [x__0, x__1, x__2]
3244  >>> Sum(X)
3245  x__0 + x__1 + x__2
3246  """
3247  ctx = _get_ctx(ctx)
3248  return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3249 
3250 

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

2756 def is_add(a):
2757  """Return `True` if `a` is an expression of the form b + c.
2758 
2759  >>> x, y = Ints('x y')
2760  >>> is_add(x + y)
2761  True
2762  >>> is_add(x - y)
2763  False
2764  """
2765  return is_app_of(a, Z3_OP_ADD)
2766 
2767 

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

2742 def is_algebraic_value(a):
2743  """Return `True` if `a` is an algebraic value of sort Real.
2744 
2745  >>> is_algebraic_value(RealVal("3/5"))
2746  False
2747  >>> n = simplify(Sqrt(2))
2748  >>> n
2749  1.4142135623?
2750  >>> is_algebraic_value(n)
2751  True
2752  """
2753  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2754 
2755 

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

1587 def is_and(a):
1588  """Return `True` if `a` is a Z3 and expression.
1589 
1590  >>> p, q = Bools('p q')
1591  >>> is_and(And(p, q))
1592  True
1593  >>> is_and(Or(p, q))
1594  False
1595  """
1596  return is_app_of(a, Z3_OP_AND)
1597 
1598 

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

1235 def is_app(a):
1236  """Return `True` if `a` is a Z3 function application.
1237 
1238  Note that, constants are function applications with 0 arguments.
1239 
1240  >>> a = Int('a')
1241  >>> is_app(a)
1242  True
1243  >>> is_app(a + 1)
1244  True
1245  >>> is_app(IntSort())
1246  False
1247  >>> is_app(1)
1248  False
1249  >>> is_app(IntVal(1))
1250  True
1251  >>> x = Int('x')
1252  >>> is_app(ForAll(x, x >= 0))
1253  False
1254  """
1255  if not isinstance(a, ExprRef):
1256  return False
1257  k = _ast_kind(a.ctx, a)
1258  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
1259 
1260 

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

1338 def is_app_of(a, k):
1339  """Return `True` if `a` is an application of the given kind `k`.
1340 
1341  >>> x = Int('x')
1342  >>> n = x + 1
1343  >>> is_app_of(n, Z3_OP_ADD)
1344  True
1345  >>> is_app_of(n, Z3_OP_MUL)
1346  False
1347  """
1348  return is_app(a) and a.decl().kind() == k
1349 
1350 

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

2629 def is_arith(a):
2630  """Return `True` if `a` is an arithmetical expression.
2631 
2632  >>> x = Int('x')
2633  >>> is_arith(x)
2634  True
2635  >>> is_arith(x + 1)
2636  True
2637  >>> is_arith(1)
2638  False
2639  >>> is_arith(IntVal(1))
2640  True
2641  >>> y = Real('y')
2642  >>> is_arith(y)
2643  True
2644  >>> is_arith(y + 1)
2645  True
2646  """
2647  return isinstance(a, ArithRef)
2648 
2649 

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

2328 def is_arith_sort(s):
2329  """Return `True` if s is an arithmetical sort (type).
2330 
2331  >>> is_arith_sort(IntSort())
2332  True
2333  >>> is_arith_sort(RealSort())
2334  True
2335  >>> is_arith_sort(BoolSort())
2336  False
2337  >>> n = Int('x') + 1
2338  >>> is_arith_sort(n.sort())
2339  True
2340  """
2341  return isinstance(s, ArithSortRef)
2342 
2343 

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

4558 def is_array(a):
4559  """Return `True` if `a` is a Z3 array expression.
4560 
4561  >>> a = Array('a', IntSort(), IntSort())
4562  >>> is_array(a)
4563  True
4564  >>> is_array(Store(a, 0, 1))
4565  True
4566  >>> is_array(a[0])
4567  False
4568  """
4569  return isinstance(a, ArrayRef)
4570 
4571 

Referenced by Ext(), and Map().

◆ is_array_sort()

def z3py.is_array_sort (   a)

Definition at line 4554 of file z3py.py.

4554 def is_array_sort(a):
4555  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4556 
4557 

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

6595 def is_as_array(n):
6596  """Return true if n is a Z3 expression of the form (_ as-array f)."""
6597  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6598 
6599 

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

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

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

1537 def is_bool(a):
1538  """Return `True` if `a` is a Z3 Boolean expression.
1539 
1540  >>> p = Bool('p')
1541  >>> is_bool(p)
1542  True
1543  >>> q = Bool('q')
1544  >>> is_bool(And(p, q))
1545  True
1546  >>> x = Real('x')
1547  >>> is_bool(x)
1548  False
1549  >>> is_bool(x == 0)
1550  True
1551  """
1552  return isinstance(a, BoolRef)
1553 
1554 

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

3908 def is_bv(a):
3909  """Return `True` if `a` is a Z3 bit-vector expression.
3910 
3911  >>> b = BitVec('b', 32)
3912  >>> is_bv(b)
3913  True
3914  >>> is_bv(b + 10)
3915  True
3916  >>> is_bv(Int('x'))
3917  False
3918  """
3919  return isinstance(a, BitVecRef)
3920 
3921 

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

3440 def is_bv_sort(s):
3441  """Return True if `s` is a Z3 bit-vector sort.
3442 
3443  >>> is_bv_sort(BitVecSort(32))
3444  True
3445  >>> is_bv_sort(IntSort())
3446  False
3447  """
3448  return isinstance(s, BitVecSortRef)
3449 
3450 

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

3922 def is_bv_value(a):
3923  """Return `True` if `a` is a Z3 bit-vector numeral value.
3924 
3925  >>> b = BitVec('b', 32)
3926  >>> is_bv_value(b)
3927  False
3928  >>> b = BitVecVal(10, 32)
3929  >>> b
3930  10
3931  >>> is_bv_value(b)
3932  True
3933  """
3934  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3935 
3936 

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

1261 def is_const(a):
1262  """Return `True` if `a` is Z3 constant/variable expression.
1263 
1264  >>> a = Int('a')
1265  >>> is_const(a)
1266  True
1267  >>> is_const(a + 1)
1268  False
1269  >>> is_const(1)
1270  False
1271  >>> is_const(IntVal(1))
1272  True
1273  >>> x = Int('x')
1274  >>> is_const(ForAll(x, x >= 0))
1275  False
1276  """
1277  return is_app(a) and a.num_args() == 0
1278 
1279 

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

4572 def is_const_array(a):
4573  """Return `True` if `a` is a Z3 constant array.
4574 
4575  >>> a = K(IntSort(), 10)
4576  >>> is_const_array(a)
4577  True
4578  >>> a = Array('a', IntSort(), IntSort())
4579  >>> is_const_array(a)
4580  False
4581  """
4582  return is_app_of(a, Z3_OP_CONST_ARRAY)
4583 
4584 

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

4614 def is_default(a):
4615  """Return `True` if `a` is a Z3 default array expression.
4616  >>> d = Default(K(IntSort(), 10))
4617  >>> is_default(d)
4618  True
4619  """
4620  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4621 
4622 

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

1645 def is_distinct(a):
1646  """Return `True` if `a` is a Z3 distinct expression.
1647 
1648  >>> x, y, z = Ints('x y z')
1649  >>> is_distinct(x == y)
1650  False
1651  >>> is_distinct(Distinct(x, y, z))
1652  True
1653  """
1654  return is_app_of(a, Z3_OP_DISTINCT)
1655 
1656 

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

2792 def is_div(a):
2793  """Return `True` if `a` is an expression of the form b / c.
2794 
2795  >>> x, y = Reals('x y')
2796  >>> is_div(x / y)
2797  True
2798  >>> is_div(x + y)
2799  False
2800  >>> x, y = Ints('x y')
2801  >>> is_div(x / y)
2802  False
2803  >>> is_idiv(x / y)
2804  True
2805  """
2806  return is_app_of(a, Z3_OP_DIV)
2807 
2808 

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

1635 def is_eq(a):
1636  """Return `True` if `a` is a Z3 equality expression.
1637 
1638  >>> x, y = Ints('x y')
1639  >>> is_eq(x == y)
1640  True
1641  """
1642  return is_app_of(a, Z3_OP_EQ)
1643 
1644 

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

1212 def is_expr(a):
1213  """Return `True` if `a` is a Z3 expression.
1214 
1215  >>> a = Int('a')
1216  >>> is_expr(a)
1217  True
1218  >>> is_expr(a + 1)
1219  True
1220  >>> is_expr(IntSort())
1221  False
1222  >>> is_expr(1)
1223  False
1224  >>> is_expr(IntVal(1))
1225  True
1226  >>> x = Int('x')
1227  >>> is_expr(ForAll(x, x >= 0))
1228  True
1229  >>> is_expr(FPVal(1.0))
1230  True
1231  """
1232  return isinstance(a, ExprRef)
1233 
1234 

Referenced by SeqRef.__gt__(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), ExprRef.children(), Concat(), AlgebraicNumRef.index(), IndexOf(), IntToStr(), is_quantifier(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), substitute(), 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 1573 of file z3py.py.

1573 def is_false(a):
1574  """Return `True` if `a` is the Z3 false expression.
1575 
1576  >>> p = Bool('p')
1577  >>> is_false(p)
1578  False
1579  >>> is_false(False)
1580  False
1581  >>> is_false(BoolVal(False))
1582  True
1583  """
1584  return is_app_of(a, Z3_OP_FALSE)
1585 
1586 

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

7632 def is_finite_domain(a):
7633  """Return `True` if `a` is a Z3 finite-domain expression.
7634 
7635  >>> s = FiniteDomainSort('S', 100)
7636  >>> b = Const('b', s)
7637  >>> is_finite_domain(b)
7638  True
7639  >>> is_finite_domain(Int('x'))
7640  False
7641  """
7642  return isinstance(a, FiniteDomainRef)
7643 
7644 

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

7609 def is_finite_domain_sort(s):
7610  """Return True if `s` is a Z3 finite-domain sort.
7611 
7612  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7613  True
7614  >>> is_finite_domain_sort(IntSort())
7615  False
7616  """
7617  return isinstance(s, FiniteDomainSortRef)
7618 
7619 

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

7686 def is_finite_domain_value(a):
7687  """Return `True` if `a` is a Z3 finite-domain value.
7688 
7689  >>> s = FiniteDomainSort('S', 100)
7690  >>> b = Const('b', s)
7691  >>> is_finite_domain_value(b)
7692  False
7693  >>> b = FiniteDomainVal(10, s)
7694  >>> b
7695  10
7696  >>> is_finite_domain_value(b)
7697  True
7698  """
7699  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7700 
7701 

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

9709 def is_fp(a):
9710  """Return `True` if `a` is a Z3 floating-point expression.
9711 
9712  >>> b = FP('b', FPSort(8, 24))
9713  >>> is_fp(b)
9714  True
9715  >>> is_fp(b + 1.0)
9716  True
9717  >>> is_fp(Int('x'))
9718  False
9719  """
9720  return isinstance(a, FPRef)
9721 
9722 

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

9293 def is_fp_sort(s):
9294  """Return True if `s` is a Z3 floating-point sort.
9295 
9296  >>> is_fp_sort(FPSort(8, 24))
9297  True
9298  >>> is_fp_sort(IntSort())
9299  False
9300  """
9301  return isinstance(s, FPSortRef)
9302 
9303 

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

9723 def is_fp_value(a):
9724  """Return `True` if `a` is a Z3 floating-point numeral value.
9725 
9726  >>> b = FP('b', FPSort(8, 24))
9727  >>> is_fp_value(b)
9728  False
9729  >>> b = FPVal(1.0, FPSort(8, 24))
9730  >>> b
9731  1
9732  >>> is_fp_value(b)
9733  True
9734  """
9735  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9736 
9737 

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

9553 def is_fprm(a):
9554  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9555 
9556  >>> rm = RNE()
9557  >>> is_fprm(rm)
9558  True
9559  >>> rm = 1.0
9560  >>> is_fprm(rm)
9561  False
9562  """
9563  return isinstance(a, FPRMRef)
9564 
9565 

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

9304 def is_fprm_sort(s):
9305  """Return True if `s` is a Z3 floating-point rounding mode sort.
9306 
9307  >>> is_fprm_sort(FPSort(8, 24))
9308  False
9309  >>> is_fprm_sort(RNE().sort())
9310  True
9311  """
9312  return isinstance(s, FPRMSortRef)
9313 
9314 # FP Expressions
9315 
9316 

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

9566 def is_fprm_value(a):
9567  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9568  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9569 
9570 # FP Numerals
9571 
9572 

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

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

Referenced by Map(), prove(), 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 2857 of file z3py.py.

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

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

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

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

2809 def is_idiv(a):
2810  """Return `True` if `a` is an expression of the form b div c.
2811 
2812  >>> x, y = Ints('x y')
2813  >>> is_idiv(x / y)
2814  True
2815  >>> is_idiv(x + y)
2816  False
2817  """
2818  return is_app_of(a, Z3_OP_IDIV)
2819 
2820 

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

1611 def is_implies(a):
1612  """Return `True` if `a` is a Z3 implication expression.
1613 
1614  >>> p, q = Bools('p q')
1615  >>> is_implies(Implies(p, q))
1616  True
1617  >>> is_implies(And(p, q))
1618  False
1619  """
1620  return is_app_of(a, Z3_OP_IMPLIES)
1621 
1622 

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

2650 def is_int(a):
2651  """Return `True` if `a` is an integer expression.
2652 
2653  >>> x = Int('x')
2654  >>> is_int(x + 1)
2655  True
2656  >>> is_int(1)
2657  False
2658  >>> is_int(IntVal(1))
2659  True
2660  >>> y = Real('y')
2661  >>> is_int(y)
2662  False
2663  >>> is_int(y + 1)
2664  False
2665  """
2666  return is_arith(a) and a.is_int()
2667 
2668 

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

2696 def is_int_value(a):
2697  """Return `True` if `a` is an integer value of sort Int.
2698 
2699  >>> is_int_value(IntVal(1))
2700  True
2701  >>> is_int_value(1)
2702  False
2703  >>> is_int_value(Int('x'))
2704  False
2705  >>> n = Int('x') + 1
2706  >>> n
2707  x + 1
2708  >>> n.arg(1)
2709  1
2710  >>> is_int_value(n.arg(1))
2711  True
2712  >>> is_int_value(RealVal("1/3"))
2713  False
2714  >>> is_int_value(RealVal(1))
2715  False
2716  """
2717  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2718 
2719 

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

2881 def is_is_int(a):
2882  """Return `True` if `a` is an expression of the form IsInt(b).
2883 
2884  >>> x = Real('x')
2885  >>> is_is_int(IsInt(x))
2886  True
2887  >>> is_is_int(x)
2888  False
2889  """
2890  return is_app_of(a, Z3_OP_IS_INT)
2891 
2892 

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

4585 def is_K(a):
4586  """Return `True` if `a` is a Z3 constant array.
4587 
4588  >>> a = K(IntSort(), 10)
4589  >>> is_K(a)
4590  True
4591  >>> a = Array('a', IntSort(), IntSort())
4592  >>> is_K(a)
4593  False
4594  """
4595  return is_app_of(a, Z3_OP_CONST_ARRAY)
4596 
4597 

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

2833 def is_le(a):
2834  """Return `True` if `a` is an expression of the form b <= c.
2835 
2836  >>> x, y = Ints('x y')
2837  >>> is_le(x <= y)
2838  True
2839  >>> is_le(x < y)
2840  False
2841  """
2842  return is_app_of(a, Z3_OP_LE)
2843 
2844 

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

2845 def is_lt(a):
2846  """Return `True` if `a` is an expression of the form b < c.
2847 
2848  >>> x, y = Ints('x y')
2849  >>> is_lt(x < y)
2850  True
2851  >>> is_lt(x == y)
2852  False
2853  """
2854  return is_app_of(a, Z3_OP_LT)
2855 
2856 

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

4598 def is_map(a):
4599  """Return `True` if `a` is a Z3 map array expression.
4600 
4601  >>> f = Function('f', IntSort(), IntSort())
4602  >>> b = Array('b', IntSort(), IntSort())
4603  >>> a = Map(f, b)
4604  >>> a
4605  Map(f, b)
4606  >>> is_map(a)
4607  True
4608  >>> is_map(b)
4609  False
4610  """
4611  return is_app_of(a, Z3_OP_ARRAY_MAP)
4612 
4613 

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

2821 def is_mod(a):
2822  """Return `True` if `a` is an expression of the form b % c.
2823 
2824  >>> x, y = Ints('x y')
2825  >>> is_mod(x % y)
2826  True
2827  >>> is_mod(x + y)
2828  False
2829  """
2830  return is_app_of(a, Z3_OP_MOD)
2831 
2832 

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

2768 def is_mul(a):
2769  """Return `True` if `a` is an expression of the form b * c.
2770 
2771  >>> x, y = Ints('x y')
2772  >>> is_mul(x * y)
2773  True
2774  >>> is_mul(x - y)
2775  False
2776  """
2777  return is_app_of(a, Z3_OP_MUL)
2778 
2779 

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

1623 def is_not(a):
1624  """Return `True` if `a` is a Z3 not expression.
1625 
1626  >>> p = Bool('p')
1627  >>> is_not(p)
1628  False
1629  >>> is_not(Not(p))
1630  True
1631  """
1632  return is_app_of(a, Z3_OP_NOT)
1633 
1634 

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

1599 def is_or(a):
1600  """Return `True` if `a` is a Z3 or expression.
1601 
1602  >>> p, q = Bools('p q')
1603  >>> is_or(Or(p, q))
1604  True
1605  >>> is_or(And(p, q))
1606  False
1607  """
1608  return is_app_of(a, Z3_OP_OR)
1609 
1610 

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

1899 def is_pattern(a):
1900  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1901 
1902  >>> f = Function('f', IntSort(), IntSort())
1903  >>> x = Int('x')
1904  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1905  >>> q
1906  ForAll(x, f(x) == 0)
1907  >>> q.num_patterns()
1908  1
1909  >>> is_pattern(q.pattern(0))
1910  True
1911  >>> q.pattern(0)
1912  f(Var(0))
1913  """
1914  return isinstance(a, PatternRef)
1915 
1916 

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

8522 def is_probe(p):
8523  """Return `True` if `p` is a Z3 probe.
8524 
8525  >>> is_probe(Int('x'))
8526  False
8527  >>> is_probe(Probe('memory'))
8528  True
8529  """
8530  return isinstance(p, Probe)
8531 
8532 

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

2140 def is_quantifier(a):
2141  """Return `True` if `a` is a Z3 quantifier.
2142 
2143  >>> f = Function('f', IntSort(), IntSort())
2144  >>> x = Int('x')
2145  >>> q = ForAll(x, f(x) == 0)
2146  >>> is_quantifier(q)
2147  True
2148  >>> is_quantifier(f(x))
2149  False
2150  """
2151  return isinstance(a, QuantifierRef)
2152 
2153 

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

2720 def is_rational_value(a):
2721  """Return `True` if `a` is rational value of sort Real.
2722 
2723  >>> is_rational_value(RealVal(1))
2724  True
2725  >>> is_rational_value(RealVal("3/5"))
2726  True
2727  >>> is_rational_value(IntVal(1))
2728  False
2729  >>> is_rational_value(1)
2730  False
2731  >>> n = Real('x') + 1
2732  >>> n.arg(1)
2733  1
2734  >>> is_rational_value(n.arg(1))
2735  True
2736  >>> is_rational_value(Real('x'))
2737  False
2738  """
2739  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2740 
2741 

◆ is_re()

def z3py.is_re (   s)

Definition at line 10943 of file z3py.py.

10943 def is_re(s):
10944  return isinstance(s, ReRef)
10945 
10946 

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

2669 def is_real(a):
2670  """Return `True` if `a` is a real expression.
2671 
2672  >>> x = Int('x')
2673  >>> is_real(x + 1)
2674  False
2675  >>> y = Real('y')
2676  >>> is_real(y)
2677  True
2678  >>> is_real(y + 1)
2679  True
2680  >>> is_real(1)
2681  False
2682  >>> is_real(RealVal(1))
2683  True
2684  """
2685  return is_arith(a) and a.is_real()
2686 
2687 

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

4822 def is_select(a):
4823  """Return `True` if `a` is a Z3 array select application.
4824 
4825  >>> a = Array('a', IntSort(), IntSort())
4826  >>> is_select(a)
4827  False
4828  >>> i = Int('i')
4829  >>> is_select(a[i])
4830  True
4831  """
4832  return is_app_of(a, Z3_OP_SELECT)
4833 
4834 

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

10682 def is_seq(a):
10683  """Return `True` if `a` is a Z3 sequence expression.
10684  >>> print (is_seq(Unit(IntVal(0))))
10685  True
10686  >>> print (is_seq(StringVal("abc")))
10687  True
10688  """
10689  return isinstance(a, SeqRef)
10690 
10691 

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

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

Referenced by ArraySort(), CreateDatatypes(), FreshFunction(), Function(), IsSubset(), K(), 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 4835 of file z3py.py.

4835 def is_store(a):
4836  """Return `True` if `a` is a Z3 array store application.
4837 
4838  >>> a = Array('a', IntSort(), IntSort())
4839  >>> is_store(a)
4840  False
4841  >>> is_store(Store(a, 0, 1))
4842  True
4843  """
4844  return is_app_of(a, Z3_OP_STORE)
4845 

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

10692 def is_string(a):
10693  """Return `True` if `a` is a Z3 string expression.
10694  >>> print (is_string(StringVal("ab")))
10695  True
10696  """
10697  return isinstance(a, SeqRef) and a.is_string()
10698 
10699 

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

10700 def is_string_value(a):
10701  """return 'True' if 'a' is a Z3 string constant expression.
10702  >>> print (is_string_value(StringVal("a")))
10703  True
10704  >>> print (is_string_value(StringVal("a") + StringVal("b")))
10705  False
10706  """
10707  return isinstance(a, SeqRef) and a.is_string_value()
10708 

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

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

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

2908 def is_to_int(a):
2909  """Return `True` if `a` is an expression of the form ToInt(b).
2910 
2911  >>> x = Real('x')
2912  >>> n = ToInt(x)
2913  >>> n
2914  ToInt(x)
2915  >>> is_to_int(n)
2916  True
2917  >>> is_to_int(x)
2918  False
2919  """
2920  return is_app_of(a, Z3_OP_TO_INT)
2921 
2922 

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

2893 def is_to_real(a):
2894  """Return `True` if `a` is an expression of the form ToReal(b).
2895 
2896  >>> x = Int('x')
2897  >>> n = ToReal(x)
2898  >>> n
2899  ToReal(x)
2900  >>> is_to_real(n)
2901  True
2902  >>> is_to_real(x)
2903  False
2904  """
2905  return is_app_of(a, Z3_OP_TO_REAL)
2906 
2907 

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

1555 def is_true(a):
1556  """Return `True` if `a` is the Z3 true expression.
1557 
1558  >>> p = Bool('p')
1559  >>> is_true(p)
1560  False
1561  >>> is_true(simplify(p == p))
1562  True
1563  >>> x = Real('x')
1564  >>> is_true(x == 0)
1565  False
1566  >>> # True is a Python Boolean expression
1567  >>> is_true(True)
1568  False
1569  """
1570  return is_app_of(a, Z3_OP_TRUE)
1571 
1572 

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

1280 def is_var(a):
1281  """Return `True` if `a` is variable.
1282 
1283  Z3 uses de-Bruijn indices for representing bound variables in
1284  quantifiers.
1285 
1286  >>> x = Int('x')
1287  >>> is_var(x)
1288  False
1289  >>> is_const(x)
1290  True
1291  >>> f = Function('f', IntSort(), IntSort())
1292  >>> # Z3 replaces x with bound variables when ForAll is executed.
1293  >>> q = ForAll(x, f(x) == x)
1294  >>> b = q.body()
1295  >>> b
1296  f(Var(0)) == Var(0)
1297  >>> b.arg(1)
1298  Var(0)
1299  >>> is_var(b.arg(1))
1300  True
1301  """
1302  return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
1303 
1304 

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

3358 def IsInt(a):
3359  """ Return the Z3 predicate IsInt(a).
3360 
3361  >>> x = Real('x')
3362  >>> IsInt(x + "1/2")
3363  IsInt(x + 1/2)
3364  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3365  [x = 1/2]
3366  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3367  no solution
3368  """
3369  if z3_debug():
3370  _z3_assert(a.is_real(), "Z3 real expression expected.")
3371  ctx = a.ctx
3372  return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
3373 
3374 

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

4945 def IsMember(e, s):
4946  """ Check if e is a member of set s
4947  >>> a = Const('a', SetSort(IntSort()))
4948  >>> IsMember(1, a)
4949  a[1]
4950  """
4951  ctx = _ctx_from_ast_arg_list([s, e])
4952  e = _py2expr(e, ctx)
4953  return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
4954 
4955 

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

4956 def IsSubset(a, b):
4957  """ Check if a is a subset of b
4958  >>> a = Const('a', SetSort(IntSort()))
4959  >>> b = Const('b', SetSort(IntSort()))
4960  >>> IsSubset(a, b)
4961  subset(a, b)
4962  """
4963  ctx = _ctx_from_ast_arg_list([a, b])
4964  return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4965 
4966 

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

4782 def K(dom, v):
4783  """Return a Z3 constant array expression.
4784 
4785  >>> a = K(IntSort(), 10)
4786  >>> a
4787  K(Int, 10)
4788  >>> a.sort()
4789  Array(Int, Int)
4790  >>> i = Int('i')
4791  >>> a[i]
4792  K(Int, 10)[i]
4793  >>> simplify(a[i])
4794  10
4795  """
4796  if z3_debug():
4797  _z3_assert(is_sort(dom), "Z3 sort expected")
4798  ctx = dom.ctx
4799  if not is_expr(v):
4800  v = _py2expr(v, ctx)
4801  return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
4802 
4803 

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

2228 def Lambda(vs, body):
2229  """Create a Z3 lambda expression.
2230 
2231  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2232  >>> mem0 = Array('mem0', IntSort(), IntSort())
2233  >>> lo, hi, e, i = Ints('lo hi e i')
2234  >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2235  >>> mem1
2236  Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2237  """
2238  ctx = body.ctx
2239  if is_app(vs):
2240  vs = [vs]
2241  num_vars = len(vs)
2242  _vs = (Ast * num_vars)()
2243  for i in range(num_vars):
2244  # TODO: Check if is constant
2245  _vs[i] = vs[i].as_ast()
2246  return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)
2247 

Referenced by Context.MkLambda().

◆ LastIndexOf()

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

Definition at line 10866 of file z3py.py.

10866 def LastIndexOf(s, substr):
10867  """Retrieve the last index of substring within a string"""
10868  ctx = None
10869  ctx = _get_ctx2(s, substr, ctx)
10870  s = _coerce_seq(s, ctx)
10871  substr = _coerce_seq(substr, ctx)
10872  return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx)
10873 
10874 

◆ Length()

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

Definition at line 10875 of file z3py.py.

10875 def Length(s):
10876  """Obtain the length of a sequence 's'
10877  >>> l = Length(StringVal("abc"))
10878  >>> simplify(l)
10879  3
10880  """
10881  s = _coerce_seq(s)
10882  return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
10883 
10884 

◆ LinearOrder()

def z3py.LinearOrder (   a,
  index 
)

Definition at line 11085 of file z3py.py.

11085 def LinearOrder(a, index):
11086  return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11087 
11088 

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

11043 def Loop(re, lo, hi=0):
11044  """Create the regular expression accepting between a lower and upper bound repetitions
11045  >>> re = Loop(Re("a"), 1, 3)
11046  >>> print(simplify(InRe("aa", re)))
11047  True
11048  >>> print(simplify(InRe("aaaa", re)))
11049  False
11050  >>> print(simplify(InRe("", re)))
11051  False
11052  """
11053  return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
11054 
11055 

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

4263 def LShR(a, b):
4264  """Create the Z3 expression logical right shift.
4265 
4266  Use the operator >> for the arithmetical right shift.
4267 
4268  >>> x, y = BitVecs('x y', 32)
4269  >>> LShR(x, y)
4270  LShR(x, y)
4271  >>> (x >> y).sexpr()
4272  '(bvashr x y)'
4273  >>> LShR(x, y).sexpr()
4274  '(bvlshr x y)'
4275  >>> BitVecVal(4, 3)
4276  4
4277  >>> BitVecVal(4, 3).as_signed_long()
4278  -4
4279  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4280  -2
4281  >>> simplify(BitVecVal(4, 3) >> 1)
4282  6
4283  >>> simplify(LShR(BitVecVal(4, 3), 1))
4284  2
4285  >>> simplify(BitVecVal(2, 3) >> 1)
4286  1
4287  >>> simplify(LShR(BitVecVal(2, 3), 1))
4288  1
4289  """
4290  _check_bv_args(a, b)
4291  a, b = _coerce_exprs(a, b)
4292  return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4293 
4294 

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

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

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

4759 def Map(f, *args):
4760  """Return a Z3 map array expression.
4761 
4762  >>> f = Function('f', IntSort(), IntSort(), IntSort())
4763  >>> a1 = Array('a1', IntSort(), IntSort())
4764  >>> a2 = Array('a2', IntSort(), IntSort())
4765  >>> b = Map(f, a1, a2)
4766  >>> b
4767  Map(f, a1, a2)
4768  >>> prove(b[0] == f(a1[0], a2[0]))
4769  proved
4770  """
4771  args = _get_args(args)
4772  if z3_debug():
4773  _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
4774  _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
4775  _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
4776  _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
4777  _args, sz = _to_ast_array(args)
4778  ctx = f.ctx
4779  return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
4780 
4781 

Referenced by Context.Context().

◆ mk_not()

def z3py.mk_not (   a)

Definition at line 1800 of file z3py.py.

1800 def mk_not(a):
1801  if is_not(a):
1802  return a.arg(0)
1803  else:
1804  return Not(a)
1805 
1806 

◆ Model()

def z3py.Model (   ctx = None)

Definition at line 6590 of file z3py.py.

6590 def Model(ctx=None):
6591  ctx = _get_ctx(ctx)
6592  return ModelRef(Z3_mk_model(ctx.ref()), ctx)
6593 
6594 

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

1917 def MultiPattern(*args):
1918  """Create a Z3 multi-pattern using the given expressions `*args`
1919 
1920  >>> f = Function('f', IntSort(), IntSort())
1921  >>> g = Function('g', IntSort(), IntSort())
1922  >>> x = Int('x')
1923  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1924  >>> q
1925  ForAll(x, f(x) != g(x))
1926  >>> q.num_patterns()
1927  1
1928  >>> is_pattern(q.pattern(0))
1929  True
1930  >>> q.pattern(0)
1931  MultiPattern(f(Var(0)), g(Var(0)))
1932  """
1933  if z3_debug():
1934  _z3_assert(len(args) > 0, "At least one argument expected")
1935  _z3_assert(all([is_expr(a) for a in args]), "Z3 expressions expected")
1936  ctx = args[0].ctx
1937  args, sz = _to_ast_array(args)
1938  return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
1939 
1940 

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

1781 def Not(a, ctx=None):
1782  """Create a Z3 not expression or probe.
1783 
1784  >>> p = Bool('p')
1785  >>> Not(Not(p))
1786  Not(Not(p))
1787  >>> simplify(Not(Not(p)))
1788  p
1789  """
1790  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1791  if is_probe(a):
1792  # Not is also used to build probes
1793  return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1794  else:
1795  s = BoolSort(ctx)
1796  a = s.cast(a)
1797  return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
1798 
1799 

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

119 def open_log(fname):
120  """Log interaction to a file. This function must be invoked immediately after init(). """
121  Z3_open_log(fname)
122 
123 

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

11012 def Option(re):
11013  """Create the regular expression that optionally accepts the argument.
11014  >>> re = Option(Re("a"))
11015  >>> print(simplify(InRe("a", re)))
11016  True
11017  >>> print(simplify(InRe("", re)))
11018  True
11019  >>> print(simplify(InRe("aa", re)))
11020  False
11021  """
11022  return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
11023 
11024 

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

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

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

8215 def OrElse(*ts, **ks):
8216  """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
8217 
8218  >>> x = Int('x')
8219  >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
8220  >>> # Tactic split-clause fails if there is no clause in the given goal.
8221  >>> t(x == 0)
8222  [[x == 0]]
8223  >>> t(Or(x == 0, x == 1))
8224  [[x == 0], [x == 1]]
8225  """
8226  if z3_debug():
8227  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8228  ctx = ks.get("ctx", None)
8229  num = len(ts)
8230  r = ts[0]
8231  for i in range(num - 1):
8232  r = _or_else(r, ts[i + 1], ctx)
8233  return r
8234 
8235 

◆ ParAndThen()

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

Definition at line 8271 of file z3py.py.

8271 def ParAndThen(t1, t2, ctx=None):
8272  """Alias for ParThen(t1, t2, ctx)."""
8273  return ParThen(t1, t2, ctx)
8274 
8275 

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

8236 def ParOr(*ts, **ks):
8237  """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
8238 
8239  >>> x = Int('x')
8240  >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
8241  >>> t(x + 1 == 2)
8242  [[x == 1]]
8243  """
8244  if z3_debug():
8245  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8246  ctx = _get_ctx(ks.get("ctx", None))
8247  ts = [_to_tactic(t, ctx) for t in ts]
8248  sz = len(ts)
8249  _args = (TacticObj * sz)()
8250  for i in range(sz):
8251  _args[i] = ts[i].tactic
8252  return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
8253 
8254 

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

9103 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
9104  """Parse a file in SMT 2.0 format using the given sorts and decls.
9105 
9106  This function is similar to parse_smt2_string().
9107  """
9108  ctx = _get_ctx(ctx)
9109  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9110  dsz, dnames, ddecls = _dict2darray(decls, ctx)
9111  return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9112 
9113 

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

9082 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
9083  """Parse a string in SMT 2.0 format using the given sorts and decls.
9084 
9085  The arguments sorts and decls are Python dictionaries used to initialize
9086  the symbol table used for the SMT 2.0 parser.
9087 
9088  >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
9089  [x > 0, x < 10]
9090  >>> x, y = Ints('x y')
9091  >>> f = Function('f', IntSort(), IntSort())
9092  >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
9093  [x + f(y) > 0]
9094  >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
9095  [a > 0]
9096  """
9097  ctx = _get_ctx(ctx)
9098  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9099  dsz, dnames, ddecls = _dict2darray(decls, ctx)
9100  return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9101 
9102 

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

8255 def ParThen(t1, t2, ctx=None):
8256  """Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
8257  The subgoals are processed in parallel.
8258 
8259  >>> x, y = Ints('x y')
8260  >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
8261  >>> t(And(Or(x == 1, x == 2), y == x + 1))
8262  [[x == 1, y == 2], [x == 2, y == 3]]
8263  """
8264  t1 = _to_tactic(t1, ctx)
8265  t2 = _to_tactic(t2, ctx)
8266  if z3_debug():
8267  _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
8268  return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
8269 
8270 

Referenced by ParAndThen().

◆ PartialOrder()

def z3py.PartialOrder (   a,
  index 
)

Definition at line 11081 of file z3py.py.

11081 def PartialOrder(a, index):
11082  return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx)
11083 
11084 

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

8878 def PbEq(args, k, ctx=None):
8879  """Create a Pseudo-Boolean inequality k constraint.
8880 
8881  >>> a, b, c = Bools('a b c')
8882  >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
8883  """
8884  _z3_check_cint_overflow(k, "k")
8885  ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8886  return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
8887 
8888 

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

8867 def PbGe(args, k):
8868  """Create a Pseudo-Boolean inequality k constraint.
8869 
8870  >>> a, b, c = Bools('a b c')
8871  >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
8872  """
8873  _z3_check_cint_overflow(k, "k")
8874  ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8875  return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
8876 
8877 

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

8856 def PbLe(args, k):
8857  """Create a Pseudo-Boolean inequality k constraint.
8858 
8859  >>> a, b, c = Bools('a b c')
8860  >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
8861  """
8862  _z3_check_cint_overflow(k, "k")
8863  ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8864  return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
8865 
8866 

◆ PiecewiseLinearOrder()

def z3py.PiecewiseLinearOrder (   a,
  index 
)

Definition at line 11093 of file z3py.py.

11093 def PiecewiseLinearOrder(a, index):
11094  return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11095 
11096 

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

10999 def Plus(re):
11000  """Create the regular expression accepting one or more repetitions of argument.
11001  >>> re = Plus(Re("a"))
11002  >>> print(simplify(InRe("aa", re)))
11003  True
11004  >>> print(simplify(InRe("ab", re)))
11005  False
11006  >>> print(simplify(InRe("", re)))
11007  False
11008  """
11009  return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
11010 
11011 

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

10782 def PrefixOf(a, b):
10783  """Check if 'a' is a prefix of 'b'
10784  >>> s1 = PrefixOf("ab", "abc")
10785  >>> simplify(s1)
10786  True
10787  >>> s2 = PrefixOf("bc", "abc")
10788  >>> simplify(s2)
10789  False
10790  """
10791  ctx = _get_ctx2(a, b)
10792  a = _coerce_seq(a, ctx)
10793  b = _coerce_seq(b, ctx)
10794  return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10795 
10796 

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

8551 def probe_description(name, ctx=None):
8552  """Return a short description for the probe named `name`.
8553 
8554  >>> d = probe_description('memory')
8555  """
8556  ctx = _get_ctx(ctx)
8557  return Z3_probe_get_descr(ctx.ref(), name)
8558 
8559 

Referenced by describe_probes().

◆ probes()

def z3py.probes (   ctx = None)
Return a list of all available probes in Z3.

>>> l = probes()
>>> l.count('memory') == 1
True

Definition at line 8540 of file z3py.py.

8540 def probes(ctx=None):
8541  """Return a list of all available probes in Z3.
8542 
8543  >>> l = probes()
8544  >>> l.count('memory') == 1
8545  True
8546  """
8547  ctx = _get_ctx(ctx)
8548  return [Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref()))]
8549 
8550 

Referenced by describe_probes().

◆ Product()

def z3py.Product ( args)
Create the product of the Z3 expressions.

>>> a, b, c = Ints('a b c')
>>> Product(a, b, c)
a*b*c
>>> Product([a, b, c])
a*b*c
>>> A = IntVector('a', 5)
>>> Product(A)
a__0*a__1*a__2*a__3*a__4

Definition at line 8767 of file z3py.py.

8767 def Product(*args):
8768  """Create the product of the Z3 expressions.
8769 
8770  >>> a, b, c = Ints('a b c')
8771  >>> Product(a, b, c)
8772  a*b*c
8773  >>> Product([a, b, c])
8774  a*b*c
8775  >>> A = IntVector('a', 5)
8776  >>> Product(A)
8777  a__0*a__1*a__2*a__3*a__4
8778  """
8779  args = _get_args(args)
8780  if len(args) == 0:
8781  return 1
8782  ctx = _ctx_from_ast_arg_list(args)
8783  if ctx is None:
8784  return _reduce(lambda a, b: a * b, args, 1)
8785  args = _coerce_expr_list(args, ctx)
8786  if is_bv(args[0]):
8787  return _reduce(lambda a, b: a * b, args, 1)
8788  else:
8789  _args, sz = _to_ast_array(args)
8790  return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
8791 
8792 

◆ prove()

def z3py.prove (   claim,
  show = False,
**  keywords 
)
Try to prove the given claim.

This is a simple function for creating demonstrations.  It tries to prove
`claim` by showing the negation is unsatisfiable.

>>> p, q = Bools('p q')
>>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
proved

Definition at line 8950 of file z3py.py.

8950 def prove(claim, show=False, **keywords):
8951  """Try to prove the given claim.
8952 
8953  This is a simple function for creating demonstrations. It tries to prove
8954  `claim` by showing the negation is unsatisfiable.
8955 
8956  >>> p, q = Bools('p q')
8957  >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
8958  proved
8959  """
8960  if z3_debug():
8961  _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
8962  s = Solver()
8963  s.set(**keywords)
8964  s.add(Not(claim))
8965  if show:
8966  print(s)
8967  r = s.check()
8968  if r == unsat:
8969  print("proved")
8970  elif r == unknown:
8971  print("failed to prove")
8972  print(s.model())
8973  else:
8974  print("counterexample")
8975  print(s.model())
8976 
8977 

◆ Q()

def z3py.Q (   a,
  b,
  ctx = None 
)
Return a Z3 rational a/b.

If `ctx=None`, then the global context is used.

>>> Q(3,5)
3/5
>>> Q(3,5).sort()
Real

Definition at line 3199 of file z3py.py.

3199 def Q(a, b, ctx=None):
3200  """Return a Z3 rational a/b.
3201 
3202  If `ctx=None`, then the global context is used.
3203 
3204  >>> Q(3,5)
3205  3/5
3206  >>> Q(3,5).sort()
3207  Real
3208  """
3209  return simplify(RatVal(a, b, ctx=ctx))
3210 
3211 

◆ Range()

def z3py.Range (   lo,
  hi,
  ctx = None 
)
Create the range regular expression over two sequences of length 1
>>> range = Range("a","z")
>>> print(simplify(InRe("b", range)))
True
>>> print(simplify(InRe("bb", range)))
False

Definition at line 11056 of file z3py.py.

11056 def Range(lo, hi, ctx=None):
11057  """Create the range regular expression over two sequences of length 1
11058  >>> range = Range("a","z")
11059  >>> print(simplify(InRe("b", range)))
11060  True
11061  >>> print(simplify(InRe("bb", range)))
11062  False
11063  """
11064  lo = _coerce_seq(lo, ctx)
11065  hi = _coerce_seq(hi, ctx)
11066  return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
11067 

◆ RatVal()

def z3py.RatVal (   a,
  b,
  ctx = None 
)
Return a Z3 rational a/b.

If `ctx=None`, then the global context is used.

>>> RatVal(3,5)
3/5
>>> RatVal(3,5).sort()
Real

Definition at line 3183 of file z3py.py.

3183 def RatVal(a, b, ctx=None):
3184  """Return a Z3 rational a/b.
3185 
3186  If `ctx=None`, then the global context is used.
3187 
3188  >>> RatVal(3,5)
3189  3/5
3190  >>> RatVal(3,5).sort()
3191  Real
3192  """
3193  if z3_debug():
3194  _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
3195  _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
3196  return simplify(RealVal(a, ctx) / RealVal(b, ctx))
3197 
3198