z3py Namespace Reference

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

Functions
def	z3_debug ()
def	enable_trace (msg)
def	disable_trace (msg)
def	get_version_string ()
def	get_version ()
def	get_full_version ()
def	open_log (fname)
def	append_log (s)
def	to_symbol
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
def	is_func_decl (a)
def	Function (name, sig)
def	FreshFunction (sig)
def	RecFunction (name, sig)
def	RecAddDefinition (f, args, body)
def	is_expr (a)
def	is_app (a)
def	is_const (a)
def	is_var (a)
def	get_var_index (a)
def	is_app_of (a, k)
def	If
def	Distinct (args)
def	Const (name, sort)
def	Consts (names, sort)
def	FreshConst
def	Var (idx, s)
def	RealVar
def	RealVarVector
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
def	BoolVal
def	Bool
def	Bools
def	BoolVector
def	FreshBool
def	Implies
def	Xor
def	Not
def	mk_not (a)
def	And (args)
def	Or (args)
def	is_pattern (a)
def	MultiPattern (args)
def	is_quantifier (a)
def	ForAll
def	Exists
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
def	RealSort
def	IntVal
def	RealVal
def	RatVal
def	Q
def	Int
def	Ints
def	IntVector
def	FreshInt
def	Real
def	Reals
def	RealVector
def	FreshReal
def	ToReal (a)
def	ToInt (a)
def	IsInt (a)
def	Sqrt
def	Cbrt
def	is_bv_sort (s)
def	is_bv (a)
def	is_bv_value (a)
def	BV2Int
def	Int2BV (a, num_bits)
def	BitVecSort
def	BitVecVal
def	BitVec
def	BitVecs
def	Concat (args)
def	Extract (high, low, a)
def	ULE (a, b)
def	ULT (a, b)
def	UGE (a, b)
def	UGT (a, b)
def	UDiv (a, b)
def	URem (a, b)
def	SRem (a, b)
def	LShR (a, b)
def	RotateLeft (a, b)
def	RotateRight (a, b)
def	SignExt (n, a)
def	ZeroExt (n, a)
def	RepeatBitVec (n, a)
def	BVRedAnd (a)
def	BVRedOr (a)
def	BVAddNoOverflow (a, b, signed)
def	BVAddNoUnderflow (a, b)
def	BVSubNoOverflow (a, b)
def	BVSubNoUnderflow (a, b, signed)
def	BVSDivNoOverflow (a, b)
def	BVSNegNoOverflow (a)
def	BVMulNoOverflow (a, b, signed)
def	BVMulNoUnderflow (a, b)
def	is_array_sort (a)
def	is_array (a)
def	is_const_array (a)
def	is_K (a)
def	is_map (a)
def	is_default (a)
def	get_map_func (a)
def	ArraySort (sig)
def	Array (name, dom, rng)
def	Update (a, i, v)
def	Default (a)
def	Store (a, i, v)
def	Select (a, i)
def	Map (f, args)
def	K (dom, v)
def	Ext (a, b)
def	SetHasSize (a, k)
def	is_select (a)
def	is_store (a)
def	SetSort (s)
	Sets. More...
def	EmptySet (s)
def	FullSet (s)
def	SetUnion (args)
def	SetIntersect (args)
def	SetAdd (s, e)
def	SetDel (s, e)
def	SetComplement (s)
def	SetDifference (a, b)
def	IsMember (e, s)
def	IsSubset (a, b)
def	CreateDatatypes (ds)
def	TupleSort
def	DisjointSum
def	EnumSort
def	args2params
def	Model
def	is_as_array (n)
def	get_as_array_func (n)
def	SolverFor
def	SimpleSolver
def	FiniteDomainSort
def	is_finite_domain_sort (s)
def	is_finite_domain (a)
def	FiniteDomainVal
def	is_finite_domain_value (a)
def	AndThen (ts, ks)
def	Then (ts, ks)
def	OrElse (ts, ks)
def	ParOr (ts, ks)
def	ParThen
def	ParAndThen
def	With (t, args, keys)
def	WithParams (t, p)
def	Repeat
def	TryFor
def	tactics
def	tactic_description
def	describe_tactics ()
def	is_probe (p)
def	probes
def	probe_description
def	describe_probes ()
def	FailIf
def	When
def	Cond
def	simplify (a, arguments, keywords)
	Utils. More...
def	help_simplify ()
def	simplify_param_descrs ()
def	substitute (t, m)
def	substitute_vars (t, m)
def	Sum (args)
def	Product (args)
def	AtMost (args)
def	AtLeast (args)
def	PbLe (args, k)
def	PbGe (args, k)
def	PbEq
def	solve (args, keywords)
def	solve_using (s, args, keywords)
def	prove (claim, show=False, keywords)
def	parse_smt2_string
def	parse_smt2_file
def	get_default_rounding_mode
def	set_default_rounding_mode
def	get_default_fp_sort
def	set_default_fp_sort
def	Float16
def	FloatHalf
def	Float32
def	FloatSingle
def	Float64
def	FloatDouble
def	Float128
def	FloatQuadruple
def	is_fp_sort (s)
def	is_fprm_sort (s)
def	RoundNearestTiesToEven
def	RNE
def	RoundNearestTiesToAway
def	RNA
def	RoundTowardPositive
def	RTP
def	RoundTowardNegative
def	RTN
def	RoundTowardZero
def	RTZ
def	is_fprm (a)
def	is_fprm_value (a)
def	is_fp (a)
def	is_fp_value (a)
def	FPSort
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
def	FP
def	FPs
def	fpAbs
def	fpNeg
def	fpAdd
def	fpSub
def	fpMul
def	fpDiv
def	fpRem
def	fpMin
def	fpMax
def	fpFMA
def	fpSqrt
def	fpRoundToIntegral
def	fpIsNaN
def	fpIsInf
def	fpIsZero
def	fpIsNormal
def	fpIsSubnormal
def	fpIsNegative
def	fpIsPositive
def	fpLT
def	fpLEQ
def	fpGT
def	fpGEQ
def	fpEQ
def	fpNEQ
def	fpFP
def	fpToFP
def	fpBVToFP
def	fpFPToFP
def	fpRealToFP
def	fpSignedToFP
def	fpUnsignedToFP
def	fpToFPUnsigned
def	fpToSBV
def	fpToUBV
def	fpToReal
def	fpToIEEEBV
def	StringSort
def	CharSort
def	SeqSort (s)
def	is_seq (a)
def	is_string (a)
def	is_string_value (a)
def	StringVal
def	String
def	Strings
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
def	LastIndexOf (s, substr)
def	Length (s)
def	StrToInt (s)
def	IntToStr (s)
def	Re
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
def	Range
def	AllChar
def	PartialOrder (a, index)
def	LinearOrder (a, index)
def	TreeOrder (a, index)
def	PiecewiseLinearOrder (a, index)
def	TransitiveClosure (f)
def	ensure_prop_closures ()
def	user_prop_push (ctx)
def	user_prop_pop (ctx, num_scopes)
def	user_prop_fresh (id, ctx)
def	user_prop_fixed (ctx, cb, id, value)
def	user_prop_final (ctx, cb)
def	user_prop_eq (ctx, cb, x, y)
def	user_prop_diseq (ctx, cb, x, y)

Variables
	Z3_DEBUG = __debug__
	_main_ctx = None
tuple	sat = CheckSatResult(Z3_L_TRUE)
tuple	unsat = CheckSatResult(Z3_L_FALSE)
tuple	unknown = CheckSatResult(Z3_L_UNDEF)
dictionary	_on_models = {}
tuple	_on_model_eh = on_model_eh_type(_global_on_model)
	_dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
	Floating-Point Arithmetic. More...
int	_dflt_fpsort_ebits = 11
int	_dflt_fpsort_sbits = 53
tuple	_ROUNDING_MODES
	_prop_closures = None
tuple	_user_prop_push = push_eh_type(user_prop_push)
tuple	_user_prop_pop = pop_eh_type(user_prop_pop)
tuple	_user_prop_fresh = fresh_eh_type(user_prop_fresh)
tuple	_user_prop_fixed = fixed_eh_type(user_prop_fixed)
tuple	_user_prop_final = final_eh_type(user_prop_final)
tuple	_user_prop_eq = eq_eh_type(user_prop_eq)
tuple	_user_prop_diseq = eq_eh_type(user_prop_diseq)

Function Documentation

def z3py.AllChar	(		regex_sort,
			ctx = None
	)

Create a regular expression that accepts all single character strings

Definition at line 11068 of file z3py.py.

def AllChar(regex_sort, ctx=None):
    """Create a regular expression that accepts all single character strings
    """
    return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)

# Special Relations

def z3py.And

(

args

)

Create a Z3 and-expression or and-probe.

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

Definition at line 1815 of file z3py.py.

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

def And(*args):
    """Create a Z3 and-expression or and-probe.

    >>> p, q, r = Bools('p q r')
    >>> And(p, q, r)
    And(p, q, r)
    >>> P = BoolVector('p', 5)
    >>> And(P)
    And(p__0, p__1, p__2, p__3, p__4)
    """
    last_arg = None
    if len(args) > 0:
        last_arg = args[len(args) - 1]
    if isinstance(last_arg, Context):
        ctx = args[len(args) - 1]
        args = args[:len(args) - 1]
    elif len(args) == 1 and isinstance(args[0], AstVector):
        ctx = args[0].ctx
        args = [a for a in args[0]]
    else:
        ctx = None
    args = _get_args(args)
    ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
    if z3_debug():
        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
    if _has_probe(args):
        return _probe_and(args, ctx)
    else:
        args = _coerce_expr_list(args, ctx)
        _args, sz = _to_ast_array(args)
        return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)

def z3py.AndThen	(		ts,
			ks
	)

Return a tactic that applies the tactics in `*ts` in sequence.

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

Definition at line 8182 of file z3py.py.

Referenced by Then().

def 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)
    """
    if z3_debug():
        _z3_assert(len(ts) >= 2, "At least two arguments expected")
    ctx = ks.get("ctx", None)
    num = len(ts)
    r = ts[0]
    for i in range(num - 1):
        r = _and_then(r, ts[i + 1], ctx)
    return r

def z3py.append_log

(

s

)

Append user-defined string to interaction log. 

Definition at line 124 of file z3py.py.

def append_log(s):
    """Append user-defined string to interaction log. """
    Z3_append_log(s)

def z3py.args2params	(		arguments,
			keywords,
			ctx = None
	)

Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'

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

Definition at line 5398 of file z3py.py.

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

def 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)
    """
    if z3_debug():
        _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
    prev = None
    r = ParamsRef(ctx)
    for a in arguments:
        if prev is None:
            prev = a
        else:
            r.set(prev, a)
            prev = None
    for k in keywords:
        v = keywords[k]
        r.set(k, v)
    return r

def z3py.Array	(		name,
			dom,
			rng
	)

Return an array constant named `name` with the given domain and range sorts.

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

Definition at line 4680 of file z3py.py.

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

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

    >>> a = Array('a', IntSort(), IntSort())
    >>> a.sort()
    Array(Int, Int)
    >>> a[0]
    a[0]
    """
    s = ArraySort(dom, rng)
    ctx = s.ctx
    return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)

def z3py.ArraySort

(

sig

)

Return the Z3 array sort with the given domain and range sorts.

>>> A = ArraySort(IntSort(), BoolSort())
>>> A
Array(Int, Bool)
>>> A.domain()
Int
>>> A.range()
Bool
>>> AA = ArraySort(IntSort(), A)
>>> AA
Array(Int, Array(Int, Bool))

Definition at line 4647 of file z3py.py.

Referenced by Array(), ArraySortRef.domain(), and ArraySortRef.range().

def 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))
    """
    sig = _get_args(sig)
    if z3_debug():
        _z3_assert(len(sig) > 1, "At least two arguments expected")
    arity = len(sig) - 1
    r = sig[arity]
    d = sig[0]
    if z3_debug():
        for s in sig:
            _z3_assert(is_sort(s), "Z3 sort expected")
            _z3_assert(s.ctx == r.ctx, "Context mismatch")
    ctx = d.ctx
    if len(sig) == 2:
        return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
    dom = (Sort * arity)()
    for i in range(arity):
        dom[i] = sig[i].ast
    return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)

def z3py.AtLeast

(

args

)

Create an at-most Pseudo-Boolean k constraint.

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

Definition at line 8811 of file z3py.py.

def AtLeast(*args):
    """Create an at-most Pseudo-Boolean k constraint.

    >>> a, b, c = Bools('a b c')
    >>> f = AtLeast(a, b, c, 2)
    """
    args = _get_args(args)
    if z3_debug():
        _z3_assert(len(args) > 1, "Non empty list of arguments expected")
    ctx = _ctx_from_ast_arg_list(args)
    if z3_debug():
        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
    args1 = _coerce_expr_list(args[:-1], ctx)
    k = args[-1]
    _args, sz = _to_ast_array(args1)
    return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)

def z3py.AtMost

(

args

)

Create an at-most Pseudo-Boolean k constraint.

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

Definition at line 8793 of file z3py.py.

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

    >>> a, b, c = Bools('a b c')
    >>> f = AtMost(a, b, c, 2)
    """
    args = _get_args(args)
    if z3_debug():
        _z3_assert(len(args) > 1, "Non empty list of arguments expected")
    ctx = _ctx_from_ast_arg_list(args)
    if z3_debug():
        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
    args1 = _coerce_expr_list(args[:-1], ctx)
    k = args[-1]
    _args, sz = _to_ast_array(args1)
    return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)

def z3py.BitVec	(		name,
			bv,
			ctx = None
	)

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

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

Definition at line 4001 of file z3py.py.

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

def 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
    """
    if isinstance(bv, BitVecSortRef):
        ctx = bv.ctx
    else:
        ctx = _get_ctx(ctx)
        bv = BitVecSort(bv, ctx)
    return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)

def z3py.BitVecs	(		names,
			bv,
			ctx = None
	)

Return a tuple of bit-vector constants of size bv.

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

Definition at line 4025 of file z3py.py.

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

def 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
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [BitVec(name, bv, ctx) for name in names]

def z3py.BitVecSort	(		sz,
			ctx = None
	)

Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.

>>> Byte = BitVecSort(8)
>>> Word = BitVecSort(16)
>>> Byte
BitVec(8)
>>> x = Const('x', Byte)
>>> eq(x, BitVec('x', 8))
True

Definition at line 3969 of file z3py.py.

Referenced by BitVec(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), BitVecSortRef.size(), and BitVecRef.sort().

def 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
    """
    ctx = _get_ctx(ctx)
    return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)

def z3py.BitVecVal	(		val,
			bv,
			ctx = None
	)

Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.

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

Definition at line 3984 of file z3py.py.

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

def 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
    """
    if is_bv_sort(bv):
        ctx = bv.ctx
        return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
    else:
        ctx = _get_ctx(ctx)
        return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)

def z3py.Bool	(		name,
			ctx = None
	)

Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.

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

Definition at line 1694 of file z3py.py.

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

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

    >>> p = Bool('p')
    >>> q = Bool('q')
    >>> And(p, q)
    And(p, q)
    """
    ctx = _get_ctx(ctx)
    return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)

def z3py.Bools	(		names,
			ctx = None
	)

Return a tuple of Boolean constants.

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

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

Definition at line 1706 of file z3py.py.

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

def 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))
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [Bool(name, ctx) for name in names]

def z3py.BoolSort

(

ctx = None

)

Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.

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

Definition at line 1657 of file z3py.py.

Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), ArraySortRef.domain(), ArrayRef.domain(), If(), IntSort(), is_arith_sort(), ArraySortRef.range(), ArrayRef.range(), and ArrayRef.sort().

def 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
    """
    ctx = _get_ctx(ctx)
    return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)

