Z3
Data Structures | Functions | Variables
z3py Namespace Reference

Data Structures

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

Functions

def z3_debug ()
 
def enable_trace (msg)
 
def disable_trace (msg)
 
def get_version_string ()
 
def get_version ()
 
def get_full_version ()
 
def open_log (fname)
 
def append_log (s)
 
def to_symbol (s, ctx=None)
 
def z3_error_handler (c, e)
 
def main_ctx ()
 
def get_ctx (ctx)
 
def set_param (*args, **kws)
 
def reset_params ()
 
def set_option (*args, **kws)
 
def get_param (name)
 
def is_ast (a)
 
def eq (a, b)
 
def is_sort (s)
 
def DeclareSort (name, ctx=None)
 
def is_func_decl (a)
 
def Function (name, *sig)
 
def FreshFunction (*sig)
 
def RecFunction (name, *sig)
 
def RecAddDefinition (f, args, body)
 
def deserialize (st)
 
def is_expr (a)
 
def is_app (a)
 
def is_const (a)
 
def is_var (a)
 
def get_var_index (a)
 
def is_app_of (a, k)
 
def If (a, b, c, ctx=None)
 
def Distinct (*args)
 
def Const (name, sort)
 
def Consts (names, sort)
 
def FreshConst (sort, prefix="c")
 
def Var (idx, s)
 
def RealVar (idx, ctx=None)
 
def RealVarVector (n, ctx=None)
 
def is_bool (a)
 
def is_true (a)
 
def is_false (a)
 
def is_and (a)
 
def is_or (a)
 
def is_implies (a)
 
def is_not (a)
 
def is_eq (a)
 
def is_distinct (a)
 
def BoolSort (ctx=None)
 
def BoolVal (val, ctx=None)
 
def Bool (name, ctx=None)
 
def Bools (names, ctx=None)
 
def BoolVector (prefix, sz, ctx=None)
 
def FreshBool (prefix="b", ctx=None)
 
def Implies (a, b, ctx=None)
 
def Xor (a, b, ctx=None)
 
def Not (a, ctx=None)
 
def mk_not (a)
 
def And (*args)
 
def Or (*args)
 
def is_pattern (a)
 
def MultiPattern (*args)
 
def is_quantifier (a)
 
def ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
 
def Lambda (vs, body)
 
def is_arith_sort (s)
 
def is_arith (a)
 
def is_int (a)
 
def is_real (a)
 
def is_int_value (a)
 
def is_rational_value (a)
 
def is_algebraic_value (a)
 
def is_add (a)
 
def is_mul (a)
 
def is_sub (a)
 
def is_div (a)
 
def is_idiv (a)
 
def is_mod (a)
 
def is_le (a)
 
def is_lt (a)
 
def is_ge (a)
 
def is_gt (a)
 
def is_is_int (a)
 
def is_to_real (a)
 
def is_to_int (a)
 
def IntSort (ctx=None)
 
def RealSort (ctx=None)
 
def IntVal (val, ctx=None)
 
def RealVal (val, ctx=None)
 
def RatVal (a, b, ctx=None)
 
def Q (a, b, ctx=None)
 
def Int (name, ctx=None)
 
def Ints (names, ctx=None)
 
def IntVector (prefix, sz, ctx=None)
 
def FreshInt (prefix="x", ctx=None)
 
def Real (name, ctx=None)
 
def Reals (names, ctx=None)
 
def RealVector (prefix, sz, ctx=None)
 
def FreshReal (prefix="b", ctx=None)
 
def ToReal (a)
 
def ToInt (a)
 
def IsInt (a)
 
def Sqrt (a, ctx=None)
 
def Cbrt (a, ctx=None)
 
def is_bv_sort (s)
 
def is_bv (a)
 
def is_bv_value (a)
 
def BV2Int (a, is_signed=False)
 
def Int2BV (a, num_bits)
 
def BitVecSort (sz, ctx=None)
 
def BitVecVal (val, bv, ctx=None)
 
def BitVec (name, bv, ctx=None)
 
def BitVecs (names, bv, ctx=None)
 
def Concat (*args)
 
def Extract (high, low, a)
 
def ULE (a, b)
 
def ULT (a, b)
 
def UGE (a, b)
 
def UGT (a, b)
 
def UDiv (a, b)
 
def URem (a, b)
 
def SRem (a, b)
 
def LShR (a, b)
 
def RotateLeft (a, b)
 
def RotateRight (a, b)
 
def SignExt (n, a)
 
def ZeroExt (n, a)
 
def RepeatBitVec (n, a)
 
def BVRedAnd (a)
 
def BVRedOr (a)
 
def BVAddNoOverflow (a, b, signed)
 
def BVAddNoUnderflow (a, b)
 
def BVSubNoOverflow (a, b)
 
def BVSubNoUnderflow (a, b, signed)
 
def BVSDivNoOverflow (a, b)
 
def BVSNegNoOverflow (a)
 
def BVMulNoOverflow (a, b, signed)
 
def BVMulNoUnderflow (a, b)
 
def is_array_sort (a)
 
def is_array (a)
 
def is_const_array (a)
 
def is_K (a)
 
def is_map (a)
 
def is_default (a)
 
def get_map_func (a)
 
def ArraySort (*sig)
 
def Array (name, *sorts)
 
def Update (a, *args)
 
def Default (a)
 
def Store (a, *args)
 
def Select (a, *args)
 
def Map (f, *args)
 
def K (dom, v)
 
def Ext (a, b)
 
def SetHasSize (a, k)
 
def is_select (a)
 
def is_store (a)
 
def SetSort (s)
 Sets. More...
 
def EmptySet (s)
 
def FullSet (s)
 
def SetUnion (*args)
 
def SetIntersect (*args)
 
def SetAdd (s, e)
 
def SetDel (s, e)
 
def SetComplement (s)
 
def SetDifference (a, b)
 
def IsMember (e, s)
 
def IsSubset (a, b)
 
def CreateDatatypes (*ds)
 
def 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 Abs (arg)
 
def AtMost (*args)
 
def AtLeast (*args)
 
def PbLe (args, k)
 
def PbGe (args, k)
 
def PbEq (args, k, ctx=None)
 
def solve (*args, **keywords)
 
def solve_using (s, *args, **keywords)
 
def prove (claim, show=False, **keywords)
 
def parse_smt2_string (s, sorts={}, decls={}, ctx=None)
 
def parse_smt2_file (f, sorts={}, decls={}, ctx=None)
 
def get_default_rounding_mode (ctx=None)
 
def set_default_rounding_mode (rm, ctx=None)
 
def get_default_fp_sort (ctx=None)
 
def set_default_fp_sort (ebits, sbits, ctx=None)
 
def Float16 (ctx=None)
 
def FloatHalf (ctx=None)
 
def Float32 (ctx=None)
 
def FloatSingle (ctx=None)
 
def Float64 (ctx=None)
 
def FloatDouble (ctx=None)
 
def Float128 (ctx=None)
 
def FloatQuadruple (ctx=None)
 
def is_fp_sort (s)
 
def is_fprm_sort (s)
 
def RoundNearestTiesToEven (ctx=None)
 
def RNE (ctx=None)
 
def RoundNearestTiesToAway (ctx=None)
 
def RNA (ctx=None)
 
def RoundTowardPositive (ctx=None)
 
def RTP (ctx=None)
 
def RoundTowardNegative (ctx=None)
 
def RTN (ctx=None)
 
def RoundTowardZero (ctx=None)
 
def RTZ (ctx=None)
 
def is_fprm (a)
 
def is_fprm_value (a)
 
def is_fp (a)
 
def is_fp_value (a)
 
def FPSort (ebits, sbits, ctx=None)
 
def fpNaN (s)
 
def fpPlusInfinity (s)
 
def fpMinusInfinity (s)
 
def fpInfinity (s, negative)
 
def fpPlusZero (s)
 
def fpMinusZero (s)
 
def fpZero (s, negative)
 
def FPVal (sig, exp=None, fps=None, ctx=None)
 
def FP (name, fpsort, ctx=None)
 
def FPs (names, fpsort, ctx=None)
 
def fpAbs (a, ctx=None)
 
def fpNeg (a, ctx=None)
 
def fpAdd (rm, a, b, ctx=None)
 
def fpSub (rm, a, b, ctx=None)
 
def fpMul (rm, a, b, ctx=None)
 
def fpDiv (rm, a, b, ctx=None)
 
def fpRem (a, b, ctx=None)
 
def fpMin (a, b, ctx=None)
 
def fpMax (a, b, ctx=None)
 
def fpFMA (rm, a, b, c, ctx=None)
 
def fpSqrt (rm, a, ctx=None)
 
def fpRoundToIntegral (rm, a, ctx=None)
 
def fpIsNaN (a, ctx=None)
 
def fpIsInf (a, ctx=None)
 
def fpIsZero (a, ctx=None)
 
def fpIsNormal (a, ctx=None)
 
def fpIsSubnormal (a, ctx=None)
 
def fpIsNegative (a, ctx=None)
 
def fpIsPositive (a, ctx=None)
 
def fpLT (a, b, ctx=None)
 
def fpLEQ (a, b, ctx=None)
 
def fpGT (a, b, ctx=None)
 
def fpGEQ (a, b, ctx=None)
 
def fpEQ (a, b, ctx=None)
 
def fpNEQ (a, b, ctx=None)
 
def fpFP (sgn, exp, sig, ctx=None)
 
def fpToFP (a1, a2=None, a3=None, ctx=None)
 
def fpBVToFP (v, sort, ctx=None)
 
def fpFPToFP (rm, v, sort, ctx=None)
 
def fpRealToFP (rm, v, sort, ctx=None)
 
def fpSignedToFP (rm, v, sort, ctx=None)
 
def fpUnsignedToFP (rm, v, sort, ctx=None)
 
def fpToFPUnsigned (rm, x, s, ctx=None)
 
def fpToSBV (rm, x, s, ctx=None)
 
def fpToUBV (rm, x, s, ctx=None)
 
def fpToReal (x, ctx=None)
 
def fpToIEEEBV (x, ctx=None)
 
def StringSort (ctx=None)
 
def CharSort (ctx=None)
 
def SeqSort (s)
 
def CharVal (ch, ctx=None)
 
def CharFromBv (ch, ctx=None)
 
def CharToBv (ch, ctx=None)
 
def CharToInt (ch, ctx=None)
 
def CharIsDigit (ch, ctx=None)
 
def is_seq (a)
 
def is_string (a)
 
def is_string_value (a)
 
def StringVal (s, ctx=None)
 
def String (name, ctx=None)
 
def Strings (names, ctx=None)
 
def SubString (s, offset, length)
 
def SubSeq (s, offset, length)
 
def Empty (s)
 
def Full (s)
 
def Unit (a)
 
def PrefixOf (a, b)
 
def SuffixOf (a, b)
 
def Contains (a, b)
 
def Replace (s, src, dst)
 
def IndexOf (s, substr, offset=None)
 
def LastIndexOf (s, substr)
 
def Length (s)
 
def StrToInt (s)
 
def IntToStr (s)
 
def StrToCode (s)
 
def StrFromCode (c)
 
def Re (s, ctx=None)
 
def ReSort (s)
 
def is_re (s)
 
def InRe (s, re)
 
def Union (*args)
 
def Intersect (*args)
 
def Plus (re)
 
def Option (re)
 
def Complement (re)
 
def Star (re)
 
def Loop (re, lo, hi=0)
 
def Range (lo, hi, ctx=None)
 
def Diff (a, b, ctx=None)
 
def AllChar (regex_sort, ctx=None)
 
def PartialOrder (a, index)
 
def LinearOrder (a, index)
 
def TreeOrder (a, index)
 
def PiecewiseLinearOrder (a, index)
 
def TransitiveClosure (f)
 
def ensure_prop_closures ()
 
def user_prop_push (ctx, cb)
 
def user_prop_pop (ctx, cb, num_scopes)
 
def user_prop_fresh (id, ctx)
 
def to_Ast (ptr)
 
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

◆ Abs()

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

Definition at line 8854 of file z3py.py.

8854 def Abs(arg):
8855  """Create the absolute value of an arithmetic expression"""
8856  return If(arg > 0, arg, -arg)
8857 
8858 

◆ AllChar()

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

Definition at line 11201 of file z3py.py.

11201 def AllChar(regex_sort, ctx=None):
11202  """Create a regular expression that accepts all single character strings
11203  """
11204  return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
11205 
11206 # Special Relations
11207 
11208 

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

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

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

◆ AndThen()

def z3py.AndThen ( ts,
**  ks 
)
Return a tactic that applies the tactics in `*ts` in sequence.

>>> x, y = Ints('x y')
>>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
>>> t(And(x == 0, y > x + 1))
[[Not(y <= 1)]]
>>> t(And(x == 0, y > x + 1)).as_expr()
Not(y <= 1)

Definition at line 8244 of file z3py.py.

8244 def AndThen(*ts, **ks):
8245  """Return a tactic that applies the tactics in `*ts` in sequence.
8246 
8247  >>> x, y = Ints('x y')
8248  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
8249  >>> t(And(x == 0, y > x + 1))
8250  [[Not(y <= 1)]]
8251  >>> t(And(x == 0, y > x + 1)).as_expr()
8252  Not(y <= 1)
8253  """
8254  if z3_debug():
8255  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8256  ctx = ks.get("ctx", None)
8257  num = len(ts)
8258  r = ts[0]
8259  for i in range(num - 1):
8260  r = _and_then(r, ts[i + 1], ctx)
8261  return r
8262 
8263 

Referenced by Then().

◆ append_log()

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

Definition at line 119 of file z3py.py.

119 def append_log(s):
120  """Append user-defined string to interaction log. """
121  Z3_append_log(s)
122 
123 

◆ args2params()

def z3py.args2params (   arguments,
  keywords,
  ctx = None 
)
Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'

