A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://z3prover.github.io/api/html/namespacez3py.html below:

Z3: z3py Namespace Reference

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  DeclareTypeVar (name, ctx=None)   def  is_func_decl (a)   def  Function (name, *sig)   def  FreshFunction (*sig)   def  RecFunction (name, *sig)   def  RecAddDefinition (f, args, body)   def  deserialize (st)   def  is_expr (a)   def  is_app (a)   def  is_const (a)   def  is_var (a)   def  get_var_index (a)   def  is_app_of (a, k)   def  If (a, b, c, ctx=None)   def  Distinct (*args)   def  Const (name, sort)   def  Consts (names, sort)   def  FreshConst (sort, prefix="c")   def  Var (idx, s)   def  RealVar (idx, ctx=None)   def  RealVarVector (n, ctx=None)   def  is_bool (a)   def  is_true (a)   def  is_false (a)   def  is_and (a)   def  is_or (a)   def  is_implies (a)   def  is_not (a)   def  is_eq (a)   def  is_distinct (a)   def  BoolSort (ctx=None)   def  BoolVal (val, ctx=None)   def  Bool (name, ctx=None)   def  Bools (names, ctx=None)   def  BoolVector (prefix, sz, ctx=None)   def  FreshBool (prefix="b", ctx=None)   def  Implies (a, b, ctx=None)   def  Xor (a, b, ctx=None)   def  Not (a, ctx=None)   def  mk_not (a)   def  And (*args)   def  Or (*args)   def  is_pattern (a)   def  MultiPattern (*args)   def  is_quantifier (a)   def  ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])   def  Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])   def  Lambda (vs, body)   def  is_arith_sort (s)   def  is_arith (a)   def  is_int (a)   def  is_real (a)   def  is_int_value (a)   def  is_rational_value (a)   def  is_algebraic_value (a)   def  is_add (a)   def  is_mul (a)   def  is_sub (a)   def  is_div (a)   def  is_idiv (a)   def  is_mod (a)   def  is_le (a)   def  is_lt (a)   def  is_ge (a)   def  is_gt (a)   def  is_is_int (a)   def  is_to_real (a)   def  is_to_int (a)   def  IntSort (ctx=None)   def  RealSort (ctx=None)   def  IntVal (val, ctx=None)   def  RealVal (val, ctx=None)   def  RatVal (a, b, ctx=None)   def  Q (a, b, ctx=None)   def  Int (name, ctx=None)   def  Ints (names, ctx=None)   def  IntVector (prefix, sz, ctx=None)   def  FreshInt (prefix="x", ctx=None)   def  Real (name, ctx=None)   def  Reals (names, ctx=None)   def  RealVector (prefix, sz, ctx=None)   def  FreshReal (prefix="b", ctx=None)   def  ToReal (a)   def  ToInt (a)   def  IsInt (a)   def  Sqrt (a, ctx=None)   def  Cbrt (a, ctx=None)   def  is_bv_sort (s)   def  is_bv (a)   def  is_bv_value (a)   def  BV2Int (a, is_signed=False)   def  Int2BV (a, num_bits)   def  BitVecSort (sz, ctx=None)   def  BitVecVal (val, bv, ctx=None)   def  BitVec (name, bv, ctx=None)   def  BitVecs (names, bv, ctx=None)   def  Concat (*args)   def  Extract (high, low, a)   def  ULE (a, b)   def  ULT (a, b)   def  UGE (a, b)   def  UGT (a, b)   def  UDiv (a, b)   def  URem (a, b)   def  SRem (a, b)   def  LShR (a, b)   def  RotateLeft (a, b)   def  RotateRight (a, b)   def  SignExt (n, a)   def  ZeroExt (n, a)   def  RepeatBitVec (n, a)   def  BVRedAnd (a)   def  BVRedOr (a)   def  BVAddNoOverflow (a, b, signed)   def  BVAddNoUnderflow (a, b)   def  BVSubNoOverflow (a, b)   def  BVSubNoUnderflow (a, b, signed)   def  BVSDivNoOverflow (a, b)   def  BVSNegNoOverflow (a)   def  BVMulNoOverflow (a, b, signed)   def  BVMulNoUnderflow (a, b)   def  is_array_sort (a)   def  is_array (a)   def  is_const_array (a)   def  is_K (a)   def  is_map (a)   def  is_default (a)   def  get_map_func (a)   def  ArraySort (*sig)   def  Array (name, *sorts)   def  Update (a, *args)   def  Default (a)   def  Store (a, *args)   def  Select (a, *args)   def  Map (f, *args)   def  K (dom, v)   def  Ext (a, b)   def  SetHasSize (a, k)   def  is_select (a)   def  is_store (a)   def  SetSort (s)   Sets. More...
  def  EmptySet (s)   def  FullSet (s)   def  SetUnion (*args)   def  SetIntersect (*args)   def  SetAdd (s, e)   def  SetDel (s, e)   def  SetComplement (s)   def  SetDifference (a, b)   def  IsMember (e, s)   def  IsSubset (a, b)   def  CreateDatatypes (*ds)   def  DatatypeSort (name, ctx=None)   def  TupleSort (name, sorts, ctx=None)   def  DisjointSum (name, sorts, ctx=None)   def  EnumSort (name, values, ctx=None)   def  args2params (arguments, keywords, ctx=None)   def  Model (ctx=None)   def  is_as_array (n)   def  get_as_array_func (n)   def  SolverFor (logic, ctx=None, logFile=None)   def  SimpleSolver (ctx=None, logFile=None)   def  FiniteDomainSort (name, sz, ctx=None)   def  is_finite_domain_sort (s)   def  is_finite_domain (a)   def  FiniteDomainVal (val, sort, ctx=None)   def  is_finite_domain_value (a)   def  AndThen (*ts, **ks)   def  Then (*ts, **ks)   def  OrElse (*ts, **ks)   def  ParOr (*ts, **ks)   def  ParThen (t1, t2, ctx=None)   def  ParAndThen (t1, t2, ctx=None)   def  With (t, *args, **keys)   def  WithParams (t, p)   def  Repeat (t, max=4294967295, ctx=None)   def  TryFor (t, ms, ctx=None)   def  tactics (ctx=None)   def  tactic_description (name, ctx=None)   def  describe_tactics ()   def  is_probe (p)   def  probes (ctx=None)   def  probe_description (name, ctx=None)   def  describe_probes ()   def  FailIf (p, ctx=None)   def  When (p, t, ctx=None)   def  Cond (p, t1, t2, ctx=None)   def  simplify (a, *arguments, **keywords)   Utils. More...
  def  help_simplify ()   def  simplify_param_descrs ()   def  substitute (t, *m)   def  substitute_vars (t, *m)   def  substitute_funs (t, *m)   def  Sum (*args)   def  Product (*args)   def  Abs (arg)   def  AtMost (*args)   def  AtLeast (*args)   def  PbLe (args, k)   def  PbGe (args, k)   def  PbEq (args, k, ctx=None)   def  solve (*args, **keywords)   def  solve_using (s, *args, **keywords)   def  prove (claim, show=False, **keywords)   def  parse_smt2_string (s, sorts={}, decls={}, ctx=None)   def  parse_smt2_file (f, sorts={}, decls={}, ctx=None)   def  get_default_rounding_mode (ctx=None)   def  set_default_rounding_mode (rm, ctx=None)   def  get_default_fp_sort (ctx=None)   def  set_default_fp_sort (ebits, sbits, ctx=None)   def  Float16 (ctx=None)   def  FloatHalf (ctx=None)   def  Float32 (ctx=None)   def  FloatSingle (ctx=None)   def  Float64 (ctx=None)   def  FloatDouble (ctx=None)   def  Float128 (ctx=None)   def  FloatQuadruple (ctx=None)   def  is_fp_sort (s)   def  is_fprm_sort (s)   def  RoundNearestTiesToEven (ctx=None)   def  RNE (ctx=None)   def  RoundNearestTiesToAway (ctx=None)   def  RNA (ctx=None)   def  RoundTowardPositive (ctx=None)   def  RTP (ctx=None)   def  RoundTowardNegative (ctx=None)   def  RTN (ctx=None)   def  RoundTowardZero (ctx=None)   def  RTZ (ctx=None)   def  is_fprm (a)   def  is_fprm_value (a)   def  is_fp (a)   def  is_fp_value (a)   def  FPSort (ebits, sbits, ctx=None)   def  fpNaN (s)   def  fpPlusInfinity (s)   def  fpMinusInfinity (s)   def  fpInfinity (s, negative)   def  fpPlusZero (s)   def  fpMinusZero (s)   def  fpZero (s, negative)   def  FPVal (sig, exp=None, fps=None, ctx=None)   def  FP (name, fpsort, ctx=None)   def  FPs (names, fpsort, ctx=None)   def  fpAbs (a, ctx=None)   def  fpNeg (a, ctx=None)   def  fpAdd (rm, a, b, ctx=None)   def  fpSub (rm, a, b, ctx=None)   def  fpMul (rm, a, b, ctx=None)   def  fpDiv (rm, a, b, ctx=None)   def  fpRem (a, b, ctx=None)   def  fpMin (a, b, ctx=None)   def  fpMax (a, b, ctx=None)   def  fpFMA (rm, a, b, c, ctx=None)   def  fpSqrt (rm, a, ctx=None)   def  fpRoundToIntegral (rm, a, ctx=None)   def  fpIsNaN (a, ctx=None)   def  fpIsInf (a, ctx=None)   def  fpIsZero (a, ctx=None)   def  fpIsNormal (a, ctx=None)   def  fpIsSubnormal (a, ctx=None)   def  fpIsNegative (a, ctx=None)   def  fpIsPositive (a, ctx=None)   def  fpLT (a, b, ctx=None)   def  fpLEQ (a, b, ctx=None)   def  fpGT (a, b, ctx=None)   def  fpGEQ (a, b, ctx=None)   def  fpEQ (a, b, ctx=None)   def  fpNEQ (a, b, ctx=None)   def  fpFP (sgn, exp, sig, ctx=None)   def  fpToFP (a1, a2=None, a3=None, ctx=None)   def  fpBVToFP (v, sort, ctx=None)   def  fpFPToFP (rm, v, sort, ctx=None)   def  fpRealToFP (rm, v, sort, ctx=None)   def  fpSignedToFP (rm, v, sort, ctx=None)   def  fpUnsignedToFP (rm, v, sort, ctx=None)   def  fpToFPUnsigned (rm, x, s, ctx=None)   def  fpToSBV (rm, x, s, ctx=None)   def  fpToUBV (rm, x, s, ctx=None)   def  fpToReal (x, ctx=None)   def  fpToIEEEBV (x, ctx=None)   def  StringSort (ctx=None)   def  CharSort (ctx=None)   def  SeqSort (s)   def  CharVal (ch, ctx=None)   def  CharFromBv (bv)   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  SeqMap (f, s)   def  SeqMapI (f, i, s)   def  SeqFoldLeft (f, a, s)   def  SeqFoldLeftI (f, i, a, s)   def  StrToInt (s)   def  IntToStr (s)   def  StrToCode (s)   def  StrFromCode (c)   def  Re (s, ctx=None)   def  ReSort (s)   def  is_re (s)   def  InRe (s, re)   def  Union (*args)   def  Intersect (*args)   def  Plus (re)   def  Option (re)   def  Complement (re)   def  Star (re)   def  Loop (re, lo, hi=0)   def  Range (lo, hi, ctx=None)   def  Diff (a, b, ctx=None)   def  AllChar (regex_sort, ctx=None)   def  PartialOrder (a, index)   def  LinearOrder (a, index)   def  TreeOrder (a, index)   def  PiecewiseLinearOrder (a, index)   def  TransitiveClosure (f)   def  to_Ast (ptr)   def  to_ContextObj (ptr)   def  to_AstVectorObj (ptr)   def  on_clause_eh (ctx, p, n, dep, clause)   def  ensure_prop_closures ()   def  user_prop_push (ctx, cb)   def  user_prop_pop (ctx, cb, num_scopes)   def  user_prop_fresh (ctx, _new_ctx)   def  user_prop_fixed (ctx, cb, id, value)   def  user_prop_created (ctx, cb, id)   def  user_prop_final (ctx, cb)   def  user_prop_eq (ctx, cb, x, y)   def  user_prop_diseq (ctx, cb, x, y)   def  user_prop_decide (ctx, cb, t, idx, phase)   def  PropagateFunction (name, *sig)   ◆ Abs() 
Create the absolute value of an arithmetic expression

Definition at line 9065 of file z3py.py.

9066  """Create the absolute value of an arithmetic expression""" 9067  return If

(arg > 0, arg, -arg)

def If(a, b, c, ctx=None)

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

Definition at line 11471 of file z3py.py.

11471 def AllChar

(regex_sort, ctx=None):

11472  """Create a regular expression that accepts all single character strings 11474  return

ReRef(

Z3_mk_re_allchar

(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)

Z3_ast Z3_API Z3_mk_re_allchar(Z3_context c, Z3_sort regex_sort)

Create a regular expression that accepts all singleton sequences of the regular expression sort.

def AllChar(regex_sort, ctx=None)

◆ And() 
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 1889 of file z3py.py.

1890  """Create a Z3 and-expression or and-probe. 1892  >>> p, q, r = Bools('p q r') 1895  >>> P = BoolVector('p', 5) 1897  And(p__0, p__1, p__2, p__3, p__4) 1901

last_arg = args[len(args) - 1]

1902  if

isinstance(last_arg, Context):

1903

ctx = args[len(args) - 1]

1904

args = args[:len(args) - 1]

1905  elif

len(args) == 1

and

isinstance(args[0], AstVector):

1907

args = [a

for

a

in

args[0]]

1910

args = _get_args(args)

1911

ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))

1913

_z3_assert(ctx

is not None

,

"At least one of the arguments must be a Z3 expression or probe"

)

1914  if

_has_probe(args):

1915  return

_probe_and(args, ctx)

1917

args = _coerce_expr_list(args, ctx)

1918

_args, sz = _to_ast_array(args)

1919  return

BoolRef(

Z3_mk_and

(ctx.ref(), sz, _args), ctx)

Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] and ... and args[num_args-1].

Referenced by BoolRef.__and__(), 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 8430 of file z3py.py.

8431  """Return a tactic that applies the tactics in `*ts` in sequence. 8433  >>> x, y = Ints('x y') 8434  >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 8435  >>> t(And(x == 0, y > x + 1)) 8437  >>> t(And(x == 0, y > x + 1)).as_expr() 8441

_z3_assert(len(ts) >= 2,

"At least two arguments expected"

)

8442

ctx = ks.get(

"ctx"

,

None

)

8445  for

i

in range

(num - 1):

8446

r = _and_then(r, ts[i + 1], ctx)

expr range(expr const &lo, expr const &hi)

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.

120  """Append user-defined string to interaction log. """

void Z3_API Z3_append_log(Z3_string string)

Append user-defined string to interaction log.

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

5513  """Convert python arguments into a Z3_params object. 5514  A ':' is added to the keywords, and '_' is replaced with '-' 5516  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) 5517  (params model true relevancy 2 elim_and true) 5520

_z3_assert(len(arguments) % 2 == 0,

"Argument list must have an even number of elements."

)

def args2params(arguments, keywords, ctx=None)

Referenced by Tactic.apply(), Solver.set(), Fixedpoint.set(), Optimize.set(), simplify(), Simplifier.using_params(), 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 4779 of file z3py.py.

4779 def Array

(name, *sorts):

4780  """Return an array constant named `name` with the given domain and range sorts. 4782  >>> a = Array('a', IntSort(), IntSort())

Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)

Declare and create a constant.

def to_symbol(s, ctx=None)

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

4747  """Return the Z3 array sort with the given domain and range sorts. 4749  >>> A = ArraySort(IntSort(), BoolSort()) 4756  >>> AA = ArraySort(IntSort(), A) 4758  Array(Int, Array(Int, Bool)) 4760

sig = _get_args(sig)

4762

_z3_assert(len(sig) > 1,

"At least two arguments expected"

)

4763

arity = len(sig) - 1

4768

_z3_assert(

is_sort

(s),

"Z3 sort expected"

)

4769

_z3_assert(s.ctx == r.ctx,

"Context mismatch"

)

4773

dom = (Sort * arity)()

4774  for

i

in range

(arity):

Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)

Create an array type with N arguments.

Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)

Create an array type.

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

◆ AtLeast() def z3py.AtLeast ( *  args ) 
Create an at-least Pseudo-Boolean k constraint.

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

Definition at line 9088 of file z3py.py.

9089  """Create an at-least Pseudo-Boolean k constraint. 9091  >>> a, b, c = Bools('a b c') 9092  >>> f = AtLeast(a, b, c, 2) 9094

args = _get_args(args)

9096

_z3_assert(len(args) > 1,

"Non empty list of arguments expected"

)

9097

ctx = _ctx_from_ast_arg_list(args)

9099

_z3_assert(ctx

is not None

,

"At least one of the arguments must be a Z3 expression"

)

9100

args1 = _coerce_expr_list(args[:-1], ctx)

9102

_args, sz = _to_ast_array(args1)

9103  return

BoolRef(

Z3_mk_atleast

(ctx.ref(), sz, _args, k), ctx)

Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)

Pseudo-Boolean relations.

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

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

Definition at line 9070 of file z3py.py.

9071  """Create an at-most Pseudo-Boolean k constraint. 9073  >>> a, b, c = Bools('a b c') 9074  >>> f = AtMost(a, b, c, 2) 9076

args = _get_args(args)

9078

_z3_assert(len(args) > 1,

"Non empty list of arguments expected"

)

9079

ctx = _ctx_from_ast_arg_list(args)

9081

_z3_assert(ctx

is not None

,

"At least one of the arguments must be a Z3 expression"

)

9082

args1 = _coerce_expr_list(args[:-1], ctx)

9084

_args, sz = _to_ast_array(args1)

9085  return

BoolRef(

Z3_mk_atmost

(ctx.ref(), sz, _args, k), ctx)

Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)

Pseudo-Boolean relations.

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

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

Definition at line 4083 of file z3py.py.

4083 def BitVec

(name, bv, ctx=None):

4084  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. 4085  If `ctx=None`, then the global context is used. 4087  >>> x = BitVec('x', 16) 4094  >>> word = BitVecSort(16) 4095  >>> x2 = BitVec('x', word) 4099  if

isinstance(bv, BitVecSortRef):

def BitVec(name, bv, ctx=None)

def BitVecSort(sz, ctx=None)

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

4107 def BitVecs

(names, bv, ctx=None):

4108  """Return a tuple of bit-vector constants of size bv. 4110  >>> x, y, z = BitVecs('x y z', 16) 4117  >>> Product(x, y, z) 4119  >>> simplify(Product(x, y, z)) 4123  if

isinstance(names, str):

4124

names = names.split(

" "

)

4125  return

[

BitVec

(name, bv, ctx)

for

name

in

names]

def BitVecs(names, bv, ctx=None)

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

4052  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. 4054  >>> Byte = BitVecSort(8) 4055  >>> Word = BitVecSort(16) 4058  >>> x = Const('x', Byte) 4059  >>> eq(x, BitVec('x', 8))

Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)

Create a bit-vector type of the given size.

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

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

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

Definition at line 4066 of file z3py.py.

4067  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. 4069  >>> v = BitVecVal(10, 32) 4072  >>> print("0x%.8x" % v.as_long()) 4077  return

BitVecNumRef(

Z3_mk_numeral

(ctx.ref(), _to_int_str(val), bv.ast), ctx)

Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)

Create a numeral of a given sort.

def BitVecVal(val, bv, ctx=None)

◆ Bool() def z3py.Bool (   name,   ctx = None  ) ◆ 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 1780 of file z3py.py.

1780 def Bools

(names, ctx=None):

1781  """Return a tuple of Boolean constants. 1783  `names` is a single string containing all names separated by blank spaces. 1784  If `ctx=None`, then the global context is used. 1786  >>> p, q, r = Bools('p q r') 1787  >>> And(p, Or(q, r)) 1791  if

isinstance(names, str):

1792

names = names.split(

" "

)

1793  return

[

Bool

(name, ctx)

for

name

in

names]

def Bools(names, ctx=None)

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

1732  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 1736  >>> p = Const('p', BoolSort()) 1739  >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 1742  >>> is_bool(r(0, 1))

Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)

Create the Boolean type.

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

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

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

Definition at line 1749 of file z3py.py.

1750  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. 1754  >>> is_true(BoolVal(True)) 1758  >>> is_false(BoolVal(False))

Z3_ast Z3_API Z3_mk_true(Z3_context c)

Create an AST node representing true.

Z3_ast Z3_API Z3_mk_false(Z3_context c)

Create an AST node representing false.

def BoolVal(val, ctx=None)

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