def z3py.BoolVal	(		val,
			ctx = None
	)

Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.

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

Definition at line 1675 of file z3py.py.

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

def 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
    """
    ctx = _get_ctx(ctx)
    if val:
        return BoolRef(Z3_mk_true(ctx.ref()), ctx)
    else:
        return BoolRef(Z3_mk_false(ctx.ref()), ctx)

def z3py.BoolVector	(		prefix,
			sz,
			ctx = None
	)

Return a list of Boolean constants of size `sz`.

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

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

Definition at line 1722 of file z3py.py.

Referenced by And(), and Or().

def 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)
    """
    return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]

def z3py.BV2Int	(		a,
			is_signed = False
	)

Return the Z3 expression BV2Int(a).

>>> b = BitVec('b', 3)
>>> BV2Int(b).sort()
Int
>>> x = Int('x')
>>> x > BV2Int(b)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=False)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=True)
x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
>>> solve(x > BV2Int(b), b == 1, x < 3)
[x = 2, b = 1]

Definition at line 3937 of file z3py.py.

def 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]
    """
    if z3_debug():
        _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
    ctx = a.ctx
    # investigate problem with bv2int
    return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)

def z3py.BVAddNoOverflow	(		a,
			b,
			signed
	)

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

Definition at line 4423 of file z3py.py.

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

def z3py.BVAddNoUnderflow	(		a,
			b
	)

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

Definition at line 4430 of file z3py.py.

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

def z3py.BVMulNoOverflow	(		a,
			b,
			signed
	)

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

Definition at line 4465 of file z3py.py.

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

def z3py.BVMulNoUnderflow	(		a,
			b
	)

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

Definition at line 4472 of file z3py.py.

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

def z3py.BVRedAnd

(

a

)

Return the reduction-and expression of `a`.

Definition at line 4409 of file z3py.py.

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

def z3py.BVRedOr

(

a

)

Return the reduction-or expression of `a`.

Definition at line 4416 of file z3py.py.

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

def z3py.BVSDivNoOverflow	(		a,
			b
	)

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

Definition at line 4451 of file z3py.py.

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

def z3py.BVSNegNoOverflow

(

a

)

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

Definition at line 4458 of file z3py.py.

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

def z3py.BVSubNoOverflow	(		a,
			b
	)

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

Definition at line 4437 of file z3py.py.

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

def z3py.BVSubNoUnderflow	(		a,
			b,
			signed
	)

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

Definition at line 4444 of file z3py.py.

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

def z3py.Cbrt	(		a,
			ctx = None
	)

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

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

Definition at line 3388 of file z3py.py.

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

    >>> x = Real('x')
    >>> Cbrt(x)
    x**(1/3)
    """
    if not is_expr(a):
        ctx = _get_ctx(ctx)
        a = RealVal(a, ctx)
    return a ** "1/3"

def z3py.CharSort

(

ctx = None

)

Create a character sort
>>> ch = CharSort()
>>> print(ch)
Char

Definition at line 10593 of file z3py.py.

def CharSort(ctx=None):
    """Create a character sort
    >>> ch = CharSort()
    >>> print(ch)
    Char
    """
    ctx = _get_ctx(ctx)
    return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)

def z3py.Complement

(

re

)

Create the complement regular expression.

Definition at line 11025 of file z3py.py.

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

def z3py.Concat

(

args

)

Create a Z3 bit-vector concatenation expression.

>>> v = BitVecVal(1, 4)
>>> Concat(v, v+1, v)
Concat(Concat(1, 1 + 1), 1)
>>> simplify(Concat(v, v+1, v))
289
>>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
121

Definition at line 4046 of file z3py.py.

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

def 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
    """
    args = _get_args(args)
    sz = len(args)
    if z3_debug():
        _z3_assert(sz >= 2, "At least two arguments expected.")

    ctx = None
    for a in args:
        if is_expr(a):
            ctx = a.ctx
            break
    if is_seq(args[0]) or isinstance(args[0], str):
        args = [_coerce_seq(s, ctx) for s in args]
        if z3_debug():
            _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
        v = (Ast * sz)()
        for i in range(sz):
            v[i] = args[i].as_ast()
        return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)

    if is_re(args[0]):
        if z3_debug():
            _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
        v = (Ast * sz)()
        for i in range(sz):
            v[i] = args[i].as_ast()
        return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)

    if z3_debug():
        _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
    r = args[0]
    for i in range(sz - 1):
        r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
    return r

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

Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.

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

Definition at line 8639 of file z3py.py.

Referenced by If().

def 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'))
    """
    p = _to_probe(p, ctx)
    t1 = _to_tactic(t1, ctx)
    t2 = _to_tactic(t2, ctx)
    return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)

def z3py.Const	(		name,
			sort
	)

Create a constant of the given sort.

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

Definition at line 1407 of file z3py.py.

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

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

    >>> Const('x', IntSort())
    x
    """
    if z3_debug():
        _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
    ctx = sort.ctx
    return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)

def z3py.Consts	(		names,
			sort
	)

Create several constants of the given sort.

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

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

Definition at line 1419 of file z3py.py.

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

def 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
    """
    if isinstance(names, str):
        names = names.split(" ")
    return [Const(name, sort) for name in names]

def z3py.Contains	(		a,
			b
	)

Check if 'a' contains 'b'
>>> s1 = Contains("abc", "ab")
>>> simplify(s1)
True
>>> s2 = Contains("abc", "bc")
>>> simplify(s2)
True
>>> x, y, z = Strings('x y z')
>>> s3 = Contains(Concat(x,y,z), y)
>>> simplify(s3)
True

Definition at line 10812 of file z3py.py.

def 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
    """
    ctx = _get_ctx2(a, b)
    a = _coerce_seq(a, ctx)
    b = _coerce_seq(b, ctx)
    return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.CreateDatatypes

(

ds

)

Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.

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

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

Definition at line 5094 of file z3py.py.

Referenced by Datatype.create().

def 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
    """
    ds = _get_args(ds)
    if z3_debug():
        _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
        _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
        _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
        _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
    ctx = ds[0].ctx
    num = len(ds)
    names = (Symbol * num)()
    out = (Sort * num)()
    clists = (ConstructorList * num)()
    to_delete = []
    for i in range(num):
        d = ds[i]
        names[i] = to_symbol(d.name, ctx)
        num_cs = len(d.constructors)
        cs = (Constructor * num_cs)()
        for j in range(num_cs):
            c = d.constructors[j]
            cname = to_symbol(c[0], ctx)
            rname = to_symbol(c[1], ctx)
            fs = c[2]
            num_fs = len(fs)
            fnames = (Symbol * num_fs)()
            sorts = (Sort * num_fs)()
            refs = (ctypes.c_uint * num_fs)()
            for k in range(num_fs):
                fname = fs[k][0]
                ftype = fs[k][1]
                fnames[k] = to_symbol(fname, ctx)
                if isinstance(ftype, Datatype):
                    if z3_debug():
                        _z3_assert(
                            ds.count(ftype) == 1,
                            "One and only one occurrence of each datatype is expected",
                        )
                    sorts[k] = None
                    refs[k] = ds.index(ftype)
                else:
                    if z3_debug():
                        _z3_assert(is_sort(ftype), "Z3 sort expected")
                    sorts[k] = ftype.ast
                    refs[k] = 0
            cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
            to_delete.append(ScopedConstructor(cs[j], ctx))
        clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
        to_delete.append(ScopedConstructorList(clists[i], ctx))
    Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
    result = []
    # Create a field for every constructor, recognizer and accessor
    for i in range(num):
        dref = DatatypeSortRef(out[i], ctx)
        num_cs = dref.num_constructors()
        for j in range(num_cs):
            cref = dref.constructor(j)
            cref_name = cref.name()
            cref_arity = cref.arity()
            if cref.arity() == 0:
                cref = cref()
            setattr(dref, cref_name, cref)
            rref = dref.recognizer(j)
            setattr(dref, "is_" + cref_name, rref)
            for k in range(cref_arity):
                aref = dref.accessor(j, k)
                setattr(dref, aref.name(), aref)
        result.append(dref)
    return tuple(result)

def z3py.DeclareSort	(		name,
			ctx = None
	)

Create a new uninterpreted sort named `name`.

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

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

Definition at line 692 of file z3py.py.

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

def 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
    """
    ctx = _get_ctx(ctx)
    return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)

def z3py.Default

(

a

)

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

Definition at line 4716 of file z3py.py.

Referenced by is_default().

def Default(a):
    """ Return a default value for array expression.
    >>> b = K(IntSort(), 1)
    >>> prove(Default(b) == 1)
    proved
    """
    if z3_debug():
        _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
    return a.default()

def z3py.describe_probes

(

)

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

Definition at line 8560 of file z3py.py.

def describe_probes():
    """Display a (tabular) description of all available probes in Z3."""
    if in_html_mode():
        even = True
        print('<table border="1" cellpadding="2" cellspacing="0">')
        for p in probes():
            if even:
                print('<tr style="background-color:#CFCFCF">')
                even = False
            else:
                print("<tr>")
                even = True
            print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
        print("</table>")
    else:
        for p in probes():
            print("%s : %s" % (p, probe_description(p)))

def z3py.describe_tactics

(

)

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

Definition at line 8354 of file z3py.py.

def describe_tactics():
    """Display a (tabular) description of all available tactics in Z3."""
    if in_html_mode():
        even = True
        print('<table border="1" cellpadding="2" cellspacing="0">')
        for t in tactics():
            if even:
                print('<tr style="background-color:#CFCFCF">')
                even = False
            else:
                print("<tr>")
                even = True
            print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
        print("</table>")
    else:
        for t in tactics():
            print("%s : %s" % (t, tactic_description(t)))

def z3py.disable_trace

(

msg

)

Definition at line 81 of file z3py.py.

def disable_trace(msg):
    Z3_disable_trace(msg)

def z3py.DisjointSum	(		name,
			sorts,
			ctx = None
	)

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

Definition at line 5307 of file z3py.py.

def 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()])
    """
    sum = Datatype(name, ctx)
    for i in range(len(sorts)):
        sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
    sum = sum.create()
    return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]

def z3py.Distinct

(

args

)

Create a Z3 distinct expression.

>>> x = Int('x')
>>> y = Int('y')
>>> Distinct(x, y)
x != y
>>> z = Int('z')
>>> Distinct(x, y, z)
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z))
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z), blast_distinct=True)
And(Not(x == y), Not(x == z), Not(y == z))

Definition at line 1374 of file z3py.py.

def 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))
    """
    args = _get_args(args)
    ctx = _ctx_from_ast_arg_list(args)
    if z3_debug():
        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
    args = _coerce_expr_list(args, ctx)
    _args, sz = _to_ast_array(args)
    return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)

def z3py.Empty

(

s

)

Create the empty sequence of the given sort
>>> e = Empty(StringSort())
>>> e2 = StringVal("")
>>> print(e.eq(e2))
True
>>> e3 = Empty(SeqSort(IntSort()))
>>> print(e3)
Empty(Seq(Int))
>>> e4 = Empty(ReSort(SeqSort(IntSort())))
>>> print(e4)
Empty(ReSort(Seq(Int)))

Definition at line 10743 of file z3py.py.

def Empty(s):
    """Create the empty sequence of the given sort
    >>> e = Empty(StringSort())
    >>> e2 = StringVal("")
    >>> print(e.eq(e2))
    True
    >>> e3 = Empty(SeqSort(IntSort()))
    >>> print(e3)
    Empty(Seq(Int))
    >>> e4 = Empty(ReSort(SeqSort(IntSort())))
    >>> print(e4)
    Empty(ReSort(Seq(Int)))
    """
    if isinstance(s, SeqSortRef):
        return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
    if isinstance(s, ReSortRef):
        return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
    raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")

def z3py.EmptySet

(

s

)

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

Definition at line 4858 of file z3py.py.

def EmptySet(s):
    """Create the empty set
    >>> EmptySet(IntSort())
    K(Int, False)
    """
    ctx = s.ctx
    return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)

def z3py.enable_trace

(

msg

)

Definition at line 77 of file z3py.py.

def enable_trace(msg):
    Z3_enable_trace(msg)

def z3py.ensure_prop_closures

(

)

Definition at line 11139 of file z3py.py.

def ensure_prop_closures():
    global _prop_closures
    if _prop_closures is None:
        _prop_closures = PropClosures()

def z3py.EnumSort	(		name,
			values,
			ctx = None
	)

Return a new enumeration sort named `name` containing the given values.

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

Definition at line 5319 of file z3py.py.

def 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'])
    """
    if z3_debug():
        _z3_assert(isinstance(name, str), "Name must be a string")
        _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
        _z3_assert(len(values) > 0, "At least one value expected")
    ctx = _get_ctx(ctx)
    num = len(values)
    _val_names = (Symbol * num)()
    for i in range(num):
        _val_names[i] = to_symbol(values[i])
    _values = (FuncDecl * num)()
    _testers = (FuncDecl * num)()
    name = to_symbol(name)
    S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
    V = []
    for i in range(num):
        V.append(FuncDeclRef(_values[i], ctx))
    V = [a() for a in V]
    return S, V

def z3py.eq	(		a,
			b
	)

Return `True` if `a` and `b` are structurally identical AST nodes.

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

Definition at line 471 of file z3py.py.

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

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

    >>> x = Int('x')
    >>> y = Int('y')
    >>> eq(x, y)
    False
    >>> eq(x + 1, x + 1)
    True
    >>> eq(x + 1, 1 + x)
    False
    >>> eq(simplify(x + 1), simplify(1 + x))
    True
    """
    if z3_debug():
        _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
    return a.eq(b)

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

Create a Z3 exists formula.

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


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

Definition at line 2207 of file z3py.py.

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

def 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
    """
    return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)

def z3py.Ext	(		a,
			b
	)

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

Definition at line 4804 of file z3py.py.

def Ext(a, b):
    """Return extensionality index for one-dimensional arrays.
    >> a, b = Consts('a b', SetSort(IntSort()))
    >> Ext(a, b)
    Ext(a, b)
    """
    ctx = a.ctx
    if z3_debug():
        _z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays")
    return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.Extract	(		high,
			low,
			a
	)

Create a Z3 bit-vector extraction expression.
Extract is overloaded to also work on sequence extraction.
The functions SubString and SubSeq are redirected to Extract.
For this case, the arguments are reinterpreted as:
    high - is a sequence (string)
    low  - is an offset
    a    - is the length to be extracted

>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)
>>> simplify(Extract(StringVal("abcd"),2,1))
"c"

Definition at line 4092 of file z3py.py.

def 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"
    """
    if isinstance(high, str):
        high = StringVal(high)
    if is_seq(high):
        s = high
        offset, length = _coerce_exprs(low, a, s.ctx)
        return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
    if z3_debug():
        _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
        _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0,
                   "First and second arguments must be non negative integers")
        _z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
    return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)

def z3py.FailIf	(		p,
			ctx = None
	)

Return a tactic that fails if the probe `p` evaluates to true.
Otherwise, it returns the input goal unmodified.

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

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

Definition at line 8597 of file z3py.py.

def 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]]
    """
    p = _to_probe(p, ctx)
    return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)

def z3py.FiniteDomainSort	(		name,
			sz,
			ctx = None
	)

Create a named finite domain sort of a given size sz

Definition at line 7601 of file z3py.py.

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

def z3py.FiniteDomainVal	(		val,
			sort,
			ctx = None
	)

Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.

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

Definition at line 7671 of file z3py.py.

def 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
    """
    if z3_debug():
        _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
    ctx = sort.ctx
    return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)

def z3py.Float128

(

ctx = None

)

Floating-point 128-bit (quadruple) sort.

Definition at line 9277 of file z3py.py.

def Float128(ctx=None):
    """Floating-point 128-bit (quadruple) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)