>>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
(params model true relevancy 2 elim_and true)

Definition at line 5447 of file z3py.py.

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

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

◆ Array()

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

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

Definition at line 4718 of file z3py.py.

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

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

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

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

◆ AtLeast()

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

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

Definition at line 8877 of file z3py.py.

8877 def AtLeast(*args):
8878  """Create an at-most Pseudo-Boolean k constraint.
8879 
8880  >>> a, b, c = Bools('a b c')
8881  >>> f = AtLeast(a, b, c, 2)
8882  """
8883  args = _get_args(args)
8884  if z3_debug():
8885  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8886  ctx = _ctx_from_ast_arg_list(args)
8887  if z3_debug():
8888  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8889  args1 = _coerce_expr_list(args[:-1], ctx)
8890  k = args[-1]
8891  _args, sz = _to_ast_array(args1)
8892  return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
8893 
8894 

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

8859 def AtMost(*args):
8860  """Create an at-most Pseudo-Boolean k constraint.
8861 
8862  >>> a, b, c = Bools('a b c')
8863  >>> f = AtMost(a, b, c, 2)
8864  """
8865  args = _get_args(args)
8866  if z3_debug():
8867  _z3_assert(len(args) > 1, "Non empty list of arguments expected")
8868  ctx = _ctx_from_ast_arg_list(args)
8869  if z3_debug():
8870  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
8871  args1 = _coerce_expr_list(args[:-1], ctx)
8872  k = args[-1]
8873  _args, sz = _to_ast_array(args1)
8874  return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
8875 
8876 

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

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

Referenced by BitVecs().

◆ BitVecs()

def z3py.BitVecs (   names,
  bv,
  ctx = None 
)
Return a tuple of bit-vector constants of size bv.

>>> x, y, z = BitVecs('x y z', 16)
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> Sum(x, y, z)
0 + x + y + z
>>> Product(x, y, z)
1*x*y*z
>>> simplify(Product(x, y, z))
x*y*z

Definition at line 4046 of file z3py.py.

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

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

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

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

◆ BitVecVal()

def z3py.BitVecVal (   val,
  bv,
  ctx = None 
)
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.

>>> v = BitVecVal(10, 32)
>>> v
10
>>> print("0x%.8x" % v.as_long())
0x0000000a

Definition at line 4005 of file z3py.py.

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

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

1713 def Bool(name, ctx=None):
1714  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1715 
1716  >>> p = Bool('p')
1717  >>> q = Bool('q')
1718  >>> And(p, q)
1719  And(p, q)
1720  """
1721  ctx = _get_ctx(ctx)
1722  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1723 
1724 

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

◆ Bools()

def z3py.Bools (   names,
  ctx = None 
)
Return a tuple of Boolean constants.

`names` is a single string containing all names separated by blank spaces.
If `ctx=None`, then the global context is used.

>>> p, q, r = Bools('p q r')
>>> And(p, Or(q, r))
And(p, Or(q, r))

Definition at line 1725 of file z3py.py.

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

◆ BoolSort()

def z3py.BoolSort (   ctx = None)
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.

>>> BoolSort()
Bool
>>> p = Const('p', BoolSort())
>>> is_bool(p)
True
>>> r = Function('r', IntSort(), IntSort(), BoolSort())
>>> r(0, 1)
r(0, 1)
>>> is_bool(r(0, 1))
True

Definition at line 1676 of file z3py.py.

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

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

◆ BoolVal()

def z3py.BoolVal (   val,
  ctx = None 
)
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.

>>> BoolVal(True)
True
>>> is_true(BoolVal(True))
True
>>> is_true(True)
False
>>> is_false(BoolVal(False))
True

Definition at line 1694 of file z3py.py.

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

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

◆ BoolVector()

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

The constants are named using the given prefix.
If `ctx=None`, then the global context is used.

>>> P = BoolVector('p', 3)
>>> P
[p__0, p__1, p__2]
>>> And(P)
And(p__0, p__1, p__2)

Definition at line 1741 of file z3py.py.

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

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

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

◆ BVAddNoOverflow()

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

Definition at line 4444 of file z3py.py.

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

◆ BVAddNoUnderflow()

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

Definition at line 4451 of file z3py.py.

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

◆ BVMulNoOverflow()

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

Definition at line 4486 of file z3py.py.

4486 def BVMulNoOverflow(a, b, signed):
4487  """A predicate the determines that bit-vector multiplication does not overflow"""
4488  _check_bv_args(a, b)
4489  a, b = _coerce_exprs(a, b)
4490  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4491 
4492 

◆ BVMulNoUnderflow()

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

Definition at line 4493 of file z3py.py.

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

◆ BVRedAnd()

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

Definition at line 4430 of file z3py.py.

4430 def BVRedAnd(a):
4431  """Return the reduction-and expression of `a`."""
4432  if z3_debug():
4433  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4434  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4435 
4436 

◆ BVRedOr()

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

Definition at line 4437 of file z3py.py.

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

◆ BVSDivNoOverflow()

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

Definition at line 4472 of file z3py.py.

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

◆ BVSNegNoOverflow()

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

Definition at line 4479 of file z3py.py.

4479 def BVSNegNoOverflow(a):
4480  """A predicate the determines that bit-vector unary negation does not overflow"""
4481  if z3_debug():
4482  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4483  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4484 
4485 

◆ BVSubNoOverflow()

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

Definition at line 4458 of file z3py.py.

4458 def BVSubNoOverflow(a, b):
4459  """A predicate the determines that bit-vector subtraction does not overflow"""
4460  _check_bv_args(a, b)
4461  a, b = _coerce_exprs(a, b)
4462  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4463 
4464 

◆ BVSubNoUnderflow()

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

Definition at line 4465 of file z3py.py.

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

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

3409 def Cbrt(a, ctx=None):
3410  """ Return a Z3 expression which represents the cubic root of a.
3411 
3412  >>> x = Real('x')
3413  >>> Cbrt(x)
3414  x**(1/3)
3415  """
3416  if not is_expr(a):
3417  ctx = _get_ctx(ctx)
3418  a = RealVal(a, ctx)
3419  return a ** "1/3"
3420 

◆ CharFromBv()

def z3py.CharFromBv (   ch,
  ctx = None 
)

Definition at line 10759 of file z3py.py.

10759 def CharFromBv(ch, ctx=None):
10760  if not is_expr(ch):
10761  raise Z3Expression("Bit-vector expression needed")
10762  return _to_expr_ref(Z3_mk_char_from_bv(ch.ctx_ref(), ch.as_ast()), ch.ctx)
10763 

◆ CharIsDigit()

def z3py.CharIsDigit (   ch,
  ctx = None 
)

Definition at line 10772 of file z3py.py.

10772 def CharIsDigit(ch, ctx=None):
10773  ch = _coerce_char(ch, ctx)
10774  return ch.is_digit()
10775 

◆ CharSort()

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

Definition at line 10658 of file z3py.py.

10658 def CharSort(ctx=None):
10659  """Create a character sort
10660  >>> ch = CharSort()
10661  >>> print(ch)
10662  Char
10663  """
10664  ctx = _get_ctx(ctx)
10665  return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
10666 
10667 

Referenced by Context.mkCharSort().

◆ CharToBv()

def z3py.CharToBv (   ch,
  ctx = None 
)

Definition at line 10764 of file z3py.py.

10764 def CharToBv(ch, ctx=None):
10765  ch = _coerce_char(ch, ctx)
10766  return ch.to_bv()
10767 

◆ CharToInt()

def z3py.CharToInt (   ch,
  ctx = None 
)

Definition at line 10768 of file z3py.py.

10768 def CharToInt(ch, ctx=None):
10769  ch = _coerce_char(ch, ctx)
10770  return ch.to_int()
10771 

◆ CharVal()

def z3py.CharVal (   ch,
  ctx = None 
)

Definition at line 10751 of file z3py.py.

10751 def CharVal(ch, ctx=None):
10752  ctx = _get_ctx(ctx)
10753  if isinstance(ch, str):
10754  ch = ord(ch)
10755  if not isinstance(ch, int):
10756  raise Z3Exception("character value should be an ordinal")
10757  return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
10758 

Referenced by SeqRef.__gt__().

◆ Complement()

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

Definition at line 11153 of file z3py.py.

11153 def Complement(re):
11154  """Create the complement regular expression."""
11155  return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
11156 
11157 

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

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

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

◆ Cond()

def z3py.Cond (   p,
  t1,
  t2,
  ctx = None 
)
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.

>>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))

Definition at line 8701 of file z3py.py.

8701 def Cond(p, t1, t2, ctx=None):
8702  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8703 
8704  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8705  """
8706  p = _to_probe(p, ctx)
8707  t1 = _to_tactic(t1, ctx)
8708  t2 = _to_tactic(t2, ctx)
8709  return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8710 

Referenced by If().

◆ Const()

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

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

Definition at line 1426 of file z3py.py.

1426 def Const(name, sort):
1427  """Create a constant of the given sort.
1428 
1429  >>> Const('x', IntSort())
1430  x
1431  """
1432  if z3_debug():
1433  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1434  ctx = sort.ctx
1435  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1436 
1437 

Referenced by Consts().

◆ Consts()

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

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

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

Definition at line 1438 of file z3py.py.

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

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

10928 def Contains(a, b):
10929  """Check if 'a' contains 'b'
10930  >>> s1 = Contains("abc", "ab")
10931  >>> simplify(s1)
10932  True
10933  >>> s2 = Contains("abc", "bc")
10934  >>> simplify(s2)
10935  True
10936  >>> x, y, z = Strings('x y z')
10937  >>> s3 = Contains(Concat(x,y,z), y)
10938  >>> simplify(s3)
10939  True
10940  """
10941  ctx = _get_ctx2(a, b)
10942  a = _coerce_seq(a, ctx)
10943  b = _coerce_seq(b, ctx)
10944  return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10945 
10946 

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

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

Referenced by Datatype.create().

◆ DeclareSort()

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

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

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

Definition at line 687 of file z3py.py.

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

◆ Default()

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

Definition at line 4764 of file z3py.py.

4764 def Default(a):
4765  """ Return a default value for array expression.
4766  >>> b = K(IntSort(), 1)
4767  >>> prove(Default(b) == 1)
4768  proved
4769  """
4770  if z3_debug():
4771  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4772  return a.default()
4773 
4774 

◆ describe_probes()

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

Definition at line 8622 of file z3py.py.

8622 def describe_probes():
8623  """Display a (tabular) description of all available probes in Z3."""
8624  if in_html_mode():
8625  even = True
8626  print('<table border="1" cellpadding="2" cellspacing="0">')
8627  for p in probes():
8628  if even:
8629  print('<tr style="background-color:#CFCFCF">')
8630  even = False
8631  else:
8632  print("<tr>")
8633  even = True
8634  print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
8635  print("</table>")
8636  else:
8637  for p in probes():
8638  print("%s : %s" % (p, probe_description(p)))
8639 
8640 

◆ describe_tactics()

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

Definition at line 8416 of file z3py.py.

8416 def describe_tactics():
8417  """Display a (tabular) description of all available tactics in Z3."""
8418  if in_html_mode():
8419  even = True
8420  print('<table border="1" cellpadding="2" cellspacing="0">')
8421  for t in tactics():
8422  if even:
8423  print('<tr style="background-color:#CFCFCF">')
8424  even = False
8425  else:
8426  print("<tr>")
8427  even = True
8428  print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
8429  print("</table>")
8430  else:
8431  for t in tactics():
8432  print("%s : %s" % (t, tactic_description(t)))
8433 
8434 

◆ deserialize()

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

Definition at line 1113 of file z3py.py.

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

◆ Diff()

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

Definition at line 11196 of file z3py.py.

11196 def Diff(a, b, ctx=None):
11197  """Create the difference regular epression
11198  """
11199  return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)
11200 

◆ disable_trace()

def z3py.disable_trace (   msg)

Definition at line 79 of file z3py.py.

79 def disable_trace(msg):
80  Z3_disable_trace(msg)
81 
82 

◆ DisjointSum()

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

Definition at line 5356 of file z3py.py.

5356 def DisjointSum(name, sorts, ctx=None):
5357  """Create a named tagged union sort base on a set of underlying sorts
5358  Example:
5359  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5360  """
5361  sum = Datatype(name, ctx)
5362  for i in range(len(sorts)):
5363  sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
5364  sum = sum.create()
5365  return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
5366 
5367 

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

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

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

10858 def Empty(s):
10859  """Create the empty sequence of the given sort
10860  >>> e = Empty(StringSort())
10861  >>> e2 = StringVal("")
10862  >>> print(e.eq(e2))
10863  True
10864  >>> e3 = Empty(SeqSort(IntSort()))
10865  >>> print(e3)
10866  Empty(Seq(Int))
10867  >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10868  >>> print(e4)
10869  Empty(ReSort(Seq(Int)))
10870  """
10871  if isinstance(s, SeqSortRef):
10872  return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
10873  if isinstance(s, ReSortRef):
10874  return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
10875  raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
10876 
10877 

◆ EmptySet()

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

Definition at line 4907 of file z3py.py.

4907 def EmptySet(s):
4908  """Create the empty set
4909  >>> EmptySet(IntSort())
4910  K(Int, False)
4911  """
4912  ctx = s.ctx
4913  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4914 
4915 

◆ enable_trace()

def z3py.enable_trace (   msg)

Definition at line 75 of file z3py.py.

75 def enable_trace(msg):
76  Z3_enable_trace(msg)
77 
78 

◆ ensure_prop_closures()

def z3py.ensure_prop_closures ( )

Definition at line 11272 of file z3py.py.

11272 def ensure_prop_closures():
11273  global _prop_closures
11274  if _prop_closures is None:
11275  _prop_closures = PropClosures()
11276 
11277 

