z3py Namespace Reference

Data Structures
class	AlgebraicNumRef
class	ApplyResult
class	ArithRef
class	ArithSortRef
	Arithmetic. More...
class	ArrayRef
class	ArraySortRef
	Arrays. More...
class	AstMap
class	AstRef
class	AstVector
class	BitVecNumRef
class	BitVecRef
class	BitVecSortRef
	Bit-Vectors. More...
class	BoolRef
class	BoolSortRef
	Booleans. More...
class	CharRef
class	CharSortRef
class	CheckSatResult
class	Context
class	Datatype
class	DatatypeRef
class	DatatypeSortRef
class	ExprRef
	Expressions. More...
class	FiniteDomainNumRef
class	FiniteDomainRef
class	FiniteDomainSortRef
class	Fixedpoint
	Fixedpoint. More...
class	FPNumRef
class	FPRef
class	FPRMRef
class	FPRMSortRef
class	FPSortRef
class	FuncDeclRef
	Function Declarations. More...
class	FuncEntry
class	FuncInterp
class	Goal
class	IntNumRef
class	ModelRef
class	OnClause
class	Optimize
class	OptimizeObjective
	Optimize. More...
class	ParamDescrsRef
class	ParamsRef
	Parameter Sets. More...
class	ParserContext
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	Simplifier
class	Solver
class	SortRef
class	Statistics
	Statistics. More...
class	Tactic
class	TypeVarRef
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
def	eq
def	is_sort
def	DeclareSort
def	DeclareTypeVar
def	is_func_decl (a)
def	Function (name, sig)
def	FreshFunction (sig)
def	RecFunction (name, sig)
def	RecAddDefinition (f, args, body)
def	deserialize (st)
def	is_expr (a)
def	is_app (a)
def	is_const (a)
def	is_var (a)
def	get_var_index (a)
def	is_app_of (a, k)
def	If
def	Distinct (args)
def	Const (name, sort)
def	Consts (names, sort)
def	FreshConst
def	Var
def	RealVar
def	RealVarVector
def	is_bool
def	is_true
def	is_false
def	is_and
def	is_or
def	is_implies
def	is_not
def	is_eq
def	is_distinct
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
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
def	is_mul
def	is_sub
def	is_div
def	is_idiv
def	is_mod
def	is_le
def	is_lt
def	is_ge
def	is_gt
def	is_is_int
def	is_to_real
def	is_to_int
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
def	is_const_array (a)
def	is_K (a)
def	is_map (a)
def	is_default (a)
def	get_map_func (a)
def	ArraySort (sig)
def	Array (name, sorts)
def	Update (a, args)
def	Default (a)
def	Store (a, args)
def	Select (a, args)
def	Map (f, args)
def	K (dom, v)
def	Ext (a, b)
def	SetHasSize (a, k)
def	is_select (a)
def	is_store (a)
def	SetSort (s)
	Sets. More...
def	EmptySet (s)
def	FullSet (s)
def	SetUnion (args)
def	SetIntersect (args)
def	SetAdd (s, e)
def	SetDel (s, e)
def	SetComplement (s)
def	SetDifference (a, b)
def	IsMember (e, s)
def	IsSubset (a, b)
def	CreateDatatypes (ds)
def	DatatypeSort
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	substitute_funs (t, m)
def	Sum (args)
def	Product (args)
def	Abs (arg)
def	AtMost (args)
def	AtLeast (args)
def	PbLe (args, k)
def	PbGe (args, k)
def	PbEq
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	CharVal
def	CharFromBv (bv)
def	CharToBv
def	CharToInt
def	CharIsDigit
def	is_seq (a)
def	is_string
def	is_string_value
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	SeqMap (f, s)
def	SeqMapI (f, i, s)
def	SeqFoldLeft (f, a, s)
def	SeqFoldLeftI (f, i, a, s)
def	StrToInt (s)
def	IntToStr (s)
def	StrToCode (s)
def	StrFromCode (c)
def	Re
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	Diff
def	AllChar
def	PartialOrder (a, index)
def	LinearOrder (a, index)
def	TreeOrder (a, index)
def	PiecewiseLinearOrder (a, index)
def	TransitiveClosure (f)
def	to_Ast (ptr)
def	to_ContextObj (ptr)
def	to_AstVectorObj (ptr)
def	on_clause_eh (ctx, p, n, dep, clause)
def	ensure_prop_closures ()
def	user_prop_push (ctx, cb)
def	user_prop_pop (ctx, cb, num_scopes)
def	user_prop_fresh (ctx, _new_ctx)
def	user_prop_fixed (ctx, cb, id, value)
def	user_prop_created (ctx, cb, id)
def	user_prop_final (ctx, cb)
def	user_prop_eq (ctx, cb, x, y)
def	user_prop_diseq (ctx, cb, x, y)
def	user_prop_decide (ctx, cb, t_ref, idx, phase)
def	PropagateFunction (name, sig)

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_NEAREST_TIES_TO_EVEN
	Floating-Point Arithmetic. More...