def z3py.Float16

(

ctx = None

)

Floating-point 16-bit (half) sort.

Definition at line 9241 of file z3py.py.

def Float16(ctx=None):
    """Floating-point 16-bit (half) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)

def z3py.Float32

(

ctx = None

)

Floating-point 32-bit (single) sort.

Definition at line 9253 of file z3py.py.

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

def Float32(ctx=None):
    """Floating-point 32-bit (single) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)

def z3py.Float64

(

ctx = None

)

Floating-point 64-bit (double) sort.

Definition at line 9265 of file z3py.py.

Referenced by fpFPToFP(), and fpToFP().

def Float64(ctx=None):
    """Floating-point 64-bit (double) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)

def z3py.FloatDouble

(

ctx = None

)

Floating-point 64-bit (double) sort.

Definition at line 9271 of file z3py.py.

def FloatDouble(ctx=None):
    """Floating-point 64-bit (double) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)

def z3py.FloatHalf

(

ctx = None

)

Floating-point 16-bit (half) sort.

Definition at line 9247 of file z3py.py.

def FloatHalf(ctx=None):
    """Floating-point 16-bit (half) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)

def z3py.FloatQuadruple

(

ctx = None

)

Floating-point 128-bit (quadruple) sort.

Definition at line 9283 of file z3py.py.

def FloatQuadruple(ctx=None):
    """Floating-point 128-bit (quadruple) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)

def z3py.FloatSingle

(

ctx = None

)

Floating-point 32-bit (single) sort.

Definition at line 9259 of file z3py.py.

def FloatSingle(ctx=None):
    """Floating-point 32-bit (single) sort."""
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)

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

Create a Z3 forall formula.

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

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

Definition at line 2189 of file z3py.py.

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

def 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)
    """
    return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)

def z3py.FP	(		name,
			fpsort,
			ctx = None
	)

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

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

Definition at line 9909 of file z3py.py.

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

def 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
    """
    if isinstance(fpsort, FPSortRef) and ctx is None:
        ctx = fpsort.ctx
    else:
        ctx = _get_ctx(ctx)
    return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)

def z3py.fpAbs	(		a,
			ctx = None
	)

Create a Z3 floating-point absolute value expression.

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

Definition at line 9952 of file z3py.py.

def 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)
    """
    ctx = _get_ctx(ctx)
    [a] = _coerce_fp_expr_list([a], ctx)
    return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)

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

Create a Z3 floating-point addition expression.

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

Definition at line 10043 of file z3py.py.

Referenced by FPs().

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

    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpAdd(rm, x, y)
    fpAdd(RNE(), x, y)
    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
    x + y
    >>> fpAdd(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)

def z3py.fpBVToFP	(		v,
			sort,
			ctx = None
	)

Create a Z3 floating-point conversion expression that represents the
conversion from a bit-vector term to a floating-point term.

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

Definition at line 10365 of file z3py.py.

def 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
    """
    _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
    _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
    ctx = _get_ctx(ctx)
    return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)

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

Create a Z3 floating-point division expression.

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

Definition at line 10090 of file z3py.py.

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

    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpDiv(rm, x, y)
    fpDiv(RNE(), x, y)
    >>> fpDiv(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)

def z3py.fpEQ	(		a,
			b,
			ctx = None
	)

Create the Z3 floating-point expression `fpEQ(other, self)`.

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

Definition at line 10273 of file z3py.py.

Referenced by fpFP(), and fpNEQ().

def 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)'
    """
    return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)

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

Create a Z3 floating-point fused multiply-add expression.

Definition at line 10149 of file z3py.py.

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

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

Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.

>>> s = FPSort(8, 24)
>>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
>>> print(x)
fpFP(1, 127, 4194304)
>>> xv = FPVal(-1.5, s)
>>> print(xv)
-1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
sat
>>> xv = FPVal(+1.5, s)
>>> print(xv)
1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
unsat

Definition at line 10297 of file z3py.py.

def 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
    """
    _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
    _z3_assert(sgn.sort().size() == 1, "sort mismatch")
    ctx = _get_ctx(ctx)
    _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
    return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)

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

Create a Z3 floating-point conversion expression that represents the
conversion from a floating-point term to a floating-point term of different precision.

>>> x_sgl = FPVal(1.0, Float32())
>>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
>>> x_dbl
fpToFP(RNE(), 1)
>>> simplify(x_dbl)
1
>>> x_dbl.sort()
FPSort(11, 53)

Definition at line 10382 of file z3py.py.

def 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)
    """
    _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
    _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
    _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
    ctx = _get_ctx(ctx)
    return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)

def z3py.fpGEQ	(		a,
			b,
			ctx = None
	)

Create the Z3 floating-point expression `other >= self`.

>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGEQ(x, y)
x >= y
>>> (x >= y).sexpr()
'(fp.geq x y)'

Definition at line 10261 of file z3py.py.

def 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)'
    """
    return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)

def z3py.fpGT	(		a,
			b,
			ctx = None
	)

Create the Z3 floating-point expression `other > self`.

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

Definition at line 10249 of file z3py.py.

def 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)'
    """
    return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)

def z3py.fpInfinity	(		s,
			negative
	)

Create a Z3 floating-point +oo or -oo term.

Definition at line 9837 of file z3py.py.

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

def z3py.fpIsInf	(		a,
			ctx = None
	)

Create a Z3 floating-point isInfinite expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> fpIsInf(x)
fpIsInf(x)

Definition at line 10179 of file z3py.py.

def fpIsInf(a, ctx=None):
    """Create a Z3 floating-point isInfinite expression.

    >>> s = FPSort(8, 24)
    >>> x = FP('x', s)
    >>> fpIsInf(x)
    fpIsInf(x)
    """
    return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)

def z3py.fpIsNaN	(		a,
			ctx = None
	)

Create a Z3 floating-point isNaN expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpIsNaN(x)
fpIsNaN(x)

Definition at line 10167 of file z3py.py.

def 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)
    """
    return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)

def z3py.fpIsNegative	(		a,
			ctx = None
	)

Create a Z3 floating-point isNegative expression.

Definition at line 10208 of file z3py.py.

def fpIsNegative(a, ctx=None):
    """Create a Z3 floating-point isNegative expression.
    """
    return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)

def z3py.fpIsNormal	(		a,
			ctx = None
	)

Create a Z3 floating-point isNormal expression.

Definition at line 10196 of file z3py.py.

def fpIsNormal(a, ctx=None):
    """Create a Z3 floating-point isNormal expression.
    """
    return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)

def z3py.fpIsPositive	(		a,
			ctx = None
	)

Create a Z3 floating-point isPositive expression.

Definition at line 10214 of file z3py.py.

def fpIsPositive(a, ctx=None):
    """Create a Z3 floating-point isPositive expression.
    """
    return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)

def z3py.fpIsSubnormal	(		a,
			ctx = None
	)

Create a Z3 floating-point isSubnormal expression.

Definition at line 10202 of file z3py.py.

def fpIsSubnormal(a, ctx=None):
    """Create a Z3 floating-point isSubnormal expression.
    """
    return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)

def z3py.fpIsZero	(		a,
			ctx = None
	)

Create a Z3 floating-point isZero expression.

Definition at line 10190 of file z3py.py.

def fpIsZero(a, ctx=None):
    """Create a Z3 floating-point isZero expression.
    """
    return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)

def z3py.fpLEQ	(		a,
			b,
			ctx = None
	)

Create the Z3 floating-point expression `other <= self`.

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

Definition at line 10237 of file z3py.py.

def 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)'
    """
    return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)

def z3py.fpLT	(		a,
			b,
			ctx = None
	)

Create the Z3 floating-point expression `other < self`.

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

Definition at line 10225 of file z3py.py.

def 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)'
    """
    return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)

def z3py.fpMax	(		a,
			b,
			ctx = None
	)

Create a Z3 floating-point maximum expression.

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

Definition at line 10134 of file z3py.py.

def 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)
    """
    return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)

def z3py.fpMin	(		a,
			b,
			ctx = None
	)

Create a Z3 floating-point minimum expression.

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

Definition at line 10119 of file z3py.py.

def 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)
    """
    return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)

def z3py.fpMinusInfinity

(

s

)

Create a Z3 floating-point -oo term.

Definition at line 9831 of file z3py.py.

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

def z3py.fpMinusZero

(

s

)

Create a Z3 floating-point -0.0 term.

Definition at line 9850 of file z3py.py.

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

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

Create a Z3 floating-point multiplication expression.

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

Definition at line 10075 of file z3py.py.

Referenced by FPs().

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

    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpMul(rm, x, y)
    fpMul(RNE(), x, y)
    >>> fpMul(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)

def z3py.fpNaN

(

s

)

Create a Z3 floating-point NaN term.

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

Definition at line 9797 of file z3py.py.

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

    >>> s = FPSort(8, 24)
    >>> set_fpa_pretty(True)
    >>> fpNaN(s)
    NaN
    >>> pb = get_fpa_pretty()
    >>> set_fpa_pretty(False)
    >>> fpNaN(s)
    fpNaN(FPSort(8, 24))
    >>> set_fpa_pretty(pb)
    """
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)

def z3py.fpNeg	(		a,
			ctx = None
	)

Create a Z3 floating-point addition expression.

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

Definition at line 9975 of file z3py.py.

def 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)
    """
    ctx = _get_ctx(ctx)
    [a] = _coerce_fp_expr_list([a], ctx)
    return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)

def z3py.fpNEQ	(		a,
			b,
			ctx = None
	)

Create the Z3 floating-point expression `Not(fpEQ(other, self))`.

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

Definition at line 10285 of file z3py.py.

def 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)'
    """
    return Not(fpEQ(a, b, ctx))

def z3py.fpPlusInfinity

(

s

)

Create a Z3 floating-point +oo term.

>>> s = FPSort(8, 24)
>>> pb = get_fpa_pretty()
>>> set_fpa_pretty(True)
>>> fpPlusInfinity(s)
+oo
>>> set_fpa_pretty(False)
>>> fpPlusInfinity(s)
fpPlusInfinity(FPSort(8, 24))
>>> set_fpa_pretty(pb)

Definition at line 9814 of file z3py.py.

def 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)
    """
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)

def z3py.fpPlusZero

(

s

)

Create a Z3 floating-point +0.0 term.

Definition at line 9844 of file z3py.py.

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

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

Create a Z3 floating-point conversion expression that represents the
conversion from a real term to a floating-point term.

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

Definition at line 10402 of file z3py.py.

def 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
    """
    _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
    _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
    _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
    ctx = _get_ctx(ctx)
    return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)

def z3py.fpRem	(		a,
			b,
			ctx = None
	)

Create a Z3 floating-point remainder expression.

>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpRem(x, y)
fpRem(x, y)
>>> fpRem(x, y).sort()
FPSort(8, 24)

Definition at line 10105 of file z3py.py.

def 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)
    """
    return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)

def z3py.fpRoundToIntegral	(		rm,
			a,
			ctx = None
	)

Create a Z3 floating-point roundToIntegral expression.

Definition at line 10161 of file z3py.py.

def fpRoundToIntegral(rm, a, ctx=None):
    """Create a Z3 floating-point roundToIntegral expression.
    """
    return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)

def z3py.FPs	(		names,
			fpsort,
			ctx = None
	)

Return an array of floating-point constants.

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

Definition at line 9933 of file z3py.py.

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

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

    >>> x, y, z = FPs('x y z', FPSort(8, 24))
    >>> x.sort()
    FPSort(8, 24)
    >>> x.sbits()
    24
    >>> x.ebits()
    8
    >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
    fpMul(RNE(), fpAdd(RNE(), x, y), z)
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [FP(name, fpsort, ctx) for name in names]

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

Create a Z3 floating-point conversion expression that represents the
conversion from a signed bit-vector term (encoding an integer) to a floating-point term.

>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
>>> x_fp
fpToFP(RNE(), 4294967291)
>>> simplify(x_fp)
-1.25*(2**2)

Definition at line 10420 of file z3py.py.

def 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)
    """
    _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
    _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
    _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
    ctx = _get_ctx(ctx)
    return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)

def z3py.FPSort	(		ebits,
			sbits,
			ctx = None
	)

Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.

>>> Single = FPSort(8, 24)
>>> Double = FPSort(11, 53)
>>> Single
FPSort(8, 24)
>>> x = Const('x', Single)
>>> eq(x, FP('x', FPSort(8, 24)))
True

Definition at line 9738 of file z3py.py.

Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FPSortRef.cast(), FPSortRef.ebits(), FPRef.ebits(), FPNumRef.exponent(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpFP(), fpFPToFP(), fpGEQ(), fpGT(), fpIsInf(), fpIsNaN(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNaN(), fpNeg(), fpNEQ(), fpPlusInfinity(), fpRem(), FPs(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), is_fp(), is_fp_sort(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), and FPRef.sort().

def 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
    """
    ctx = _get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)

def z3py.fpSqrt	(		rm,
			a,
			ctx = None
	)

Create a Z3 floating-point square root expression.

Definition at line 10155 of file z3py.py.

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

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

Create a Z3 floating-point subtraction expression.

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

Definition at line 10060 of file z3py.py.

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

    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpSub(rm, x, y)
    fpSub(RNE(), x, y)
    >>> fpSub(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)

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

Create a Z3 floating-point conversion expression from other term sorts
to floating-point.

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

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

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

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

Definition at line 10326 of file z3py.py.

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

def 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)
    """
    ctx = _get_ctx(ctx)
    if is_bv(a1) and is_fp_sort(a2):
        return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
    elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
        return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
    elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
        return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
    elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
        return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
    else:
        raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")

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

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

Definition at line 10456 of file z3py.py.

Referenced by fpUnsignedToFP().

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

def z3py.fpToIEEEBV	(		x,
			ctx = None
	)

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

The size of the resulting bit-vector is automatically determined.

Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
knows only one NaN and it will always produce the same bit-vector representation of
that NaN.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToIEEEBV(x)
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False

Definition at line 10530 of file z3py.py.

Referenced by fpToFP().

def 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
    """
    if z3_debug():
        _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
    ctx = _get_ctx(ctx)
    return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)

def z3py.fpToReal	(		x,
			ctx = None
	)

Create a Z3 floating-point conversion expression, from floating-point expression to real.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToReal(x)
>>> print(is_fp(x))
True
>>> print(is_real(y))
True
>>> print(is_fp(y))
False
>>> print(is_real(x))
False

Definition at line 10510 of file z3py.py.

def 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
    """
    if z3_debug():
        _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)

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

Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToSBV(RTZ(), x, BitVecSort(32))
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False

Definition at line 10466 of file z3py.py.

def 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
    """
    if z3_debug():
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
        _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
    ctx = _get_ctx(ctx)
    return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)

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

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

>>> x = FP('x', FPSort(8, 24))
>>> y = fpToUBV(RTZ(), x, BitVecSort(32))
>>> print(is_fp(x))
True
>>> print(is_bv(y))
True
>>> print(is_fp(y))
False
>>> print(is_bv(x))
False

Definition at line 10488 of file z3py.py.

def 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
    """
    if z3_debug():
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
        _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
    ctx = _get_ctx(ctx)
    return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)

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

Create a Z3 floating-point conversion expression that represents the
conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.

>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
>>> x_fp
fpToFPUnsigned(RNE(), 4294967291)
>>> simplify(x_fp)
1*(2**32)

Definition at line 10438 of file z3py.py.

def 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)
    """
    _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
    _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
    _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
    ctx = _get_ctx(ctx)
    return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)

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

Return a floating-point value of value `val` and sort `fps`.
If `ctx=None`, then the global context is used.

