z3py Namespace Reference

Data Structures
class	Context
class	Z3PPObject
	ASTs base class. More...
class	AstRef
class	SortRef
class	FuncDeclRef
	Function Declarations. More...
class	ExprRef
	Expressions. More...
class	BoolSortRef
	Booleans. More...
class	BoolRef
class	PatternRef
	Patterns. More...
class	QuantifierRef
	Quantifiers. More...
class	ArithSortRef
	Arithmetic. More...
class	ArithRef
class	IntNumRef
class	RatNumRef
class	AlgebraicNumRef
class	BitVecSortRef
	Bit-Vectors. More...
class	BitVecRef
class	BitVecNumRef
class	ArraySortRef
	Arrays. More...
class	ArrayRef
class	Datatype
class	ScopedConstructor
class	ScopedConstructorList
class	DatatypeSortRef
class	DatatypeRef
class	ParamsRef
	Parameter Sets. More...
class	ParamDescrsRef
class	Goal
class	AstVector
class	AstMap
class	FuncEntry
class	FuncInterp
class	ModelRef
class	Statistics
	Statistics. More...
class	CheckSatResult
class	Solver
class	Fixedpoint
	Fixedpoint. More...
class	FiniteDomainSortRef
class	OptimizeObjective
	Optimize. More...
class	Optimize
class	ApplyResult
class	Tactic
class	Probe
class	FPSortRef
	FP Sorts. More...
class	FPRMSortRef
class	FPRef
	FP Expressions. More...
class	FPRMRef
class	FPNumRef
	FP Numerals. More...
Functions
def	enable_trace
def	disable_trace
def	get_version_string
def	get_version
def	open_log
def	append_log
def	to_symbol
def	main_ctx
def	set_param
def	reset_params
def	set_option
def	get_param
def	is_ast
def	eq
def	is_sort
def	DeclareSort
def	is_func_decl
def	Function
def	is_expr
def	is_app
def	is_const
def	is_var
def	get_var_index
def	is_app_of
def	If
def	Distinct
def	Const
def	Consts
def	Var
def	RealVar
def	RealVarVector
def	is_bool
def	is_true
def	is_false
def	is_and
def	is_or
def	is_not
def	is_eq
def	is_distinct
def	BoolSort
def	BoolVal
def	Bool
def	Bools
def	BoolVector
def	FreshBool
def	Implies
def	Xor
def	Not
def	And
def	Or
def	is_pattern
def	MultiPattern
def	is_quantifier
def	ForAll
def	Exists
def	is_arith_sort
def	is_arith
def	is_int
def	is_real
def	is_int_value
def	is_rational_value
def	is_algebraic_value
def	is_add
def	is_mul
def	is_sub
def	is_div
def	is_idiv
def	is_mod
def	is_le
def	is_lt
def	is_ge
def	is_gt
def	is_is_int
def	is_to_real
def	is_to_int
def	IntSort
def	RealSort
def	IntVal
def	RealVal
def	RatVal
def	Q
def	Int
def	Ints
def	IntVector
def	FreshInt
def	Real
def	Reals
def	RealVector
def	FreshReal
def	ToReal
def	ToInt
def	IsInt
def	Sqrt
def	Cbrt
def	is_bv_sort
def	is_bv
def	is_bv_value
def	BV2Int
def	BitVecSort
def	BitVecVal
def	BitVec
def	BitVecs
def	Concat
def	Extract
def	ULE
def	ULT
def	UGE
def	UGT
def	UDiv
def	URem
def	SRem
def	LShR
def	RotateLeft
def	RotateRight
def	SignExt
def	ZeroExt
def	RepeatBitVec
def	BVRedAnd
def	BVRedOr
def	is_array
def	is_const_array
def	is_K
def	is_map
def	is_default
def	get_map_func
def	ArraySort
def	Array
def	Update
def	Default
def	Store
def	Select
def	Map
def	K
def	is_select
def	is_store
def	CreateDatatypes
def	EnumSort
def	args2params
def	is_as_array
def	get_as_array_func
def	SolverFor
def	SimpleSolver
def	FiniteDomainSort
def	AndThen
def	Then
def	OrElse
def	ParOr
def	ParThen
def	ParAndThen
def	With
def	Repeat
def	TryFor
def	tactics
def	tactic_description
def	describe_tactics
def	is_probe
def	probes
def	probe_description
def	describe_probes
def	FailIf
def	When
def	Cond
def	simplify
	Utils.
def	help_simplify
def	simplify_param_descrs
def	substitute
def	substitute_vars
def	Sum
def	Product
def	solve
def	solve_using
def	prove
def	parse_smt2_string
def	parse_smt2_file
def	Interpolant
def	tree_interpolant
def	binary_interpolant
def	sequence_interpolant
def	get_default_rounding_mode
def	set_default_rounding_mode
def	get_default_fp_sort
def	set_default_fp_sort
def	Float16
def	FloatHalf
def	Float32
def	FloatSingle
def	Float64
def	Float128
def	is_fp_sort
def	is_fprm_sort
def	RoundNearestTiesToEven
def	RNE
def	RoundNearestTiesToAway
def	RNA
def	RoundTowardPositive
def	RTP
def	RoundTowardNegative
def	RTN
def	RoundTowardZero
def	RTZ
def	is_fprm
def	is_fprm_value
def	is_fp
def	is_fp_value
def	FPSort
def	fpNaN
def	fpPlusInfinity
def	fpMinusInfinity
def	fpInfinity
def	fpPlusZero
def	fpMinusZero
def	fpZero
def	FPVal
def	FP
def	FPs
def	fpAbs
def	fpNeg
def	fpAdd
def	fpSub
def	fpMul
def	fpDiv
def	fpRem
def	fpMin
def	fpMax
def	fpFMA
def	fpSqrt
def	fpRoundToIntegral
def	fpIsNaN
def	fpIsInfinite
def	fpIsZero
def	fpIsNormal
def	fpIsSubnormal
def	fpIsNegative
def	fpIsPositive
def	fpLT
def	fpLEQ
def	fpGT
def	fpGEQ
def	fpEQ
def	fpNEQ
def	fpFP
def	fpToFP
def	fpToFPUnsigned
def	fpToSBV
def	fpToUBV
def	fpToReal
def	fpToIEEEBV
Variables
tuple	_error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
tuple	_Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
	_main_ctx = None
tuple	sat = CheckSatResult(Z3_L_TRUE)
tuple	unsat = CheckSatResult(Z3_L_FALSE)
tuple	unknown = CheckSatResult(Z3_L_UNDEF)
	_dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
	Floating-Point Arithmetic.
int	_dflt_fpsort_ebits = 11
int	_dflt_fpsort_sbits = 53

---

Function Documentation

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

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

def And(*args):
    """Create a Z3 and-expression or and-probe. 
    
    >>> p, q, r = Bools('p q r')
    >>> And(p, q, r)
    And(p, q, r)
    >>> P = BoolVector('p', 5)
    >>> And(P)
    And(p__0, p__1, p__2, p__3, p__4)
    """
    last_arg = None
    if len(args) > 0:
        last_arg = args[len(args)-1]
    if isinstance(last_arg, Context):
        ctx = args[len(args)-1]
        args = args[:len(args)-1]
    else:
        ctx = main_ctx()
    args = _get_args(args)
    ctx_args  = _ctx_from_ast_arg_list(args, ctx)
    if __debug__:
        _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
        _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
    if _has_probe(args):
        return _probe_and(args, ctx)
    else:
        args  = _coerce_expr_list(args, ctx)
        _args, sz = _to_ast_array(args)
        return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)

def z3py.AndThen	(		ts,
			ks
	)

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

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

Definition at line 6759 of file z3py.py.

Referenced by Context.Then(), and Then().

def AndThen(*ts, **ks):
    """Return a tactic that applies the tactics in `*ts` in sequence.
    
    >>> x, y = Ints('x y')
    >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
    >>> t(And(x == 0, y > x + 1))
    [[Not(y <= 1)]]
    >>> t(And(x == 0, y > x + 1)).as_expr()
    Not(y <= 1)
    """
    if __debug__:
        _z3_assert(len(ts) >= 2, "At least two arguments expected")
    ctx = ks.get('ctx', None)
    num = len(ts)
    r = ts[0]
    for i in range(num - 1):
        r = _and_then(r, ts[i+1], ctx)
    return r

def z3py.append_log

(

s

)

Append user-defined string to interaction log. 

Definition at line 90 of file z3py.py.

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

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

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

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

Definition at line 4527 of file z3py.py.

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

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

    >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
    (params model true relevancy 2 elim_and true)
    """
    if __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 == None:
            prev = a
        else:
            r.set(prev, a)
            prev = None
    for k in keywords:
        v = keywords[k]
        r.set(k, v)
    return r

def z3py.Array	(		name,
			dom,
			rng
	)

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

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

Definition at line 4025 of file z3py.py.

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

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

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

def z3py.ArraySort	(		d,
			r
	)

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

Referenced by Array(), Sort.create(), ArraySortRef.domain(), Context.mkArraySort(), Context.MkArraySort(), and ArraySortRef.range().

def ArraySort(d, r):
    """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))
    """
    if __debug__:
        _z3_assert(is_sort(d), "Z3 sort expected")
        _z3_assert(is_sort(r), "Z3 sort expected")
        _z3_assert(d.ctx == r.ctx, "Context mismatch")
    ctx = d.ctx
    return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)

def z3py.binary_interpolant	(		a,
			b,
			p = None,
			ctx = None
	)

Compute an interpolant for a binary conjunction.

If a & b is unsatisfiable, returns an interpolant for a & b.
This is a formula phi such that

1) a implies phi
2) b implies not phi
3) All the uninterpreted symbols of phi occur in both a and b.

If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a &b.

If parameters p are supplied, these are used in creating the
solver that determines satisfiability.

x = Int('x')
print binary_interpolant(x<0,x>2)
Not(x >= 0)

Definition at line 7590 of file z3py.py.

def binary_interpolant(a,b,p=None,ctx=None):
    """Compute an interpolant for a binary conjunction.

    If a & b is unsatisfiable, returns an interpolant for a & b.
    This is a formula phi such that

    1) a implies phi
    2) b implies not phi
    3) All the uninterpreted symbols of phi occur in both a and b.

    If a & b is satisfiable, raises an object of class ModelRef
    that represents a model of a &b.

    If parameters p are supplied, these are used in creating the
    solver that determines satisfiability.

    x = Int('x')
    print binary_interpolant(x<0,x>2)
    Not(x >= 0)
    """
    f = And(Interpolant(a),b)
    return tree_interpolant(f,p,ctx)[0]

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

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

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

    >>> x  = BitVec('x', 16)
    >>> is_bv(x)
    True
    >>> x.size()
    16
    >>> x.sort()
    BitVec(16)
    >>> word = BitVecSort(16)
    >>> x2 = BitVec('x', word)
    >>> eq(x, x2)
    True
    """
    if isinstance(bv, BitVecSortRef):
        ctx = bv.ctx
    else:
        ctx = _get_ctx(ctx)
        bv = BitVecSort(bv, ctx)
    return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)

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

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

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

Definition at line 3513 of file z3py.py.

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