int	_dflt_fpsort_ebits = 11
int	_dflt_fpsort_sbits = 53
tuple	_ROUNDING_MODES
	_my_hacky_class = None
tuple	_on_clause_eh = Z3_on_clause_eh(on_clause_eh)
	_prop_closures = None
tuple	_user_prop_push = Z3_push_eh(user_prop_push)
tuple	_user_prop_pop = Z3_pop_eh(user_prop_pop)
tuple	_user_prop_fresh = Z3_fresh_eh(user_prop_fresh)
tuple	_user_prop_fixed = Z3_fixed_eh(user_prop_fixed)
tuple	_user_prop_created = Z3_created_eh(user_prop_created)
tuple	_user_prop_final = Z3_final_eh(user_prop_final)
tuple	_user_prop_eq = Z3_eq_eh(user_prop_eq)
tuple	_user_prop_diseq = Z3_eq_eh(user_prop_diseq)
tuple	_user_prop_decide = Z3_decide_eh(user_prop_decide)

Function Documentation

def z3py.Abs

(

arg

)

Create the absolute value of an arithmetic expression

Definition at line 9162 of file z3py.py.

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

def z3py.AllChar	(		regex_sort,
			ctx = None
	)

Create a regular expression that accepts all single character strings

Definition at line 11581 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 1920 of file z3py.py.

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

Referenced by Tactic.apply(), Fixedpoint.set(), Optimize.set(), simplify(), Simplifier.using_params(), 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,
			sorts
	)

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

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

Definition at line 4823 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, *sorts):
    """Return an array constant named `name` with the given domain and range sorts.

    >>> a = Array('a', IntSort(), IntSort())
    >>> a.sort()
    Array(Int, Int)
    >>> a[0]
    a[0]
    """
    s = ArraySort(sorts)
    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 4790 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-least Pseudo-Boolean k constraint.

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

Definition at line 9185 of file z3py.py.

def AtLeast(*args):
    """Create an at-least 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 9167 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 4127 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 4151 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 4095 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 4110 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 1799 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 1811 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 1762 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 1780 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 1827 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 4063 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 4549 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 4556 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 4591 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 4598 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 4535 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 4542 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 4577 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 4584 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 4563 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 4570 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 3509 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.CharFromBv

(

bv

)

Definition at line 11099 of file z3py.py.

def CharFromBv(bv):
    if not is_expr(bv):
        raise Z3Exception("Bit-vector expression needed")
    return _to_expr_ref(Z3_mk_char_from_bv(bv.ctx_ref(), bv.as_ast()), bv.ctx)

def z3py.CharIsDigit	(		ch,
			ctx = None
	)

Definition at line 11112 of file z3py.py.

def CharIsDigit(ch, ctx=None):
    ch = _coerce_char(ch, ctx)
    return ch.is_digit()

def z3py.CharSort

(

ctx = None

)

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

Definition at line 10995 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.CharToBv	(		ch,
			ctx = None
	)

Definition at line 11104 of file z3py.py.

def CharToBv(ch, ctx=None):
    ch = _coerce_char(ch, ctx)
    return ch.to_bv()

def z3py.CharToInt	(		ch,
			ctx = None
	)

Definition at line 11108 of file z3py.py.

def CharToInt(ch, ctx=None):
    ch = _coerce_char(ch, ctx)
    return ch.to_int()

def z3py.CharVal	(		ch,
			ctx = None
	)

Definition at line 11091 of file z3py.py.

def CharVal(ch, ctx=None):
    ctx = _get_ctx(ctx)
    if isinstance(ch, str):
        ch = ord(ch)
    if not isinstance(ch, int):
        raise Z3Exception("character value should be an ordinal")
    return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
    

def z3py.Complement

(

re

)

Create the complement regular expression.

Definition at line 11523 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 4172 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 8984 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 1480 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 1492 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 11268 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 5248 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.DatatypeSort	(		name,
			ctx = None
	)

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

Definition at line 5448 of file z3py.py.

def DatatypeSort(name, ctx = None):
    """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
    ctx = _get_ctx(ctx)
    return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)