>>> v = FPVal(20.0, FPSort(8, 24))
>>> v
1.25*(2**4)
>>> print("0x%.8x" % v.exponent_as_long(False))
0x00000004
>>> v = FPVal(2.25, FPSort(8, 24))
>>> v
1.125*(2**1)
>>> v = FPVal(-2.25, FPSort(8, 24))
>>> v
-1.125*(2**1)
>>> FPVal(-0.0, FPSort(8, 24))
-0.0
>>> FPVal(0.0, FPSort(8, 24))
+0.0
>>> FPVal(+0.0, FPSort(8, 24))
+0.0

Definition at line 9863 of file z3py.py.

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

def 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
    """
    ctx = _get_ctx(ctx)
    if is_fp_sort(exp):
        fps = exp
        exp = None
    elif fps is None:
        fps = _dflt_fps(ctx)
    _z3_assert(is_fp_sort(fps), "sort mismatch")
    if exp is None:
        exp = 0
    val = _to_float_str(sig)
    if val == "NaN" or val == "nan":
        return fpNaN(fps)
    elif val == "-0.0":
        return fpMinusZero(fps)
    elif val == "0.0" or val == "+0.0":
        return fpPlusZero(fps)
    elif val == "+oo" or val == "+inf" or val == "+Inf":
        return fpPlusInfinity(fps)
    elif val == "-oo" or val == "-inf" or val == "-Inf":
        return fpMinusInfinity(fps)
    else:
        return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)

def z3py.fpZero	(		s,
			negative
	)

Create a Z3 floating-point +0.0 or -0.0 term.

Definition at line 9856 of file z3py.py.

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

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

Return a fresh Boolean constant in the given context using the given prefix.

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

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

Definition at line 1737 of file z3py.py.

def 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
    """
    ctx = _get_ctx(ctx)
    return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)

def z3py.FreshConst	(		sort,
			prefix = "c"
	)

Create a fresh constant of a specified sort

Definition at line 1434 of file z3py.py.

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

def z3py.FreshFunction

(

sig

)

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

Definition at line 885 of file z3py.py.

def FreshFunction(*sig):
    """Create a new fresh Z3 uninterpreted function with the given sorts.
    """
    sig = _get_args(sig)
    if z3_debug():
        _z3_assert(len(sig) > 0, "At least two arguments expected")
    arity = len(sig) - 1
    rng = sig[arity]
    if z3_debug():
        _z3_assert(is_sort(rng), "Z3 sort expected")
    dom = (z3.Sort * arity)()
    for i in range(arity):
        if z3_debug():
            _z3_assert(is_sort(sig[i]), "Z3 sort expected")
        dom[i] = sig[i].ast
    ctx = rng.ctx
    return FuncDeclRef(Z3_mk_fresh_func_decl(ctx.ref(), "f", arity, dom, rng.ast), ctx)

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

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

>>> x = FreshInt()
>>> y = FreshInt()
>>> eq(x, y)
False
>>> x.sort()
Int

Definition at line 3251 of file z3py.py.

def 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
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)

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

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

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

Definition at line 3308 of file z3py.py.

def 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
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)

def z3py.Full

(

s

)

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

Definition at line 10763 of file z3py.py.

def Full(s):
    """Create the regular expression that accepts the universal language
    >>> e = Full(ReSort(SeqSort(IntSort())))
    >>> print(e)
    Full(ReSort(Seq(Int)))
    >>> e1 = Full(ReSort(StringSort()))
    >>> print(e1)
    Full(ReSort(String))
    """
    if isinstance(s, ReSortRef):
        return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
    raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")

def z3py.FullSet

(

s

)

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

Definition at line 4867 of file z3py.py.

def FullSet(s):
    """Create the full set
    >>> FullSet(IntSort())
    K(Int, True)
    """
    ctx = s.ctx
    return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)

def z3py.Function	(		name,
			sig
	)

Create a new Z3 uninterpreted function with the given sorts.

>>> f = Function('f', IntSort(), IntSort())
>>> f(f(0))
f(f(0))

Definition at line 862 of file z3py.py.

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

def Function(name, *sig):
    """Create a new Z3 uninterpreted function with the given sorts.

    >>> f = Function('f', IntSort(), IntSort())
    >>> f(f(0))
    f(f(0))
    """
    sig = _get_args(sig)
    if z3_debug():
        _z3_assert(len(sig) > 0, "At least two arguments expected")
    arity = len(sig) - 1
    rng = sig[arity]
    if z3_debug():
        _z3_assert(is_sort(rng), "Z3 sort expected")
    dom = (Sort * arity)()
    for i in range(arity):
        if z3_debug():
            _z3_assert(is_sort(sig[i]), "Z3 sort expected")
        dom[i] = sig[i].ast
    ctx = rng.ctx
    return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)

def z3py.get_as_array_func

(

n

)

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

Definition at line 6600 of file z3py.py.

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

def z3py.get_ctx

(

ctx

)

Definition at line 266 of file z3py.py.

def get_ctx(ctx):
    return _get_ctx(ctx)

def z3py.get_default_fp_sort

(

ctx = None

)

Definition at line 9160 of file z3py.py.

def get_default_fp_sort(ctx=None):
    return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)

def z3py.get_default_rounding_mode

(

ctx = None

)

Retrieves the global default rounding mode.

Definition at line 9127 of file z3py.py.

def get_default_rounding_mode(ctx=None):
    """Retrieves the global default rounding mode."""
    global _dflt_rounding_mode
    if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
        return RTZ(ctx)
    elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
        return RTN(ctx)
    elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
        return RTP(ctx)
    elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
        return RNE(ctx)
    elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
        return RNA(ctx)

def z3py.get_full_version

(

)

Definition at line 103 of file z3py.py.

def get_full_version():
    return Z3_get_full_version()

# We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com

def z3py.get_map_func

(

a

)

Return the function declaration associated with a Z3 map array expression.

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

Definition at line 4623 of file z3py.py.

def 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)
    """
    if z3_debug():
        _z3_assert(is_map(a), "Z3 array map expression expected.")
    return FuncDeclRef(
        Z3_to_func_decl(
            a.ctx_ref(),
            Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
        ),
        ctx=a.ctx,
    )

def z3py.get_param

(

name

)

Return the value of a Z3 global (or module) parameter

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

Definition at line 306 of file z3py.py.

def get_param(name):
    """Return the value of a Z3 global (or module) parameter

    >>> get_param('nlsat.reorder')
    'true'
    """
    ptr = (ctypes.c_char_p * 1)()
    if Z3_global_param_get(str(name), ptr):
        r = z3core._to_pystr(ptr[0])
        return r
    raise Z3Exception("failed to retrieve value for '%s'" % name)

def z3py.get_var_index

(

a

)

Return the de-Bruijn index of the Z3 bounded variable `a`.

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

Definition at line 1305 of file z3py.py.

def 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
    """
    if z3_debug():
        _z3_assert(is_var(a), "Z3 bound variable expected")
    return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))

def z3py.get_version

(

)

Definition at line 94 of file z3py.py.

def get_version():
    major = ctypes.c_uint(0)
    minor = ctypes.c_uint(0)
    build = ctypes.c_uint(0)
    rev = ctypes.c_uint(0)
    Z3_get_version(major, minor, build, rev)
    return (major.value, minor.value, build.value, rev.value)

def z3py.get_version_string

(

)

Definition at line 85 of file z3py.py.

def get_version_string():
    major = ctypes.c_uint(0)
    minor = ctypes.c_uint(0)
    build = ctypes.c_uint(0)
    rev = ctypes.c_uint(0)
    Z3_get_version(major, minor, build, rev)
    return "%s.%s.%s" % (major.value, minor.value, build.value)

def z3py.help_simplify

(

)

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

Definition at line 8681 of file z3py.py.

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

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

Create a Z3 if-then-else expression.

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

Definition at line 1351 of file z3py.py.

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

def 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)
    """
    if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
        return Cond(a, b, c, ctx)
    else:
        ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
        s = BoolSort(ctx)
        a = s.cast(a)
        b, c = _coerce_exprs(b, c, ctx)
        if z3_debug():
            _z3_assert(a.ctx == b.ctx, "Context mismatch")
        return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)

def z3py.Implies	(		a,
			b,
			ctx = None
	)

Create a Z3 implies expression.

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

Definition at line 1751 of file z3py.py.

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

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

    >>> p, q = Bools('p q')
    >>> Implies(p, q)
    Implies(p, q)
    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
    s = BoolSort(ctx)
    a = s.cast(a)
    b = s.cast(b)
    return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.IndexOf	(		s,
			substr,
			offset = None
	)

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

Definition at line 10846 of file z3py.py.

def 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
    """
    if offset is None:
        offset = IntVal(0)
    ctx = None
    if is_expr(offset):
        ctx = offset.ctx
    ctx = _get_ctx2(s, substr, ctx)
    s = _coerce_seq(s, ctx)
    substr = _coerce_seq(substr, ctx)
    if _is_int(offset):
        offset = IntVal(offset, ctx)
    return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)

def z3py.InRe	(		s,
			re
	)

Create regular expression membership test
>>> re = Union(Re("a"),Re("b"))
>>> print (simplify(InRe("a", re)))
True
>>> print (simplify(InRe("b", re)))
True
>>> print (simplify(InRe("c", re)))
False

Definition at line 10947 of file z3py.py.

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

def InRe(s, re):
    """Create regular expression membership test
    >>> re = Union(Re("a"),Re("b"))
    >>> print (simplify(InRe("a", re)))
    True
    >>> print (simplify(InRe("b", re)))
    True
    >>> print (simplify(InRe("c", re)))
    False
    """
    s = _coerce_seq(s, re.ctx)
    return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)

def z3py.Int	(		name,
			ctx = None
	)

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

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

Definition at line 3212 of file z3py.py.

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

def 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
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)

def z3py.Int2BV	(		a,
			num_bits
	)

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

Definition at line 3960 of file z3py.py.

def 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
    """
    ctx = a.ctx
    return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)

def z3py.Intersect

(

args

)

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

Definition at line 10981 of file z3py.py.

def Intersect(*args):
    """Create intersection of regular expressions.
    >>> re = Intersect(Re("a"), Re("b"), Re("c"))
    """
    args = _get_args(args)
    sz = len(args)
    if z3_debug():
        _z3_assert(sz > 0, "At least one argument expected.")
        _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
    if sz == 1:
        return args[0]
    ctx = args[0].ctx
    v = (Ast * sz)()
    for i in range(sz):
        v[i] = args[i].as_ast()
    return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)

def z3py.Ints	(		names,
			ctx = None
	)

Return a tuple of Integer constants.

>>> x, y, z = Ints('x y z')
>>> Sum(x, y, z)
x + y + z

Definition at line 3225 of file z3py.py.

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

def Ints(names, ctx=None):
    """Return a tuple of Integer constants.

    >>> x, y, z = Ints('x y z')
    >>> Sum(x, y, z)
    x + y + z
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [Int(name, ctx) for name in names]

def z3py.IntSort

(

ctx = None

)

Return the integer sort in the given context. If `ctx=None`, then the global context is used.

>>> IntSort()
Int
>>> x = Const('x', IntSort())
>>> is_int(x)
True
>>> x.sort() == IntSort()
True
>>> x.sort() == BoolSort()
False

Definition at line 3102 of file z3py.py.

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

def 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
    """
    ctx = _get_ctx(ctx)
    return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)

def z3py.IntToStr

(

s

)

Convert integer expression to string

Definition at line 10901 of file z3py.py.

Referenced by StrToInt().

def IntToStr(s):
    """Convert integer expression to string"""
    if not is_expr(s):
        s = _py2expr(s)
    return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)

def z3py.IntVal	(		val,
			ctx = None
	)

Return a Z3 integer value. If `ctx=None`, then the global context is used.

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

Definition at line 3152 of file z3py.py.

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

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

    >>> IntVal(1)
    1
    >>> IntVal("100")
    100
    """
    ctx = _get_ctx(ctx)
    return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)

def z3py.IntVector	(		prefix,
			sz,
			ctx = None
	)

Return a list of integer constants of size `sz`.

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

Definition at line 3238 of file z3py.py.

def 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
    """
    ctx = _get_ctx(ctx)
    return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]

def z3py.is_add

(

a

)

Return `True` if `a` is an expression of the form b + c.

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

Definition at line 2756 of file z3py.py.

def is_add(a):
    """Return `True` if `a` is an expression of the form b + c.

    >>> x, y = Ints('x y')
    >>> is_add(x + y)
    True
    >>> is_add(x - y)
    False
    """
    return is_app_of(a, Z3_OP_ADD)

def z3py.is_algebraic_value

(

a

)

Return `True` if `a` is an algebraic value of sort Real.

>>> is_algebraic_value(RealVal("3/5"))
False
>>> n = simplify(Sqrt(2))
>>> n
1.4142135623?
>>> is_algebraic_value(n)
True

Definition at line 2742 of file z3py.py.

def 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
    """
    return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())

def z3py.is_and

(

a

)

Return `True` if `a` is a Z3 and expression.

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

Definition at line 1587 of file z3py.py.

def is_and(a):
    """Return `True` if `a` is a Z3 and expression.

    >>> p, q = Bools('p q')
    >>> is_and(And(p, q))
    True
    >>> is_and(Or(p, q))
    False
    """
    return is_app_of(a, Z3_OP_AND)

def z3py.is_app

(

a

)

Return `True` if `a` is a Z3 function application.

Note that, constants are function applications with 0 arguments.

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

Definition at line 1235 of file z3py.py.

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

def is_app(a):
    """Return `True` if `a` is a Z3 function application.

    Note that, constants are function applications with 0 arguments.

    >>> a = Int('a')
    >>> is_app(a)
    True
    >>> is_app(a + 1)
    True
    >>> is_app(IntSort())
    False
    >>> is_app(1)
    False
    >>> is_app(IntVal(1))
    True
    >>> x = Int('x')
    >>> is_app(ForAll(x, x >= 0))
    False
    """
    if not isinstance(a, ExprRef):
        return False
    k = _ast_kind(a.ctx, a)
    return k == Z3_NUMERAL_AST or k == Z3_APP_AST

def z3py.is_app_of	(		a,
			k
	)

Return `True` if `a` is an application of the given kind `k`.

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

Definition at line 1338 of file z3py.py.

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

def 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
    """
    return is_app(a) and a.decl().kind() == k

def z3py.is_arith

(

a

)

Return `True` if `a` is an arithmetical expression.

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

Definition at line 2629 of file z3py.py.

Referenced by is_algebraic_value().

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

    >>> x = Int('x')
    >>> is_arith(x)
    True
    >>> is_arith(x + 1)
    True
    >>> is_arith(1)
    False
    >>> is_arith(IntVal(1))
    True
    >>> y = Real('y')
    >>> is_arith(y)
    True
    >>> is_arith(y + 1)
    True
    """
    return isinstance(a, ArithRef)

def z3py.is_arith_sort

(

s

)

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

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

Definition at line 2328 of file z3py.py.

def 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
    """
    return isinstance(s, ArithSortRef)

def z3py.is_array

(

a

)

Return `True` if `a` is a Z3 array expression.

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

Definition at line 4558 of file z3py.py.

Referenced by Ext().

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

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

def z3py.is_array_sort

(

a

)

Definition at line 4554 of file z3py.py.

Referenced by Default(), and Ext().

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

def z3py.is_as_array

(

n

)

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

Definition at line 6595 of file z3py.py.

Referenced by get_as_array_func().

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

def z3py.is_ast

(

a

)

Return `True` if `a` is an AST node.

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

Definition at line 450 of file z3py.py.

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

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

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

def z3py.is_bool

(

a

)

Return `True` if `a` is a Z3 Boolean expression.

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

Definition at line 1537 of file z3py.py.

Referenced by BoolSort(), and prove().

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

    >>> p = Bool('p')
    >>> is_bool(p)
    True
    >>> q = Bool('q')
    >>> is_bool(And(p, q))
    True
    >>> x = Real('x')
    >>> is_bool(x)
    False
    >>> is_bool(x == 0)
    True
    """
    return isinstance(a, BoolRef)