def BitVecs(names, bv, ctx=None):
    """Return a tuple of bit-vector constants of size bv. 
    
    >>> x, y, z = BitVecs('x y z', 16)
    >>> x.size()
    16
    >>> x.sort()
    BitVec(16)
    >>> Sum(x, y, z)
    0 + x + y + z
    >>> Product(x, y, z)
    1*x*y*z
    >>> simplify(Product(x, y, z))
    x*y*z
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [BitVec(name, bv, ctx) for name in names]

def z3py.BitVecSort	(		sz,
			ctx = None
	)

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

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

Definition at line 3460 of file z3py.py.

Referenced by BitVec(), BitVecSortRef.cast(), Sort.create(), fpToSBV(), fpToUBV(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), and BitVecRef.sort().

def BitVecSort(sz, ctx=None):
    """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.

    >>> Byte = BitVecSort(8)
    >>> Word = BitVecSort(16)
    >>> Byte
    BitVec(8)
    >>> x = Const('x', Byte)
    >>> eq(x, BitVec('x', 8))
    True
    """
    ctx = _get_ctx(ctx)
    return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)

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

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

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

Definition at line 3474 of file z3py.py.

Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), Concat(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().

def BitVecVal(val, bv, ctx=None):
    """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
    
    >>> v = BitVecVal(10, 32)
    >>> v
    10
    >>> print("0x%.8x" % v.as_long())
    0x0000000a
    """
    if is_bv_sort(bv):
        ctx = bv.ctx
        return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
    else:
        ctx = _get_ctx(ctx)
        return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)

def z3py.Bool	(		name,
			ctx = None
	)

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

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

Definition at line 1381 of file z3py.py.

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

def Bool(name, ctx=None):
    """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
    
    >>> p = Bool('p')
    >>> q = Bool('q')
    >>> And(p, q)
    And(p, q)
    """
    ctx = _get_ctx(ctx)
    return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)

def z3py.Bools	(		names,
			ctx = None
	)

Return a tuple of Boolean constants. 

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

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

Definition at line 1392 of file z3py.py.

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

def Bools(names, ctx=None):
    """Return a tuple of Boolean constants. 
    
    `names` is a single string containing all names separated by blank spaces. 
    If `ctx=None`, then the global context is used.

    >>> p, q, r = Bools('p q r')
    >>> And(p, Or(q, r))
    And(p, Or(q, r))
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [Bool(name, ctx) for name in names]

def z3py.BoolSort

(

ctx = None

)

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

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

Definition at line 1346 of file z3py.py.

Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Bool(), Sort.create(), ArraySortRef.domain(), ArrayRef.domain(), Context.getBoolSort(), If(), IntSort(), is_arith_sort(), Context.mkBoolSort(), Context.MkBoolSort(), ArraySortRef.range(), ArrayRef.range(), and ArrayRef.sort().

def BoolSort(ctx=None):
    """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
    
    >>> BoolSort()
    Bool
    >>> p = Const('p', BoolSort())
    >>> is_bool(p)
    True
    >>> r = Function('r', IntSort(), IntSort(), BoolSort())
    >>> r(0, 1)
    r(0, 1)
    >>> is_bool(r(0, 1))
    True
    """
    ctx = _get_ctx(ctx)
    return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)

def z3py.BoolVal	(		val,
			ctx = None
	)

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

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

Definition at line 1363 of file z3py.py.

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

def BoolVal(val, ctx=None):
    """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
    
    >>> BoolVal(True)
    True
    >>> is_true(BoolVal(True))
    True
    >>> is_true(True)
    False
    >>> is_false(BoolVal(False))
    True
    """
    ctx = _get_ctx(ctx)
    if val == False:
        return BoolRef(Z3_mk_false(ctx.ref()), ctx)
    else:
        return BoolRef(Z3_mk_true(ctx.ref()), ctx)

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

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

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

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

Definition at line 1407 of file z3py.py.

Referenced by And(), and Or().

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

    The constants are named using the given prefix.
    If `ctx=None`, then the global context is used.
    
    >>> P = BoolVector('p', 3)
    >>> P
    [p__0, p__1, p__2]
    >>> And(P)
    And(p__0, p__1, p__2)
    """
    return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]

def z3py.BV2Int

(

a

)

Return the Z3 expression BV2Int(a). 

>>> b = BitVec('b', 3)
>>> BV2Int(b).sort()
Int
>>> x = Int('x')
>>> x > BV2Int(b)
x > BV2Int(b)
>>> solve(x > BV2Int(b), b == 1, x < 3)
[b = 1, x = 2]

Definition at line 3442 of file z3py.py.

def BV2Int(a):
    """Return the Z3 expression BV2Int(a). 
    
    >>> b = BitVec('b', 3)
    >>> BV2Int(b).sort()
    Int
    >>> x = Int('x')
    >>> x > BV2Int(b)
    x > BV2Int(b)
    >>> solve(x > BV2Int(b), b == 1, x < 3)
    [b = 1, x = 2]
    """
    if __debug__:
        _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
    ctx = a.ctx
    ## investigate problem with bv2int
    return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)

def z3py.BVRedAnd

(

a

)

Return the reduction-and expression of `a`.

Definition at line 3841 of file z3py.py.

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

def z3py.BVRedOr

(

a

)

Return the reduction-or expression of `a`.

Definition at line 3847 of file z3py.py.

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

def z3py.Cbrt	(		a,
			ctx = None
	)

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

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

Definition at line 2904 of file z3py.py.

def Cbrt(a, ctx=None):
    """ Return a Z3 expression which represents the cubic root of a. 
    
    >>> x = Real('x')
    >>> Cbrt(x)
    x**(1/3)
    """
    if not is_expr(a):
        ctx = _get_ctx(ctx)
        a = RealVal(a, ctx)
    return a ** "1/3"

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

Referenced by BitVecRef.size().

def Concat(*args):
    """Create a Z3 bit-vector concatenation expression. 
    
    >>> v = BitVecVal(1, 4)
    >>> Concat(v, v+1, v)
    Concat(Concat(1, 1 + 1), 1)
    >>> simplify(Concat(v, v+1, v))
    289
    >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
    121
    """
    args = _get_args(args)
    if __debug__:
        _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
        _z3_assert(len(args) >= 2, "At least two arguments expected.")
    ctx = args[0].ctx
    r   = args[0]
    for i in range(len(args) - 1):
        r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
    return r

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

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

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

Definition at line 7162 of file z3py.py.

Referenced by If().

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

def z3py.Const	(		name,
			sort
	)

Create a constant of the given sort.

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

Definition at line 1145 of file z3py.py.

Referenced by BitVecSort(), Consts(), FPSort(), IntSort(), RealSort(), and DatatypeSortRef.recognizer().

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

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

def z3py.Consts	(		names,
			sort
	)

Create a 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 1156 of file z3py.py.

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

def Consts(names, sort):
    """Create a several constants of the given sort. 
    
    `names` is a string containing the names of all constants to be created. 
    Blank spaces separate the names of different constants.
    
    >>> x, y, z = Consts('x y z', IntSort())
    >>> x + y + z
    x + y + z
    """
    if isinstance(names, str):
        names = names.split(" ")
    return [Const(name, sort) for name in names]

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

Referenced by Datatype.create().

def CreateDatatypes(*ds):
    """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
    
    In the following example we define a Tree-List using two mutually recursive datatypes.

    >>> TreeList = Datatype('TreeList')
    >>> Tree     = Datatype('Tree')
    >>> # Tree has two constructors: leaf and node
    >>> Tree.declare('leaf', ('val', IntSort()))
    >>> # a node contains a list of trees
    >>> Tree.declare('node', ('children', TreeList))
    >>> TreeList.declare('nil')
    >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
    >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
    >>> Tree.val(Tree.leaf(10))
    val(leaf(10))
    >>> simplify(Tree.val(Tree.leaf(10)))
    10
    >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
    >>> n1
    node(cons(leaf(10), cons(leaf(20), nil)))
    >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
    >>> simplify(n2 == n1)
    False
    >>> simplify(TreeList.car(Tree.children(n2)) == n1)
    True
    """
    ds = _get_args(ds)
    if __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 __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 __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, rref.name(), rref)
            for k in range(cref_arity):
                aref = dref.accessor(j, k)
                setattr(dref, aref.name(), aref)
        result.append(dref)
    return tuple(result)

def z3py.DeclareSort	(		name,
			ctx = None
	)

Create a new uninterpred 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 567 of file z3py.py.

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

def DeclareSort(name, ctx=None):
    """Create a new uninterpred sort named `name`.

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

    >>> A = DeclareSort('A')
    >>> a = Const('a', A)
    >>> b = Const('b', A)
    >>> a.sort() == A
    True
    >>> b.sort() == A
    True
    >>> a == b
    a == b
    """
    ctx = _get_ctx(ctx)
    return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)

def z3py.Default

(

a

)

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

Definition at line 4059 of file z3py.py.

Referenced by is_default().

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

def z3py.describe_probes

(

)

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

Definition at line 7092 of file z3py.py.

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

def z3py.describe_tactics

(

)

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

Definition at line 6904 of file z3py.py.

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

def z3py.disable_trace

(

msg

)

Definition at line 61 of file z3py.py.

def disable_trace(msg):
    Z3_disable_trace(msg)

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 1114 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 __debug__:
        _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
    args  = _coerce_expr_list(args, ctx)
    _args, sz = _to_ast_array(args)
    return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)

def z3py.enable_trace

(

msg

)

Definition at line 58 of file z3py.py.

def enable_trace(msg):
    Z3_enable_trace(msg)

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

Referenced by Context.mkEnumSort(), and Context.MkEnumSort().

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

def z3py.eq	(		a,
			b
	)

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

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

Definition at line 371 of file z3py.py.

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

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

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

Create a Z3 exists formula.

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

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

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

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

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.

    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

    >>> f = Function('f', IntSort(), IntSort(), IntSort())
    >>> x = Int('x')
    >>> y = Int('y')
    >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
    >>> q
    Exists([x, y], f(x, y) >= x)
    >>> is_quantifier(q)
    True
    >>> r = Tactic('nnf')(q).as_expr()
    >>> is_quantifier(r)
    False
    """
    return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)

def z3py.Extract	(		high,
			low,
			a
	)

Create a Z3 bit-vector extraction expression.

>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)

Definition at line 3554 of file z3py.py.

def Extract(high, low, a):
    """Create a Z3 bit-vector extraction expression.

    >>> x = BitVec('x', 8)
    >>> Extract(6, 2, x)
    Extract(6, 2, x)
    >>> Extract(6, 2, x).sort()
    BitVec(5)
    """
    if __debug__:
        _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
        _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
        _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
    return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)

def z3py.FailIf	(		p,
			ctx = None
	)

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

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

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

Definition at line 7125 of file z3py.py.

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

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

    >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
    >>> x, y = Ints('x y')
    >>> g = Goal()
    >>> g.add(x > 0)
    >>> g.add(y > 0)
    >>> t(g)
    [[x > 0, y > 0]]
    >>> g.add(x == y + 1)
    >>> t(g)
    [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
    """
    p = _to_probe(p, ctx)
    return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)

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

Create a named finite domain sort of a given size sz

Definition at line 6389 of file z3py.py.

Referenced by Sort.create(), Context.mkFiniteDomainSort(), and Context.MkFiniteDomainSort().

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

def z3py.Float128

(

ctx = None

)

Floating-point 128-bit (quadruple) sort.

Definition at line 7764 of file z3py.py.

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

def z3py.Float16

(

ctx = None

)

Floating-point 16-bit (half) sort.

Definition at line 7734 of file z3py.py.

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

def z3py.Float32

(

ctx = None

)

Floating-point 32-bit (single) sort.

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

def z3py.Float64

(

ctx = None

)

Floating-point 64-bit (double) sort.

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

def z3py.FloatHalf

(

ctx = None

)

Floating-point 16-bit (half) sort.

Definition at line 7739 of file z3py.py.

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

def FloatSingle

(

ctx = None

)

Floating-point 32-bit (single) sort.

Floating-point 64-bit (double) sort.

Floating-point 128-bit (quadruple) sort.

Definition at line 7749 of file z3py.py.

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

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

Create a Z3 forall formula.

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

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

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

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

def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
    """Create a Z3 forall formula.
    
    The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.

    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

    >>> f = Function('f', IntSort(), IntSort(), IntSort())
    >>> x = Int('x')
    >>> y = Int('y')
    >>> ForAll([x, y], f(x, y) >= x)
    ForAll([x, y], f(x, y) >= x)
    >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
    ForAll([x, y], f(x, y) >= x)
    >>> ForAll([x, y], f(x, y) >= x, weight=10)
    ForAll([x, y], f(x, y) >= x)
    """
    return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)

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

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

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

Definition at line 8207 of file z3py.py.

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

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

    >>> x  = FP('x', FPSort(8, 24))
    >>> is_fp(x)
    True
    >>> x.ebits()
    8
    >>> x.sort()
    FPSort(8, 24)
    >>> word = FPSort(8, 24)
    >>> x2 = FP('x', word)
    >>> eq(x, x2)
    True
    """ 
    if isinstance(fpsort, FPSortRef):
        ctx = fpsort.ctx
    else:
        ctx = _get_ctx(ctx)
    return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)