def z3py.DeclareSort	(		name,
			ctx = None,
			SortRef
	)

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

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

def DeclareSort(name, ctx= None) -> SortRef:
    """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.DeclareTypeVar	(		name,
			ctx = None
	)

Create a new type variable named `name`.

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

Definition at line 737 of file z3py.py.

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

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

    """
    ctx = _get_ctx(ctx)
    return TypeVarRef(Z3_mk_type_variable(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 4869 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 8905 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 8699 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.deserialize

(

st

)

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

Definition at line 1162 of file z3py.py.

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

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

Create the difference regular expression

Definition at line 11573 of file z3py.py.

def Diff(a, b, ctx=None):
    """Create the difference regular expression
    """
    if z3_debug():
        _z3_assert(is_expr(a), "expression expected")
        _z3_assert(is_expr(b), "expression expected")
    return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)

def z3py.disable_trace

(

msg

)

Definition at line 87 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 5465 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 1447 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 11198 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 5012 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 83 of file z3py.py.

def enable_trace(msg):
    Z3_enable_trace(msg)

def z3py.ensure_prop_closures

(

)

Definition at line 11692 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 5477 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]), "Enumeration 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], ctx)
    _values = (FuncDecl * num)()
    _testers = (FuncDecl * num)()
    name = to_symbol(name, ctx)
    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

)

Definition at line 486 of file z3py.py.

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

def eq(a : AstRef, b : AstRef) -> bool:
    """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 2321 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 4958 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) or b.is_lambda()), "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 4218 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 8942 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 7873 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 7943 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 9670 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 9634 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 9646 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 9658 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 9664 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 9640 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 9676 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 9652 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 2303 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 10312 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 10355 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)
x + y
>>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
fpAdd(RTZ(), x, y)
>>> fpAdd(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10446 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)
    x + y
    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
    fpAdd(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 10768 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)
x / y
>>> fpDiv(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10493 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)
    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 10676 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 10552 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 10700 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 10785 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 10664 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 10652 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 10240 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 10582 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 10570 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 10611 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 10599 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 10617 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 10605 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 10593 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 10640 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 10628 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 10537 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 10522 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 10234 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 10253 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)
x * y
>>> fpMul(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10478 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)
    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 10200 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 10378 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 10688 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 10217 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 10247 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 10805 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 10508 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 10564 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)
(x + y) * z

Definition at line 10336 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)
    (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 10823 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 10141 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 10558 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)
x - y
>>> fpSub(rm, x, y).sort()
FPSort(8, 24)

Definition at line 10463 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)
    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 10729 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 10859 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 10933 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 10913 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 10869 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 10891 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 10841 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 10266 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 10259 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 1842 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 1507 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 922 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 3370 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 3427 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 11218 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 5021 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 899 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 6816 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,
			Context
	)

Definition at line 277 of file z3py.py.

def get_ctx(ctx) -> Context:
    return _get_ctx(ctx)

def z3py.get_default_fp_sort

(

ctx = None

)

Definition at line 9553 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 9520 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 109 of file z3py.py.

def get_full_version():
    return Z3_get_full_version()

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 4766 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 317 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 1378 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 100 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 91 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 9026 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 1424 of file z3py.py.

Referenced by BoolRef.__add__(), BoolRef.__mul__(), Abs(), 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 1856 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 11302 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 11441 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 3331 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 4086 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 11475 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 3344 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 3225 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 11383 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 3271 of file z3py.py.

Referenced by AstMap.__len__(), ArithRef.__mod__(), BoolRef.__mul__(), 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 3357 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

)

Definition at line 2873 of file z3py.py.

def is_add(a : Any) -> bool:
    """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 2859 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

)

Definition at line 1692 of file z3py.py.

def is_and(a : Any) -> bool:
    """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 1308 of file z3py.py.

Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), ExprRef.kind(), 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 1411 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.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 2746 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

)

Definition at line 2445 of file z3py.py.

def is_arith_sort(s : Any) -> bool:
    """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

)

Definition at line 4701 of file z3py.py.

Referenced by Ext().

def is_array(a : Any) -> bool:
    """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 4697 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 6811 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

)

Definition at line 465 of file z3py.py.

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

def is_ast(a : Any) -> bool:
    """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

)

Definition at line 1642 of file z3py.py.