def z3py.is_bv

(

a

)

Return `True` if `a` is a Z3 bit-vector expression.

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

Definition at line 3908 of file z3py.py.

Referenced by BitVec(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToIEEEBV(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), Product(), and Sum().

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

    >>> b = BitVec('b', 32)
    >>> is_bv(b)
    True
    >>> is_bv(b + 10)
    True
    >>> is_bv(Int('x'))
    False
    """
    return isinstance(a, BitVecRef)

def z3py.is_bv_sort

(

s

)

Return True if `s` is a Z3 bit-vector sort.

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

Definition at line 3440 of file z3py.py.

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

def 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
    """
    return isinstance(s, BitVecSortRef)

def z3py.is_bv_value

(

a

)

Return `True` if `a` is a Z3 bit-vector numeral value.

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

Definition at line 3922 of file z3py.py.

def 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
    """
    return is_bv(a) and _is_numeral(a.ctx, a.as_ast())

def z3py.is_const

(

a

)

Return `True` if `a` is Z3 constant/variable expression.

>>> a = Int('a')
>>> is_const(a)
True
>>> is_const(a + 1)
False
>>> is_const(1)
False
>>> is_const(IntVal(1))
True
>>> x = Int('x')
>>> is_const(ForAll(x, x >= 0))
False

Definition at line 1261 of file z3py.py.

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

def is_const(a):
    """Return `True` if `a` is Z3 constant/variable expression.

    >>> a = Int('a')
    >>> is_const(a)
    True
    >>> is_const(a + 1)
    False
    >>> is_const(1)
    False
    >>> is_const(IntVal(1))
    True
    >>> x = Int('x')
    >>> is_const(ForAll(x, x >= 0))
    False
    """
    return is_app(a) and a.num_args() == 0

def z3py.is_const_array

(

a

)

Return `True` if `a` is a Z3 constant array.

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

Definition at line 4572 of file z3py.py.

def 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
    """
    return is_app_of(a, Z3_OP_CONST_ARRAY)

def z3py.is_default

(

a

)

Return `True` if `a` is a Z3 default array expression.
>>> d = Default(K(IntSort(), 10))
>>> is_default(d)
True

Definition at line 4614 of file z3py.py.

def is_default(a):
    """Return `True` if `a` is a Z3 default array expression.
    >>> d = Default(K(IntSort(), 10))
    >>> is_default(d)
    True
    """
    return is_app_of(a, Z3_OP_ARRAY_DEFAULT)

def z3py.is_distinct

(

a

)

Return `True` if `a` is a Z3 distinct expression.

>>> x, y, z = Ints('x y z')
>>> is_distinct(x == y)
False
>>> is_distinct(Distinct(x, y, z))
True

Definition at line 1645 of file z3py.py.

def 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
    """
    return is_app_of(a, Z3_OP_DISTINCT)

def z3py.is_div

(

a

)

Return `True` if `a` is an expression of the form b / c.

>>> x, y = Reals('x y')
>>> is_div(x / y)
True
>>> is_div(x + y)
False
>>> x, y = Ints('x y')
>>> is_div(x / y)
False
>>> is_idiv(x / y)
True

Definition at line 2792 of file z3py.py.

def is_div(a):
    """Return `True` if `a` is an expression of the form b / c.

    >>> x, y = Reals('x y')
    >>> is_div(x / y)
    True
    >>> is_div(x + y)
    False
    >>> x, y = Ints('x y')
    >>> is_div(x / y)
    False
    >>> is_idiv(x / y)
    True
    """
    return is_app_of(a, Z3_OP_DIV)

def z3py.is_eq

(

a

)

Return `True` if `a` is a Z3 equality expression.

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

Definition at line 1635 of file z3py.py.

Referenced by AstRef.__bool__().

def is_eq(a):
    """Return `True` if `a` is a Z3 equality expression.

    >>> x, y = Ints('x y')
    >>> is_eq(x == y)
    True
    """
    return is_app_of(a, Z3_OP_EQ)

def z3py.is_expr

(

a

)

Return `True` if `a` is a Z3 expression.

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

Definition at line 1212 of file z3py.py.

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

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

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

def z3py.is_false

(

a

)

Return `True` if `a` is the Z3 false expression.

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

Definition at line 1573 of file z3py.py.

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

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

    >>> p = Bool('p')
    >>> is_false(p)
    False
    >>> is_false(False)
    False
    >>> is_false(BoolVal(False))
    True
    """
    return is_app_of(a, Z3_OP_FALSE)

def z3py.is_finite_domain

(

a

)

Return `True` if `a` is a Z3 finite-domain expression.

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

Definition at line 7632 of file z3py.py.

Referenced by is_finite_domain_value().

def 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
    """
    return isinstance(a, FiniteDomainRef)

def z3py.is_finite_domain_sort

(

s

)

Return True if `s` is a Z3 finite-domain sort.

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

Definition at line 7609 of file z3py.py.

Referenced by FiniteDomainVal().

def 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
    """
    return isinstance(s, FiniteDomainSortRef)

def z3py.is_finite_domain_value

(

a

)

Return `True` if `a` is a Z3 finite-domain value.

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

Definition at line 7686 of file z3py.py.

def 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
    """
    return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())

def z3py.is_fp

(

a

)

Return `True` if `a` is a Z3 floating-point expression.

>>> b = FP('b', FPSort(8, 24))
>>> is_fp(b)
True
>>> is_fp(b + 1.0)
True
>>> is_fp(Int('x'))
False

Definition at line 9709 of file z3py.py.

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

def is_fp(a):
    """Return `True` if `a` is a Z3 floating-point expression.

    >>> b = FP('b', FPSort(8, 24))
    >>> is_fp(b)
    True
    >>> is_fp(b + 1.0)
    True
    >>> is_fp(Int('x'))
    False
    """
    return isinstance(a, FPRef)

def z3py.is_fp_sort

(

s

)

Return True if `s` is a Z3 floating-point sort.

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

Definition at line 9293 of file z3py.py.

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

def 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
    """
    return isinstance(s, FPSortRef)

def z3py.is_fp_value

(

a

)

Return `True` if `a` is a Z3 floating-point numeral value.

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

Definition at line 9723 of file z3py.py.

def 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
    """
    return is_fp(a) and _is_numeral(a.ctx, a.ast)

def z3py.is_fprm

(

a

)

Return `True` if `a` is a Z3 floating-point rounding mode expression.

>>> rm = RNE()
>>> is_fprm(rm)
True
>>> rm = 1.0
>>> is_fprm(rm)
False

Definition at line 9553 of file z3py.py.

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

def is_fprm(a):
    """Return `True` if `a` is a Z3 floating-point rounding mode expression.

    >>> rm = RNE()
    >>> is_fprm(rm)
    True
    >>> rm = 1.0
    >>> is_fprm(rm)
    False
    """
    return isinstance(a, FPRMRef)

def z3py.is_fprm_sort

(

s

)

Return True if `s` is a Z3 floating-point rounding mode sort.

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

Definition at line 9304 of file z3py.py.

def 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
    """
    return isinstance(s, FPRMSortRef)

# FP Expressions

def z3py.is_fprm_value

(

a

)

Return `True` if `a` is a Z3 floating-point rounding mode numeral value.

Definition at line 9566 of file z3py.py.

def is_fprm_value(a):
    """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
    return is_fprm(a) and _is_numeral(a.ctx, a.ast)

# FP Numerals

def z3py.is_func_decl

(

a

)

Return `True` if `a` is a Z3 function declaration.

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

Definition at line 849 of file z3py.py.

Referenced by prove().

def 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
    """
    return isinstance(a, FuncDeclRef)

def z3py.is_ge

(

a

)

Return `True` if `a` is an expression of the form b >= c.

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

Definition at line 2857 of file z3py.py.

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

    >>> x, y = Ints('x y')
    >>> is_ge(x >= y)
    True
    >>> is_ge(x == y)
    False
    """
    return is_app_of(a, Z3_OP_GE)

def z3py.is_gt

(

a

)

Return `True` if `a` is an expression of the form b > c.

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

Definition at line 2869 of file z3py.py.

def is_gt(a):
    """Return `True` if `a` is an expression of the form b > c.

    >>> x, y = Ints('x y')
    >>> is_gt(x > y)
    True
    >>> is_gt(x == y)
    False
    """
    return is_app_of(a, Z3_OP_GT)

def z3py.is_idiv

(

a

)

Return `True` if `a` is an expression of the form b div c.

>>> x, y = Ints('x y')
>>> is_idiv(x / y)
True
>>> is_idiv(x + y)
False

Definition at line 2809 of file z3py.py.

Referenced by is_div().

def is_idiv(a):
    """Return `True` if `a` is an expression of the form b div c.

    >>> x, y = Ints('x y')
    >>> is_idiv(x / y)
    True
    >>> is_idiv(x + y)
    False
    """
    return is_app_of(a, Z3_OP_IDIV)

def z3py.is_implies

(

a

)

Return `True` if `a` is a Z3 implication expression.

>>> p, q = Bools('p q')
>>> is_implies(Implies(p, q))
True
>>> is_implies(And(p, q))
False

Definition at line 1611 of file z3py.py.

def 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
    """
    return is_app_of(a, Z3_OP_IMPLIES)

def z3py.is_int

(

a

)

Return `True` if `a` is an integer expression.

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

Definition at line 2650 of file z3py.py.

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

def is_int(a):
    """Return `True` if `a` is an integer expression.

    >>> x = Int('x')
    >>> is_int(x + 1)
    True
    >>> is_int(1)
    False
    >>> is_int(IntVal(1))
    True
    >>> y = Real('y')
    >>> is_int(y)
    False
    >>> is_int(y + 1)
    False
    """
    return is_arith(a) and a.is_int()

def z3py.is_int_value

(

a

)

Return `True` if `a` is an integer value of sort Int.

>>> is_int_value(IntVal(1))
True
>>> is_int_value(1)
False
>>> is_int_value(Int('x'))
False
>>> n = Int('x') + 1
>>> n
x + 1
>>> n.arg(1)
1
>>> is_int_value(n.arg(1))
True
>>> is_int_value(RealVal("1/3"))
False
>>> is_int_value(RealVal(1))
False

Definition at line 2696 of file z3py.py.

def 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
    """
    return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())

def z3py.is_is_int

(

a

)

Return `True` if `a` is an expression of the form IsInt(b).

>>> x = Real('x')
>>> is_is_int(IsInt(x))
True
>>> is_is_int(x)
False

Definition at line 2881 of file z3py.py.

def is_is_int(a):
    """Return `True` if `a` is an expression of the form IsInt(b).

    >>> x = Real('x')
    >>> is_is_int(IsInt(x))
    True
    >>> is_is_int(x)
    False
    """
    return is_app_of(a, Z3_OP_IS_INT)

def z3py.is_K

(

a

)

Return `True` if `a` is a Z3 constant array.

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

Definition at line 4585 of file z3py.py.

def is_K(a):
    """Return `True` if `a` is a Z3 constant array.

    >>> a = K(IntSort(), 10)
    >>> is_K(a)
    True
    >>> a = Array('a', IntSort(), IntSort())
    >>> is_K(a)
    False
    """
    return is_app_of(a, Z3_OP_CONST_ARRAY)

def z3py.is_le

(

a

)

Return `True` if `a` is an expression of the form b <= c.

>>> x, y = Ints('x y')
>>> is_le(x <= y)
True
>>> is_le(x < y)
False

Definition at line 2833 of file z3py.py.

def is_le(a):
    """Return `True` if `a` is an expression of the form b <= c.

    >>> x, y = Ints('x y')
    >>> is_le(x <= y)
    True
    >>> is_le(x < y)
    False
    """
    return is_app_of(a, Z3_OP_LE)

def z3py.is_lt

(

a

)

Return `True` if `a` is an expression of the form b < c.

>>> x, y = Ints('x y')
>>> is_lt(x < y)
True
>>> is_lt(x == y)
False

Definition at line 2845 of file z3py.py.

def is_lt(a):
    """Return `True` if `a` is an expression of the form b < c.

    >>> x, y = Ints('x y')
    >>> is_lt(x < y)
    True
    >>> is_lt(x == y)
    False
    """
    return is_app_of(a, Z3_OP_LT)

def z3py.is_map

(

a

)

Return `True` if `a` is a Z3 map array expression.

>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a  = Map(f, b)
>>> a
Map(f, b)
>>> is_map(a)
True
>>> is_map(b)
False

Definition at line 4598 of file z3py.py.

Referenced by get_map_func().

def is_map(a):
    """Return `True` if `a` is a Z3 map array expression.

    >>> f = Function('f', IntSort(), IntSort())
    >>> b = Array('b', IntSort(), IntSort())
    >>> a  = Map(f, b)
    >>> a
    Map(f, b)
    >>> is_map(a)
    True
    >>> is_map(b)
    False
    """
    return is_app_of(a, Z3_OP_ARRAY_MAP)

def z3py.is_mod

(

a

)

Return `True` if `a` is an expression of the form b % c.

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

Definition at line 2821 of file z3py.py.

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

    >>> x, y = Ints('x y')
    >>> is_mod(x % y)
    True
    >>> is_mod(x + y)
    False
    """
    return is_app_of(a, Z3_OP_MOD)

def z3py.is_mul

(

a

)

Return `True` if `a` is an expression of the form b * c.

>>> x, y = Ints('x y')
>>> is_mul(x * y)
True
>>> is_mul(x - y)
False

Definition at line 2768 of file z3py.py.

def is_mul(a):
    """Return `True` if `a` is an expression of the form b * c.

    >>> x, y = Ints('x y')
    >>> is_mul(x * y)
    True
    >>> is_mul(x - y)
    False
    """
    return is_app_of(a, Z3_OP_MUL)

def z3py.is_not

(

a

)

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

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

Definition at line 1623 of file z3py.py.

def is_not(a):
    """Return `True` if `a` is a Z3 not expression.

    >>> p = Bool('p')
    >>> is_not(p)
    False
    >>> is_not(Not(p))
    True
    """
    return is_app_of(a, Z3_OP_NOT)

def z3py.is_or

(

a

)

Return `True` if `a` is a Z3 or expression.

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

Definition at line 1599 of file z3py.py.

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

    >>> p, q = Bools('p q')
    >>> is_or(Or(p, q))
    True
    >>> is_or(And(p, q))
    False
    """
    return is_app_of(a, Z3_OP_OR)

def z3py.is_pattern

(

a

)

Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.

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

Definition at line 1899 of file z3py.py.

Referenced by MultiPattern().

def 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))
    """
    return isinstance(a, PatternRef)

def z3py.is_probe

(

p

)

Return `True` if `p` is a Z3 probe.

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

Definition at line 8522 of file z3py.py.

Referenced by eq().

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

    >>> is_probe(Int('x'))
    False
    >>> is_probe(Probe('memory'))
    True
    """
    return isinstance(p, Probe)

def z3py.is_quantifier

(

a

)

Return `True` if `a` is a Z3 quantifier.

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

Definition at line 2140 of file z3py.py.

Referenced by Exists().

def 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
    """
    return isinstance(a, QuantifierRef)

def z3py.is_rational_value

(

a

)

Return `True` if `a` is rational value of sort Real.

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

Definition at line 2720 of file z3py.py.

Referenced by RatNumRef.denominator(), and RatNumRef.numerator().

def 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
    """
    return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())

def z3py.is_re

(

s

)

Definition at line 10943 of file z3py.py.

Referenced by Concat(), and Intersect().

def is_re(s):
    return isinstance(s, ReRef)

def z3py.is_real

(

a

)

Return `True` if `a` is a real expression.

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

Definition at line 2669 of file z3py.py.

Referenced by fpRealToFP(), fpToFP(), fpToReal(), Real(), and RealSort().

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

    >>> x = Int('x')
    >>> is_real(x + 1)
    False
    >>> y = Real('y')
    >>> is_real(y)
    True
    >>> is_real(y + 1)
    True
    >>> is_real(1)
    False
    >>> is_real(RealVal(1))
    True
    """
    return is_arith(a) and a.is_real()

def z3py.is_select

(

a

)

Return `True` if `a` is a Z3 array select application.

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

Definition at line 4822 of file z3py.py.

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

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

def z3py.is_seq

(

a

)

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

Definition at line 10682 of file z3py.py.

Referenced by Concat(), and Extract().

def is_seq(a):
    """Return `True` if `a` is a Z3 sequence expression.
    >>> print (is_seq(Unit(IntVal(0))))
    True
    >>> print (is_seq(StringVal("abc")))
    True
    """
    return isinstance(a, SeqRef)

def z3py.is_sort

(

s

)

Return `True` if `s` is a Z3 sort.

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

Definition at line 646 of file z3py.py.

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

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

    >>> is_sort(IntSort())
    True
    >>> is_sort(Int('x'))
    False
    >>> is_expr(Int('x'))
    True
    """
    return isinstance(s, SortRef)

def z3py.is_store

(

a

)

Return `True` if `a` is a Z3 array store application.

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

Definition at line 4835 of file z3py.py.

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

    >>> a = Array('a', IntSort(), IntSort())
    >>> is_store(a)
    False
    >>> is_store(Store(a, 0, 1))
    True
    """
    return is_app_of(a, Z3_OP_STORE)

def z3py.is_string

(

a

)

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

Definition at line 10692 of file z3py.py.

def is_string(a):
    """Return `True` if `a` is a Z3 string expression.
    >>> print (is_string(StringVal("ab")))
    True
    """
    return isinstance(a, SeqRef) and a.is_string()

def z3py.is_string_value

(

a

)

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

Definition at line 10700 of file z3py.py.

def 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
    """
    return isinstance(a, SeqRef) and a.is_string_value()

def z3py.is_sub

(

a

)

Return `True` if `a` is an expression of the form b - c.

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

Definition at line 2780 of file z3py.py.

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

    >>> x, y = Ints('x y')
    >>> is_sub(x - y)
    True
    >>> is_sub(x + y)
    False
    """
    return is_app_of(a, Z3_OP_SUB)

def z3py.is_to_int

(

a

)

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

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

Definition at line 2908 of file z3py.py.

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

    >>> x = Real('x')
    >>> n = ToInt(x)
    >>> n
    ToInt(x)
    >>> is_to_int(n)
    True
    >>> is_to_int(x)
    False
    """
    return is_app_of(a, Z3_OP_TO_INT)

def z3py.is_to_real

(

a

)

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

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

Definition at line 2893 of file z3py.py.

def 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
    """
    return is_app_of(a, Z3_OP_TO_REAL)

def z3py.is_true

(

a

)

Return `True` if `a` is the Z3 true expression.

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

Definition at line 1555 of file z3py.py.

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

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

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

def z3py.is_var

(

a

)

Return `True` if `a` is variable.

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

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

Definition at line 1280 of file z3py.py.

Referenced by get_var_index().

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

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

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

def z3py.IsInt

(

a

)

Return the Z3 predicate IsInt(a).

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

Definition at line 3358 of file z3py.py.

Referenced by is_is_int().

def IsInt(a):
    """ Return the Z3 predicate IsInt(a).

    >>> x = Real('x')
    >>> IsInt(x + "1/2")
    IsInt(x + 1/2)
    >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
    [x = 1/2]
    >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
    no solution
    """
    if z3_debug():
        _z3_assert(a.is_real(), "Z3 real expression expected.")
    ctx = a.ctx
    return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)