def z3py.fpAbs

(

a

)

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

def fpAbs(a):
    """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 = None
    if not is_expr(a):
        ctx =_get_ctx(ctx)
        s = get_default_fp_sort(ctx)
        a = FPVal(a, s)
    else:
        ctx = a.ctx
    if __debug__:     
        _z3_assert(is_fp(a), "First argument must be Z3 floating-point expression")
    return FPRef(Z3_mk_fpa_abs(a.ctx_ref(), a.as_ast()), a.ctx)

def z3py.fpAdd	(		rm,
			a,
			b
	)

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(rm, x, y).sort()
FPSort(8, 24)

Definition at line 8299 of file z3py.py.

Referenced by FPs().

def fpAdd(rm, a, b):
    """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(rm, x, y).sort()
    FPSort(8, 24)
    """
    if __debug__:
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
    a, b = _coerce_exprs(a, b)
    return FPRef(Z3_mk_fpa_add(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)

def z3py.fpDiv	(		rm,
			a,
			b
	)

Create a Z3 floating-point divison 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 8353 of file z3py.py.

def fpDiv(rm, a, b):
    """Create a Z3 floating-point divison 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)
    """
    if __debug__:
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
    a, b = _coerce_exprs(a, b)
    return FPRef(Z3_mk_fpa_div(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)

def z3py.fpEQ	(		a,
			b
	)

Create the Z3 floating-point expression `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 8568 of file z3py.py.

Referenced by fpNEQ().

def fpEQ(a, b):
    """Create the Z3 floating-point expression `other <= self`.
    
    >>> x, y = FPs('x y', FPSort(8, 24))
    >>> fpEQ(x, y)
    fpEQ(x, y)
    >>> fpEQ(x, y).sexpr()
    '(fp.eq x y)'
    """
    _check_fp_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_fpa_eq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpFMA	(		rm,
			a,
			b,
			c
	)

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

Definition at line 8421 of file z3py.py.

def fpFMA(rm, a, b, c):
    """Create a Z3 floating-point fused multiply-add expression.
    """
    if __debug__:
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "Second, third, or fourth argument must be a Z3 floating-point expression")
    a, b, c = _coerce_expr_list([a, b, c])
    return FPRef(Z3_mk_fpa_fma(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), rm.ctx)    

def z3py.fpFP	(		sgn,
			exp,
			sig
	)

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

Definition at line 8596 of file z3py.py.

def fpFP(sgn, exp, sig):
    """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectorssgn, sig, and exp."""    
    _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
    _z3_assert(sgn.sort().size() == 1, "sort mismatch")
    return FPRef(Z3_mk_fpa_fp(sgn.ctx_ref(), sgn.ast, exp.ast, sig.ast), sgn.ctx)
    

def z3py.fpGEQ	(		a,
			b
	)

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

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

Definition at line 8553 of file z3py.py.

def fpGEQ(a, b):
    """Create the Z3 floating-point expression `other <= self`.
    
    >>> x, y = FPs('x y', FPSort(8, 24))
    >>> x + y
    x + y
    >>> fpGEQ(x, y)
    x >= y
    >>> (x >= y).sexpr()
    '(fp.geq x y)'
    """
    _check_fp_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_fpa_geq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpGT	(		a,
			b
	)

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

def fpGT(a, b):
    """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)'
    """
    _check_fp_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_fpa_gt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpInfinity	(		s,
			negative
	)

Definition at line 8160 of file z3py.py.

def fpInfinity(s, negative):
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    _z3_assert(isinstance(negative, bool), "expected Boolean flag")
    return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)

def z3py.fpIsInfinite

(

a

)

Create a Z3 floating-point isNaN expression.

Definition at line 8467 of file z3py.py.

def fpIsInfinite(a):
    """Create a Z3 floating-point isNaN expression.
    """
    if __debug__:        
        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_is_infinite(a.ctx_ref(), a.as_ast()), a.ctx) 

def z3py.fpIsNaN

(

a

)

Create a Z3 floating-point isNaN expression.

Definition at line 8460 of file z3py.py.

def fpIsNaN(a):
    """Create a Z3 floating-point isNaN expression.
    """
    if __debug__:        
        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_is_nan(a.ctx_ref(), a.as_ast()), a.ctx) 

def z3py.fpIsNegative

(

a

)

Create a Z3 floating-point isNaN expression.

Definition at line 8495 of file z3py.py.

def fpIsNegative(a):
    """Create a Z3 floating-point isNaN expression.
    """
    if __debug__:        
        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_is_negative(a.ctx_ref(), a.as_ast()), a.ctx) 

def z3py.fpIsNormal

(

a

)

Create a Z3 floating-point isNaN expression.

Definition at line 8481 of file z3py.py.

def fpIsNormal(a):
    """Create a Z3 floating-point isNaN expression.
    """
    if __debug__:        
        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_is_normal(a.ctx_ref(), a.as_ast()), a.ctx) 

def z3py.fpIsPositive

(

a

)

Create a Z3 floating-point isNaN expression.

Definition at line 8502 of file z3py.py.

08502 
08503 def fpIsPositive(a):
08504     """Create a Z3 floating-point isNaN expression.
08505     """
08506     if __debug__:        
08507         _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
08508     return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 
    

def z3py.fpIsSubnormal

(

a

)

Create a Z3 floating-point isNaN expression.

Definition at line 8488 of file z3py.py.

def fpIsSubnormal(a):
    """Create a Z3 floating-point isNaN expression.
    """
    if __debug__:        
        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_is_subnormal(a.ctx_ref(), a.as_ast()), a.ctx) 

def z3py.fpIsZero

(

a

)

Create a Z3 floating-point isNaN expression.

Definition at line 8474 of file z3py.py.

def fpIsZero(a):
    """Create a Z3 floating-point isNaN expression.
    """
    if __debug__:        
        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_is_zero(a.ctx_ref(), a.as_ast()), a.ctx) 

def z3py.fpLEQ	(		a,
			b
	)

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

def fpLEQ(a, b):
    """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)'
    """
    _check_fp_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_fpa_leq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpLT	(		a,
			b
	)

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.leq x y)'

Definition at line 8513 of file z3py.py.

def fpLT(a, b):
    """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.leq x y)'
    """
    _check_fp_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_fpa_lt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpMax	(		a,
			b
	)

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

def fpMax(a, b):
    """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)
    """
    if __debug__:        
        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
    a, b = _coerce_exprs(a, b)
    return FPRef(Z3_mk_fpa_max(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpMin	(		a,
			b
	)

Create a Z3 floating-point minimium 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 8387 of file z3py.py.

def fpMin(a, b):
    """Create a Z3 floating-point minimium 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)
    """
    if __debug__:        
        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
    a, b = _coerce_exprs(a, b)
    return FPRef(Z3_mk_fpa_min(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpMinusInfinity

(

s

)

Definition at line 8156 of file z3py.py.

def fpMinusInfinity(s):
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)

def z3py.fpMinusZero

(

s

)

Definition at line 8169 of file z3py.py.

def fpMinusZero(s):
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)

def z3py.fpMul	(		rm,
			a,
			b
	)

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

Referenced by FPs().

def fpMul(rm, a, b):
    """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)
    """
    if __debug__:
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
    a, b = _coerce_exprs(a, b)
    return FPRef(Z3_mk_fpa_mul(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)

def z3py.fpNaN

(

s

)

Definition at line 8148 of file z3py.py.

def fpNaN(s):
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)

def z3py.fpNeg

(

a

)

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

def fpNeg(a):
    """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 = None
    if not is_expr(a):
        ctx =_get_ctx(ctx)
        s = get_default_fp_sort(ctx)
        a = FPVal(a, s)
    else:
        ctx = a.ctx
    if __debug__:        
        _z3_assert(is_fp(a), "First argument must be Z3 floating-point expression")
    return FPRef(Z3_mk_fpa_neg(a.ctx_ref(), a.as_ast()), a.ctx)

def z3py.fpNEQ	(		a,
			b
	)

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

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

Definition at line 8581 of file z3py.py.

def fpNEQ(a, b):
    """Create the Z3 floating-point expression `other <= self`.
    
    >>> x, y = FPs('x y', FPSort(8, 24))
    >>> fpNEQ(x, y)
    Not(fpEQ(x, y))
    >>> (x != y).sexpr()
    '(not (fp.eq x y))'
    """
    _check_fp_args(a, b)
    a, b = _coerce_exprs(a, b)
    return Not(BoolRef(Z3_mk_fpa_eq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx), a.ctx)

def z3py.fpPlusInfinity

(

s

)

Definition at line 8152 of file z3py.py.

def fpPlusInfinity(s):
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)

def z3py.fpPlusZero

(

s

)

Definition at line 8165 of file z3py.py.

def fpPlusZero(s):
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)

def z3py.fpRem	(		a,
			b
	)

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

def fpRem(a, b):
    """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)
    """
    if __debug__:        
        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
    a, b = _coerce_exprs(a, b)
    return FPRef(Z3_mk_fpa_rem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.fpRoundToIntegral	(		rm,
			a
	)

Create a Z3 floating-point roundToIntegral expression.

Definition at line 8445 of file z3py.py.

def fpRoundToIntegral(rm, a):
    """Create a Z3 floating-point roundToIntegral expression.
    """
    ctx = None
    if not is_expr(a):
        ctx =_get_ctx(ctx)
        s = get_default_fp_sort(ctx)
        a = FPVal(a, s)
    else:
        ctx = a.ctx
    if __debug__:
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_round_to_integral(rm.ctx_ref(), rm.as_ast(), a.as_ast()), rm.ctx)    

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

Return an array of floating-point constants.

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

Definition at line 8230 of file z3py.py.

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

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

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