Referenced by BoolSort(), and prove().

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

    >>> p = Bool('p')
    >>> is_bool(p)
    True
    >>> q = Bool('q')
    >>> is_bool(And(p, q))
    True
    >>> x = Real('x')
    >>> is_bool(x)
    False
    >>> is_bool(x == 0)
    True
    """
    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 4034 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 3561 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 4048 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 1334 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 4715 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 4757 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

)

Definition at line 1750 of file z3py.py.

def is_distinct(a : Any) -> bool:
    """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

)

Definition at line 2909 of file z3py.py.

def is_div(a : Any) -> bool:
    """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

)

Definition at line 1740 of file z3py.py.

Referenced by AstRef.__bool__().

def is_eq(a : Any) -> bool:
    """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 1285 of file z3py.py.

Referenced by SortRef.cast(), BoolSortRef.cast(), Cbrt(), CharFromBv(), Concat(), deserialize(), Diff(), IndexOf(), IntToStr(), is_var(), simplify(), substitute(), substitute_funs(), 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

)

Definition at line 1678 of file z3py.py.

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

def is_false(a : Any) -> bool:
    """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 7904 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 7881 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 7958 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 10112 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 9686 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 10126 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 9946 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 9697 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 9959 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 886 of file z3py.py.

Referenced by prove(), and substitute_funs().

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

)

Definition at line 2974 of file z3py.py.

def is_ge(a : Any) -> bool:
    """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

)

Definition at line 2986 of file z3py.py.

def is_gt(a : Any) -> bool:
    """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

)

Definition at line 2926 of file z3py.py.

Referenced by is_div().

def is_idiv(a : Any) -> bool:
    """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

)

Definition at line 1716 of file z3py.py.

def is_implies(a : Any) -> bool:
    """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,
			bool
	)

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

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

def is_int(a) -> bool:
    """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 2813 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

)

Definition at line 2998 of file z3py.py.

def is_is_int(a : Any) -> bool:
    """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 4728 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

)

Definition at line 2950 of file z3py.py.

def is_le(a : Any) -> bool:
    """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

)

Definition at line 2962 of file z3py.py.

def is_lt(a : Any) -> bool:
    """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 4741 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

)

Definition at line 2938 of file z3py.py.

def is_mod(a : Any) -> bool:
    """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

)

Definition at line 2885 of file z3py.py.

def is_mul(a : Any) -> bool:
    """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

)

Definition at line 1728 of file z3py.py.

def is_not(a : Any) -> bool:
    """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

)

Definition at line 1704 of file z3py.py.

def is_or(a : Any) -> bool:
    """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 2004 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 8867 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 2254 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 2837 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 11437 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 2786 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 4976 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 11137 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

)

Definition at line 661 of file z3py.py.

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

def is_sort(s : Any) -> bool:
    """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 4989 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

)

Definition at line 11147 of file z3py.py.

def is_string(a: Any) -> bool:
    """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

)

Definition at line 11155 of file z3py.py.

def is_string_value(a: Any) -> bool:
    """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

)

Definition at line 2897 of file z3py.py.

def is_sub(a : Any) -> bool:
    """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

)

Definition at line 3025 of file z3py.py.

def is_to_int(a : Any) -> bool:
    """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

)

Definition at line 3010 of file z3py.py.

def is_to_real(a : Any) -> bool:
    """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

)

Definition at line 1660 of file z3py.py.

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

def is_true(a : Any) -> bool:
    """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 1353 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 3479 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 5099 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 5110 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 4936 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 2342 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 11322 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 11331 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 11593 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 11543 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
    """
    if z3_debug():
        _z3_assert(is_expr(re), "expression expected")
    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 4389 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

(

Context

)

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

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

def main_ctx() -> Context:
    """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 4913 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 1905 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,
			eval = {}
	)

Definition at line 6803 of file z3py.py.

Referenced by Optimize.set_on_model().

def Model(ctx=None, eval = {}):
    ctx = _get_ctx(ctx)
    mdl = ModelRef(Z3_mk_model(ctx.ref()), ctx)
    for k, v in eval.items():
        mdl.update_value(k, v)
    return mdl

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

Referenced by BoolRef.__invert__(), 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.on_clause_eh	(		ctx,
			p,
			n,
			dep,
			clause
	)

Definition at line 11633 of file z3py.py.

Referenced by on_clause.on_clause().

def on_clause_eh(ctx, p, n, dep, clause):
    onc = _my_hacky_class
    p = _to_expr_ref(to_Ast(p), onc.ctx)
    clause = AstVector(to_AstVectorObj(clause), onc.ctx)
    deps = [dep[i] for i in range(n)]
    onc.on_clause(p, deps, clause)
    

