z3py Namespace Reference

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

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

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

Function Documentation

And()

def z3py.And

(

*

args

)

Create a Z3 and-expression or and-probe.

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

Definition at line 1813 of file z3py.py.

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)
 
 

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

AndThen()

def z3py.AndThen	(	*	ts,
		**	ks
	)

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

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

Definition at line 8171 of file z3py.py.

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
 
 

Referenced by Then().

append_log()

def z3py.append_log

(

s

)

Append user-defined string to interaction log. 

Definition at line 124 of file z3py.py.

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

args2params()

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

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

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

Definition at line 5396 of file z3py.py.

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
 
 

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

Array()

def z3py.Array	(		name,
			dom,
			rng
	)

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

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

Definition at line 4678 of file z3py.py.

def Array(name, dom, rng):
    """Return an array constant named `name` with the given domain and range sorts.
 
    >>> a = Array('a', IntSort(), IntSort())
    >>> a.sort()
    Array(Int, Int)
    >>> a[0]
    a[0]
    """
    s = ArraySort(dom, rng)
    ctx = s.ctx
    return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
 
 

ArraySort()

def z3py.ArraySort

(

*

sig

)

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

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

Definition at line 4645 of file z3py.py.

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)
 
 

Referenced by Array(), and SetSort().

AtLeast()

def z3py.AtLeast

(

*

args

)

Create an at-most Pseudo-Boolean k constraint.

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

Definition at line 8800 of file z3py.py.

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

AtMost()

def z3py.AtMost

(

*

args

)

Create an at-most Pseudo-Boolean k constraint.

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

Definition at line 8782 of file z3py.py.

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)
 
 

BitVec()

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

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

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

Definition at line 3999 of file z3py.py.

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)
 
 

Referenced by BitVecs().

BitVecs()

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

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

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

Definition at line 4023 of file z3py.py.

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]
 
 

BitVecSort()

def z3py.BitVecSort	(		sz,
			ctx = None
	)

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

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

Definition at line 3967 of file z3py.py.

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)
 
 

Referenced by BitVec(), and BitVecVal().

BitVecVal()

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

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

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

Definition at line 3982 of file z3py.py.

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)
 
 

Bool()

def z3py.Bool	(		name,
			ctx = None
	)

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

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

Definition at line 1692 of file z3py.py.

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)
 
 

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

Bools()

def z3py.Bools	(		names,
			ctx = None
	)

Return a tuple of Boolean constants.

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

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

Definition at line 1704 of file z3py.py.

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]
 
 

BoolSort()

def z3py.BoolSort

(

ctx = None

)

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

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

Definition at line 1655 of file z3py.py.

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)
 
 

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

BoolVal()

def z3py.BoolVal	(		val,
			ctx = None
	)

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

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

Definition at line 1673 of file z3py.py.

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)
 
 

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

BoolVector()

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

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

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

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

Definition at line 1720 of file z3py.py.

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)]
 
 

BV2Int()

def z3py.BV2Int	(		a,
			is_signed = False
	)

Return the Z3 expression BV2Int(a).

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

Definition at line 3935 of file z3py.py.

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)
 
 

BVAddNoOverflow()

def z3py.BVAddNoOverflow	(		a,
			b,
			signed
	)

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

Definition at line 4421 of file z3py.py.

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)
 
 

BVAddNoUnderflow()

def z3py.BVAddNoUnderflow	(		a,
			b
	)

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

Definition at line 4428 of file z3py.py.

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)
 
 

BVMulNoOverflow()

def z3py.BVMulNoOverflow	(		a,
			b,
			signed
	)

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

Definition at line 4463 of file z3py.py.

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)
 
 

BVMulNoUnderflow()

def z3py.BVMulNoUnderflow	(		a,
			b
	)

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

Definition at line 4470 of file z3py.py.

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)
 
 

BVRedAnd()

def z3py.BVRedAnd

(

a

)

Return the reduction-and expression of `a`.

Definition at line 4407 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)
 
 

BVRedOr()

def z3py.BVRedOr

(

a

)

Return the reduction-or expression of `a`.

Definition at line 4414 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)
 
 

BVSDivNoOverflow()

def z3py.BVSDivNoOverflow	(		a,
			b
	)

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

Definition at line 4449 of file z3py.py.

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)
 
 

BVSNegNoOverflow()

def z3py.BVSNegNoOverflow

(

a

)

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

Definition at line 4456 of file z3py.py.

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)
 
 

BVSubNoOverflow()

def z3py.BVSubNoOverflow	(		a,
			b
	)

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

Definition at line 4435 of file z3py.py.

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)
 
 

BVSubNoUnderflow()

def z3py.BVSubNoUnderflow	(		a,
			b,
			signed
	)

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

Definition at line 4442 of file z3py.py.

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)
 
 

Cbrt()

def z3py.Cbrt	(		a,
			ctx = None
	)

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

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

Definition at line 3386 of file z3py.py.

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"
 

Complement()

def z3py.Complement

(

re

)

Create the complement regular expression.

Definition at line 11002 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)
 
 

Concat()

def z3py.Concat

(

*

args

)

Create a Z3 bit-vector concatenation expression.

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

Definition at line 4044 of file z3py.py.

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
 
 

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

Cond()

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

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

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

Definition at line 8628 of file z3py.py.

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)
 

Referenced by If().

Const()

def z3py.Const	(		name,
			sort
	)

Create a constant of the given sort.

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

Definition at line 1405 of file z3py.py.

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)
 
 

Referenced by Consts().

Consts()

def z3py.Consts	(		names,
			sort
	)

Create several constants of the given sort.

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

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

Definition at line 1417 of file z3py.py.

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]
 
 

Contains()

def z3py.Contains	(		a,
			b
	)

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

Definition at line 10789 of file z3py.py.

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)
 
 

CreateDatatypes()

def z3py.CreateDatatypes

(

*

ds

)

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

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

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

Definition at line 5092 of file z3py.py.

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)
 
 

Referenced by Datatype.create().

DeclareSort()

def z3py.DeclareSort	(		name,
			ctx = None
	)

Create a new uninterpreted sort named `name`.

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

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

Definition at line 690 of file z3py.py.

def DeclareSort(name, ctx=None):
    """Create a new uninterpreted sort named `name`.
 
    If `ctx=None`, then the new sort is declared in the global Z3Py context.
 
    >>> A = DeclareSort('A')
    >>> a = Const('a', A)
    >>> b = Const('b', A)
    >>> a.sort() == A
    True
    >>> b.sort() == A
    True
    >>> a == b
    a == b
    """
    ctx = _get_ctx(ctx)
    return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
 

Default()

def z3py.Default

(

a

)

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

Definition at line 4714 of file z3py.py.

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()
 
 

describe_probes()

def z3py.describe_probes

(

)

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

Definition at line 8549 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)))
 
 

describe_tactics()

def z3py.describe_tactics

(

)

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

Definition at line 8343 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)))
 
 

disable_trace()

def z3py.disable_trace

(

msg

)

Definition at line 81 of file z3py.py.

def disable_trace(msg):
    Z3_disable_trace(msg)
 
 

DisjointSum()

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

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

Definition at line 5305 of file z3py.py.

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))]
 
 

Distinct()

def z3py.Distinct

(

*

args

)

Create a Z3 distinct expression.

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

Definition at line 1372 of file z3py.py.

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)
 
 

Empty()

def z3py.Empty

(

s

)

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

Definition at line 10720 of file z3py.py.

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")
 
 

EmptySet()

def z3py.EmptySet

(

s

)

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

Definition at line 4856 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)
 
 

enable_trace()

def z3py.enable_trace

(

msg

)

Definition at line 77 of file z3py.py.

def enable_trace(msg):
    Z3_enable_trace(msg)
 
 

ensure_prop_closures()

def z3py.ensure_prop_closures

(

)

Definition at line 11110 of file z3py.py.

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

Referenced by UserPropagateBase.__init__().

EnumSort()

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

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

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

Definition at line 5317 of file z3py.py.

def EnumSort(name, values, ctx=None):
    """Return a new enumeration sort named `name` containing the given values.
 
    The result is a pair (sort, list of constants).
    Example:
        >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
    """
    if z3_debug():
        _z3_assert(isinstance(name, str), "Name must be a string")
        _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
        _z3_assert(len(values) > 0, "At least one value expected")
    ctx = _get_ctx(ctx)
    num = len(values)
    _val_names = (Symbol * num)()
    for i in range(num):
        _val_names[i] = to_symbol(values[i])
    _values = (FuncDecl * num)()
    _testers = (FuncDecl * num)()
    name = to_symbol(name)
    S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
    V = []
    for i in range(num):
        V.append(FuncDeclRef(_values[i], ctx))
    V = [a() for a in V]
    return S, V
 

eq()

def z3py.eq	(		a,
			b
	)

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

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

Definition at line 471 of file z3py.py.

def eq(a, b):
    """Return `True` if `a` and `b` are structurally identical AST nodes.
 
    >>> x = Int('x')
    >>> y = Int('y')
    >>> eq(x, y)
    False
    >>> eq(x + 1, x + 1)
    True
    >>> eq(x + 1, 1 + x)
    False
    >>> eq(simplify(x + 1), simplify(1 + x))
    True
    """
    if z3_debug():
        _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
    return a.eq(b)
 
 

Referenced by substitute().

Exists()

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

Create a Z3 exists formula.

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


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