Referenced by FPRef.__add__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FPSortRef.cast(), Sort.create(), FPSortRef.ebits(), FPRef.ebits(), FPNumRef.exponent(), FPNumRef.exponent_as_long(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpGEQ(), fpGT(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNeg(), fpNEQ(), fpRem(), FPs(), fpSub(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), is_fp(), is_fp_sort(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), Context.mkFPSort(), Context.MkFPSort(), Context.mkFPSort128(), Context.MkFPSort128(), Context.mkFPSort16(), Context.MkFPSort16(), Context.mkFPSort32(), Context.MkFPSort32(), Context.mkFPSort64(), Context.MkFPSort64(), Context.mkFPSortDouble(), Context.MkFPSortDouble(), Context.mkFPSortHalf(), Context.MkFPSortHalf(), Context.mkFPSortQuadruple(), Context.MkFPSortQuadruple(), Context.mkFPSortSingle(), Context.MkFPSortSingle(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign(), FPNumRef.significand(), and FPRef.sort().

def FPSort(ebits, sbits, ctx=None):
    """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.

    >>> Single = FPSort(8, 24)
    >>> Double = FPSort(11, 53)
    >>> Single
    FPSort(8, 24)
    >>> x = Const('x', Single)
    >>> eq(x, FP('x', FPSort(8, 24)))
    True
    """
    ctx = z3._get_ctx(ctx)
    return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)

def z3py.fpSqrt	(		rm,
			a
	)

Create a Z3 floating-point square root expression.

Definition at line 8430 of file z3py.py.

def fpSqrt(rm, a):
    """Create a Z3 floating-point square root expression.
    """
    ctx = None
    if not is_expr(a):
        ctx =_get_ctx(ctx)
        s = get_default_fp_sort(ctx)
        a = FPVal(a, s)
    else:
        ctx = a.ctx
    if __debug__:
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expressions")
    return FPRef(Z3_mk_fpa_sqrt(rm.ctx_ref(), rm.as_ast(), a.as_ast()), rm.ctx)    

def z3py.fpSub	(		rm,
			a,
			b
	)

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

def fpSub(rm, a, b):
    """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)
    """
    if __debug__:
        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
    a, b = _coerce_exprs(a, b)
    return FPRef(Z3_mk_fpa_sub(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)

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

Create a Z3 floating-point conversion expression from other terms.

Definition at line 8603 of file z3py.py.

def fpToFP(a1, a2=None, a3=None):
    """Create a Z3 floating-point conversion expression from other terms."""
    if is_bv(a1) and is_fp_sort(a2):
        return FPRef(Z3_mk_fpa_to_fp_bv(a1.ctx_ref(), a1.ast, a2.ast), a1.ctx)
    elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
        return FPRef(Z3_mk_fpa_to_fp_float(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
    elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
        return FPRef(Z3_mk_fpa_to_fp_real(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
    elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
        return FPRef(Z3_mk_fpa_to_fp_signed(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
    else:
        raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")

def z3py.fpToFPUnsigned	(		rm,
			x,
			s
	)

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

Definition at line 8616 of file z3py.py.

def fpToFPUnsigned(rm, x, s):
    """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
    if __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")
    return FPRef(Z3_mk_fpa_to_fp_unsigned(rm.ctx_ref(), rm.ast, x.ast, s.ast), rm.ctx)

def z3py.fpToIEEEBV

(

x

)

\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 represenatation 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 8682 of file z3py.py.

def fpToIEEEBV(x):
    """\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 represenatation 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 __debug__:
        _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
    return BitVecRef(Z3_mk_fpa_to_ieee_bv(x.ctx_ref(), x.ast), x.ctx)

def z3py.fpToReal

(

x

)

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

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

def z3py.fpToSBV	(		rm,
			x,
			s
	)

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

def fpToSBV(rm, x, s):
    """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 __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")
    return BitVecRef(Z3_mk_fpa_to_sbv(rm.ctx_ref(), rm.ast, x.ast, s.size()), rm.ctx)

def z3py.fpToUBV	(		rm,
			x,
			s
	)

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

def fpToUBV(rm, x, s):
    """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 __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")
    return BitVecRef(Z3_mk_fpa_to_ubv(rm.ctx_ref(), rm.ast, x.ast, s.size()), rm.ctx)

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

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

>>> v = FPVal(20.0, FPSort(8, 24))
>>> v
1.25*(2**4)
>>> print("0x%.8x" % v.exponent_as_long())
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)

Definition at line 8178 of file z3py.py.

Referenced by fpAbs(), fpNeg(), fpRoundToIntegral(), fpSqrt(), and is_fp_value().

08178 
08179 def FPVal(sig, exp=None, fps=None, ctx=None):
08180     """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
08181     
08182     >>> v = FPVal(20.0, FPSort(8, 24))
08183     >>> v
08184     1.25*(2**4)
08185     >>> print("0x%.8x" % v.exponent_as_long())
08186     0x00000004
08187     >>> v = FPVal(2.25, FPSort(8, 24))
08188     >>> v
08189     1.125*(2**1)
08190     >>> v = FPVal(-2.25, FPSort(8, 24))
08191     >>> v
08192     -1.125*(2**1)
08193     """
08194     ctx = _get_ctx(ctx)
08195     if is_fp_sort(exp):
08196         fps = exp
08197         exp = None
08198     elif fps == None:
08199         fps = _dflt_fps(ctx)
08200     _z3_assert(is_fp_sort(fps), "sort mismatch")
08201     if exp == None:
08202         exp = 0    
08203     val = _to_float_str(sig)
08204     val = val + 'p'
08205     val = val + _to_int_str(exp)
08206     return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
        

def z3py.fpZero	(		s,
			negative
	)

Definition at line 8173 of file z3py.py.

def fpZero(s, negative):
    _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
    _z3_assert(isinstance(negative, bool), "expected Boolean flag")
    return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)

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

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

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

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

Definition at line 1421 of file z3py.py.

def FreshBool(prefix='b', ctx=None):
    """Return a fresh Boolean constant in the given context using the given prefix.
    
    If `ctx=None`, then the global context is used.    

    >>> b1 = FreshBool()
    >>> b2 = FreshBool()
    >>> eq(b1, b2)
    False
    """
    ctx = _get_ctx(ctx)
    return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)

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

def FreshInt(prefix='x', ctx=None):
    """Return a fresh integer constant in the given context using the given prefix.

    >>> x = FreshInt()
    >>> y = FreshInt()
    >>> eq(x, y)
    False
    >>> x.sort()
    Int
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)

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

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

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

Definition at line 2829 of file z3py.py.

def FreshReal(prefix='b', ctx=None):
    """Return a fresh real constant in the given context using the given prefix.

    >>> x = FreshReal()
    >>> y = FreshReal()
    >>> eq(x, y)
    False
    >>> x.sort()
    Real
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)

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

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

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

def z3py.get_as_array_func

(

n

)

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

Definition at line 5593 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 __debug__:
        _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
    return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)

def z3py.get_default_fp_sort

(

ctx = None

)

Definition at line 7681 of file z3py.py.

Referenced by fpAbs(), fpNeg(), fpRoundToIntegral(), and fpSqrt().

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

def z3py.get_default_rounding_mode

(

ctx = None

)

Retrieves the global default rounding mode.

Definition at line 7654 of file z3py.py.

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

def z3py.get_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 3987 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 __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)), a.ctx)

def z3py.get_param

(

name

)

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

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

Definition at line 247 of file z3py.py.

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

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

def z3py.get_var_index

(

a

)

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

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

Definition at line 1048 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 __debug__:
        _z3_assert(is_var(a), "Z3 bound variable expected")
    return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))

def z3py.get_version

(

)

Definition at line 72 of file z3py.py.

00072 
00073 def get_version():
00074   major = ctypes.c_uint(0)
00075   minor = ctypes.c_uint(0)
00076   build = ctypes.c_uint(0)
00077   rev = ctypes.c_uint(0)
00078   Z3_get_version(major, minor, build, rev)
00079   return (major.value, minor.value, build.value, rev.value)
00080 
00081 # We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com

def z3py.get_version_string

(

)

Definition at line 64 of file z3py.py.

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

def z3py.help_simplify

(

)

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

Definition at line 7202 of file z3py.py.

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

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

Create a Z3 if-then-else expression. 

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

Definition at line 1092 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 __debug__:
            _z3_assert(a.ctx == b.ctx, "Context mismatch")
        return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)

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

Create a Z3 implies expression. 

>>> p, q = Bools('p q')
>>> Implies(p, q)
Implies(p, q)
>>> simplify(Implies(p, q))
Or(Not(p), q)

Definition at line 1434 of file z3py.py.

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

def Implies(a, b, ctx=None):
    """Create a Z3 implies expression. 
    
    >>> p, q = Bools('p q')
    >>> Implies(p, q)
    Implies(p, q)
    >>> simplify(Implies(p, q))
    Or(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_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

def z3py.Int	(		name,
			ctx = None
	)

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

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

Definition at line 2742 of file z3py.py.

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

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

    >>> x = Int('x')
    >>> is_int(x)
    True
    >>> is_int(x + 1)
    True
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)

def z3py.Interpolant	(		a,
			ctx = None
	)

Create an interpolation operator.

The argument is an interpolation pattern (see tree_interpolant). 

>>> x = Int('x')
>>> print Interpolant(x>0)
interp(x > 0)

Definition at line 7517 of file z3py.py.

Referenced by binary_interpolant(), and tree_interpolant().

def Interpolant(a,ctx=None):
    """Create an interpolation operator.
    
    The argument is an interpolation pattern (see tree_interpolant). 

    >>> x = Int('x')
    >>> print Interpolant(x>0)
    interp(x > 0)
    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
    s = BoolSort(ctx)
    a = s.cast(a)
    return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)

def z3py.Ints	(		names,
			ctx = None
	)

Return a tuple of Integer constants. 

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

Definition at line 2754 of file z3py.py.

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

def Ints(names, ctx=None):
    """Return a tuple of Integer constants. 
    
    >>> x, y, z = Ints('x y z')
    >>> Sum(x, y, z)
    x + y + z
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [Int(name, ctx) for name in names]

def z3py.IntSort

(

ctx = None

)

Return the interger 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 2639 of file z3py.py.

Referenced by ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), DatatypeSortRef.accessor(), FuncEntry.arg_value(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), ArithSortRef.cast(), QuantifierRef.children(), DatatypeSortRef.constructor(), Sort.create(), Datatype.create(), CreateDatatypes(), Datatype.declare(), ModelRef.decls(), Default(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), FreshInt(), ModelRef.get_interp(), get_map_func(), Context.getIntSort(), Int(), is_arith_sort(), is_array(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_forall(), is_fp_sort(), is_K(), is_map(), is_pattern(), is_quantifier(), is_select(), is_store(), K(), Map(), Context.mkIntSort(), Context.MkIntSort(), MultiPattern(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), ArraySortRef.range(), ArrayRef.range(), DatatypeSortRef.recognizer(), Select(), ArrayRef.sort(), Store(), Update(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().

def IntSort(ctx=None):
    """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
    
    >>> IntSort()
    Int
    >>> x = Const('x', IntSort())
    >>> is_int(x)
    True
    >>> x.sort() == IntSort()
    True
    >>> x.sort() == BoolSort()
    False
    """
    ctx = _get_ctx(ctx)
    return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)

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

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

def IntVal(val, ctx=None):
    """Return a Z3 integer value. If `ctx=None`, then the global context is used.
    
    >>> IntVal(1)
    1
    >>> IntVal("100")
    100
    """
    ctx = _get_ctx(ctx)
    return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)

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

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

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

Definition at line 2766 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
    """
    return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]

def z3py.is_add

(

a

)

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

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

Definition at line 2343 of file z3py.py.

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

def z3py.is_algebraic_value

(

a

)

Return `True` if `a` is an algerbraic 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 2330 of file z3py.py.

def is_algebraic_value(a):
    """Return `True` if `a` is an algerbraic value of sort Real.
    
    >>> is_algebraic_value(RealVal("3/5"))
    False
    >>> n = simplify(Sqrt(2))
    >>> n
    1.4142135623?
    >>> is_algebraic_value(n)
    True
    """
    return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())

def z3py.is_and

(

a

)

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

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

Definition at line 1293 of file z3py.py.

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

def z3py.is_app

(

a

)

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

Note that, constants are function applications with 0 arguments. 

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

Definition at line 981 of file z3py.py.

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

