Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

class  AlgebraicNumRef
 
class  ApplyResult
 
class  ArithRef
 
class  ArithSortRef
 Arithmetic. More...
 
class  ArrayRef
 
class  ArraySortRef
 Arrays. More...
 
class  AstMap
 
class  AstRef
 
class  AstVector
 
class  BitVecNumRef
 
class  BitVecRef
 
class  BitVecSortRef
 Bit-Vectors. More...
 
class  BoolRef
 
class  BoolSortRef
 Booleans. More...
 
class  CheckSatResult
 
class  Context
 
class  Datatype
 
class  DatatypeRef
 
class  DatatypeSortRef
 
class  ExprRef
 Expressions. More...
 
class  FiniteDomainNumRef
 
class  FiniteDomainRef
 
class  FiniteDomainSortRef
 
class  Fixedpoint
 Fixedpoint. More...
 
class  FPNumRef
 
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 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 PartialOrder (a, index)
 
def LinearOrder (a, index)
 
def TreeOrder (a, index)
 
def PiecewiseLinearOrder (a, index)
 
def TransitiveClosure (f)
 
def ensure_prop_closures ()
 
def user_prop_push (ctx)
 
def user_prop_pop (ctx, num_scopes)
 
def user_prop_fresh (id, ctx)
 
def user_prop_fixed (ctx, cb, id, value)
 
def user_prop_final (ctx, cb)
 
def user_prop_eq (ctx, cb, x, y)
 
def user_prop_diseq (ctx, cb, x, y)
 

Variables

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

Function Documentation

◆ And()

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

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

Definition at line 1813 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Goal.as_expr(), Bool(), Bools(), BoolVector(), Lambda(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().

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

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

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

8171 def AndThen(*ts, **ks):
8172  """Return a tactic that applies the tactics in `*ts` in sequence.
8173 
8174  >>> x, y = Ints('x y')
8175  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
8176  >>> t(And(x == 0, y > x + 1))
8177  [[Not(y <= 1)]]
8178  >>> t(And(x == 0, y > x + 1)).as_expr()
8179  Not(y <= 1)
8180  """
8181  if z3_debug():
8182  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8183  ctx = ks.get("ctx", None)
8184  num = len(ts)
8185  r = ts[0]
8186  for i in range(num - 1):
8187  r = _and_then(r, ts[i + 1], ctx)
8188  return r
8189 
8190 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def AndThen(ts, ks)
Definition: z3py.py:8171
def z3_debug()
Definition: z3py.py:64

◆ 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 
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
def append_log(s)
Definition: z3py.py:124

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

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

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

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

Referenced by ArrayRef.__getitem__(), ArraySort(), ArrayRef.domain(), get_map_func(), is_array(), is_const_array(), is_K(), is_map(), is_select(), is_store(), K(), Lambda(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), Store(), and Update().

4678 def Array(name, dom, rng):
4679  """Return an array constant named `name` with the given domain and range sorts.
4680 
4681  >>> a = Array('a', IntSort(), IntSort())
4682  >>> a.sort()
4683  Array(Int, Int)
4684  >>> a[0]
4685  a[0]
4686  """
4687  s = ArraySort(dom, rng)
4688  ctx = s.ctx
4689  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4690 
4691 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def ArraySort(sig)
Definition: z3py.py:4645
def to_symbol(s, ctx=None)
Definition: z3py.py:129
def Array(name, dom, rng)
Definition: z3py.py:4678

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

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

4645 def ArraySort(*sig):
4646  """Return the Z3 array sort with the given domain and range sorts.
4647 
4648  >>> A = ArraySort(IntSort(), BoolSort())
4649  >>> A
4650  Array(Int, Bool)
4651  >>> A.domain()
4652  Int
4653  >>> A.range()
4654  Bool
4655  >>> AA = ArraySort(IntSort(), A)
4656  >>> AA
4657  Array(Int, Array(Int, Bool))
4658  """
4659  sig = _get_args(sig)
4660  if z3_debug():
4661  _z3_assert(len(sig) > 1, "At least two arguments expected")
4662  arity = len(sig) - 1
4663  r = sig[arity]
4664  d = sig[0]
4665  if z3_debug():
4666  for s in sig:
4667  _z3_assert(is_sort(s), "Z3 sort expected")
4668  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4669  ctx = d.ctx
4670  if len(sig) == 2:
4671  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4672  dom = (Sort * arity)()
4673  for i in range(arity):
4674  dom[i] = sig[i].ast
4675  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4676 
4677 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def ArraySort(sig)
Definition: z3py.py:4645
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
def is_sort(s)
Definition: z3py.py:646
def z3_debug()
Definition: z3py.py:64

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

8800 def AtLeast(*args):
8801  """Create an at-most Pseudo-Boolean k constraint.
8802 
8803  >>> a, b, c = Bools('a b c')
8804  >>> f = AtLeast(a, b, c, 2)
8805  """
8806  args = _get_args(args)
8807  if z3_debug():
8808  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8809  ctx = _ctx_from_ast_arg_list(args)
8810  if z3_debug():
8811  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8812  args1 = _coerce_expr_list(args[:-1], ctx)
8813  k = args[-1]
8814  _args, sz = _to_ast_array(args1)
8815  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8816 
8817 
def AtLeast(args)
Definition: z3py.py:8800
def z3_debug()
Definition: z3py.py:64
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ AtMost()

def z3py.AtMost (   args)
Create an at-most Pseudo-Boolean k constraint.

>>> a, b, c = Bools('a b c')
>>> f = AtMost(a, b, c, 2)

Definition at line 8782 of file z3py.py.

8782 def AtMost(*args):
8783  """Create an at-most Pseudo-Boolean k constraint.
8784 
8785  >>> a, b, c = Bools('a b c')
8786  >>> f = AtMost(a, b, c, 2)
8787  """
8788  args = _get_args(args)
8789  if z3_debug():
8790  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8791  ctx = _ctx_from_ast_arg_list(args)
8792  if z3_debug():
8793  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8794  args1 = _coerce_expr_list(args[:-1], ctx)
8795  k = args[-1]
8796  _args, sz = _to_ast_array(args1)
8797  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8798 
8799 
def AtMost(args)
Definition: z3py.py:8782
def z3_debug()
Definition: z3py.py:64
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ BitVec()

def z3py.BitVec (   name,
  bv,
  ctx = None 
)
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
If `ctx=None`, then the global context is used.

>>> x  = BitVec('x', 16)
>>> is_bv(x)
True
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> word = BitVecSort(16)
>>> x2 = BitVec('x', word)
>>> eq(x, x2)
True

Definition at line 3999 of file z3py.py.

Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__invert__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__neg__(), BitVecRef.__or__(), BitVecRef.__pos__(), BitVecRef.__radd__(), BitVecRef.__rand__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), BitVecRef.__rrshift__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BitVecs(), BitVecSort(), BV2Int(), Extract(), is_bv(), is_bv_value(), RepeatBitVec(), SignExt(), BitVecRef.size(), BitVecRef.sort(), SRem(), UDiv(), URem(), and ZeroExt().

3999 def BitVec(name, bv, ctx=None):
4000  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4001  If `ctx=None`, then the global context is used.
4002 
4003  >>> x = BitVec('x', 16)
4004  >>> is_bv(x)
4005  True
4006  >>> x.size()
4007  16
4008  >>> x.sort()
4009  BitVec(16)
4010  >>> word = BitVecSort(16)
4011  >>> x2 = BitVec('x', word)
4012  >>> eq(x, x2)
4013  True
4014  """
4015  if isinstance(bv, BitVecSortRef):
4016  ctx = bv.ctx
4017  else:
4018  ctx = _get_ctx(ctx)
4019  bv = BitVecSort(bv, ctx)
4020  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
4021 
4022 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:129
def BitVec(name, bv, ctx=None)
Definition: z3py.py:3999
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967

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

Referenced by BitVecRef.__ge__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__rshift__(), LShR(), RotateLeft(), RotateRight(), UGE(), UGT(), ULE(), and ULT().

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

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

Referenced by BitVec(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), BitVecRef.sort(), Sort.translate(), and Sort.Translate().

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

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

Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), Concat(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().

3982 def BitVecVal(val, bv, ctx=None):
3983  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3984 
3985  >>> v = BitVecVal(10, 32)
3986  >>> v
3987  10
3988  >>> print("0x%.8x" % v.as_long())
3989  0x0000000a
3990  """
3991  if is_bv_sort(bv):
3992  ctx = bv.ctx
3993  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3994  else:
3995  ctx = _get_ctx(ctx)
3996  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3997 
3998 
def BitVecVal(val, bv, ctx=None)
Definition: z3py.py:3982
def is_bv_sort(s)
Definition: z3py.py:3438
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ Bool()

def z3py.Bool (   name,
  ctx = None 
)
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.

>>> p = Bool('p')
>>> q = Bool('q')
>>> And(p, q)
And(p, q)

Definition at line 1692 of file z3py.py.

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

1692 def Bool(name, ctx=None):
1693  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1694 
1695  >>> p = Bool('p')
1696  >>> q = Bool('q')
1697  >>> And(p, q)
1698  And(p, q)
1699  """
1700  ctx = _get_ctx(ctx)
1701  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1702 
1703 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:129
def Bool(name, ctx=None)
Definition: z3py.py:1692
def BoolSort(ctx=None)
Definition: z3py.py:1655

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

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

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

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

Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), ArraySortRef.domain(), ArrayRef.domain(), Context.getBoolSort(), If(), IntSort(), is_arith_sort(), Context.mkBoolSort(), Context.MkBoolSort(), ArraySortRef.range(), ArrayRef.range(), ArrayRef.sort(), Sort.translate(), and Sort.Translate().

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

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

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

1673 def BoolVal(val, ctx=None):
1674  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1675 
1676  >>> BoolVal(True)
1677  True
1678  >>> is_true(BoolVal(True))
1679  True
1680  >>> is_true(True)
1681  False
1682  >>> is_false(BoolVal(False))
1683  True
1684  """
1685  ctx = _get_ctx(ctx)
1686  if val:
1687  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1688  else:
1689  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1690 
1691 
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
def BoolVal(val, ctx=None)
Definition: z3py.py:1673

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

Referenced by And(), and Or().

1720 def BoolVector(prefix, sz, ctx=None):
1721  """Return a list of Boolean constants of size `sz`.
1722 
1723  The constants are named using the given prefix.
1724  If `ctx=None`, then the global context is used.
1725 
1726  >>> P = BoolVector('p', 3)
1727  >>> P
1728  [p__0, p__1, p__2]
1729  >>> And(P)
1730  And(p__0, p__1, p__2)
1731  """
1732  return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]
1733 
1734 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def BoolVector(prefix, sz, ctx=None)
Definition: z3py.py:1720
def Bool(name, ctx=None)
Definition: z3py.py:1692

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