Definition at line 2205 of file z3py.py.

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)
 
 

Referenced by Fixedpoint.abstract().

Ext()

def z3py.Ext	(		a,
			b
	)

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

Definition at line 4802 of file z3py.py.

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

Extract()

def z3py.Extract	(		high,
			low,
			a
	)

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

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

Definition at line 4090 of file z3py.py.

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)
 
 

Referenced by SubSeq(), and SubString().

FailIf()

def z3py.FailIf	(		p,
			ctx = None
	)

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

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

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

Definition at line 8586 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)
 
 

FiniteDomainSort()

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

Create a named finite domain sort of a given size sz

Definition at line 7590 of file z3py.py.

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)
 
 

FiniteDomainVal()

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

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

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

Definition at line 7660 of file z3py.py.

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)
 
 

Float128()

def z3py.Float128

(

ctx = None

)

Floating-point 128-bit (quadruple) sort.

Definition at line 9266 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)
 
 

Float16()

def z3py.Float16

(

ctx = None

)

Floating-point 16-bit (half) sort.

Definition at line 9230 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)
 
 

Float32()

def z3py.Float32

(

ctx = None

)

Floating-point 32-bit (single) sort.

Definition at line 9242 of file z3py.py.

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

Float64()

def z3py.Float64

(

ctx = None

)

Floating-point 64-bit (double) sort.

Definition at line 9254 of file z3py.py.

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

FloatDouble()

def z3py.FloatDouble

(

ctx = None

)

Floating-point 64-bit (double) sort.

Definition at line 9260 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)
 
 

FloatHalf()

def z3py.FloatHalf

(

ctx = None

)

Floating-point 16-bit (half) sort.

Definition at line 9236 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)
 
 

FloatQuadruple()

def z3py.FloatQuadruple

(

ctx = None

)

Floating-point 128-bit (quadruple) sort.

Definition at line 9272 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)
 
 

FloatSingle()

def z3py.FloatSingle

(

ctx = None

)

Floating-point 32-bit (single) sort.

Definition at line 9248 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)
 
 

ForAll()

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

Create a Z3 forall formula.

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

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

Definition at line 2187 of file z3py.py.

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)
 
 

Referenced by Fixedpoint.abstract().

FP()

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

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

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

Definition at line 9898 of file z3py.py.

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)
 
 

Referenced by FPs().

fpAbs()

def z3py.fpAbs	(		a,
			ctx = None
	)

Create a Z3 floating-point absolute value expression.

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

Definition at line 9941 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)
 
 

fpAdd()

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

Create a Z3 floating-point addition expression.

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

Definition at line 10032 of file z3py.py.

def fpAdd(rm, a, b, ctx=None):
    """Create a Z3 floating-point addition expression.
 
    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpAdd(rm, x, y)
    fpAdd(RNE(), x, y)
    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
    x + y
    >>> fpAdd(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
 
 

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

fpBVToFP()

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

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

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

Definition at line 10354 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)
 
 

fpDiv()

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

Create a Z3 floating-point division expression.

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

Definition at line 10079 of file z3py.py.

def fpDiv(rm, a, b, ctx=None):
    """Create a Z3 floating-point division expression.
 
    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpDiv(rm, x, y)
    fpDiv(RNE(), x, y)
    >>> fpDiv(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
 
 

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

fpEQ()

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

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

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

Definition at line 10262 of file z3py.py.

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)
 
 

Referenced by fpNEQ().

fpFMA()

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

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

Definition at line 10138 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)
 
 

fpFP()

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

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

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

Definition at line 10286 of file z3py.py.

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)
 
 

fpFPToFP()

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

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

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

Definition at line 10371 of file z3py.py.

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)
 
 

fpGEQ()

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

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

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

Definition at line 10250 of file z3py.py.

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)
 
 

Referenced by FPRef.__ge__().

fpGT()

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

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

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

Definition at line 10238 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)
 
 

Referenced by FPRef.__gt__().

fpInfinity()

def z3py.fpInfinity	(		s,
			negative
	)

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

Definition at line 9826 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)
 
 

fpIsInf()

def z3py.fpIsInf	(		a,
			ctx = None
	)

Create a Z3 floating-point isInfinite expression.

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

Definition at line 10168 of file z3py.py.

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)
 
 

fpIsNaN()

def z3py.fpIsNaN	(		a,
			ctx = None
	)

Create a Z3 floating-point isNaN expression.

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

Definition at line 10156 of file z3py.py.

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)
 
 

fpIsNegative()

def z3py.fpIsNegative	(		a,
			ctx = None
	)

Create a Z3 floating-point isNegative expression.

Definition at line 10197 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)
 
 

fpIsNormal()

def z3py.fpIsNormal	(		a,
			ctx = None
	)

Create a Z3 floating-point isNormal expression.

Definition at line 10185 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)
 
 

fpIsPositive()

def z3py.fpIsPositive	(		a,
			ctx = None
	)

Create a Z3 floating-point isPositive expression.

Definition at line 10203 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)
 
 

fpIsSubnormal()

def z3py.fpIsSubnormal	(		a,
			ctx = None
	)

Create a Z3 floating-point isSubnormal expression.

Definition at line 10191 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)
 
 

fpIsZero()

def z3py.fpIsZero	(		a,
			ctx = None
	)

Create a Z3 floating-point isZero expression.

Definition at line 10179 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)
 
 

fpLEQ()

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

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

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

Definition at line 10226 of file z3py.py.

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)
 
 

Referenced by FPRef.__le__().

fpLT()

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

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

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

Definition at line 10214 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)
 
 

Referenced by FPRef.__lt__().

fpMax()

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

Create a Z3 floating-point maximum expression.

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

Definition at line 10123 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)
 
 

fpMin()

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

Create a Z3 floating-point minimum expression.

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

Definition at line 10108 of file z3py.py.

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)
 
 

fpMinusInfinity()

def z3py.fpMinusInfinity

(

s

)

Create a Z3 floating-point -oo term.

Definition at line 9820 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)
 
 

Referenced by FPVal().

fpMinusZero()

def z3py.fpMinusZero

(

s

)

Create a Z3 floating-point -0.0 term.

Definition at line 9839 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)
 
 

Referenced by FPVal().

fpMul()

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

Create a Z3 floating-point multiplication expression.

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

Definition at line 10064 of file z3py.py.

def fpMul(rm, a, b, ctx=None):
    """Create a Z3 floating-point multiplication expression.
 
    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpMul(rm, x, y)
    fpMul(RNE(), x, y)
    >>> fpMul(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
 
 

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

fpNaN()

def z3py.fpNaN

(

s

)

Create a Z3 floating-point NaN term.

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

Definition at line 9786 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)
 
 

Referenced by FPVal().

fpNeg()

def z3py.fpNeg	(		a,
			ctx = None
	)

Create a Z3 floating-point addition expression.

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

Definition at line 9964 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)
 
 

Referenced by FPRef.__neg__().

fpNEQ()

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

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

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

Definition at line 10274 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))
 
 

fpPlusInfinity()

def z3py.fpPlusInfinity

(

s

)

Create a Z3 floating-point +oo term.

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

Definition at line 9803 of file z3py.py.

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)
 
 

Referenced by FPVal().

fpPlusZero()

def z3py.fpPlusZero

(

s

)

Create a Z3 floating-point +0.0 term.

Definition at line 9833 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)
 
 

Referenced by FPVal().

fpRealToFP()

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

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

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

Definition at line 10391 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)
 
 

fpRem()

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

Create a Z3 floating-point remainder expression.

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

Definition at line 10094 of file z3py.py.

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)
 
 

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

fpRoundToIntegral()

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

Create a Z3 floating-point roundToIntegral expression.

Definition at line 10150 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)
 
 

FPs()

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

Return an array of floating-point constants.

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

Definition at line 9922 of file z3py.py.

def FPs(names, fpsort, ctx=None):
    """Return an array of floating-point constants.
 
    >>> x, y, z = FPs('x y z', FPSort(8, 24))
    >>> x.sort()
    FPSort(8, 24)
    >>> x.sbits()
    24
    >>> x.ebits()
    8
    >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
    fpMul(RNE(), fpAdd(RNE(), x, y), z)
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [FP(name, fpsort, ctx) for name in names]
 
 

fpSignedToFP()

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

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

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

Definition at line 10409 of file z3py.py.

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)
 
 

FPSort()

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

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

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

Definition at line 9727 of file z3py.py.

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)
 
 

Referenced by get_default_fp_sort().

fpSqrt()

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

Create a Z3 floating-point square root expression.

Definition at line 10144 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)
 
 

fpSub()

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

Create a Z3 floating-point subtraction expression.

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

Definition at line 10049 of file z3py.py.

def fpSub(rm, a, b, ctx=None):
    """Create a Z3 floating-point subtraction expression.
 
    >>> s = FPSort(8, 24)
    >>> rm = RNE()
    >>> x = FP('x', s)
    >>> y = FP('y', s)
    >>> fpSub(rm, x, y)
    fpSub(RNE(), x, y)
    >>> fpSub(rm, x, y).sort()
    FPSort(8, 24)
    """
    return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
 
 

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

fpToFP()

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

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

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

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

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

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

Definition at line 10315 of file z3py.py.

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.")
 
 

fpToFPUnsigned()

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

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

Definition at line 10445 of file z3py.py.

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)
 
 

fpToIEEEBV()