def is_app(a):
    """Return `True` if `a` is a Z3 function application. 
    
    Note that, constants are function applications with 0 arguments. 

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

def z3py.is_app_of	(		a,
			k
	)

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

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

Definition at line 1080 of file z3py.py.

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

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

def z3py.is_arith

(

a

)

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

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

Definition at line 2224 of file z3py.py.

Referenced by is_algebraic_value().

def is_arith(a):
    """Return `True` if `a` is an arithmetical expression.
    
    >>> x = Int('x')
    >>> is_arith(x)
    True
    >>> is_arith(x + 1)
    True
    >>> is_arith(1)
    False
    >>> is_arith(IntVal(1))
    True
    >>> y = Real('y')
    >>> is_arith(y)
    True
    >>> is_arith(y + 1)
    True
    """
    return isinstance(a, ArithRef)

def z3py.is_arith_sort

(

s

)

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

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

Definition at line 1927 of file z3py.py.

01927 
01928 def is_arith_sort(s):
01929     """Return `True` if s is an arithmetical sort (type).
01930     
01931     >>> is_arith_sort(IntSort())
01932     True
01933     >>> is_arith_sort(RealSort())
01934     True
01935     >>> is_arith_sort(BoolSort())
01936     False
01937     >>> n = Int('x') + 1
01938     >>> is_arith_sort(n.sort())
01939     True
01940     """
01941     return isinstance(s, ArithSortRef)
    

def z3py.is_array

(

a

)

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

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

Definition at line 3927 of file z3py.py.

Referenced by Default().

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

def z3py.is_as_array

(

n

)

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

Definition at line 5589 of file z3py.py.

Referenced by get_as_array_func().

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

def z3py.is_ast

(

a

)

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

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

Definition at line 351 of file z3py.py.

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

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

def z3py.is_bool

(

a

)

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

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

Definition at line 1246 of file z3py.py.

Referenced by BoolSort(), and prove().

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

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

def z3py.is_bv

(

a

)

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

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

Definition at line 3415 of file z3py.py.

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

def is_bv(a):
    """Return `True` if `a` is a Z3 bit-vector expression.
    
    >>> b = BitVec('b', 32)
    >>> is_bv(b)
    True
    >>> is_bv(b + 10)
    True
    >>> is_bv(Int('x'))
    False
    """
    return isinstance(a, BitVecRef)

def z3py.is_bv_sort

(

s

)

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

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

Definition at line 2954 of file z3py.py.

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

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

    >>> is_bv_sort(BitVecSort(32))
    True
    >>> is_bv_sort(IntSort())
    False
    """
    return isinstance(s, BitVecSortRef)

def z3py.is_bv_value

(

a

)

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

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

Definition at line 3428 of file z3py.py.

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

    >>> b = BitVec('b', 32)
    >>> is_bv_value(b)
    False
    >>> b = BitVecVal(10, 32)
    >>> b
    10
    >>> is_bv_value(b)
    True
    """
    return is_bv(a) and _is_numeral(a.ctx, a.as_ast())

def z3py.is_const

(

a

)

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

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

Definition at line 1006 of file z3py.py.

Referenced by prove().

def is_const(a):
    """Return `True` if `a` is Z3 constant/variable expression. 
    
    >>> a = Int('a')
    >>> is_const(a)
    True
    >>> is_const(a + 1)
    False
    >>> is_const(1)
    False
    >>> is_const(IntVal(1))
    True
    >>> x = Int('x')
    >>> is_const(ForAll(x, x >= 0))
    False
    """
    return is_app(a) and a.num_args() == 0

def z3py.is_const_array

(

a

)

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

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

Definition at line 3940 of file z3py.py.

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

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

def z3py.is_default

(

a

)

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

Definition at line 3979 of file z3py.py.

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

def z3py.is_distinct

(

a

)

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

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

Definition at line 1335 of file z3py.py.

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

def z3py.is_div

(

a

)

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

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

Definition at line 2376 of file z3py.py.

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

def z3py.is_eq

(

a

)

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

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

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

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

Definition at line 961 of file z3py.py.

Referenced by SortRef.cast(), BoolSortRef.cast(), Cbrt(), ExprRef.children(), fpAbs(), fpNeg(), fpRoundToIntegral(), fpSqrt(), is_var(), simplify(), substitute(), and substitute_vars().

def is_expr(a):
    """Return `True` if `a` is a Z3 expression.
    
    >>> a = Int('a')
    >>> is_expr(a)
    True
    >>> is_expr(a + 1)
    True
    >>> is_expr(IntSort())
    False
    >>> is_expr(1)
    False
    >>> is_expr(IntVal(1))
    True
    >>> x = Int('x')
    >>> is_expr(ForAll(x, x >= 0))
    True
    """
    return isinstance(a, ExprRef)

def z3py.is_false

(

a

)

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

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

Definition at line 1280 of file z3py.py.

Referenced by BoolVal().

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

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

def z3py.is_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 8092 of file z3py.py.

Referenced by FP(), fpAbs(), fpAdd(), fpDiv(), fpFMA(), fpIsInfinite(), fpIsNaN(), fpIsNegative(), fpIsNormal(), fpIsPositive(), fpIsSubnormal(), fpIsZero(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), fpRoundToIntegral(), fpSqrt(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), and fpToUBV().

def is_fp(a):
    """Return `True` if `a` is a Z3 floating-point expression.
    
    >>> b = FP('b', FPSort(8, 24))
    >>> is_fp(b)
    True
    >>> is_fp(b + 1.0)
    True
    >>> is_fp(Int('x'))
    False
    """
    return isinstance(a, FPRef)

def z3py.is_fp_sort

(

s

)

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

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

Definition at line 7778 of file z3py.py.

Referenced by fpToFP(), fpToFPUnsigned(), and FPVal().

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

    >>> is_fp_sort(FPSort(8, 24))
    True
    >>> is_fp_sort(IntSort())
    False
    """
    return isinstance(s, FPSortRef)

def z3py.is_fp_value

(

a

)

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

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

Definition at line 8105 of file z3py.py.

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

    >>> b = FP('b', FPSort(8, 24))
    >>> is_fp_value(b)
    False
    >>> b = FPVal(1.0, FPSort(8, 24))
    >>> b
    1
    >>> is_fp_value(b)
    True
    """
    return is_fp(a) and _is_numeral(a.ctx, a.ast)

def z3py.is_fprm

(

a

)

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

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

Definition at line 7996 of file z3py.py.

Referenced by fpAdd(), fpDiv(), fpFMA(), fpMul(), fpRoundToIntegral(), fpSqrt(), fpSub(), fpToFP(), fpToFPUnsigned(), fpToSBV(), and fpToUBV().

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

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

def z3py.is_fprm_sort

(

s

)

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

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

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

def z3py.is_fprm_value

(

a

)

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

Definition at line 8008 of file z3py.py.

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

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

Referenced by prove().

def is_func_decl(a):
    """Return `True` if `a` is a Z3 function declaration.
    
    >>> f = Function('f', IntSort(), IntSort())
    >>> is_func_decl(f)
    True
    >>> x = Real('x')
    >>> is_func_decl(x)
    False
    """
    return isinstance(a, FuncDeclRef)

def z3py.is_ge

(

a

)

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

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

Definition at line 2436 of file z3py.py.

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

def z3py.is_gt

(

a

)

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

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

Definition at line 2447 of file z3py.py.

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

def z3py.is_idiv

(

a

)

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

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

Definition at line 2392 of file z3py.py.

Referenced by is_div().

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

def z3py.is_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 2244 of file z3py.py.

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

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

def z3py.is_int_value

(

a

)

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

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

Definition at line 2286 of file z3py.py.

def is_int_value(a):
    """Return `True` if `a` is an integer value of sort Int.
    
    >>> is_int_value(IntVal(1))
    True
    >>> is_int_value(1)
    False
    >>> is_int_value(Int('x'))
    False
    >>> n = Int('x') + 1
    >>> n
    x + 1
    >>> n.arg(1)
    1
    >>> is_int_value(n.arg(1))
    True
    >>> is_int_value(RealVal("1/3"))
    False
    >>> is_int_value(RealVal(1))
    False
    """
    return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())

def z3py.is_is_int

(

a

)

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

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

Definition at line 2458 of file z3py.py.

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

def z3py.is_K

(

a

)

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

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

Definition at line 3952 of file z3py.py.

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

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

def z3py.is_le

(

a

)

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

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

Definition at line 2414 of file z3py.py.

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

def z3py.is_lt

(

a

)

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

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

Definition at line 2425 of file z3py.py.

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

def z3py.is_map

(

a

)

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

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

Definition at line 3964 of file z3py.py.

Referenced by get_map_func().

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

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

def z3py.is_mod

(

a

)

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

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

Definition at line 2403 of file z3py.py.

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

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

def z3py.is_mul

(

a

)

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

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

Definition at line 2354 of file z3py.py.

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

def z3py.is_not

(

a

)

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

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

Definition at line 1315 of file z3py.py.

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

def z3py.is_or

(

a

)

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

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

Definition at line 1304 of file z3py.py.

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

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

def z3py.is_pattern

(

a

)

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

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

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

Referenced by MultiPattern().

def is_pattern(a):
    """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.

    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
    
    >>> f = Function('f', IntSort(), IntSort())
    >>> x = Int('x')
    >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
    >>> q
    ForAll(x, f(x) == 0)
    >>> q.num_patterns()
    1
    >>> is_pattern(q.pattern(0))
    True
    >>> q.pattern(0)
    f(Var(0))
    """
    return isinstance(a, PatternRef)

def z3py.is_probe

(

p

)

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

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

Definition at line 7058 of file z3py.py.

Referenced by eq().

def is_probe(p):
    """Return `True` if `p` is a Z3 probe.
    
    >>> is_probe(Int('x'))
    False
    >>> is_probe(Probe('memory'))
    True
    """
    return isinstance(p, Probe)

def z3py.is_quantifier

(

a

)

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

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

Definition at line 1769 of file z3py.py.

Referenced by Exists().

def is_quantifier(a):
    """Return `True` if `a` is a Z3 quantifier.
    
    >>> f = Function('f', IntSort(), IntSort())
    >>> x = Int('x')
    >>> q = ForAll(x, f(x) == 0)
    >>> is_quantifier(q)
    True
    >>> is_quantifier(f(x))
    False
    """
    return isinstance(a, QuantifierRef)

def z3py.is_rational_value

(

a

)

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

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

Definition at line 2309 of file z3py.py.

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

def is_rational_value(a):
    """Return `True` if `a` is rational value of sort Real.
    
    >>> is_rational_value(RealVal(1))
    True
    >>> is_rational_value(RealVal("3/5"))
    True
    >>> is_rational_value(IntVal(1))
    False
    >>> is_rational_value(1)
    False
    >>> n = Real('x') + 1
    >>> n.arg(1)
    1
    >>> is_rational_value(n.arg(1))
    True
    >>> is_rational_value(Real('x'))
    False
    """
    return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())

def z3py.is_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 2262 of file z3py.py.

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

def is_real(a):
    """Return `True` if `a` is a real expression.
    
    >>> x = Int('x')
    >>> is_real(x + 1)
    False
    >>> y = Real('y')
    >>> is_real(y)
    True
    >>> is_real(y + 1)
    True
    >>> is_real(1)
    False
    >>> is_real(RealVal(1))
    True
    """
    return is_arith(a) and a.is_real()

def z3py.is_select

(

a

)

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

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

Definition at line 4143 of file z3py.py.

def is_select(a):
    """Return `True` if `a` is a Z3 array select application.
    
    >>> a = Array('a', IntSort(), IntSort())
    >>> is_select(a)
    False
    >>> i = Int('i')
    >>> is_select(a[i])
    True
    """
    return is_app_of(a, Z3_OP_SELECT)

def z3py.is_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 530 of file z3py.py.

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

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

def z3py.is_store

(

a

)

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

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

Definition at line 4155 of file z3py.py.

def is_store(a):
    """Return `True` if `a` is a Z3 array store application.
    
    >>> a = Array('a', IntSort(), IntSort())
    >>> is_store(a)
    False
    >>> is_store(Store(a, 0, 1))
    True
    """
    return is_app_of(a, Z3_OP_STORE)

def z3py.is_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 2365 of file z3py.py.

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

def z3py.is_to_int

(

a

)

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

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

Definition at line 2483 of file z3py.py.

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

def z3py.is_to_real

(

a

)

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

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

Definition at line 2469 of file z3py.py.

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

def z3py.is_true

(

a

)

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

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

Definition at line 1263 of file z3py.py.

Referenced by BoolVal().

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

def z3py.is_var

(

a

)

Return `True` if `a` is variable. 

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

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

Definition at line 1024 of file z3py.py.

Referenced by get_var_index().

def is_var(a):
    """Return `True` if `a` is variable. 
    
    Z3 uses de-Bruijn indices for representing bound variables in
    quantifiers.

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