1797  """Return a list of Boolean constants of size `sz`. 1799  The constants are named using the given prefix. 1800  If `ctx=None`, then the global context is used. 1802  >>> P = BoolVector('p', 3) 1806  And(p__0, p__1, p__2) 1808  return

[

Bool

(

"%s__%s"

% (prefix, i))

for

i

in range

(sz)]

def BoolVector(prefix, sz, ctx=None)

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

4019 def BV2Int

(a, is_signed=False):

4020  """Return the Z3 expression BV2Int(a). 4022  >>> b = BitVec('b', 3) 4023  >>> BV2Int(b).sort() 4028  >>> x > BV2Int(b, is_signed=False) 4030  >>> x > BV2Int(b, is_signed=True) 4031  x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) 4032  >>> solve(x > BV2Int(b), b == 1, x < 3) 4036

_z3_assert(

is_bv

(a),

"First argument must be a Z3 bit-vector expression"

)

4039  return

ArithRef(

Z3_mk_bv2int

(ctx.ref(), a.as_ast(), is_signed), ctx)

Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)

Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...

def BV2Int(a, is_signed=False)

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

Definition at line 4505 of file z3py.py.

4506  """A predicate the determines that bit-vector addition does not overflow""" 4507

_check_bv_args(a, b)

4508

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

def BVAddNoOverflow(a, b, signed)

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

Definition at line 4512 of file z3py.py.

4513  """A predicate the determines that signed bit-vector addition does not underflow""" 4514

_check_bv_args(a, b)

4515

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

def BVAddNoUnderflow(a, b)

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

Definition at line 4547 of file z3py.py.

4548  """A predicate the determines that bit-vector multiplication does not overflow""" 4549

_check_bv_args(a, b)

4550

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

def BVMulNoOverflow(a, b, signed)

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

Definition at line 4554 of file z3py.py.

4555  """A predicate the determines that bit-vector signed multiplication does not underflow""" 4556

_check_bv_args(a, b)

4557

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...

def BVMulNoUnderflow(a, b)

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

Definition at line 4491 of file z3py.py.

4492  """Return the reduction-and expression of `a`.""" 4494

_z3_assert(

is_bv

(a),

"First argument must be a Z3 bit-vector expression"

)

4495  return

BitVecRef(

Z3_mk_bvredand

(a.ctx_ref(), a.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)

Take conjunction of bits in vector, return vector of length 1.

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

Definition at line 4498 of file z3py.py.

4499  """Return the reduction-or expression of `a`.""" 4501

_z3_assert(

is_bv

(a),

"First argument must be a Z3 bit-vector expression"

)

4502  return

BitVecRef(

Z3_mk_bvredor

(a.ctx_ref(), a.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)

Take disjunction of bits in vector, return vector of length 1.

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

Definition at line 4533 of file z3py.py.

4534  """A predicate the determines that bit-vector signed division does not overflow""" 4535

_check_bv_args(a, b)

4536

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

def BVSDivNoOverflow(a, b)

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

Definition at line 4540 of file z3py.py.

4541  """A predicate the determines that bit-vector unary negation does not overflow""" 4543

_z3_assert(

is_bv

(a),

"First argument must be a Z3 bit-vector expression"

)

Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

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

Definition at line 4519 of file z3py.py.

4520  """A predicate the determines that bit-vector subtraction does not overflow""" 4521

_check_bv_args(a, b)

4522

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

def BVSubNoOverflow(a, b)

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

Definition at line 4526 of file z3py.py.

4527  """A predicate the determines that bit-vector subtraction does not underflow""" 4528

_check_bv_args(a, b)

4529

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

def BVSubNoUnderflow(a, b, signed)

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

3470 def Cbrt

(a, ctx=None):

3471  """ Return a Z3 expression which represents the cubic root of a.

def RealVal(val, ctx=None)

◆ CharFromBv() def z3py.CharFromBv (   bv )

Definition at line 10989 of file z3py.py.

10991  raise

Z3Exception(

"Bit-vector expression needed"

)

Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)

Create a character from a bit-vector (code point).

◆ CharIsDigit() def z3py.CharIsDigit (   ch,   ctx = None  )

Definition at line 11002 of file z3py.py.

11003

ch = _coerce_char(ch, ctx)

11004  return

ch.is_digit()

def CharIsDigit(ch, ctx=None)

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

Definition at line 10888 of file z3py.py.

10889  """Create a character sort 10890  >>> ch = CharSort() 10894

ctx = _get_ctx(ctx)

Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)

Create a sort for unicode characters.

Referenced by Context.mkCharSort().

◆ CharToBv() def z3py.CharToBv (   ch,   ctx = None  )

Definition at line 10994 of file z3py.py.

10995

ch = _coerce_char(ch, ctx)

def CharToBv(ch, ctx=None)

◆ CharToInt() def z3py.CharToInt (   ch,   ctx = None  )

Definition at line 10998 of file z3py.py.

10999

ch = _coerce_char(ch, ctx)

def CharToInt(ch, ctx=None)

◆ CharVal() def z3py.CharVal (   ch,   ctx = None  )

Definition at line 10981 of file z3py.py.

10982

ctx = _get_ctx(ctx)

10983  if

isinstance(ch, str):

10985  if not

isinstance(ch, int):

10986  raise

Z3Exception(

"character value should be an ordinal"

)

10987  return

_to_expr_ref(

Z3_mk_char

(ctx.ref(), ch), ctx)

Z3_ast Z3_API Z3_mk_char(Z3_context c, unsigned ch)

Create a character literal.

def CharVal(ch, ctx=None)

Referenced by SeqRef.__gt__().

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

Definition at line 11413 of file z3py.py.

11414  """Create the complement regular expression."""

Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)

Create the complement of the regular language re.

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

4129  """Create a Z3 bit-vector concatenation expression. 4131  >>> v = BitVecVal(1, 4) 4132  >>> Concat(v, v+1, v) 4133  Concat(Concat(1, 1 + 1), 1) 4134  >>> simplify(Concat(v, v+1, v)) 4136  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 4139

args = _get_args(args)

4142

_z3_assert(sz >= 2,

"At least two arguments expected."

)

4149  if is_seq

(args[0])

or

isinstance(args[0], str):

4150

args = [_coerce_seq(s, ctx)

for

s

in

args]

4152

_z3_assert(all([

is_seq

(a)

for

a

in

args]),

"All arguments must be sequence expressions."

)

4154  for

i

in range

(sz):

4155

v[i] = args[i].as_ast()

4160

_z3_assert(all([

is_re

(a)

for

a

in

args]),

"All arguments must be regular expressions."

)

4162  for

i

in range

(sz):

4163

v[i] = args[i].as_ast()

4167

_z3_assert(all([

is_bv

(a)

for

a

in

args]),

"All arguments must be Z3 bit-vector expressions."

)

4169  for

i

in range

(sz - 1):

4170

r = BitVecRef(

Z3_mk_concat

(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)

Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])

Concatenate sequences.

Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])

Create the concatenation of the regular languages.

Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)

Concatenate the given bit-vectors.

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

8887 def Cond

(p, t1, t2, ctx=None):

8888  """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 8890  >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 8892

p = _to_probe(p, ctx)

8893

t1 = _to_tactic(t1, ctx)

8894

t2 = _to_tactic(t2, ctx)

8895  return

Tactic(

Z3_tactic_cond

(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)

Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)

Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...

def Cond(p, t1, t2, ctx=None)

Referenced by If().

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

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

Definition at line 1455 of file z3py.py.

1455 def Const

(name, sort):

1456  """Create a constant of the given sort. 1458  >>> Const('x', IntSort()) 1462

_z3_assert(isinstance(sort, SortRef),

"Z3 sort expected"

)

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

1467 def Consts

(names, sort):

1468  """Create several constants of the given sort. 1470  `names` is a string containing the names of all constants to be created. 1471  Blank spaces separate the names of different constants. 1473  >>> x, y, z = Consts('x y z', IntSort()) 1477  if

isinstance(names, str):

1478

names = names.split(

" "

)

1479  return

[

Const

(name, sort)

for

name

in

names]

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

11159  """Check if 'a' contains 'b' 11160  >>> s1 = Contains("abc", "ab") 11163  >>> s2 = Contains("abc", "bc") 11166  >>> x, y, z = Strings('x y z') 11167  >>> s3 = Contains(Concat(x,y,z), y) 11171

ctx = _get_ctx2(a, b)

11172

a = _coerce_seq(a, ctx)

11173

b = _coerce_seq(b, ctx)

Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)

Check if container contains containee.

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

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

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

Definition at line 5204 of file z3py.py.

5205  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. 5207  In the following example we define a Tree-List using two mutually recursive datatypes. 5209  >>> TreeList = Datatype('TreeList') 5210  >>> Tree = Datatype('Tree') 5211  >>> # Tree has two constructors: leaf and node 5212  >>> Tree.declare('leaf', ('val', IntSort())) 5213  >>> # a node contains a list of trees 5214  >>> Tree.declare('node', ('children', TreeList)) 5215  >>> TreeList.declare('nil') 5216  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) 5217  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) 5218  >>> Tree.val(Tree.leaf(10)) 5220  >>> simplify(Tree.val(Tree.leaf(10))) 5222  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) 5224  node(cons(leaf(10), cons(leaf(20), nil))) 5225  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) 5226  >>> simplify(n2 == n1) 5228  >>> simplify(TreeList.car(Tree.children(n2)) == n1) 5233

_z3_assert(len(ds) > 0,

"At least one Datatype must be specified"

)

5234

_z3_assert(all([isinstance(d, Datatype)

for

d

in

ds]),

"Arguments must be Datatypes"

)

5235

_z3_assert(all([d.ctx == ds[0].ctx

for

d

in

ds]),

"Context mismatch"

)

5236

_z3_assert(all([d.constructors != []

for

d

in

ds]),

"Non-empty Datatypes expected"

)

5239

names = (Symbol * num)()

5240

out = (Sort * num)()

5241

clists = (ConstructorList * num)()

5243  for

i

in range

(num):

5246

num_cs = len(d.constructors)

5247

cs = (Constructor * num_cs)()

5248  for

j

in range

(num_cs):

5249

c = d.constructors[j]

5254

fnames = (Symbol * num_fs)()

5255

sorts = (Sort * num_fs)()

5256

refs = (ctypes.c_uint * num_fs)()

5257  for

k

in range

(num_fs):

5261  if

isinstance(ftype, Datatype):

5264

ds.count(ftype) == 1,

5265  "One and only one occurrence of each datatype is expected"

,

5268

refs[k] = ds.index(ftype)

5271

_z3_assert(

is_sort

(ftype),

"Z3 sort expected"

)

5272

sorts[k] = ftype.ast

5274

cs[j] =

Z3_mk_constructor

(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)

5275

to_delete.append(ScopedConstructor(cs[j], ctx))

5277

to_delete.append(ScopedConstructorList(clists[i], ctx))

5281  for

i

in range

(num):

5282

dref = DatatypeSortRef(out[i], ctx)

5283

num_cs = dref.num_constructors()

5284  for

j

in range

(num_cs):

5285

cref = dref.constructor(j)

5286

cref_name = cref.name()

5287

cref_arity = cref.arity()

5288  if

cref.arity() == 0:

5290

setattr(dref, cref_name, cref)

5291

rref = dref.recognizer(j)

5292

setattr(dref,

"is_"

+ cref_name, rref)

5293  for

k

in range

(cref_arity):

5294

aref = dref.accessor(j, k)

5295

setattr(dref, aref.name(), aref)

5297  return

tuple(result)

Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])

Create a constructor.

void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])

Create mutually recursive datatypes.

Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])

Create list of constructors.

Referenced by Datatype.create().

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

Definition at line 5404 of file z3py.py.

5405  """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""

Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)

create a forward reference to a recursive datatype being declared. The forward reference can be used ...

def DatatypeSort(name, ctx=None)

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

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

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

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

Definition at line 695 of file z3py.py.

696  """Create a new uninterpreted sort named `name`. 698  If `ctx=None`, then the new sort is declared in the global Z3Py context. 700  >>> A = DeclareSort('A') 701  >>> a = Const('a', A) 702  >>> b = Const('b', A)

Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)

Create a free (uninterpreted) type using the given name (symbol).

def DeclareSort(name, ctx=None)

◆ DeclareTypeVar() def z3py.DeclareTypeVar (   name,   ctx = None  ) 
Create a new type variable named `name`.

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

Definition at line 723 of file z3py.py.

724  """Create a new type variable named `name`. 726  If `ctx=None`, then the new sort is declared in the global Z3Py context.

Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol s)

Create a type variable.

def DeclareTypeVar(name, ctx=None)

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

Definition at line 4825 of file z3py.py.

4826  """ Return a default value for array expression. 4827  >>> b = K(IntSort(), 1) 4828  >>> prove(Default(b) == 1) 4832

_z3_assert(

is_array_sort

(a),

"First argument must be a Z3 array expression"

)

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

Definition at line 8808 of file z3py.py.

8809  """Display a (tabular) description of all available probes in Z3.""" 8812

print(

'<table border="1" cellpadding="2" cellspacing="0">'

)

8815

print(

'<tr style="background-color:#CFCFCF">'

)

8820

print(

"<td>%s</td><td>%s</td></tr>"

% (p, insert_line_breaks(

probe_description

(p), 40)))

def probe_description(name, ctx=None)

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

Definition at line 8602 of file z3py.py.

8603  """Display a (tabular) description of all available tactics in Z3.""" 8606

print(

'<table border="1" cellpadding="2" cellspacing="0">'

)

8609

print(

'<tr style="background-color:#CFCFCF">'

)

8614

print(

"<td>%s</td><td>%s</td></tr>"

% (t, insert_line_breaks(

tactic_description

(t), 40)))

def tactic_description(name, ctx=None)

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

1138  """inverse function to the serialize method on ExprRef. 1139  It is made available to make it easier for users to serialize expressions back and forth between 1140  strings. Solvers can be serialized using the 'sexpr()' method. 1144  if

len(s.assertions()) != 1:

1145  raise

Z3Exception(

"single assertion expected"

)

1146

fml = s.assertions()[0]

1147  if

fml.num_args() != 1:

1148  raise

Z3Exception(

"dummy function 'F' expected"

)

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

Definition at line 11463 of file z3py.py.

11463 def Diff

(a, b, ctx=None):

11464  """Create the difference regular expression 11467

_z3_assert(

is_expr

(a),

"expression expected"

)

11468

_z3_assert(

is_expr

(b),

"expression expected"

)

11469  return

ReRef(

Z3_mk_re_diff

(a.ctx_ref(), a.ast, b.ast), a.ctx)

Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)

Create the difference of regular expressions.

◆ disable_trace() def z3py.disable_trace (   msg )

Definition at line 79 of file z3py.py.

void Z3_API Z3_disable_trace(Z3_string tag)

Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.

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

5422  """Create a named tagged union sort base on a set of underlying sorts 5424  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()]) 5426

sum = Datatype(name, ctx)

5427  for

i

in range

(len(sorts)):

5428

sum.declare(

"inject%d"

% i, (

"project%d"

% i, sorts[i]))

5430  return

sum, [(sum.constructor(i), sum.accessor(i, 0))

for

i

in range

(len(sorts))]

def DisjointSum(name, sorts, ctx=None)

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

1423  """Create a Z3 distinct expression. 1430  >>> Distinct(x, y, z) 1432  >>> simplify(Distinct(x, y, z)) 1434  >>> simplify(Distinct(x, y, z), blast_distinct=True) 1435  And(Not(x == y), Not(x == z), Not(y == z)) 1437

args = _get_args(args)

1438

ctx = _ctx_from_ast_arg_list(args)

1440

_z3_assert(ctx

is not None

,

"At least one of the arguments must be a Z3 expression"

)

1441

args = _coerce_expr_list(args, ctx)

1442

_args, sz = _to_ast_array(args)

Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing distinct(args[0], ..., args[num_args-1]).

◆ Empty() 
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 11088 of file z3py.py.

11089  """Create the empty sequence of the given sort 11090  >>> e = Empty(StringSort()) 11091  >>> e2 = StringVal("") 11092  >>> print(e.eq(e2)) 11094  >>> e3 = Empty(SeqSort(IntSort())) 11097  >>> e4 = Empty(ReSort(SeqSort(IntSort()))) 11099  Empty(ReSort(Seq(Int))) 11101  if

isinstance(s, SeqSortRef):

11103  if

isinstance(s, ReSortRef):

11105  raise

Z3Exception(

"Non-sequence, non-regular expression sort passed to Empty"

)

Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)

Create an empty sequence of the sequence sort seq.

Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)

Create an empty regular expression of sort re.

◆ EmptySet() 
Create the empty set
>>> EmptySet(IntSort())
K(Int, False)

Definition at line 4968 of file z3py.py.

4969  """Create the empty set 4970  >>> EmptySet(IntSort())

Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)

Create the empty set.

◆ enable_trace() def z3py.enable_trace (   msg )

Definition at line 75 of file z3py.py.

void Z3_API Z3_enable_trace(Z3_string tag)

Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.

◆ ensure_prop_closures() def z3py.ensure_prop_closures ( )

Definition at line 11582 of file z3py.py.

11583  global

_prop_closures

11584  if

_prop_closures

is None

:

11585

_prop_closures = PropClosures()

def ensure_prop_closures()

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

5433 def EnumSort

(name, values, ctx=None):

5434  """Return a new enumeration sort named `name` containing the given values. 5436  The result is a pair (sort, list of constants). 5438  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue']) 5441

_z3_assert(isinstance(name, str),

"Name must be a string"

)

5442

_z3_assert(all([isinstance(v, str)

for

v

in

values]),

"Enumeration sort values must be strings"

)

5443

_z3_assert(len(values) > 0,

"At least one value expected"

)

5446

_val_names = (Symbol * num)()

5447  for

i

in range

(num):

5448

_val_names[i] =

to_symbol

(values[i], ctx)

5449

_values = (FuncDecl * num)()

5450

_testers = (FuncDecl * num)()

5454  for

i

in range

(num):

5455

V.append(FuncDeclRef(_values[i], ctx))

5456

V = [a()

for

a

in

V]

Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])

Create a enumeration sort.

def EnumSort(name, values, ctx=None)

Referenced by Context.MkEnumSort().

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

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

Definition at line 472 of file z3py.py.

473  """Return `True` if `a` and `b` are structurally identical AST nodes. 483  >>> eq(simplify(x + 1), simplify(1 + x)) 487

_z3_assert(

is_ast

(a)

and is_ast

(b),

"Z3 ASTs expected"

)

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

2290 def Exists

(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):

2291  """Create a Z3 exists formula. 2293  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. 2296  >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2299  >>> q = Exists([x, y], f(x, y) >= x, skid="foo") 2301  Exists([x, y], f(x, y) >= x) 2302  >>> is_quantifier(q) 2304  >>> r = Tactic('nnf')(q).as_expr() 2305  >>> is_quantifier(r) 2308  return

_mk_quantifier(

False

, vs, body, weight, qid, skid, patterns, no_patterns)

def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])

Referenced by Fixedpoint.abstract().

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

Definition at line 4914 of file z3py.py.

4915  """Return extensionality index for one-dimensional arrays. 4916  >> a, b = Consts('a b', SetSort(IntSort())) 4923  return

_to_expr_ref(

Z3_mk_array_ext

(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...

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

4175  """Create a Z3 bit-vector extraction expression. 4176  Extract is overloaded to also work on sequence extraction. 4177  The functions SubString and SubSeq are redirected to Extract. 4178  For this case, the arguments are reinterpreted as: 4179  high - is a sequence (string) 4181  a - is the length to be extracted 4183  >>> x = BitVec('x', 8) 4184  >>> Extract(6, 2, x) 4186  >>> Extract(6, 2, x).sort() 4188  >>> simplify(Extract(StringVal("abcd"),2,1)) 4191  if

isinstance(high, str):

4195

offset, length = _coerce_exprs(low, a, s.ctx)

4196  return

SeqRef(

Z3_mk_seq_extract

(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)

4198

_z3_assert(low <= high,

"First argument must be greater than or equal to second argument"

)

4199

_z3_assert(_is_int(high)

and

high >= 0

and

_is_int(low)

and

low >= 0,

4200  "First and second arguments must be non negative integers"

)

4201

_z3_assert(

is_bv

(a),

"Third argument must be a Z3 bit-vector expression"

)

4202  return

BitVecRef(

Z3_mk_extract

(a.ctx_ref(), high, low, a.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)

Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...

Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)

Extract subsequence starting at offset of length.

def Extract(high, low, a)

def StringVal(s, ctx=None)

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

8845 def FailIf

(p, ctx=None):

8846  """Return a tactic that fails if the probe `p` evaluates to true. 8847  Otherwise, it returns the input goal unmodified. 8849  In the following example, the tactic applies 'simplify' if and only if there are 8850  more than 2 constraints in the goal. 8852  >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 8853  >>> x, y = Ints('x y') 8859  >>> g.add(x == y + 1) 8861  [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8863

p = _to_probe(p, ctx)

Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)

Return a tactic that fails if the probe p evaluates to false.

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

Definition at line 7783 of file z3py.py.

7784  """Create a named finite domain sort of a given size sz""" 7785  if not

isinstance(name, Symbol):

Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)

Create a named finite domain sort.

def FiniteDomainSort(name, sz, ctx=None)

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

7854  """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 7856  >>> s = FiniteDomainSort('S', 256) 7857  >>> FiniteDomainVal(255, s) 7859  >>> FiniteDomainVal('100', s) 7865  return

FiniteDomainNumRef(

Z3_mk_numeral

(ctx.ref(), _to_int_str(val), sort.ast), ctx)

def FiniteDomainVal(val, sort, ctx=None)

def is_finite_domain_sort(s)

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

Definition at line 9573 of file z3py.py.

9574  """Floating-point 128-bit (quadruple) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c)

Create the quadruple-precision (128-bit) FloatingPoint sort.

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

Definition at line 9537 of file z3py.py.

9538  """Floating-point 16-bit (half) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c)