def z3py.fpToIEEEBV	(		x,
			ctx = None
	)

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

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

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

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

Definition at line 10519 of file z3py.py.

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)
 
 

fpToReal()

def z3py.fpToReal	(		x,
			ctx = None
	)

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

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

Definition at line 10499 of file z3py.py.

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)
 
 

fpToSBV()

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

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

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

Definition at line 10455 of file z3py.py.

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)
 
 

fpToUBV()

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

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

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

Definition at line 10477 of file z3py.py.

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)
 
 

fpUnsignedToFP()

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

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

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

Definition at line 10427 of file z3py.py.

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)
 
 

FPVal()

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

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

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

Definition at line 9852 of file z3py.py.

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)
 
 

Referenced by set_default_fp_sort().

fpZero()

def z3py.fpZero	(		s,
			negative
	)

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

Definition at line 9845 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)
 
 

FreshBool()

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

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

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

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

Definition at line 1735 of file z3py.py.

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)
 
 

FreshConst()

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

Create a fresh constant of a specified sort

Definition at line 1432 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)
 
 

FreshFunction()

def z3py.FreshFunction

(

*

sig

)

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

Definition at line 883 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)
 
 

FreshInt()

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

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

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

Definition at line 3249 of file z3py.py.

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)
 
 

FreshReal()

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

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

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

Definition at line 3306 of file z3py.py.

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)
 
 

Full()

def z3py.Full

(

s

)

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

Definition at line 10740 of file z3py.py.

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")
 
 

FullSet()

def z3py.FullSet

(

s

)

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

Definition at line 4865 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)
 
 

Function()

def z3py.Function	(		name,
		*	sig
	)

Create a new Z3 uninterpreted function with the given sorts.

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

Definition at line 860 of file z3py.py.

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)
 
 

get_as_array_func()

def z3py.get_as_array_func

(

n

)

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

Definition at line 6589 of file z3py.py.

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)
 

Referenced by ModelRef.get_interp().

get_ctx()

def z3py.get_ctx

(

ctx

)

Definition at line 266 of file z3py.py.

def get_ctx(ctx):
    return _get_ctx(ctx)
 
 

get_default_fp_sort()

def z3py.get_default_fp_sort

(

ctx = None

)

Definition at line 9149 of file z3py.py.

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

Referenced by set_default_fp_sort().

get_default_rounding_mode()

def z3py.get_default_rounding_mode

(

ctx = None

)

Retrieves the global default rounding mode.

Definition at line 9116 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)
 
 

Referenced by set_default_fp_sort().

get_full_version()

def z3py.get_full_version

(

)

Definition at line 103 of file z3py.py.

def get_full_version():
    return Z3_get_full_version()
 
# We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com
 
 

get_map_func()

def z3py.get_map_func

(

a

)

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

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

Definition at line 4621 of file z3py.py.

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,
    )
 
 

get_param()

def z3py.get_param

(

name

)

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

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

Definition at line 306 of file z3py.py.

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)
 

get_var_index()

def z3py.get_var_index

(

a

)

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

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

Definition at line 1303 of file z3py.py.

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()))
 
 

get_version()

def z3py.get_version

(

)

Definition at line 94 of file z3py.py.

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

get_version_string()

def z3py.get_version_string

(

)

Definition at line 85 of file z3py.py.

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

help_simplify()

def z3py.help_simplify

(

)

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

Definition at line 8670 of file z3py.py.

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

If()

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

Create a Z3 if-then-else expression.

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

Definition at line 1349 of file z3py.py.

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)
 
 

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

Implies()

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

Create a Z3 implies expression.

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

Definition at line 1749 of file z3py.py.

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)
 
 

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

IndexOf()

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

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

Definition at line 10823 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)
 
 

InRe()

def z3py.InRe	(		s,
			re
	)

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

Definition at line 10924 of file z3py.py.

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)
 
 

Int()

def z3py.Int	(		name,
			ctx = None
	)

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

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

Definition at line 3210 of file z3py.py.

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)
 
 

Referenced by Ints(), and IntVector().

Int2BV()

def z3py.Int2BV	(		a,
			num_bits
	)

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

Definition at line 3958 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)
 
 

Intersect()

def z3py.Intersect

(

*

args

)

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

Definition at line 10958 of file z3py.py.

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)
 
 

Ints()

def z3py.Ints	(		names,
			ctx = None
	)

Return a tuple of Integer constants.

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

Definition at line 3223 of file z3py.py.

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]
 
 

IntSort()

def z3py.IntSort

(

ctx = None

)

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

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

Definition at line 3100 of file z3py.py.

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)
 
 

Referenced by FreshInt(), Int(), and IntVal().

IntToStr()

def z3py.IntToStr

(

s

)

Convert integer expression to string

Definition at line 10878 of file z3py.py.

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)
 
 

IntVal()

def z3py.IntVal	(		val,
			ctx = None
	)

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

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

Definition at line 3150 of file z3py.py.

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)
 
 

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

IntVector()

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

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

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

Definition at line 3236 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)]
 
 

is_add()

def z3py.is_add

(

a

)

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

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

Definition at line 2754 of file z3py.py.

def is_add(a):
    """Return `True` if `a` is an expression of the form b + c.
 
    >>> x, y = Ints('x y')
    >>> is_add(x + y)
    True
    >>> is_add(x - y)
    False
    """
    return is_app_of(a, Z3_OP_ADD)
 
 

is_algebraic_value()

def z3py.is_algebraic_value

(

a

)

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

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

Definition at line 2740 of file z3py.py.

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())
 
 

is_and()

def z3py.is_and

(

a

)

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

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

Definition at line 1585 of file z3py.py.

def is_and(a):
    """Return `True` if `a` is a Z3 and expression.
 
    >>> p, q = Bools('p q')
    >>> is_and(And(p, q))
    True
    >>> is_and(Or(p, q))
    False
    """
    return is_app_of(a, Z3_OP_AND)
 
 

is_app()

def z3py.is_app

(

a

)

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

Note that, constants are function applications with 0 arguments.

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

Definition at line 1233 of file z3py.py.

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
 
 

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

is_app_of()

def z3py.is_app_of	(		a,
			k
	)

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

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

Definition at line 1336 of file z3py.py.

def is_app_of(a, k):
    """Return `True` if `a` is an application of the given kind `k`.
 
    >>> x = Int('x')
    >>> n = x + 1
    >>> is_app_of(n, Z3_OP_ADD)
    True
    >>> is_app_of(n, Z3_OP_MUL)
    False
    """
    return is_app(a) and a.decl().kind() == k
 
 

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

is_arith()

def z3py.is_arith

(

a

)

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

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

Definition at line 2627 of file z3py.py.

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)
 
 

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

is_arith_sort()

def z3py.is_arith_sort

(

s

)

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

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

Definition at line 2326 of file z3py.py.

def is_arith_sort(s):
    """Return `True` if s is an arithmetical sort (type).
 
    >>> is_arith_sort(IntSort())
    True
    >>> is_arith_sort(RealSort())
    True
    >>> is_arith_sort(BoolSort())
    False
    >>> n = Int('x') + 1
    >>> is_arith_sort(n.sort())
    True
    """
    return isinstance(s, ArithSortRef)
 
 

Referenced by ArithSortRef.subsort().

is_array()

def z3py.is_array

(

a

)

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

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

Definition at line 4556 of file z3py.py.

def is_array(a):
    """Return `True` if `a` is a Z3 array expression.
 
    >>> a = Array('a', IntSort(), IntSort())
    >>> is_array(a)
    True
    >>> is_array(Store(a, 0, 1))
    True
    >>> is_array(a[0])
    False
    """
    return isinstance(a, ArrayRef)
 
 

Referenced by Ext(), and Map().

is_array_sort()

def z3py.is_array_sort

(

a

)

Definition at line 4552 of file z3py.py.

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

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

is_as_array()

def z3py.is_as_array

(

n

)

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

Definition at line 6584 of file z3py.py.

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())
 
 

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

is_ast()

def z3py.is_ast

(

a

)

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

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

Definition at line 450 of file z3py.py.

def is_ast(a):
    """Return `True` if `a` is an AST node.
 
    >>> is_ast(10)
    False
    >>> is_ast(IntVal(10))
    True
    >>> is_ast(Int('x'))
    True
    >>> is_ast(BoolSort())
    True
    >>> is_ast(Function('f', IntSort(), IntSort()))
    True
    >>> is_ast("x")
    False
    >>> is_ast(Solver())
    False
    """
    return isinstance(a, AstRef)
 
 

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

is_bool()

def z3py.is_bool

(

a

)

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

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

Definition at line 1535 of file z3py.py.

def is_bool(a):
    """Return `True` if `a` is a Z3 Boolean expression.
 
    >>> p = Bool('p')
    >>> is_bool(p)
    True
    >>> q = Bool('q')
    >>> is_bool(And(p, q))
    True
    >>> x = Real('x')
    >>> is_bool(x)
    False
    >>> is_bool(x == 0)
    True
    """
    return isinstance(a, BoolRef)
 
 

Referenced by is_quantifier(), and prove().

is_bv()

def z3py.is_bv

(

a

)

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

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

Definition at line 3906 of file z3py.py.

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)
 
 

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

is_bv_sort()

def z3py.is_bv_sort

(

s

)

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

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

Definition at line 3438 of file z3py.py.

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)
 
 

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

is_bv_value()

def z3py.is_bv_value

(

a

)

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

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