3935 def BV2Int(a, is_signed=False):
3936  """Return the Z3 expression BV2Int(a).
3937 
3938  >>> b = BitVec('b', 3)
3939  >>> BV2Int(b).sort()
3940  Int
3941  >>> x = Int('x')
3942  >>> x > BV2Int(b)
3943  x > BV2Int(b)
3944  >>> x > BV2Int(b, is_signed=False)
3945  x > BV2Int(b)
3946  >>> x > BV2Int(b, is_signed=True)
3947  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3948  >>> solve(x > BV2Int(b), b == 1, x < 3)
3949  [x = 2, b = 1]
3950  """
3951  if z3_debug():
3952  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
3953  ctx = a.ctx
3954  # investigate problem with bv2int
3955  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3956 
3957 
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
def z3_debug()
Definition: z3py.py:64
def BV2Int(a, is_signed=False)
Definition: z3py.py:3935
def is_bv(a)
Definition: z3py.py:3906

◆ BVAddNoOverflow()

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

Definition at line 4421 of file z3py.py.

4421 def BVAddNoOverflow(a, b, signed):
4422  """A predicate the determines that bit-vector addition does not overflow"""
4423  _check_bv_args(a, b)
4424  a, b = _coerce_exprs(a, b)
4425  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4426 
4427 
def BVAddNoOverflow(a, b, signed)
Definition: z3py.py:4421
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

◆ BVAddNoUnderflow()

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

Definition at line 4428 of file z3py.py.

4428 def BVAddNoUnderflow(a, b):
4429  """A predicate the determines that signed bit-vector addition does not underflow"""
4430  _check_bv_args(a, b)
4431  a, b = _coerce_exprs(a, b)
4432  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4433 
4434 
def BVAddNoUnderflow(a, b)
Definition: z3py.py:4428
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow...

◆ BVMulNoOverflow()

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

Definition at line 4463 of file z3py.py.

4463 def BVMulNoOverflow(a, b, signed):
4464  """A predicate the determines that bit-vector multiplication does not overflow"""
4465  _check_bv_args(a, b)
4466  a, b = _coerce_exprs(a, b)
4467  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4468 
4469 
def BVMulNoOverflow(a, b, signed)
Definition: z3py.py:4463
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow...

◆ BVMulNoUnderflow()

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

Definition at line 4470 of file z3py.py.

4470 def BVMulNoUnderflow(a, b):
4471  """A predicate the determines that bit-vector signed multiplication does not underflow"""
4472  _check_bv_args(a, b)
4473  a, b = _coerce_exprs(a, b)
4474  return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4475 
4476 
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
def BVMulNoUnderflow(a, b)
Definition: z3py.py:4470

◆ BVRedAnd()

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

Definition at line 4407 of file z3py.py.

4407 def BVRedAnd(a):
4408  """Return the reduction-and expression of `a`."""
4409  if z3_debug():
4410  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4411  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4412 
4413 
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
def BVRedAnd(a)
Definition: z3py.py:4407
def z3_debug()
Definition: z3py.py:64
def is_bv(a)
Definition: z3py.py:3906

◆ BVRedOr()

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

Definition at line 4414 of file z3py.py.

4414 def BVRedOr(a):
4415  """Return the reduction-or expression of `a`."""
4416  if z3_debug():
4417  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4418  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4419 
4420 
def BVRedOr(a)
Definition: z3py.py:4414
def z3_debug()
Definition: z3py.py:64
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
def is_bv(a)
Definition: z3py.py:3906

◆ BVSDivNoOverflow()

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

Definition at line 4449 of file z3py.py.

4449 def BVSDivNoOverflow(a, b):
4450  """A predicate the determines that bit-vector signed division does not overflow"""
4451  _check_bv_args(a, b)
4452  a, b = _coerce_exprs(a, b)
4453  return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4454 
4455 
def BVSDivNoOverflow(a, b)
Definition: z3py.py:4449
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow...

◆ BVSNegNoOverflow()

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

Definition at line 4456 of file z3py.py.

4456 def BVSNegNoOverflow(a):
4457  """A predicate the determines that bit-vector unary negation does not overflow"""
4458  if z3_debug():
4459  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4460  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4461 
4462 
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector...
def z3_debug()
Definition: z3py.py:64
def BVSNegNoOverflow(a)
Definition: z3py.py:4456
def is_bv(a)
Definition: z3py.py:3906

◆ BVSubNoOverflow()

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

Definition at line 4435 of file z3py.py.

4435 def BVSubNoOverflow(a, b):
4436  """A predicate the determines that bit-vector subtraction does not overflow"""
4437  _check_bv_args(a, b)
4438  a, b = _coerce_exprs(a, b)
4439  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4440 
4441 
def BVSubNoOverflow(a, b)
Definition: z3py.py:4435
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow...

◆ BVSubNoUnderflow()

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

Definition at line 4442 of file z3py.py.

4442 def BVSubNoUnderflow(a, b, signed):
4443  """A predicate the determines that bit-vector subtraction does not underflow"""
4444  _check_bv_args(a, b)
4445  a, b = _coerce_exprs(a, b)
4446  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4447 
4448 
def BVSubNoUnderflow(a, b, signed)
Definition: z3py.py:4442
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow...

◆ Cbrt()

def z3py.Cbrt (   a,
  ctx = None 
)
Return a Z3 expression which represents the cubic root of a.

>>> x = Real('x')
>>> Cbrt(x)
x**(1/3)

Definition at line 3386 of file z3py.py.

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

◆ Complement()

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

Definition at line 11002 of file z3py.py.

11002 def Complement(re):
11003  """Create the complement regular expression."""
11004  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
11005 
11006 
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
def Complement(re)
Definition: z3py.py:11002

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

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

4044 def Concat(*args):
4045  """Create a Z3 bit-vector concatenation expression.
4046 
4047  >>> v = BitVecVal(1, 4)
4048  >>> Concat(v, v+1, v)
4049  Concat(Concat(1, 1 + 1), 1)
4050  >>> simplify(Concat(v, v+1, v))
4051  289
4052  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
4053  121
4054  """
4055  args = _get_args(args)
4056  sz = len(args)
4057  if z3_debug():
4058  _z3_assert(sz >= 2, "At least two arguments expected.")
4059 
4060  ctx = None
4061  for a in args:
4062  if is_expr(a):
4063  ctx = a.ctx
4064  break
4065  if is_seq(args[0]) or isinstance(args[0], str):
4066  args = [_coerce_seq(s, ctx) for s in args]
4067  if z3_debug():
4068  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
4069  v = (Ast * sz)()
4070  for i in range(sz):
4071  v[i] = args[i].as_ast()
4072  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
4073 
4074  if is_re(args[0]):
4075  if z3_debug():
4076  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
4077  v = (Ast * sz)()
4078  for i in range(sz):
4079  v[i] = args[i].as_ast()
4080  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
4081 
4082  if z3_debug():
4083  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
4084  r = args[0]
4085  for i in range(sz - 1):
4086  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
4087  return r
4088 
4089 
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
def is_re(s)
Definition: z3py.py:10920
def z3_debug()
Definition: z3py.py:64
def is_expr(a)
Definition: z3py.py:1210
def is_bv(a)
Definition: z3py.py:3906
def Concat(args)
Definition: z3py.py:4044
def is_seq(a)
Definition: z3py.py:10658

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

Referenced by If().

