z3py.py File Reference

Go to the source code of this file.

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
class	FPSortRef
	FP Sorts. More...
class	FPRMSortRef
class	FPRef
	FP Expressions. More...
class	FPRMRef
class	FPNumRef
	FP Numerals. More...

Namespaces
	z3py

Functions
def	enable_trace (msg)
def	disable_trace (msg)
def	get_version_string ()
def	get_version ()
def	open_log (fname)
def	append_log (s)
def	to_symbol
def	main_ctx ()
def	set_param (args, kws)
def	reset_params ()
def	set_option (args, kws)
def	get_param (name)
def	is_ast (a)
def	eq (a, b)
def	is_sort (s)
def	DeclareSort
def	is_func_decl (a)
def	Function (name, sig)
def	is_expr (a)
def	is_app (a)
def	is_const (a)
def	is_var (a)
def	get_var_index (a)
def	is_app_of (a, k)
def	If
def	Distinct (args)
def	Const (name, sort)
def	Consts (names, sort)
def	Var (idx, s)
def	RealVar
def	RealVarVector
def	is_bool (a)
def	is_true (a)
def	is_false (a)
def	is_and (a)
def	is_or (a)
def	is_not (a)
def	is_eq (a)
def	is_distinct (a)
def	BoolSort
def	BoolVal
def	Bool
def	Bools
def	BoolVector
def	FreshBool
def	Implies
def	Xor
def	Not
def	And (args)
def	Or (args)
def	is_pattern (a)
def	MultiPattern (args)
def	is_quantifier (a)
def	ForAll
def	Exists
def	is_arith_sort (s)
def	is_arith (a)
def	is_int (a)
def	is_real (a)
def	is_int_value (a)
def	is_rational_value (a)
def	is_algebraic_value (a)
def	is_add (a)
def	is_mul (a)
def	is_sub (a)
def	is_div (a)
def	is_idiv (a)
def	is_mod (a)
def	is_le (a)
def	is_lt (a)
def	is_ge (a)
def	is_gt (a)
def	is_is_int (a)
def	is_to_real (a)
def	is_to_int (a)
def	IntSort
def	RealSort
def	IntVal
def	RealVal
def	RatVal
def	Q
def	Int
def	Ints
def	IntVector
def	FreshInt
def	Real
def	Reals
def	RealVector
def	FreshReal
def	ToReal (a)
def	ToInt (a)
def	IsInt (a)
def	Sqrt
def	Cbrt
def	is_bv_sort (s)
def	is_bv (a)
def	is_bv_value (a)
def	BV2Int (a)
def	BitVecSort
def	BitVecVal
def	BitVec
def	BitVecs
def	Concat (args)
def	Extract (high, low, a)
def	ULE (a, b)
def	ULT (a, b)
def	UGE (a, b)
def	UGT (a, b)
def	UDiv (a, b)
def	URem (a, b)
def	SRem (a, b)
def	LShR (a, b)
def	RotateLeft (a, b)
def	RotateRight (a, b)
def	SignExt (n, a)
def	ZeroExt (n, a)
def	RepeatBitVec (n, a)
def	BVRedAnd (a)
def	BVRedOr (a)
def	is_array (a)
def	is_const_array (a)
def	is_K (a)
def	is_map (a)
def	get_map_func (a)
def	ArraySort (d, r)
def	Array (name, dom, rng)
def	Update (a, i, v)
def	Store (a, i, v)
def	Select (a, i)
def	Map (f, args)
def	K (dom, v)
def	is_select (a)
def	is_store (a)
def	CreateDatatypes (ds)
def	EnumSort
def	args2params
def	is_as_array (n)
def	get_as_array_func (n)
def	SolverFor
def	SimpleSolver
def	AndThen (ts, ks)
def	Then (ts, ks)
def	OrElse (ts, ks)
def	ParOr (ts, ks)
def	ParThen
def	ParAndThen
def	With (t, args, keys)
def	Repeat
def	TryFor
def	tactics
def	tactic_description
def	describe_tactics ()
def	is_probe (p)
def	probes
def	probe_description
def	describe_probes ()
def	FailIf
def	When
def	Cond
def	simplify (a, arguments, keywords)
	Utils. More...
def	help_simplify ()
def	simplify_param_descrs ()
def	substitute (t, m)
def	substitute_vars (t, m)
def	Sum (args)
def	Product (args)
def	solve (args, keywords)
def	solve_using (s, args, keywords)
def	prove (claim, keywords)
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 (s)
def	is_fprm_sort (s)
def	RoundNearestTiesToEven
def	RNE
def	RoundNearestTiesToAway
def	RNA
def	RoundTowardPositive
def	RTP
def	RoundTowardNegative
def	RTN
def	RoundTowardZero
def	RTZ
def	is_fprm (a)
def	is_fprm_value (a)
def	is_fp (a)
def	is_fp_value (a)
def	FPSort
def	fpNaN (s)
def	fpPlusInfinity (s)
def	fpMinusInfinity (s)
def	fpInfinity (s, negative)
def	fpPlusZero (s)
def	fpMinusZero (s)
def	fpZero (s, negative)
def	FPVal
def	FP
def	FPs
def	fpAbs (a)
def	fpNeg (a)
def	fpAdd (rm, a, b)
def	fpSub (rm, a, b)
def	fpMul (rm, a, b)
def	fpDiv (rm, a, b)
def	fpRem (a, b)
def	fpMin (a, b)
def	fpMax (a, b)
def	fpFMA (rm, a, b, c)
def	fpSqrt (rm, a)
def	fpRoundToIntegral (rm, a)
def	fpIsNaN (a)
def	fpIsInfinite (a)
def	fpIsZero (a)
def	fpIsNormal (a)
def	fpIsSubnormal (a)
def	fpIsNegative (a)
def	fpIsPositive (a)
def	fpLT (a, b)
def	fpLEQ (a, b)
def	fpGT (a, b)
def	fpGEQ (a, b)
def	fpEQ (a, b)
def	fpNEQ (a, b)
def	fpFP (sgn, exp, sig)
def	fpToFP
def	fpToFPUnsigned (rm, x, s)
def	fpToSBV (rm, x, s)
def	fpToUBV (rm, x, s)
def	fpToReal (x)
def	fpToIEEEBV (x)

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