Definition at line 3920 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())
 
 

is_const()

def z3py.is_const

(

a

)

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

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

Definition at line 1259 of file z3py.py.

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
 
 

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

is_const_array()

def z3py.is_const_array

(

a

)

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

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

Definition at line 4570 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)
 
 

is_default()

def z3py.is_default

(

a

)

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

Definition at line 4612 of file z3py.py.

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)
 
 

is_distinct()

def z3py.is_distinct

(

a

)

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

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

Definition at line 1643 of file z3py.py.

def is_distinct(a):
    """Return `True` if `a` is a Z3 distinct expression.
 
    >>> x, y, z = Ints('x y z')
    >>> is_distinct(x == y)
    False
    >>> is_distinct(Distinct(x, y, z))
    True
    """
    return is_app_of(a, Z3_OP_DISTINCT)
 
 

is_div()

def z3py.is_div

(

a

)

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

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

Definition at line 2790 of file z3py.py.

def is_div(a):
    """Return `True` if `a` is an expression of the form b / c.
 
    >>> x, y = Reals('x y')
    >>> is_div(x / y)
    True
    >>> is_div(x + y)
    False
    >>> x, y = Ints('x y')
    >>> is_div(x / y)
    False
    >>> is_idiv(x / y)
    True
    """
    return is_app_of(a, Z3_OP_DIV)
 
 

is_eq()

def z3py.is_eq

(

a

)

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

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

Definition at line 1633 of file z3py.py.

def is_eq(a):
    """Return `True` if `a` is a Z3 equality expression.
 
    >>> x, y = Ints('x y')
    >>> is_eq(x == y)
    True
    """
    return is_app_of(a, Z3_OP_EQ)
 
 

Referenced by AstRef.__bool__().

is_expr()

def z3py.is_expr

(

a

)

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

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

Definition at line 1210 of file z3py.py.

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)
 
 

Referenced by SeqRef.__gt__(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), ExprRef.children(), Concat(), AlgebraicNumRef.index(), IndexOf(), IntToStr(), is_quantifier(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), substitute(), and substitute_vars().

is_false()

def z3py.is_false

(

a

)

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

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

Definition at line 1571 of file z3py.py.

def is_false(a):
    """Return `True` if `a` is the Z3 false expression.
 
    >>> p = Bool('p')
    >>> is_false(p)
    False
    >>> is_false(False)
    False
    >>> is_false(BoolVal(False))
    True
    """
    return is_app_of(a, Z3_OP_FALSE)
 
 

Referenced by AstRef.__bool__().

is_finite_domain()

def z3py.is_finite_domain

(

a

)

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

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

Definition at line 7621 of file z3py.py.

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)
 
 

Referenced by is_finite_domain_value().

is_finite_domain_sort()

def z3py.is_finite_domain_sort

(

s

)

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

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

Definition at line 7598 of file z3py.py.

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)
 
 

Referenced by FiniteDomainVal().

is_finite_domain_value()

def z3py.is_finite_domain_value

(

a

)

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

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

Definition at line 7675 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())
 
 

is_fp()

def z3py.is_fp

(

a

)

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

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

Definition at line 9698 of file z3py.py.

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)
 
 

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

is_fp_sort()

def z3py.is_fp_sort

(

s

)

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

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

Definition at line 9282 of file z3py.py.

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)
 
 

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

is_fp_value()

def z3py.is_fp_value

(

a

)

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

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

Definition at line 9712 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)
 
 

is_fprm()

def z3py.is_fprm

(

a

)

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

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

Definition at line 9542 of file z3py.py.

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)
 
 

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

is_fprm_sort()

def z3py.is_fprm_sort

(

s

)

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

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

Definition at line 9293 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
 
 

is_fprm_value()

def z3py.is_fprm_value

(

a

)

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

Definition at line 9555 of file z3py.py.

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
 
 

Referenced by set_default_rounding_mode().

is_func_decl()

def z3py.is_func_decl

(

a

)

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

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

Definition at line 847 of file z3py.py.

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)
 
 

Referenced by Map(), and prove().

is_ge()

def z3py.is_ge

(

a

)

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

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

Definition at line 2855 of file z3py.py.

def is_ge(a):
    """Return `True` if `a` is an expression of the form b >= c.
 
    >>> x, y = Ints('x y')
    >>> is_ge(x >= y)
    True
    >>> is_ge(x == y)
    False
    """
    return is_app_of(a, Z3_OP_GE)
 
 

is_gt()

def z3py.is_gt

(

a

)

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

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

Definition at line 2867 of file z3py.py.

def is_gt(a):
    """Return `True` if `a` is an expression of the form b > c.
 
    >>> x, y = Ints('x y')
    >>> is_gt(x > y)
    True
    >>> is_gt(x == y)
    False
    """
    return is_app_of(a, Z3_OP_GT)
 
 

is_idiv()

def z3py.is_idiv

(

a

)

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

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

Definition at line 2807 of file z3py.py.

def is_idiv(a):
    """Return `True` if `a` is an expression of the form b div c.
 
    >>> x, y = Ints('x y')
    >>> is_idiv(x / y)
    True
    >>> is_idiv(x + y)
    False
    """
    return is_app_of(a, Z3_OP_IDIV)
 
 

is_implies()

def z3py.is_implies

(

a

)

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

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

Definition at line 1609 of file z3py.py.

def is_implies(a):
    """Return `True` if `a` is a Z3 implication expression.
 
    >>> p, q = Bools('p q')
    >>> is_implies(Implies(p, q))
    True
    >>> is_implies(And(p, q))
    False
    """
    return is_app_of(a, Z3_OP_IMPLIES)
 
 

is_int()

def z3py.is_int

(

a

)

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

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

Definition at line 2648 of file z3py.py.

def is_int(a):
    """Return `True` if `a` is an integer expression.
 
    >>> x = Int('x')
    >>> is_int(x + 1)
    True
    >>> is_int(1)
    False
    >>> is_int(IntVal(1))
    True
    >>> y = Real('y')
    >>> is_int(y)
    False
    >>> is_int(y + 1)
    False
    """
    return is_arith(a) and a.is_int()
 
 

is_int_value()

def z3py.is_int_value

(

a

)

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

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

Definition at line 2694 of file z3py.py.

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())
 
 

is_is_int()

def z3py.is_is_int

(

a

)

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

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

Definition at line 2879 of file z3py.py.

def is_is_int(a):
    """Return `True` if `a` is an expression of the form IsInt(b).
 
    >>> x = Real('x')
    >>> is_is_int(IsInt(x))
    True
    >>> is_is_int(x)
    False
    """
    return is_app_of(a, Z3_OP_IS_INT)
 
 

is_K()

def z3py.is_K

(

a

)

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

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

Definition at line 4583 of file z3py.py.

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)
 
 

is_le()

def z3py.is_le

(

a

)

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

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

Definition at line 2831 of file z3py.py.

def is_le(a):
    """Return `True` if `a` is an expression of the form b <= c.
 
    >>> x, y = Ints('x y')
    >>> is_le(x <= y)
    True
    >>> is_le(x < y)
    False
    """
    return is_app_of(a, Z3_OP_LE)
 
 

is_lt()

def z3py.is_lt

(

a

)

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

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

Definition at line 2843 of file z3py.py.

def is_lt(a):
    """Return `True` if `a` is an expression of the form b < c.
 
    >>> x, y = Ints('x y')
    >>> is_lt(x < y)
    True
    >>> is_lt(x == y)
    False
    """
    return is_app_of(a, Z3_OP_LT)
 
 

is_map()

def z3py.is_map

(

a

)

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

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

Definition at line 4596 of file z3py.py.

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)
 
 

Referenced by get_map_func().

is_mod()

def z3py.is_mod

(

a

)

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

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

Definition at line 2819 of file z3py.py.

def is_mod(a):
    """Return `True` if `a` is an expression of the form b % c.
 
    >>> x, y = Ints('x y')
    >>> is_mod(x % y)
    True
    >>> is_mod(x + y)
    False
    """
    return is_app_of(a, Z3_OP_MOD)
 
 

is_mul()

def z3py.is_mul

(

a

)

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

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

Definition at line 2766 of file z3py.py.

def is_mul(a):
    """Return `True` if `a` is an expression of the form b * c.
 
    >>> x, y = Ints('x y')
    >>> is_mul(x * y)
    True
    >>> is_mul(x - y)
    False
    """
    return is_app_of(a, Z3_OP_MUL)
 
 

is_not()

def z3py.is_not

(

a

)

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

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

Definition at line 1621 of file z3py.py.

def is_not(a):
    """Return `True` if `a` is a Z3 not expression.
 
    >>> p = Bool('p')
    >>> is_not(p)
    False
    >>> is_not(Not(p))
    True
    """
    return is_app_of(a, Z3_OP_NOT)
 
 

Referenced by mk_not().

is_or()

def z3py.is_or

(

a

)

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

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

Definition at line 1597 of file z3py.py.

def is_or(a):
    """Return `True` if `a` is a Z3 or expression.
 
    >>> p, q = Bools('p q')
    >>> is_or(Or(p, q))
    True
    >>> is_or(And(p, q))
    False
    """
    return is_app_of(a, Z3_OP_OR)
 
 

is_pattern()

def z3py.is_pattern

(

a

)

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

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

Definition at line 1897 of file z3py.py.

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)
 
 

Referenced by is_quantifier(), and MultiPattern().