8628 def Cond(p, t1, t2, ctx=None):
8629  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8630 
8631  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8632  """
8633  p = _to_probe(p, ctx)
8634  t1 = _to_tactic(t1, ctx)
8635  t2 = _to_tactic(t2, ctx)
8636  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8637 
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8628
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...

◆ Const()

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

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

Definition at line 1405 of file z3py.py.

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

1405 def Const(name, sort):
1406  """Create a constant of the given sort.
1407 
1408  >>> Const('x', IntSort())
1409  x
1410  """
1411  if z3_debug():
1412  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1413  ctx = sort.ctx
1414  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1415 
1416 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:129
def Const(name, sort)
Definition: z3py.py:1405
def z3_debug()
Definition: z3py.py:64

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

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

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

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

10789 def Contains(a, b):
10790  """Check if 'a' contains 'b'
10791  >>> s1 = Contains("abc", "ab")
10792  >>> simplify(s1)
10793  True
10794  >>> s2 = Contains("abc", "bc")
10795  >>> simplify(s2)
10796  True
10797  >>> x, y, z = Strings('x y z')
10798  >>> s3 = Contains(Concat(x,y,z), y)
10799  >>> simplify(s3)
10800  True
10801  """
10802  ctx = _get_ctx2(a, b)
10803  a = _coerce_seq(a, ctx)
10804  b = _coerce_seq(b, ctx)
10805  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10806 
10807 
def Contains(a, b)
Definition: z3py.py:10789
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.

◆ CreateDatatypes()

def z3py.CreateDatatypes (   ds)
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.

In the following example we define a Tree-List using two mutually recursive datatypes.

>>> TreeList = Datatype('TreeList')
>>> Tree     = Datatype('Tree')
>>> # Tree has two constructors: leaf and node
>>> Tree.declare('leaf', ('val', IntSort()))
>>> # a node contains a list of trees
>>> Tree.declare('node', ('children', TreeList))
>>> TreeList.declare('nil')
>>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
>>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
>>> Tree.val(Tree.leaf(10))
val(leaf(10))
>>> simplify(Tree.val(Tree.leaf(10)))
10
>>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
>>> n1
node(cons(leaf(10), cons(leaf(20), nil)))
>>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
>>> simplify(n2 == n1)
False
>>> simplify(TreeList.car(Tree.children(n2)) == n1)
True

Definition at line 5092 of file z3py.py.

Referenced by Datatype.create().

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

◆ DeclareSort()

def z3py.DeclareSort (   name,
  ctx = None 
)
Create a new uninterpreted sort named `name`.

If `ctx=None`, then the new sort is declared in the global Z3Py context.

>>> A = DeclareSort('A')
>>> a = Const('a', A)
>>> b = Const('b', A)
>>> a.sort() == A
True
>>> b.sort() == A
True
>>> a == b
a == b

Definition at line 690 of file z3py.py.

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

690 def DeclareSort(name, ctx=None):
691  """Create a new uninterpreted sort named `name`.
692 
693  If `ctx=None`, then the new sort is declared in the global Z3Py context.
694 
695  >>> A = DeclareSort('A')
696  >>> a = Const('a', A)
697  >>> b = Const('b', A)
698  >>> a.sort() == A
699  True
700  >>> b.sort() == A
701  True
702  >>> a == b
703  a == b
704  """
705  ctx = _get_ctx(ctx)
706  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
707 
def to_symbol(s, ctx=None)
Definition: z3py.py:129
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
def DeclareSort(name, ctx=None)
Definition: z3py.py:690

◆ Default()

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

Definition at line 4714 of file z3py.py.

Referenced by is_default().

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

◆ describe_probes()

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

Definition at line 8549 of file z3py.py.

8549 def describe_probes():
8550  """Display a (tabular) description of all available probes in Z3."""
8551  if in_html_mode():
8552  even = True
8553  print('<table border="1" cellpadding="2" cellspacing="0">')
8554  for p in probes():
8555  if even:
8556  print('<tr style="background-color:#CFCFCF">')
8557  even = False
8558  else:
8559  print("<tr>")
8560  even = True
8561  print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
8562  print("</table>")
8563  else:
8564  for p in probes():
8565  print("%s : %s" % (p, probe_description(p)))
8566 
8567 
def probes(ctx=None)
Definition: z3py.py:8529
def probe_description(name, ctx=None)
Definition: z3py.py:8540
def describe_probes()
Definition: z3py.py:8549

◆ describe_tactics()

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

Definition at line 8343 of file z3py.py.

8343 def describe_tactics():
8344  """Display a (tabular) description of all available tactics in Z3."""
8345  if in_html_mode():
8346  even = True
8347  print('<table border="1" cellpadding="2" cellspacing="0">')
8348  for t in tactics():
8349  if even:
8350  print('<tr style="background-color:#CFCFCF">')
8351  even = False
8352  else:
8353  print("<tr>")
8354  even = True
8355  print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
8356  print("</table>")
8357  else:
8358  for t in tactics():
8359  print("%s : %s" % (t, tactic_description(t)))
8360 
8361 
def tactics(ctx=None)
Definition: z3py.py:8323
def tactic_description(name, ctx=None)
Definition: z3py.py:8334
def describe_tactics()
Definition: z3py.py:8343

◆ 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 
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def disable_trace(msg)
Definition: z3py.py:81

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

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

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

1372 def Distinct(*args):
1373  """Create a Z3 distinct expression.
1374 
1375  >>> x = Int('x')
1376  >>> y = Int('y')
1377  >>> Distinct(x, y)
1378  x != y
1379  >>> z = Int('z')
1380  >>> Distinct(x, y, z)
1381  Distinct(x, y, z)
1382  >>> simplify(Distinct(x, y, z))
1383  Distinct(x, y, z)
1384  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1385  And(Not(x == y), Not(x == z), Not(y == z))
1386  """
1387  args = _get_args(args)
1388  ctx = _ctx_from_ast_arg_list(args)
1389  if z3_debug():
1390  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
1391  args = _coerce_expr_list(args, ctx)
1392  _args, sz = _to_ast_array(args)
1393  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1394 
1395 
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
def z3_debug()
Definition: z3py.py:64
def Distinct(args)
Definition: z3py.py:1372

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

10720 def Empty(s):
10721  """Create the empty sequence of the given sort
10722  >>> e = Empty(StringSort())
10723  >>> e2 = StringVal("")
10724  >>> print(e.eq(e2))
10725  True
10726  >>> e3 = Empty(SeqSort(IntSort()))
10727  >>> print(e3)
10728  Empty(Seq(Int))
10729  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10730  >>> print(e4)
10731  Empty(ReSort(Seq(Int)))
10732  """
10733  if isinstance(s, SeqSortRef):
10734  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10735  if isinstance(s, ReSortRef):
10736  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10737  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10738 
10739 
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
def Empty(s)
Definition: z3py.py:10720

◆ EmptySet()

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

Definition at line 4856 of file z3py.py.

4856 def EmptySet(s):
4857  """Create the empty set
4858  >>> EmptySet(IntSort())
4859  K(Int, False)
4860  """
4861  ctx = s.ctx
4862  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4863 
4864 
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
def EmptySet(s)
Definition: z3py.py:4856

◆ 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 
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def enable_trace(msg)
Definition: z3py.py:77

◆ ensure_prop_closures()

def z3py.ensure_prop_closures ( )

Definition at line 11110 of file z3py.py.

11110 def ensure_prop_closures():
11111  global _prop_closures
11112  if _prop_closures is None:
11113  _prop_closures = PropClosures()
11114 
11115 
def ensure_prop_closures()
Definition: z3py.py:11110

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

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

5317 def EnumSort(name, values, ctx=None):
5318  """Return a new enumeration sort named `name` containing the given values.
5319 
5320  The result is a pair (sort, list of constants).
5321  Example:
5322  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5323  """
5324  if z3_debug():
5325  _z3_assert(isinstance(name, str), "Name must be a string")
5326  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
5327  _z3_assert(len(values) > 0, "At least one value expected")
5328  ctx = _get_ctx(ctx)
5329  num = len(values)
5330  _val_names = (Symbol * num)()
5331  for i in range(num):
5332  _val_names[i] = to_symbol(values[i])
5333  _values = (FuncDecl * num)()
5334  _testers = (FuncDecl * num)()
5335  name = to_symbol(name)
5336  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5337  V = []
5338  for i in range(num):
5339  V.append(FuncDeclRef(_values[i], ctx))
5340  V = [a() for a in V]
5341  return S, V
5342 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def to_symbol(s, ctx=None)
Definition: z3py.py:129
def z3_debug()
Definition: z3py.py:64
def EnumSort(name, values, ctx=None)
Definition: z3py.py:5317
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.

◆ eq()

def z3py.eq (   a,
  b 
)
Return `True` if `a` and `b` are structurally identical AST nodes.

>>> x = Int('x')
>>> y = Int('y')
>>> eq(x, y)
False
>>> eq(x + 1, x + 1)
True
>>> eq(x + 1, 1 + x)
False
>>> eq(simplify(x + 1), simplify(1 + x))
True

Definition at line 471 of file z3py.py.

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

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 
def z3_debug()
Definition: z3py.py:64
def is_ast(a)
Definition: z3py.py:450

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

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

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

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

4802 def Ext(a, b):
4803  """Return extensionality index for one-dimensional arrays.
4804  >> a, b = Consts('a b', SetSort(IntSort()))
4805  >> Ext(a, b)
4806  Ext(a, b)
4807  """
4808  ctx = a.ctx
4809  if z3_debug():
4810  _z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays")
4811  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4812 
4813 
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
def is_array_sort(a)
Definition: z3py.py:4552
def is_array(a)
Definition: z3py.py:4556
def z3_debug()
Definition: z3py.py:64
def Ext(a, b)
Definition: z3py.py:4802

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

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

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

8586 def FailIf(p, ctx=None):
8587  """Return a tactic that fails if the probe `p` evaluates to true.
8588  Otherwise, it returns the input goal unmodified.
8589 
8590  In the following example, the tactic applies 'simplify' if and only if there are
8591  more than 2 constraints in the goal.
8592 
8593  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8594  >>> x, y = Ints('x y')
8595  >>> g = Goal()
8596  >>> g.add(x > 0)
8597  >>> g.add(y > 0)
8598  >>> t(g)
8599  [[x > 0, y > 0]]
8600  >>> g.add(x == y + 1)
8601  >>> t(g)
8602  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8603  """
8604  p = _to_probe(p, ctx)
8605  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8606 
8607 
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
def FailIf(p, ctx=None)
Definition: z3py.py:8586

◆ FiniteDomainSort()

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

Definition at line 7590 of file z3py.py.

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

7590 def FiniteDomainSort(name, sz, ctx=None):
7591  """Create a named finite domain sort of a given size sz"""
7592  if not isinstance(name, Symbol):
7593  name = to_symbol(name)
7594  ctx = _get_ctx(ctx)
7595  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7596 
7597 
def to_symbol(s, ctx=None)
Definition: z3py.py:129
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)
Create a named finite domain sort.
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7590

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

7660 def FiniteDomainVal(val, sort, ctx=None):
7661  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7662 
7663  >>> s = FiniteDomainSort('S', 256)
7664  >>> FiniteDomainVal(255, s)
7665  255
7666  >>> FiniteDomainVal('100', s)
7667  100
7668  """
7669  if z3_debug():
7670  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
7671  ctx = sort.ctx
7672  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7673 
7674 
def is_finite_domain_sort(s)
Definition: z3py.py:7598
def FiniteDomainVal(val, sort, ctx=None)
Definition: z3py.py:7660
def z3_debug()
Definition: z3py.py:64
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ Float128()

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

Definition at line 9266 of file z3py.py.

9266 def Float128(ctx=None):
9267  """Floating-point 128-bit (quadruple) sort."""
9268  ctx = _get_ctx(ctx)
9269  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
9270 
9271 
def Float128(ctx=None)
Definition: z3py.py:9266
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.

◆ Float16()

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

Definition at line 9230 of file z3py.py.

9230 def Float16(ctx=None):
9231  """Floating-point 16-bit (half) sort."""
9232  ctx = _get_ctx(ctx)
9233  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
9234 
9235 
def Float16(ctx=None)
Definition: z3py.py:9230
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.

◆ Float32()

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

Definition at line 9242 of file z3py.py.

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

9242 def Float32(ctx=None):
9243  """Floating-point 32-bit (single) sort."""
9244  ctx = _get_ctx(ctx)
9245  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
9246 
9247 
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
def Float32(ctx=None)
Definition: z3py.py:9242

◆ Float64()

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

Definition at line 9254 of file z3py.py.

Referenced by fpFPToFP(), and fpToFP().

9254 def Float64(ctx=None):
9255  """Floating-point 64-bit (double) sort."""
9256  ctx = _get_ctx(ctx)
9257  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
9258 
9259 
def Float64(ctx=None)
Definition: z3py.py:9254
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.

◆ FloatDouble()

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

Definition at line 9260 of file z3py.py.

9260 def FloatDouble(ctx=None):
9261  """Floating-point 64-bit (double) sort."""
9262  ctx = _get_ctx(ctx)
9263  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
9264 
9265 
def FloatDouble(ctx=None)
Definition: z3py.py:9260
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.

◆ FloatHalf()

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

Definition at line 9236 of file z3py.py.

9236 def FloatHalf(ctx=None):
9237  """Floating-point 16-bit (half) sort."""
9238  ctx = _get_ctx(ctx)
9239  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
9240 
9241 
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
def FloatHalf(ctx=None)
Definition: z3py.py:9236

◆ FloatQuadruple()

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

Definition at line 9272 of file z3py.py.

9272 def FloatQuadruple(ctx=None):
9273  """Floating-point 128-bit (quadruple) sort."""
9274  ctx = _get_ctx(ctx)
9275  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
9276 
9277 
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
def FloatQuadruple(ctx=None)
Definition: z3py.py:9272

◆ FloatSingle()

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

Definition at line 9248 of file z3py.py.

9248 def FloatSingle(ctx=None):
9249  """Floating-point 32-bit (single) sort."""
9250  ctx = _get_ctx(ctx)
9251  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
9252 
9253 
def FloatSingle(ctx=None)
Definition: z3py.py:9248
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.

◆ ForAll()

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

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

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

Definition at line 2187 of file z3py.py.

