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