is_probe()

def z3py.is_probe

(

p

)

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

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

Definition at line 8511 of file z3py.py.

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)
 
 

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

is_quantifier()

def z3py.is_quantifier

(

a

)

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

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

Definition at line 2138 of file z3py.py.

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)
 
 

is_rational_value()

def z3py.is_rational_value

(

a

)

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

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

Definition at line 2718 of file z3py.py.

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())
 
 

is_re()

def z3py.is_re

(

s

)

Definition at line 10920 of file z3py.py.

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

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

is_real()

def z3py.is_real

(

a

)

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

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

Definition at line 2667 of file z3py.py.

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()
 
 

Referenced by fpRealToFP(), and fpToFP().

is_select()

def z3py.is_select

(

a

)

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

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

Definition at line 4820 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)
 
 

is_seq()

def z3py.is_seq

(

a

)

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

Definition at line 10658 of file z3py.py.

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)
 
 

Referenced by SeqRef.__gt__(), Concat(), and Extract().

is_sort()

def z3py.is_sort

(

s

)

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

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

Definition at line 646 of file z3py.py.

def is_sort(s):
    """Return `True` if `s` is a Z3 sort.
 
    >>> is_sort(IntSort())
    True
    >>> is_sort(Int('x'))
    False
    >>> is_expr(Int('x'))
    True
    """
    return isinstance(s, SortRef)
 
 

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

is_store()

def z3py.is_store

(

a

)

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

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

Definition at line 4833 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)
 

is_string()

def z3py.is_string

(

a

)

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

Definition at line 10668 of file z3py.py.

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

is_string_value()

def z3py.is_string_value

(

a

)

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

Definition at line 10676 of file z3py.py.

def is_string_value(a):
    """return 'True' if 'a' is a Z3 string constant expression.
    >>> print (is_string_value(StringVal("a")))
    True
    >>> print (is_string_value(StringVal("a") + StringVal("b")))
    False
    """
    return isinstance(a, SeqRef) and a.is_string_value()
 
 

is_sub()

def z3py.is_sub

(

a

)

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

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

Definition at line 2778 of file z3py.py.

def is_sub(a):
    """Return `True` if `a` is an expression of the form b - c.
 
    >>> x, y = Ints('x y')
    >>> is_sub(x - y)
    True
    >>> is_sub(x + y)
    False
    """
    return is_app_of(a, Z3_OP_SUB)
 
 

is_to_int()

def z3py.is_to_int

(

a

)

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

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

Definition at line 2906 of file z3py.py.

def is_to_int(a):
    """Return `True` if `a` is an expression of the form ToInt(b).
 
    >>> x = Real('x')
    >>> n = ToInt(x)
    >>> n
    ToInt(x)
    >>> is_to_int(n)
    True
    >>> is_to_int(x)
    False
    """
    return is_app_of(a, Z3_OP_TO_INT)
 
 

is_to_real()

def z3py.is_to_real

(

a

)

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

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

Definition at line 2891 of file z3py.py.

def is_to_real(a):
    """Return `True` if `a` is an expression of the form ToReal(b).
 
    >>> x = Int('x')
    >>> n = ToReal(x)
    >>> n
    ToReal(x)
    >>> is_to_real(n)
    True
    >>> is_to_real(x)
    False
    """
    return is_app_of(a, Z3_OP_TO_REAL)
 
 

is_true()

def z3py.is_true

(

a

)

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

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

Definition at line 1553 of file z3py.py.

def is_true(a):
    """Return `True` if `a` is the Z3 true expression.
 
    >>> p = Bool('p')
    >>> is_true(p)
    False
    >>> is_true(simplify(p == p))
    True
    >>> x = Real('x')
    >>> is_true(x == 0)
    False
    >>> # True is a Python Boolean expression
    >>> is_true(True)
    False
    """
    return is_app_of(a, Z3_OP_TRUE)
 
 

Referenced by AstRef.__bool__().

is_var()

def z3py.is_var

(

a

)

Return `True` if `a` is variable.

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

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

Definition at line 1278 of file z3py.py.

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
 
 

Referenced by get_var_index().

IsInt()

def z3py.IsInt

(

a

)

 Return the Z3 predicate IsInt(a).

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

Definition at line 3356 of file z3py.py.

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)
 
 

IsMember()

def z3py.IsMember	(		e,
			s
	)

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

Definition at line 4943 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)
 
 

IsSubset()

def z3py.IsSubset	(		a,
			b
	)

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

Definition at line 4954 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)
 
 

K()

def z3py.K	(		dom,
			v
	)

Return a Z3 constant array expression.

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

Definition at line 4780 of file z3py.py.

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)
 
 

Lambda()

def z3py.Lambda	(		vs,
			body
	)

Create a Z3 lambda expression.

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

Definition at line 2226 of file z3py.py.

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)
 

LastIndexOf()

def z3py.LastIndexOf	(		s,
			substr
	)

Retrieve the last index of substring within a string

Definition at line 10843 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)
 
 

Length()

def z3py.Length

(

s

)

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

Definition at line 10852 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)
 
 

LinearOrder()

def z3py.LinearOrder	(		a,
			index
	)

Definition at line 11052 of file z3py.py.

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

Loop()

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

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

Definition at line 11020 of file z3py.py.

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

LShR()

def z3py.LShR	(		a,
			b
	)

Create the Z3 expression logical right shift.

Use the operator >> for the arithmetical right shift.

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

Definition at line 4261 of file z3py.py.

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)
 
 

main_ctx()

def z3py.main_ctx

(

)

Return a reference to the global Z3 context.

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

Definition at line 238 of file z3py.py.

def main_ctx():
    """Return a reference to the global Z3 context.
 
    >>> x = Real('x')
    >>> x.ctx == main_ctx()
    True
    >>> c = Context()
    >>> c == main_ctx()
    False
    >>> x2 = Real('x', c)
    >>> x2.ctx == c
    True
    >>> eq(x, x2)
    False
    """
    global _main_ctx
    if _main_ctx is None:
        _main_ctx = Context()
    return _main_ctx
 
 

Referenced by SeqRef.__gt__(), help_simplify(), and simplify_param_descrs().

Map()

def z3py.Map	(		f,
		*	args
	)

Return a Z3 map array expression.

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

Definition at line 4757 of file z3py.py.

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)
 
 

mk_not()

def z3py.mk_not

(

a

)

Definition at line 1798 of file z3py.py.

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

Model()

def z3py.Model

(

ctx = None

)

Definition at line 6579 of file z3py.py.

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

Referenced by Optimize.set_on_model().

MultiPattern()

def z3py.MultiPattern

(

*

args

)

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

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

Definition at line 1915 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)
 
 

Not()

def z3py.Not	(		a,
			ctx = None
	)

Create a Z3 not expression or probe.

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

Definition at line 1779 of file z3py.py.

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)
 
 

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

open_log()

def z3py.open_log

(

fname

)

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

Definition at line 119 of file z3py.py.

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

Option()

def z3py.Option

(

re

)

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

Definition at line 10989 of file z3py.py.

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

Or()

def z3py.Or

(

*

args

)

Create a Z3 or-expression or or-probe.

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

Definition at line 1846 of file z3py.py.

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)
 

Referenced by ApplyResult.as_expr().

OrElse()

def z3py.OrElse	(	*	ts,
		**	ks
	)

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

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

Definition at line 8204 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
 
 

ParAndThen()

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

Alias for ParThen(t1, t2, ctx).

Definition at line 8260 of file z3py.py.

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

ParOr()

def z3py.ParOr	(	*	ts,
		**	ks
	)

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

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

Definition at line 8225 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)
 
 

parse_smt2_file()

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

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

This function is similar to parse_smt2_string().

Definition at line 9092 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)
 
 

parse_smt2_string()

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

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

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

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

Definition at line 9071 of file z3py.py.

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)
 
 

ParThen()

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

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

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

Definition at line 8244 of file z3py.py.

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)
 
 

Referenced by ParAndThen().

PartialOrder()

def z3py.PartialOrder	(		a,
			index
	)

Definition at line 11048 of file z3py.py.

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

PbEq()

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

Create a Pseudo-Boolean inequality k constraint.

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

Definition at line 8867 of file z3py.py.

def PbEq(args, k, ctx=None):
    """Create a Pseudo-Boolean inequality k constraint.
 
    >>> a, b, c = Bools('a b c')
    >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
    """
    _z3_check_cint_overflow(k, "k")
    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
    return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 

PbGe()

def z3py.PbGe	(		args,
			k
	)

Create a Pseudo-Boolean inequality k constraint.

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

Definition at line 8856 of file z3py.py.

def PbGe(args, k):
    """Create a Pseudo-Boolean inequality k constraint.
 
    >>> a, b, c = Bools('a b c')
    >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
    """
    _z3_check_cint_overflow(k, "k")
    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
    return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 

PbLe()

def z3py.PbLe	(		args,
			k
	)

Create a Pseudo-Boolean inequality k constraint.

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

Definition at line 8845 of file z3py.py.

def PbLe(args, k):
    """Create a Pseudo-Boolean inequality k constraint.
 
    >>> a, b, c = Bools('a b c')
    >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
    """
    _z3_check_cint_overflow(k, "k")
    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
    return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 

PiecewiseLinearOrder()

def z3py.PiecewiseLinearOrder	(		a,
			index
	)

Definition at line 11060 of file z3py.py.

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

Plus()