def z3py.IsMember	(		e,
			s
	)

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

Definition at line 4945 of file z3py.py.

def IsMember(e, s):
    """ Check if e is a member of set s
    >>> a = Const('a', SetSort(IntSort()))
    >>> IsMember(1, a)
    a[1]
    """
    ctx = _ctx_from_ast_arg_list([s, e])
    e = _py2expr(e, ctx)
    return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)

def z3py.IsSubset	(		a,
			b
	)

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

Definition at line 4956 of file z3py.py.

def 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)
    """
    ctx = _ctx_from_ast_arg_list([a, b])
    return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.K	(		dom,
			v
	)

Return a Z3 constant array expression.

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

Definition at line 4782 of file z3py.py.

Referenced by Default(), EmptySet(), FullSet(), is_const_array(), is_default(), and is_K().

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

    >>> a = K(IntSort(), 10)
    >>> a
    K(Int, 10)
    >>> a.sort()
    Array(Int, Int)
    >>> i = Int('i')
    >>> a[i]
    K(Int, 10)[i]
    >>> simplify(a[i])
    10
    """
    if z3_debug():
        _z3_assert(is_sort(dom), "Z3 sort expected")
    ctx = dom.ctx
    if not is_expr(v):
        v = _py2expr(v, ctx)
    return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)

def z3py.Lambda	(		vs,
			body
	)

Create a Z3 lambda expression.

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

Definition at line 2228 of file z3py.py.

Referenced by QuantifierRef.is_lambda().

def 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]))
    """
    ctx = body.ctx
    if is_app(vs):
        vs = [vs]
    num_vars = len(vs)
    _vs = (Ast * num_vars)()
    for i in range(num_vars):
        # TODO: Check if is constant
        _vs[i] = vs[i].as_ast()
    return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)

def z3py.LastIndexOf	(		s,
			substr
	)

Retrieve the last index of substring within a string

Definition at line 10866 of file z3py.py.

def LastIndexOf(s, substr):
    """Retrieve the last index of substring within a string"""
    ctx = None
    ctx = _get_ctx2(s, substr, ctx)
    s = _coerce_seq(s, ctx)
    substr = _coerce_seq(substr, ctx)
    return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx)

def z3py.Length

(

s

)

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

Definition at line 10875 of file z3py.py.

def Length(s):
    """Obtain the length of a sequence 's'
    >>> l = Length(StringVal("abc"))
    >>> simplify(l)
    3
    """
    s = _coerce_seq(s)
    return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)

def z3py.LinearOrder	(		a,
			index
	)

Definition at line 11080 of file z3py.py.

def LinearOrder(a, index):
    return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx)

def z3py.Loop	(		re,
			lo,
			hi = 0
	)

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

Definition at line 11043 of file z3py.py.

def 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
    """
    return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)

def z3py.LShR	(		a,
			b
	)

Create the Z3 expression logical right shift.

Use the operator >> for the arithmetical right shift.

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

Definition at line 4263 of file z3py.py.

Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), and BitVecRef.__rshift__().

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

    Use the operator >> for the arithmetical right shift.

    >>> x, y = BitVecs('x y', 32)
    >>> LShR(x, y)
    LShR(x, y)
    >>> (x >> y).sexpr()
    '(bvashr x y)'
    >>> LShR(x, y).sexpr()
    '(bvlshr x y)'
    >>> BitVecVal(4, 3)
    4
    >>> BitVecVal(4, 3).as_signed_long()
    -4
    >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
    -2
    >>> simplify(BitVecVal(4, 3) >> 1)
    6
    >>> simplify(LShR(BitVecVal(4, 3), 1))
    2
    >>> simplify(BitVecVal(2, 3) >> 1)
    1
    >>> simplify(LShR(BitVecVal(2, 3), 1))
    1
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.main_ctx

(

)

Return a reference to the global Z3 context.

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

Definition at line 238 of file z3py.py.

Referenced by help_simplify(), simplify_param_descrs(), and Goal.translate().

def 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
    """
    global _main_ctx
    if _main_ctx is None:
        _main_ctx = Context()
    return _main_ctx

def z3py.Map	(		f,
			args
	)

Return a Z3 map array expression.

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

Definition at line 4759 of file z3py.py.

Referenced by get_map_func(), and is_map().

def 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
    """
    args = _get_args(args)
    if z3_debug():
        _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
        _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
        _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
        _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
    _args, sz = _to_ast_array(args)
    ctx = f.ctx
    return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)

def z3py.mk_not

(

a

)

Definition at line 1800 of file z3py.py.

def mk_not(a):
    if is_not(a):
        return a.arg(0)
    else:
        return Not(a)

def z3py.Model

(

ctx = None

)

Definition at line 6590 of file z3py.py.

Referenced by Optimize.set_on_model().

def Model(ctx=None):
    ctx = _get_ctx(ctx)
    return ModelRef(Z3_mk_model(ctx.ref()), ctx)

def z3py.MultiPattern

(

args

)

Create a Z3 multi-pattern using the given expressions `*args`

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

Definition at line 1917 of file z3py.py.

def 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)))
    """
    if z3_debug():
        _z3_assert(len(args) > 0, "At least one argument expected")
        _z3_assert(all([is_expr(a) for a in args]), "Z3 expressions expected")
    ctx = args[0].ctx
    args, sz = _to_ast_array(args)
    return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)

def z3py.Not	(		a,
			ctx = None
	)

Create a Z3 not expression or probe.

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

Definition at line 1781 of file z3py.py.

Referenced by Solver.consequences(), Goal.convert_model(), fpNEQ(), mk_not(), prove(), and Xor().

def 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
    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
    if is_probe(a):
        # Not is also used to build probes
        return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
    else:
        s = BoolSort(ctx)
        a = s.cast(a)
        return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)

def z3py.open_log

(

fname

)

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

Definition at line 119 of file z3py.py.

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

def z3py.Option

(

re

)

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

Definition at line 11012 of file z3py.py.

def Option(re):
    """Create the regular expression that optionally accepts the argument.
    >>> re = Option(Re("a"))
    >>> print(simplify(InRe("a", re)))
    True
    >>> print(simplify(InRe("", re)))
    True
    >>> print(simplify(InRe("aa", re)))
    False
    """
    return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)

def z3py.Or

(

args

)

Create a Z3 or-expression or or-probe.

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

Definition at line 1848 of file z3py.py.

Referenced by ApplyResult.as_expr(), Bools(), and Goal.convert_model().

def Or(*args):
    """Create a Z3 or-expression or or-probe.

    >>> p, q, r = Bools('p q r')
    >>> Or(p, q, r)
    Or(p, q, r)
    >>> P = BoolVector('p', 5)
    >>> Or(P)
    Or(p__0, p__1, p__2, p__3, p__4)
    """
    last_arg = None
    if len(args) > 0:
        last_arg = args[len(args) - 1]
    if isinstance(last_arg, Context):
        ctx = args[len(args) - 1]
        args = args[:len(args) - 1]
    elif len(args) == 1 and isinstance(args[0], AstVector):
        ctx = args[0].ctx
        args = [a for a in args[0]]
    else:
        ctx = None
    args = _get_args(args)
    ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
    if z3_debug():
        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
    if _has_probe(args):
        return _probe_or(args, ctx)
    else:
        args = _coerce_expr_list(args, ctx)
        _args, sz = _to_ast_array(args)
        return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)

def z3py.OrElse	(		ts,
			ks
	)

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

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

Definition at line 8215 of file z3py.py.

def 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]]
    """
    if z3_debug():
        _z3_assert(len(ts) >= 2, "At least two arguments expected")
    ctx = ks.get("ctx", None)
    num = len(ts)
    r = ts[0]
    for i in range(num - 1):
        r = _or_else(r, ts[i + 1], ctx)
    return r

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

Alias for ParThen(t1, t2, ctx).

Definition at line 8271 of file z3py.py.

def ParAndThen(t1, t2, ctx=None):
    """Alias for ParThen(t1, t2, ctx)."""
    return ParThen(t1, t2, ctx)

def z3py.ParOr	(		ts,
			ks
	)

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

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

Definition at line 8236 of file z3py.py.

def 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]]
    """
    if z3_debug():
        _z3_assert(len(ts) >= 2, "At least two arguments expected")
    ctx = _get_ctx(ks.get("ctx", None))
    ts = [_to_tactic(t, ctx) for t in ts]
    sz = len(ts)
    _args = (TacticObj * sz)()
    for i in range(sz):
        _args[i] = ts[i].tactic
    return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)

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

Parse a file in SMT 2.0 format using the given sorts and decls.

This function is similar to parse_smt2_string().

Definition at line 9103 of file z3py.py.

def 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().
    """
    ctx = _get_ctx(ctx)
    ssz, snames, ssorts = _dict2sarray(sorts, ctx)
    dsz, dnames, ddecls = _dict2darray(decls, ctx)
    return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)

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

Parse a string in SMT 2.0 format using the given sorts and decls.

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

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

Definition at line 9082 of file z3py.py.

Referenced by parse_smt2_file().

def 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]
    """
    ctx = _get_ctx(ctx)
    ssz, snames, ssorts = _dict2sarray(sorts, ctx)
    dsz, dnames, ddecls = _dict2darray(decls, ctx)
    return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)

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

Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
The subgoals are processed in parallel.

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

Definition at line 8255 of file z3py.py.

Referenced by ParAndThen().

def 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]]
    """
    t1 = _to_tactic(t1, ctx)
    t2 = _to_tactic(t2, ctx)
    if z3_debug():
        _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
    return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)

def z3py.PartialOrder	(		a,
			index
	)

Definition at line 11076 of file z3py.py.

def PartialOrder(a, index):
    return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx)

def z3py.PbEq	(		args,
			k,
			ctx = None
	)

Create a Pseudo-Boolean inequality k constraint.

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

Definition at line 8878 of file z3py.py.

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

    >>> a, b, c = Bools('a b c')
    >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
    """
    _z3_check_cint_overflow(k, "k")
    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
    return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)

def z3py.PbGe	(		args,
			k
	)

Create a Pseudo-Boolean inequality k constraint.

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

Definition at line 8867 of file z3py.py.

def 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)
    """
    _z3_check_cint_overflow(k, "k")
    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
    return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)

def z3py.PbLe	(		args,
			k
	)

Create a Pseudo-Boolean inequality k constraint.

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

Definition at line 8856 of file z3py.py.

def 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)
    """
    _z3_check_cint_overflow(k, "k")
    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
    return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)

def z3py.PiecewiseLinearOrder	(		a,
			index
	)

Definition at line 11088 of file z3py.py.

def PiecewiseLinearOrder(a, index):
    return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx)

def z3py.Plus

(

re

)

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

Definition at line 10999 of file z3py.py.

def Plus(re):
    """Create the regular expression accepting one or more repetitions of argument.
    >>> re = Plus(Re("a"))
    >>> print(simplify(InRe("aa", re)))
    True
    >>> print(simplify(InRe("ab", re)))
    False
    >>> print(simplify(InRe("", re)))
    False
    """
    return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)

def z3py.PrefixOf	(		a,
			b
	)

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

Definition at line 10782 of file z3py.py.

def 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
    """
    ctx = _get_ctx2(a, b)
    a = _coerce_seq(a, ctx)
    b = _coerce_seq(b, ctx)
    return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.probe_description	(		name,
			ctx = None
	)

Return a short description for the probe named `name`.

>>> d = probe_description('memory')

Definition at line 8551 of file z3py.py.

Referenced by describe_probes().

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

    >>> d = probe_description('memory')
    """
    ctx = _get_ctx(ctx)
    return Z3_probe_get_descr(ctx.ref(), name)

def z3py.probes

(

ctx = None

)

Return a list of all available probes in Z3.

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

Definition at line 8540 of file z3py.py.

Referenced by describe_probes().

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

    >>> l = probes()
    >>> l.count('memory') == 1
    True
    """
    ctx = _get_ctx(ctx)
    return [Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref()))]