Referenced by UserPropagateBase.__init__().

◆ EnumSort()

def z3py.EnumSort (   name,
  values,
  ctx = None 
)
Return a new enumeration sort named `name` containing the given values.

The result is a pair (sort, list of constants).
Example:
    >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])

Definition at line 5368 of file z3py.py.

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

Referenced by Context.MkEnumSort().

◆ eq()

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

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

Definition at line 466 of file z3py.py.

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

Referenced by substitute().

◆ Exists()

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

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


>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = Exists([x, y], f(x, y) >= x, skid="foo")
>>> q
Exists([x, y], f(x, y) >= x)
>>> is_quantifier(q)
True
>>> r = Tactic('nnf')(q).as_expr()
>>> is_quantifier(r)
False

Definition at line 2225 of file z3py.py.

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

Referenced by Fixedpoint.abstract().

◆ Ext()

def z3py.Ext (   a,
  b 
)
Return extensionality index for one-dimensional arrays.
>> a, b = Consts('a b', SetSort(IntSort()))
>> Ext(a, b)
Ext(a, b)

Definition at line 4853 of file z3py.py.

4853 def Ext(a, b):
4854  """Return extensionality index for one-dimensional arrays.
4855  >> a, b = Consts('a b', SetSort(IntSort()))
4856  >> Ext(a, b)
4857  Ext(a, b)
4858  """
4859  ctx = a.ctx
4860  if z3_debug():
4861  _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
4862  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4863 
4864 

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

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

Referenced by SubSeq(), and SubString().

◆ FailIf()

def z3py.FailIf (   p,
  ctx = None 
)
Return a tactic that fails if the probe `p` evaluates to true.
Otherwise, it returns the input goal unmodified.

In the following example, the tactic applies 'simplify' if and only if there are
more than 2 constraints in the goal.

>>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(y > 0)
>>> t(g)
[[x > 0, y > 0]]
>>> g.add(x == y + 1)
>>> t(g)
[[Not(x <= 0), Not(y <= 0), x == 1 + y]]

Definition at line 8659 of file z3py.py.

8659 def FailIf(p, ctx=None):
8660  """Return a tactic that fails if the probe `p` evaluates to true.
8661  Otherwise, it returns the input goal unmodified.
8662 
8663  In the following example, the tactic applies 'simplify' if and only if there are
8664  more than 2 constraints in the goal.
8665 
8666  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8667  >>> x, y = Ints('x y')
8668  >>> g = Goal()
8669  >>> g.add(x > 0)
8670  >>> g.add(y > 0)
8671  >>> t(g)
8672  [[x > 0, y > 0]]
8673  >>> g.add(x == y + 1)
8674  >>> t(g)
8675  [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8676  """
8677  p = _to_probe(p, ctx)
8678  return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8679 
8680 

◆ FiniteDomainSort()

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

Definition at line 7663 of file z3py.py.

7663 def FiniteDomainSort(name, sz, ctx=None):
7664  """Create a named finite domain sort of a given size sz"""
7665  if not isinstance(name, Symbol):
7666  name = to_symbol(name)
7667  ctx = _get_ctx(ctx)
7668  return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7669 
7670 

Referenced by Context.MkFiniteDomainSort().

◆ FiniteDomainVal()

def z3py.FiniteDomainVal (   val,
  sort,
  ctx = None 
)
Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.

>>> s = FiniteDomainSort('S', 256)
>>> FiniteDomainVal(255, s)
255
>>> FiniteDomainVal('100', s)
100

Definition at line 7733 of file z3py.py.

7733 def FiniteDomainVal(val, sort, ctx=None):
7734  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7735 
7736  >>> s = FiniteDomainSort('S', 256)
7737  >>> FiniteDomainVal(255, s)
7738  255
7739  >>> FiniteDomainVal('100', s)
7740  100
7741  """
7742  if z3_debug():
7743  _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
7744  ctx = sort.ctx
7745  return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7746 
7747 

◆ Float128()

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

Definition at line 9343 of file z3py.py.

9343 def Float128(ctx=None):
9344  """Floating-point 128-bit (quadruple) sort."""
9345  ctx = _get_ctx(ctx)
9346  return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
9347 
9348 

◆ Float16()

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

Definition at line 9307 of file z3py.py.

9307 def Float16(ctx=None):
9308  """Floating-point 16-bit (half) sort."""
9309  ctx = _get_ctx(ctx)
9310  return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
9311 
9312 

◆ Float32()

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

Definition at line 9319 of file z3py.py.

9319 def Float32(ctx=None):
9320  """Floating-point 32-bit (single) sort."""
9321  ctx = _get_ctx(ctx)
9322  return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
9323 
9324 

◆ Float64()

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

Definition at line 9331 of file z3py.py.

9331 def Float64(ctx=None):
9332  """Floating-point 64-bit (double) sort."""
9333  ctx = _get_ctx(ctx)
9334  return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
9335 
9336 

◆ FloatDouble()

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

Definition at line 9337 of file z3py.py.

9337 def FloatDouble(ctx=None):
9338  """Floating-point 64-bit (double) sort."""
9339  ctx = _get_ctx(ctx)
9340  return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
9341 
9342 

◆ FloatHalf()

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

Definition at line 9313 of file z3py.py.

9313 def FloatHalf(ctx=None):
9314  """Floating-point 16-bit (half) sort."""
9315  ctx = _get_ctx(ctx)
9316  return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
9317 
9318 

◆ FloatQuadruple()

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

Definition at line 9349 of file z3py.py.

9349 def FloatQuadruple(ctx=None):
9350  """Floating-point 128-bit (quadruple) sort."""
9351  ctx = _get_ctx(ctx)
9352  return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
9353 
9354 

◆ FloatSingle()

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

Definition at line 9325 of file z3py.py.

9325 def FloatSingle(ctx=None):
9326  """Floating-point 32-bit (single) sort."""
9327  ctx = _get_ctx(ctx)
9328  return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
9329 
9330 

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

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

Referenced by Fixedpoint.abstract().

◆ FP()

def z3py.FP (   name,
  fpsort,
  ctx = None 
)
Return a floating-point constant named `name`.
`fpsort` is the floating-point sort.
If `ctx=None`, then the global context is used.

>>> x  = FP('x', FPSort(8, 24))
>>> is_fp(x)
True
>>> x.ebits()
8
>>> x.sort()
FPSort(8, 24)
>>> word = FPSort(8, 24)
>>> x2 = FP('x', word)
>>> eq(x, x2)
True

Definition at line 9975 of file z3py.py.

9975 def FP(name, fpsort, ctx=None):
9976  """Return a floating-point constant named `name`.
9977  `fpsort` is the floating-point sort.
9978  If `ctx=None`, then the global context is used.
9979 
9980  >>> x = FP('x', FPSort(8, 24))
9981  >>> is_fp(x)
9982  True
9983  >>> x.ebits()
9984  8
9985  >>> x.sort()
9986  FPSort(8, 24)
9987  >>> word = FPSort(8, 24)
9988  >>> x2 = FP('x', word)
9989  >>> eq(x, x2)
9990  True
9991  """
9992  if isinstance(fpsort, FPSortRef) and ctx is None:
9993  ctx = fpsort.ctx
9994  else:
9995  ctx = _get_ctx(ctx)
9996  return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
9997 
9998 

Referenced by FPs().

◆ fpAbs()

def z3py.fpAbs (   a,
  ctx = None 
)
Create a Z3 floating-point absolute value expression.

>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FPVal(1.0, s)
>>> fpAbs(x)
fpAbs(1)
>>> y = FPVal(-20.0, s)
>>> y
-1.25*(2**4)
>>> fpAbs(y)
fpAbs(-1.25*(2**4))
>>> fpAbs(-1.25*(2**4))
fpAbs(-1.25*(2**4))
>>> fpAbs(x).sort()
FPSort(8, 24)

Definition at line 10018 of file z3py.py.

10018 def fpAbs(a, ctx=None):
10019  """Create a Z3 floating-point absolute value expression.
10020 
10021  >>> s = FPSort(8, 24)
10022  >>> rm = RNE()
10023  >>> x = FPVal(1.0, s)
10024  >>> fpAbs(x)
10025  fpAbs(1)
10026  >>> y = FPVal(-20.0, s)
10027  >>> y
10028  -1.25*(2**4)
10029  >>> fpAbs(y)
10030  fpAbs(-1.25*(2**4))
10031  >>> fpAbs(-1.25*(2**4))
10032  fpAbs(-1.25*(2**4))
10033  >>> fpAbs(x).sort()
10034  FPSort(8, 24)
10035  """
10036  ctx = _get_ctx(ctx)
10037  [a] = _coerce_fp_expr_list([a], ctx)
10038  return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
10039 
10040 

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

10109 def fpAdd(rm, a, b, ctx=None):
10110  """Create a Z3 floating-point addition expression.
10111 
10112  >>> s = FPSort(8, 24)
10113  >>> rm = RNE()
10114  >>> x = FP('x', s)
10115  >>> y = FP('y', s)
10116  >>> fpAdd(rm, x, y)
10117  fpAdd(RNE(), x, y)
10118  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
10119  x + y
10120  >>> fpAdd(rm, x, y).sort()
10121  FPSort(8, 24)
10122  """
10123  return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
10124 
10125 

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

◆ fpBVToFP()

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

>>> x_bv = BitVecVal(0x3F800000, 32)
>>> x_fp = fpBVToFP(x_bv, Float32())
>>> x_fp
fpToFP(1065353216)
>>> simplify(x_fp)
1

Definition at line 10431 of file z3py.py.

10431 def fpBVToFP(v, sort, ctx=None):
10432  """Create a Z3 floating-point conversion expression that represents the
10433  conversion from a bit-vector term to a floating-point term.
10434 
10435  >>> x_bv = BitVecVal(0x3F800000, 32)
10436  >>> x_fp = fpBVToFP(x_bv, Float32())
10437  >>> x_fp
10438  fpToFP(1065353216)
10439  >>> simplify(x_fp)
10440  1
10441  """
10442  _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
10443  _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
10444  ctx = _get_ctx(ctx)
10445  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
10446 
10447 

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

10156 def fpDiv(rm, a, b, ctx=None):
10157  """Create a Z3 floating-point division expression.
10158 
10159  >>> s = FPSort(8, 24)
10160  >>> rm = RNE()
10161  >>> x = FP('x', s)
10162  >>> y = FP('y', s)
10163  >>> fpDiv(rm, x, y)
10164  fpDiv(RNE(), x, y)
10165  >>> fpDiv(rm, x, y).sort()
10166  FPSort(8, 24)
10167  """
10168  return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
10169 
10170 

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

◆ fpEQ()

def z3py.fpEQ (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `fpEQ(other, self)`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpEQ(x, y)
fpEQ(x, y)
>>> fpEQ(x, y).sexpr()
'(fp.eq x y)'

Definition at line 10339 of file z3py.py.

10339 def fpEQ(a, b, ctx=None):
10340  """Create the Z3 floating-point expression `fpEQ(other, self)`.
10341 
10342  >>> x, y = FPs('x y', FPSort(8, 24))
10343  >>> fpEQ(x, y)
10344  fpEQ(x, y)
10345  >>> fpEQ(x, y).sexpr()
10346  '(fp.eq x y)'
10347  """
10348  return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
10349 
10350 

Referenced by fpNEQ().

◆ fpFMA()

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

Definition at line 10215 of file z3py.py.

10215 def fpFMA(rm, a, b, c, ctx=None):
10216  """Create a Z3 floating-point fused multiply-add expression.
10217  """
10218  return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
10219 
10220 

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

10363 def fpFP(sgn, exp, sig, ctx=None):
10364  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
10365 
10366  >>> s = FPSort(8, 24)
10367  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
10368  >>> print(x)
10369  fpFP(1, 127, 4194304)
10370  >>> xv = FPVal(-1.5, s)
10371  >>> print(xv)
10372  -1.5
10373  >>> slvr = Solver()
10374  >>> slvr.add(fpEQ(x, xv))
10375  >>> slvr.check()
10376  sat
10377  >>> xv = FPVal(+1.5, s)
10378  >>> print(xv)
10379  1.5
10380  >>> slvr = Solver()
10381  >>> slvr.add(fpEQ(x, xv))
10382  >>> slvr.check()
10383  unsat
10384  """
10385  _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
10386  _z3_assert(sgn.sort().size() == 1, "sort mismatch")
10387  ctx = _get_ctx(ctx)
10388  _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
10389  return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
10390 
10391 

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

10448 def fpFPToFP(rm, v, sort, ctx=None):
10449  """Create a Z3 floating-point conversion expression that represents the
10450  conversion from a floating-point term to a floating-point term of different precision.
10451 
10452  >>> x_sgl = FPVal(1.0, Float32())
10453  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
10454  >>> x_dbl
10455  fpToFP(RNE(), 1)
10456  >>> simplify(x_dbl)
10457  1
10458  >>> x_dbl.sort()
10459  FPSort(11, 53)
10460  """
10461  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10462  _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
10463  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10464  ctx = _get_ctx(ctx)
10465  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10466 
10467 

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

10327 def fpGEQ(a, b, ctx=None):
10328  """Create the Z3 floating-point expression `other >= self`.
10329 
10330  >>> x, y = FPs('x y', FPSort(8, 24))
10331  >>> fpGEQ(x, y)
10332  x >= y
10333  >>> (x >= y).sexpr()
10334  '(fp.geq x y)'
10335  """
10336  return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
10337 
10338 

Referenced by FPRef.__ge__().

◆ fpGT()