def z3py.Plus

(

re

)

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

Definition at line 10976 of file z3py.py.

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

PrefixOf()

def z3py.PrefixOf	(		a,
			b
	)

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

Definition at line 10759 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)
 
 

probe_description()

def z3py.probe_description	(		name,
			ctx = None
	)

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

>>> d = probe_description('memory')

Definition at line 8540 of file z3py.py.

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)
 
 

Referenced by describe_probes().

probes()

def z3py.probes

(

ctx = None

)

Return a list of all available probes in Z3.

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

Definition at line 8529 of file z3py.py.

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()))]
 
 

Referenced by describe_probes().

Product()

def z3py.Product

(

*

args

)

Create the product of the Z3 expressions.

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

Definition at line 8756 of file z3py.py.

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)
 
 

prove()

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

Try to prove the given claim.

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

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

Definition at line 8939 of file z3py.py.

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())
 
 

Q()

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

Return a Z3 rational a/b.

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

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

Definition at line 3197 of file z3py.py.

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))
 
 

Range()

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

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

Definition at line 11033 of file z3py.py.

def Range(lo, hi, ctx=None):
    """Create the range regular expression over two sequences of length 1
    >>> range = Range("a","z")
    >>> print(simplify(InRe("b", range)))
    True
    >>> print(simplify(InRe("bb", range)))
    False
    """
    lo = _coerce_seq(lo, ctx)
    hi = _coerce_seq(hi, ctx)
    return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
 
# Special Relations
 
 

RatVal()

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

Return a Z3 rational a/b.

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

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

Definition at line 3181 of file z3py.py.

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))
 
 

Referenced by Q().

Re()

def z3py.Re	(		s,
			ctx = None
	)

The regular expression that accepts sequence 's'
>>> s1 = Re("ab")
>>> s2 = Re(StringVal("ab"))
>>> s3 = Re(Unit(BoolVal(True)))

Definition at line 10885 of file z3py.py.

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
 

Real()

def z3py.Real	(		name,
			ctx = None
	)

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

>>> x = Real('x')
>>> is_real(x)
True
>>> is_real(x + 1)
True

Definition at line 3263 of file z3py.py.

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)
 
 

Referenced by Reals(), and RealVector().

Reals()

def z3py.Reals	(		names,
			ctx = None
	)

Return a tuple of real constants.

>>> x, y, z = Reals('x y z')
>>> Sum(x, y, z)
x + y + z
>>> Sum(x, y, z).sort()
Real

Definition at line 3276 of file z3py.py.

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]
 
 

RealSort()

def z3py.RealSort

(

ctx = None

)

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

>>> RealSort()
Real
>>> x = Const('x', RealSort())
>>> is_real(x)
True
>>> is_int(x)
False
>>> x.sort() == RealSort()
True

Definition at line 3117 of file z3py.py.

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)
 
 

Referenced by FreshReal(), Real(), RealVal(), and RealVar().

RealVal()

def z3py.RealVal	(		val,
			ctx = None
	)

Return a Z3 real value.

`val` may be a Python int, long, float or string representing a number in decimal or rational notation.
If `ctx=None`, then the global context is used.

>>> RealVal(1)
1
>>> RealVal(1).sort()
Real
>>> RealVal("3/5")
3/5
>>> RealVal("1.5")
3/2

Definition at line 3162 of file z3py.py.

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)
 
 

Referenced by Cbrt(), AlgebraicNumRef.index(), RatVal(), and Sqrt().

RealVar()

def z3py.RealVar	(		idx,
			ctx = None
	)

Create a real free variable. Free variables are used to create quantified formulas.
They are also used to create polynomials.

>>> RealVar(0)
Var(0)

Definition at line 1451 of file z3py.py.

def RealVar(idx, ctx=None):
    """
    Create a real free variable. Free variables are used to create quantified formulas.
    They are also used to create polynomials.
 
    >>> RealVar(0)
    Var(0)
    """
    return Var(idx, RealSort(ctx))
 
 

Referenced by RealVarVector().

RealVarVector()

def z3py.RealVarVector	(		n,
			ctx = None
	)

Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1

>>> x0, x1, x2, x3 = RealVarVector(4)
>>> x2
Var(2)

Definition at line 1462 of file z3py.py.

def RealVarVector(n, ctx=None):
    """
    Create a list of Real free variables.
    The variables have ids: 0, 1, ..., n-1
 
    >>> x0, x1, x2, x3 = RealVarVector(4)
    >>> x2
    Var(2)
    """
    return [RealVar(i, ctx) for i in range(n)]
 

RealVector()

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

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

>>> X = RealVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
>>> Sum(X).sort()
Real

Definition at line 3291 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)]
 
 

RecAddDefinition()

def z3py.RecAddDefinition	(		f,
			args,
			body
	)

Set the body of a recursive function.
   Recursive definitions can be simplified if they are applied to ground
   arguments.
>>> ctx = Context()
>>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
>>> n = Int('n', ctx)
>>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
>>> simplify(fac(5))
120
>>> s = Solver(ctx=ctx)
>>> s.add(fac(n) < 3)
>>> s.check()
sat
>>> s.model().eval(fac(5))
120

Definition at line 924 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)
 

RecFunction()

def z3py.RecFunction	(		name,
		*	sig
	)

Create a new Z3 recursive with the given sorts.

Definition at line 906 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)
 
 

Repeat()

def z3py.Repeat	(		t,
			max = 4294967295,
			ctx = None
	)

Return a tactic that keeps applying `t` until the goal is not modified anymore
or the maximum number of iterations `max` is reached.

>>> x, y = Ints('x y')
>>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
>>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
>>> r = t(c)
>>> for subgoal in r: print(subgoal)
[x == 0, y == 0, x > y]
[x == 0, y == 1, x > y]
[x == 1, y == 0, x > y]
[x == 1, y == 1, x > y]
>>> t = Then(t, Tactic('propagate-values'))
>>> t(c)
[[x == 1, y == 0]]

Definition at line 8293 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)
 
 

RepeatBitVec()

def z3py.RepeatBitVec	(		n,
			a
	)

Return an expression representing `n` copies of `a`.

>>> x = BitVec('x', 8)
>>> n = RepeatBitVec(4, x)
>>> n
RepeatBitVec(4, x)
>>> n.size()
32
>>> v0 = BitVecVal(10, 4)
>>> print("%.x" % v0.as_long())
a
>>> v = simplify(RepeatBitVec(4, v0))
>>> v.size()
16
>>> print("%.x" % v.as_long())
aaaa

Definition at line 4383 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)
 
 

Replace()

def z3py.Replace	(		s,
			src,
			dst
	)

Replace the first occurrence of 'src' by 'dst' in 's'
>>> r = Replace("aaa", "a", "b")
>>> simplify(r)
"baa"

Definition at line 10808 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)
 
 

reset_params()

def z3py.reset_params

(

)

Reset all global (or module) parameters.

Definition at line 294 of file z3py.py.

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

ReSort()

def z3py.ReSort

(

s

)

Definition at line 10904 of file z3py.py.

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")
 
 

RNA()

def z3py.RNA

(

ctx = None

)

Definition at line 9507 of file z3py.py.

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

Referenced by get_default_rounding_mode().

RNE()

def z3py.RNE

(

ctx = None

)

Definition at line 9497 of file z3py.py.

def RNE(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
 
 

Referenced by get_default_rounding_mode().

RotateLeft()

def z3py.RotateLeft	(		a,
			b
	)

Return an expression representing `a` rotated to the left `b` times.

>>> a, b = BitVecs('a b', 16)
>>> RotateLeft(a, b)
RotateLeft(a, b)
>>> simplify(RotateLeft(a, 0))
a
>>> simplify(RotateLeft(a, 16))
a

Definition at line 4293 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)
 
 

RotateRight()

def z3py.RotateRight	(		a,
			b
	)

Return an expression representing `a` rotated to the right `b` times.

>>> a, b = BitVecs('a b', 16)
>>> RotateRight(a, b)
RotateRight(a, b)
>>> simplify(RotateRight(a, 0))
a
>>> simplify(RotateRight(a, 16))
a

Definition at line 4309 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)
 
 

RoundNearestTiesToAway()

def z3py.RoundNearestTiesToAway

(

ctx = None

)

Definition at line 9502 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)
 
 

RoundNearestTiesToEven()

def z3py.RoundNearestTiesToEven

(

ctx = None

)

Definition at line 9492 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)
 
 

RoundTowardNegative()

def z3py.RoundTowardNegative

(

ctx = None

)

Definition at line 9522 of file z3py.py.