Create the half-precision (16-bit) FloatingPoint sort.

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

Definition at line 9549 of file z3py.py.

9550  """Floating-point 32-bit (single) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c)

Create the single-precision (32-bit) FloatingPoint sort.

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

Definition at line 9561 of file z3py.py.

9562  """Floating-point 64-bit (double) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c)

Create the double-precision (64-bit) FloatingPoint sort.

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

Definition at line 9567 of file z3py.py.

9568  """Floating-point 64-bit (double) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)

Create the double-precision (64-bit) FloatingPoint sort.

def FloatDouble(ctx=None)

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

Definition at line 9543 of file z3py.py.

9544  """Floating-point 16-bit (half) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c)

Create the half-precision (16-bit) FloatingPoint sort.

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

Definition at line 9579 of file z3py.py.

9580  """Floating-point 128-bit (quadruple) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c)

Create the quadruple-precision (128-bit) FloatingPoint sort.

def FloatQuadruple(ctx=None)

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

Definition at line 9555 of file z3py.py.

9556  """Floating-point 32-bit (single) sort."""

Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c)

Create the single-precision (32-bit) FloatingPoint sort.

def FloatSingle(ctx=None)

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

2272 def ForAll

(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):

2273  """Create a Z3 forall formula. 2275  The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations. 2277  >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2280  >>> ForAll([x, y], f(x, y) >= x) 2281  ForAll([x, y], f(x, y) >= x) 2282  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ]) 2283  ForAll([x, y], f(x, y) >= x) 2284  >>> ForAll([x, y], f(x, y) >= x, weight=10) 2285  ForAll([x, y], f(x, y) >= x) 2287  return

_mk_quantifier(

True

, vs, body, weight, qid, skid, patterns, no_patterns)

def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])

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

10205 def FP

(name, fpsort, ctx=None):

10206  """Return a floating-point constant named `name`. 10207  `fpsort` is the floating-point sort. 10208  If `ctx=None`, then the global context is used. 10210  >>> x = FP('x', FPSort(8, 24)) 10217  >>> word = FPSort(8, 24) 10218  >>> x2 = FP('x', word) 10222  if

isinstance(fpsort, FPSortRef)

and

ctx

is None

:

10225

ctx = _get_ctx(ctx)

def FP(name, fpsort, ctx=None)

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

10248 def fpAbs

(a, ctx=None):

10249  """Create a Z3 floating-point absolute value expression. 10251  >>> s = FPSort(8, 24) 10253  >>> x = FPVal(1.0, s) 10256  >>> y = FPVal(-20.0, s) 10260  fpAbs(-1.25*(2**4)) 10261  >>> fpAbs(-1.25*(2**4)) 10262  fpAbs(-1.25*(2**4)) 10263  >>> fpAbs(x).sort() 10266

ctx = _get_ctx(ctx)

10267

[a] = _coerce_fp_expr_list([a], ctx)

Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)

Floating-point absolute value.

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

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

Definition at line 10339 of file z3py.py.

10339 def fpAdd

(rm, a, b, ctx=None):

10340  """Create a Z3 floating-point addition expression. 10342  >>> s = FPSort(8, 24) 10346  >>> fpAdd(rm, x, y) 10348  >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ 10350  >>> fpAdd(rm, x, y).sort() 10353  return

_mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)

def fpAdd(rm, a, b, ctx=None)

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

10662  """Create a Z3 floating-point conversion expression that represents the 10663  conversion from a bit-vector term to a floating-point term. 10665  >>> x_bv = BitVecVal(0x3F800000, 32) 10666  >>> x_fp = fpBVToFP(x_bv, Float32()) 10672

_z3_assert(

is_bv

(v),

"First argument must be a Z3 bit-vector expression"

)

10673

_z3_assert(

is_fp_sort

(sort),

"Second argument must be a Z3 floating-point sort."

)

10674

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

def fpBVToFP(v, sort, ctx=None)

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

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

Definition at line 10386 of file z3py.py.

10386 def fpDiv

(rm, a, b, ctx=None):

10387  """Create a Z3 floating-point division expression. 10389  >>> s = FPSort(8, 24) 10393  >>> fpDiv(rm, x, y) 10395  >>> fpDiv(rm, x, y).sort() 10398  return

_mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)

def fpDiv(rm, a, b, ctx=None)

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

10569 def fpEQ

(a, b, ctx=None):

10570  """Create the Z3 floating-point expression `fpEQ(other, self)`. 10572  >>> x, y = FPs('x y', FPSort(8, 24)) 10575  >>> fpEQ(x, y).sexpr() 10578  return

_mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)

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

10445 def fpFMA

(rm, a, b, c, ctx=None):

10446  """Create a Z3 floating-point fused multiply-add expression. 10448  return

_mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)

def fpFMA(rm, a, b, c, ctx=None)

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

10593 def fpFP

(sgn, exp, sig, ctx=None):

10594  """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. 10596  >>> s = FPSort(8, 24) 10597  >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) 10599  fpFP(1, 127, 4194304) 10600  >>> xv = FPVal(-1.5, s) 10603  >>> slvr = Solver() 10604  >>> slvr.add(fpEQ(x, xv)) 10607  >>> xv = FPVal(+1.5, s) 10610  >>> slvr = Solver() 10611  >>> slvr.add(fpEQ(x, xv)) 10615

_z3_assert(

is_bv

(sgn)

and is_bv

(exp)

and is_bv

(sig),

"sort mismatch"

)

10616

_z3_assert(sgn.sort().size() == 1,

"sort mismatch"

)

10617

ctx = _get_ctx(ctx)

10618

_z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx,

"context mismatch"

)

10619  return

FPRef(

Z3_mk_fpa_fp

(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)

Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)

Create an expression of FloatingPoint sort from three bit-vector expressions.

def fpFP(sgn, exp, sig, ctx=None)

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

10678 def fpFPToFP

(rm, v, sort, ctx=None):

10679  """Create a Z3 floating-point conversion expression that represents the 10680  conversion from a floating-point term to a floating-point term of different precision. 10682  >>> x_sgl = FPVal(1.0, Float32()) 10683  >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) 10686  >>> simplify(x_dbl) 10691

_z3_assert(

is_fprm

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10692

_z3_assert(

is_fp

(v),

"Second argument must be a Z3 floating-point expression."

)

10693

_z3_assert(

is_fp_sort

(sort),

"Third argument must be a Z3 floating-point sort."

)

10694

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

def fpFPToFP(rm, v, sort, ctx=None)

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

10557 def fpGEQ

(a, b, ctx=None):

10558  """Create the Z3 floating-point expression `other >= self`. 10560  >>> x, y = FPs('x y', FPSort(8, 24)) 10563  >>> (x >= y).sexpr() 10566  return

_mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)

def fpGEQ(a, b, ctx=None)

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

10545 def fpGT

(a, b, ctx=None):

10546  """Create the Z3 floating-point expression `other > self`. 10548  >>> x, y = FPs('x y', FPSort(8, 24)) 10551  >>> (x > y).sexpr() 10554  return

_mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)

Referenced by FPRef.__gt__().

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

Definition at line 10133 of file z3py.py.

10134  """Create a Z3 floating-point +oo or -oo term.""" 10135

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10136

_z3_assert(isinstance(negative, bool),

"expected Boolean flag"

)

10137  return

FPNumRef(

Z3_mk_fpa_inf

(s.ctx_ref(), s.ast, negative), s.ctx)

Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)

Create a floating-point infinity of sort s.

def fpInfinity(s, negative)

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

10476  """Create a Z3 floating-point isInfinite expression. 10478  >>> s = FPSort(8, 24) 10483  return

_mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)

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

10464  """Create a Z3 floating-point isNaN expression. 10466  >>> s = FPSort(8, 24) 10472  return

_mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)

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

Definition at line 10504 of file z3py.py.

10505  """Create a Z3 floating-point isNegative expression. 10507  return

_mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)

def fpIsNegative(a, ctx=None)

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

Definition at line 10492 of file z3py.py.

10493  """Create a Z3 floating-point isNormal expression. 10495  return

_mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)

def fpIsNormal(a, ctx=None)

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

Definition at line 10510 of file z3py.py.

10511  """Create a Z3 floating-point isPositive expression. 10513  return

_mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)

def fpIsPositive(a, ctx=None)

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

Definition at line 10498 of file z3py.py.

10499  """Create a Z3 floating-point isSubnormal expression. 10501  return

_mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)

def fpIsSubnormal(a, ctx=None)

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

Definition at line 10486 of file z3py.py.

10487  """Create a Z3 floating-point isZero expression. 10489  return

_mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)

def fpIsZero(a, ctx=None)

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

10533 def fpLEQ

(a, b, ctx=None):

10534  """Create the Z3 floating-point expression `other <= self`. 10536  >>> x, y = FPs('x y', FPSort(8, 24)) 10539  >>> (x <= y).sexpr() 10542  return

_mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)

def fpLEQ(a, b, ctx=None)

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

10521 def fpLT

(a, b, ctx=None):

10522  """Create the Z3 floating-point expression `other < self`. 10524  >>> x, y = FPs('x y', FPSort(8, 24)) 10527  >>> (x < y).sexpr() 10530  return

_mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)

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

10430 def fpMax

(a, b, ctx=None):

10431  """Create a Z3 floating-point maximum expression. 10433  >>> s = FPSort(8, 24) 10439  >>> fpMax(x, y).sort() 10442  return

_mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)

def fpMax(a, b, ctx=None)

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

10415 def fpMin

(a, b, ctx=None):

10416  """Create a Z3 floating-point minimum expression. 10418  >>> s = FPSort(8, 24) 10424  >>> fpMin(x, y).sort() 10427  return

_mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)

def fpMin(a, b, ctx=None)

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

Definition at line 10127 of file z3py.py.

10128  """Create a Z3 floating-point -oo term.""" 10129

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10130  return

FPNumRef(

Z3_mk_fpa_inf

(s.ctx_ref(), s.ast,

True

), s.ctx)

Referenced by FPVal().

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

Definition at line 10146 of file z3py.py.

10147  """Create a Z3 floating-point -0.0 term.""" 10148

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10149  return

FPNumRef(

Z3_mk_fpa_zero

(s.ctx_ref(), s.ast,

True

), s.ctx)

Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)

Create a floating-point zero of sort s.

Referenced by FPVal().

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

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

Definition at line 10371 of file z3py.py.

10371 def fpMul

(rm, a, b, ctx=None):

10372  """Create a Z3 floating-point multiplication expression. 10374  >>> s = FPSort(8, 24) 10378  >>> fpMul(rm, x, y) 10380  >>> fpMul(rm, x, y).sort() 10383  return

_mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)

def fpMul(rm, a, b, ctx=None)

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

◆ fpNaN() 
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 10093 of file z3py.py.

10094  """Create a Z3 floating-point NaN term. 10096  >>> s = FPSort(8, 24) 10097  >>> set_fpa_pretty(True) 10100  >>> pb = get_fpa_pretty() 10101  >>> set_fpa_pretty(False) 10103  fpNaN(FPSort(8, 24)) 10104  >>> set_fpa_pretty(pb) 10106

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10107  return

FPNumRef(

Z3_mk_fpa_nan

(s.ctx_ref(), s.ast), s.ctx)

Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)

Create a floating-point NaN of sort s.

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

10271 def fpNeg

(a, ctx=None):

10272  """Create a Z3 floating-point addition expression. 10274  >>> s = FPSort(8, 24) 10279  >>> fpNeg(x).sort() 10282

ctx = _get_ctx(ctx)

10283

[a] = _coerce_fp_expr_list([a], ctx)

Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)

Floating-point negation.

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

10581 def fpNEQ

(a, b, ctx=None):

10582  """Create the Z3 floating-point expression `Not(fpEQ(other, self))`. 10584  >>> x, y = FPs('x y', FPSort(8, 24)) 10587  >>> (x != y).sexpr() 10590  return Not

(

fpEQ

(a, b, ctx))

def fpNEQ(a, b, ctx=None)

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

10111  """Create a Z3 floating-point +oo term. 10113  >>> s = FPSort(8, 24) 10114  >>> pb = get_fpa_pretty() 10115  >>> set_fpa_pretty(True) 10116  >>> fpPlusInfinity(s) 10118  >>> set_fpa_pretty(False) 10119  >>> fpPlusInfinity(s) 10120  fpPlusInfinity(FPSort(8, 24)) 10121  >>> set_fpa_pretty(pb) 10123

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10124  return

FPNumRef(

Z3_mk_fpa_inf

(s.ctx_ref(), s.ast,

False

), s.ctx)

Referenced by FPVal().

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

Definition at line 10140 of file z3py.py.

10141  """Create a Z3 floating-point +0.0 term.""" 10142

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10143  return

FPNumRef(

Z3_mk_fpa_zero

(s.ctx_ref(), s.ast,

False

), s.ctx)

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

10699  """Create a Z3 floating-point conversion expression that represents the 10700  conversion from a real term to a floating-point term. 10702  >>> x_r = RealVal(1.5) 10703  >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) 10709

_z3_assert(

is_fprm

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10710

_z3_assert(

is_real

(v),

"Second argument must be a Z3 expression or real sort."

)

10711

_z3_assert(

is_fp_sort

(sort),

"Third argument must be a Z3 floating-point sort."

)

10712

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a term of real sort into a term of FloatingPoint sort.

def fpRealToFP(rm, v, sort, ctx=None)

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

10401 def fpRem

(a, b, ctx=None):

10402  """Create a Z3 floating-point remainder expression. 10404  >>> s = FPSort(8, 24) 10409  >>> fpRem(x, y).sort() 10412  return

_mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)

def fpRem(a, b, ctx=None)

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

10458  """Create a Z3 floating-point roundToIntegral expression. 10460  return

_mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)

def fpRoundToIntegral(rm, a, ctx=None)

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

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

Definition at line 10229 of file z3py.py.

10229 def FPs

(names, fpsort, ctx=None):

10230  """Return an array of floating-point constants. 10232  >>> x, y, z = FPs('x y z', FPSort(8, 24)) 10239  >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) 10242

ctx = _get_ctx(ctx)

10243  if

isinstance(names, str):

10244

names = names.split(

" "

)

10245  return

[

FP

(name, fpsort, ctx)

for

name

in

names]

def FPs(names, fpsort, ctx=None)

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

10717  """Create a Z3 floating-point conversion expression that represents the 10718  conversion from a signed bit-vector term (encoding an integer) to a floating-point term. 10720  >>> x_signed = BitVecVal(-5, BitVecSort(32)) 10721  >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) 10723  fpToFP(RNE(), 4294967291) 10727

_z3_assert(

is_fprm

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10728

_z3_assert(

is_bv

(v),

"Second argument must be a Z3 bit-vector expression"

)

10729

_z3_assert(

is_fp_sort

(sort),

"Third argument must be a Z3 floating-point sort."

)

10730

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

def fpSignedToFP(rm, v, sort, ctx=None)

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

10034 def FPSort

(ebits, sbits, ctx=None):

10035  """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used. 10037  >>> Single = FPSort(8, 24) 10038  >>> Double = FPSort(11, 53) 10041  >>> x = Const('x', Single) 10042  >>> eq(x, FP('x', FPSort(8, 24))) 10045

ctx = _get_ctx(ctx)

10046  return

FPSortRef(

Z3_mk_fpa_sort

(ctx.ref(), ebits, sbits), ctx)

Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)

Create a FloatingPoint sort.

def FPSort(ebits, sbits, ctx=None)

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

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

Definition at line 10451 of file z3py.py.

10451 def fpSqrt

(rm, a, ctx=None):

10452  """Create a Z3 floating-point square root expression. 10454  return

_mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)

def fpSqrt(rm, a, ctx=None)

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

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

Definition at line 10356 of file z3py.py.

10356 def fpSub

(rm, a, b, ctx=None):

10357  """Create a Z3 floating-point subtraction expression. 10359  >>> s = FPSort(8, 24) 10363  >>> fpSub(rm, x, y) 10365  >>> fpSub(rm, x, y).sort() 10368  return

_mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)

def fpSub(rm, a, b, ctx=None)

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

10622 def fpToFP

(a1, a2=None, a3=None, ctx=None):

10623  """Create a Z3 floating-point conversion expression from other term sorts 10626  From a bit-vector term in IEEE 754-2008 format: 10627  >>> x = FPVal(1.0, Float32()) 10628  >>> x_bv = fpToIEEEBV(x) 10629  >>> simplify(fpToFP(x_bv, Float32())) 10632  From a floating-point term with different precision: 10633  >>> x = FPVal(1.0, Float32()) 10634  >>> x_db = fpToFP(RNE(), x, Float64()) 10639  >>> x_r = RealVal(1.5) 10640  >>> simplify(fpToFP(RNE(), x_r, Float32())) 10643  From a signed bit-vector term: 10644  >>> x_signed = BitVecVal(-5, BitVecSort(32)) 10645  >>> simplify(fpToFP(RNE(), x_signed, Float32())) 10648

ctx = _get_ctx(ctx)

10658  raise

Z3Exception(

"Unsupported combination of arguments for conversion to floating-point term."

)

def fpToFP(a1, a2=None, a3=None, ctx=None)

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

10753  """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.""" 10755

_z3_assert(

is_fprm

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10756

_z3_assert(

is_bv

(x),

"Second argument must be a Z3 bit-vector expression"

)

10757

_z3_assert(

is_fp_sort

(s),

"Third argument must be Z3 floating-point sort"

)

10758

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

def fpToFPUnsigned(rm, x, s, ctx=None)

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

10827  """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. 10829  The size of the resulting bit-vector is automatically determined. 10831  Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion 10832  knows only one NaN and it will always produce the same bit-vector representation of 10835  >>> x = FP('x', FPSort(8, 24)) 10836  >>> y = fpToIEEEBV(x) 10837  >>> print(is_fp(x)) 10839  >>> print(is_bv(y)) 10841  >>> print(is_fp(y)) 10843  >>> print(is_bv(x)) 10847

_z3_assert(

is_fp

(x),

"First argument must be a Z3 floating-point expression"

)

10848

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)

Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

def fpToIEEEBV(x, ctx=None)

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

10807  """Create a Z3 floating-point conversion expression, from floating-point expression to real. 10809  >>> x = FP('x', FPSort(8, 24)) 10810  >>> y = fpToReal(x) 10811  >>> print(is_fp(x)) 10813  >>> print(is_real(y)) 10815  >>> print(is_fp(y)) 10817  >>> print(is_real(x)) 10821

_z3_assert(

is_fp

(x),

"First argument must be a Z3 floating-point expression"

)

10822

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t)

Conversion of a floating-point term into a real-numbered term.

def fpToReal(x, ctx=None)

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

10762 def fpToSBV

(rm, x, s, ctx=None):

10763  """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector. 10765  >>> x = FP('x', FPSort(8, 24)) 10766  >>> y = fpToSBV(RTZ(), x, BitVecSort(32)) 10767  >>> print(is_fp(x)) 10769  >>> print(is_bv(y)) 10771  >>> print(is_fp(y)) 10773  >>> print(is_bv(x)) 10777

_z3_assert(

is_fprm

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10778

_z3_assert(

is_fp

(x),

"Second argument must be a Z3 floating-point expression"

)

10779

_z3_assert(

is_bv_sort

(s),

"Third argument must be Z3 bit-vector sort"

)

10780

ctx = _get_ctx(ctx)

10781  return

BitVecRef(

Z3_mk_fpa_to_sbv

(ctx.ref(), rm.ast, x.ast, s.size()), ctx)

Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)

Conversion of a floating-point term into a signed bit-vector.

def fpToSBV(rm, x, s, ctx=None)

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

10784 def fpToUBV

(rm, x, s, ctx=None):

10785  """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector. 10787  >>> x = FP('x', FPSort(8, 24)) 10788  >>> y = fpToUBV(RTZ(), x, BitVecSort(32)) 10789  >>> print(is_fp(x)) 10791  >>> print(is_bv(y)) 10793  >>> print(is_fp(y)) 10795  >>> print(is_bv(x)) 10799

_z3_assert(

is_fprm

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10800

_z3_assert(

is_fp

(x),

"Second argument must be a Z3 floating-point expression"

)

10801

_z3_assert(

is_bv_sort

(s),

"Third argument must be Z3 bit-vector sort"

)

10802

ctx = _get_ctx(ctx)

10803  return

BitVecRef(

Z3_mk_fpa_to_ubv

(ctx.ref(), rm.ast, x.ast, s.size()), ctx)

Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)