def z3py.open_log

(

fname

)

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

Definition at line 122 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 11508 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
    """
    if z3_debug():
        _z3_assert(is_expr(re), "expression expected")
    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 1953 of file z3py.py.

Referenced by BoolRef.__or__(), 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 8560 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 8616 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 8581 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 9496 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 9475 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 8600 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 11589 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 equality k constraint.

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

Definition at line 9252 of file z3py.py.

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

    >>> a, b, c = Bools('a b c')
    >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
    """
    _z3_check_cint_overflow(k, "k")
    ctx, sz, _args, _coeffs, args = _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 9241 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, args = _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 9230 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, args = _pb_args_coeffs(args)
    return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)

def z3py.PiecewiseLinearOrder	(		a,
			index
	)

Definition at line 11601 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 11493 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
    """
    if z3_debug():
        _z3_assert(is_expr(re), "expression expected")
    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 11238 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 8896 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 8885 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 9137 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.PropagateFunction	(		name,
			sig
	)

Create a function that gets tracked by user propagator.
   Every term headed by this function symbol is tracked.
   If a term is fixed and the fixed callback is registered a
   callback is invoked that the term headed by this function is fixed.

Definition at line 11787 of file z3py.py.

def PropagateFunction(name, *sig):
    """Create a function that gets tracked by user propagator.
       Every term headed by this function symbol is tracked.
       If a term is fixed and the fixed callback is registered a
       callback is invoked that the term headed by this function is fixed.
    """
    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_solver_propagate_declare(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), 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 9324 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 3318 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 11558 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)
    if z3_debug():
        _z3_assert(is_expr(lo), "expression expected")
        _z3_assert(is_expr(hi), "expression expected")
    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 3302 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 11402 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 3384 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 3397 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 3242 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 3283 of file z3py.py.

Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), deserialize(), 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

)

Definition at line 1528 of file z3py.py.

Referenced by RealVarVector().

def RealVar(idx: int, ctx=None) -> ExprRef:
    """
    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

)

Definition at line 1538 of file z3py.py.

def RealVarVector(n: int, 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 3412 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 963 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 945 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 8649 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 4511 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 11287 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

(

None

)

Reset all global (or module) parameters.

Definition at line 305 of file z3py.py.

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

def z3py.ReSort

(

s

)

Definition at line 11421 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 9911 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 9901 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 4421 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 4437 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 9906 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 9896 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 9926 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 9916 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 9936 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 9931 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 9921 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 9941 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,
			args
	)

Return a Z3 select array expression.

>>> a = Array('a', IntSort(), IntSort())
>>> i = Int('i')
>>> Select(a, i)
a[i]
>>> eq(Select(a, i), a[i])
True

Definition at line 4897 of file z3py.py.

def Select(a, *args):
    """Return a Z3 select array expression.

    >>> a = Array('a', IntSort(), IntSort())
    >>> i = Int('i')
    >>> Select(a, i)
    a[i]
    >>> eq(Select(a, i), a[i])
    True
    """
    args = _get_args(args)
    if z3_debug():
        _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
    return a[args]

def z3py.SeqFoldLeft	(		f,
			a,
			s
	)

Definition at line 11354 of file z3py.py.