def RoundTowardNegative(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
 
 

RoundTowardPositive()

def z3py.RoundTowardPositive

(

ctx = None

)

Definition at line 9512 of file z3py.py.

def RoundTowardPositive(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
 
 

RoundTowardZero()

def z3py.RoundTowardZero

(

ctx = None

)

Definition at line 9532 of file z3py.py.

def RoundTowardZero(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
 
 

RTN()

def z3py.RTN

(

ctx = None

)

Definition at line 9527 of file z3py.py.

def RTN(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
 
 

Referenced by get_default_rounding_mode().

RTP()

def z3py.RTP

(

ctx = None

)

Definition at line 9517 of file z3py.py.

def RTP(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
 
 

Referenced by get_default_rounding_mode().

RTZ()

def z3py.RTZ

(

ctx = None

)

Definition at line 9537 of file z3py.py.

def RTZ(ctx=None):
    ctx = _get_ctx(ctx)
    return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
 
 

Referenced by get_default_rounding_mode().

Select()

def z3py.Select	(		a,
			i
	)

Return a Z3 select array expression.

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

Definition at line 4742 of file z3py.py.

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

SeqSort()

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

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)
 
 

set_default_fp_sort()

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

Definition at line 9153 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
 
 

set_default_rounding_mode()

def z3py.set_default_rounding_mode	(		rm,
			ctx = None
	)

Definition at line 9140 of file z3py.py.

def set_default_rounding_mode(rm, ctx=None):
    global _dflt_rounding_mode
    if is_fprm_value(rm):
        _dflt_rounding_mode = rm.decl().kind()
    else:
        _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode")
        _dflt_rounding_mode = rm
 
 

set_option()

def z3py.set_option	(	*	args,
		**	kws
	)

Alias for 'set_param' for backward compatibility.

Definition at line 300 of file z3py.py.

def set_option(*args, **kws):
    """Alias for 'set_param' for backward compatibility.
    """
    return set_param(*args, **kws)
 
 

set_param()

def z3py.set_param	(	*	args,
		**	kws
	)

Set Z3 global (or module) parameters.

>>> set_param(precision=10)

Definition at line 270 of file z3py.py.

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
 
 

Referenced by set_option().

SetAdd()

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 4900 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)
 
 

SetComplement()

def z3py.SetComplement

(

s

)

 The complement of set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
complement(a)

Definition at line 4922 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)
 
 

SetDel()

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 4911 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)
 
 

SetDifference()

def z3py.SetDifference	(		a,
			b
	)

 The set difference of a and b
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetDifference(a, b)
setminus(a, b)

Definition at line 4932 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)
 
 

SetHasSize()

def z3py.SetHasSize	(		a,
			k
	)

Definition at line 4814 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)
 
 

SetIntersect()

def z3py.SetIntersect

(

*

args

)

 Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetIntersect(a, b)
intersection(a, b)

Definition at line 4887 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)
 
 

SetSort()

def z3py.SetSort

(

s

)

Sets.

 Create a set sort over element sort s

Definition at line 4851 of file z3py.py.

def SetSort(s):
    """ Create a set sort over element sort s"""
    return ArraySort(s, BoolSort())
 
 

SetUnion()

def z3py.SetUnion

(

*

args

)

 Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetUnion(a, b)
union(a, b)

Definition at line 4874 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)
 
 

SignExt()

def z3py.SignExt	(		n,
			a
	)

Return a bit-vector expression with `n` extra sign-bits.

>>> x = BitVec('x', 16)
>>> n = SignExt(8, x)
>>> n.size()
24
>>> n
SignExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(SignExt(6, v0))
>>> v
254
>>> v.size()
8
>>> print("%.x" % v.as_long())
fe

Definition at line 4325 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)
 
 

SimpleSolver()

def z3py.SimpleSolver	(		ctx = None,
			logFile = None
	)

Return a simple general purpose solver with limited amount of preprocessing.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat

Definition at line 7293 of file z3py.py.

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)
 

simplify()

def z3py.simplify	(		a,
		*	arguments,
		**	keywords
	)

Utils.

Simplify the expression `a` using the given options.

This function has many options. Use `help_simplify` to obtain the complete list.

>>> x = Int('x')
>>> y = Int('y')
>>> simplify(x + 1 + y + x + 1)
2 + 2*x + y
>>> simplify((x + 1)*(y + 1), som=True)
1 + x + y + x*y
>>> simplify(Distinct(x, y, 1), blast_distinct=True)
And(Not(x == y), Not(x == 1), Not(y == 1))
>>> simplify(And(x == 0, y == 1), elim_and=True)
Not(Or(Not(x == 0), Not(y == 1)))

Definition at line 8645 of file z3py.py.

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)
 
 

Referenced by Q(), and RatVal().

simplify_param_descrs()

def z3py.simplify_param_descrs

(

)

Return the set of parameter descriptions for Z3 `simplify` procedure.

Definition at line 8675 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())
 
 

solve()

def z3py.solve	(	*	args,
		**	keywords
	)

Solve the constraints `*args`.

This is a simple function for creating demonstrations. It creates a solver,
configure it using the options in `keywords`, adds the constraints
in `args`, and invokes check.

>>> a = Int('a')
>>> solve(a > 0, a < 2)
[a = 1]

Definition at line 8878 of file z3py.py.

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())
 
 

solve_using()

def z3py.solve_using	(		s,
		*	args,
		**	keywords
	)

Solve the constraints `*args` using solver `s`.

This is a simple function for creating demonstrations. It is similar to `solve`,
but it uses the given solver `s`.
It configures solver `s` using the options in `keywords`, adds the constraints
in `args`, and invokes check.

Definition at line 8908 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())
 
 

SolverFor()

def z3py.SolverFor	(		logic,
			ctx = None,
			logFile = None
	)

Create a solver customized for the given logic.

The parameter `logic` is a string. It should be contains
the name of a SMT-LIB logic.
See http://www.smtlib.org/ for the name of all available logics.

>>> s = SolverFor("QF_LIA")
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> s.check()
sat
>>> s.model()
[x = 1]

Definition at line 7272 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)
 
 

Sqrt()

def z3py.Sqrt	(		a,
			ctx = None
	)

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

>>> x = Real('x')
>>> Sqrt(x)
x**(1/2)

Definition at line 3373 of file z3py.py.

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"
 
 

SRem()

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

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)
 
 

Star()

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

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

Store()

def z3py.Store	(		a,
			i,
			v
	)

Return a Z3 store array expression.

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

Definition at line 4725 of file z3py.py.

def Store(a, i, v):
    """Return a Z3 store array expression.
 
    >>> a    = Array('a', IntSort(), IntSort())
    >>> i, v = Ints('i v')
    >>> s    = Store(a, i, v)
    >>> s.sort()
    Array(Int, Int)
    >>> prove(s[i] == v)
    proved
    >>> j    = Int('j')
    >>> prove(Implies(i != j, s[j] == a[j]))
    proved
    """
    return Update(a, i, v)
 
 

String()

def z3py.String	(		name,
			ctx = None
	)

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

>>> x = String('x')

Definition at line 10693 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)
 
 

Referenced by Strings().

Strings()

def z3py.Strings	(		names,
			ctx = None
	)

Return a tuple of String constants. 

Definition at line 10702 of file z3py.py.

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]
 
 

StringSort()

def z3py.StringSort

(

ctx = None

)

Create a string sort
>>> s = StringSort()
>>> print(s)
String

Definition at line 10569 of file z3py.py.

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)
 
 

Referenced by String().

StringVal()

def z3py.StringVal	(		s,
			ctx = None
	)

create a string expression

Definition at line 10686 of file z3py.py.

def StringVal(s, ctx=None):
    """create a string expression"""
    s = "".join(str(ch) if ord(ch) < 128 else "\\u{%x}" % (ord(ch)) for ch in s)
    ctx = _get_ctx(ctx)
    return SeqRef(Z3_mk_lstring(ctx.ref(), len(s), s), ctx)
 
 

Referenced by SeqRef.__gt__(), ExprRef.children(), Extract(), and AlgebraicNumRef.index().

StrToInt()

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 10862 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)
 
 

SubSeq()

def z3py.SubSeq	(		s,
			offset,
			length
	)

Extract substring or subsequence starting at offset

Definition at line 10715 of file z3py.py.

def SubSeq(s, offset, length):
    """Extract substring or subsequence starting at offset"""
    return Extract(s, offset, length)
 
 

substitute()

def z3py.substitute	(		t,
		*	m
	)

Apply substitution m on t, m is a list of pairs of the form (from, to).
Every occurrence in t of from is replaced with to.

>>> x = Int('x')
>>> y = Int('y')
>>> substitute(x + 1, (x, y + 1))
y + 1 + 1
>>> f = Function('f', IntSort(), IntSort())
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
1 + 1

Definition at line 8680 of file z3py.py.

def substitute(t, *m):
    """Apply substitution m on t, m is a list of pairs of the form (from, to).
    Every occurrence in t of from is replaced with to.
 
    >>> x = Int('x')
    >>> y = Int('y')
    >>> substitute(x + 1, (x, y + 1))
    y + 1 + 1
    >>> f = Function('f', IntSort(), IntSort())
    >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
    1 + 1
    """
    if isinstance(m, tuple):
        m1 = _get_args(m)
        if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1):
            m = m1
    if z3_debug():
        _z3_assert(is_expr(t), "Z3 expression expected")
        _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(
            p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
    num = len(m)
    _from = (Ast * num)()
    _to = (Ast * num)()
    for i in range(num):
        _from[i] = m[i][0].as_ast()
        _to[i] = m[i][1].as_ast()
    return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
 
 

substitute_vars()

def z3py.substitute_vars	(		t,
		*	m
	)

Substitute the free variables in t with the expression in m.

>>> v0 = Var(0, IntSort())
>>> v1 = Var(1, IntSort())
>>> x  = Int('x')
>>> f  = Function('f', IntSort(), IntSort(), IntSort())
>>> # replace v0 with x+1 and v1 with x
>>> substitute_vars(f(v0, v1), x + 1, x)
f(x + 1, x)

Definition at line 8709 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)
 
 

SubString()

def z3py.SubString	(		s,
			offset,
			length
	)

Extract substring or subsequence starting at offset