def z3py.IsInt

(

a

)

Return the Z3 predicate IsInt(a). 

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

Definition at line 2876 of file z3py.py.

Referenced by is_is_int().

02876 
02877 def IsInt(a):
02878     """ Return the Z3 predicate IsInt(a). 
02879     
02880     >>> x = Real('x')
02881     >>> IsInt(x + "1/2")
02882     IsInt(x + 1/2)
02883     >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
02884     [x = 1/2]
02885     >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
02886     no solution
02887     """
02888     if __debug__:
02889         _z3_assert(a.is_real(), "Z3 real expression expected.")
02890     ctx = a.ctx
02891     return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
    

def z3py.K	(		dom,
			v
	)

Return a Z3 constant array expression. 

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

Definition at line 4122 of file z3py.py.

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

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

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

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

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

    Use the operator >> for the arithmetical right shift.

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

def z3py.main_ctx

(

)

Return a reference to the global Z3 context. 

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

Definition at line 188 of file z3py.py.

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

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

def z3py.Map	(		f,
			args
	)

Return a Z3 map array expression. 

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

Definition at line 4100 of file z3py.py.

Referenced by Context.Context(), get_map_func(), InterpolationContext.InterpolationContext(), and is_map().

def Map(f, *args):
    """Return a Z3 map array expression. 

    >>> f = Function('f', IntSort(), IntSort(), IntSort())
    >>> a1 = Array('a1', IntSort(), IntSort())
    >>> a2 = Array('a2', IntSort(), IntSort())
    >>> b  = Map(f, a1, a2)
    >>> b
    Map(f, a1, a2)
    >>> prove(b[0] == f(a1[0], a2[0]))
    proved
    """
    args = _get_args(args)
    if __debug__:
        _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
        _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
        _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
        _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
    _args, sz = _to_ast_array(args)
    ctx = f.ctx
    return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)

def z3py.MultiPattern

(

args

)

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

See http://rise4fun.com/Z3Py/tutorial/advanced for more details.

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

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

    See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
    
    >>> 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 __debug__:
        _z3_assert(len(args) > 0, "At least one argument expected")
        _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
    ctx = args[0].ctx
    args, sz = _to_ast_array(args)
    return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)

def z3py.Not	(		a,
			ctx = None
	)

Create a Z3 not expression or probe. 

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

Definition at line 1464 of file z3py.py.

Referenced by binary_interpolant(), fpNEQ(), Implies(), prove(), sequence_interpolant(), tree_interpolant(), and Xor().

def Not(a, ctx=None):
    """Create a Z3 not expression or probe. 
    
    >>> p = Bool('p')
    >>> Not(Not(p))
    Not(Not(p))
    >>> simplify(Not(Not(p)))
    p
    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
    if is_probe(a):
        # Not is also used to build probes
        return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
    else:
        s = BoolSort(ctx)
        a = s.cast(a)
        return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)

def z3py.open_log

(

fname

)

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

Definition at line 86 of file z3py.py.

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

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

Referenced by ApplyResult.as_expr(), Bools(), and Implies().

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]
    else:
        ctx = main_ctx()
    args = _get_args(args)
    ctx_args  = _ctx_from_ast_arg_list(args, ctx)
    if __debug__:
        _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
        _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
    if _has_probe(args):
        return _probe_or(args, ctx)
    else:
        args  = _coerce_expr_list(args, ctx)
        _args, sz = _to_ast_array(args)
        return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)

def z3py.OrElse	(		ts,
			ks
	)

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

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

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

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

Alias for ParThen(t1, t2, ctx).

Definition at line 6842 of file z3py.py.

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

def z3py.ParOr	(		ts,
			ks
	)

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

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

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

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

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

This function is similar to parse_smt2_string().

Definition at line 7507 of file z3py.py.

07507 
07508 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
07509     """Parse a file in SMT 2.0 format using the given sorts and decls.
07510     
07511     This function is similar to parse_smt2_string().
07512     """
07513     ctx = _get_ctx(ctx)
07514     ssz, snames, ssorts = _dict2sarray(sorts, ctx)
07515     dsz, dnames, ddecls = _dict2darray(decls, ctx)
07516     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
   

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

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

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

>>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
And(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 7487 of file z3py.py.

Referenced by parse_smt2_file().

def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
    """Parse a string in SMT 2.0 format using the given sorts and decls.
    
    The arguments sorts and decls are Python dictionaries used to initialize
    the symbol table used for the SMT 2.0 parser.

    >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
    And(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 _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)

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

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

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

Definition at line 6828 of file z3py.py.

Referenced by ParAndThen().

def ParThen(t1, t2, ctx=None):
    """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
    
    >>> x, y = Ints('x y')
    >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
    >>> t(And(Or(x == 1, x == 2), y == x + 1))
    [[x == 1, y == 2], [x == 2, y == 3]]
    """
    t1 = _to_tactic(t1, ctx)
    t2 = _to_tactic(t2, ctx)
    if __debug__:
        _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
    return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)

def z3py.probe_description	(		name,
			ctx = None
	)

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

>>> d = probe_description('memory')

Definition at line 7084 of file z3py.py.

Referenced by describe_probes().

def probe_description(name, ctx=None):
    """Return a short description for the probe named `name`.
    
    >>> d = probe_description('memory')
    """
    ctx = _get_ctx(ctx)
    return Z3_probe_get_descr(ctx.ref(), name)

def z3py.probes

(

ctx = None

)

Return a list of all available probes in Z3.

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

Definition at line 7074 of file z3py.py.

Referenced by describe_probes().

def probes(ctx=None):
    """Return a list of all available probes in Z3.
    
    >>> l = probes()
    >>> l.count('memory') == 1
    True
    """
    ctx = _get_ctx(ctx)
    return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]

def z3py.Product

(

args

)

Create the product of the Z3 expressions. 

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

Definition at line 7281 of file z3py.py.

Referenced by BitVecs().

def Product(*args):
    """Create the product of the Z3 expressions. 
    
    >>> a, b, c = Ints('a b c')
    >>> Product(a, b, c)
    a*b*c
    >>> Product([a, b, c])
    a*b*c
    >>> A = IntVector('a', 5)
    >>> Product(A)
    a__0*a__1*a__2*a__3*a__4
    """
    args  = _get_args(args)
    if __debug__:
        _z3_assert(len(args) > 0, "Non empty list of arguments expected")
    ctx   = _ctx_from_ast_arg_list(args)
    if __debug__:
        _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
    args  = _coerce_expr_list(args, ctx)
    if is_bv(args[0]):
        return _reduce(lambda a, b: a * b, args, 1)
    else:
        _args, sz = _to_ast_array(args)
        return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)