Conversion of a floating-point term into an unsigned bit-vector.

def fpToUBV(rm, x, s, ctx=None)

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

10735  """Create a Z3 floating-point conversion expression that represents the 10736  conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term. 10738  >>> x_signed = BitVecVal(-5, BitVecSort(32)) 10739  >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32()) 10741  fpToFPUnsigned(RNE(), 4294967291) 10745

_z3_assert(

is_fprm

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10746

_z3_assert(

is_bv

(v),

"Second argument must be a Z3 bit-vector expression"

)

10747

_z3_assert(

is_fp_sort

(sort),

"Third argument must be a Z3 floating-point sort."

)

10748

ctx = _get_ctx(ctx)

def fpUnsignedToFP(rm, v, sort, ctx=None)

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

10159 def FPVal

(sig, exp=None, fps=None, ctx=None):

10160  """Return a floating-point value of value `val` and sort `fps`. 10161  If `ctx=None`, then the global context is used. 10163  >>> v = FPVal(20.0, FPSort(8, 24)) 10166  >>> print("0x%.8x" % v.exponent_as_long(False)) 10168  >>> v = FPVal(2.25, FPSort(8, 24)) 10171  >>> v = FPVal(-2.25, FPSort(8, 24)) 10174  >>> FPVal(-0.0, FPSort(8, 24)) 10176  >>> FPVal(0.0, FPSort(8, 24)) 10178  >>> FPVal(+0.0, FPSort(8, 24)) 10181

ctx = _get_ctx(ctx)

10186

fps = _dflt_fps(ctx)

10187

_z3_assert(

is_fp_sort

(fps),

"sort mismatch"

)

10190

val = _to_float_str(sig)

10191  if

val ==

"NaN" or

val ==

"nan"

:

10193  elif

val ==

"-0.0"

:

10195  elif

val ==

"0.0" or

val ==

"+0.0"

:

10197  elif

val ==

"+oo" or

val ==

"+inf" or

val ==

"+Inf"

:

10199  elif

val ==

"-oo" or

val ==

"-inf" or

val ==

"-Inf"

:

10202  return

FPNumRef(

Z3_mk_numeral

(ctx.ref(), val, fps.ast), ctx)

def FPVal(sig, exp=None, fps=None, ctx=None)

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

10152 def fpZero

(s, negative):

10153  """Create a Z3 floating-point +0.0 or -0.0 term.""" 10154

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10155

_z3_assert(isinstance(negative, bool),

"expected Boolean flag"

)

10156  return

FPNumRef(

Z3_mk_fpa_zero

(s.ctx_ref(), s.ast, negative), s.ctx)

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

1812  """Return a fresh Boolean constant in the given context using the given prefix. 1814  If `ctx=None`, then the global context is used. 1816  >>> b1 = FreshBool() 1817  >>> b2 = FreshBool()

Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)

Declare and create a fresh constant.

def FreshBool(prefix="b", ctx=None)

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

Definition at line 1482 of file z3py.py.

1483  """Create a fresh constant of a specified sort""" 1484

ctx = _get_ctx(sort.ctx)

def FreshConst(sort, prefix="c")

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

Definition at line 904 of file z3py.py.

905  """Create a new fresh Z3 uninterpreted function with the given sorts. 909

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

913

_z3_assert(

is_sort

(rng),

"Z3 sort expected"

)

914

dom = (z3.Sort * arity)()

915  for

i

in range

(arity):

917

_z3_assert(

is_sort

(sig[i]),

"Z3 sort expected"

)

Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a fresh constant or function.

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

3333 def FreshInt

(prefix="x", ctx=None):

3334  """Return a fresh integer constant in the given context using the given prefix.

def FreshInt(prefix="x", ctx=None)

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

3391  """Return a fresh real constant in the given context using the given prefix.

def FreshReal(prefix="b", ctx=None)

◆ Full() 
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 11108 of file z3py.py.

11109  """Create the regular expression that accepts the universal language 11110  >>> e = Full(ReSort(SeqSort(IntSort()))) 11112  Full(ReSort(Seq(Int))) 11113  >>> e1 = Full(ReSort(StringSort())) 11115  Full(ReSort(String)) 11117  if

isinstance(s, ReSortRef):

11119  raise

Z3Exception(

"Non-sequence, non-regular expression sort passed to Full"

)

Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)

Create an universal regular expression of sort re.

◆ FullSet() 
Create the full set
>>> FullSet(IntSort())
K(Int, True)

Definition at line 4977 of file z3py.py.

4978  """Create the full set 4979  >>> FullSet(IntSort())

Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)

Create the full set.

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

882  """Create a new Z3 uninterpreted function with the given sorts. 884  >>> f = Function('f', IntSort(), IntSort()) 890

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

894

_z3_assert(

is_sort

(rng),

"Z3 sort expected"

)

895

dom = (Sort * arity)()

896  for

i

in range

(arity):

898

_z3_assert(

is_sort

(sig[i]),

"Z3 sort expected"

)

Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a constant or function.

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

6746  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f).""" 6748

_z3_assert(

is_as_array

(n),

"as-array Z3 expression expected."

)

Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)

Return the function declaration f associated with a (_ as_array f) node.

Referenced by ModelRef.get_interp().

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

Definition at line 9423 of file z3py.py.

9424  """Retrieves the global default rounding mode.""" 9425  global

_dflt_rounding_mode

9426  if

_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:

9428  elif

_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:

9430  elif

_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:

9432  elif

_dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:

9434  elif

_dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:

def get_default_rounding_mode(ctx=None)

Referenced by set_default_fp_sort().

◆ get_full_version() def z3py.get_full_version ( )

Definition at line 101 of file z3py.py.

Z3_string Z3_API Z3_get_full_version(void)

Return a string that fully describes the version of Z3 in use.

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

4723  """Return the function declaration associated with a Z3 map array expression. 4725  >>> f = Function('f', IntSort(), IntSort()) 4726  >>> b = Array('b', IntSort(), IntSort()) 4728  >>> eq(f, get_map_func(a)) 4732  >>> get_map_func(a)(0) 4736

_z3_assert(

is_map

(a),

"Z3 array map expression expected."

)

Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)

Convert an AST into a FUNC_DECL_AST. This is just type casting.

Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)

Return the expression value associated with an expression parameter.

◆ get_param() def z3py.get_param (   name ) 
Return the value of a Z3 global (or module) parameter

>>> get_param('nlsat.reorder')
'true'

Definition at line 307 of file z3py.py.

308  """Return the value of a Z3 global (or module) parameter 310  >>> get_param('nlsat.reorder') 313

ptr = (ctypes.c_char_p * 1)()

315

r = z3core._to_pystr(ptr[0])

317  raise

Z3Exception(

"failed to retrieve value for '%s'"

% name)

bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)

Get a global (or module) parameter.

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

1354  """Return the de-Bruijn index of the Z3 bounded variable `a`. 1362  >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1363  >>> # Z3 replaces x and y with bound variables when ForAll is executed. 1364  >>> q = ForAll([x, y], f(x, y) == x + y) 1366  f(Var(1), Var(0)) == Var(1) + Var(0) 1370  >>> v1 = b.arg(0).arg(0) 1371  >>> v2 = b.arg(0).arg(1) 1376  >>> get_var_index(v1) 1378  >>> get_var_index(v2) 1382

_z3_assert(

is_var

(a),

"Z3 bound variable expected"

)

unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)

Return index of de-Bruijn bound variable.

◆ get_version()

Definition at line 92 of file z3py.py.

93

major = ctypes.c_uint(0)

94

minor = ctypes.c_uint(0)

95

build = ctypes.c_uint(0)

96

rev = ctypes.c_uint(0)

98  return

(major.value, minor.value, build.value, rev.value)

void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)

Return Z3 version number information.

◆ get_version_string() def z3py.get_version_string ( )

Definition at line 83 of file z3py.py.

84

major = ctypes.c_uint(0)

85

minor = ctypes.c_uint(0)

86

build = ctypes.c_uint(0)

87

rev = ctypes.c_uint(0)

89  return "%s.%s.%s"

% (major.value, minor.value, build.value)

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

Definition at line 8929 of file z3py.py.

8930  """Return a string describing all options available for Z3 `simplify` procedure."""

Z3_string Z3_API Z3_simplify_get_help(Z3_context c)

Return a string describing all available parameters.

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

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

Definition at line 1399 of file z3py.py.

1399 def If

(a, b, c, ctx=None):

1400  """Create a Z3 if-then-else expression. 1404  >>> max = If(x > y, x, y) 1410  if

isinstance(a, Probe)

or

isinstance(b, Tactic)

or

isinstance(c, Tactic):

1411  return Cond

(a, b, c, ctx)

1413

ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))

1416

b, c = _coerce_exprs(b, c, ctx)

1418

_z3_assert(a.ctx == b.ctx,

"Context mismatch"

)

1419  return

_to_expr_ref(

Z3_mk_ite

(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)

Create an AST node representing an if-then-else: ite(t1, t2, t3).

Referenced by BoolRef.__add__(), 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 1825 of file z3py.py.

1826  """Create a Z3 implies expression. 1828  >>> p, q = Bools('p q') 1832

ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))

1836  return

BoolRef(

Z3_mk_implies

(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)

Create an AST node representing t1 implies t2.

def Implies(a, b, ctx=None)

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

11192 def IndexOf

(s, substr, offset=None):

11193  """Retrieve the index of substring within a string starting at a specified offset. 11194  >>> simplify(IndexOf("abcabc", "bc", 0)) 11196  >>> simplify(IndexOf("abcabc", "bc", 2)) 11199  if

offset

is None

:

11204

ctx = _get_ctx2(s, substr, ctx)

11205

s = _coerce_seq(s, ctx)

11206

substr = _coerce_seq(substr, ctx)

11207  if

_is_int(offset):

11208

offset =

IntVal

(offset, ctx)

11209  return

ArithRef(

Z3_mk_seq_index

(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)

Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)

Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...

def IndexOf(s, substr, offset=None)

def IntVal(val, ctx=None)

◆ InRe() 
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 11331 of file z3py.py.

11332  """Create regular expression membership test 11333  >>> re = Union(Re("a"),Re("b")) 11334  >>> print (simplify(InRe("a", re))) 11336  >>> print (simplify(InRe("b", re))) 11338  >>> print (simplify(InRe("c", re))) 11341

s = _coerce_seq(s, re.ctx)

11342  return

BoolRef(

Z3_mk_seq_in_re

(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)

Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)

Check if seq is in the language generated by the regular expression re.

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

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

Definition at line 3294 of file z3py.py.

3294 def Int

(name, ctx=None):

3295  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.

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

4042 def Int2BV

(a, num_bits):

4043  """Return the z3 expression Int2BV(a, num_bits). 4044  It is a bit-vector of width num_bits and represents the 4045  modulo of a by 2^num_bits 4048  return

BitVecRef(

Z3_mk_int2bv

(ctx.ref(), num_bits, a.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)

Create an n bit bit-vector from the integer argument t1.

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

Definition at line 11365 of file z3py.py.

11366  """Create intersection of regular expressions. 11367  >>> re = Intersect(Re("a"), Re("b"), Re("c")) 11369

args = _get_args(args)

11372

_z3_assert(sz > 0,

"At least one argument expected."

)

11373

_z3_assert(all([

is_re

(a)

for

a

in

args]),

"All arguments must be regular expressions."

)

11378  for

i

in range

(sz):

11379

v[i] = args[i].as_ast()

Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])

Create the intersection of the regular languages.

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

3307 def Ints

(names, ctx=None):

3308  """Return a tuple of Integer constants. 3310  >>> x, y, z = Ints('x y z') 3315  if

isinstance(names, str):

3316

names = names.split(

" "

)

3317  return

[

Int

(name, ctx)

for

name

in

names]

def Ints(names, ctx=None)

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

3189  """Return the integer sort in the given context. If `ctx=None`, then the global context is used. 3193  >>> x = Const('x', IntSort()) 3196  >>> x.sort() == IntSort() 3198  >>> x.sort() == BoolSort()

Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)

Create the integer type.

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

◆ IntToStr() 
Convert integer expression to string

Definition at line 11273 of file z3py.py.

11274  """Convert integer expression to string"""

Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)

Integer to string conversion.

◆ IntVal() def z3py.IntVal (   val,   ctx = None  ) ◆ 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 3320 of file z3py.py.

3321  """Return a list of integer constants of size `sz`. 3323  >>> X = IntVector('x', 3) 3330  return

[

Int

(

"%s__%s"

% (prefix, i), ctx)

for

i

in range

(sz)]

def IntVector(prefix, sz, ctx=None)

◆ is_add() 
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 2842 of file z3py.py.

2843  """Return `True` if `a` is an expression of the form b + c. 2845  >>> x, y = Ints('x y') ◆ 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 2828 of file z3py.py.

2829  """Return `True` if `a` is an algebraic value of sort Real. 2831  >>> is_algebraic_value(RealVal("3/5")) 2833  >>> n = simplify(Sqrt(2)) 2836  >>> is_algebraic_value(n) 2839  return is_arith

(a)

and

a.is_real()

and

_is_algebraic(a.ctx, a.as_ast())

def is_algebraic_value(a)

◆ is_and() 
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 1661 of file z3py.py.

1662  """Return `True` if `a` is a Z3 and expression. 1664  >>> p, q = Bools('p q') 1665  >>> is_and(And(p, q)) 1667  >>> is_and(Or(p, q)) ◆ is_app() 
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 1283 of file z3py.py.

1284  """Return `True` if `a` is a Z3 function application. 1286  Note that, constants are function applications with 0 arguments. 1293  >>> is_app(IntSort()) 1297  >>> is_app(IntVal(1)) 1300  >>> is_app(ForAll(x, x >= 0)) 1303  if not

isinstance(a, ExprRef):

1305

k = _ast_kind(a.ctx, a)

1306  return

k == Z3_NUMERAL_AST

or

k == Z3_APP_AST

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

1387  """Return `True` if `a` is an application of the given kind `k`. 1391  >>> is_app_of(n, Z3_OP_ADD) 1393  >>> is_app_of(n, Z3_OP_MUL) 1396  return is_app

(a)

and

a.decl().kind() == k

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() 
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 2715 of file z3py.py.

2716  """Return `True` if `a` is an arithmetical expression. 2725  >>> is_arith(IntVal(1)) 2733  return

isinstance(a, ArithRef)

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

2415  """Return `True` if s is an arithmetical sort (type). 2417  >>> is_arith_sort(IntSort()) 2419  >>> is_arith_sort(RealSort()) 2421  >>> is_arith_sort(BoolSort()) 2423  >>> n = Int('x') + 1 2424  >>> is_arith_sort(n.sort()) 2427  return

isinstance(s, ArithSortRef)

Referenced by ArithSortRef.subsort().

◆ is_array() 
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 4657 of file z3py.py.

4658  """Return `True` if `a` is a Z3 array expression. 4660  >>> a = Array('a', IntSort(), IntSort()) 4663  >>> is_array(Store(a, 0, 1)) 4668  return

isinstance(a, ArrayRef)

Referenced by Ext(), and Map().

◆ is_array_sort() def z3py.is_array_sort (   a )

Definition at line 4653 of file z3py.py.

Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)

Return the sort kind (e.g., array, tuple, int, bool, etc).

Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)

Return the sort of an AST node.

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

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

Definition at line 6740 of file z3py.py.

6741  """Return true if n is a Z3 expression of the form (_ as-array f).""" 6742  return

isinstance(n, ExprRef)

and Z3_is_as_array

(n.ctx.ref(), n.as_ast())

bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)

The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3....

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

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

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

Definition at line 451 of file z3py.py.

452  """Return `True` if `a` is an AST node. 456  >>> is_ast(IntVal(10)) 460  >>> is_ast(BoolSort()) 462  >>> is_ast(Function('f', IntSort(), IntSort())) 469  return

isinstance(a, AstRef)

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

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

1612  """Return `True` if `a` is a Z3 Boolean expression. 1618  >>> is_bool(And(p, q)) 1626  return

isinstance(a, BoolRef)

Referenced by is_quantifier(), and prove().

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

3991  """Return `True` if `a` is a Z3 bit-vector expression. 3993  >>> b = BitVec('b', 32) 4001  return

isinstance(a, BitVecRef)

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

3523  """Return True if `s` is a Z3 bit-vector sort. 3525  >>> is_bv_sort(BitVecSort(32)) 3527  >>> is_bv_sort(IntSort()) 3530  return

isinstance(s, BitVecSortRef)

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

4005  """Return `True` if `a` is a Z3 bit-vector numeral value. 4007  >>> b = BitVec('b', 32) 4010  >>> b = BitVecVal(10, 32) 4016  return is_bv

(a)

and

_is_numeral(a.ctx, a.as_ast())

◆ is_const() ◆ 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 4671 of file z3py.py.

4672  """Return `True` if `a` is a Z3 constant array. 4674  >>> a = K(IntSort(), 10) 4675  >>> is_const_array(a) 4677  >>> a = Array('a', IntSort(), IntSort()) 4678  >>> is_const_array(a) ◆ 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 4713 of file z3py.py.

4714  """Return `True` if `a` is a Z3 default array expression. 4715  >>> d = Default(K(IntSort(), 10)) 4719  return is_app_of

(a, Z3_OP_ARRAY_DEFAULT)

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

1720  """Return `True` if `a` is a Z3 distinct expression. 1722  >>> x, y, z = Ints('x y z') 1723  >>> is_distinct(x == y) 1725  >>> is_distinct(Distinct(x, y, z)) ◆ is_div() 
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 2878 of file z3py.py.

2879  """Return `True` if `a` is an expression of the form b / c. 2881  >>> x, y = Reals('x y') 2886  >>> x, y = Ints('x y') ◆ is_eq() 
Return `True` if `a` is a Z3 equality expression.

>>> x, y = Ints('x y')
>>> is_eq(x == y)
True

Definition at line 1709 of file z3py.py.

1710  """Return `True` if `a` is a Z3 equality expression. 1712  >>> x, y = Ints('x y')

Referenced by AstRef.__bool__().

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

1261  """Return `True` if `a` is a Z3 expression. 1268  >>> is_expr(IntSort()) 1272  >>> is_expr(IntVal(1)) 1275  >>> is_expr(ForAll(x, x >= 0)) 1277  >>> is_expr(FPVal(1.0)) 1280  return

isinstance(a, ExprRef)

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

◆ is_false() 
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 1647 of file z3py.py.

1648  """Return `True` if `a` is the Z3 false expression. 1655  >>> is_false(BoolVal(False))

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

7815  """Return `True` if `a` is a Z3 finite-domain expression. 7817  >>> s = FiniteDomainSort('S', 100) 7818  >>> b = Const('b', s) 7819  >>> is_finite_domain(b) 7821  >>> is_finite_domain(Int('x')) 7824  return

isinstance(a, FiniteDomainRef)

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

7792  """Return True if `s` is a Z3 finite-domain sort. 7794  >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 7796  >>> is_finite_domain_sort(IntSort()) 7799  return

isinstance(s, FiniteDomainSortRef)

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

7869  """Return `True` if `a` is a Z3 finite-domain value. 7871  >>> s = FiniteDomainSort('S', 100) 7872  >>> b = Const('b', s) 7873  >>> is_finite_domain_value(b) 7875  >>> b = FiniteDomainVal(10, s) 7878  >>> is_finite_domain_value(b)

def is_finite_domain_value(a)

◆ is_fp() 
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 10005 of file z3py.py.

10006  """Return `True` if `a` is a Z3 floating-point expression. 10008  >>> b = FP('b', FPSort(8, 24)) 10013  >>> is_fp(Int('x')) 10016  return

isinstance(a, FPRef)

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

9590  """Return True if `s` is a Z3 floating-point sort. 9592  >>> is_fp_sort(FPSort(8, 24)) 9594  >>> is_fp_sort(IntSort()) 9597  return

isinstance(s, FPSortRef)

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

10020  """Return `True` if `a` is a Z3 floating-point numeral value. 10022  >>> b = FP('b', FPSort(8, 24)) 10025  >>> b = FPVal(1.0, FPSort(8, 24)) 10031  return is_fp

(a)

and

_is_numeral(a.ctx, a.ast)

◆ is_fprm() 
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 9849 of file z3py.py.

9850  """Return `True` if `a` is a Z3 floating-point rounding mode expression. 9859  return

isinstance(a, FPRMRef)

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

9601  """Return True if `s` is a Z3 floating-point rounding mode sort. 9603  >>> is_fprm_sort(FPSort(8, 24)) 9605  >>> is_fprm_sort(RNE().sort()) 9608  return

isinstance(s, FPRMSortRef)

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

9863  """Return `True` if `a` is a Z3 floating-point rounding mode numeral value.""" 9864  return is_fprm

(a)

and

_is_numeral(a.ctx, a.ast)

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