def SeqFoldLeft(f, a, s):
    ctx = _get_ctx2(f, s)
    s = _coerce_seq(s, ctx)
    a = _py2expr(a)
    return _to_expr_ref(Z3_mk_seq_foldl(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx)

def z3py.SeqFoldLeftI	(		f,
			i,
			a,
			s
	)

Definition at line 11360 of file z3py.py.

def SeqFoldLeftI(f, i, a, s):
    ctx = _get_ctx2(f, s)
    s = _coerce_seq(s, ctx)
    a = _py2expr(a)
    i = _py2expr(i)
    return _to_expr_ref(Z3_mk_seq_foldli(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx)

def z3py.SeqMap	(		f,
			s
	)

Map function 'f' over sequence 's'

Definition at line 11340 of file z3py.py.

def SeqMap(f, s):
    """Map function 'f' over sequence 's'"""
    ctx = _get_ctx2(f, s)
    s = _coerce_seq(s, ctx)
    return _to_expr_ref(Z3_mk_seq_map(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx)

def z3py.SeqMapI	(		f,
			i,
			s
	)

Map function 'f' over sequence 's' at index 'i'

Definition at line 11346 of file z3py.py.

def SeqMapI(f, i, s):
    """Map function 'f' over sequence 's' at index 'i'"""
    ctx = _get_ctx2(f, s)
    s = _coerce_seq(s, ctx)
    if not is_expr(i):
        i = _py2expr(i)
    return _to_expr_ref(Z3_mk_seq_mapi(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx)

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 11005 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 9557 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 9544 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.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 311 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 281 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 5056 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 5078 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 5067 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 5088 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 4970 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 5043 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 5007 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 5030 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 4453 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 7576 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 9001 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 9031 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 9263 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 9293 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 7555 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 3496 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 4368 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 11528 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
    """
    if z3_debug():
        _z3_assert(is_expr(re), "expression expected")
    return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)

def z3py.Store	(		a,
			args
	)

Return a Z3 store array expression.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Store(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

Definition at line 4880 of file z3py.py.

Referenced by is_array(), is_store(), SetAdd(), and SetDel().

def Store(a, *args):
    """Return a Z3 store array expression.

    >>> a    = Array('a', IntSort(), IntSort())
    >>> i, v = Ints('i v')
    >>> s    = Store(a, i, v)
    >>> s.sort()
    Array(Int, Int)
    >>> prove(s[i] == v)
    proved
    >>> j    = Int('j')
    >>> prove(Implies(i != j, s[j] == a[j]))
    proved
    """
    return Update(a, args)

def z3py.StrFromCode

(

c

)

Convert code to a string

Definition at line 11396 of file z3py.py.

def StrFromCode(c):
    """Convert code to a string"""
    if not is_expr(c):
        c = _py2expr(c)
    return SeqRef(Z3_mk_string_from_code(c.ctx_ref(), c.as_ast()), c.ctx)
    

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 11171 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 11180 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 10986 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 11164 of file z3py.py.

Referenced by deserialize(), 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.StrToCode

(

s

)

Convert a unit length string to integer code

Definition at line 11390 of file z3py.py.

def StrToCode(s):
    """Convert a unit length string to integer code"""
    if not is_expr(s):
        s = _py2expr(s)
    return ArithRef(Z3_mk_string_to_code(s.ctx_ref(), s.as_ast()), 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 11367 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 11193 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 9036 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]) for p in m]),
            "Z3 invalid substitution, expression pairs expected.")
        _z3_assert(
            all([p[0].sort().eq(p[1].sort()) for p in m]),
            'Z3 invalid substitution, mismatching "from" and "to" sorts.')
    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_funs	(		t,
			m
	)

Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
Every occurrence in to of the function from is replaced with the expression to.
The expression to can have free variables, that refer to the arguments of from.
For examples, see 

Definition at line 9089 of file z3py.py.

def substitute_funs(t, *m):
    """Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
    Every occurrence in to of the function from is replaced with the expression to.
    The expression to can have free variables, that refer to the arguments of from.
    For examples, see 
    """
    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_func_decl(p[0]) and is_expr(p[1]) for p in m]), "Z3 invalid substitution, function pairs expected.")
    num = len(m)
    _from = (FuncDecl * num)()
    _to = (Ast * num)()
    for i in range(num):
        _from[i] = m[i][0].as_func_decl()
        _to[i] = m[i][1].as_ast()
    return _to_expr_ref(Z3_substitute_funs(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 9069 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 11188 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 11253 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 9111 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 8690 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 8679 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 8547 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_Ast

(

ptr

)

Definition at line 11612 of file z3py.py.

Referenced by on_clause_eh().

def to_Ast(ptr,):
    ast = Ast(ptr)
    super(ctypes.c_void_p, ast).__init__(ptr)
    return ast

def z3py.to_AstVectorObj

(

ptr

)

Definition at line 11622 of file z3py.py.

Referenced by on_clause_eh().

def to_AstVectorObj(ptr,):
    v = AstVectorObj(ptr)
    super(ctypes.c_void_p, v).__init__(ptr)    
    return v

# NB. my-hacky-class only works for a single instance of OnClause
# it should be replaced with a proper correlation between OnClause
# and object references that can be passed over the FFI.
# for UserPropagator we use a global dictionary, which isn't great code.

def z3py.to_ContextObj

(

ptr

)

Definition at line 11617 of file z3py.py.

def to_ContextObj(ptr,):
    ctx = ContextObj(ptr)
    super(ctypes.c_void_p, ctx).__init__(ptr)
    return ctx

def z3py.to_symbol	(		s,
			ctx = None
	)

Convert an integer or string into a Z3 symbol.

Definition at line 132 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DatatypeSort(), DeclareSort(), DeclareTypeVar(), EnumSort(), FiniteDomainSort(), FP(), Function(), Int(), PropagateFunction(), 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 3461 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 3441 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
    """
    ctx = a.ctx
    if isinstance(a, BoolRef):
        return If(a, RealVal(1, ctx), RealVal(0, ctx))
    if z3_debug():
        _z3_assert(a.is_int(), "Z3 integer expression expected.")
    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 11605 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 11597 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 8670 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 5453 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 4326 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 4290 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 4308 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 4254 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 4272 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 11455 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 11233 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,
			args
	)

Return a Z3 store array expression.

>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Update(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved

Definition at line 4837 of file z3py.py.

Referenced by Store().

def Update(a, *args):
    """Return a Z3 store array expression.

    >>> a    = Array('a', IntSort(), IntSort())
    >>> i, v = Ints('i v')
    >>> s    = Update(a, i, v)
    >>> s.sort()
    Array(Int, Int)
    >>> prove(s[i] == v)
    proved
    >>> j    = Int('j')
    >>> prove(Implies(i != j, s[j] == a[j]))
    proved
    """
    if z3_debug():
        _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
    args = _get_args(args)
    ctx = a.ctx
    if len(args) <= 1:
        raise Z3Exception("array update requires index and value arguments")
    if len(args) == 2:
        i = args[0]
        v = args[1]
        i = a.sort().domain().cast(i)
        v = a.sort().range().cast(v)
        return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
    v = a.sort().range().cast(args[-1])
    idxs = [a.sort().domain_n(i).cast(args[i]) for i in range(len(args)-1)]
    _args, sz = _to_ast_array(idxs)
    return _to_expr_ref(Z3_mk_store_n(ctx.ref(), a.as_ast(), sz, _args, 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 4347 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_created	(		ctx,
			cb,
			id
	)

Definition at line 11733 of file z3py.py.

def user_prop_created(ctx, cb, id):
    prop = _prop_closures.get(ctx)
    old_cb = prop.cb
    prop.cb = cb
    id = _to_expr_ref(to_Ast(id), prop.ctx())
    prop.created(id)
    prop.cb = old_cb
    
    

def z3py.user_prop_decide	(		ctx,
			cb,
			t_ref,
			idx,
			phase
	)

Definition at line 11767 of file z3py.py.

def user_prop_decide(ctx, cb, t_ref, idx, phase):
    prop = _prop_closures.get(ctx)
    old_cb = prop.cb
    prop.cb = cb
    t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
    prop.decide(t, idx, phase)
    prop.cb = old_cb
    

def z3py.user_prop_diseq	(		ctx,
			cb,
			x,
			y
	)

Definition at line 11758 of file z3py.py.

def user_prop_diseq(ctx, cb, x, y):
    prop = _prop_closures.get(ctx)
    old_cb = prop.cb
    prop.cb = cb
    x = _to_expr_ref(to_Ast(x), prop.ctx())
    y = _to_expr_ref(to_Ast(y), prop.ctx())
    prop.diseq(x, y)
    prop.cb = old_cb

def z3py.user_prop_eq	(		ctx,
			cb,
			x,
			y
	)

Definition at line 11749 of file z3py.py.

def user_prop_eq(ctx, cb, x, y):
    prop = _prop_closures.get(ctx)
    old_cb = prop.cb
    prop.cb = cb
    x = _to_expr_ref(to_Ast(x), prop.ctx())
    y = _to_expr_ref(to_Ast(y), prop.ctx())
    prop.eq(x, y)
    prop.cb = old_cb

def z3py.user_prop_final	(		ctx,
			cb
	)

Definition at line 11742 of file z3py.py.

def user_prop_final(ctx, cb):
    prop = _prop_closures.get(ctx)
    old_cb = prop.cb
    prop.cb = cb
    prop.final()
    prop.cb = old_cb

def z3py.user_prop_fixed	(		ctx,
			cb,
			id,
			value
	)

Definition at line 11724 of file z3py.py.

def user_prop_fixed(ctx, cb, id, value):
    prop = _prop_closures.get(ctx)
    old_cb = prop.cb
    prop.cb = cb    
    id = _to_expr_ref(to_Ast(id), prop.ctx())
    value = _to_expr_ref(to_Ast(value), prop.ctx())
    prop.fixed(id, value)
    prop.cb = old_cb

def z3py.user_prop_fresh	(		ctx,
			_new_ctx
	)

Definition at line 11710 of file z3py.py.

def user_prop_fresh(ctx, _new_ctx):
    _prop_closures.set_threaded()
    prop = _prop_closures.get(ctx)
    nctx = Context()
    Z3_del_context(nctx.ctx)
    new_ctx = to_ContextObj(_new_ctx)
    nctx.ctx = new_ctx
    nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler)
    nctx.owner = False
    new_prop = prop.fresh(nctx)
    _prop_closures.set(new_prop.id, new_prop)
    return new_prop.id

def z3py.user_prop_pop	(		ctx,
			cb,
			num_scopes
	)

Definition at line 11704 of file z3py.py.

def user_prop_pop(ctx, cb, num_scopes):
    prop = _prop_closures.get(ctx)
    prop.cb = cb
    prop.pop(num_scopes)

def z3py.user_prop_push	(		ctx,
			cb
	)

Definition at line 11698 of file z3py.py.

def user_prop_push(ctx, cb):
    prop = _prop_closures.get(ctx)
    prop.cb = cb
    prop.push()

def z3py.Var

(

idx

)

Definition at line 1513 of file z3py.py.

Referenced by QuantifierRef.body(), QuantifierRef.children(), is_pattern(), MultiPattern(), QuantifierRef.pattern(), and RealVar().

def Var(idx : int, s : SortRef) -> ExprRef:
    """Create a Z3 free variable. Free variables are used to create quantified formulas.
    A free variable with index n is bound when it occurs within the scope of n+1 quantified
    declarations.
    
    >>> Var(0, IntSort())
    Var(0)
    >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
    False
    """
    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 8964 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 8621 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 8635 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 1870 of file z3py.py.

Referenced by BoolRef.__xor__().

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

Referenced by Probe.__call__(), Context.__init__(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), Concat(), Const(), CreateDatatypes(), ExprRef.decl(), Default(), describe_probes(), deserialize(), Diff(), Distinct(), 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(), ExprRef.kind(), Loop(), Map(), MultiPattern(), ExprRef.num_args(), Option(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), Plus(), PropagateFunction(), prove(), Range(), RatVal(), RecFunction(), RepeatBitVec(), Select(), set_param(), SignExt(), simplify(), solve_using(), Star(), substitute(), substitute_funs(), 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 184 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 4483 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 9516 of file z3py.py.

int _dflt_fpsort_sbits = 53

Definition at line 9517 of file z3py.py.

_dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN

Floating-Point Arithmetic.

Definition at line 9515 of file z3py.py.

_main_ctx = None

Definition at line 246 of file z3py.py.

_my_hacky_class = None

Definition at line 11632 of file z3py.py.

tuple _on_clause_eh = Z3_on_clause_eh(on_clause_eh)

Definition at line 11640 of file z3py.py.

tuple _on_model_eh = on_model_eh_type(_global_on_model)

Definition at line 8020 of file z3py.py.

dictionary _on_models = {}

Definition at line 8012 of file z3py.py.

_prop_closures = None

Definition at line 11689 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 9535 of file z3py.py.

tuple _user_prop_created = Z3_created_eh(user_prop_created)

Definition at line 11780 of file z3py.py.

tuple _user_prop_decide = Z3_decide_eh(user_prop_decide)

Definition at line 11784 of file z3py.py.

tuple _user_prop_diseq = Z3_eq_eh(user_prop_diseq)

Definition at line 11783 of file z3py.py.

tuple _user_prop_eq = Z3_eq_eh(user_prop_eq)

Definition at line 11782 of file z3py.py.

tuple _user_prop_final = Z3_final_eh(user_prop_final)

Definition at line 11781 of file z3py.py.

tuple _user_prop_fixed = Z3_fixed_eh(user_prop_fixed)

Definition at line 11779 of file z3py.py.

tuple _user_prop_fresh = Z3_fresh_eh(user_prop_fresh)

Definition at line 11778 of file z3py.py.

tuple _user_prop_pop = Z3_pop_eh(user_prop_pop)

Definition at line 11777 of file z3py.py.

tuple _user_prop_push = Z3_push_eh(user_prop_push)

Definition at line 11776 of file z3py.py.

tuple sat = CheckSatResult(Z3_L_TRUE)

Definition at line 7009 of file z3py.py.

tuple unknown = CheckSatResult(Z3_L_UNDEF)

Definition at line 7011 of file z3py.py.

tuple unsat = CheckSatResult(Z3_L_FALSE)

Definition at line 7010 of file z3py.py.

Z3_DEBUG = __debug__

Definition at line 67 of file z3py.py.