def z3py.Product

(

args

)

Create the product of the Z3 expressions.

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

Definition at line 8767 of file z3py.py.

Referenced by BitVecs().

def 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
    """
    args = _get_args(args)
    if len(args) == 0:
        return 1
    ctx = _ctx_from_ast_arg_list(args)
    if ctx is None:
        return _reduce(lambda a, b: a * b, args, 1)
    args = _coerce_expr_list(args, ctx)
    if is_bv(args[0]):
        return _reduce(lambda a, b: a * b, args, 1)
    else:
        _args, sz = _to_ast_array(args)
        return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)

def z3py.prove	(		claim,
			show = False,
			keywords
	)

Try to prove the given claim.

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

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

Definition at line 8950 of file z3py.py.

Referenced by Default(), Map(), Store(), and Update().

def 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
    """
    if z3_debug():
        _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
    s = Solver()
    s.set(**keywords)
    s.add(Not(claim))
    if show:
        print(s)
    r = s.check()
    if r == unsat:
        print("proved")
    elif r == unknown:
        print("failed to prove")
        print(s.model())
    else:
        print("counterexample")
        print(s.model())

def z3py.Q	(		a,
			b,
			ctx = None
	)

Return a Z3 rational a/b.

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

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

Definition at line 3199 of file z3py.py.

Referenced by RatNumRef.as_string(), RatNumRef.denominator(), and RatNumRef.numerator().

def 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
    """
    return simplify(RatVal(a, b, ctx=ctx))

def z3py.Range	(		lo,
			hi,
			ctx = None
	)

Create the range regular expression over two sequences of length 1
>>> range = Range("a","z")
>>> print(simplify(InRe("b", range)))
True
>>> print(simplify(InRe("bb", range)))
False

Definition at line 11056 of file z3py.py.

def 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
    """
    lo = _coerce_seq(lo, ctx)
    hi = _coerce_seq(hi, ctx)
    return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)

def z3py.RatVal	(		a,
			b,
			ctx = None
	)

Return a Z3 rational a/b.

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

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

Definition at line 3183 of file z3py.py.

Referenced by Q().

def 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
    """
    if z3_debug():
        _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
        _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
    return simplify(RealVal(a, ctx) / RealVal(b, ctx))

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

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

def Re(s, ctx=None):
    """The regular expression that accepts sequence 's'
    >>> s1 = Re("ab")
    >>> s2 = Re(StringVal("ab"))
    >>> s3 = Re(Unit(BoolVal(True)))
    """
    s = _coerce_seq(s, ctx)
    return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx)


# Regular expressions

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

Referenced by ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_is_int(), is_rational_value(), ArithSortRef.is_real(), ArithRef.is_real(), is_real(), is_to_int(), IsInt(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().

def 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
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)

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

Referenced by is_div().

def 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
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [Real(name, ctx) for name in names]

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

Referenced by ArithSortRef.cast(), FreshReal(), is_arith_sort(), Real(), RealVar(), and QuantifierRef.var_sort().

def 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
    """
    ctx = _get_ctx(ctx)
    return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)

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

Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), fpRealToFP(), fpToFP(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), RatNumRef.numerator_as_long(), and RatVal().

def 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
    """
    ctx = _get_ctx(ctx)
    return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)

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

Referenced by RealVarVector().

def 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)
    """
    return Var(idx, RealSort(ctx))

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

def 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)
    """
    return [RealVar(i, ctx) for i in range(n)]

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

def 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
    """
    ctx = _get_ctx(ctx)
    return [Real("%s__%s" % (prefix, i), ctx) for i in range(sz)]

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

def 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
    """
    if is_app(args):
        args = [args]
    ctx = body.ctx
    args = _get_args(args)
    n = len(args)
    _args = (Ast * n)()
    for i in range(n):
        _args[i] = args[i].ast
    Z3_add_rec_def(ctx.ref(), f.ast, n, _args, body.ast)

def z3py.RecFunction	(		name,
			sig
	)

Create a new Z3 recursive with the given sorts.

Definition at line 908 of file z3py.py.

def RecFunction(name, *sig):
    """Create a new Z3 recursive with the given sorts."""
    sig = _get_args(sig)
    if z3_debug():
        _z3_assert(len(sig) > 0, "At least two arguments expected")
    arity = len(sig) - 1
    rng = sig[arity]
    if z3_debug():
        _z3_assert(is_sort(rng), "Z3 sort expected")
    dom = (Sort * arity)()
    for i in range(arity):
        if z3_debug():
            _z3_assert(is_sort(sig[i]), "Z3 sort expected")
        dom[i] = sig[i].ast
    ctx = rng.ctx
    return FuncDeclRef(Z3_mk_rec_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)

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

def 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]]
    """
    t = _to_tactic(t, ctx)
    return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)

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

def 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
    """
    if z3_debug():
        _z3_assert(_is_int(n), "First argument must be an integer")
        _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
    return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)

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

def Replace(s, src, dst):
    """Replace the first occurrence of 'src' by 'dst' in 's'
    >>> r = Replace("aaa", "a", "b")
    >>> simplify(r)
    "baa"
    """
    ctx = _get_ctx2(dst, s)
    if ctx is None and is_expr(src):
        ctx = src.ctx
    src = _coerce_seq(src, ctx)
    dst = _coerce_seq(dst, ctx)
    s = _coerce_seq(s, ctx)
    return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)

def z3py.reset_params

(

)

Reset all global (or module) parameters.

Definition at line 294 of file z3py.py.

def reset_params():
    """Reset all global (or module) parameters.
    """
    Z3_global_param_reset_all()

def z3py.ReSort

(

s

)

Definition at line 10927 of file z3py.py.

Referenced by Empty(), and Full().

def ReSort(s):
    if is_ast(s):
        return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx)
    if s is None or isinstance(s, Context):
        ctx = _get_ctx(s)
        return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx)
    raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument")

def z3py.RNA

(

ctx = None

)

Definition at line 9518 of file z3py.py.

Referenced by get_default_rounding_mode().

def RNA(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)

def z3py.RNE

(

ctx = None

)

Definition at line 9508 of file z3py.py.

Referenced by fpAbs(), fpAdd(), fpDiv(), fpFPToFP(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRealToFP(), FPs(), fpSignedToFP(), fpSub(), fpToFP(), fpUnsignedToFP(), get_default_rounding_mode(), is_fprm(), and is_fprm_sort().

def RNE(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)

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

def 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
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

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

def 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
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.RoundNearestTiesToAway

(

ctx = None

)

Definition at line 9513 of file z3py.py.

def RoundNearestTiesToAway(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)

def z3py.RoundNearestTiesToEven

(

ctx = None

)

Definition at line 9503 of file z3py.py.

def RoundNearestTiesToEven(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)

def z3py.RoundTowardNegative

(

ctx = None

)

Definition at line 9533 of file z3py.py.

def RoundTowardNegative(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)

def z3py.RoundTowardPositive

(

ctx = None

)

Definition at line 9523 of file z3py.py.

def RoundTowardPositive(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)

def z3py.RoundTowardZero

(

ctx = None

)

Definition at line 9543 of file z3py.py.

def RoundTowardZero(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)

def z3py.RTN

(

ctx = None

)

Definition at line 9538 of file z3py.py.

Referenced by get_default_rounding_mode().

def RTN(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)

def z3py.RTP

(

ctx = None

)

Definition at line 9528 of file z3py.py.

Referenced by get_default_rounding_mode().

def RTP(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)

def z3py.RTZ

(

ctx = None

)

Definition at line 9548 of file z3py.py.

Referenced by fpAdd(), fpToSBV(), fpToUBV(), and get_default_rounding_mode().

def RTZ(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)

def z3py.Select	(		a,
			i
	)

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

def Select(a, i):
    """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
    """
    if z3_debug():
        _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
    return a[i]

def z3py.SeqSort

(

s

)

Create a sequence sort over elements provided in the argument
>>> s = SeqSort(IntSort())
>>> s == Unit(IntVal(1)).sort()
True

Definition at line 10603 of file z3py.py.

Referenced by Empty(), Full(), and SeqSortRef.is_string().

def SeqSort(s):
    """Create a sequence sort over elements provided in the argument
    >>> s = SeqSort(IntSort())
    >>> s == Unit(IntVal(1)).sort()
    True
    """
    return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)

def z3py.set_default_fp_sort	(		ebits,
			sbits,
			ctx = None
	)

Definition at line 9164 of file z3py.py.

def set_default_fp_sort(ebits, sbits, ctx=None):
    global _dflt_fpsort_ebits
    global _dflt_fpsort_sbits
    _dflt_fpsort_ebits = ebits
    _dflt_fpsort_sbits = sbits

def z3py.set_default_rounding_mode	(		rm,
			ctx = None
	)

Definition at line 9151 of file z3py.py.

def set_default_rounding_mode(rm, ctx=None):
    global _dflt_rounding_mode
    if is_fprm_value(rm):
        _dflt_rounding_mode = rm.decl().kind()
    else:
        _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode")
        _dflt_rounding_mode = rm

def z3py.set_option	(		args,
			kws
	)

Alias for 'set_param' for backward compatibility.

Definition at line 300 of file z3py.py.

def set_option(*args, **kws):
    """Alias for 'set_param' for backward compatibility.
    """
    return set_param(*args, **kws)

def z3py.set_param	(		args,
			kws
	)

Set Z3 global (or module) parameters.

>>> set_param(precision=10)

Definition at line 270 of file z3py.py.

Referenced by set_option().

def set_param(*args, **kws):
    """Set Z3 global (or module) parameters.

    >>> set_param(precision=10)
    """
    if z3_debug():
        _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
    new_kws = {}
    for k in kws:
        v = kws[k]
        if not set_pp_option(k, v):
            new_kws[k] = v
    for key in new_kws:
        value = new_kws[key]
        Z3_global_param_set(str(key).upper(), _to_param_value(value))
    prev = None
    for a in args:
        if prev is None:
            prev = a
        else:
            Z3_global_param_set(str(prev), _to_param_value(a))
            prev = None

def z3py.SetAdd	(		s,
			e
	)

Add element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetAdd(a, 1)
Store(a, 1, True)

Definition at line 4902 of file z3py.py.

def SetAdd(s, e):
    """ Add element e to set s
    >>> a = Const('a', SetSort(IntSort()))
    >>> SetAdd(a, 1)
    Store(a, 1, True)
    """
    ctx = _ctx_from_ast_arg_list([s, e])
    e = _py2expr(e, ctx)
    return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx)

def z3py.SetComplement

(

s

)

The complement of set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
complement(a)

Definition at line 4924 of file z3py.py.

def SetComplement(s):
    """ The complement of set s
    >>> a = Const('a', SetSort(IntSort()))
    >>> SetComplement(a)
    complement(a)
    """
    ctx = s.ctx
    return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx)

def z3py.SetDel	(		s,
			e
	)

Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)

Definition at line 4913 of file z3py.py.

def SetDel(s, e):
    """ Remove element e to set s
    >>> a = Const('a', SetSort(IntSort()))
    >>> SetDel(a, 1)
    Store(a, 1, False)
    """
    ctx = _ctx_from_ast_arg_list([s, e])
    e = _py2expr(e, ctx)
    return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx)

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

def 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)
    """
    ctx = _ctx_from_ast_arg_list([a, b])
    return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.SetHasSize	(		a,
			k
	)

Definition at line 4816 of file z3py.py.

def SetHasSize(a, k):
    ctx = a.ctx
    k = _py2expr(k, ctx)
    return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx)

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

def SetIntersect(*args):
    """ Take the union of sets
    >>> a = Const('a', SetSort(IntSort()))
    >>> b = Const('b', SetSort(IntSort()))
    >>> SetIntersect(a, b)
    intersection(a, b)
    """
    args = _get_args(args)
    ctx = _ctx_from_ast_arg_list(args)
    _args, sz = _to_ast_array(args)
    return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx)

def z3py.SetSort

(

s

)

Sets.

Create a set sort over element sort s

Definition at line 4853 of file z3py.py.

Referenced by Ext(), IsMember(), IsSubset(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().

def SetSort(s):
    """ Create a set sort over element sort s"""
    return ArraySort(s, BoolSort())

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

def SetUnion(*args):
    """ Take the union of sets
    >>> a = Const('a', SetSort(IntSort()))
    >>> b = Const('b', SetSort(IntSort()))
    >>> SetUnion(a, b)
    union(a, b)
    """
    args = _get_args(args)
    ctx = _ctx_from_ast_arg_list(args)
    _args, sz = _to_ast_array(args)
    return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx)

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

def 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
    """
    if z3_debug():
        _z3_assert(_is_int(n), "First argument must be an integer")
        _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
    return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)

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

Referenced by Solver.reason_unknown(), and Solver.statistics().

def 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
    """
    ctx = _get_ctx(ctx)
    return Solver(Z3_mk_simple_solver(ctx.ref()), ctx, logFile)

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

Referenced by BitVecRef.__invert__(), BitVecRef.__lshift__(), ArithRef.__mod__(), ArithRef.__neg__(), BitVecRef.__neg__(), ArithRef.__pow__(), ArithRef.__rpow__(), BitVecRef.__rshift__(), AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), BitVecs(), Concat(), Contains(), CreateDatatypes(), Extract(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), IndexOf(), InRe(), is_algebraic_value(), K(), Length(), Loop(), LShR(), Not(), Option(), Plus(), PrefixOf(), Q(), Range(), RatVal(), DatatypeSortRef.recognizer(), RepeatBitVec(), Replace(), RotateLeft(), RotateRight(), SignExt(), Star(), StrToInt(), SuffixOf(), Union(), Xor(), and ZeroExt().

def simplify(a, *arguments, **keywords):
    """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)))
    """
    if z3_debug():
        _z3_assert(is_expr(a), "Z3 expression expected")
    if len(arguments) > 0 or len(keywords) > 0:
        p = args2params(arguments, keywords, a.ctx)
        return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
    else:
        return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)

def z3py.simplify_param_descrs

(

)

Return the set of parameter descriptions for Z3 `simplify` procedure.

Definition at line 8686 of file z3py.py.

def simplify_param_descrs():
    """Return the set of parameter descriptions for Z3 `simplify` procedure."""
    return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())

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

Referenced by BV2Int(), and IsInt().

def 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]
    """
    show = keywords.pop("show", False)
    s = Solver()
    s.set(**keywords)
    s.add(*args)
    if show:
        print(s)
    r = s.check()
    if r == unsat:
        print("no solution")
    elif r == unknown:
        print("failed to solve")
        try:
            print(s.model())
        except Z3Exception:
            return
    else:
        print(s.model())

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

def 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.
    """
    show = keywords.pop("show", False)
    if z3_debug():
        _z3_assert(isinstance(s, Solver), "Solver object expected")
    s.set(**keywords)
    s.add(*args)
    if show:
        print("Problem:")
        print(s)
    r = s.check()
    if r == unsat:
        print("no solution")
    elif r == unknown:
        print("failed to solve")
        try:
            print(s.model())
        except Z3Exception:
            return
    else:
        if show:
            print("Solution:")
        print(s.model())

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

def 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]
    """
    ctx = _get_ctx(ctx)
    logic = to_symbol(logic)
    return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx, logFile)

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

Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), and is_algebraic_value().

def Sqrt(a, ctx=None):
    """ Return a Z3 expression which represents the square root of a.

    >>> x = Real('x')
    >>> Sqrt(x)
    x**(1/2)
    """
    if not is_expr(a):
        ctx = _get_ctx(ctx)
        a = RealVal(a, ctx)
    return a ** "1/2"

def z3py.SRem	(		a,
			b
	)

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

Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and URem().

def SRem(a, b):
    """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)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.Star