869  """Return `True` if `a` is a Z3 function declaration. 871  >>> f = Function('f', IntSort(), IntSort()) 878  return

isinstance(a, FuncDeclRef)

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

◆ is_ge() 
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 2943 of file z3py.py.

2944  """Return `True` if `a` is an expression of the form b >= c. 2946  >>> x, y = Ints('x y') ◆ is_gt() 
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 2955 of file z3py.py.

2956  """Return `True` if `a` is an expression of the form b > c. 2958  >>> x, y = Ints('x y') ◆ is_idiv() 
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 2895 of file z3py.py.

2896  """Return `True` if `a` is an expression of the form b div c. 2898  >>> x, y = Ints('x y') ◆ 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 1685 of file z3py.py.

1686  """Return `True` if `a` is a Z3 implication expression. 1688  >>> p, q = Bools('p q') 1689  >>> is_implies(Implies(p, q)) 1691  >>> is_implies(And(p, q)) ◆ is_int() 
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 2736 of file z3py.py.

2737  """Return `True` if `a` is an integer expression. 2744  >>> is_int(IntVal(1)) ◆ 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 2782 of file z3py.py.

2783  """Return `True` if `a` is an integer value of sort Int. 2785  >>> is_int_value(IntVal(1)) 2789  >>> is_int_value(Int('x')) 2791  >>> n = Int('x') + 1 2796  >>> is_int_value(n.arg(1)) 2798  >>> is_int_value(RealVal("1/3")) 2800  >>> is_int_value(RealVal(1)) 2803  return is_arith

(a)

and

a.is_int()

and

_is_numeral(a.ctx, a.as_ast())

◆ is_is_int() 
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 2967 of file z3py.py.

2968  """Return `True` if `a` is an expression of the form IsInt(b). 2971  >>> is_is_int(IsInt(x)) ◆ is_K() 
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 4684 of file z3py.py.

4685  """Return `True` if `a` is a Z3 constant array. 4687  >>> a = K(IntSort(), 10) 4690  >>> a = Array('a', IntSort(), IntSort()) ◆ is_le() 
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 2919 of file z3py.py.

2920  """Return `True` if `a` is an expression of the form b <= c. 2922  >>> x, y = Ints('x y') ◆ is_lt() 
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 2931 of file z3py.py.

2932  """Return `True` if `a` is an expression of the form b < c. 2934  >>> x, y = Ints('x y') ◆ is_map() 
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 4697 of file z3py.py.

4698  """Return `True` if `a` is a Z3 map array expression. 4700  >>> f = Function('f', IntSort(), IntSort()) 4701  >>> b = Array('b', IntSort(), IntSort())

Referenced by get_map_func().

◆ is_mod() 
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 2907 of file z3py.py.

2908  """Return `True` if `a` is an expression of the form b % c. 2910  >>> x, y = Ints('x y') ◆ is_mul() 
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 2854 of file z3py.py.

2855  """Return `True` if `a` is an expression of the form b * c. 2857  >>> x, y = Ints('x y') ◆ is_not() 
Return `True` if `a` is a Z3 not expression.

>>> p = Bool('p')
>>> is_not(p)
False
>>> is_not(Not(p))
True

Definition at line 1697 of file z3py.py.

1698  """Return `True` if `a` is a Z3 not expression.

Referenced by mk_not().

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

1674  """Return `True` if `a` is a Z3 or expression. 1676  >>> p, q = Bools('p q') 1679  >>> is_or(And(p, q)) ◆ 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 1973 of file z3py.py.

1974  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. 1976  >>> f = Function('f', IntSort(), IntSort()) 1978  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) 1980  ForAll(x, f(x) == 0) 1981  >>> q.num_patterns() 1983  >>> is_pattern(q.pattern(0)) 1988  return

isinstance(a, PatternRef)

Referenced by is_quantifier(), and MultiPattern().

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

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

Definition at line 8770 of file z3py.py.

8771  """Return `True` if `p` is a Z3 probe. 8773  >>> is_probe(Int('x')) 8775  >>> is_probe(Probe('memory')) 8778  return

isinstance(p, Probe)

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

2224  """Return `True` if `a` is a Z3 quantifier. 2226  >>> f = Function('f', IntSort(), IntSort()) 2228  >>> q = ForAll(x, f(x) == 0) 2229  >>> is_quantifier(q) 2231  >>> is_quantifier(f(x)) 2234  return

isinstance(a, QuantifierRef)

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

2807  """Return `True` if `a` is rational value of sort Real. 2809  >>> is_rational_value(RealVal(1)) 2811  >>> is_rational_value(RealVal("3/5")) 2813  >>> is_rational_value(IntVal(1)) 2815  >>> is_rational_value(1) 2817  >>> n = Real('x') + 1 2820  >>> is_rational_value(n.arg(1)) 2822  >>> is_rational_value(Real('x')) 2825  return is_arith

(a)

and

a.is_real()

and

_is_numeral(a.ctx, a.as_ast())

◆ is_re() ◆ is_real() 
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 2755 of file z3py.py.

2756  """Return `True` if `a` is a real expression. 2768  >>> is_real(RealVal(1)) 2771  return is_arith

(a)

and

a.is_real()

Referenced by fpRealToFP(), and fpToFP().

◆ is_select() 
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 4932 of file z3py.py.

4933  """Return `True` if `a` is a Z3 array select application. 4935  >>> a = Array('a', IntSort(), IntSort()) ◆ is_seq() 
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 11027 of file z3py.py.

11028  """Return `True` if `a` is a Z3 sequence expression. 11029  >>> print (is_seq(Unit(IntVal(0)))) 11031  >>> print (is_seq(StringVal("abc"))) 11034  return

isinstance(a, SeqRef)

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

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

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

Definition at line 647 of file z3py.py.

648  """Return `True` if `s` is a Z3 sort. 650  >>> is_sort(IntSort()) 652  >>> is_sort(Int('x')) 654  >>> is_expr(Int('x')) 657  return

isinstance(s, SortRef)

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

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

4946  """Return `True` if `a` is a Z3 array store application. 4948  >>> a = Array('a', IntSort(), IntSort()) 4951  >>> is_store(Store(a, 0, 1)) ◆ is_string() 
Return `True` if `a` is a Z3 string expression.
>>> print (is_string(StringVal("ab")))
True

Definition at line 11037 of file z3py.py.

11038  """Return `True` if `a` is a Z3 string expression. 11039  >>> print (is_string(StringVal("ab"))) 11042  return

isinstance(a, SeqRef)

and

a.is_string()

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

11046  """return 'True' if 'a' is a Z3 string constant expression. 11047  >>> print (is_string_value(StringVal("a"))) 11049  >>> print (is_string_value(StringVal("a") + StringVal("b"))) 11052  return

isinstance(a, SeqRef)

and

a.is_string_value()

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

2867  """Return `True` if `a` is an expression of the form b - c. 2869  >>> x, y = Ints('x y') ◆ is_to_int() 
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 2994 of file z3py.py.

2995  """Return `True` if `a` is an expression of the form ToInt(b). ◆ 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 2979 of file z3py.py.

2980  """Return `True` if `a` is an expression of the form ToReal(b). ◆ is_true() 
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 1629 of file z3py.py.

1630  """Return `True` if `a` is the Z3 true expression. 1635  >>> is_true(simplify(p == p)) 1640  >>> # True is a Python Boolean expression

Referenced by AstRef.__bool__().

◆ is_var() 
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 1328 of file z3py.py.

1329  """Return `True` if `a` is variable. 1331  Z3 uses de-Bruijn indices for representing bound variables in 1339  >>> f = Function('f', IntSort(), IntSort()) 1340  >>> # Z3 replaces x with bound variables when ForAll is executed. 1341  >>> q = ForAll(x, f(x) == x) 1347  >>> is_var(b.arg(1)) 1350  return is_expr

(a)

and

_ast_kind(a.ctx, a) == Z3_VAR_AST

Referenced by get_var_index().

◆ IsInt() 
 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 3440 of file z3py.py.

3441  """ Return the Z3 predicate IsInt(a). 3444  >>> IsInt(x + "1/2") 3446  >>> solve(IsInt(x + "1/2"), x > 0, x < 1) 3448  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") 3452

_z3_assert(a.is_real(),

"Z3 real expression expected."

)

3454  return

BoolRef(

Z3_mk_is_int

(ctx.ref(), a.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)

Check if a real number is an integer.

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

5056  """ Check if e is a member of set s 5057  >>> a = Const('a', SetSort(IntSort())) 5061

ctx = _ctx_from_ast_arg_list([s, e])

5062

e = _py2expr(e, ctx)

Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)

Check for set membership.

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

5067  """ Check if a is a subset of b 5068  >>> a = Const('a', SetSort(IntSort())) 5069  >>> b = Const('b', SetSort(IntSort())) 5073

ctx = _ctx_from_ast_arg_list([a, b])

Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Check for subsetness of sets.

◆ K() 
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 4892 of file z3py.py.

4893  """Return a Z3 constant array expression. 4895  >>> a = K(IntSort(), 10) 4907

_z3_assert(

is_sort

(dom),

"Z3 sort expected"

)

4910

v = _py2expr(v, ctx)

Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)

Create the constant array.

Referenced by ModelRef.get_interp().

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

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

Definition at line 2311 of file z3py.py.

2312  """Create a Z3 lambda expression. 2314  >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2315  >>> mem0 = Array('mem0', IntSort(), IntSort()) 2316  >>> lo, hi, e, i = Ints('lo hi e i') 2317  >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i])) 2319  Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i])) 2325

_vs = (Ast * num_vars)()

2326  for

i

in range

(num_vars):

2328

_vs[i] = vs[i].as_ast()

2329  return

QuantifierRef(

Z3_mk_lambda_const

(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)

Create a lambda expression using a list of constants that form the set of bound variables.

Referenced by Context.MkLambda().

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

Definition at line 11212 of file z3py.py.

11213  """Retrieve the last index of substring within a string""" 11215

ctx = _get_ctx2(s, substr, ctx)

11216

s = _coerce_seq(s, ctx)

11217

substr = _coerce_seq(substr, ctx)

Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr)

Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...

def LastIndexOf(s, substr)

◆ Length() ◆ LinearOrder() def z3py.LinearOrder (   a,   index  )

Definition at line 11483 of file z3py.py.

Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)

create a linear ordering relation over signature a. The relation is identified by the index id.

def LinearOrder(a, index)

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

11433 def Loop

(re, lo, hi=0):

11434  """Create the regular expression accepting between a lower and upper bound repetitions 11435  >>> re = Loop(Re("a"), 1, 3) 11436  >>> print(simplify(InRe("aa", re))) 11438  >>> print(simplify(InRe("aaaa", re))) 11440  >>> print(simplify(InRe("", re))) 11444

_z3_assert(

is_expr

(re),

"expression expected"

)

11445  return

ReRef(

Z3_mk_re_loop

(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)

Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)

Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...

◆ LShR() 
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 4345 of file z3py.py.

4346  """Create the Z3 expression logical right shift. 4348  Use the operator >> for the arithmetical right shift. 4350  >>> x, y = BitVecs('x y', 32) 4353  >>> (x >> y).sexpr() 4355  >>> LShR(x, y).sexpr() 4359  >>> BitVecVal(4, 3).as_signed_long() 4361  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() 4363  >>> simplify(BitVecVal(4, 3) >> 1) 4365  >>> simplify(LShR(BitVecVal(4, 3), 1)) 4367  >>> simplify(BitVecVal(2, 3) >> 1) 4369  >>> simplify(LShR(BitVecVal(2, 3), 1)) 4372

_check_bv_args(a, b)

4373

a, b = _coerce_exprs(a, b)

4374  return

BitVecRef(

Z3_mk_bvlshr

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)

Logical shift right.

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

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

Definition at line 239 of file z3py.py.

240  """Return a reference to the global Z3 context. 243  >>> x.ctx == main_ctx() 248  >>> x2 = Real('x', c) 255  if

_main_ctx

is None

:

256

_main_ctx = Context()

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

4870  """Return a Z3 map array expression. 4872  >>> f = Function('f', IntSort(), IntSort(), IntSort()) 4873  >>> a1 = Array('a1', IntSort(), IntSort()) 4874  >>> a2 = Array('a2', IntSort(), IntSort()) 4875  >>> b = Map(f, a1, a2) 4878  >>> prove(b[0] == f(a1[0], a2[0])) 4881

args = _get_args(args)

4883

_z3_assert(len(args) > 0,

"At least one Z3 array expression expected"

)

4884

_z3_assert(

is_func_decl

(f),

"First argument must be a Z3 function declaration"

)

4885

_z3_assert(all([

is_array

(a)

for

a

in

args]),

"Z3 array expected expected"

)

4886

_z3_assert(len(args) == f.arity(),

"Number of arguments mismatch"

)

4887

_args, sz = _to_ast_array(args)

4889  return

ArrayRef(

Z3_mk_map

(ctx.ref(), f.ast, sz, _args), ctx)

Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const *args)

Map f on the argument arrays.

Referenced by Context.Context().

◆ mk_not() ◆ Model() def z3py.Model (   ctx = None ) ◆ 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 1991 of file z3py.py.

1992  """Create a Z3 multi-pattern using the given expressions `*args` 1994  >>> f = Function('f', IntSort(), IntSort()) 1995  >>> g = Function('g', IntSort(), IntSort()) 1997  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ]) 1999  ForAll(x, f(x) != g(x)) 2000  >>> q.num_patterns() 2002  >>> is_pattern(q.pattern(0)) 2005  MultiPattern(f(Var(0)), g(Var(0))) 2008

_z3_assert(len(args) > 0,

"At least one argument expected"

)

2009

_z3_assert(all([

is_expr

(a)

for

a

in

args]),

"Z3 expressions expected"

)

2011

args, sz = _to_ast_array(args)

2012  return

PatternRef(

Z3_mk_pattern

(ctx.ref(), sz, args), ctx)

Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[])

Create a pattern for quantifier instantiation.

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

1855 def Not

(a, ctx=None):

1856  """Create a Z3 not expression or probe. 1861  >>> simplify(Not(Not(p))) 1864

ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))

1871  return

BoolRef(

Z3_mk_not

(ctx.ref(), a.as_ast()), ctx)

Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)

Return a probe that evaluates to "true" when p does not evaluate to true.

Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)

Create an AST node representing not(a).

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

◆ on_clause_eh() def z3py.on_clause_eh (   ctx,   p,   n,   dep,   clause  )

Definition at line 11523 of file z3py.py.

11524

onc = _my_hacky_class

11525

p = _to_expr_ref(

to_Ast

(p), onc.ctx)

11527

deps = [dep[i]

for

i

in range

(n)]

11528

onc.on_clause(p, deps, clause)

def on_clause_eh(ctx, p, n, dep, clause)

Referenced by on_clause.on_clause().

◆ 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.

115  """Log interaction to a file. This function must be invoked immediately after init(). """

bool Z3_API Z3_open_log(Z3_string filename)

Log interaction to a file.

◆ Option() 
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 11398 of file z3py.py.

11399  """Create the regular expression that optionally accepts the argument. 11400  >>> re = Option(Re("a")) 11401  >>> print(simplify(InRe("a", re))) 11403  >>> print(simplify(InRe("", re))) 11405  >>> print(simplify(InRe("aa", re))) 11409

_z3_assert(

is_expr

(re),

"expression expected"

)

Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)

Create the regular language [re].

◆ Or() 
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 1922 of file z3py.py.

1923  """Create a Z3 or-expression or or-probe. 1925  >>> p, q, r = Bools('p q r') 1928  >>> P = BoolVector('p', 5) 1930  Or(p__0, p__1, p__2, p__3, p__4) 1934

last_arg = args[len(args) - 1]

1935  if

isinstance(last_arg, Context):

1936

ctx = args[len(args) - 1]

1937

args = args[:len(args) - 1]

1938  elif

len(args) == 1

and

isinstance(args[0], AstVector):

1940

args = [a

for

a

in

args[0]]

1943

args = _get_args(args)

1944

ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))

1946

_z3_assert(ctx

is not None

,

"At least one of the arguments must be a Z3 expression or probe"

)

1947  if

_has_probe(args):

1948  return

_probe_or(args, ctx)

1950

args = _coerce_expr_list(args, ctx)

1951

_args, sz = _to_ast_array(args)

1952  return

BoolRef(

Z3_mk_or

(ctx.ref(), sz, _args), ctx)

Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] or ... or args[num_args-1].

Referenced by BoolRef.__or__(), and 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 8463 of file z3py.py.

8464  """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 8467  >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 8468  >>> # Tactic split-clause fails if there is no clause in the given goal. 8471  >>> t(Or(x == 0, x == 1)) 8472  [[x == 0], [x == 1]] 8475

_z3_assert(len(ts) >= 2,

"At least two arguments expected"

)

8476

ctx = ks.get(

"ctx"

,

None

)

8479  for

i

in range

(num - 1):

8480

r = _or_else(r, ts[i + 1], ctx)

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

Definition at line 8519 of file z3py.py.

8520  """Alias for ParThen(t1, t2, ctx)."""

def ParThen(t1, t2, ctx=None)

def ParAndThen(t1, t2, ctx=None)

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

8484 def ParOr

(*ts, **ks):

8485  """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 8488  >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 8493

_z3_assert(len(ts) >= 2,

"At least two arguments expected"

)

8494

ctx = _get_ctx(ks.get(

"ctx"

,

None

))

8495

ts = [_to_tactic(t, ctx)

for

t

in

ts]

8497

_args = (TacticObj * sz)()

8498  for

i

in range

(sz):

8499

_args[i] = ts[i].tactic

Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])

Return a tactic that applies the given tactics in parallel.

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

9400  """Parse a file in SMT 2.0 format using the given sorts and decls. 9402  This function is similar to parse_smt2_string(). 9405

ssz, snames, ssorts = _dict2sarray(sorts, ctx)

9406

dsz, dnames, ddecls = _dict2darray(decls, ctx)

9407  return

AstVector(

Z3_parse_smtlib2_file

(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)

Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])

Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.

def parse_smt2_file(f, sorts={}, decls={}, ctx=None)

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

9379  """Parse a string in SMT 2.0 format using the given sorts and decls. 9381  The arguments sorts and decls are Python dictionaries used to initialize 9382  the symbol table used for the SMT 2.0 parser. 9384  >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 9386  >>> x, y = Ints('x y') 9387  >>> f = Function('f', IntSort(), IntSort()) 9388  >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 9390  >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 9394

ssz, snames, ssorts = _dict2sarray(sorts, ctx)

9395

dsz, dnames, ddecls = _dict2darray(decls, ctx)

Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])

Parse the given string using the SMT-LIB2 parser.

def parse_smt2_string(s, sorts={}, decls={}, ctx=None)

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

8503 def ParThen

(t1, t2, ctx=None):

8504  """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. 8505  The subgoals are processed in parallel. 8507  >>> x, y = Ints('x y') 8508  >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 8509  >>> t(And(Or(x == 1, x == 2), y == x + 1)) 8510  [[x == 1, y == 2], [x == 2, y == 3]] 8512

t1 = _to_tactic(t1, ctx)

8513

t2 = _to_tactic(t2, ctx)

8515

_z3_assert(t1.ctx == t2.ctx,

"Context mismatch"

)

Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)

Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....

Referenced by ParAndThen().

◆ PartialOrder() def z3py.PartialOrder (   a,   index  )

Definition at line 11479 of file z3py.py.

Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)

create a partial ordering relation over signature a and index id.

def PartialOrder(a, index)

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

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

Definition at line 9155 of file z3py.py.

9155 def PbEq

(args, k, ctx=None):

9156  """Create a Pseudo-Boolean equality k constraint. 9158  >>> a, b, c = Bools('a b c') 9159  >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 9161

_z3_check_cint_overflow(k,

"k"

)

9162

ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)

9163  return

BoolRef(

Z3_mk_pbeq

(ctx.ref(), sz, _args, _coeffs, k), ctx)

Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)

Pseudo-Boolean relations.

def PbEq(args, k, ctx=None)

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

9145  """Create a Pseudo-Boolean inequality k constraint. 9147  >>> a, b, c = Bools('a b c') 9148  >>> f = PbGe(((a,1),(b,3),(c,2)), 3) 9150

_z3_check_cint_overflow(k,

"k"

)

9151

ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)

9152  return

BoolRef(

Z3_mk_pbge

(ctx.ref(), sz, _args, _coeffs, k), ctx)

Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)

Pseudo-Boolean relations.

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

9134  """Create a Pseudo-Boolean inequality k constraint. 9136  >>> a, b, c = Bools('a b c') 9137  >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 9139

_z3_check_cint_overflow(k,

"k"

)

9140

ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)

9141  return

BoolRef(

Z3_mk_pble

(ctx.ref(), sz, _args, _coeffs, k), ctx)

Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)

Pseudo-Boolean relations.

◆ PiecewiseLinearOrder() def z3py.PiecewiseLinearOrder (   a,   index  )

Definition at line 11491 of file z3py.py.

Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)

create a piecewise linear ordering relation over signature a and index id.

def PiecewiseLinearOrder(a, index)