Definition at line 10710 of file z3py.py.

def SubString(s, offset, length):
    """Extract substring or subsequence starting at offset"""
    return Extract(s, offset, length)
 
 

SuffixOf()

def z3py.SuffixOf	(		a,
			b
	)

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

Definition at line 10774 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)
 
 

Sum()

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

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)
 
 

tactic_description()

def z3py.tactic_description	(		name,
			ctx = None
	)

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

>>> d = tactic_description('simplify')

Definition at line 8334 of file z3py.py.

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)
 
 

Referenced by describe_tactics().

tactics()

def z3py.tactics

(

ctx = None

)

Return a list of all available tactics in Z3.

>>> l = tactics()
>>> l.count('simplify') == 1
True

Definition at line 8323 of file z3py.py.

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()))]
 
 

Referenced by describe_tactics(), and z3.par_or().

Then()

def z3py.Then	(	*	ts,
		**	ks
	)

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

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

Definition at line 8191 of file z3py.py.

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)
 
 

to_symbol()

def z3py.to_symbol	(		s,
			ctx = None
	)

Convert an integer or string into a Z3 symbol.

Definition at line 129 of file z3py.py.

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)
 
 

Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DeclareSort(), EnumSort(), FiniteDomainSort(), FP(), Function(), ParamDescrsRef.get_documentation(), ParamDescrsRef.get_kind(), Int(), is_quantifier(), prove(), Real(), RecFunction(), ParamsRef.set(), Fixedpoint.set_predicate_representation(), SolverFor(), String(), and Fixedpoint.update_rule().

ToInt()

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

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)
 
 

ToReal()

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

def ToReal(a):
    """ Return the Z3 expression ToReal(a).
 
    >>> x = Int('x')
    >>> x.sort()
    Int
    >>> n = ToReal(x)
    >>> n
    ToReal(x)
    >>> n.sort()
    Real
    """
    if z3_debug():
        _z3_assert(a.is_int(), "Z3 integer expression expected.")
    ctx = a.ctx
    return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
 
 

TransitiveClosure()

def z3py.TransitiveClosure

(

f

)

Given a binary relation R, such that the two arguments have the same sort
create the transitive closure relation R+.
The transitive closure R+ is a new relation.

Definition at line 11064 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)
 
 

TreeOrder()

def z3py.TreeOrder	(		a,
			index
	)

Definition at line 11056 of file z3py.py.

def TreeOrder(a, index):
    return FuncDeclRef(Z3_mk_tree_order(a.ctx_ref(), a.ast, index), a.ctx)
 
 

TryFor()

def z3py.TryFor	(		t,
			ms,
			ctx = None
	)

Return a tactic that applies `t` to a given goal for `ms` milliseconds.

If `t` does not terminate in `ms` milliseconds, then it fails.

Definition at line 8314 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)
 
 

TupleSort()

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

Create a named tuple sort base on a set of underlying sorts
Example:
    >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])

Definition at line 5293 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))]
 
 

UDiv()

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

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)
 
 

UGE()

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

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)
 
 

UGT()

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

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)
 
 

ULE()

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

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)
 
 

ULT()

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

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)
 
 

Union()

def z3py.Union

(

*

args

)

Create union of regular expressions.
>>> re = Union(Re("a"), Re("b"), Re("c"))
>>> print (simplify(InRe("d", re)))
False

Definition at line 10938 of file z3py.py.

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)
 
 

Referenced by ReRef.__add__().

Unit()

def z3py.Unit

(

a

)

Create a singleton sequence

Definition at line 10754 of file z3py.py.

def Unit(a):
    """Create a singleton sequence"""
    return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)
 
 

Update()

def z3py.Update	(		a,
			i,
			v
	)

Return a Z3 store array expression.

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

Definition at line 4692 of file z3py.py.

def Update(a, i, v):
    """Return a Z3 store array expression.
 
    >>> a    = Array('a', IntSort(), IntSort())
    >>> i, v = Ints('i v')
    >>> s    = Update(a, i, v)
    >>> s.sort()
    Array(Int, Int)
    >>> prove(s[i] == v)
    proved
    >>> j    = Int('j')
    >>> prove(Implies(i != j, s[j] == a[j]))
    proved
    """
    if z3_debug():
        _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
    i = a.sort().domain().cast(i)
    v = a.sort().range().cast(v)
    ctx = a.ctx
    return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
 
 

Referenced by Store().

URem()

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

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)
 
 

user_prop_diseq()

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

Definition at line 11152 of file z3py.py.

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

user_prop_eq()

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

Definition at line 11145 of file z3py.py.

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

user_prop_final()

def z3py.user_prop_final	(		ctx,
			cb
	)

Definition at line 11138 of file z3py.py.

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

user_prop_fixed()

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

Definition at line 11131 of file z3py.py.

def user_prop_fixed(ctx, cb, id, value):
    prop = _prop_closures.get(ctx)
    prop.cb = cb
    prop.fixed(id, _to_expr_ref(ctypes.c_void_p(value), prop.ctx()))
    prop.cb = None
 
 

user_prop_fresh()

def z3py.user_prop_fresh	(		id,
			ctx
	)

Definition at line 11124 of file z3py.py.

def user_prop_fresh(id, ctx):
    _prop_closures.set_threaded()
    new_prop = UsePropagateBase(None, ctx)
    _prop_closures.set(new_prop.id, new_prop.fresh())
    return ctypes.c_void_p(new_prop.id)
 
 

user_prop_pop()

def z3py.user_prop_pop	(		ctx,
			num_scopes
	)

Definition at line 11120 of file z3py.py.

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

user_prop_push()

def z3py.user_prop_push

(

ctx

)

Definition at line 11116 of file z3py.py.

def user_prop_push(ctx):
    _prop_closures.get(ctx).push()
 
 

Var()

def z3py.Var	(		idx,
			s
	)

Create a Z3 free variable. Free variables are used to create quantified formulas.

>>> Var(0, IntSort())
Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort()))
False

Definition at line 1438 of file z3py.py.

def Var(idx, s):
    """Create a Z3 free variable. Free variables are used to create quantified formulas.
 
    >>> Var(0, IntSort())
    Var(0)
    >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
    False
    """
    if z3_debug():
        _z3_assert(is_sort(s), "Z3 sort expected")
    return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
 
 

Referenced by RealVar().

When()

def z3py.When	(		p,
			t,
			ctx = None
	)

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

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

Definition at line 8608 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)
 
 

With()

def z3py.With	(		t,
		*	args,
		**	keys
	)

Return a tactic that applies tactic `t` using the given configuration options.

>>> x, y = Ints('x y')
>>> t = With(Tactic('simplify'), som=True)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]

Definition at line 8265 of file z3py.py.

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)
 
 

WithParams()

def z3py.WithParams	(		t,
			p
	)

Return a tactic that applies tactic `t` using the given configuration options.

>>> x, y = Ints('x y')
>>> p = ParamsRef()
>>> p.set("som", True)
>>> t = WithParams(Tactic('simplify'), p)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]

Definition at line 8279 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)
 
 

Xor()

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

Create a Z3 Xor expression.

>>> p, q = Bools('p q')
>>> Xor(p, q)
Xor(p, q)
>>> simplify(Xor(p, q))
Not(p) == q

Definition at line 1763 of file z3py.py.

def Xor(a, b, ctx=None):
    """Create a Z3 Xor expression.
 
    >>> p, q = Bools('p q')
    >>> Xor(p, q)
    Xor(p, q)
    >>> simplify(Xor(p, q))
    Not(p) == q
    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
    s = BoolSort(ctx)
    a = s.cast(a)
    b = s.cast(b)
    return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
 
 

z3_debug()

def z3py.z3_debug

(

)

Definition at line 64 of file z3py.py.

def z3_debug():
    global Z3_DEBUG
    return Z3_DEBUG
 
 

Referenced by FuncDeclRef.__call__(), Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), ExprRef.children(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), describe_probes(), Distinct(), FuncDeclRef.domain(), EnumSort(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpIsPositive(), fpNeg(), FPSort(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), AlgebraicNumRef.index(), Intersect(), is_quantifier(), is_sort(), IsInt(), K(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), QuantifierRef.pattern(), prove(), RatVal(), RealSort(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), simplify(), solve_using(), substitute(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Union(), Update(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().

z3_error_handler()

def z3py.z3_error_handler	(		c,
			e
	)

Definition at line 179 of file z3py.py.

def z3_error_handler(c, e):
    # Do nothing error handler, just avoid exit(0)
    # The wrappers in z3core.py will raise a Z3Exception if an error is detected
    return
 
 

ZeroExt()

def z3py.ZeroExt	(		n,
			a
	)

Return a bit-vector expression with `n` extra zero-bits.

>>> x = BitVec('x', 16)
>>> n = ZeroExt(8, x)
>>> n.size()
24
>>> n
ZeroExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(ZeroExt(6, v0))
>>> v
2
>>> v.size()
8

Definition at line 4355 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

sat

sat = CheckSatResult(Z3_L_TRUE)

Definition at line 6782 of file z3py.py.

unknown

unknown = CheckSatResult(Z3_L_UNDEF)

Definition at line 6784 of file z3py.py.

unsat

unsat = CheckSatResult(Z3_L_FALSE)

Definition at line 6783 of file z3py.py.

Z3_DEBUG

Z3_DEBUG = __debug__

Definition at line 61 of file z3py.py.