def z3py.prove	(		claim,
			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 7363 of file z3py.py.

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

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

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

Return a Z3 rational a/b.

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

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

Definition at line 2730 of file z3py.py.

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

def Q(a, b, ctx=None):
    """Return a Z3 rational a/b.
    
    If `ctx=None`, then the global context is used.

    >>> Q(3,5)
    3/5
    >>> Q(3,5).sort()
    Real
    """
    return simplify(RatVal(a, b))

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

Referenced by Q().

def RatVal(a, b, ctx=None):
    """Return a Z3 rational a/b.

    If `ctx=None`, then the global context is used.
    
    >>> RatVal(3,5)
    3/5
    >>> RatVal(3,5).sort()
    Real
    """
    if __debug__:
        _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
        _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
    return simplify(RealVal(a, ctx)/RealVal(b, ctx))

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

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

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

    >>> x = Real('x')
    >>> is_real(x)
    True
    >>> is_real(x + 1)
    True
    """
    ctx = _get_ctx(ctx)
    return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)

def z3py.Reals	(		names,
			ctx = None
	)

Return a tuple of real constants. 

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

Definition at line 2802 of file z3py.py.

Referenced by is_div().

def Reals(names, ctx=None):
    """Return a tuple of real constants. 
    
    >>> x, y, z = Reals('x y z')
    >>> Sum(x, y, z)
    x + y + z
    >>> Sum(x, y, z).sort()
    Real
    """
    ctx = _get_ctx(ctx)
    if isinstance(names, str):
        names = names.split(" ")
    return [Real(name, ctx) for name in names]

def z3py.RealSort

(

ctx = None

)

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

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

Definition at line 2655 of file z3py.py.

Referenced by ArithSortRef.cast(), Sort.create(), FreshReal(), Context.getRealSort(), is_arith_sort(), Context.mkRealSort(), Context.MkRealSort(), Real(), RealVar(), and QuantifierRef.var_sort().

def RealSort(ctx=None):
    """Return the real sort in the given context. If `ctx=None`, then the global context is used.
    
    >>> RealSort()
    Real
    >>> x = Const('x', RealSort())
    >>> is_real(x)
    True
    >>> is_int(x)
    False
    >>> x.sort() == RealSort()
    True
    """
    ctx = _get_ctx(ctx)
    return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)

def z3py.RealVal	(		val,
			ctx = None
	)

Return a Z3 real value. 

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

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

Definition at line 2697 of file z3py.py.

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

def RealVal(val, ctx=None):
    """Return a Z3 real value. 
    
    `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
    If `ctx=None`, then the global context is used.
    
    >>> RealVal(1)
    1
    >>> RealVal(1).sort()
    Real
    >>> RealVal("3/5")
    3/5
    >>> RealVal("1.5")
    3/2
    """
    ctx = _get_ctx(ctx)
    return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)

def z3py.RealVar	(		idx,
			ctx = None
	)

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

>>> RealVar(0)
Var(0)

Definition at line 1182 of file z3py.py.

Referenced by RealVarVector().

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

def z3py.RealVarVector	(		n,
			ctx = None
	)

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

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

Definition at line 1192 of file z3py.py.

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

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

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

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

Definition at line 2816 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
    """
    return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]

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

def Repeat(t, max=4294967295, ctx=None):
    """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.

    >>> x, y = Ints('x y')
    >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
    >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
    >>> r = t(c)
    >>> for subgoal in r: print(subgoal)
    [x == 0, y == 0, x > y]
    [x == 0, y == 1, x > y]
    [x == 1, y == 0, x > y]
    [x == 1, y == 1, x > y]
    >>> t = Then(t, Tactic('propagate-values'))
    >>> t(c)
    [[x == 1, y == 0]]
    """
    t = _to_tactic(t, ctx)
    return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)

def z3py.RepeatBitVec	(		n,
			a
	)

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

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

Definition at line 3818 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 __debug__:
        _z3_assert(isinstance(n, int), "First argument must be an integer")
        _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
    return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)

def z3py.reset_params

(

)

Reset all global (or module) parameters.

Definition at line 237 of file z3py.py.

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

def z3py.RNA

(

ctx = None

)

Definition at line 7968 of file z3py.py.

Referenced by get_default_rounding_mode().

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

def z3py.RNE

(

ctx = None

)

Definition at line 7960 of file z3py.py.

Referenced by fpAbs(), fpAdd(), fpDiv(), fpMax(), fpMin(), fpMul(), fpNeg(), FPs(), fpSub(), get_default_rounding_mode(), is_fprm(), and is_fprm_sort().

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

def z3py.RotateLeft	(		a,
			b
	)

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

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

Definition at line 3732 of file z3py.py.

def RotateLeft(a, b):
    """Return an expression representing `a` rotated to the left `b` times.

    >>> a, b = BitVecs('a b', 16)
    >>> RotateLeft(a, b)
    RotateLeft(a, b)
    >>> simplify(RotateLeft(a, 0))
    a
    >>> simplify(RotateLeft(a, 16))
    a
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.RotateRight	(		a,
			b
	)

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

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

Definition at line 3747 of file z3py.py.

def RotateRight(a, b):
    """Return an expression representing `a` rotated to the right `b` times.

    >>> a, b = BitVecs('a b', 16)
    >>> RotateRight(a, b)
    RotateRight(a, b)
    >>> simplify(RotateRight(a, 0))
    a
    >>> simplify(RotateRight(a, 16))
    a
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.RoundNearestTiesToAway

(

ctx = None

)

Definition at line 7964 of file z3py.py.

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

def z3py.RoundNearestTiesToEven

(

ctx = None

)

Definition at line 7956 of file z3py.py.

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

def z3py.RoundTowardNegative

(

ctx = None

)

Definition at line 7980 of file z3py.py.

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

def z3py.RoundTowardPositive

(

ctx = None

)

Definition at line 7972 of file z3py.py.

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

def z3py.RoundTowardZero

(

ctx = None

)

Definition at line 7988 of file z3py.py.

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

def z3py.RTN

(

ctx = None

)

Definition at line 7984 of file z3py.py.

Referenced by get_default_rounding_mode().

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

def z3py.RTP

(

ctx = None

)

Definition at line 7976 of file z3py.py.

Referenced by get_default_rounding_mode().

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

def z3py.RTZ

(

ctx = None

)

Definition at line 7992 of file z3py.py.

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

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

def z3py.Select	(		a,
			i
	)

Return a Z3 select array expression.

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

Definition at line 4086 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 __debug__:
        _z3_assert(is_array(a), "First argument must be a Z3 array expression")
    return a[i]

def z3py.sequence_interpolant	(		v,
			p = None,
			ctx = None
	)

Compute interpolant for a sequence of formulas.

If len(v) == N, and if the conjunction of the formulas in v is
unsatisfiable, the interpolant is a sequence of formulas w
such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:

1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
and v[i+1]..v[n]

Requires len(v) >= 1. 

If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a & b.

If parameters p are supplied, these are used in creating the
solver that determines satisfiability.

>>> x = Int('x')
>>> y = Int('y')
>>> print sequence_interpolant([x < 0, y == x , y > 2])
[Not(x >= 0), Not(y >= 0)]

Definition at line 7613 of file z3py.py.

def sequence_interpolant(v,p=None,ctx=None):
    """Compute interpolant for a sequence of formulas.

    If len(v) == N, and if the conjunction of the formulas in v is
    unsatisfiable, the interpolant is a sequence of formulas w
    such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:

    1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
    2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
    and v[i+1]..v[n]
    
    Requires len(v) >= 1. 

    If a & b is satisfiable, raises an object of class ModelRef
    that represents a model of a & b.

    If parameters p are supplied, these are used in creating the
    solver that determines satisfiability.

    >>> x = Int('x')
    >>> y = Int('y')
    >>> print sequence_interpolant([x < 0, y == x , y > 2])
    [Not(x >= 0), Not(y >= 0)]
    """
    f = v[0]
    for i in range(1,len(v)):
        f = And(Interpolant(f),v[i])
    return tree_interpolant(f,p,ctx)

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

Definition at line 7684 of file z3py.py.

def set_default_fp_sort(ebits, sbits, ctx=None):
    global _dflt_fpsort_ebits
    global _dflt_fpsort_sbits
    _dflt_fpsort_ebits = ebits
    _dflt_fpsort_sbits = sbits

def z3py.set_default_rounding_mode	(		rm,
			ctx = None
	)

Definition at line 7668 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 == Z3_OP_FPA_RM_TOWARD_ZERO or
                   _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or
                   _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or
                   _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or
                   _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
                   "illegal rounding mode")
        _dflt_rounding_mode = rm

def z3py.set_option	(		args,
			kws
	)

Alias for 'set_param' for backward compatibility.

Definition at line 242 of file z3py.py.

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

def z3py.set_param	(		args,
			kws
	)

Set Z3 global (or module) parameters.

>>> set_param(precision=10)

Definition at line 214 of file z3py.py.

Referenced by set_option().

def set_param(*args, **kws):
    """Set Z3 global (or module) parameters.

    >>> set_param(precision=10)
    """
    if __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 == None:
            prev = a
        else:
            Z3_global_param_set(str(prev), _to_param_value(a))
            prev = None

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 3762 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 __debug__:
        _z3_assert(isinstance(n, int), "First argument must be an integer")
        _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
    return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)

def z3py.SimpleSolver

(

ctx = 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 6131 of file z3py.py.

Referenced by Solver.reason_unknown(), and Solver.statistics().

def SimpleSolver(ctx=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)

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

Referenced by BitVecRef.__invert__(), BitVecRef.__lshift__(), ArithRef.__mod__(), ArithRef.__neg__(), BitVecRef.__neg__(), ArithRef.__pow__(), ArithRef.__rpow__(), BitVecRef.__rshift__(), AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), BitVecs(), Concat(), CreateDatatypes(), Implies(), is_algebraic_value(), K(), LShR(), Not(), Q(), RatVal(), DatatypeSortRef.recognizer(), RepeatBitVec(), RotateLeft(), RotateRight(), SignExt(), Xor(), and ZeroExt().

def simplify(a, *arguments, **keywords):
    """Simplify the expression `a` using the given options.

    This function has many options. Use `help_simplify` to obtain the complete list.
    
    >>> x = Int('x')
    >>> y = Int('y')
    >>> simplify(x + 1 + y + x + 1)
    2 + 2*x + y
    >>> simplify((x + 1)*(y + 1), som=True)
    1 + x + y + x*y
    >>> simplify(Distinct(x, y, 1), blast_distinct=True)
    And(Not(x == y), Not(x == 1), Not(y == 1))
    >>> simplify(And(x == 0, y == 1), elim_and=True)
    Not(Or(Not(x == 0), Not(y == 1)))
    """
    if __debug__:
        _z3_assert(is_expr(a), "Z3 expression expected")
    if len(arguments) > 0 or len(keywords) > 0:
        p = args2params(arguments, keywords, a.ctx)
        return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
    else:
        return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)

def z3py.simplify_param_descrs

(

)

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

Definition at line 7206 of file z3py.py.

def simplify_param_descrs():
    """Return the set of parameter descriptions for Z3 `simplify` procedure."""
    return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())

def z3py.solve	(		args,
			keywords
	)

Solve the constraints `*args`.

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

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

Definition at line 7306 of file z3py.py.

Referenced by BV2Int(), and IsInt().

def solve(*args, **keywords):
    """Solve the constraints `*args`.
    
    This is a simple function for creating demonstrations. It creates a solver,
    configure it using the options in `keywords`, adds the constraints
    in `args`, and invokes check.
    
    >>> a = Int('a')
    >>> solve(a > 0, a < 2)
    [a = 1]
    """
    s = Solver()
    s.set(**keywords)
    s.add(*args)
    if keywords.get('show', False):
        print(s)
    r = s.check()
    if r == unsat:
        print("no solution")
    elif r == unknown:
        print("failed to solve")
        try:
            print(s.model())
        except Z3Exception:
            return
    else:
        print(s.model())

def z3py.solve_using	(		s,
			args,
			keywords
	)

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

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

Definition at line 7334 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.
    """
    if __debug__:
        _z3_assert(isinstance(s, Solver), "Solver object expected")
    s.set(**keywords)
    s.add(*args)
    if keywords.get('show', False):
        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 keywords.get('show', False):
            print("Solution:")
        print(s.model())

def z3py.SolverFor	(		logic,
			ctx = 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 6111 of file z3py.py.

def SolverFor(logic, ctx=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)

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

Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), and is_algebraic_value().

def Sqrt(a, ctx=None):
    """ Return a Z3 expression which represents the square root of a. 
    
    >>> x = Real('x')
    >>> Sqrt(x)
    x**(1/2)
    """
    if not is_expr(a):
        ctx = _get_ctx(ctx)
        a = RealVal(a, ctx)
    return a ** "1/2"

def z3py.SRem	(		a,
			b
	)

Create the Z3 expression signed remainder.

Use the operator % for signed modulus, and URem() for unsigned remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SRem(x, y)
SRem(x, y)
>>> SRem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'

Definition at line 3681 of file z3py.py.

Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and URem().

def SRem(a, b):
    """Create the Z3 expression signed remainder.
    
    Use the operator % for signed modulus, and URem() for unsigned remainder.
    
    >>> x = BitVec('x', 32)
    >>> y = BitVec('y', 32)
    >>> SRem(x, y)
    SRem(x, y)
    >>> SRem(x, y).sort()
    BitVec(32)
    >>> (x % y).sexpr()
    '(bvsmod x y)'
    >>> SRem(x, y).sexpr()
    '(bvsrem x y)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

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

Referenced by is_array(), and is_store().

def Store(a, i, v):
    """Return a Z3 store array expression.

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

def z3py.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 7210 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):
            m = m1
    if __debug__:
        _z3_assert(is_expr(t), "Z3 expression expected")
        _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
    num = len(m)
    _from = (Ast * num)()
    _to   = (Ast * num)()
    for i in range(num):
        _from[i] = m[i][0].as_ast()
        _to[i]   = m[i][1].as_ast()
    return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)

def z3py.substitute_vars	(		t,
			m
	)

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

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

Definition at line 7236 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 __debug__:
        _z3_assert(is_expr(t), "Z3 expression expected")
        _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
    num = len(m)
    _to   = (Ast * num)()
    for i in range(num):
        _to[i] = m[i].as_ast()
    return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)

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

Referenced by BitVecs(), Ints(), IntVector(), Reals(), and RealVector().

def Sum(*args):
    """Create the sum of the Z3 expressions. 
    
    >>> a, b, c = Ints('a b c')
    >>> Sum(a, b, c)
    a + b + c
    >>> Sum([a, b, c])
    a + b + c
    >>> A = IntVector('a', 5)
    >>> Sum(A)
    a__0 + a__1 + a__2 + a__3 + a__4
    """
    args  = _get_args(args)
    if __debug__:
        _z3_assert(len(args) > 0, "Non empty list of arguments expected")
    ctx   = _ctx_from_ast_arg_list(args)
    if __debug__:
        _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
    args  = _coerce_expr_list(args, ctx)
    if is_bv(args[0]):
        return _reduce(lambda a, b: a + b, args, 0)
    else:
        _args, sz = _to_ast_array(args)
        return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)

def z3py.tactic_description	(		name,
			ctx = None
	)

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

>>> d = tactic_description('simplify')

Definition at line 6896 of file z3py.py.

Referenced by describe_tactics().

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

    >>> d = tactic_description('simplify')
    """
    ctx = _get_ctx(ctx)
    return Z3_tactic_get_descr(ctx.ref(), name)

def z3py.tactics

(

ctx = None

)

Return a list of all available tactics in Z3.

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

Definition at line 6886 of file z3py.py.

Referenced by describe_tactics().

def tactics(ctx=None):
    """Return a list of all available tactics in Z3.
    
    >>> l = tactics()
    >>> l.count('simplify') == 1
    True
    """
    ctx = _get_ctx(ctx)
    return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]

def z3py.Then	(		ts,
			ks
	)

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

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

Definition at line 6778 of file z3py.py.

Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), Goal.depth(), Statistics.get_key_value(), and Statistics.keys().

06778 
06779 def Then(*ts, **ks):
06780     """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
06781     
06782     >>> x, y = Ints('x y')
06783     >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
06784     >>> t(And(x == 0, y > x + 1))
06785     [[Not(y <= 1)]]
06786     >>> t(And(x == 0, y > x + 1)).as_expr()
06787     Not(y <= 1)
06788     """
06789     return AndThen(*ts, **ks)
    

def z3py.to_symbol	(		s,
			ctx = None
	)

Convert an integer or string into a Z3 symbol.

Definition at line 94 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DeclareSort(), EnumSort(), FP(), Function(), Int(), prove(), Real(), Fixedpoint.set_predicate_representation(), SolverFor(), and Fixedpoint.update_rule().

def to_symbol(s, ctx=None):
    """Convert an integer or string into a Z3 symbol."""
    if isinstance(s, int):
        return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
    else:
        return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)

def z3py.ToInt

(

a

)

Return the Z3 expression ToInt(a). 

>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int

Definition at line 2859 of file z3py.py.

Referenced by is_to_int().

def ToInt(a):
    """ Return the Z3 expression ToInt(a). 
    
    >>> x = Real('x')
    >>> x.sort()
    Real
    >>> n = ToInt(x)
    >>> n
    ToInt(x)
    >>> n.sort()
    Int
    """
    if __debug__:
        _z3_assert(a.is_real(), "Z3 real expression expected.")
    ctx = a.ctx
    return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)

def z3py.ToReal

(

a

)

Return the Z3 expression ToReal(a). 

>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real

Definition at line 2842 of file z3py.py.

Referenced by ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), and is_to_real().

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

def z3py.tree_interpolant	(		pat,
			p = None,
			ctx = None
	)

Compute interpolant for a tree of formulas.

The input is an interpolation pattern over a set of formulas C.
The pattern pat is a formula combining the formulas in C using
logical conjunction and the "interp" operator (see Interp). This
interp operator is logically the identity operator. It marks the
sub-formulas of the pattern for which interpolants should be
computed. The interpolant is a map sigma from marked subformulas
to formulas, such that, for each marked subformula phi of pat
(where phi sigma is phi with sigma(psi) substituted for each
subformula psi of phi such that psi in dom(sigma)):

  1) phi sigma implies sigma(phi), and

  2) sigma(phi) is in the common uninterpreted vocabulary between
  the formulas of C occurring in phi and those not occurring in
  phi

  and moreover pat sigma implies false. In the simplest case
  an interpolant for the pattern "(and (interp A) B)" maps A
  to an interpolant for A /\ B. 

  The return value is a vector of formulas representing sigma. This
  vector contains sigma(phi) for each marked subformula of pat, in
  pre-order traversal. This means that subformulas of phi occur before phi
  in the vector. Also, subformulas that occur multiply in pat will
  occur multiply in the result vector.

If pat is satisfiable, raises an object of class ModelRef
that represents a model of pat.

If parameters p are supplied, these are used in creating the
solver that determines satisfiability.

>>> x = Int('x')
>>> y = Int('y')
>>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
[Not(x >= 0), Not(y <= 2)]

>>> g = And(Interpolant(x<0),x<2)
>>> try:
...     print tree_interpolant(g).sexpr()
... except ModelRef as m:
...     print m.sexpr()
(define-fun x () Int
  (- 1))

Definition at line 7531 of file z3py.py.

Referenced by binary_interpolant(), and sequence_interpolant().

def tree_interpolant(pat,p=None,ctx=None):
    """Compute interpolant for a tree of formulas.

    The input is an interpolation pattern over a set of formulas C.
    The pattern pat is a formula combining the formulas in C using
    logical conjunction and the "interp" operator (see Interp). This
    interp operator is logically the identity operator. It marks the
    sub-formulas of the pattern for which interpolants should be
    computed. The interpolant is a map sigma from marked subformulas
    to formulas, such that, for each marked subformula phi of pat
    (where phi sigma is phi with sigma(psi) substituted for each
    subformula psi of phi such that psi in dom(sigma)):

      1) phi sigma implies sigma(phi), and

      2) sigma(phi) is in the common uninterpreted vocabulary between
      the formulas of C occurring in phi and those not occurring in
      phi

      and moreover pat sigma implies false. In the simplest case
      an interpolant for the pattern "(and (interp A) B)" maps A
      to an interpolant for A /\ B. 

      The return value is a vector of formulas representing sigma. This
      vector contains sigma(phi) for each marked subformula of pat, in
      pre-order traversal. This means that subformulas of phi occur before phi
      in the vector. Also, subformulas that occur multiply in pat will
      occur multiply in the result vector.

    If pat is satisfiable, raises an object of class ModelRef
    that represents a model of pat.

    If parameters p are supplied, these are used in creating the
    solver that determines satisfiability.

    >>> x = Int('x')
    >>> y = Int('y')
    >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
    [Not(x >= 0), Not(y <= 2)]

    >>> g = And(Interpolant(x<0),x<2)
    >>> try:
    ...     print tree_interpolant(g).sexpr()
    ... except ModelRef as m:
    ...     print m.sexpr()
    (define-fun x () Int
      (- 1))
    """
    f = pat
    ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
    ptr = (AstVectorObj * 1)()
    mptr = (Model * 1)()
    if p == None:
        p = ParamsRef(ctx)
    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
    if res == Z3_L_FALSE:
        return AstVector(ptr[0],ctx)
    raise ModelRef(mptr[0], ctx)

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

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

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

Definition at line 6878 of file z3py.py.

def TryFor(t, ms, ctx=None):
    """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
    
    If `t` does not terminate in `ms` milliseconds, then it fails.
    """
    t = _to_tactic(t, ctx)
    return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)

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

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

def UDiv(a, b):
    """Create the Z3 expression (unsigned) division `self / other`.
    
    Use the operator / for signed division.
    
    >>> x = BitVec('x', 32)
    >>> y = BitVec('y', 32)
    >>> UDiv(x, y)
    UDiv(x, y)
    >>> UDiv(x, y).sort()
    BitVec(32)
    >>> (x / y).sexpr()
    '(bvsdiv x y)'
    >>> UDiv(x, y).sexpr()
    '(bvudiv x y)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.UGE	(		a,
			b
	)

Create the Z3 expression (unsigned) `other >= self`.

Use the operator >= for signed greater than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> UGE(x, y)
UGE(x, y)
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'

Definition at line 3607 of file z3py.py.

Referenced by BitVecRef.__ge__().

def UGE(a, b):
    """Create the Z3 expression (unsigned) `other >= self`.
    
    Use the operator >= for signed greater than or equal to.
    
    >>> x, y = BitVecs('x y', 32)
    >>> UGE(x, y)
    UGE(x, y)
    >>> (x >= y).sexpr()
    '(bvsge x y)'
    >>> UGE(x, y).sexpr()
    '(bvuge x y)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.UGT	(		a,
			b
	)

Create the Z3 expression (unsigned) `other > self`.

Use the operator > for signed greater than.

>>> x, y = BitVecs('x y', 32)
>>> UGT(x, y)
UGT(x, y)
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'

Definition at line 3624 of file z3py.py.

Referenced by BitVecRef.__gt__().

def UGT(a, b):
    """Create the Z3 expression (unsigned) `other > self`.
    
    Use the operator > for signed greater than.
    
    >>> x, y = BitVecs('x y', 32)
    >>> UGT(x, y)
    UGT(x, y)
    >>> (x > y).sexpr()
    '(bvsgt x y)'
    >>> UGT(x, y).sexpr()
    '(bvugt x y)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.ULE	(		a,
			b
	)

Create the Z3 expression (unsigned) `other <= self`.

Use the operator <= for signed less than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> ULE(x, y)
ULE(x, y)
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'

Definition at line 3573 of file z3py.py.

Referenced by BitVecRef.__le__().

def ULE(a, b):
    """Create the Z3 expression (unsigned) `other <= self`.
    
    Use the operator <= for signed less than or equal to.
    
    >>> x, y = BitVecs('x y', 32)
    >>> ULE(x, y)
    ULE(x, y)
    >>> (x <= y).sexpr()
    '(bvsle x y)'
    >>> ULE(x, y).sexpr()
    '(bvule x y)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

def z3py.ULT	(		a,
			b
	)

Create the Z3 expression (unsigned) `other < self`.

Use the operator < for signed less than.

>>> x, y = BitVecs('x y', 32)
>>> ULT(x, y)
ULT(x, y)
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'

Definition at line 3590 of file z3py.py.

Referenced by BitVecRef.__lt__().

def ULT(a, b):
    """Create the Z3 expression (unsigned) `other < self`.
    
    Use the operator < for signed less than.
    
    >>> x, y = BitVecs('x y', 32)
    >>> ULT(x, y)
    ULT(x, y)
    >>> (x < y).sexpr()
    '(bvslt x y)'
    >>> ULT(x, y).sexpr()
    '(bvult x y)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

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

Referenced by Store().

def Update(a, i, v):
    """Return a Z3 store array expression.

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

def z3py.URem	(		a,
			b
	)

Create the Z3 expression (unsigned) remainder `self % other`.

Use the operator % for signed modulus, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> URem(x, y)
URem(x, y)
>>> URem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'

Definition at line 3661 of file z3py.py.

Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and SRem().

def URem(a, b):
    """Create the Z3 expression (unsigned) remainder `self % other`.
    
    Use the operator % for signed modulus, and SRem() for signed remainder.
    
    >>> x = BitVec('x', 32)
    >>> y = BitVec('y', 32)
    >>> URem(x, y)
    URem(x, y)
    >>> URem(x, y).sort()
    BitVec(32)
    >>> (x % y).sexpr()
    '(bvsmod x y)'
    >>> URem(x, y).sexpr()
    '(bvurem x y)'
    """
    _check_bv_args(a, b)
    a, b = _coerce_exprs(a, b)
    return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

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

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

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

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

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

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

Definition at line 7144 of file z3py.py.

def When(p, t, ctx=None):
    """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
    
    >>> t = When(Probe('size') > 2, Tactic('simplify'))
    >>> x, y = Ints('x y')
    >>> g = Goal()
    >>> g.add(x > 0)
    >>> g.add(y > 0)
    >>> t(g)
    [[x > 0, y > 0]]
    >>> g.add(x == y + 1)
    >>> t(g)
    [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
    """
    p = _to_probe(p, ctx)
    t = _to_tactic(t, ctx)
    return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)

def z3py.With	(		t,
			args,
			keys
	)

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

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

Definition at line 6846 of file z3py.py.

Referenced by Goal.prec().

def With(t, *args, **keys):
    """Return a tactic that applies tactic `t` using the given configuration options.
    
    >>> x, y = Ints('x y')
    >>> t = With(Tactic('simplify'), som=True)
    >>> t((x + 1)*(y + 2) == 0)
    [[2*x + y + x*y == -2]]
    """
    ctx = keys.get('ctx', None)
    t = _to_tactic(t, ctx)
    p = args2params(args, keys, t.ctx)
    return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)

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

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

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

def z3py.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 3791 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 __debug__:
        _z3_assert(isinstance(n, int), "First argument must be an integer")
        _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
    return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)

---

Variable Documentation

int _dflt_fpsort_ebits = 11

Definition at line 7651 of file z3py.py.

int _dflt_fpsort_sbits = 53

Definition at line 7652 of file z3py.py.

_dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO

Floating-Point Arithmetic.

Definition at line 7650 of file z3py.py.

tuple _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)

Definition at line 108 of file z3py.py.

_main_ctx = None

Definition at line 187 of file z3py.py.

tuple _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)

Definition at line 126 of file z3py.py.

tuple sat = CheckSatResult(Z3_L_TRUE)

Definition at line 5771 of file z3py.py.

tuple unknown = CheckSatResult(Z3_L_UNDEF)

Definition at line 5773 of file z3py.py.

tuple unsat = CheckSatResult(Z3_L_FALSE)

Definition at line 5772 of file z3py.py.