◆ Plus() 
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 11383 of file z3py.py.

11384  """Create the regular expression accepting one or more repetitions of argument. 11385  >>> re = Plus(Re("a")) 11386  >>> print(simplify(InRe("aa", re))) 11388  >>> print(simplify(InRe("ab", re))) 11390  >>> print(simplify(InRe("", re))) 11394

_z3_assert(

is_expr

(re),

"expression expected"

)

11395  return

ReRef(

Z3_mk_re_plus

(re.ctx_ref(), re.as_ast()), re.ctx)

Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)

Create the regular language re+.

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

11129  """Check if 'a' is a prefix of 'b' 11130  >>> s1 = PrefixOf("ab", "abc") 11133  >>> s2 = PrefixOf("bc", "abc") 11137

ctx = _get_ctx2(a, b)

11138

a = _coerce_seq(a, ctx)

11139

b = _coerce_seq(b, ctx)

11140  return

BoolRef(

Z3_mk_seq_prefix

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)

Check if prefix is a prefix of s.

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

8800  """Return a short description for the probe named `name`. 8802  >>> d = probe_description('memory')

Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)

Return a string containing a description of the probe with the given name.

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

8789  """Return a list of all available probes in Z3. 8792  >>> l.count('memory') == 1

unsigned Z3_API Z3_get_num_probes(Z3_context c)

Return the number of builtin probes available in Z3.

Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)

Return the name of the i probe.

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

9041  """Create the product of the Z3 expressions. 9043  >>> a, b, c = Ints('a b c') 9044  >>> Product(a, b, c) 9046  >>> Product([a, b, c]) 9048  >>> A = IntVector('a', 5) 9050  a__0*a__1*a__2*a__3*a__4 9052

args = _get_args(args)

9055

ctx = _ctx_from_ast_arg_list(args)

9057  return

_reduce(

lambda

a, b: a * b, args, 1)

9058

args = _coerce_expr_list(args, ctx)

9060  return

_reduce(

lambda

a, b: a * b, args, 1)

9062

_args, sz = _to_ast_array(args)

9063  return

ArithRef(

Z3_mk_mul

(ctx.ref(), sz, _args), ctx)

Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] * ... * args[num_args-1].

◆ PropagateFunction() def z3py.PropagateFunction (   name, *  sig  ) 
Create a function that gets tracked by user propagator.
   Every term headed by this function symbol is tracked.
   If a term is fixed and the fixed callback is registered a
   callback is invoked that the term headed by this function is fixed.

Definition at line 11677 of file z3py.py.

11678  """Create a function that gets tracked by user propagator. 11679  Every term headed by this function symbol is tracked. 11680  If a term is fixed and the fixed callback is registered a 11681  callback is invoked that the term headed by this function is fixed. 11683

sig = _get_args(sig)

11685

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

11686

arity = len(sig) - 1

11689

_z3_assert(

is_sort

(rng),

"Z3 sort expected"

)

11690

dom = (Sort * arity)()

11691  for

i

in range

(arity):

11693

_z3_assert(

is_sort

(sig[i]),

"Z3 sort expected"

)

11694

dom[i] = sig[i].ast

Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)

def PropagateFunction(name, *sig)

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

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

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

Definition at line 9227 of file z3py.py.

9227 def prove

(claim, show=False, **keywords):

9228  """Try to prove the given claim. 9230  This is a simple function for creating demonstrations. It tries to prove 9231  `claim` by showing the negation is unsatisfiable. 9233  >>> p, q = Bools('p q') 9234  >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 9238

_z3_assert(

is_bool

(claim),

"Z3 Boolean expression expected"

)

9248

print(

"failed to prove"

)

9251

print(

"counterexample"

)

def prove(claim, show=False, **keywords)

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

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

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

Definition at line 3281 of file z3py.py.

3281 def Q

(a, b, ctx=None):

3282  """Return a Z3 rational a/b. 3284  If `ctx=None`, then the global context is used.

def simplify(a, *arguments, **keywords)

Utils.

def RatVal(a, b, ctx=None)

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

Definition at line 11448 of file z3py.py.

11448 def Range

(lo, hi, ctx=None):

11449  """Create the range regular expression over two sequences of length 1 11450  >>> range = Range("a","z") 11451  >>> print(simplify(InRe("b", range))) 11453  >>> print(simplify(InRe("bb", range))) 11456

lo = _coerce_seq(lo, ctx)

11457

hi = _coerce_seq(hi, ctx)

11459

_z3_assert(

is_expr

(lo),

"expression expected"

)

11460

_z3_assert(

is_expr

(hi),

"expression expected"

)

11461  return

ReRef(

Z3_mk_re_range

(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)

Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)

Create the range regular expression over two sequences of length 1.

def Range(lo, hi, ctx=None)

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

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

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

Definition at line 3265 of file z3py.py.

3265 def RatVal

(a, b, ctx=None):

3266  """Return a Z3 rational a/b. 3268  If `ctx=None`, then the global context is used. 3272  >>> RatVal(3,5).sort() 3276

_z3_assert(_is_int(a)

or

isinstance(a, str),

"First argument cannot be converted into an integer"

)

3277

_z3_assert(_is_int(b)

or

isinstance(b, str),

"Second argument cannot be converted into an integer"

)

Referenced by Q().

◆ Re() def z3py.Re (   s,   ctx = None  ) 
The regular expression that accepts sequence 's'
>>> s1 = Re("ab")
>>> s2 = Re(StringVal("ab"))
>>> s3 = Re(Unit(BoolVal(True)))

Definition at line 11292 of file z3py.py.

11292 def Re

(s, ctx=None):

11293  """The regular expression that accepts sequence 's' 11295  >>> s2 = Re(StringVal("ab")) 11296  >>> s3 = Re(Unit(BoolVal(True))) 11298

s = _coerce_seq(s, ctx)

Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)

Create a regular expression that accepts the sequence seq.

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

>>> x = Real('x')
>>> is_real(x)
True
>>> is_real(x + 1)
True

Definition at line 3347 of file z3py.py.

3347 def Real

(name, ctx=None):

3348  """Return a real constant named `name`. If `ctx=None`, then the global context is used.

Referenced by Reals(), and RealVector().

◆ Reals() def z3py.Reals (   names,   ctx = None  ) 
Return a tuple of real constants.

>>> x, y, z = Reals('x y z')
>>> Sum(x, y, z)
x + y + z
>>> Sum(x, y, z).sort()
Real

Definition at line 3360 of file z3py.py.

3360 def Reals

(names, ctx=None):

3361  """Return a tuple of real constants. 3363  >>> x, y, z = Reals('x y z') 3366  >>> Sum(x, y, z).sort() 3370  if

isinstance(names, str):

3371

names = names.split(

" "

)

3372  return

[

Real

(name, ctx)

for

name

in

names]

def Reals(names, ctx=None)

◆ RealSort() def z3py.RealSort (   ctx = None ) 
Return the real sort in the given context. If `ctx=None`, then the global context is used.

>>> RealSort()
Real
>>> x = Const('x', RealSort())
>>> is_real(x)
True
>>> is_int(x)
False
>>> x.sort() == RealSort()
True

Definition at line 3205 of file z3py.py.

3206  """Return the real sort in the given context. If `ctx=None`, then the global context is used. 3210  >>> x = Const('x', RealSort()) 3215  >>> x.sort() == RealSort()

Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)

Create the real type.

Referenced by FreshReal(), Context.getRealSort(), Context.mkRealSort(), Real(), RealVal(), and RealVar().

◆ RealVal() def z3py.RealVal (   val,   ctx = None  ) 
Return a Z3 real value.

`val` may be a Python int, long, float or string representing a number in decimal or rational notation.
If `ctx=None`, then the global context is used.

>>> RealVal(1)
1
>>> RealVal(1).sort()
Real
>>> RealVal("3/5")
3/5
>>> RealVal("1.5")
3/2

Definition at line 3246 of file z3py.py.

3247  """Return a Z3 real value. 3249  `val` may be a Python int, long, float or string representing a number in decimal or rational notation. 3250  If `ctx=None`, then the global context is used. 3254  >>> RealVal(1).sort()

Referenced by Cbrt(), deserialize(), AlgebraicNumRef.index(), RatVal(), and Sqrt().

◆ RealVar() def z3py.RealVar (   idx,   ctx = None  ) 
Create a real free variable. Free variables are used to create quantified formulas.
They are also used to create polynomials.

>>> RealVar(0)
Var(0)

Definition at line 1503 of file z3py.py.

1505  Create a real free variable. Free variables are used to create quantified formulas. 1506  They are also used to create polynomials.

def RealVar(idx, ctx=None)

Referenced by RealVarVector().

◆ RealVarVector() def z3py.RealVarVector (   n,   ctx = None  ) 
Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1

>>> x0, x1, x2, x3 = RealVarVector(4)
>>> x2
Var(2)

Definition at line 1514 of file z3py.py.

1516  Create a list of Real free variables. 1517  The variables have ids: 0, 1, ..., n-1 1519  >>> x0, x1, x2, x3 = RealVarVector(4)

def RealVarVector(n, ctx=None)

◆ RealVector() def z3py.RealVector (   prefix,   sz,   ctx = None  ) 
Return a list of real constants of size `sz`.

>>> X = RealVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
>>> Sum(X).sort()
Real

Definition at line 3375 of file z3py.py.

3376  """Return a list of real constants of size `sz`. 3378  >>> X = RealVector('x', 3) 3387  return

[

Real

(

"%s__%s"

% (prefix, i), ctx)

for

i

in range

(sz)]

def RealVector(prefix, sz, ctx=None)

◆ RecAddDefinition() def z3py.RecAddDefinition (   f,   args,   body  ) 
Set the body of a recursive function.
   Recursive definitions can be simplified if they are applied to ground
   arguments.
>>> ctx = Context()
>>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
>>> n = Int('n', ctx)
>>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
>>> simplify(fac(5))
120
>>> s = Solver(ctx=ctx)
>>> s.add(fac(n) < 3)
>>> s.check()
sat
>>> s.model().eval(fac(5))
120

Definition at line 945 of file z3py.py.

946  """Set the body of a recursive function. 947  Recursive definitions can be simplified if they are applied to ground 950  >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) 951  >>> n = Int('n', ctx) 952  >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) 955  >>> s = Solver(ctx=ctx) 956  >>> s.add(fac(n) < 3) 959  >>> s.model().eval(fac(5)) 965

args = _get_args(args)

969

_args[i] = args[i].ast

void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)

Define the body of a recursive function.

def RecAddDefinition(f, args, body)

◆ RecFunction() def z3py.RecFunction (   name, *  sig  ) 
Create a new Z3 recursive with the given sorts.

Definition at line 927 of file z3py.py.

928  """Create a new Z3 recursive with the given sorts.""" 931

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

935

_z3_assert(

is_sort

(rng),

"Z3 sort expected"

)

936

dom = (Sort * arity)()

937  for

i

in range

(arity):

939

_z3_assert(

is_sort

(sig[i]),

"Z3 sort expected"

)

Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a recursive function.

def RecFunction(name, *sig)

◆ Repeat() def z3py.Repeat (   t,   max = 4294967295,   ctx = None  ) 
Return a tactic that keeps applying `t` until the goal is not modified anymore
or the maximum number of iterations `max` is reached.

>>> x, y = Ints('x y')
>>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
>>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
>>> r = t(c)
>>> for subgoal in r: print(subgoal)
[x == 0, y == 0, x > y]
[x == 0, y == 1, x > y]
[x == 1, y == 0, x > y]
[x == 1, y == 1, x > y]
>>> t = Then(t, Tactic('propagate-values'))
>>> t(c)
[[x == 1, y == 0]]

Definition at line 8552 of file z3py.py.

8552 def Repeat

(t, max=4294967295, ctx=None):

8553  """Return a tactic that keeps applying `t` until the goal is not modified anymore 8554  or the maximum number of iterations `max` is reached. 8556  >>> x, y = Ints('x y') 8557  >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 8558  >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 8560  >>> for subgoal in r: print(subgoal) 8561  [x == 0, y == 0, x > y] 8562  [x == 0, y == 1, x > y] 8563  [x == 1, y == 0, x > y] 8564  [x == 1, y == 1, x > y] 8565  >>> t = Then(t, Tactic('propagate-values')) 8569

t = _to_tactic(t, ctx)

Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)

Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...

def Repeat(t, max=4294967295, ctx=None)

◆ RepeatBitVec() def z3py.RepeatBitVec (   n,   a  ) 
Return an expression representing `n` copies of `a`.

>>> x = BitVec('x', 8)
>>> n = RepeatBitVec(4, x)
>>> n
RepeatBitVec(4, x)
>>> n.size()
32
>>> v0 = BitVecVal(10, 4)
>>> print("%.x" % v0.as_long())
a
>>> v = simplify(RepeatBitVec(4, v0))
>>> v.size()
16
>>> print("%.x" % v.as_long())
aaaa

Definition at line 4467 of file z3py.py.

4468  """Return an expression representing `n` copies of `a`. 4470  >>> x = BitVec('x', 8) 4471  >>> n = RepeatBitVec(4, x) 4476  >>> v0 = BitVecVal(10, 4) 4477  >>> print("%.x" % v0.as_long()) 4479  >>> v = simplify(RepeatBitVec(4, v0)) 4482  >>> print("%.x" % v.as_long()) 4486

_z3_assert(_is_int(n),

"First argument must be an integer"

)

4487

_z3_assert(

is_bv

(a),

"Second argument must be a Z3 bit-vector expression"

)

4488  return

BitVecRef(

Z3_mk_repeat

(a.ctx_ref(), n, a.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)

Repeat the given bit-vector up length i.

◆ Replace() def z3py.Replace (   s,   src,   dst  ) 
Replace the first occurrence of 'src' by 'dst' in 's'
>>> r = Replace("aaa", "a", "b")
>>> simplify(r)
"baa"

Definition at line 11177 of file z3py.py.

11178  """Replace the first occurrence of 'src' by 'dst' in 's' 11179  >>> r = Replace("aaa", "a", "b") 11183

ctx = _get_ctx2(dst, s)

11184  if

ctx

is None and is_expr

(src):

11186

src = _coerce_seq(src, ctx)

11187

dst = _coerce_seq(dst, ctx)

11188

s = _coerce_seq(s, ctx)

11189  return

SeqRef(

Z3_mk_seq_replace

(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)

Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)

Replace the first occurrence of src with dst in s.

◆ reset_params() def z3py.reset_params ( ) 
Reset all global (or module) parameters.

Definition at line 295 of file z3py.py.

296  """Reset all global (or module) parameters.

void Z3_API Z3_global_param_reset_all(void)

Restore the value of all global (and module) parameters. This command will not affect already created...

◆ ReSort()

Definition at line 11311 of file z3py.py.

11313  return

ReSortRef(

Z3_mk_re_sort

(s.ctx.ref(), s.ast), s.ctx)

11314  if

s

is None or

isinstance(s, Context):

11317  raise

Z3Exception(

"Regular expression sort constructor expects either a string or a context or no argument"

)

Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)

Create a regular expression sort out of a sequence sort.

Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)

Create a sort for unicode strings.

Referenced by Context.MkReSort().

◆ RNA() def z3py.RNA (   ctx = None )

Definition at line 9814 of file z3py.py.

Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c)

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Referenced by get_default_rounding_mode().

◆ RNE() def z3py.RNE (   ctx = None )

Definition at line 9804 of file z3py.py.

Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c)

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Referenced by get_default_rounding_mode().

◆ RotateLeft() def z3py.RotateLeft (   a,   b  ) 
Return an expression representing `a` rotated to the left `b` times.

>>> a, b = BitVecs('a b', 16)
>>> RotateLeft(a, b)
RotateLeft(a, b)
>>> simplify(RotateLeft(a, 0))
a
>>> simplify(RotateLeft(a, 16))
a

Definition at line 4377 of file z3py.py.

4378  """Return an expression representing `a` rotated to the left `b` times. 4380  >>> a, b = BitVecs('a b', 16) 4381  >>> RotateLeft(a, b) 4383  >>> simplify(RotateLeft(a, 0)) 4385  >>> simplify(RotateLeft(a, 16)) 4388

_check_bv_args(a, b)

4389

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)

Rotate bits of t1 to the left t2 times.

◆ RotateRight() def z3py.RotateRight (   a,   b  ) 
Return an expression representing `a` rotated to the right `b` times.

>>> a, b = BitVecs('a b', 16)
>>> RotateRight(a, b)
RotateRight(a, b)
>>> simplify(RotateRight(a, 0))
a
>>> simplify(RotateRight(a, 16))
a

Definition at line 4393 of file z3py.py.

4394  """Return an expression representing `a` rotated to the right `b` times. 4396  >>> a, b = BitVecs('a b', 16) 4397  >>> RotateRight(a, b) 4399  >>> simplify(RotateRight(a, 0)) 4401  >>> simplify(RotateRight(a, 16)) 4404

_check_bv_args(a, b)

4405

a, b = _coerce_exprs(a, b)

Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)

Rotate bits of t1 to the right t2 times.

◆ RoundNearestTiesToAway() def z3py.RoundNearestTiesToAway (   ctx = None )

Definition at line 9809 of file z3py.py.

def RoundNearestTiesToAway(ctx=None)

◆ RoundNearestTiesToEven() def z3py.RoundNearestTiesToEven (   ctx = None )

Definition at line 9799 of file z3py.py.

def RoundNearestTiesToEven(ctx=None)

◆ RoundTowardNegative() def z3py.RoundTowardNegative (   ctx = None )

Definition at line 9829 of file z3py.py.

Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

def RoundTowardNegative(ctx=None)

◆ RoundTowardPositive() def z3py.RoundTowardPositive (   ctx = None )

Definition at line 9819 of file z3py.py.

Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

def RoundTowardPositive(ctx=None)

◆ RoundTowardZero() def z3py.RoundTowardZero (   ctx = None )

Definition at line 9839 of file z3py.py.

Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

def RoundTowardZero(ctx=None)

◆ RTN() def z3py.RTN (   ctx = None ) ◆ RTP() def z3py.RTP (   ctx = None ) ◆ RTZ() def z3py.RTZ (   ctx = None ) ◆ Select() def z3py.Select (   a, *  args  ) 
Return a Z3 select array expression.

>>> a = Array('a', IntSort(), IntSort())
>>> i = Int('i')
>>> Select(a, i)
a[i]
>>> eq(Select(a, i), a[i])
True

Definition at line 4853 of file z3py.py.

4854  """Return a Z3 select array expression. 4856  >>> a = Array('a', IntSort(), IntSort()) 4860  >>> eq(Select(a, i), a[i]) 4863

args = _get_args(args)

4865

_z3_assert(

is_array_sort

(a),

"First argument must be a Z3 array expression"

)

◆ SeqFoldLeft() def z3py.SeqFoldLeft (   f,   a,   s  )

Definition at line 11244 of file z3py.py.

11245

ctx = _get_ctx2(f, s)

11246

s = _coerce_seq(s, ctx)

11248  return