Referenced by Fixedpoint.abstract(), QuantifierRef.body(), QuantifierRef.children(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

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

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

Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__neg__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), fpAdd(), fpDiv(), fpIsInf(), fpIsNaN(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), FPSort(), fpSub(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and FPRef.sort().

9898 def FP(name, fpsort, ctx=None):
9899  """Return a floating-point constant named `name`.
9900  `fpsort` is the floating-point sort.
9901  If `ctx=None`, then the global context is used.
9902 
9903  >>> x = FP('x', FPSort(8, 24))
9904  >>> is_fp(x)
9905  True
9906  >>> x.ebits()
9907  8
9908  >>> x.sort()
9909  FPSort(8, 24)
9910  >>> word = FPSort(8, 24)
9911  >>> x2 = FP('x', word)
9912  >>> eq(x, x2)
9913  True
9914  """
9915  if isinstance(fpsort, FPSortRef) and ctx is None:
9916  ctx = fpsort.ctx
9917  else:
9918  ctx = _get_ctx(ctx)
9919  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
9920 
9921 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:129
def FP(name, fpsort, ctx=None)
Definition: z3py.py:9898

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

9941 def fpAbs(a, ctx=None):
9942  """Create a Z3 floating-point absolute value expression.
9943 
9944  >>> s = FPSort(8, 24)
9945  >>> rm = RNE()
9946  >>> x = FPVal(1.0, s)
9947  >>> fpAbs(x)
9948  fpAbs(1)
9949  >>> y = FPVal(-20.0, s)
9950  >>> y
9951  -1.25*(2**4)
9952  >>> fpAbs(y)
9953  fpAbs(-1.25*(2**4))
9954  >>> fpAbs(-1.25*(2**4))
9955  fpAbs(-1.25*(2**4))
9956  >>> fpAbs(x).sort()
9957  FPSort(8, 24)
9958  """
9959  ctx = _get_ctx(ctx)
9960  [a] = _coerce_fp_expr_list([a], ctx)
9961  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
9962 
9963 
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
def fpAbs(a, ctx=None)
Definition: z3py.py:9941

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

Referenced by FPs().

10032 def fpAdd(rm, a, b, ctx=None):
10033  """Create a Z3 floating-point addition expression.
10034 
10035  >>> s = FPSort(8, 24)
10036  >>> rm = RNE()
10037  >>> x = FP('x', s)
10038  >>> y = FP('y', s)
10039  >>> fpAdd(rm, x, y)
10040  fpAdd(RNE(), x, y)
10041  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
10042  x + y
10043  >>> fpAdd(rm, x, y).sort()
10044  FPSort(8, 24)
10045  """
10046  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
10047 
10048 
def fpAdd(rm, a, b, ctx=None)
Definition: z3py.py:10032

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

10354 def fpBVToFP(v, sort, ctx=None):
10355  """Create a Z3 floating-point conversion expression that represents the
10356  conversion from a bit-vector term to a floating-point term.
10357 
10358  >>> x_bv = BitVecVal(0x3F800000, 32)
10359  >>> x_fp = fpBVToFP(x_bv, Float32())
10360  >>> x_fp
10361  fpToFP(1065353216)
10362  >>> simplify(x_fp)
10363  1
10364  """
10365  _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
10366  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
10367  ctx = _get_ctx(ctx)
10368  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
10369 
10370 
def fpBVToFP(v, sort, ctx=None)
Definition: z3py.py:10354
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
def is_fp_sort(s)
Definition: z3py.py:9282
def is_bv(a)
Definition: z3py.py:3906

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

10079 def fpDiv(rm, a, b, ctx=None):
10080  """Create a Z3 floating-point division expression.
10081 
10082  >>> s = FPSort(8, 24)
10083  >>> rm = RNE()
10084  >>> x = FP('x', s)
10085  >>> y = FP('y', s)
10086  >>> fpDiv(rm, x, y)
10087  fpDiv(RNE(), x, y)
10088  >>> fpDiv(rm, x, y).sort()
10089  FPSort(8, 24)
10090  """
10091  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
10092 
10093 
def fpDiv(rm, a, b, ctx=None)
Definition: z3py.py:10079

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

Referenced by fpFP(), and fpNEQ().

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

◆ fpFMA()

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

Definition at line 10138 of file z3py.py.

10138 def fpFMA(rm, a, b, c, ctx=None):
10139  """Create a Z3 floating-point fused multiply-add expression.
10140  """
10141  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
10142 
10143 
def fpFMA(rm, a, b, c, ctx=None)
Definition: z3py.py:10138

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

10286 def fpFP(sgn, exp, sig, ctx=None):
10287  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
10288 
10289  >>> s = FPSort(8, 24)
10290  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
10291  >>> print(x)
10292  fpFP(1, 127, 4194304)
10293  >>> xv = FPVal(-1.5, s)
10294  >>> print(xv)
10295  -1.5
10296  >>> slvr = Solver()
10297  >>> slvr.add(fpEQ(x, xv))
10298  >>> slvr.check()
10299  sat
10300  >>> xv = FPVal(+1.5, s)
10301  >>> print(xv)
10302  1.5
10303  >>> slvr = Solver()
10304  >>> slvr.add(fpEQ(x, xv))
10305  >>> slvr.check()
10306  unsat
10307  """
10308  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
10309  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
10310  ctx = _get_ctx(ctx)
10311  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
10312  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
10313 
10314 
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
def fpFP(sgn, exp, sig, ctx=None)
Definition: z3py.py:10286
def is_bv(a)
Definition: z3py.py:3906

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

10371 def fpFPToFP(rm, v, sort, ctx=None):
10372  """Create a Z3 floating-point conversion expression that represents the
10373  conversion from a floating-point term to a floating-point term of different precision.
10374 
10375  >>> x_sgl = FPVal(1.0, Float32())
10376  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
10377  >>> x_dbl
10378  fpToFP(RNE(), 1)
10379  >>> simplify(x_dbl)
10380  1
10381  >>> x_dbl.sort()
10382  FPSort(11, 53)
10383  """
10384  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10385  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
10386  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10387  ctx = _get_ctx(ctx)
10388  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10389 
10390 
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
def is_fp_sort(s)
Definition: z3py.py:9282
def fpFPToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10371
def is_fprm(a)
Definition: z3py.py:9542
def is_fp(a)
Definition: z3py.py:9698

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

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

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

10238 def fpGT(a, b, ctx=None):
10239  """Create the Z3 floating-point expression `other > self`.
10240 
10241  >>> x, y = FPs('x y', FPSort(8, 24))
10242  >>> fpGT(x, y)
10243  x > y
10244  >>> (x > y).sexpr()
10245  '(fp.gt x y)'
10246  """
10247  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
10248 
10249 
def fpGT(a, b, ctx=None)
Definition: z3py.py:10238

◆ fpInfinity()

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

Definition at line 9826 of file z3py.py.

9826 def fpInfinity(s, negative):
9827  """Create a Z3 floating-point +oo or -oo term."""
9828  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9829  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9830  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
9831 
9832 
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
def fpInfinity(s, negative)
Definition: z3py.py:9826

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

10168 def fpIsInf(a, ctx=None):
10169  """Create a Z3 floating-point isInfinite expression.
10170 
10171  >>> s = FPSort(8, 24)
10172  >>> x = FP('x', s)
10173  >>> fpIsInf(x)
10174  fpIsInf(x)
10175  """
10176  return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
10177 
10178 
def fpIsInf(a, ctx=None)
Definition: z3py.py:10168

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

10156 def fpIsNaN(a, ctx=None):
10157  """Create a Z3 floating-point isNaN expression.
10158 
10159  >>> s = FPSort(8, 24)
10160  >>> x = FP('x', s)
10161  >>> y = FP('y', s)
10162  >>> fpIsNaN(x)
10163  fpIsNaN(x)
10164  """
10165  return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
10166 
10167 
def fpIsNaN(a, ctx=None)
Definition: z3py.py:10156

◆ fpIsNegative()

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

Definition at line 10197 of file z3py.py.

10197 def fpIsNegative(a, ctx=None):
10198  """Create a Z3 floating-point isNegative expression.
10199  """
10200  return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
10201 
10202 
def fpIsNegative(a, ctx=None)
Definition: z3py.py:10197

◆ fpIsNormal()

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

Definition at line 10185 of file z3py.py.

10185 def fpIsNormal(a, ctx=None):
10186  """Create a Z3 floating-point isNormal expression.
10187  """
10188  return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
10189 
10190 
def fpIsNormal(a, ctx=None)
Definition: z3py.py:10185

◆ fpIsPositive()

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

Definition at line 10203 of file z3py.py.

10203 def fpIsPositive(a, ctx=None):
10204  """Create a Z3 floating-point isPositive expression.
10205  """
10206  return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
10207 
10208 
def fpIsPositive(a, ctx=None)
Definition: z3py.py:10203

◆ fpIsSubnormal()

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

Definition at line 10191 of file z3py.py.

10191 def fpIsSubnormal(a, ctx=None):
10192  """Create a Z3 floating-point isSubnormal expression.
10193  """
10194  return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
10195 
10196 
def fpIsSubnormal(a, ctx=None)
Definition: z3py.py:10191

◆ fpIsZero()

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

Definition at line 10179 of file z3py.py.

10179 def fpIsZero(a, ctx=None):
10180  """Create a Z3 floating-point isZero expression.
10181  """
10182  return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
10183 
10184 
def fpIsZero(a, ctx=None)
Definition: z3py.py:10179

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

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

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

10214 def fpLT(a, b, ctx=None):
10215  """Create the Z3 floating-point expression `other < self`.
10216 
10217  >>> x, y = FPs('x y', FPSort(8, 24))
10218  >>> fpLT(x, y)
10219  x < y
10220  >>> (x < y).sexpr()
10221  '(fp.lt x y)'
10222  """
10223  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
10224 
10225 
def fpLT(a, b, ctx=None)
Definition: z3py.py:10214

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

10123 def fpMax(a, b, ctx=None):
10124  """Create a Z3 floating-point maximum expression.
10125 
10126  >>> s = FPSort(8, 24)
10127  >>> rm = RNE()
10128  >>> x = FP('x', s)
10129  >>> y = FP('y', s)
10130  >>> fpMax(x, y)
10131  fpMax(x, y)
10132  >>> fpMax(x, y).sort()
10133  FPSort(8, 24)
10134  """
10135  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
10136 
10137 
def fpMax(a, b, ctx=None)
Definition: z3py.py:10123

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

10108 def fpMin(a, b, ctx=None):
10109  """Create a Z3 floating-point minimum expression.
10110 
10111  >>> s = FPSort(8, 24)
10112  >>> rm = RNE()
10113  >>> x = FP('x', s)
10114  >>> y = FP('y', s)
10115  >>> fpMin(x, y)
10116  fpMin(x, y)
10117  >>> fpMin(x, y).sort()
10118  FPSort(8, 24)
10119  """
10120  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
10121 
10122 
def fpMin(a, b, ctx=None)
Definition: z3py.py:10108

◆ fpMinusInfinity()

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

Definition at line 9820 of file z3py.py.

9820 def fpMinusInfinity(s):
9821  """Create a Z3 floating-point -oo term."""
9822  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9823  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9824 
9825 
def fpMinusInfinity(s)
Definition: z3py.py:9820
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.

◆ fpMinusZero()

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

Definition at line 9839 of file z3py.py.

9839 def fpMinusZero(s):
9840  """Create a Z3 floating-point -0.0 term."""
9841  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9842  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
9843 
9844 
def fpMinusZero(s)
Definition: z3py.py:9839
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.

◆ fpMul()

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

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

Definition at line 10064 of file z3py.py.

Referenced by FPs().

10064 def fpMul(rm, a, b, ctx=None):
10065  """Create a Z3 floating-point multiplication expression.
10066 
10067  >>> s = FPSort(8, 24)
10068  >>> rm = RNE()
10069  >>> x = FP('x', s)
10070  >>> y = FP('y', s)
10071  >>> fpMul(rm, x, y)
10072  fpMul(RNE(), x, y)
10073  >>> fpMul(rm, x, y).sort()
10074  FPSort(8, 24)
10075  """
10076  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
10077 
10078 
def fpMul(rm, a, b, ctx=None)
Definition: z3py.py:10064

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

9786 def fpNaN(s):
9787  """Create a Z3 floating-point NaN term.
9788 
9789  >>> s = FPSort(8, 24)
9790  >>> set_fpa_pretty(True)
9791  >>> fpNaN(s)
9792  NaN
9793  >>> pb = get_fpa_pretty()
9794  >>> set_fpa_pretty(False)
9795  >>> fpNaN(s)
9796  fpNaN(FPSort(8, 24))
9797  >>> set_fpa_pretty(pb)
9798  """
9799  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9800  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9801 
9802 
def fpNaN(s)
Definition: z3py.py:9786
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.

◆ fpNeg()

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

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

Definition at line 9964 of file z3py.py.

9964 def fpNeg(a, ctx=None):
9965  """Create a Z3 floating-point addition expression.
9966 
9967  >>> s = FPSort(8, 24)
9968  >>> rm = RNE()
9969  >>> x = FP('x', s)
9970  >>> fpNeg(x)
9971  -x
9972  >>> fpNeg(x).sort()
9973  FPSort(8, 24)
9974  """
9975  ctx = _get_ctx(ctx)
9976  [a] = _coerce_fp_expr_list([a], ctx)
9977  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
9978 
9979 
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
def fpNeg(a, ctx=None)
Definition: z3py.py:9964

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

10274 def fpNEQ(a, b, ctx=None):
10275  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
10276 
10277  >>> x, y = FPs('x y', FPSort(8, 24))
10278  >>> fpNEQ(x, y)
10279  Not(fpEQ(x, y))
10280  >>> (x != y).sexpr()
10281  '(distinct x y)'
10282  """
10283  return Not(fpEQ(a, b, ctx))
10284 
10285 
def fpEQ(a, b, ctx=None)
Definition: z3py.py:10262
def Not(a, ctx=None)
Definition: z3py.py:1779
def fpNEQ(a, b, ctx=None)
Definition: z3py.py:10274

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

9803 def fpPlusInfinity(s):
9804  """Create a Z3 floating-point +oo term.
9805 
9806  >>> s = FPSort(8, 24)
9807  >>> pb = get_fpa_pretty()
9808  >>> set_fpa_pretty(True)
9809  >>> fpPlusInfinity(s)
9810  +oo
9811  >>> set_fpa_pretty(False)
9812  >>> fpPlusInfinity(s)
9813  fpPlusInfinity(FPSort(8, 24))
9814  >>> set_fpa_pretty(pb)
9815  """
9816  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9817  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9818 
9819 
def fpPlusInfinity(s)
Definition: z3py.py:9803
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.

◆ fpPlusZero()

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

Definition at line 9833 of file z3py.py.

9833 def fpPlusZero(s):
9834  """Create a Z3 floating-point +0.0 term."""
9835  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9836  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
9837 
9838 
def fpPlusZero(s)
Definition: z3py.py:9833
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.

◆ fpRealToFP()

def z3py.fpRealToFP (   rm,
  v,
  sort,
  ctx = None 
)
Create a Z3 floating-point conversion expression that represents the
conversion from a real term to a floating-point term.

>>> x_r = RealVal(1.5)
>>> x_fp = fpRealToFP(RNE(), x_r, Float32())
>>> x_fp
fpToFP(RNE(), 3/2)
>>> simplify(x_fp)
1.5

Definition at line 10391 of file z3py.py.

10391 def fpRealToFP(rm, v, sort, ctx=None):
10392  """Create a Z3 floating-point conversion expression that represents the
10393  conversion from a real term to a floating-point term.
10394 
10395  >>> x_r = RealVal(1.5)
10396  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
10397  >>> x_fp
10398  fpToFP(RNE(), 3/2)
10399  >>> simplify(x_fp)
10400  1.5
10401  """
10402  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10403  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
10404  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10405  ctx = _get_ctx(ctx)
10406  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10407 
10408 
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
def is_real(a)
Definition: z3py.py:2667
def is_fp_sort(s)
Definition: z3py.py:9282
def fpRealToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10391
def is_fprm(a)
Definition: z3py.py:9542

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

10094 def fpRem(a, b, ctx=None):
10095  """Create a Z3 floating-point remainder expression.
10096 
10097  >>> s = FPSort(8, 24)
10098  >>> x = FP('x', s)
10099  >>> y = FP('y', s)
10100  >>> fpRem(x, y)
10101  fpRem(x, y)
10102  >>> fpRem(x, y).sort()
10103  FPSort(8, 24)
10104  """
10105  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
10106 
10107 
def fpRem(a, b, ctx=None)
Definition: z3py.py:10094

◆ fpRoundToIntegral()

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

Definition at line 10150 of file z3py.py.

10150 def fpRoundToIntegral(rm, a, ctx=None):
10151  """Create a Z3 floating-point roundToIntegral expression.
10152  """
10153  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
10154 
10155 
def fpRoundToIntegral(rm, a, ctx=None)
Definition: z3py.py:10150

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

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

9922 def FPs(names, fpsort, ctx=None):
9923  """Return an array of floating-point constants.
9924 
9925  >>> x, y, z = FPs('x y z', FPSort(8, 24))
9926  >>> x.sort()
9927  FPSort(8, 24)
9928  >>> x.sbits()
9929  24
9930  >>> x.ebits()
9931  8
9932  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9933  fpMul(RNE(), fpAdd(RNE(), x, y), z)
9934  """
9935  ctx = _get_ctx(ctx)
9936  if isinstance(names, str):
9937  names = names.split(" ")
9938  return [FP(name, fpsort, ctx) for name in names]
9939 
9940 
def FPs(names, fpsort, ctx=None)
Definition: z3py.py:9922
def FP(name, fpsort, ctx=None)
Definition: z3py.py:9898

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

10409 def fpSignedToFP(rm, v, sort, ctx=None):
10410  """Create a Z3 floating-point conversion expression that represents the
10411  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
10412 
10413  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10414  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
10415  >>> x_fp
10416  fpToFP(RNE(), 4294967291)
10417  >>> simplify(x_fp)
10418  -1.25*(2**2)
10419  """
10420  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10421  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10422  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10423  ctx = _get_ctx(ctx)
10424  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10425 
10426 
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement signed bit-vector term into a term of FloatingPoint sort...
def fpSignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10409
def is_fp_sort(s)
Definition: z3py.py:9282
def is_bv(a)
Definition: z3py.py:3906
def is_fprm(a)
Definition: z3py.py:9542

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

Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FPSortRef.cast(), FPSortRef.ebits(), FPRef.ebits(), FPNumRef.exponent(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpFP(), fpFPToFP(), fpGEQ(), fpGT(), fpIsInf(), fpIsNaN(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNaN(), fpNeg(), fpNEQ(), fpPlusInfinity(), fpRem(), FPs(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), is_fp(), is_fp_sort(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), Context.MkFPRTZ(), Context.mkFPSort(), Context.mkFPSort128(), Context.MkFPSort128(), Context.mkFPSort16(), Context.MkFPSort16(), Context.mkFPSort32(), Context.MkFPSort32(), Context.mkFPSort64(), Context.MkFPSort64(), Context.mkFPSortDouble(), Context.MkFPSortDouble(), Context.mkFPSortHalf(), Context.MkFPSortHalf(), Context.mkFPSortQuadruple(), Context.MkFPSortQuadruple(), Context.mkFPSortSingle(), Context.MkFPSortSingle(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPRef.sort(), Sort.translate(), and Sort.Translate().

9727 def FPSort(ebits, sbits, ctx=None):
9728  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9729 
9730  >>> Single = FPSort(8, 24)
9731  >>> Double = FPSort(11, 53)
9732  >>> Single
9733  FPSort(8, 24)
9734  >>> x = Const('x', Single)
9735  >>> eq(x, FP('x', FPSort(8, 24)))
9736  True
9737  """
9738  ctx = _get_ctx(ctx)
9739  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9740 
9741 
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727

◆ fpSqrt()

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

Definition at line 10144 of file z3py.py.

10144 def fpSqrt(rm, a, ctx=None):
10145  """Create a Z3 floating-point square root expression.
10146  """
10147  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
10148 
10149 
def fpSqrt(rm, a, ctx=None)
Definition: z3py.py:10144

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

10049 def fpSub(rm, a, b, ctx=None):
10050  """Create a Z3 floating-point subtraction expression.
10051 
10052  >>> s = FPSort(8, 24)
10053  >>> rm = RNE()
10054  >>> x = FP('x', s)
10055  >>> y = FP('y', s)
10056  >>> fpSub(rm, x, y)
10057  fpSub(RNE(), x, y)
10058  >>> fpSub(rm, x, y).sort()
10059  FPSort(8, 24)
10060  """
10061  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
10062 
10063 
def fpSub(rm, a, b, ctx=None)
Definition: z3py.py:10049

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

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

10315 def fpToFP(a1, a2=None, a3=None, ctx=None):
10316  """Create a Z3 floating-point conversion expression from other term sorts
10317  to floating-point.
10318 
10319  From a bit-vector term in IEEE 754-2008 format:
10320  >>> x = FPVal(1.0, Float32())
10321  >>> x_bv = fpToIEEEBV(x)
10322  >>> simplify(fpToFP(x_bv, Float32()))
10323  1
10324 
10325  From a floating-point term with different precision:
10326  >>> x = FPVal(1.0, Float32())
10327  >>> x_db = fpToFP(RNE(), x, Float64())
10328  >>> x_db.sort()
10329  FPSort(11, 53)
10330 
10331  From a real term:
10332  >>> x_r = RealVal(1.5)
10333  >>> simplify(fpToFP(RNE(), x_r, Float32()))
10334  1.5
10335 
10336  From a signed bit-vector term:
10337  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10338  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
10339  -1.25*(2**2)
10340  """
10341  ctx = _get_ctx(ctx)
10342  if is_bv(a1) and is_fp_sort(a2):
10343  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
10344  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
10345  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10346  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
10347  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10348  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
10349  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10350  else:
10351  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
10352 
10353 
def fpToFP(a1, a2=None, a3=None, ctx=None)
Definition: z3py.py:10315
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement signed bit-vector term into a term of FloatingPoint sort...
def is_real(a)
Definition: z3py.py:2667
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
def is_fp_sort(s)
Definition: z3py.py:9282
def is_bv(a)
Definition: z3py.py:3906
def is_fprm(a)
Definition: z3py.py:9542
def is_fp(a)
Definition: z3py.py:9698

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

Referenced by fpUnsignedToFP().

10445 def fpToFPUnsigned(rm, x, s, ctx=None):
10446  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
10447  if z3_debug():
10448  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10449  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
10450  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
10451  ctx = _get_ctx(ctx)
10452  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
10453 
10454 
def fpToFPUnsigned(rm, x, s, ctx=None)
Definition: z3py.py:10445
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement unsigned bit-vector term into a term of FloatingPoint sort...
def z3_debug()
Definition: z3py.py:64
def is_fp_sort(s)
Definition: z3py.py:9282
def is_bv(a)
Definition: z3py.py:3906
def is_fprm(a)
Definition: z3py.py:9542

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

Referenced by fpToFP().

10519 def fpToIEEEBV(x, ctx=None):
10520  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
10521 
10522  The size of the resulting bit-vector is automatically determined.
10523 
10524  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
10525  knows only one NaN and it will always produce the same bit-vector representation of
10526  that NaN.
10527 
10528  >>> x = FP('x', FPSort(8, 24))
10529  >>> y = fpToIEEEBV(x)
10530  >>> print(is_fp(x))
10531  True
10532  >>> print(is_bv(y))
10533  True
10534  >>> print(is_fp(y))
10535  False
10536  >>> print(is_bv(x))
10537  False
10538  """
10539  if z3_debug():
10540  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10541  ctx = _get_ctx(ctx)
10542  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
10543 
10544 
def fpToIEEEBV(x, ctx=None)
Definition: z3py.py:10519
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
def z3_debug()
Definition: z3py.py:64
def is_fp(a)
Definition: z3py.py:9698

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

10499 def fpToReal(x, ctx=None):
10500  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
10501 
10502  >>> x = FP('x', FPSort(8, 24))
10503  >>> y = fpToReal(x)
10504  >>> print(is_fp(x))
10505  True
10506  >>> print(is_real(y))
10507  True
10508  >>> print(is_fp(y))
10509  False
10510  >>> print(is_real(x))
10511  False
10512  """
10513  if z3_debug():
10514  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10515  ctx = _get_ctx(ctx)
10516  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
10517 
10518 
Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a real-numbered term.
def z3_debug()
Definition: z3py.py:64
def fpToReal(x, ctx=None)
Definition: z3py.py:10499
def is_fp(a)
Definition: z3py.py:9698

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

10455 def fpToSBV(rm, x, s, ctx=None):
10456  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
10457 
10458  >>> x = FP('x', FPSort(8, 24))
10459  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
10460  >>> print(is_fp(x))
10461  True
10462  >>> print(is_bv(y))
10463  True
10464  >>> print(is_fp(y))
10465  False
10466  >>> print(is_bv(x))
10467  False
10468  """
10469  if z3_debug():
10470  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10471  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10472  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10473  ctx = _get_ctx(ctx)
10474  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10475 
10476 
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
def fpToSBV(rm, x, s, ctx=None)
Definition: z3py.py:10455
def z3_debug()
Definition: z3py.py:64
def is_bv_sort(s)
Definition: z3py.py:3438
def is_fprm(a)
Definition: z3py.py:9542
def is_fp(a)
Definition: z3py.py:9698

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

10477 def fpToUBV(rm, x, s, ctx=None):
10478  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
10479 
10480  >>> x = FP('x', FPSort(8, 24))
10481  >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
10482  >>> print(is_fp(x))
10483  True
10484  >>> print(is_bv(y))
10485  True
10486  >>> print(is_fp(y))
10487  False
10488  >>> print(is_bv(x))
10489  False
10490  """
10491  if z3_debug():
10492  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10493  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10494  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10495  ctx = _get_ctx(ctx)
10496  return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10497 
10498 
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
def fpToUBV(rm, x, s, ctx=None)
Definition: z3py.py:10477
def z3_debug()
Definition: z3py.py:64
def is_bv_sort(s)
Definition: z3py.py:3438
def is_fprm(a)
Definition: z3py.py:9542
def is_fp(a)
Definition: z3py.py:9698

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

10427 def fpUnsignedToFP(rm, v, sort, ctx=None):
10428  """Create a Z3 floating-point conversion expression that represents the
10429  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
10430 
10431  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10432  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
10433  >>> x_fp
10434  fpToFPUnsigned(RNE(), 4294967291)
10435  >>> simplify(x_fp)
10436  1*(2**32)
10437  """
10438  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10439  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10440  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10441  ctx = _get_ctx(ctx)
10442  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10443 
10444 
def fpUnsignedToFP(rm, v, sort, ctx=None)
Definition: z3py.py:10427
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2&#39;s complement unsigned bit-vector term into a term of FloatingPoint sort...
def is_fp_sort(s)
Definition: z3py.py:9282
def is_bv(a)
Definition: z3py.py:3906
def is_fprm(a)
Definition: z3py.py:9542

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

Referenced by FPNumRef.exponent(), fpAbs(), fpFP(), fpFPToFP(), fpToFP(), is_fp_value(), FPNumRef.isNegative(), FPNumRef.sign_as_bv(), FPNumRef.significand(), and FPNumRef.significand_as_bv().

9852 def FPVal(sig, exp=None, fps=None, ctx=None):
9853  """Return a floating-point value of value `val` and sort `fps`.
9854  If `ctx=None`, then the global context is used.
9855 
9856  >>> v = FPVal(20.0, FPSort(8, 24))
9857  >>> v
9858  1.25*(2**4)
9859  >>> print("0x%.8x" % v.exponent_as_long(False))
9860  0x00000004
9861  >>> v = FPVal(2.25, FPSort(8, 24))
9862  >>> v
9863  1.125*(2**1)
9864  >>> v = FPVal(-2.25, FPSort(8, 24))
9865  >>> v
9866  -1.125*(2**1)
9867  >>> FPVal(-0.0, FPSort(8, 24))
9868  -0.0
9869  >>> FPVal(0.0, FPSort(8, 24))
9870  +0.0
9871  >>> FPVal(+0.0, FPSort(8, 24))
9872  +0.0
9873  """
9874  ctx = _get_ctx(ctx)
9875  if is_fp_sort(exp):
9876  fps = exp
9877  exp = None
9878  elif fps is None:
9879  fps = _dflt_fps(ctx)
9880  _z3_assert(is_fp_sort(fps), "sort mismatch")
9881  if exp is None:
9882  exp = 0
9883  val = _to_float_str(sig)
9884  if val == "NaN" or val == "nan":
9885  return fpNaN(fps)
9886  elif val == "-0.0":
9887  return fpMinusZero(fps)
9888  elif val == "0.0" or val == "+0.0":
9889  return fpPlusZero(fps)
9890  elif val == "+oo" or val == "+inf" or val == "+Inf":
9891  return fpPlusInfinity(fps)
9892  elif val == "-oo" or val == "-inf" or val == "-Inf":
9893  return fpMinusInfinity(fps)
9894  else:
9895  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
9896 
9897 
def FPVal(sig, exp=None, fps=None, ctx=None)
Definition: z3py.py:9852
def fpMinusInfinity(s)
Definition: z3py.py:9820
def fpMinusZero(s)
Definition: z3py.py:9839
def fpPlusZero(s)
Definition: z3py.py:9833
def fpPlusInfinity(s)
Definition: z3py.py:9803
def fpNaN(s)
Definition: z3py.py:9786
def is_fp_sort(s)
Definition: z3py.py:9282
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ fpZero()

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

Definition at line 9845 of file z3py.py.

9845 def fpZero(s, negative):
9846  """Create a Z3 floating-point +0.0 or -0.0 term."""
9847  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9848  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9849  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
9850 
9851 
def fpZero(s, negative)
Definition: z3py.py:9845
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.

◆ FreshBool()

def z3py.FreshBool (   prefix = "b",
  ctx = None 
)
Return a fresh Boolean constant in the given context using the given prefix.

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

>>> b1 = FreshBool()
>>> b2 = FreshBool()
>>> eq(b1, b2)
False

Definition at line 1735 of file z3py.py.

1735 def FreshBool(prefix="b", ctx=None):
1736  """Return a fresh Boolean constant in the given context using the given prefix.
1737 
1738  If `ctx=None`, then the global context is used.
1739 
1740  >>> b1 = FreshBool()
1741  >>> b2 = FreshBool()
1742  >>> eq(b1, b2)
1743  False
1744  """
1745  ctx = _get_ctx(ctx)
1746  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1747 
1748 
def FreshBool(prefix="b", ctx=None)
Definition: z3py.py:1735
def BoolSort(ctx=None)
Definition: z3py.py:1655
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshConst()

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

Definition at line 1432 of file z3py.py.

1432 def FreshConst(sort, prefix="c"):
1433  """Create a fresh constant of a specified sort"""
1434  ctx = _get_ctx(sort.ctx)
1435  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1436 
1437 
def FreshConst(sort, prefix="c")
Definition: z3py.py:1432
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshFunction()

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

Definition at line 883 of file z3py.py.

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

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

3249 def FreshInt(prefix="x", ctx=None):
3250  """Return a fresh integer constant in the given context using the given prefix.
3251 
3252  >>> x = FreshInt()
3253  >>> y = FreshInt()
3254  >>> eq(x, y)
3255  False
3256  >>> x.sort()
3257  Int
3258  """
3259  ctx = _get_ctx(ctx)
3260  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3261 
3262 
def FreshInt(prefix="x", ctx=None)
Definition: z3py.py:3249
def IntSort(ctx=None)
Definition: z3py.py:3100
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ FreshReal()

def z3py.FreshReal (   prefix = "b",
  ctx = None 
)
Return a fresh real constant in the given context using the given prefix.

>>> x = FreshReal()
>>> y = FreshReal()
>>> eq(x, y)
False
>>> x.sort()
Real

Definition at line 3306 of file z3py.py.

3306 def FreshReal(prefix="b", ctx=None):
3307  """Return a fresh real constant in the given context using the given prefix.
3308 
3309  >>> x = FreshReal()
3310  >>> y = FreshReal()
3311  >>> eq(x, y)
3312  False
3313  >>> x.sort()
3314  Real
3315  """
3316  ctx = _get_ctx(ctx)
3317  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3318 
3319 
def FreshReal(prefix="b", ctx=None)
Definition: z3py.py:3306
def RealSort(ctx=None)
Definition: z3py.py:3117
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.

◆ Full()

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

Definition at line 10740 of file z3py.py.

10740 def Full(s):
10741  """Create the regular expression that accepts the universal language
10742  >>> e = Full(ReSort(SeqSort(IntSort())))
10743  >>> print(e)
10744  Full(ReSort(Seq(Int)))
10745  >>> e1 = Full(ReSort(StringSort()))
10746  >>> print(e1)
10747  Full(ReSort(String))
10748  """
10749  if isinstance(s, ReSortRef):
10750  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10751  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10752 
10753 
def Full(s)
Definition: z3py.py:10740
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.

◆ FullSet()

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

Definition at line 4865 of file z3py.py.

4865 def FullSet(s):
4866  """Create the full set
4867  >>> FullSet(IntSort())
4868  K(Int, True)
4869  """
4870  ctx = s.ctx
4871  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4872 
4873 
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
def FullSet(s)
Definition: z3py.py:4865

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

Referenced by ModelRef.__getitem__(), ModelRef.__len__(), FuncEntry.arg_value(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), QuantifierRef.children(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), ModelRef.get_interp(), get_map_func(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), Lambda(), Map(), MultiPattern(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

860 def Function(name, *sig):
861  """Create a new Z3 uninterpreted function with the given sorts.
862 
863  >>> f = Function('f', IntSort(), IntSort())
864  >>> f(f(0))
865  f(f(0))
866  """
867  sig = _get_args(sig)
868  if z3_debug():
869  _z3_assert(len(sig) > 0, "At least two arguments expected")
870  arity = len(sig) - 1
871  rng = sig[arity]
872  if z3_debug():
873  _z3_assert(is_sort(rng), "Z3 sort expected")
874  dom = (Sort * arity)()
875  for i in range(arity):
876  if z3_debug():
877  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
878  dom[i] = sig[i].ast
879  ctx = rng.ctx
880  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
881 
882 
def Function(name, sig)
Definition: z3py.py:860
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def to_symbol(s, ctx=None)
Definition: z3py.py:129
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
def is_sort(s)
Definition: z3py.py:646
def z3_debug()
Definition: z3py.py:64

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

6589 def get_as_array_func(n):
6590  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6591  if z3_debug():
6592  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6593  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6594 
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
def get_as_array_func(n)
Definition: z3py.py:6589
def z3_debug()
Definition: z3py.py:64
def is_as_array(n)
Definition: z3py.py:6584

◆ 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 
def get_ctx(ctx)
Definition: z3py.py:266

◆ get_default_fp_sort()

def z3py.get_default_fp_sort (   ctx = None)

Definition at line 9149 of file z3py.py.

9149 def get_default_fp_sort(ctx=None):
9150  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
9151 
9152 
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727
def get_default_fp_sort(ctx=None)
Definition: z3py.py:9149

◆ get_default_rounding_mode()

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

Definition at line 9116 of file z3py.py.

9116 def get_default_rounding_mode(ctx=None):
9117  """Retrieves the global default rounding mode."""
9118  global _dflt_rounding_mode
9119  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
9120  return RTZ(ctx)
9121  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
9122  return RTN(ctx)
9123  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
9124  return RTP(ctx)
9125  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
9126  return RNE(ctx)
9127  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
9128  return RNA(ctx)
9129 
9130 
def RTN(ctx=None)
Definition: z3py.py:9527
def RTZ(ctx=None)
Definition: z3py.py:9537
def RTP(ctx=None)
Definition: z3py.py:9517
def RNA(ctx=None)
Definition: z3py.py:9507
def get_default_rounding_mode(ctx=None)
Definition: z3py.py:9116
def RNE(ctx=None)
Definition: z3py.py:9497

◆ 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 
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
def get_full_version()
Definition: z3py.py:103

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

4621 def get_map_func(a):
4622  """Return the function declaration associated with a Z3 map array expression.
4623 
4624  >>> f = Function('f', IntSort(), IntSort())
4625  >>> b = Array('b', IntSort(), IntSort())
4626  >>> a = Map(f, b)
4627  >>> eq(f, get_map_func(a))
4628  True
4629  >>> get_map_func(a)
4630  f
4631  >>> get_map_func(a)(0)
4632  f(0)
4633  """
4634  if z3_debug():
4635  _z3_assert(is_map(a), "Z3 array map expression expected.")
4636  return FuncDeclRef(
4638  a.ctx_ref(),
4639  Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
4640  ),
4641  ctx=a.ctx,
4642  )
4643 
4644 
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
def is_map(a)
Definition: z3py.py:4596
def get_map_func(a)
Definition: z3py.py:4621
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def z3_debug()
Definition: z3py.py:64

◆ 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 
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
def get_param(name)
Definition: z3py.py:306

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

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

◆ 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 
def get_version()
Definition: z3py.py:94
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.

◆ get_version_string()

def z3py.get_version_string ( )

Definition at line 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 
def get_version_string()
Definition: z3py.py:85
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.

◆ help_simplify()

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

Definition at line 8670 of file z3py.py.

8670 def help_simplify():
8671  """Return a string describing all options available for Z3 `simplify` procedure."""
8672  print(Z3_simplify_get_help(main_ctx().ref()))
8673 
8674 
def main_ctx()
Definition: z3py.py:238
def help_simplify()
Definition: z3py.py:8670
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.

◆ If()

def z3py.If (   a,
  b,
  c,
  ctx = None 
)
Create a Z3 if-then-else expression.

>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
>>> max
If(x > y, x, y)
>>> simplify(max)
If(x <= y, y, x)

Definition at line 1349 of file z3py.py.

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

1349 def If(a, b, c, ctx=None):
1350  """Create a Z3 if-then-else expression.
1351 
1352  >>> x = Int('x')
1353  >>> y = Int('y')
1354  >>> max = If(x > y, x, y)
1355  >>> max
1356  If(x > y, x, y)
1357  >>> simplify(max)
1358  If(x <= y, y, x)
1359  """
1360  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1361  return Cond(a, b, c, ctx)
1362  else:
1363  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1364  s = BoolSort(ctx)
1365  a = s.cast(a)
1366  b, c = _coerce_exprs(b, c, ctx)
1367  if z3_debug():
1368  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1369  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1370 
1371 
def If(a, b, c, ctx=None)
Definition: z3py.py:1349
def Cond(p, t1, t2, ctx=None)
Definition: z3py.py:8628
def z3_debug()
Definition: z3py.py:64
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
def BoolSort(ctx=None)
Definition: z3py.py:1655

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

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

1749 def Implies(a, b, ctx=None):
1750  """Create a Z3 implies expression.
1751 
1752  >>> p, q = Bools('p q')
1753  >>> Implies(p, q)
1754  Implies(p, q)
1755  """
1756  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1757  s = BoolSort(ctx)
1758  a = s.cast(a)
1759  b = s.cast(b)
1760  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1761 
1762 
def Implies(a, b, ctx=None)
Definition: z3py.py:1749
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
def BoolSort(ctx=None)
Definition: z3py.py:1655

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

10823 def IndexOf(s, substr, offset=None):
10824  """Retrieve the index of substring within a string starting at a specified offset.
10825  >>> simplify(IndexOf("abcabc", "bc", 0))
10826  1
10827  >>> simplify(IndexOf("abcabc", "bc", 2))
10828  4
10829  """
10830  if offset is None:
10831  offset = IntVal(0)
10832  ctx = None
10833  if is_expr(offset):
10834  ctx = offset.ctx
10835  ctx = _get_ctx2(s, substr, ctx)
10836  s = _coerce_seq(s, ctx)
10837  substr = _coerce_seq(substr, ctx)
10838  if _is_int(offset):
10839  offset = IntVal(offset, ctx)
10840  return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
10841 
10842 
def IntVal(val, ctx=None)
Definition: z3py.py:3150
def IndexOf(s, substr, offset=None)
Definition: z3py.py:10823
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
def is_expr(a)
Definition: z3py.py:1210

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

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

10924 def InRe(s, re):
10925  """Create regular expression membership test
10926  >>> re = Union(Re("a"),Re("b"))
10927  >>> print (simplify(InRe("a", re)))
10928  True
10929  >>> print (simplify(InRe("b", re)))
10930  True
10931  >>> print (simplify(InRe("c", re)))
10932  False
10933  """
10934  s = _coerce_seq(s, re.ctx)
10935  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
10936 
10937 
def InRe(s, re)
Definition: z3py.py:10924
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.

◆ Int()

def z3py.Int (   name,
  ctx = None 
)
Return an integer constant named `name`. If `ctx=None`, then the global context is used.

>>> x = Int('x')
>>> is_int(x)
True
>>> is_int(x + 1)
True

Definition at line 3210 of file z3py.py.

Referenced by ArithRef.__add__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ArithRef.__mod__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), QuantifierRef.body(), BV2Int(), Solver.check(), QuantifierRef.children(), ModelRef.decls(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), Goal.insert(), Solver.insert(), is_arith(), is_arith_sort(), is_bv(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_fp(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_int_value(), QuantifierRef.is_lambda(), is_pattern(), is_quantifier(), ArithSortRef.is_real(), is_real(), is_select(), is_to_real(), K(), AstMap.keys(), Statistics.keys(), Solver.model(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), Solver.pop(), AstVector.push(), Solver.push(), Solver.reason_unknown(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), Solver.sexpr(), Goal.simplify(), ArithRef.sort(), Solver.statistics(), Store(), ToReal(), Goal.translate(), AstVector.translate(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

3210 def Int(name, ctx=None):
3211  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3212 
3213  >>> x = Int('x')
3214  >>> is_int(x)
3215  True
3216  >>> is_int(x + 1)
3217  True
3218  """
3219  ctx = _get_ctx(ctx)
3220  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3221 
3222 
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
def to_symbol(s, ctx=None)
Definition: z3py.py:129
def Int(name, ctx=None)
Definition: z3py.py:3210
def IntSort(ctx=None)
Definition: z3py.py:3100

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

3958 def Int2BV(a, num_bits):
3959  """Return the z3 expression Int2BV(a, num_bits).
3960  It is a bit-vector of width num_bits and represents the
3961  modulo of a by 2^num_bits
3962  """
3963  ctx = a.ctx
3964  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
3965 
3966 
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
def Int2BV(a, num_bits)
Definition: z3py.py:3958

◆ Intersect()

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

Definition at line 10958 of file z3py.py.

10958 def Intersect(*args):
10959  """Create intersection of regular expressions.
10960  >>> re = Intersect(Re("a"), Re("b"), Re("c"))
10961  """
10962  args = _get_args(args)
10963  sz = len(args)
10964  if z3_debug():
10965  _z3_assert(sz > 0, "At least one argument expected.")
10966  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
10967  if sz == 1:
10968  return args[0]
10969  ctx = args[0].ctx
10970  v = (Ast * sz)()
10971  for i in range(sz):
10972  v[i] = args[i].as_ast()
10973  return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
10974 
10975 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def Intersect(args)
Definition: z3py.py:10958
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
def is_re(s)
Definition: z3py.py:10920
def z3_debug()
Definition: z3py.py:64

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

Referenced by ArithRef.__ge__(), Goal.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ArithRef.__lt__(), Goal.convert_model(), Goal.depth(), Goal.get(), Goal.inconsistent(), is_add(), is_div(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Lambda(), Goal.prec(), Goal.size(), Store(), Solver.unsat_core(), and Update().

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

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

Referenced by ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), DatatypeSortRef.accessor(), FuncEntry.arg_value(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), ArithSortRef.cast(), QuantifierRef.children(), DatatypeSortRef.constructor(), Datatype.create(), CreateDatatypes(), Datatype.declare(), ModelRef.decls(), Default(), DisjointSum(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), Full(), FullSet(), ModelRef.get_interp(), get_map_func(), Context.getIntSort(), is_arith_sort(), is_array(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_fp_sort(), is_K(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_select(), is_store(), SeqSortRef.is_string(), IsMember(), IsSubset(), K(), Lambda(), Map(), Context.mkIntSort(), Context.MkIntSort(), MultiPattern(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), ArraySortRef.range(), ArrayRef.range(), DatatypeSortRef.recognizer(), Select(), SeqSort(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), ArrayRef.sort(), Store(), Sort.translate(), Sort.Translate(), TupleSort(), Update(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

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

◆ IntToStr()

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

Definition at line 10878 of file z3py.py.

Referenced by StrToInt().

10878 def IntToStr(s):
10879  """Convert integer expression to string"""
10880  if not is_expr(s):
10881  s = _py2expr(s)
10882  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
10883 
10884 
def IntToStr(s)
Definition: z3py.py:10878
def is_expr(a)
Definition: z3py.py:1210
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.

◆ IntVal()

def z3py.IntVal (   val,
  ctx = None 
)
Return a Z3 integer value. If `ctx=None`, then the global context is used.

>>> IntVal(1)
1
>>> IntVal("100")
100

Definition at line 3150 of file z3py.py.

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

3150 def IntVal(val, ctx=None):
3151  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3152 
3153  >>> IntVal(1)
3154  1
3155  >>> IntVal("100")
3156  100
3157  """
3158  ctx = _get_ctx(ctx)
3159  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3160 
3161 
def IntVal(val, ctx=None)
Definition: z3py.py:3150
def IntSort(ctx=None)
Definition: z3py.py:3100
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ IntVector()

def z3py.IntVector (   prefix,
  sz,
  ctx = None 
)
Return a list of integer constants of size `sz`.

>>> X = IntVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2

Definition at line 3236 of file z3py.py.

3236 def IntVector(prefix, sz, ctx=None):
3237  """Return a list of integer constants of size `sz`.
3238 
3239  >>> X = IntVector('x', 3)
3240  >>> X
3241  [x__0, x__1, x__2]
3242  >>> Sum(X)
3243  x__0 + x__1 + x__2
3244  """
3245  ctx = _get_ctx(ctx)
3246  return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3247 
3248 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def Int(name, ctx=None)
Definition: z3py.py:3210
def IntVector(prefix, sz, ctx=None)
Definition: z3py.py:3236

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

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

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

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

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

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

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

Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), expr.hi(), expr.is_and(), is_app_of(), expr.is_const(), is_const(), expr.is_distinct(), expr.is_eq(), expr.is_false(), expr.is_implies(), expr.is_ite(), expr.is_not(), expr.is_or(), expr.is_true(), expr.is_xor(), expr.lo(), ExprRef.num_args(), expr.operator Z3_app(), and RecAddDefinition().

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

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

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

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

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

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

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

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

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

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

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

◆ is_array_sort()

def z3py.is_array_sort (   a)

Definition at line 4552 of file z3py.py.

4552 def is_array_sort(a):
4553  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4554 
4555 
def is_array_sort(a)
Definition: z3py.py:4552
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

◆ is_as_array()

def z3py.is_as_array (   n)
Return true if n is a Z3 expression of the form (_ as-array f).

Definition at line 6584 of file z3py.py.

6584 def is_as_array(n):
6585  """Return true if n is a Z3 expression of the form (_ as-array f)."""
6586  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6587 
6588 
def is_as_array(n)
Definition: z3py.py:6584
bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3...

◆ is_ast()

def z3py.is_ast (   a)
Return `True` if `a` is an AST node.

>>> is_ast(10)
False
>>> is_ast(IntVal(10))
True
>>> is_ast(Int('x'))
True
>>> is_ast(BoolSort())
True
>>> is_ast(Function('f', IntSort(), IntSort()))
True
>>> is_ast("x")
False
>>> is_ast(Solver())
False

Definition at line 450 of file z3py.py.

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

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 
def is_ast(a)
Definition: z3py.py:450

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

Referenced by BoolSort(), and prove().

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4612 def is_default(a):
4613  """Return `True` if `a` is a Z3 default array expression.
4614  >>> d = Default(K(IntSort(), 10))
4615  >>> is_default(d)
4616  True
4617  """
4618  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4619 
4620 
def is_default(a)
Definition: z3py.py:4612
def is_app_of(a, k)
Definition: z3py.py:1336

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

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

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

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

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

Referenced by AstRef.__bool__().

1633 def is_eq(a):
1634  """Return `True` if `a` is a Z3 equality expression.
1635 
1636  >>> x, y = Ints('x y')
1637  >>> is_eq(x == y)
1638  True
1639  """
1640  return is_app_of(a, Z3_OP_EQ)
1641 
1642 
def is_eq(a)
Definition: z3py.py:1633
def is_app_of(a, k)
Definition: z3py.py:1336

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

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

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

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

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

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

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

Referenced by is_finite_domain_value().

7621 def is_finite_domain(a):
7622  """Return `True` if `a` is a Z3 finite-domain expression.
7623 
7624  >>> s = FiniteDomainSort('S', 100)
7625  >>> b = Const('b', s)
7626  >>> is_finite_domain(b)
7627  True
7628  >>> is_finite_domain(Int('x'))
7629  False
7630  """
7631  return isinstance(a, FiniteDomainRef)
7632 
7633 
def is_finite_domain(a)
Definition: z3py.py:7621

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

Referenced by FiniteDomainVal().

7598 def is_finite_domain_sort(s):
7599  """Return True if `s` is a Z3 finite-domain sort.
7600 
7601  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7602  True
7603  >>> is_finite_domain_sort(IntSort())
7604  False
7605  """
7606  return isinstance(s, FiniteDomainSortRef)
7607 
7608 
def is_finite_domain_sort(s)
Definition: z3py.py:7598

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

7675 def is_finite_domain_value(a):
7676  """Return `True` if `a` is a Z3 finite-domain value.
7677 
7678  >>> s = FiniteDomainSort('S', 100)
7679  >>> b = Const('b', s)
7680  >>> is_finite_domain_value(b)
7681  False
7682  >>> b = FiniteDomainVal(10, s)
7683  >>> b
7684  10
7685  >>> is_finite_domain_value(b)
7686  True
7687  """
7688  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7689 
7690 
def is_finite_domain_value(a)
Definition: z3py.py:7675
def is_finite_domain(a)
Definition: z3py.py:7621

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

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

9698 def is_fp(a):
9699  """Return `True` if `a` is a Z3 floating-point expression.
9700 
9701  >>> b = FP('b', FPSort(8, 24))
9702  >>> is_fp(b)
9703  True
9704  >>> is_fp(b + 1.0)
9705  True
9706  >>> is_fp(Int('x'))
9707  False
9708  """
9709  return isinstance(a, FPRef)
9710 
9711 
def is_fp(a)
Definition: z3py.py:9698

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

9282 def is_fp_sort(s):
9283  """Return True if `s` is a Z3 floating-point sort.
9284 
9285  >>> is_fp_sort(FPSort(8, 24))
9286  True
9287  >>> is_fp_sort(IntSort())
9288  False
9289  """
9290  return isinstance(s, FPSortRef)
9291 
9292 
def is_fp_sort(s)
Definition: z3py.py:9282

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

9712 def is_fp_value(a):
9713  """Return `True` if `a` is a Z3 floating-point numeral value.
9714 
9715  >>> b = FP('b', FPSort(8, 24))
9716  >>> is_fp_value(b)
9717  False
9718  >>> b = FPVal(1.0, FPSort(8, 24))
9719  >>> b
9720  1
9721  >>> is_fp_value(b)
9722  True
9723  """
9724  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9725 
9726 
def is_fp_value(a)
Definition: z3py.py:9712
def is_fp(a)
Definition: z3py.py:9698

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

9542 def is_fprm(a):
9543  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9544 
9545  >>> rm = RNE()
9546  >>> is_fprm(rm)
9547  True
9548  >>> rm = 1.0
9549  >>> is_fprm(rm)
9550  False
9551  """
9552  return isinstance(a, FPRMRef)
9553 
9554 
def is_fprm(a)
Definition: z3py.py:9542

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

9293 def is_fprm_sort(s):
9294  """Return True if `s` is a Z3 floating-point rounding mode sort.
9295 
9296  >>> is_fprm_sort(FPSort(8, 24))
9297  False
9298  >>> is_fprm_sort(RNE().sort())
9299  True
9300  """
9301  return isinstance(s, FPRMSortRef)
9302 
9303 # FP Expressions
9304 
9305 
def is_fprm_sort(s)
Definition: z3py.py:9293

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

9555 def is_fprm_value(a):
9556  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9557  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9558 
9559 # FP Numerals
9560 
9561 
def is_fprm_value(a)
Definition: z3py.py:9555
def is_fprm(a)
Definition: z3py.py:9542

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

Referenced by prove().

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

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

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

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

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

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

Referenced by is_div().

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Referenced by MultiPattern().

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

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

Referenced by eq().

8511 def is_probe(p):
8512  """Return `True` if `p` is a Z3 probe.
8513 
8514  >>> is_probe(Int('x'))
8515  False
8516  >>> is_probe(Probe('memory'))
8517  True
8518  """
8519  return isinstance(p, Probe)
8520 
8521 
def is_probe(p)
Definition: z3py.py:8511

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

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

2138 def is_quantifier(a):
2139  """Return `True` if `a` is a Z3 quantifier.
2140 
2141  >>> f = Function('f', IntSort(), IntSort())
2142  >>> x = Int('x')
2143  >>> q = ForAll(x, f(x) == 0)
2144  >>> is_quantifier(q)
2145  True
2146  >>> is_quantifier(f(x))
2147  False
2148