def z3py.fpGT (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `other > self`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGT(x, y)
x > y
>>> (x > y).sexpr()
'(fp.gt x y)'

Definition at line 10315 of file z3py.py.

10315 def fpGT(a, b, ctx=None):
10316  """Create the Z3 floating-point expression `other > self`.
10317 
10318  >>> x, y = FPs('x y', FPSort(8, 24))
10319  >>> fpGT(x, y)
10320  x > y
10321  >>> (x > y).sexpr()
10322  '(fp.gt x y)'
10323  """
10324  return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
10325 
10326 

Referenced by FPRef.__gt__().

◆ fpInfinity()

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

Definition at line 9903 of file z3py.py.

9903 def fpInfinity(s, negative):
9904  """Create a Z3 floating-point +oo or -oo term."""
9905  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9906  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9907  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
9908 
9909 

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

10245 def fpIsInf(a, ctx=None):
10246  """Create a Z3 floating-point isInfinite expression.
10247 
10248  >>> s = FPSort(8, 24)
10249  >>> x = FP('x', s)
10250  >>> fpIsInf(x)
10251  fpIsInf(x)
10252  """
10253  return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
10254 
10255 

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

10233 def fpIsNaN(a, ctx=None):
10234  """Create a Z3 floating-point isNaN expression.
10235 
10236  >>> s = FPSort(8, 24)
10237  >>> x = FP('x', s)
10238  >>> y = FP('y', s)
10239  >>> fpIsNaN(x)
10240  fpIsNaN(x)
10241  """
10242  return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
10243 
10244 

◆ fpIsNegative()

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

Definition at line 10274 of file z3py.py.

10274 def fpIsNegative(a, ctx=None):
10275  """Create a Z3 floating-point isNegative expression.
10276  """
10277  return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
10278 
10279 

◆ fpIsNormal()

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

Definition at line 10262 of file z3py.py.

10262 def fpIsNormal(a, ctx=None):
10263  """Create a Z3 floating-point isNormal expression.
10264  """
10265  return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
10266 
10267 

◆ fpIsPositive()

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

Definition at line 10280 of file z3py.py.

10280 def fpIsPositive(a, ctx=None):
10281  """Create a Z3 floating-point isPositive expression.
10282  """
10283  return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
10284 
10285 

◆ fpIsSubnormal()

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

Definition at line 10268 of file z3py.py.

10268 def fpIsSubnormal(a, ctx=None):
10269  """Create a Z3 floating-point isSubnormal expression.
10270  """
10271  return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
10272 
10273 

◆ fpIsZero()

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

Definition at line 10256 of file z3py.py.

10256 def fpIsZero(a, ctx=None):
10257  """Create a Z3 floating-point isZero expression.
10258  """
10259  return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
10260 
10261 

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

10303 def fpLEQ(a, b, ctx=None):
10304  """Create the Z3 floating-point expression `other <= self`.
10305 
10306  >>> x, y = FPs('x y', FPSort(8, 24))
10307  >>> fpLEQ(x, y)
10308  x <= y
10309  >>> (x <= y).sexpr()
10310  '(fp.leq x y)'
10311  """
10312  return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
10313 
10314 

Referenced by FPRef.__le__().

◆ fpLT()

def z3py.fpLT (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `other < self`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLT(x, y)
x < y
>>> (x < y).sexpr()
'(fp.lt x y)'

Definition at line 10291 of file z3py.py.

10291 def fpLT(a, b, ctx=None):
10292  """Create the Z3 floating-point expression `other < self`.
10293 
10294  >>> x, y = FPs('x y', FPSort(8, 24))
10295  >>> fpLT(x, y)
10296  x < y
10297  >>> (x < y).sexpr()
10298  '(fp.lt x y)'
10299  """
10300  return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
10301 
10302 

Referenced by FPRef.__lt__().

◆ fpMax()

def z3py.fpMax (   a,
  b,
  ctx = None 
)
Create a Z3 floating-point maximum expression.

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

Definition at line 10200 of file z3py.py.

10200 def fpMax(a, b, ctx=None):
10201  """Create a Z3 floating-point maximum expression.
10202 
10203  >>> s = FPSort(8, 24)
10204  >>> rm = RNE()
10205  >>> x = FP('x', s)
10206  >>> y = FP('y', s)
10207  >>> fpMax(x, y)
10208  fpMax(x, y)
10209  >>> fpMax(x, y).sort()
10210  FPSort(8, 24)
10211  """
10212  return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
10213 
10214 

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

10185 def fpMin(a, b, ctx=None):
10186  """Create a Z3 floating-point minimum expression.
10187 
10188  >>> s = FPSort(8, 24)
10189  >>> rm = RNE()
10190  >>> x = FP('x', s)
10191  >>> y = FP('y', s)
10192  >>> fpMin(x, y)
10193  fpMin(x, y)
10194  >>> fpMin(x, y).sort()
10195  FPSort(8, 24)
10196  """
10197  return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
10198 
10199 

◆ fpMinusInfinity()

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

Definition at line 9897 of file z3py.py.

9897 def fpMinusInfinity(s):
9898  """Create a Z3 floating-point -oo term."""
9899  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9900  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
9901 
9902 

Referenced by FPVal().

◆ fpMinusZero()

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

Definition at line 9916 of file z3py.py.

9916 def fpMinusZero(s):
9917  """Create a Z3 floating-point -0.0 term."""
9918  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9919  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
9920 
9921 

Referenced by FPVal().

◆ fpMul()

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

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

Definition at line 10141 of file z3py.py.

10141 def fpMul(rm, a, b, ctx=None):
10142  """Create a Z3 floating-point multiplication expression.
10143 
10144  >>> s = FPSort(8, 24)
10145  >>> rm = RNE()
10146  >>> x = FP('x', s)
10147  >>> y = FP('y', s)
10148  >>> fpMul(rm, x, y)
10149  fpMul(RNE(), x, y)
10150  >>> fpMul(rm, x, y).sort()
10151  FPSort(8, 24)
10152  """
10153  return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
10154 
10155 

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

◆ fpNaN()

def z3py.fpNaN (   s)
Create a Z3 floating-point NaN term.

>>> s = FPSort(8, 24)
>>> set_fpa_pretty(True)
>>> fpNaN(s)
NaN
>>> pb = get_fpa_pretty()
>>> set_fpa_pretty(False)
>>> fpNaN(s)
fpNaN(FPSort(8, 24))
>>> set_fpa_pretty(pb)

Definition at line 9863 of file z3py.py.

9863 def fpNaN(s):
9864  """Create a Z3 floating-point NaN term.
9865 
9866  >>> s = FPSort(8, 24)
9867  >>> set_fpa_pretty(True)
9868  >>> fpNaN(s)
9869  NaN
9870  >>> pb = get_fpa_pretty()
9871  >>> set_fpa_pretty(False)
9872  >>> fpNaN(s)
9873  fpNaN(FPSort(8, 24))
9874  >>> set_fpa_pretty(pb)
9875  """
9876  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9877  return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
9878 
9879 

Referenced by FPVal().

◆ fpNeg()

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

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

Definition at line 10041 of file z3py.py.

10041 def fpNeg(a, ctx=None):
10042  """Create a Z3 floating-point addition expression.
10043 
10044  >>> s = FPSort(8, 24)
10045  >>> rm = RNE()
10046  >>> x = FP('x', s)
10047  >>> fpNeg(x)
10048  -x
10049  >>> fpNeg(x).sort()
10050  FPSort(8, 24)
10051  """
10052  ctx = _get_ctx(ctx)
10053  [a] = _coerce_fp_expr_list([a], ctx)
10054  return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
10055 
10056 

Referenced by FPRef.__neg__().

◆ fpNEQ()

def z3py.fpNEQ (   a,
  b,
  ctx = None 
)
Create the Z3 floating-point expression `Not(fpEQ(other, self))`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpNEQ(x, y)
Not(fpEQ(x, y))
>>> (x != y).sexpr()
'(distinct x y)'

Definition at line 10351 of file z3py.py.

10351 def fpNEQ(a, b, ctx=None):
10352  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
10353 
10354  >>> x, y = FPs('x y', FPSort(8, 24))
10355  >>> fpNEQ(x, y)
10356  Not(fpEQ(x, y))
10357  >>> (x != y).sexpr()
10358  '(distinct x y)'
10359  """
10360  return Not(fpEQ(a, b, ctx))
10361 
10362 

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

9880 def fpPlusInfinity(s):
9881  """Create a Z3 floating-point +oo term.
9882 
9883  >>> s = FPSort(8, 24)
9884  >>> pb = get_fpa_pretty()
9885  >>> set_fpa_pretty(True)
9886  >>> fpPlusInfinity(s)
9887  +oo
9888  >>> set_fpa_pretty(False)
9889  >>> fpPlusInfinity(s)
9890  fpPlusInfinity(FPSort(8, 24))
9891  >>> set_fpa_pretty(pb)
9892  """
9893  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9894  return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
9895 
9896 

Referenced by FPVal().

◆ fpPlusZero()

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

Definition at line 9910 of file z3py.py.

9910 def fpPlusZero(s):
9911  """Create a Z3 floating-point +0.0 term."""
9912  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9913  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
9914 
9915 

Referenced by FPVal().

◆ fpRealToFP()

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

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

Definition at line 10468 of file z3py.py.

10468 def fpRealToFP(rm, v, sort, ctx=None):
10469  """Create a Z3 floating-point conversion expression that represents the
10470  conversion from a real term to a floating-point term.
10471 
10472  >>> x_r = RealVal(1.5)
10473  >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
10474  >>> x_fp
10475  fpToFP(RNE(), 3/2)
10476  >>> simplify(x_fp)
10477  1.5
10478  """
10479  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10480  _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
10481  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10482  ctx = _get_ctx(ctx)
10483  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10484 
10485 

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

10171 def fpRem(a, b, ctx=None):
10172  """Create a Z3 floating-point remainder expression.
10173 
10174  >>> s = FPSort(8, 24)
10175  >>> x = FP('x', s)
10176  >>> y = FP('y', s)
10177  >>> fpRem(x, y)
10178  fpRem(x, y)
10179  >>> fpRem(x, y).sort()
10180  FPSort(8, 24)
10181  """
10182  return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
10183 
10184 

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

◆ fpRoundToIntegral()

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

Definition at line 10227 of file z3py.py.

10227 def fpRoundToIntegral(rm, a, ctx=None):
10228  """Create a Z3 floating-point roundToIntegral expression.
10229  """
10230  return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
10231 
10232 

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

9999 def FPs(names, fpsort, ctx=None):
10000  """Return an array of floating-point constants.
10001 
10002  >>> x, y, z = FPs('x y z', FPSort(8, 24))
10003  >>> x.sort()
10004  FPSort(8, 24)
10005  >>> x.sbits()
10006  24
10007  >>> x.ebits()
10008  8
10009  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
10010  fpMul(RNE(), fpAdd(RNE(), x, y), z)
10011  """
10012  ctx = _get_ctx(ctx)
10013  if isinstance(names, str):
10014  names = names.split(" ")
10015  return [FP(name, fpsort, ctx) for name in names]
10016 
10017 

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

10486 def fpSignedToFP(rm, v, sort, ctx=None):
10487  """Create a Z3 floating-point conversion expression that represents the
10488  conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
10489 
10490  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10491  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
10492  >>> x_fp
10493  fpToFP(RNE(), 4294967291)
10494  >>> simplify(x_fp)
10495  -1.25*(2**2)
10496  """
10497  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10498  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10499  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10500  ctx = _get_ctx(ctx)
10501  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10502 
10503 

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

9804 def FPSort(ebits, sbits, ctx=None):
9805  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9806 
9807  >>> Single = FPSort(8, 24)
9808  >>> Double = FPSort(11, 53)
9809  >>> Single
9810  FPSort(8, 24)
9811  >>> x = Const('x', Single)
9812  >>> eq(x, FP('x', FPSort(8, 24)))
9813  True
9814  """
9815  ctx = _get_ctx(ctx)
9816  return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
9817 
9818 

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

◆ fpSqrt()

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

Definition at line 10221 of file z3py.py.

10221 def fpSqrt(rm, a, ctx=None):
10222  """Create a Z3 floating-point square root expression.
10223  """
10224  return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
10225 
10226 

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

10126 def fpSub(rm, a, b, ctx=None):
10127  """Create a Z3 floating-point subtraction expression.
10128 
10129  >>> s = FPSort(8, 24)
10130  >>> rm = RNE()
10131  >>> x = FP('x', s)
10132  >>> y = FP('y', s)
10133  >>> fpSub(rm, x, y)
10134  fpSub(RNE(), x, y)
10135  >>> fpSub(rm, x, y).sort()
10136  FPSort(8, 24)
10137  """
10138  return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
10139 
10140 

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

◆ fpToFP()

def z3py.fpToFP (   a1,
  a2 = None,
  a3 = None,
  ctx = None 
)
Create a Z3 floating-point conversion expression from other term sorts
to floating-point.

From a bit-vector term in IEEE 754-2008 format:
>>> x = FPVal(1.0, Float32())
>>> x_bv = fpToIEEEBV(x)
>>> simplify(fpToFP(x_bv, Float32()))
1

From a floating-point term with different precision:
>>> x = FPVal(1.0, Float32())
>>> x_db = fpToFP(RNE(), x, Float64())
>>> x_db.sort()
FPSort(11, 53)

From a real term:
>>> x_r = RealVal(1.5)
>>> simplify(fpToFP(RNE(), x_r, Float32()))
1.5

From a signed bit-vector term:
>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> simplify(fpToFP(RNE(), x_signed, Float32()))
-1.25*(2**2)

Definition at line 10392 of file z3py.py.

10392 def fpToFP(a1, a2=None, a3=None, ctx=None):
10393  """Create a Z3 floating-point conversion expression from other term sorts
10394  to floating-point.
10395 
10396  From a bit-vector term in IEEE 754-2008 format:
10397  >>> x = FPVal(1.0, Float32())
10398  >>> x_bv = fpToIEEEBV(x)
10399  >>> simplify(fpToFP(x_bv, Float32()))
10400  1
10401 
10402  From a floating-point term with different precision:
10403  >>> x = FPVal(1.0, Float32())
10404  >>> x_db = fpToFP(RNE(), x, Float64())
10405  >>> x_db.sort()
10406  FPSort(11, 53)
10407 
10408  From a real term:
10409  >>> x_r = RealVal(1.5)
10410  >>> simplify(fpToFP(RNE(), x_r, Float32()))
10411  1.5
10412 
10413  From a signed bit-vector term:
10414  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10415  >>> simplify(fpToFP(RNE(), x_signed, Float32()))
10416  -1.25*(2**2)
10417  """
10418  ctx = _get_ctx(ctx)
10419  if is_bv(a1) and is_fp_sort(a2):
10420  return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
10421  elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
10422  return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10423  elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
10424  return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10425  elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
10426  return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10427  else:
10428  raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
10429 
10430 

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

10522 def fpToFPUnsigned(rm, x, s, ctx=None):
10523  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
10524  if z3_debug():
10525  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10526  _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
10527  _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
10528  ctx = _get_ctx(ctx)
10529  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
10530 
10531 

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

10596 def fpToIEEEBV(x, ctx=None):
10597  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
10598 
10599  The size of the resulting bit-vector is automatically determined.
10600 
10601  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
10602  knows only one NaN and it will always produce the same bit-vector representation of
10603  that NaN.
10604 
10605  >>> x = FP('x', FPSort(8, 24))
10606  >>> y = fpToIEEEBV(x)
10607  >>> print(is_fp(x))
10608  True
10609  >>> print(is_bv(y))
10610  True
10611  >>> print(is_fp(y))
10612  False
10613  >>> print(is_bv(x))
10614  False
10615  """
10616  if z3_debug():
10617  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10618  ctx = _get_ctx(ctx)
10619  return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
10620 
10621 

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

10576 def fpToReal(x, ctx=None):
10577  """Create a Z3 floating-point conversion expression, from floating-point expression to real.
10578 
10579  >>> x = FP('x', FPSort(8, 24))
10580  >>> y = fpToReal(x)
10581  >>> print(is_fp(x))
10582  True
10583  >>> print(is_real(y))
10584  True
10585  >>> print(is_fp(y))
10586  False
10587  >>> print(is_real(x))
10588  False
10589  """
10590  if z3_debug():
10591  _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10592  ctx = _get_ctx(ctx)
10593  return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
10594 
10595 

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

10532 def fpToSBV(rm, x, s, ctx=None):
10533  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
10534 
10535  >>> x = FP('x', FPSort(8, 24))
10536  >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
10537  >>> print(is_fp(x))
10538  True
10539  >>> print(is_bv(y))
10540  True
10541  >>> print(is_fp(y))
10542  False
10543  >>> print(is_bv(x))
10544  False
10545  """
10546  if z3_debug():
10547  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10548  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10549  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10550  ctx = _get_ctx(ctx)
10551  return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10552 
10553 

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

10554 def fpToUBV(rm, x, s, ctx=None):
10555  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
10556 
10557  >>> x = FP('x', FPSort(8, 24))
10558  >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
10559  >>> print(is_fp(x))
10560  True
10561  >>> print(is_bv(y))
10562  True
10563  >>> print(is_fp(y))
10564  False
10565  >>> print(is_bv(x))
10566  False
10567  """
10568  if z3_debug():
10569  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10570  _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10571  _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10572  ctx = _get_ctx(ctx)
10573  return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10574 
10575 

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

10504 def fpUnsignedToFP(rm, v, sort, ctx=None):
10505  """Create a Z3 floating-point conversion expression that represents the
10506  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
10507 
10508  >>> x_signed = BitVecVal(-5, BitVecSort(32))
10509  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
10510  >>> x_fp
10511  fpToFPUnsigned(RNE(), 4294967291)
10512  >>> simplify(x_fp)
10513  1*(2**32)
10514  """
10515  _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10516  _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10517  _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10518  ctx = _get_ctx(ctx)
10519  return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10520 
10521 

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

9929 def FPVal(sig, exp=None, fps=None, ctx=None):
9930  """Return a floating-point value of value `val` and sort `fps`.
9931  If `ctx=None`, then the global context is used.
9932 
9933  >>> v = FPVal(20.0, FPSort(8, 24))
9934  >>> v
9935  1.25*(2**4)
9936  >>> print("0x%.8x" % v.exponent_as_long(False))
9937  0x00000004
9938  >>> v = FPVal(2.25, FPSort(8, 24))
9939  >>> v
9940  1.125*(2**1)
9941  >>> v = FPVal(-2.25, FPSort(8, 24))
9942  >>> v
9943  -1.125*(2**1)
9944  >>> FPVal(-0.0, FPSort(8, 24))
9945  -0.0
9946  >>> FPVal(0.0, FPSort(8, 24))
9947  +0.0
9948  >>> FPVal(+0.0, FPSort(8, 24))
9949  +0.0
9950  """
9951  ctx = _get_ctx(ctx)
9952  if is_fp_sort(exp):
9953  fps = exp
9954  exp = None
9955  elif fps is None:
9956  fps = _dflt_fps(ctx)
9957  _z3_assert(is_fp_sort(fps), "sort mismatch")
9958  if exp is None:
9959  exp = 0
9960  val = _to_float_str(sig)
9961  if val == "NaN" or val == "nan":
9962  return fpNaN(fps)
9963  elif val == "-0.0":
9964  return fpMinusZero(fps)
9965  elif val == "0.0" or val == "+0.0":
9966  return fpPlusZero(fps)
9967  elif val == "+oo" or val == "+inf" or val == "+Inf":
9968  return fpPlusInfinity(fps)
9969  elif val == "-oo" or val == "-inf" or val == "-Inf":
9970  return fpMinusInfinity(fps)
9971  else:
9972  return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
9973 
9974 

Referenced by set_default_fp_sort().

◆ fpZero()

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

Definition at line 9922 of file z3py.py.

9922 def fpZero(s, negative):
9923  """Create a Z3 floating-point +0.0 or -0.0 term."""
9924  _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
9925  _z3_assert(isinstance(negative, bool), "expected Boolean flag")
9926  return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
9927 
9928 

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

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

◆ FreshConst()

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

Definition at line 1453 of file z3py.py.

1453 def FreshConst(sort, prefix="c"):
1454  """Create a fresh constant of a specified sort"""
1455  ctx = _get_ctx(sort.ctx)
1456  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1457 
1458 

◆ FreshFunction()

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

Definition at line 880 of file z3py.py.

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

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

3272 def FreshInt(prefix="x", ctx=None):
3273  """Return a fresh integer constant in the given context using the given prefix.
3274 
3275  >>> x = FreshInt()
3276  >>> y = FreshInt()
3277  >>> eq(x, y)
3278  False
3279  >>> x.sort()
3280  Int
3281  """
3282  ctx = _get_ctx(ctx)
3283  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3284 
3285 

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

3329 def FreshReal(prefix="b", ctx=None):
3330  """Return a fresh real constant in the given context using the given prefix.
3331 
3332  >>> x = FreshReal()
3333  >>> y = FreshReal()
3334  >>> eq(x, y)
3335  False
3336  >>> x.sort()
3337  Real
3338  """
3339  ctx = _get_ctx(ctx)
3340  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3341 
3342 

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

10878 def Full(s):
10879  """Create the regular expression that accepts the universal language
10880  >>> e = Full(ReSort(SeqSort(IntSort())))
10881  >>> print(e)
10882  Full(ReSort(Seq(Int)))
10883  >>> e1 = Full(ReSort(StringSort()))
10884  >>> print(e1)
10885  Full(ReSort(String))
10886  """
10887  if isinstance(s, ReSortRef):
10888  return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
10889  raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
10890 
10891 
10892 

◆ FullSet()

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

Definition at line 4916 of file z3py.py.

4916 def FullSet(s):
4917  """Create the full set
4918  >>> FullSet(IntSort())
4919  K(Int, True)
4920  """
4921  ctx = s.ctx
4922  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4923 
4924 

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

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

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

6662 def get_as_array_func(n):
6663  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6664  if z3_debug():
6665  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6666  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6667 

Referenced by ModelRef.get_interp().

◆ get_ctx()

def z3py.get_ctx (   ctx)

Definition at line 261 of file z3py.py.

261 def get_ctx(ctx):
262  return _get_ctx(ctx)
263 
264 

◆ get_default_fp_sort()

def z3py.get_default_fp_sort (   ctx = None)

Definition at line 9226 of file z3py.py.

9226 def get_default_fp_sort(ctx=None):
9227  return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
9228 
9229 

Referenced by set_default_fp_sort().

◆ get_default_rounding_mode()

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

Definition at line 9193 of file z3py.py.

9193 def get_default_rounding_mode(ctx=None):
9194  """Retrieves the global default rounding mode."""
9195  global _dflt_rounding_mode
9196  if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
9197  return RTZ(ctx)
9198  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
9199  return RTN(ctx)
9200  elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
9201  return RTP(ctx)
9202  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
9203  return RNE(ctx)
9204  elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
9205  return RNA(ctx)
9206 
9207 

Referenced by set_default_fp_sort().

◆ get_full_version()

def z3py.get_full_version ( )

Definition at line 101 of file z3py.py.

101 def get_full_version():
102  return Z3_get_full_version()
103 
104 

◆ get_map_func()

def z3py.get_map_func (   a)
Return the function declaration associated with a Z3 map array expression.

>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a  = Map(f, b)
>>> eq(f, get_map_func(a))
True
>>> get_map_func(a)
f
>>> get_map_func(a)(0)
f(0)

Definition at line 4661 of file z3py.py.

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

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

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

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

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

◆ get_version()

def z3py.get_version ( )

Definition at line 92 of file z3py.py.

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

◆ get_version_string()

def z3py.get_version_string ( )

Definition at line 83 of file z3py.py.

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

◆ help_simplify()

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

Definition at line 8743 of file z3py.py.

8743 def help_simplify():
8744  """Return a string describing all options available for Z3 `simplify` procedure."""
8745  print(Z3_simplify_get_help(main_ctx().ref()))
8746 
8747 

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

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

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

◆ Implies()

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

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

Definition at line 1770 of file z3py.py.

1770 def Implies(a, b, ctx=None):
1771  """Create a Z3 implies expression.
1772 
1773  >>> p, q = Bools('p q')
1774  >>> Implies(p, q)
1775  Implies(p, q)
1776  """
1777  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1778  s = BoolSort(ctx)
1779  a = s.cast(a)
1780  b = s.cast(b)
1781  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1782 
1783 

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

◆ IndexOf()

def z3py.IndexOf (   s,
  substr,
  offset = None 
)
Retrieve the index of substring within a string starting at a specified offset.
>>> simplify(IndexOf("abcabc", "bc", 0))
1
>>> simplify(IndexOf("abcabc", "bc", 2))
4

Definition at line 10962 of file z3py.py.

10962 def IndexOf(s, substr, offset=None):
10963  """Retrieve the index of substring within a string starting at a specified offset.
10964  >>> simplify(IndexOf("abcabc", "bc", 0))
10965  1
10966  >>> simplify(IndexOf("abcabc", "bc", 2))
10967  4
10968  """
10969  if offset is None:
10970  offset = IntVal(0)
10971  ctx = None
10972  if is_expr(offset):
10973  ctx = offset.ctx
10974  ctx = _get_ctx2(s, substr, ctx)
10975  s = _coerce_seq(s, ctx)
10976  substr = _coerce_seq(substr, ctx)
10977  if _is_int(offset):
10978  offset = IntVal(offset, ctx)
10979  return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
10980 
10981 

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

11075 def InRe(s, re):
11076  """Create regular expression membership test
11077  >>> re = Union(Re("a"),Re("b"))
11078  >>> print (simplify(InRe("a", re)))
11079  True
11080  >>> print (simplify(InRe("b", re)))
11081  True
11082  >>> print (simplify(InRe("c", re)))
11083  False
11084  """
11085  s = _coerce_seq(s, re.ctx)
11086  return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
11087 
11088 

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

3233 def Int(name, ctx=None):
3234  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3235 
3236  >>> x = Int('x')
3237  >>> is_int(x)
3238  True
3239  >>> is_int(x + 1)
3240  True
3241  """
3242  ctx = _get_ctx(ctx)
3243  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3244 
3245 

Referenced by Ints(), and IntVector().

◆ Int2BV()

def z3py.Int2BV (   a,
  num_bits 
)
Return the z3 expression Int2BV(a, num_bits).
It is a bit-vector of width num_bits and represents the
modulo of a by 2^num_bits

Definition at line 3981 of file z3py.py.

3981 def Int2BV(a, num_bits):
3982  """Return the z3 expression Int2BV(a, num_bits).
3983  It is a bit-vector of width num_bits and represents the
3984  modulo of a by 2^num_bits
3985  """
3986  ctx = a.ctx
3987  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
3988 
3989 

◆ Intersect()

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

Definition at line 11109 of file z3py.py.

11109 def Intersect(*args):
11110  """Create intersection of regular expressions.
11111  >>> re = Intersect(Re("a"), Re("b"), Re("c"))
11112  """
11113  args = _get_args(args)
11114  sz = len(args)
11115  if z3_debug():
11116  _z3_assert(sz > 0, "At least one argument expected.")
11117  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
11118  if sz == 1:
11119  return args[0]
11120  ctx = args[0].ctx
11121  v = (Ast * sz)()
11122  for i in range(sz):
11123  v[i] = args[i].as_ast()
11124  return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
11125 
11126 

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

3246 def Ints(names, ctx=None):
3247  """Return a tuple of Integer constants.
3248 
3249  >>> x, y, z = Ints('x y z')
3250  >>> Sum(x, y, z)
3251  x + y + z
3252  """
3253  ctx = _get_ctx(ctx)
3254  if isinstance(names, str):
3255  names = names.split(" ")
3256  return [Int(name, ctx) for name in names]
3257 
3258 

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

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

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

◆ IntToStr()

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

Definition at line 11017 of file z3py.py.

11017 def IntToStr(s):
11018  """Convert integer expression to string"""
11019  if not is_expr(s):
11020  s = _py2expr(s)
11021  return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
11022 
11023 

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

3173 def IntVal(val, ctx=None):
3174  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3175 
3176  >>> IntVal(1)
3177  1
3178  >>> IntVal("100")
3179  100
3180  """
3181  ctx = _get_ctx(ctx)
3182  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3183 
3184 

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

◆ IntVector()

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

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

Definition at line 3259 of file z3py.py.

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

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

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

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

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

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

1606 def is_and(a):
1607  """Return `True` if `a` is a Z3 and expression.
1608 
1609  >>> p, q = Bools('p q')
1610  >>> is_and(And(p, q))
1611  True
1612  >>> is_and(Or(p, q))
1613  False
1614  """
1615  return is_app_of(a, Z3_OP_AND)
1616 
1617 

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

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

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

◆ is_app_of()

def z3py.is_app_of (   a,
  k 
)
Return `True` if `a` is an application of the given kind `k`.

>>> x = Int('x')
>>> n = x + 1
>>> is_app_of(n, Z3_OP_ADD)
True
>>> is_app_of(n, Z3_OP_MUL)
False

Definition at line 1357 of file z3py.py.

1357 def is_app_of(a, k):
1358  """Return `True` if `a` is an application of the given kind `k`.
1359 
1360  >>> x = Int('x')
1361  >>> n = x + 1
1362  >>> is_app_of(n, Z3_OP_ADD)
1363  True
1364  >>> is_app_of(n, Z3_OP_MUL)
1365  False
1366  """
1367  return is_app(a) and a.decl().kind() == k
1368 
1369 

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

◆ is_arith()

def z3py.is_arith (   a)
Return `True` if `a` is an arithmetical expression.

>>> x = Int('x')
>>> is_arith(x)
True
>>> is_arith(x + 1)
True
>>> is_arith(1)
False
>>> is_arith(IntVal(1))
True
>>> y = Real('y')
>>> is_arith(y)
True
>>> is_arith(y + 1)
True

Definition at line 2650 of file z3py.py.

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

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

◆ is_arith_sort()

def z3py.is_arith_sort (   s)
Return `True` if s is an arithmetical sort (type).

>>> is_arith_sort(IntSort())
True
>>> is_arith_sort(RealSort())
True
>>> is_arith_sort(BoolSort())
False
>>> n = Int('x') + 1
>>> is_arith_sort(n.sort())
True

Definition at line 2349 of file z3py.py.

2349 def is_arith_sort(s):
2350  """Return `True` if s is an arithmetical sort (type).
2351 
2352  >>> is_arith_sort(IntSort())
2353  True
2354  >>> is_arith_sort(RealSort())
2355  True
2356  >>> is_arith_sort(BoolSort())
2357  False
2358  >>> n = Int('x') + 1
2359  >>> is_arith_sort(n.sort())
2360  True
2361  """
2362  return isinstance(s, ArithSortRef)
2363 
2364 

Referenced by ArithSortRef.subsort().

◆ is_array()

def z3py.is_array (   a)
Return `True` if `a` is a Z3 array expression.

>>> a = Array('a', IntSort(), IntSort())
>>> is_array(a)
True
>>> is_array(Store(a, 0, 1))
True
>>> is_array(a[0])
False

Definition at line 4596 of file z3py.py.

4596 def is_array(a):
4597  """Return `True` if `a` is a Z3 array expression.
4598 
4599  >>> a = Array('a', IntSort(), IntSort())
4600  >>> is_array(a)
4601  True
4602  >>> is_array(Store(a, 0, 1))
4603  True
4604  >>> is_array(a[0])
4605  False
4606  """
4607  return isinstance(a, ArrayRef)
4608 
4609 

Referenced by Ext(), and Map().

◆ is_array_sort()

def z3py.is_array_sort (   a)

Definition at line 4592 of file z3py.py.

4592 def is_array_sort(a):
4593  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4594 
4595 

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

◆ is_as_array()

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

Definition at line 6657 of file z3py.py.

6657 def is_as_array(n):
6658  """Return true if n is a Z3 expression of the form (_ as-array f)."""
6659  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6660 
6661 

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

◆ is_ast()

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

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

Definition at line 445 of file z3py.py.

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

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

◆ is_bool()

def z3py.is_bool (   a)
Return `True` if `a` is a Z3 Boolean expression.

>>> p = Bool('p')
>>> is_bool(p)
True
>>> q = Bool('q')
>>> is_bool(And(p, q))
True
>>> x = Real('x')
>>> is_bool(x)
False
>>> is_bool(x == 0)
True

Definition at line 1556 of file z3py.py.

1556 def is_bool(a):
1557  """Return `True` if `a` is a Z3 Boolean expression.
1558 
1559  >>> p = Bool('p')
1560  >>> is_bool(p)
1561  True
1562  >>> q = Bool('q')
1563  >>> is_bool(And(p, q))
1564  True
1565  >>> x = Real('x')
1566  >>> is_bool(x)
1567  False
1568  >>> is_bool(x == 0)
1569  True
1570  """
1571  return isinstance(a, BoolRef)
1572 
1573 

Referenced by is_quantifier(), and prove().

◆ is_bv()

def z3py.is_bv (   a)
Return `True` if `a` is a Z3 bit-vector expression.

>>> b = BitVec('b', 32)
>>> is_bv(b)
True
>>> is_bv(b + 10)
True
>>> is_bv(Int('x'))
False

Definition at line 3929 of file z3py.py.

3929 def is_bv(a):
3930  """Return `True` if `a` is a Z3 bit-vector expression.
3931 
3932  >>> b = BitVec('b', 32)
3933  >>> is_bv(b)
3934  True
3935  >>> is_bv(b + 10)
3936  True
3937  >>> is_bv(Int('x'))
3938  False
3939  """
3940  return isinstance(a, BitVecRef)
3941 
3942 

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

◆ is_bv_sort()

def z3py.is_bv_sort (   s)
Return True if `s` is a Z3 bit-vector sort.

>>> is_bv_sort(BitVecSort(32))
True
>>> is_bv_sort(IntSort())
False

Definition at line 3461 of file z3py.py.

3461 def is_bv_sort(s):
3462  """Return True if `s` is a Z3 bit-vector sort.
3463 
3464  >>> is_bv_sort(BitVecSort(32))
3465  True
3466  >>> is_bv_sort(IntSort())
3467  False
3468  """
3469  return isinstance(s, BitVecSortRef)
3470 
3471 

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

◆ is_bv_value()

def z3py.is_bv_value (   a)
Return `True` if `a` is a Z3 bit-vector numeral value.

>>> b = BitVec('b', 32)
>>> is_bv_value(b)
False
>>> b = BitVecVal(10, 32)
>>> b
10
>>> is_bv_value(b)
True

Definition at line 3943 of file z3py.py.

3943 def is_bv_value(a):
3944  """Return `True` if `a` is a Z3 bit-vector numeral value.
3945 
3946  >>> b = BitVec('b', 32)
3947  >>> is_bv_value(b)
3948  False
3949  >>> b = BitVecVal(10, 32)
3950  >>> b
3951  10
3952  >>> is_bv_value(b)
3953  True
3954  """
3955  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3956 
3957 

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

1280 def is_const(a):
1281  """Return `True` if `a` is Z3 constant/variable expression.
1282 
1283  >>> a = Int('a')
1284  >>> is_const(a)
1285  True
1286  >>> is_const(a + 1)
1287  False
1288  >>> is_const(1)
1289  False
1290  >>> is_const(IntVal(1))
1291  True
1292  >>> x = Int('x')
1293  >>> is_const(ForAll(x, x >= 0))
1294  False
1295  """
1296  return is_app(a) and a.num_args() == 0
1297 
1298 

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

◆ is_const_array()

def z3py.is_const_array (   a)
Return `True` if `a` is a Z3 constant array.

>>> a = K(IntSort(), 10)
>>> is_const_array(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_const_array(a)
False

Definition at line 4610 of file z3py.py.

4610 def is_const_array(a):
4611  """Return `True` if `a` is a Z3 constant array.
4612 
4613  >>> a = K(IntSort(), 10)
4614  >>> is_const_array(a)
4615  True
4616  >>> a = Array('a', IntSort(), IntSort())
4617  >>> is_const_array(a)
4618  False
4619  """
4620  return is_app_of(a, Z3_OP_CONST_ARRAY)
4621 
4622 

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

4652 def is_default(a):
4653  """Return `True` if `a` is a Z3 default array expression.
4654  >>> d = Default(K(IntSort(), 10))
4655  >>> is_default(d)
4656  True
4657  """
4658  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4659 
4660 

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

1664 def is_distinct(a):
1665  """Return `True` if `a` is a Z3 distinct expression.
1666 
1667  >>> x, y, z = Ints('x y z')
1668  >>> is_distinct(x == y)
1669  False
1670  >>> is_distinct(Distinct(x, y, z))
1671  True
1672  """
1673  return is_app_of(a, Z3_OP_DISTINCT)
1674 
1675 

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

2813 def is_div(a):
2814  """Return `True` if `a` is an expression of the form b / c.
2815 
2816  >>> x, y = Reals('x y')
2817  >>> is_div(x / y)
2818  True
2819  >>> is_div(x + y)
2820  False
2821  >>> x, y = Ints('x y')
2822  >>> is_div(x / y)
2823  False
2824  >>> is_idiv(x / y)
2825  True
2826  """
2827  return is_app_of(a, Z3_OP_DIV)
2828 
2829 

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

1654 def is_eq(a):
1655  """Return `True` if `a` is a Z3 equality expression.
1656 
1657  >>> x, y = Ints('x y')
1658  >>> is_eq(x == y)
1659  True
1660  """
1661  return is_app_of(a, Z3_OP_EQ)
1662 
1663 

Referenced by AstRef.__bool__().

◆ is_expr()

def z3py.is_expr (   a)
Return `True` if `a` is a Z3 expression.

>>> a = Int('a')
>>> is_expr(a)
True
>>> is_expr(a + 1)
True
>>> is_expr(IntSort())
False
>>> is_expr(1)
False
>>> is_expr(IntVal(1))
True
>>> x = Int('x')
>>> is_expr(ForAll(x, x >= 0))
True
>>> is_expr(FPVal(1.0))
True

Definition at line 1231 of file z3py.py.

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

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

◆ is_false()

def z3py.is_false (   a)
Return `True` if `a` is the Z3 false expression.

>>> p = Bool('p')
>>> is_false(p)
False
>>> is_false(False)
False
>>> is_false(BoolVal(False))
True

Definition at line 1592 of file z3py.py.

1592 def is_false(a):
1593  """Return `True` if `a` is the Z3 false expression.
1594 
1595  >>> p = Bool('p')
1596  >>> is_false(p)
1597  False
1598  >>> is_false(False)
1599  False
1600  >>> is_false(BoolVal(False))
1601  True
1602  """
1603  return is_app_of(a, Z3_OP_FALSE)
1604 
1605 

Referenced by AstRef.__bool__().

◆ is_finite_domain()

def z3py.is_finite_domain (   a)
Return `True` if `a` is a Z3 finite-domain expression.

>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain(b)
True
>>> is_finite_domain(Int('x'))
False

Definition at line 7694 of file z3py.py.

7694 def is_finite_domain(a):
7695  """Return `True` if `a` is a Z3 finite-domain expression.
7696 
7697  >>> s = FiniteDomainSort('S', 100)
7698  >>> b = Const('b', s)
7699  >>> is_finite_domain(b)
7700  True
7701  >>> is_finite_domain(Int('x'))
7702  False
7703  """
7704  return isinstance(a, FiniteDomainRef)
7705 
7706 

Referenced by is_finite_domain_value().

◆ is_finite_domain_sort()

def z3py.is_finite_domain_sort (   s)
Return True if `s` is a Z3 finite-domain sort.

>>> is_finite_domain_sort(FiniteDomainSort('S', 100))
True
>>> is_finite_domain_sort(IntSort())
False

Definition at line 7671 of file z3py.py.

7671 def is_finite_domain_sort(s):
7672  """Return True if `s` is a Z3 finite-domain sort.
7673 
7674  >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7675  True
7676  >>> is_finite_domain_sort(IntSort())
7677  False
7678  """
7679  return isinstance(s, FiniteDomainSortRef)
7680 
7681 

Referenced by FiniteDomainVal().

◆ is_finite_domain_value()

def z3py.is_finite_domain_value (   a)
Return `True` if `a` is a Z3 finite-domain value.

>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain_value(b)
False
>>> b = FiniteDomainVal(10, s)
>>> b
10
>>> is_finite_domain_value(b)
True

Definition at line 7748 of file z3py.py.

7748 def is_finite_domain_value(a):
7749  """Return `True` if `a` is a Z3 finite-domain value.
7750 
7751  >>> s = FiniteDomainSort('S', 100)
7752  >>> b = Const('b', s)
7753  >>> is_finite_domain_value(b)
7754  False
7755  >>> b = FiniteDomainVal(10, s)
7756  >>> b
7757  10
7758  >>> is_finite_domain_value(b)
7759  True
7760  """
7761  return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7762 
7763 

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

9775 def is_fp(a):
9776  """Return `True` if `a` is a Z3 floating-point expression.
9777 
9778  >>> b = FP('b', FPSort(8, 24))
9779  >>> is_fp(b)
9780  True
9781  >>> is_fp(b + 1.0)
9782  True
9783  >>> is_fp(Int('x'))
9784  False
9785  """
9786  return isinstance(a, FPRef)
9787 
9788 

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

◆ is_fp_sort()

def z3py.is_fp_sort (   s)
Return True if `s` is a Z3 floating-point sort.

>>> is_fp_sort(FPSort(8, 24))
True
>>> is_fp_sort(IntSort())
False

Definition at line 9359 of file z3py.py.

9359 def is_fp_sort(s):
9360  """Return True if `s` is a Z3 floating-point sort.
9361 
9362  >>> is_fp_sort(FPSort(8, 24))
9363  True
9364  >>> is_fp_sort(IntSort())
9365  False
9366  """
9367  return isinstance(s, FPSortRef)
9368 
9369 

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

◆ is_fp_value()

def z3py.is_fp_value (   a)
Return `True` if `a` is a Z3 floating-point numeral value.

>>> b = FP('b', FPSort(8, 24))
>>> is_fp_value(b)
False
>>> b = FPVal(1.0, FPSort(8, 24))
>>> b
1
>>> is_fp_value(b)
True

Definition at line 9789 of file z3py.py.

9789 def is_fp_value(a):
9790  """Return `True` if `a` is a Z3 floating-point numeral value.
9791 
9792  >>> b = FP('b', FPSort(8, 24))
9793  >>> is_fp_value(b)
9794  False
9795  >>> b = FPVal(1.0, FPSort(8, 24))
9796  >>> b
9797  1
9798  >>> is_fp_value(b)
9799  True
9800  """
9801  return is_fp(a) and _is_numeral(a.ctx, a.ast)
9802 
9803 

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

9619 def is_fprm(a):
9620  """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9621 
9622  >>> rm = RNE()
9623  >>> is_fprm(rm)
9624  True
9625  >>> rm = 1.0
9626  >>> is_fprm(rm)
9627  False
9628  """
9629  return isinstance(a, FPRMRef)
9630 
9631 

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

◆ is_fprm_sort()

def z3py.is_fprm_sort (   s)
Return True if `s` is a Z3 floating-point rounding mode sort.

>>> is_fprm_sort(FPSort(8, 24))
False
>>> is_fprm_sort(RNE().sort())
True

Definition at line 9370 of file z3py.py.

9370 def is_fprm_sort(s):
9371  """Return True if `s` is a Z3 floating-point rounding mode sort.
9372 
9373  >>> is_fprm_sort(FPSort(8, 24))
9374  False
9375  >>> is_fprm_sort(RNE().sort())
9376  True
9377  """
9378  return isinstance(s, FPRMSortRef)
9379 
9380 # FP Expressions
9381 
9382 

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

9632 def is_fprm_value(a):
9633  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9634  return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9635 
9636 # FP Numerals
9637 
9638 

Referenced by set_default_rounding_mode().

◆ is_func_decl()

def z3py.is_func_decl (   a)
Return `True` if `a` is a Z3 function declaration.

>>> f = Function('f', IntSort(), IntSort())
>>> is_func_decl(f)
True
>>> x = Real('x')
>>> is_func_decl(x)
False

Definition at line 844 of file z3py.py.

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

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

◆ is_ge()

def z3py.is_ge (   a)
Return `True` if `a` is an expression of the form b >= c.

>>> x, y = Ints('x y')
>>> is_ge(x >= y)
True
>>> is_ge(x == y)
False

Definition at line 2878 of file z3py.py.

2878 def is_ge(a):
2879  """Return `True` if `a` is an expression of the form b >= c.
2880 
2881  >>> x, y = Ints('x y')
2882  >>> is_ge(x >= y)
2883  True
2884  >>> is_ge(x == y)
2885  False
2886  """
2887  return is_app_of(a, Z3_OP_GE)
2888 
2889 

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

2890 def is_gt(a):
2891  """Return `True` if `a` is an expression of the form b > c.
2892 
2893  >>> x, y = Ints('x y')
2894  >>> is_gt(x > y)
2895  True
2896  >>> is_gt(x == y)
2897  False
2898  """
2899  return is_app_of(a, Z3_OP_GT)
2900 
2901 

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

2830 def is_idiv(a):
2831  """Return `True` if `a` is an expression of the form b div c.
2832 
2833  >>> x, y = Ints('x y')
2834  >>> is_idiv(x / y)
2835  True
2836  >>> is_idiv(x + y)
2837  False
2838  """
2839  return is_app_of(a, Z3_OP_IDIV)
2840 
2841 

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

1630 def is_implies(a):
1631  """Return `True` if `a` is a Z3 implication expression.
1632 
1633  >>> p, q = Bools('p q')
1634  >>> is_implies(Implies(p, q))
1635  True
1636  >>> is_implies(And(p, q))
1637  False
1638  """
1639  return is_app_of(a, Z3_OP_IMPLIES)
1640 
1641 

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

2671 def is_int(a):
2672  """Return `True` if `a` is an integer expression.
2673 
2674  >>> x = Int('x')
2675  >>> is_int(x + 1)
2676  True
2677  >>> is_int(1)
2678  False
2679  >>> is_int(IntVal(1))
2680  True
2681  >>> y = Real('y')
2682  >>> is_int(y)
2683  False
2684  >>> is_int(y + 1)
2685  False
2686  """
2687  return is_arith(a) and a.is_int()
2688 
2689 

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

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

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

2902 def is_is_int(a):
2903  """Return `True` if `a` is an expression of the form IsInt(b).
2904 
2905  >>> x = Real('x')
2906  >>> is_is_int(IsInt(x))
2907  True
2908  >>> is_is_int(x)
2909  False
2910  """
2911  return is_app_of(a, Z3_OP_IS_INT)
2912 
2913 

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

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

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

2854 def is_le(a):
2855  """Return `True` if `a` is an expression of the form b <= c.
2856 
2857  >>> x, y = Ints('x y')
2858  >>> is_le(x <= y)
2859  True
2860  >>> is_le(x < y)
2861  False
2862  """
2863  return is_app_of(a, Z3_OP_LE)
2864 
2865 

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

2866 def is_lt(a):
2867  """Return `True` if `a` is an expression of the form b < c.
2868 
2869  >>> x, y = Ints('x y')
2870  >>> is_lt(x < y)
2871  True
2872  >>> is_lt(x == y)
2873  False
2874  """
2875  return is_app_of(a, Z3_OP_LT)
2876 
2877 

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

4636 def is_map(a):
4637  """Return `True` if `a` is a Z3 map array expression.
4638 
4639  >>> f = Function('f', IntSort(), IntSort())
4640  >>> b = Array('b', IntSort(), IntSort())
4641  >>> a = Map(f, b)
4642  >>> a
4643  Map(f, b)
4644  >>> is_map(a)
4645  True
4646  >>> is_map(b)
4647  False
4648  """
4649  return is_app_of(a, Z3_OP_ARRAY_MAP)
4650 
4651 

Referenced by get_map_func().

◆ is_mod()

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

>>> x, y = Ints('x y')
>>> is_mod(x % y)
True
>>> is_mod(x + y)
False

Definition at line 2842 of file z3py.py.

2842 def is_mod(a):
2843  """Return `True` if `a` is an expression of the form b % c.
2844 
2845  >>> x, y = Ints('x y')
2846  >>> is_mod(x % y)
2847  True
2848  >>> is_mod(x + y)
2849  False
2850  """
2851  return is_app_of(a, Z3_OP_MOD)
2852 
2853 

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

2789 def is_mul(a):
2790  """Return `True` if `a` is an expression of the form b * c.
2791 
2792  >>> x, y = Ints('x y')
2793  >>> is_mul(x * y)
2794  True
2795  >>> is_mul(x - y)
2796  False
2797  """
2798  return is_app_of(a, Z3_OP_MUL)
2799 
2800 

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

1642 def is_not(a):
1643  """Return `True` if `a` is a Z3 not expression.
1644 
1645  >>> p = Bool('p')
1646  >>> is_not(p)
1647  False
1648  >>> is_not(Not(p))
1649  True
1650  """
1651  return is_app_of(a, Z3_OP_NOT)
1652 
1653 

Referenced by mk_not().

◆ is_or()

def z3py.is_or (   a)
Return `True` if `a` is a Z3 or expression.

>>> p, q = Bools('p q')
>>> is_or(Or(p, q))
True
>>> is_or(And(p, q))
False

Definition at line 1618 of file z3py.py.

1618 def is_or(a):
1619  """Return `True` if `a` is a Z3 or expression.
1620 
1621  >>> p, q = Bools('p q')
1622  >>> is_or(Or(p, q))
1623  True
1624  >>> is_or(And(p, q))
1625  False
1626  """
1627  return is_app_of(a, Z3_OP_OR)
1628 
1629 

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

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

Referenced by is_quantifier(), and MultiPattern().

◆ is_probe()

def z3py.is_probe (   p)
Return `True` if `p` is a Z3 probe.

>>> is_probe(Int('x'))
False
>>> is_probe(Probe('memory'))
True

Definition at line 8584 of file z3py.py.

8584 def is_probe(p):
8585  """Return `True` if `p` is a Z3 probe.
8586 
8587  >>> is_probe(Int('x'))
8588  False
8589  >>> is_probe(Probe('memory'))
8590  True
8591  """
8592  return isinstance(p, Probe)
8593 
8594 

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

◆ is_quantifier()

def z3py.is_quantifier (   a)
Return `True` if `a` is a Z3 quantifier.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> is_quantifier(q)
True
>>> is_quantifier(f(x))
False

Definition at line 2158 of file z3py.py.

2158 def is_quantifier(a):
2159  """Return `True` if `a` is a Z3 quantifier.
2160 
2161  >>> f = Function('f', IntSort(), IntSort())
2162  >>> x = Int('x')
2163  >>> q = ForAll(x, f(x) == 0)
2164  >>> is_quantifier(q)
2165  True
2166  >>> is_quantifier(f(x))
2167  False
2168  """
2169  return isinstance(a, QuantifierRef)
2170 
2171 

◆ is_rational_value()

def z3py.is_rational_value (   a)
Return `True` if `a` is rational value of sort Real.

>>> is_rational_value(RealVal(1))
True
>>> is_rational_value(RealVal("3/5"))
True
>>> is_rational_value(IntVal(1))
False
>>> is_rational_value(1)
False
>>> n = Real('x') + 1
>>> n.arg(1)
1
>>> is_rational_value(n.arg(1))
True
>>> is_rational_value(Real('x'))
False

Definition at line 2741 of file z3py.py.

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

◆ is_re()

def z3py.is_re (   s)

Definition at line 11071 of file z3py.py.

11071 def is_re(s):
11072  return isinstance(s, ReRef)
11073 
11074 

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

◆ is_real()

def z3py.is_real (   a)
Return `True` if `a` is a real expression.

>>> x = Int('x')
>>> is_real(x + 1)
False
>>> y = Real('y')
>>> is_real(y)
True
>>> is_real(y + 1)
True
>>> is_real(1)
False
>>> is_real(RealVal(1))
True

Definition at line 2690 of file z3py.py.

2690 def is_real(a):
2691  """Return `True` if `a` is a real expression.
2692 
2693  >>> x = Int('x')
2694  >>> is_real(x + 1)
2695  False
2696  >>> y = Real('y')
2697  >>> is_real(y)
2698  True
2699  >>> is_real(y + 1)
2700  True
2701  >>> is_real(1)
2702  False
2703  >>> is_real(RealVal(1))
2704  True
2705  """
2706  return is_arith(a) and a.is_real()
2707 
2708 

Referenced by fpRealToFP(), and fpToFP().

◆ is_select()

def z3py.is_select (   a)
Return `True` if `a` is a Z3 array select application.

>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True

Definition at line 4871 of file z3py.py.

4871 def is_select(a):
4872  """Return `True` if `a` is a Z3 array select application.
4873 
4874  >>> a = Array('a', IntSort(), IntSort())
4875  >>> is_select(a)
4876  False
4877  >>> i = Int('i')
4878  >>> is_select(a[i])
4879  True
4880  """
4881  return is_app_of(a, Z3_OP_SELECT)
4882 
4883 

◆ is_seq()

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

Definition at line 10797 of file z3py.py.

10797 def is_seq(a):
10798  """Return `True` if `a` is a Z3 sequence expression.
10799  >>> print (is_seq(Unit(IntVal(0))))
10800  True
10801  >>> print (is_seq(StringVal("abc")))
10802  True
10803  """
10804  return isinstance(a, SeqRef)
10805 
10806 

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

◆ is_sort()

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

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

Definition at line 641 of file z3py.py.

641 def is_sort(s):
642  """Return `True` if `s` is a Z3 sort.
643 
644  >>> is_sort(IntSort())
645  True
646  >>> is_sort(Int('x'))
647  False
648  >>> is_expr(Int('x'))
649  True
650  """
651  return isinstance(s, SortRef)
652 
653 

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

◆ is_store()

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

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

Definition at line 4884 of file z3py.py.

4884 def is_store(a):
4885  """Return `True` if `a` is a Z3 array store application.
4886 
4887  >>> a = Array('a', IntSort(), IntSort())
4888  >>> is_store(a)
4889  False
4890  >>> is_store(Store(a, 0, 1))
4891  True
4892  """
4893  return is_app_of(a, Z3_OP_STORE)
4894 

◆ is_string()

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

Definition at line 10807 of file z3py.py.

10807 def is_string(a):
10808  """Return `True` if `a` is a Z3 string expression.
10809  >>> print (is_string(StringVal("ab")))
10810  True
10811  """
10812  return isinstance(a, SeqRef) and a.is_string()
10813 
10814 

◆ is_string_value()

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

Definition at line 10815 of file z3py.py.

10815 def is_string_value(a):
10816  """return 'True' if 'a' is a Z3 string constant expression.
10817  >>> print (is_string_value(StringVal("a")))
10818  True
10819  >>> print (is_string_value(StringVal("a") + StringVal("b")))
10820  False
10821  """
10822  return isinstance(a, SeqRef) and a.is_string_value()
10823 

◆ is_sub()

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

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

Definition at line 2801 of file z3py.py.

2801 def is_sub(a):
2802  """Return `True` if `a` is an expression of the form b - c.
2803 
2804  >>> x, y = Ints('x y')
2805  >>> is_sub(x - y)
2806  True
2807  >>> is_sub(x + y)
2808  False
2809  """
2810  return is_app_of(a, Z3_OP_SUB)
2811 
2812 

◆ is_to_int()

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

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

Definition at line 2929 of file z3py.py.

2929 def is_to_int(a):
2930  """Return `True` if `a` is an expression of the form ToInt(b).
2931 
2932  >>> x = Real('x')
2933  >>> n = ToInt(x)
2934  >>> n
2935  ToInt(x)
2936  >>> is_to_int(n)
2937  True
2938  >>> is_to_int(x)
2939  False
2940  """
2941  return is_app_of(a, Z3_OP_TO_INT)
2942 
2943 

◆ is_to_real()

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

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

Definition at line 2914 of file z3py.py.

2914 def is_to_real(a):
2915  """Return `True` if `a` is an expression of the form ToReal(b).
2916 
2917  >>> x = Int('x')
2918  >>> n = ToReal(x)
2919  >>> n
2920  ToReal(x)
2921  >>> is_to_real(n)
2922  True
2923  >>> is_to_real(x)
2924  False
2925  """
2926  return is_app_of(a, Z3_OP_TO_REAL)
2927 
2928 

◆ is_true()

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

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

Definition at line 1574 of file z3py.py.

1574 def is_true(a):
1575  """Return `True` if `a` is the Z3 true expression.
1576 
1577  >>> p = Bool('p')
1578  >>> is_true(p)
1579  False
1580  >>> is_true(simplify(p == p))
1581  True
1582  >>> x = Real('x')
1583  >>> is_true(x == 0)
1584  False
1585  >>> # True is a Python Boolean expression
1586  >>> is_true(True)
1587  False
1588  """
1589  return is_app_of(a, Z3_OP_TRUE)
1590 
1591 

Referenced by AstRef.__bool__().

◆ is_var()

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

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

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

Definition at line 1299 of file z3py.py.

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

Referenced by get_var_index().

◆ IsInt()

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

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

Definition at line 3379 of file z3py.py.

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

◆ IsMember()

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

Definition at line 4994 of file z3py.py.

4994 def IsMember(e, s):
4995  """ Check if e is a member of set s
4996  >>> a = Const('a', SetSort(IntSort()))
4997  >>> IsMember(1, a)
4998  a[1]
4999  """
5000  ctx = _ctx_from_ast_arg_list([s, e])
5001  e = _py2expr(e, ctx)
5002  return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
5003 
5004 

◆ IsSubset()

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

Definition at line 5005 of file z3py.py.

5005 def IsSubset(a, b):
5006  """ Check if a is a subset of b
5007  >>> a = Const('a', SetSort(IntSort()))
5008  >>> b = Const('b', SetSort(IntSort()))
5009  >>> IsSubset(a, b)
5010  subset(a, b)
5011  """
5012  ctx = _ctx_from_ast_arg_list([a, b])
5013  return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
5014 
5015 

◆ K()

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

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

Definition at line 4831 of file z3py.py.

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

◆ Lambda()

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

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

Definition at line 2246 of file z3py.py.

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

Referenced by Context.MkLambda().

◆ LastIndexOf()

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

Definition at line 10982 of file z3py.py.

10982 def LastIndexOf(s, substr):
10983  """Retrieve the last index of substring within a string"""
10984  ctx = None
10985  ctx = _get_ctx2(s, substr, ctx)
10986  s = _coerce_seq(s, ctx)
10987  substr = _coerce_seq(substr, ctx)
10988  return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx)
10989 
10990 

◆ Length()

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

Definition at line 10991 of file z3py.py.

10991 def Length(s):
10992  """Obtain the length of a sequence 's'
10993  >>> l = Length(StringVal("abc"))
10994  >>> simplify(l)
10995  3
10996  """
10997  s = _coerce_seq(s)
10998  return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
10999 
11000 

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

◆ LinearOrder()

def z3py.LinearOrder (   a,
  index 
)

Definition at line 11213 of file z3py.py.

11213 def LinearOrder(a, index):
11214  return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11215 
11216 

◆ Loop()

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

Definition at line 11171 of file z3py.py.

11171 def Loop(re, lo, hi=0):
11172  """Create the regular expression accepting between a lower and upper bound repetitions
11173  >>> re = Loop(Re("a"), 1, 3)
11174  >>> print(simplify(InRe("aa", re)))
11175  True
11176  >>> print(simplify(InRe("aaaa", re)))
11177  False
11178  >>> print(simplify(InRe("", re)))
11179  False
11180  """
11181  return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
11182 
11183 

◆ LShR()

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

Use the operator >> for the arithmetical right shift.

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

Definition at line 4284 of file z3py.py.

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

◆ main_ctx()

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

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

Definition at line 233 of file z3py.py.

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

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

◆ Map()

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

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

Definition at line 4808 of file z3py.py.

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

Referenced by Context.Context().

◆ mk_not()

def z3py.mk_not (   a)

Definition at line 1819 of file z3py.py.

1819 def mk_not(a):
1820  if is_not(a):
1821  return a.arg(0)
1822  else:
1823  return Not(a)
1824 
1825 

◆ Model()

def z3py.Model (   ctx = None)

Definition at line 6652 of file z3py.py.

6652 def Model(ctx=None):
6653  ctx = _get_ctx(ctx)
6654  return ModelRef(Z3_mk_model(ctx.ref()), ctx)
6655 
6656 

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

◆ MultiPattern()

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

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

Definition at line 1936 of file z3py.py.

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

◆ Not()

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

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

Definition at line 1800 of file z3py.py.

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

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

◆ open_log()

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

Definition at line 114 of file z3py.py.

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

◆ Option()

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

Definition at line 11140 of file z3py.py.

11140 def Option(re):
11141  """Create the regular expression that optionally accepts the argument.
11142  >>> re = Option(Re("a"))
11143  >>> print(simplify(InRe("a", re)))
11144  True
11145  >>> print(simplify(InRe("", re)))
11146  True
11147  >>> print(simplify(InRe("aa", re)))
11148  False
11149  """
11150  return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
11151 
11152 

◆ Or()

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

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

Definition at line 1867 of file z3py.py.

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

Referenced by ApplyResult.as_expr().

◆ OrElse()

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

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

Definition at line 8277 of file z3py.py.

8277 def OrElse(*ts, **ks):
8278  """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
8279 
8280  >>> x = Int('x')
8281  >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
8282  >>> # Tactic split-clause fails if there is no clause in the given goal.
8283  >>> t(x == 0)
8284  [[x == 0]]
8285  >>> t(Or(x == 0, x == 1))
8286  [[x == 0], [x == 1]]
8287  """
8288  if z3_debug():
8289  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8290  ctx = ks.get("ctx", None)
8291  num = len(ts)
8292  r = ts[0]
8293  for i in range(num - 1):
8294  r = _or_else(r, ts[i + 1], ctx)
8295  return r
8296 
8297 

◆ ParAndThen()

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

Definition at line 8333 of file z3py.py.

8333 def ParAndThen(t1, t2, ctx=None):
8334  """Alias for ParThen(t1, t2, ctx)."""
8335  return ParThen(t1, t2, ctx)
8336 
8337 

◆ ParOr()

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

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

Definition at line 8298 of file z3py.py.

8298 def ParOr(*ts, **ks):
8299  """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
8300 
8301  >>> x = Int('x')
8302  >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
8303  >>> t(x + 1 == 2)
8304  [[x == 1]]
8305  """
8306  if z3_debug():
8307  _z3_assert(len(ts) >= 2, "At least two arguments expected")
8308  ctx = _get_ctx(ks.get("ctx", None))
8309  ts = [_to_tactic(t, ctx) for t in ts]
8310  sz = len(ts)
8311  _args = (TacticObj * sz)()
8312  for i in range(sz):
8313  _args[i] = ts[i].tactic
8314  return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
8315 
8316 

◆ parse_smt2_file()

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

This function is similar to parse_smt2_string().

Definition at line 9169 of file z3py.py.

9169 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
9170  """Parse a file in SMT 2.0 format using the given sorts and decls.
9171 
9172  This function is similar to parse_smt2_string().
9173  """
9174  ctx = _get_ctx(ctx)
9175  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9176  dsz, dnames, ddecls = _dict2darray(decls, ctx)
9177  return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9178 
9179 

◆ parse_smt2_string()

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

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

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

Definition at line 9148 of file z3py.py.

9148 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
9149  """Parse a string in SMT 2.0 format using the given sorts and decls.
9150 
9151  The arguments sorts and decls are Python dictionaries used to initialize
9152  the symbol table used for the SMT 2.0 parser.
9153 
9154  >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
9155  [x > 0, x < 10]
9156  >>> x, y = Ints('x y')
9157  >>> f = Function('f', IntSort(), IntSort())
9158  >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
9159  [x + f(y) > 0]
9160  >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
9161  [a > 0]
9162  """
9163  ctx = _get_ctx(ctx)
9164  ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9165  dsz, dnames, ddecls = _dict2darray(decls, ctx)
9166  return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9167 
9168 

◆ ParThen()

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

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

Definition at line 8317 of file z3py.py.

8317 def ParThen(t1, t2, ctx=None):
8318  """Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
8319  The subgoals are processed in parallel.
8320 
8321  >>> x, y = Ints('x y')
8322  >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
8323  >>> t(And(Or(x == 1, x == 2), y == x + 1))
8324  [[x == 1, y == 2], [x == 2, y == 3]]
8325  """
8326  t1 = _to_tactic(t1, ctx)
8327  t2 = _to_tactic(t2, ctx)
8328  if z3_debug():
8329  _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
8330  return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
8331 
8332 

Referenced by ParAndThen().

◆ PartialOrder()

def z3py.PartialOrder (   a,
  index 
)

Definition at line 11209 of file z3py.py.

11209 def PartialOrder(a, index):
11210  return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx)
11211 
11212 

◆ PbEq()

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

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

Definition at line 8944 of file z3py.py.

8944 def PbEq(args, k, ctx=None):
8945  """Create a Pseudo-Boolean inequality k constraint.
8946 
8947  >>> a, b, c = Bools('a b c')
8948  >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
8949  """
8950  _z3_check_cint_overflow(k, "k")
8951  ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
8952  return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
8953 
8954 

◆ PbGe()

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

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

Definition at line 8933 of file z3py.py.

8933 def PbGe(args, k):
8934  """Create a Pseudo-Boolean inequality k constraint.
8935 
8936  >>> a, b, c = Bools('a b c')
8937  >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
8938  """
8939  _z3_check_cint_overflow(k, "k")
8940  ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
8941  return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
8942 
8943 

◆ PbLe()

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

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

Definition at line 8922 of file z3py.py.

8922 def PbLe(args, k):
8923  """Create a Pseudo-Boolean inequality k constraint.
8924 
8925  >>> a, b, c = Bools('a b c')
8926  >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
8927  """
8928  _z3_check_cint_overflow(k, "k")
8929  ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
8930  return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
8931 
8932 

◆ PiecewiseLinearOrder()

def z3py.PiecewiseLinearOrder (   a,
  index 
)

Definition at line 11221 of file z3py.py.

11221 def PiecewiseLinearOrder(a, index):
11222  return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11223 
11224 

◆ Plus()

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

Definition at line 11127 of file z3py.py.

11127 def Plus(re):
11128  """Create the regular expression accepting one or more repetitions of argument.
11129  >>> re = Plus(Re("a"))
11130  >>> print(simplify(InRe("aa", re)))
11131  True
11132  >>> print(simplify(InRe("ab", re)))
11133  False
11134  >>> print(simplify(InRe("", re)))
11135  False
11136  """
11137  return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
11138 
11139 

◆ PrefixOf()

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

Definition at line 10898 of file z3py.py.

10898 def PrefixOf(a, b):
10899  """Check if 'a' is a prefix of 'b'
10900  >>> s1 = PrefixOf("ab", "abc")
10901  >>> simplify(s1)
10902  True
10903  >>> s2 = PrefixOf("bc", "abc")
10904  >>> simplify(s2)
10905  False
10906  """
10907  ctx = _get_ctx2(a, b)
10908  a = _coerce_seq(a, ctx)
10909  b = _coerce_seq(b, ctx)
10910  return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
10911 
10912 

◆ probe_description()

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

>>> d = probe_description('memory')

Definition at line 8613 of file z3py.py.

8613 def probe_description(name, ctx=None):
8614  """Return a short description for the probe named `name`.
8615 
8616  >>> d = probe_description('memory')
8617  """
8618  ctx = _get_ctx(ctx)
8619  return Z3_probe_get_descr(ctx.ref(), name)
8620 
8621 

Referenced by describe_probes().

◆ probes()

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

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

Definition at line 8602 of file z3py.py.

8602 def probes(ctx=None):
8603  """Return a list of all available probes in Z3.
8604 
8605  >>> l = probes()
8606  >>> l.count('memory') == 1
8607  True
8608  """
8609  ctx = _get_ctx(ctx)
8610  return [Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref()))]
8611 
8612 

Referenced by describe_probes().

◆ Product()

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

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

Definition at line 8829 of file z3py.py.

8829 def Product(*args):
8830  """Create the product of the Z3 expressions.
8831 
8832  >>> a, b, c = Ints('a b c')
8833  >>> Product(a, b, c)
8834  a*b*c
8835  >>> Product([a, b, c])
8836  a*b*c
8837  >>> A = IntVector('a', 5)
8838  >>> Product(A)
8839  a__0*a__1*a__2*a__3*a__4