_to_expr_ref(

Z3_mk_seq_foldl

(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s)

Create a fold of the function f over the sequence s with accumulator a.

◆ SeqFoldLeftI() def z3py.SeqFoldLeftI (   f,   i,   a,   s  )

Definition at line 11250 of file z3py.py.

11251

ctx = _get_ctx2(f, s)

11252

s = _coerce_seq(s, ctx)

11255  return

_to_expr_ref(

Z3_mk_seq_foldli

(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s)

Create a fold with index tracking of the function f over the sequence s with accumulator a starting a...

def SeqFoldLeftI(f, i, a, s)

◆ SeqMap() 
Map function 'f' over sequence 's'

Definition at line 11230 of file z3py.py.

11231  """Map function 'f' over sequence 's'""" 11232

ctx = _get_ctx2(f, s)

11233

s = _coerce_seq(s, ctx)

11234  return

_to_expr_ref(

Z3_mk_seq_map

(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s)

Create a map of the function f over the sequence s.

◆ SeqMapI() def z3py.SeqMapI (   f,   i,   s  ) 
Map function 'f' over sequence 's' at index 'i'

Definition at line 11236 of file z3py.py.

11237  """Map function 'f' over sequence 's' at index 'i'""" 11238

ctx = _get_ctx(f, s)

11239

s = _coerce_seq(s, ctx)

11242  return

_to_expr_ref(

Z3_mk_seq_mapi

(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s)

Create a map of the function f over the sequence s starting at index i.

◆ SeqSort() 
Create a sequence sort over elements provided in the argument
>>> s = SeqSort(IntSort())
>>> s == Unit(IntVal(1)).sort()
True

Definition at line 10898 of file z3py.py.

10899  """Create a sequence sort over elements provided in the argument 10900  >>> s = SeqSort(IntSort()) 10901  >>> s == Unit(IntVal(1)).sort()

Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)

Create a sequence sort out of the sort for the elements.

Referenced by Context.MkSeqSort().

◆ set_default_fp_sort() def z3py.set_default_fp_sort (   ebits,   sbits,   ctx = None  )

Definition at line 9460 of file z3py.py.

9461  global

_dflt_fpsort_ebits

9462  global

_dflt_fpsort_sbits

9463

_dflt_fpsort_ebits = ebits

9464

_dflt_fpsort_sbits = sbits

def set_default_fp_sort(ebits, sbits, ctx=None)

◆ set_default_rounding_mode() def z3py.set_default_rounding_mode (   rm,   ctx = None  )

Definition at line 9447 of file z3py.py.

9448  global

_dflt_rounding_mode

9450

_dflt_rounding_mode = rm.decl().kind()

9452

_z3_assert(_dflt_rounding_mode

in

_ROUNDING_MODES,

"illegal rounding mode"

)

9453

_dflt_rounding_mode = rm

def set_default_rounding_mode(rm, ctx=None)

◆ set_option() def z3py.set_option ( *  args, **  kws  ) 
Alias for 'set_param' for backward compatibility.

Definition at line 301 of file z3py.py.

302  """Alias for 'set_param' for backward compatibility.

def set_option(*args, **kws)

def set_param(*args, **kws)

◆ set_param() def z3py.set_param ( *  args, **  kws  ) 
Set Z3 global (or module) parameters.

>>> set_param(precision=10)

Definition at line 271 of file z3py.py.

272  """Set Z3 global (or module) parameters. 274  >>> set_param(precision=10) 277

_z3_assert(len(args) % 2 == 0,

"Argument list must have an even number of elements."

)

281  if not

set_pp_option(k, v):

void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)

Set a global (or module) parameter. This setting is shared by all Z3 contexts.

Referenced by set_option().

◆ SetAdd() 
 Add element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetAdd(a, 1)
Store(a, 1, True)

Definition at line 5012 of file z3py.py.

5013  """ Add element e to set s 5014  >>> a = Const('a', SetSort(IntSort())) 5018

ctx = _ctx_from_ast_arg_list([s, e])

5019

e = _py2expr(e, ctx)

5020  return

ArrayRef(

Z3_mk_set_add

(ctx.ref(), s.as_ast(), e.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)

Add an element to a set.

◆ SetComplement() def z3py.SetComplement (   s ) 
 The complement of set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
complement(a)

Definition at line 5034 of file z3py.py.

5035  """ The complement of set s 5036  >>> a = Const('a', SetSort(IntSort())) 5037  >>> SetComplement(a)

Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)

Take the complement of a set.

◆ SetDel() 
 Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)

Definition at line 5023 of file z3py.py.

5024  """ Remove element e to set s 5025  >>> a = Const('a', SetSort(IntSort())) 5029

ctx = _ctx_from_ast_arg_list([s, e])

5030

e = _py2expr(e, ctx)

5031  return

ArrayRef(

Z3_mk_set_del

(ctx.ref(), s.as_ast(), e.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)

Remove an element to a set.

◆ SetDifference() def z3py.SetDifference (   a,   b  ) 
 The set difference of a and b
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetDifference(a, b)
setminus(a, b)

Definition at line 5044 of file z3py.py.

5045  """ The set difference of a and b 5046  >>> a = Const('a', SetSort(IntSort())) 5047  >>> b = Const('b', SetSort(IntSort())) 5048  >>> SetDifference(a, b) 5051

ctx = _ctx_from_ast_arg_list([a, b])

Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Take the set difference between two sets.

◆ SetHasSize() def z3py.SetHasSize (   a,   k  )

Definition at line 4926 of file z3py.py.

4928

k = _py2expr(k, ctx)

Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k)

Create predicate that holds if Boolean array set has k elements set to true.

◆ SetIntersect() def z3py.SetIntersect ( *  args ) 
 Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetIntersect(a, b)
intersection(a, b)

Definition at line 4999 of file z3py.py.

5000  """ Take the union of sets 5001  >>> a = Const('a', SetSort(IntSort())) 5002  >>> b = Const('b', SetSort(IntSort())) 5003  >>> SetIntersect(a, b) 5006

args = _get_args(args)

5007

ctx = _ctx_from_ast_arg_list(args)

5008

_args, sz = _to_ast_array(args)

Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])

Take the intersection of a list of sets.

◆ SetSort()

Sets.

 Create a set sort over element sort s

Definition at line 4963 of file z3py.py.

4964  """ Create a set sort over element sort s"""

Referenced by Context.MkSetSort().

◆ SetUnion() def z3py.SetUnion ( *  args ) 
 Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetUnion(a, b)
union(a, b)

Definition at line 4986 of file z3py.py.

4987  """ Take the union of sets 4988  >>> a = Const('a', SetSort(IntSort())) 4989  >>> b = Const('b', SetSort(IntSort())) 4993

args = _get_args(args)

4994

ctx = _ctx_from_ast_arg_list(args)

4995

_args, sz = _to_ast_array(args)

Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])

Take the union of a list of sets.

◆ SignExt() def z3py.SignExt (   n,   a  ) 
Return a bit-vector expression with `n` extra sign-bits.

>>> x = BitVec('x', 16)
>>> n = SignExt(8, x)
>>> n.size()
24
>>> n
SignExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(SignExt(6, v0))
>>> v
254
>>> v.size()
8
>>> print("%.x" % v.as_long())
fe

Definition at line 4409 of file z3py.py.

4410  """Return a bit-vector expression with `n` extra sign-bits. 4412  >>> x = BitVec('x', 16) 4413  >>> n = SignExt(8, x) 4420  >>> v0 = BitVecVal(2, 2) 4425  >>> v = simplify(SignExt(6, v0)) 4430  >>> print("%.x" % v.as_long()) 4434

_z3_assert(_is_int(n),

"First argument must be an integer"

)

4435

_z3_assert(

is_bv

(a),

"Second argument must be a Z3 bit-vector expression"

)

4436  return

BitVecRef(

Z3_mk_sign_ext

(a.ctx_ref(), n, a.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)

Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...

◆ SimpleSolver() def z3py.SimpleSolver (   ctx = None,   logFile = None  ) 
Return a simple general purpose solver with limited amount of preprocessing.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat

Definition at line 7486 of file z3py.py.

7487  """Return a simple general purpose solver with limited amount of preprocessing. 7489  >>> s = SimpleSolver()

Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)

Create a new incremental solver.

def SimpleSolver(ctx=None, logFile=None)

◆ simplify() def z3py.simplify (   a, *  arguments, **  keywords  )

Utils.

Simplify the expression `a` using the given options.

This function has many options. Use `help_simplify` to obtain the complete list.

>>> x = Int('x')
>>> y = Int('y')
>>> simplify(x + 1 + y + x + 1)
2 + 2*x + y
>>> simplify((x + 1)*(y + 1), som=True)
1 + x + y + x*y
>>> simplify(Distinct(x, y, 1), blast_distinct=True)
And(Not(x == y), Not(x == 1), Not(y == 1))
>>> simplify(And(x == 0, y == 1), elim_and=True)
Not(Or(Not(x == 0), Not(y == 1)))

Definition at line 8904 of file z3py.py.

8904 def simplify

(a, *arguments, **keywords):

8905  """Simplify the expression `a` using the given options. 8907  This function has many options. Use `help_simplify` to obtain the complete list. 8911  >>> simplify(x + 1 + y + x + 1) 8913  >>> simplify((x + 1)*(y + 1), som=True) 8915  >>> simplify(Distinct(x, y, 1), blast_distinct=True) 8916  And(Not(x == y), Not(x == 1), Not(y == 1)) 8917  >>> simplify(And(x == 0, y == 1), elim_and=True) 8918  Not(Or(Not(x == 0), Not(y == 1))) 8921

_z3_assert(

is_expr

(a),

"Z3 expression expected"

)

8922  if

len(arguments) > 0

or

len(keywords) > 0:

8924  return

_to_expr_ref(

Z3_simplify_ex

(a.ctx_ref(), a.as_ast(), p.params), a.ctx)

8926  return

_to_expr_ref(

Z3_simplify

(a.ctx_ref(), a.as_ast()), a.ctx)

Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)

Interface to simplifier.

Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)

Interface to simplifier.

Referenced by Q(), RatVal(), and Expr< R extends Sort >.simplify().

◆ simplify_param_descrs() def z3py.simplify_param_descrs ( ) 
Return the set of parameter descriptions for Z3 `simplify` procedure.

Definition at line 8934 of file z3py.py.

8935  """Return the set of parameter descriptions for Z3 `simplify` procedure."""

Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)

Return the parameter description set for the simplify procedure.

def simplify_param_descrs()

◆ solve() def z3py.solve ( *  args, **  keywords  ) 
Solve the constraints `*args`.

This is a simple function for creating demonstrations. It creates a solver,
configure it using the options in `keywords`, adds the constraints
in `args`, and invokes check.

>>> a = Int('a')
>>> solve(a > 0, a < 2)
[a = 1]

Definition at line 9166 of file z3py.py.

9166 def solve

(*args, **keywords):

9167  """Solve the constraints `*args`. 9169  This is a simple function for creating demonstrations. It creates a solver, 9170  configure it using the options in `keywords`, adds the constraints 9171  in `args`, and invokes check. 9174  >>> solve(a > 0, a < 2) 9177

show = keywords.pop(

"show"

,

False

)

9185

print(

"no solution"

)

9187

print(

"failed to solve"

)

def solve(*args, **keywords)

◆ solve_using() def z3py.solve_using (   s, *  args, **  keywords  ) 
Solve the constraints `*args` using solver `s`.

This is a simple function for creating demonstrations. It is similar to `solve`,
but it uses the given solver `s`.
It configures solver `s` using the options in `keywords`, adds the constraints
in `args`, and invokes check.

Definition at line 9196 of file z3py.py.

9197  """Solve the constraints `*args` using solver `s`. 9199  This is a simple function for creating demonstrations. It is similar to `solve`, 9200  but it uses the given solver `s`. 9201  It configures solver `s` using the options in `keywords`, adds the constraints 9202  in `args`, and invokes check. 9204

show = keywords.pop(

"show"

,

False

)

9206

_z3_assert(isinstance(s, Solver),

"Solver object expected"

)

9214

print(

"no solution"

)

9216

print(

"failed to solve"

)

9223

print(

"Solution:"

)

def solve_using(s, *args, **keywords)

◆ SolverFor() def z3py.SolverFor (   logic,   ctx = None,   logFile = None  ) 
Create a solver customized for the given logic.

The parameter `logic` is a string. It should be contains
the name of a SMT-LIB logic.
See http://www.smtlib.org/ for the name of all available logics.

>>> s = SolverFor("QF_LIA")
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> s.check()
sat
>>> s.model()
[x = 1]

Definition at line 7465 of file z3py.py.

7465 def SolverFor

(logic, ctx=None, logFile=None):

7466  """Create a solver customized for the given logic. 7468  The parameter `logic` is a string. It should be contains 7469  the name of a SMT-LIB logic. 7470  See http://www.smtlib.org/ for the name of all available logics. 7472  >>> s = SolverFor("QF_LIA")

Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)

Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...

def SolverFor(logic, ctx=None, logFile=None)

◆ Sqrt() def z3py.Sqrt (   a,   ctx = None  ) 
 Return a Z3 expression which represents the square root of a.

>>> x = Real('x')
>>> Sqrt(x)
x**(1/2)

Definition at line 3457 of file z3py.py.

3457 def Sqrt

(a, ctx=None):

3458  """ Return a Z3 expression which represents the square root of a. ◆ SRem() 
Create the Z3 expression signed remainder.

Use the operator % for signed modulus, and URem() for unsigned remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SRem(x, y)
SRem(x, y)
>>> SRem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'

Definition at line 4324 of file z3py.py.

4325  """Create the Z3 expression signed remainder. 4327  Use the operator % for signed modulus, and URem() for unsigned remainder. 4329  >>> x = BitVec('x', 32) 4330  >>> y = BitVec('y', 32) 4333  >>> SRem(x, y).sort() 4337  >>> SRem(x, y).sexpr() 4340

_check_bv_args(a, b)

4341

a, b = _coerce_exprs(a, b)

4342  return

BitVecRef(

Z3_mk_bvsrem

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed remainder (sign follows dividend).

◆ Star() 
Create the regular expression accepting zero or more repetitions of argument.
>>> re = Star(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
True

Definition at line 11418 of file z3py.py.

11419  """Create the regular expression accepting zero or more repetitions of argument. 11420  >>> re = Star(Re("a")) 11421  >>> print(simplify(InRe("aa", re))) 11423  >>> print(simplify(InRe("ab", re))) 11425  >>> print(simplify(InRe("", re))) 11429

_z3_assert(

is_expr

(re),

"expression expected"

)

11430  return

ReRef(

Z3_mk_re_star

(re.ctx_ref(), re.as_ast()), re.ctx)

Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)

Create the regular language re*.

◆ Store() def z3py.Store (   a, *  args  ) 
Return a Z3 store array expression.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Store(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

Definition at line 4836 of file z3py.py.

4836 def Store

(a, *args):

4837  """Return a Z3 store array expression. 4839  >>> a = Array('a', IntSort(), IntSort()) 4840  >>> i, v = Ints('i v') 4841  >>> s = Store(a, i, v) 4844  >>> prove(s[i] == v) 4847  >>> prove(Implies(i != j, s[j] == a[j]))

Referenced by ModelRef.get_interp().

◆ StrFromCode() def z3py.StrFromCode (   c ) 
Convert code to a string

Definition at line 11286 of file z3py.py.

11287  """Convert code to a string"""

Z3_ast Z3_API Z3_mk_string_from_code(Z3_context c, Z3_ast a)

Code to string conversion.

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

>>> x = String('x')

Definition at line 11061 of file z3py.py.

11061 def String

(name, ctx=None):

11062  """Return a string constant named `name`. If `ctx=None`, then the global context is used. 11064  >>> x = String('x') 11066

ctx = _get_ctx(ctx)

def String(name, ctx=None)

Referenced by Context.Context(), Statistics.getEntries(), Statistics.getKeys(), Context.getProbeNames(), Context.getSimplifierNames(), Context.getTacticNames(), Context.mkString(), Strings(), and FuncInterp< R extends Sort >.toString().

◆ Strings() def z3py.Strings (   names,   ctx = None  ) 
Return a tuple of String constants.

Definition at line 11070 of file z3py.py.

11070 def Strings

(names, ctx=None):

11071  """Return a tuple of String constants. """ 11072

ctx = _get_ctx(ctx)

11073  if

isinstance(names, str):

11074

names = names.split(

" "

)

11075  return

[

String

(name, ctx)

for

name

in

names]

def Strings(names, ctx=None)

◆ StringSort() def z3py.StringSort (   ctx = None ) 
Create a string sort
>>> s = StringSort()
>>> print(s)
String

Definition at line 10879 of file z3py.py.

10880  """Create a string sort 10881  >>> s = StringSort() 10885

ctx = _get_ctx(ctx)

Referenced by String().

◆ StringVal() def z3py.StringVal (   s,   ctx = None  ) 
create a string expression

Definition at line 11054 of file z3py.py.

11055  """create a string expression""" 11056

s =

""

.join(str(ch)

if

32 <= ord(ch)

and

ord(ch) < 127

else "\\u{%x}"

% (ord(ch))

for

ch

in

s)

11057

ctx = _get_ctx(ctx)

Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)

Create a string constant out of the string that is passed in The string may contain escape encoding f...

Referenced by CharIsDigit(), deserialize(), Extract(), and AlgebraicNumRef.index().

◆ StrToCode() 
Convert a unit length string to integer code

Definition at line 11280 of file z3py.py.

11281  """Convert a unit length string to integer code"""

Z3_ast Z3_API Z3_mk_string_to_code(Z3_context c, Z3_ast a)

String to code conversion.

◆ StrToInt() 
Convert string expression to integer
>>> a = StrToInt("1")
>>> simplify(1 == a)
True
>>> b = StrToInt("2")
>>> simplify(1 == b)
False
>>> c = StrToInt(IntToStr(2))
>>> simplify(1 == c)
False

Definition at line 11257 of file z3py.py.

11258  """Convert string expression to integer 11259  >>> a = StrToInt("1") 11260  >>> simplify(1 == a) 11262  >>> b = StrToInt("2") 11263  >>> simplify(1 == b) 11265  >>> c = StrToInt(IntToStr(2)) 11266  >>> simplify(1 == c)

Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)

Convert string to integer.

◆ SubSeq() def z3py.SubSeq (   s,   offset,   length  ) 
Extract substring or subsequence starting at offset

Definition at line 11083 of file z3py.py.

11083 def SubSeq

(s, offset, length):

11084  """Extract substring or subsequence starting at offset""" 11085  return Extract

(s, offset, length)

def SubSeq(s, offset, length)

◆ substitute() def z3py.substitute (   t, *  m  ) 
Apply substitution m on t, m is a list of pairs of the form (from, to).
Every occurrence in t of from is replaced with to.

>>> x = Int('x')
>>> y = Int('y')
>>> substitute(x + 1, (x, y + 1))
y + 1 + 1
>>> f = Function('f', IntSort(), IntSort())
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
1 + 1

Definition at line 8939 of file z3py.py.

8940  """Apply substitution m on t, m is a list of pairs of the form (from, to). 8941  Every occurrence in t of from is replaced with to. 8945  >>> substitute(x + 1, (x, y + 1)) 8947  >>> f = Function('f', IntSort(), IntSort()) 8948  >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 8951  if

isinstance(m, tuple):

8953  if

isinstance(m1, list)

and

all(isinstance(p, tuple)

for

p

in

m1):

8956

_z3_assert(

is_expr

(t),

"Z3 expression expected"

)

8958

all([isinstance(p, tuple)

and is_expr

(p[0])

and is_expr

(p[1])

for

p

in

m]),

8959  "Z3 invalid substitution, expression pairs expected."

)

8961

all([p[0].sort().

eq

(p[1].sort())

for

p

in

m]),

8962  'Z3 invalid substitution, mismatching "from" and "to" sorts.'

)

8964

_from = (Ast * num)()

8966  for

i

in range

(num):

8967

_from[i] = m[i][0].as_ast()

8968

_to[i] = m[i][1].as_ast()

8969  return

_to_expr_ref(

Z3_substitute

(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)

Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])

Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....

Referenced by Expr< R extends Sort >.substitute().

◆ substitute_funs() def z3py.substitute_funs (   t, *  m  ) 
Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
Every occurrence in to of the function from is replaced with the expression to.
The expression to can have free variables, that refer to the arguments of from.
For examples, see

Definition at line 8992 of file z3py.py.

8993  """Apply substitution m on t, m is a list of pairs of a function and expression (from, to) 8994  Every occurrence in to of the function from is replaced with the expression to. 8995  The expression to can have free variables, that refer to the arguments of from. 8998  if

isinstance(m, tuple):

9000  if

isinstance(m1, list)

and

all(isinstance(p, tuple)

for

p

in

m1):

9003

_z3_assert(

is_expr

(t),

"Z3 expression expected"

)

9004

_z3_assert(all([isinstance(p, tuple)

and is_func_decl

(p[0])

and is_expr

(p[1])

for

p

in

m]),

"Z3 invalid substitution, function pairs expected."

)

9006

_from = (FuncDecl * num)()

9008  for

i

in range

(num):

9009

_from[i] = m[i][0].as_func_decl()

9010

_to[i] = m[i][1].as_ast()

9011  return

_to_expr_ref(

Z3_substitute_funs

(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)

Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])

Substitute functions in from with new expressions in to.

def substitute_funs(t, *m)

◆ substitute_vars() def z3py.substitute_vars (   t, *  m  ) 
Substitute the free variables in t with the expression in m.

>>> v0 = Var(0, IntSort())
>>> v1 = Var(1, IntSort())
>>> x  = Int('x')
>>> f  = Function('f', IntSort(), IntSort(), IntSort())
>>> # replace v0 with x+1 and v1 with x
>>> substitute_vars(f(v0, v1), x + 1, x)
f(x + 1, x)

Definition at line 8972 of file z3py.py.

8973  """Substitute the free variables in t with the expression in m. 8975  >>> v0 = Var(0, IntSort()) 8976  >>> v1 = Var(1, IntSort()) 8978  >>> f = Function('f', IntSort(), IntSort(), IntSort()) 8979  >>> # replace v0 with x+1 and v1 with x 8980  >>> substitute_vars(f(v0, v1), x + 1, x) 8984

_z3_assert(

is_expr

(t),

"Z3 expression expected"

)

8985

_z3_assert(all([

is_expr

(n)

for

n

in

m]),

"Z3 invalid substitution, list of expressions expected."

)

8988  for

i

in range

(num):

8989

_to[i] = m[i].as_ast()

Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])

Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...

def substitute_vars(t, *m)

◆ SubString() def z3py.SubString (   s,   offset,   length  ) 
Extract substring or subsequence starting at offset

Definition at line 11078 of file z3py.py.

11079  """Extract substring or subsequence starting at offset""" 11080  return Extract

(s, offset, length)

def SubString(s, offset, length)

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

Definition at line 11143 of file z3py.py.

11144  """Check if 'a' is a suffix of 'b' 11145  >>> s1 = SuffixOf("ab", "abc") 11148  >>> s2 = SuffixOf("bc", "abc") 11152