(

re

)

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

def Star(re):
    """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
    """
    return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)

def z3py.Store	(		a,
			i,
			v
	)

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

Referenced by is_array(), is_store(), SetAdd(), and SetDel().

def Store(a, i, v):
    """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
    """
    return Update(a, i, v)

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

def String(name, ctx=None):
    """Return a string constant named `name`. If `ctx=None`, then the global context is used.

    >>> x = String('x')
    """
    ctx = _get_ctx(ctx)
    return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)

def z3py.Strings	(		names,
			ctx = None
	)

Return a tuple of String constants. 

Definition at line 10725 of file z3py.py.

Referenced by Contains().

def Strings(names, ctx=None):
    """Return a tuple of String constants. """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [String(name, ctx) for name in names]

def z3py.StringSort

(

ctx = None

)

Create a string sort
>>> s = StringSort()
>>> print(s)
String

Definition at line 10584 of file z3py.py.

Referenced by DisjointSum(), Empty(), Full(), SeqSortRef.is_string(), String(), and TupleSort().

def StringSort(ctx=None):
    """Create a string sort
    >>> s = StringSort()
    >>> print(s)
    String
    """
    ctx = _get_ctx(ctx)
    return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)

def z3py.StringVal	(		s,
			ctx = None
	)

create a string expression

Definition at line 10709 of file z3py.py.

Referenced by ExprRef.children(), Empty(), Extract(), is_seq(), is_string(), is_string_value(), Length(), and Re().

def StringVal(s, ctx=None):
    """create a string expression"""
    s = "".join(str(ch) if 32 <= ord(ch) and ord(ch) < 127 else "\\u{%x}" % (ord(ch)) for ch in s)
    ctx = _get_ctx(ctx)
    return SeqRef(Z3_mk_string(ctx.ref(), s), ctx)

def z3py.StrToInt

(

s

)

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

def StrToInt(s):
    """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
    """
    s = _coerce_seq(s)
    return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx)

def z3py.SubSeq	(		s,
			offset,
			length
	)

Extract substring or subsequence starting at offset

Definition at line 10738 of file z3py.py.

def SubSeq(s, offset, length):
    """Extract substring or subsequence starting at offset"""
    return Extract(s, offset, length)

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

def 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
    """
    if isinstance(m, tuple):
        m1 = _get_args(m)
        if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1):
            m = m1
    if z3_debug():
        _z3_assert(is_expr(t), "Z3 expression expected")
        _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(
            p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
    num = len(m)
    _from = (Ast * num)()
    _to = (Ast * num)()
    for i in range(num):
        _from[i] = m[i][0].as_ast()
        _to[i] = m[i][1].as_ast()
    return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)

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

def 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)
    """
    if z3_debug():
        _z3_assert(is_expr(t), "Z3 expression expected")
        _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
    num = len(m)
    _to = (Ast * num)()
    for i in range(num):
        _to[i] = m[i].as_ast()
    return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)

def z3py.SubString	(		s,
			offset,
			length
	)

Extract substring or subsequence starting at offset

Definition at line 10733 of file z3py.py.

def SubString(s, offset, length):
    """Extract substring or subsequence starting at offset"""
    return Extract(s, offset, length)

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

def 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
    """
    ctx = _get_ctx2(a, b)
    a = _coerce_seq(a, ctx)
    b = _coerce_seq(b, ctx)
    return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.Sum

(

args

)

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

Referenced by BitVecs(), Ints(), IntVector(), Reals(), and RealVector().

def Sum(*args):
    """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
    """
    args = _get_args(args)
    if len(args) == 0:
        return 0
    ctx = _ctx_from_ast_arg_list(args)
    if ctx is None:
        return _reduce(lambda a, b: a + b, args, 0)
    args = _coerce_expr_list(args, ctx)
    if is_bv(args[0]):
        return _reduce(lambda a, b: a + b, args, 0)
    else:
        _args, sz = _to_ast_array(args)
        return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)

def z3py.tactic_description	(		name,
			ctx = None
	)

Return a short description for the tactic named `name`.

>>> d = tactic_description('simplify')

Definition at line 8345 of file z3py.py.

Referenced by describe_tactics().

def tactic_description(name, ctx=None):
    """Return a short description for the tactic named `name`.

    >>> d = tactic_description('simplify')
    """
    ctx = _get_ctx(ctx)
    return Z3_tactic_get_descr(ctx.ref(), name)

def z3py.tactics

(

ctx = None

)

Return a list of all available tactics in Z3.

>>> l = tactics()
>>> l.count('simplify') == 1
True

Definition at line 8334 of file z3py.py.

Referenced by describe_tactics().

def tactics(ctx=None):
    """Return a list of all available tactics in Z3.

    >>> l = tactics()
    >>> l.count('simplify') == 1
    True
    """
    ctx = _get_ctx(ctx)
    return [Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref()))]

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

Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), Goal.convert_model(), Goal.depth(), Statistics.get_key_value(), and Statistics.keys().

def 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)
    """
    return AndThen(*ts, **ks)

def z3py.to_symbol	(		s,
			ctx = None
	)

Convert an integer or string into a Z3 symbol.

Definition at line 129 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DeclareSort(), EnumSort(), FiniteDomainSort(), FP(), Function(), Int(), prove(), Real(), RecFunction(), Fixedpoint.set_predicate_representation(), SolverFor(), String(), and Fixedpoint.update_rule().

def to_symbol(s, ctx=None):
    """Convert an integer or string into a Z3 symbol."""
    if _is_int(s):
        return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
    else:
        return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)

def z3py.ToInt

(

a

)

Return the Z3 expression ToInt(a).

>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int

Definition at line 3340 of file z3py.py.

Referenced by is_to_int().

def ToInt(a):
    """ Return the Z3 expression ToInt(a).

    >>> x = Real('x')
    >>> x.sort()
    Real
    >>> n = ToInt(x)
    >>> n
    ToInt(x)
    >>> n.sort()
    Int
    """
    if z3_debug():
        _z3_assert(a.is_real(), "Z3 real expression expected.")
    ctx = a.ctx
    return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)

def z3py.ToReal

(

a

)

Return the Z3 expression ToReal(a).

>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real

Definition at line 3322 of file z3py.py.

Referenced by ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), and is_to_real().

def ToReal(a):
    """ Return the Z3 expression ToReal(a).

    >>> x = Int('x')
    >>> x.sort()
    Int
    >>> n = ToReal(x)
    >>> n
    ToReal(x)
    >>> n.sort()
    Real
    """
    if z3_debug():
        _z3_assert(a.is_int(), "Z3 integer expression expected.")
    ctx = a.ctx
    return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)

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

def 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.
    """
    return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)

def z3py.TreeOrder	(		a,
			index
	)

Definition at line 11084 of file z3py.py.

def TreeOrder(a, index):
    return FuncDeclRef(Z3_mk_tree_order(a.ctx_ref(), a.ast, index), a.ctx)

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

def 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.
    """
    t = _to_tactic(t, ctx)
    return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)

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

def 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()])
    """
    tuple = Datatype(name, ctx)
    projects = [("project%d" % i, sorts[i]) for i in range(len(sorts))]
    tuple.declare(name, *projects)
    tuple = tuple.create()
    return tuple, tuple.constructor(0), [tuple.accessor(0, i) for i in range(len(sorts))]

def z3py.UDiv	(		a,
			b
	)

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

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

def UDiv(a, b):
    """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)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.UGE	(		a,
			b
	)

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

Referenced by BitVecRef.__ge__().

def UGE(a, b):
    """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)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.UGT	(		a,
			b
	)

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

Referenced by BitVecRef.__gt__().

def UGT(a, b):
    """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)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.ULE	(		a,
			b
	)

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

Referenced by BitVecRef.__le__().

def ULE(a, b):
    """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)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.ULT	(		a,
			b
	)

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

Referenced by BitVecRef.__lt__().

def ULT(a, b):
    """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)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

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

Referenced by InRe().

def Union(*args):
    """Create union of regular expressions.
    >>> re = Union(Re("a"), Re("b"), Re("c"))
    >>> print (simplify(InRe("d", re)))
    False
    """
    args = _get_args(args)
    sz = len(args)
    if z3_debug():
        _z3_assert(sz > 0, "At least one argument expected.")
        _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
    if sz == 1:
        return args[0]
    ctx = args[0].ctx
    v = (Ast * sz)()
    for i in range(sz):
        v[i] = args[i].as_ast()
    return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)

def z3py.Unit

(

a

)

Create a singleton sequence

Definition at line 10777 of file z3py.py.

Referenced by is_seq(), Re(), and SeqSort().

def Unit(a):
    """Create a singleton sequence"""
    return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)

def z3py.Update	(		a,
			i,
			v
	)

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

Referenced by Store().

def Update(a, i, v):
    """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
    """
    if z3_debug():
        _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
    i = a.sort().domain().cast(i)
    v = a.sort().range().cast(v)
    ctx = a.ctx
    return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)

def z3py.URem	(		a,
			b
	)

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

Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and SRem().

def URem(a, b):
    """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)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.user_prop_diseq	(		ctx,
			cb,
			x,
			y
	)

Definition at line 11182 of file z3py.py.

def user_prop_diseq(ctx, cb, x, y):
    prop = _prop_closures.get(ctx)
    prop.cb = cb
    prop.diseq(x, y)
    prop.cb = None

def z3py.user_prop_eq	(		ctx,
			cb,
			x,
			y
	)

Definition at line 11175 of file z3py.py.

def user_prop_eq(ctx, cb, x, y):
    prop = _prop_closures.get(ctx)
    prop.cb = cb
    prop.eq(x, y)
    prop.cb = None

def z3py.user_prop_final	(		ctx,
			cb
	)

Definition at line 11168 of file z3py.py.

def user_prop_final(ctx, cb):
    prop = _prop_closures.get(ctx)
    prop.cb = cb
    prop.final()
    prop.cb = None

def z3py.user_prop_fixed	(		ctx,
			cb,
			id,
			value
	)

Definition at line 11161 of file z3py.py.

def user_prop_fixed(ctx, cb, id, value):
    prop = _prop_closures.get(ctx)
    prop.cb = cb
    prop.fixed(id, _to_expr_ref(ctypes.c_void_p(value), prop.ctx()))
    prop.cb = None

def z3py.user_prop_fresh	(		id,
			ctx
	)

Definition at line 11153 of file z3py.py.

def user_prop_fresh(id, ctx):
    _prop_closures.set_threaded()
    prop = _prop_closures.get(id)
    new_prop = prop.fresh()
    _prop_closures.set(new_prop.id, new_prop)
    return ctypes.c_void_p(new_prop.id)

def z3py.user_prop_pop	(		ctx,
			num_scopes
	)

Definition at line 11149 of file z3py.py.

def user_prop_pop(ctx, num_scopes):
    _prop_closures.get(ctx).pop(num_scopes)

def z3py.user_prop_push

(

ctx

)

Definition at line 11145 of file z3py.py.

def user_prop_push(ctx):
    _prop_closures.get(ctx).push()

def z3py.Var	(		idx,
			s
	)

Create a Z3 free variable. Free variables are used to create quantified formulas.

>>> Var(0, IntSort())
Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort()))
False

Definition at line 1440 of file z3py.py.

Referenced by QuantifierRef.body(), QuantifierRef.children(), is_pattern(), MultiPattern(), QuantifierRef.pattern(), and RealVar().

def Var(idx, s):
    """Create a Z3 free variable. Free variables are used to create quantified formulas.

    >>> Var(0, IntSort())
    Var(0)
    >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
    False
    """
    if z3_debug():
        _z3_assert(is_sort(s), "Z3 sort expected")
    return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)

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

def 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]]
    """
    p = _to_probe(p, ctx)
    t = _to_tactic(t, ctx)
    return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)

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

Referenced by Goal.prec().

def 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]]
    """
    ctx = keys.pop("ctx", None)
    t = _to_tactic(t, ctx)
    p = args2params(args, keys, t.ctx)
    return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)

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

def 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]]
    """
    t = _to_tactic(t, None)
    return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)

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

def 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
    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
    s = BoolSort(ctx)
    a = s.cast(a)
    b = s.cast(b)
    return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.z3_debug

(

)

Definition at line 64 of file z3py.py.

Referenced by FuncDeclRef.__call__(), Probe.__call__(), Context.__init__(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), ExprRef.children(), Concat(), Const(), CreateDatatypes(), ExprRef.decl(), Default(), describe_probes(), Distinct(), FuncDeclRef.domain(), EnumSort(), AstRef.eq(), eq(), Ext(), Extract(), FiniteDomainVal(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), get_map_func(), get_var_index(), If(), Intersect(), is_sort(), IsInt(), K(), Map(), MultiPattern(), ExprRef.num_args(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), prove(), RatVal(), RecFunction(), RepeatBitVec(), Select(), set_param(), SignExt(), simplify(), solve_using(), substitute(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Union(), Update(), and Var().

def z3_debug():
    global Z3_DEBUG
    return Z3_DEBUG

def z3py.z3_error_handler	(		c,
			e
	)

Definition at line 179 of file z3py.py.

def z3_error_handler(c, e):
    # Do nothing error handler, just avoid exit(0)
    # The wrappers in z3core.py will raise a Z3Exception if an error is detected
    return

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

def 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
    """
    if z3_debug():
        _z3_assert(_is_int(n), "First argument must be an integer")
        _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
    return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)

Variable Documentation

int _dflt_fpsort_ebits = 11

Definition at line 9123 of file z3py.py.

int _dflt_fpsort_sbits = 53

Definition at line 9124 of file z3py.py.

_dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO

Floating-Point Arithmetic.

Definition at line 9122 of file z3py.py.

_main_ctx = None

Definition at line 235 of file z3py.py.

tuple _on_model_eh = on_model_eh_type(_global_on_model)

Definition at line 7748 of file z3py.py.

dictionary _on_models = {}

Definition at line 7740 of file z3py.py.

_prop_closures = None

Definition at line 11136 of file z3py.py.

tuple _ROUNDING_MODES

Initial value:

= frozenset({
    Z3_OP_FPA_RM_TOWARD_ZERO,
    Z3_OP_FPA_RM_TOWARD_NEGATIVE,
    Z3_OP_FPA_RM_TOWARD_POSITIVE,
    Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
    Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
})

Definition at line 9142 of file z3py.py.

tuple _user_prop_diseq = eq_eh_type(user_prop_diseq)

Definition at line 11195 of file z3py.py.

tuple _user_prop_eq = eq_eh_type(user_prop_eq)

Definition at line 11194 of file z3py.py.

tuple _user_prop_final = final_eh_type(user_prop_final)

Definition at line 11193 of file z3py.py.

tuple _user_prop_fixed = fixed_eh_type(user_prop_fixed)

Definition at line 11192 of file z3py.py.

tuple _user_prop_fresh = fresh_eh_type(user_prop_fresh)

Definition at line 11191 of file z3py.py.

tuple _user_prop_pop = pop_eh_type(user_prop_pop)

Definition at line 11190 of file z3py.py.

tuple _user_prop_push = push_eh_type(user_prop_push)

Definition at line 11189 of file z3py.py.

tuple sat = CheckSatResult(Z3_L_TRUE)

Definition at line 6793 of file z3py.py.

tuple unknown = CheckSatResult(Z3_L_UNDEF)

Definition at line 6795 of file z3py.py.

tuple unsat = CheckSatResult(Z3_L_FALSE)

Definition at line 6794 of file z3py.py.

Z3_DEBUG = __debug__

Definition at line 61 of file z3py.py.