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	ApplyResult
class	Tactic
class	Probe

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_option
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	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	is_array
def	is_select
def	is_store
def	is_const_array
def	is_K
def	is_map
def	get_map_func
def	ArraySort
def	Array
def	Update
def	Store
def	Select
def	Map
def	K
def	CreateDatatypes
def	EnumSort
def	args2params
def	is_as_array
def	get_as_array_func
def	SolverFor
def	SimpleSolver
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

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)

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

Referenced by Goal.as_expr(), Bool(), Bools(), and BoolVector().

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