ctx = _get_ctx2(a, b)

11153

a = _coerce_seq(a, ctx)

11154

b = _coerce_seq(b, ctx)

11155  return

BoolRef(

Z3_mk_seq_suffix

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)

Check if suffix is a suffix of s.

◆ Sum() 
Create the sum of the Z3 expressions.

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

Definition at line 9014 of file z3py.py.

9015  """Create the sum of the Z3 expressions. 9017  >>> a, b, c = Ints('a b c') 9022  >>> A = IntVector('a', 5) 9024  a__0 + a__1 + a__2 + a__3 + a__4 9026

args = _get_args(args)

9029

ctx = _ctx_from_ast_arg_list(args)

9031  return

_reduce(

lambda

a, b: a + b, args, 0)

9032

args = _coerce_expr_list(args, ctx)

9034  return

_reduce(

lambda

a, b: a + b, args, 0)

9036

_args, sz = _to_ast_array(args)

9037  return

ArithRef(

Z3_mk_add

(ctx.ref(), sz, _args), ctx)

Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])

Create an AST node representing args[0] + ... + args[num_args-1].

◆ tactic_description() def z3py.tactic_description (   name,   ctx = None  ) 
Return a short description for the tactic named `name`.

>>> d = tactic_description('simplify')

Definition at line 8593 of file z3py.py.

8594  """Return a short description for the tactic named `name`. 8596  >>> d = tactic_description('simplify')

Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name)

Return a string containing a description of the tactic with the given name.

Referenced by describe_tactics().

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

>>> l = tactics()
>>> l.count('simplify') == 1
True

Definition at line 8582 of file z3py.py.

8583  """Return a list of all available tactics in Z3. 8586  >>> l.count('simplify') == 1

unsigned Z3_API Z3_get_num_tactics(Z3_context c)

Return the number of builtin tactics available in Z3.

Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)

Return the name of the idx tactic.

Referenced by describe_tactics().

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

>>> x, y = Ints('x y')
>>> t = Then(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 8450 of file z3py.py.

8450 def Then

(*ts, **ks):

8451  """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 8453  >>> x, y = Ints('x y') 8454  >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 8455  >>> t(And(x == 0, y > x + 1)) 8457  >>> t(And(x == 0, y > x + 1)).as_expr() ◆ to_Ast() ◆ to_AstVectorObj() def z3py.to_AstVectorObj (   ptr )

Definition at line 11512 of file z3py.py.

11513

v = AstVectorObj(ptr)

11514

super(ctypes.c_void_p, v).__init__(ptr)

Referenced by on_clause_eh().

◆ to_ContextObj() def z3py.to_ContextObj (   ptr )

Definition at line 11507 of file z3py.py.

11508

ctx = ContextObj(ptr)

11509

super(ctypes.c_void_p, ctx).__init__(ptr)

Referenced by user_prop_fresh().

◆ to_symbol() def z3py.to_symbol (   s,   ctx = None  ) 
Convert an integer or string into a Z3 symbol.

Definition at line 124 of file z3py.py.

125  """Convert an integer or string into a Z3 symbol."""

Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)

Create a Z3 symbol using a C string.

Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)

Create a Z3 symbol using an integer.

Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DatatypeSort(), DeclareSort(), DeclareTypeVar(), EnumSort(), FiniteDomainSort(), FP(), Function(), ParamDescrsRef.get_documentation(), ParamDescrsRef.get_kind(), Int(), is_quantifier(), PropagateFunction(), prove(), Real(), RecFunction(), ParamsRef.set(), Fixedpoint.set_predicate_representation(), SolverFor(), String(), and Fixedpoint.update_rule().

◆ ToInt() 
 Return the Z3 expression ToInt(a).

>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int

Definition at line 3422 of file z3py.py.

3423  """ Return the Z3 expression ToInt(a). 3435

_z3_assert(a.is_real(),

"Z3 real expression expected."

)

Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1)

Coerce a real to an integer.

◆ ToReal() 
 Return the Z3 expression ToReal(a).

>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real

Definition at line 3404 of file z3py.py.

3405  """ Return the Z3 expression ToReal(a). 3417

_z3_assert(a.is_int(),

"Z3 integer expression expected."

)

Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)

Coerce an integer to a real.

◆ TransitiveClosure() def z3py.TransitiveClosure (   f ) 
Given a binary relation R, such that the two arguments have the same sort
create the transitive closure relation R+.
The transitive closure R+ is a new relation.

Definition at line 11495 of file z3py.py.

11496  """Given a binary relation R, such that the two arguments have the same sort 11497  create the transitive closure relation R+. 11498  The transitive closure R+ is a new relation.

Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)

create transitive closure of binary relation.

◆ TreeOrder() def z3py.TreeOrder (   a,   index  )

Definition at line 11487 of file z3py.py.

Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)

create a tree ordering relation over signature a identified using index id.

◆ TryFor() def z3py.TryFor (   t,   ms,   ctx = None  ) 
Return a tactic that applies `t` to a given goal for `ms` milliseconds.

If `t` does not terminate in `ms` milliseconds, then it fails.

Definition at line 8573 of file z3py.py.

8573 def TryFor

(t, ms, ctx=None):

8574  """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 8576  If `t` does not terminate in `ms` milliseconds, then it fails. 8578

t = _to_tactic(t, ctx)

Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)

Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...

def TryFor(t, ms, ctx=None)

◆ TupleSort() def z3py.TupleSort (   name,   sorts,   ctx = None  ) 
Create a named tuple sort base on a set of underlying sorts
Example:
    >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])

Definition at line 5409 of file z3py.py.

5410  """Create a named tuple sort base on a set of underlying sorts 5412  >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()]) 5414

tuple = Datatype(name, ctx)

5415

projects = [(

"project%d"

% i, sorts[i])

for

i

in range

(len(sorts))]

5416

tuple.declare(name, *projects)

5417

tuple = tuple.create()

5418  return

tuple, tuple.constructor(0), [tuple.accessor(0, i)

for

i

in range

(len(sorts))]

def TupleSort(name, sorts, ctx=None)

Referenced by Context.MkTupleSort(), and Context.mkTupleSort().

◆ UDiv() 
Create the Z3 expression (unsigned) division `self / other`.

Use the operator / for signed division.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> UDiv(x, y)
UDiv(x, y)
>>> UDiv(x, y).sort()
BitVec(32)
>>> (x / y).sexpr()
'(bvsdiv x y)'
>>> UDiv(x, y).sexpr()
'(bvudiv x y)'

Definition at line 4282 of file z3py.py.

4283  """Create the Z3 expression (unsigned) division `self / other`. 4285  Use the operator / for signed division. 4287  >>> x = BitVec('x', 32) 4288  >>> y = BitVec('y', 32) 4291  >>> UDiv(x, y).sort() 4295  >>> UDiv(x, y).sexpr() 4298

_check_bv_args(a, b)

4299

a, b = _coerce_exprs(a, b)

4300  return

BitVecRef(

Z3_mk_bvudiv

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned division.

◆ UGE() 
Create the Z3 expression (unsigned) `other >= self`.

Use the operator >= for signed greater than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> UGE(x, y)
UGE(x, y)
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'

Definition at line 4246 of file z3py.py.

4247  """Create the Z3 expression (unsigned) `other >= self`. 4249  Use the operator >= for signed greater than or equal to. 4251  >>> x, y = BitVecs('x y', 32) 4254  >>> (x >= y).sexpr() 4256  >>> UGE(x, y).sexpr() 4259

_check_bv_args(a, b)

4260

a, b = _coerce_exprs(a, b)

4261  return

BoolRef(

Z3_mk_bvuge

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned greater than or equal to.

◆ UGT() 
Create the Z3 expression (unsigned) `other > self`.

Use the operator > for signed greater than.

>>> x, y = BitVecs('x y', 32)
>>> UGT(x, y)
UGT(x, y)
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'

Definition at line 4264 of file z3py.py.

4265  """Create the Z3 expression (unsigned) `other > self`. 4267  Use the operator > for signed greater than. 4269  >>> x, y = BitVecs('x y', 32) 4274  >>> UGT(x, y).sexpr() 4277

_check_bv_args(a, b)

4278

a, b = _coerce_exprs(a, b)

4279  return

BoolRef(

Z3_mk_bvugt

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned greater than.

◆ ULE() 
Create the Z3 expression (unsigned) `other <= self`.

Use the operator <= for signed less than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> ULE(x, y)
ULE(x, y)
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'

Definition at line 4210 of file z3py.py.

4211  """Create the Z3 expression (unsigned) `other <= self`. 4213  Use the operator <= for signed less than or equal to. 4215  >>> x, y = BitVecs('x y', 32) 4218  >>> (x <= y).sexpr() 4220  >>> ULE(x, y).sexpr() 4223

_check_bv_args(a, b)

4224

a, b = _coerce_exprs(a, b)

4225  return

BoolRef(

Z3_mk_bvule

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned less than or equal to.

◆ ULT() 
Create the Z3 expression (unsigned) `other < self`.

Use the operator < for signed less than.

>>> x, y = BitVecs('x y', 32)
>>> ULT(x, y)
ULT(x, y)
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'

Definition at line 4228 of file z3py.py.

4229  """Create the Z3 expression (unsigned) `other < self`. 4231  Use the operator < for signed less than. 4233  >>> x, y = BitVecs('x y', 32) 4238  >>> ULT(x, y).sexpr() 4241

_check_bv_args(a, b)

4242

a, b = _coerce_exprs(a, b)

4243  return

BoolRef(

Z3_mk_bvult

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned less than.

◆ Union() def z3py.Union ( *  args ) 
Create union of regular expressions.
>>> re = Union(Re("a"), Re("b"), Re("c"))
>>> print (simplify(InRe("d", re)))
False

Definition at line 11345 of file z3py.py.

11346  """Create union of regular expressions. 11347  >>> re = Union(Re("a"), Re("b"), Re("c")) 11348  >>> print (simplify(InRe("d", re))) 11351

args = _get_args(args)

11354

_z3_assert(sz > 0,

"At least one argument expected."

)

11355

_z3_assert(all([

is_re

(a)

for

a

in

args]),

"All arguments must be regular expressions."

)

11360  for

i

in range

(sz):

11361

v[i] = args[i].as_ast()

Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])

Create the union of the regular languages.

Referenced by ReRef.__add__().

◆ Unit() 
Create a singleton sequence

Definition at line 11123 of file z3py.py.

11124  """Create a singleton sequence"""

Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)

Create a unit sequence of a.

◆ Update() def z3py.Update (   a, *  args  ) 
Return a Z3 store array expression.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Update(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

Definition at line 4793 of file z3py.py.

4794  """Return a Z3 store array expression. 4796  >>> a = Array('a', IntSort(), IntSort()) 4797  >>> i, v = Ints('i v') 4798  >>> s = Update(a, i, v) 4801  >>> prove(s[i] == v) 4804  >>> prove(Implies(i != j, s[j] == a[j])) 4808

_z3_assert(

is_array_sort

(a),

"First argument must be a Z3 array expression"

)

4809

args = _get_args(args)

4812  raise

Z3Exception(

"array update requires index and value arguments"

)

4816

i = a.sort().domain().cast(i)

4817

v = a.sort().

range

().cast(v)

4818  return

_to_expr_ref(

Z3_mk_store

(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)

4819

v = a.sort().

range

().cast(args[-1])

4820

idxs = [a.sort().domain_n(i).cast(args[i])

for

i

in range

(len(args)-1)]

4821

_args, sz = _to_ast_array(idxs)

4822  return

_to_expr_ref(

Z3_mk_store_n

(ctx.ref(), a.as_ast(), sz, _args, v.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)

Array update.

Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)

n-ary Array update.

Referenced by Store().

◆ URem() 
Create the Z3 expression (unsigned) remainder `self % other`.

Use the operator % for signed modulus, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> URem(x, y)
URem(x, y)
>>> URem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'

Definition at line 4303 of file z3py.py.

4304  """Create the Z3 expression (unsigned) remainder `self % other`. 4306  Use the operator % for signed modulus, and SRem() for signed remainder. 4308  >>> x = BitVec('x', 32) 4309  >>> y = BitVec('y', 32) 4312  >>> URem(x, y).sort() 4316  >>> URem(x, y).sexpr() 4319

_check_bv_args(a, b)

4320

a, b = _coerce_exprs(a, b)

4321  return

BitVecRef(

Z3_mk_bvurem

(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned remainder.

◆ user_prop_created() def z3py.user_prop_created (   ctx,   cb,   id  )

Definition at line 11623 of file z3py.py.

11624

prop = _prop_closures.get(ctx)

11627

id = _to_expr_ref(

to_Ast

(id), prop.ctx())

def user_prop_created(ctx, cb, id)

◆ user_prop_decide() def z3py.user_prop_decide (   ctx,   cb,   t,   idx,   phase  )

Definition at line 11657 of file z3py.py.

11658

prop = _prop_closures.get(ctx)

11661

t = _to_expr_ref(

to_Ast

(t_ref), prop.ctx())

11662

prop.decide(t, idx, phase)

def user_prop_decide(ctx, cb, t, idx, phase)

◆ user_prop_diseq() def z3py.user_prop_diseq (   ctx,   cb,   x,   y  )

Definition at line 11648 of file z3py.py.

11649

prop = _prop_closures.get(ctx)

11652

x = _to_expr_ref(

to_Ast

(x), prop.ctx())

11653

y = _to_expr_ref(

to_Ast

(y), prop.ctx())

def user_prop_diseq(ctx, cb, x, y)

◆ user_prop_eq() def z3py.user_prop_eq (   ctx,   cb,   x,   y  )

Definition at line 11639 of file z3py.py.

11640

prop = _prop_closures.get(ctx)

11643

x = _to_expr_ref(

to_Ast

(x), prop.ctx())

11644

y = _to_expr_ref(

to_Ast

(y), prop.ctx())

def user_prop_eq(ctx, cb, x, y)

◆ user_prop_final() def z3py.user_prop_final (   ctx,   cb  )

Definition at line 11632 of file z3py.py.

11633

prop = _prop_closures.get(ctx)

def user_prop_final(ctx, cb)

◆ user_prop_fixed() def z3py.user_prop_fixed (   ctx,   cb,   id,   value  )

Definition at line 11614 of file z3py.py.

11615

prop = _prop_closures.get(ctx)

11618

id = _to_expr_ref(

to_Ast

(id), prop.ctx())

11619

value = _to_expr_ref(

to_Ast

(value), prop.ctx())

11620

prop.fixed(id, value)

def user_prop_fixed(ctx, cb, id, value)

◆ user_prop_fresh() def z3py.user_prop_fresh (   ctx,   _new_ctx  )

Definition at line 11600 of file z3py.py.

11601

_prop_closures.set_threaded()

11602

prop = _prop_closures.get(ctx)

11609

new_prop = prop.fresh(nctx)

11610

_prop_closures.set(new_prop.id, new_prop)

void Z3_API Z3_del_context(Z3_context c)

Delete the given logical context.

void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)

Register a Z3 error handler.

def user_prop_fresh(ctx, _new_ctx)

◆ user_prop_pop() def z3py.user_prop_pop (   ctx,   cb,   num_scopes  )

Definition at line 11594 of file z3py.py.

11595

prop = _prop_closures.get(ctx)

11597

prop.pop(num_scopes)

def user_prop_pop(ctx, cb, num_scopes)

◆ user_prop_push() def z3py.user_prop_push (   ctx,   cb  )

Definition at line 11588 of file z3py.py.

11589

prop = _prop_closures.get(ctx)

def user_prop_push(ctx, cb)

◆ Var() 
Create a Z3 free variable. Free variables are used to create quantified formulas.
A free variable with index n is bound when it occurs within the scope of n+1 quantified
declarations.

>>> Var(0, IntSort())
Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort()))
False

Definition at line 1488 of file z3py.py.

1489  """Create a Z3 free variable. Free variables are used to create quantified formulas. 1490  A free variable with index n is bound when it occurs within the scope of n+1 quantified 1493  >>> Var(0, IntSort()) 1495  >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 1499

_z3_assert(

is_sort

(s),

"Z3 sort expected"

)

1500  return

_to_expr_ref(

Z3_mk_bound

(s.ctx_ref(), idx, s.ast), s.ctx)

Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)

Create a variable.

Referenced by RealVar().

◆ When() def z3py.When (   p,   t,   ctx = None  ) 
Return a tactic that applies tactic `t` only if probe `p` evaluates to true.
Otherwise, it returns the input goal unmodified.

>>> t = When(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 8867 of file z3py.py.

8867 def When

(p, t, ctx=None):

8868  """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. 8869  Otherwise, it returns the input goal unmodified. 8871  >>> t = When(Probe('size') > 2, Tactic('simplify')) 8872  >>> x, y = Ints('x y') 8878  >>> g.add(x == y + 1) 8880  [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8882

p = _to_probe(p, ctx)

8883

t = _to_tactic(t, ctx)

8884  return

Tactic(

Z3_tactic_when

(t.ctx.ref(), p.probe, t.tactic), t.ctx)

Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)

Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...

◆ With() def z3py.With (   t, *  args, **  keys  ) 
Return a tactic that applies tactic `t` using the given configuration options.

>>> x, y = Ints('x y')
>>> t = With(Tactic('simplify'), som=True)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]

Definition at line 8524 of file z3py.py.

8524 def With

(t, *args, **keys):

8525  """Return a tactic that applies tactic `t` using the given configuration options. 8527  >>> x, y = Ints('x y') 8528  >>> t = With(Tactic('simplify'), som=True) 8529  >>> t((x + 1)*(y + 2) == 0) 8530  [[2*x + y + x*y == -2]] 8532

ctx = keys.pop(

"ctx"

,

None

)

8533

t = _to_tactic(t, ctx)

Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)

Return a tactic that applies t using the given set of parameters.

def With(t, *args, **keys)

◆ WithParams() def z3py.WithParams (   t,   p  ) 
Return a tactic that applies tactic `t` using the given configuration options.

>>> x, y = Ints('x y')
>>> p = ParamsRef()
>>> p.set("som", True)
>>> t = WithParams(Tactic('simplify'), p)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]

Definition at line 8538 of file z3py.py.

8539  """Return a tactic that applies tactic `t` using the given configuration options. 8541  >>> x, y = Ints('x y') 8543  >>> p.set("som", True) 8544  >>> t = WithParams(Tactic('simplify'), p) 8545  >>> t((x + 1)*(y + 2) == 0) 8546  [[2*x + y + x*y == -2]] 8548

t = _to_tactic(t,

None

)

◆ Xor() def z3py.Xor (   a,   b,   ctx = None  ) 
Create a Z3 Xor expression.

>>> p, q = Bools('p q')
>>> Xor(p, q)
Xor(p, q)
>>> simplify(Xor(p, q))
Not(p == q)

Definition at line 1839 of file z3py.py.

1839 def Xor

(a, b, ctx=None):

1840  """Create a Z3 Xor expression. 1842  >>> p, q = Bools('p q') 1845  >>> simplify(Xor(p, q)) 1848

ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))

1852  return

BoolRef(

Z3_mk_xor

(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)

Create an AST node representing t1 xor t2.

Referenced by BoolRef.__xor__().

◆ z3_debug()

Definition at line 62 of file z3py.py.

Referenced by Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), describe_probes(), deserialize(), Diff(), Distinct(), EnumSort(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpIsPositive(), fpNeg(), FPSort(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), AlgebraicNumRef.index(), Intersect(), is_quantifier(), is_sort(), IsInt(), K(), Loop(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Option(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), QuantifierRef.pattern(), Plus(), PropagateFunction(), prove(), Range(), RatVal(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), simplify(), solve_using(), Star(), substitute(), substitute_funs(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Union(), Update(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().

◆ z3_error_handler() def z3py.z3_error_handler (   c,   e  )

Definition at line 174 of file z3py.py.

def z3_error_handler(c, e)

◆ ZeroExt() def z3py.ZeroExt (   n,   a  ) 
Return a bit-vector expression with `n` extra zero-bits.

>>> x = BitVec('x', 16)
>>> n = ZeroExt(8, x)
>>> n.size()
24
>>> n
ZeroExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(ZeroExt(6, v0))
>>> v
2
>>> v.size()
8

Definition at line 4439 of file z3py.py.

4440  """Return a bit-vector expression with `n` extra zero-bits. 4442  >>> x = BitVec('x', 16) 4443  >>> n = ZeroExt(8, x) 4450  >>> v0 = BitVecVal(2, 2) 4455  >>> v = simplify(ZeroExt(6, v0)) 4462

_z3_assert(_is_int(n),

"First argument must be an integer"

)

4463

_z3_assert(

is_bv

(a),

"Second argument must be a Z3 bit-vector expression"

)

4464  return

BitVecRef(

Z3_mk_zero_ext

(a.ctx_ref(), n, a.as_ast()), a.ctx)

Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)

Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...

◆ sat ◆ unknown ◆ unsat ◆ Z3_DEBUG

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4