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	FiniteDomainSortRef
class	FiniteDomainRef
class	FiniteDomainNumRef
class	OptimizeObjective
	Optimize. More...
class	Optimize
class	ApplyResult
class	Tactic
class	Probe
class	FPSortRef
class	FPRMSortRef
class	FPRef
class	FPRMRef
class	FPNumRef
class	SeqSortRef
	Strings, Sequences and Regular expressions. More...
class	CharSortRef
class	SeqRef
class	ReSortRef
class	ReRef
class	PropClosures
class	UserPropagateBase

Namespaces
	z3py

Functions
def	z3_debug ()
def	enable_trace (msg)
def	disable_trace (msg)
def	get_version_string ()
def	get_version ()
def	get_full_version ()
def	open_log (fname)
def	append_log (s)
def	to_symbol
def	z3_error_handler (c, e)
def	main_ctx ()
def	get_ctx (ctx)
def	set_param (args, kws)
def	reset_params ()
def	set_option (args, kws)
def	get_param (name)
def	is_ast (a)
def	eq (a, b)
def	is_sort (s)
def	DeclareSort
def	is_func_decl (a)
def	Function (name, sig)
def	FreshFunction (sig)
def	RecFunction (name, sig)
def	RecAddDefinition (f, args, body)
def	is_expr (a)
def	is_app (a)
def	is_const (a)
def	is_var (a)
def	get_var_index (a)
def	is_app_of (a, k)
def	If
def	Distinct (args)
def	Const (name, sort)
def	Consts (names, sort)
def	FreshConst
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_implies (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	mk_not (a)
def	And (args)
def	Or (args)
def	is_pattern (a)
def	MultiPattern (args)
def	is_quantifier (a)
def	ForAll
def	Exists
def	Lambda (vs, body)
def	is_arith_sort (s)
def	is_arith (a)
def	is_int (a)
def	is_real (a)
def	is_int_value (a)
def	is_rational_value (a)
def	is_algebraic_value (a)
def	is_add (a)
def	is_mul (a)
def	is_sub (a)
def	is_div (a)
def	is_idiv (a)
def	is_mod (a)
def	is_le (a)
def	is_lt (a)
def	is_ge (a)
def	is_gt (a)
def	is_is_int (a)
def	is_to_real (a)
def	is_to_int (a)
def	IntSort
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
def	Int2BV (a, num_bits)
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	BVAddNoOverflow (a, b, signed)
def	BVAddNoUnderflow (a, b)
def	BVSubNoOverflow (a, b)
def	BVSubNoUnderflow (a, b, signed)
def	BVSDivNoOverflow (a, b)
def	BVSNegNoOverflow (a)
def	BVMulNoOverflow (a, b, signed)
def	BVMulNoUnderflow (a, b)
def	is_array_sort (a)
def	is_array (a)
def	is_const_array (a)
def	is_K (a)
def	is_map (a)
def	is_default (a)
def	get_map_func (a)
def	ArraySort (sig)
def	Array (name, dom, rng)
def	Update (a, i, v)
def	Default (a)
def	Store (a, i, v)
def	Select (a, i)
def	Map (f, args)
def	K (dom, v)
def	Ext (a, b)
def	SetHasSize (a, k)
def	is_select (a)
def	is_store (a)
def	SetSort (s)
	Sets. More...
def	EmptySet (s)
def	FullSet (s)
def	SetUnion (args)
def	SetIntersect (args)
def	SetAdd (s, e)
def	SetDel (s, e)
def	SetComplement (s)
def	SetDifference (a, b)
def	IsMember (e, s)
def	IsSubset (a, b)
def	CreateDatatypes (ds)
def	TupleSort
def	DisjointSum
def	EnumSort
def	args2params
def	Model
def	is_as_array (n)
def	get_as_array_func (n)
def	SolverFor
def	SimpleSolver
def	FiniteDomainSort
def	is_finite_domain_sort (s)
def	is_finite_domain (a)
def	FiniteDomainVal
def	is_finite_domain_value (a)
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	WithParams (t, p)
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	AtMost (args)
def	AtLeast (args)
def	PbLe (args, k)
def	PbGe (args, k)
def	PbEq
def	solve (args, keywords)
def	solve_using (s, args, keywords)
def	prove (claim, show=False, keywords)
def	parse_smt2_string
def	parse_smt2_file
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	FloatDouble
def	Float128
def	FloatQuadruple
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
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	fpIsInf
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	fpBVToFP
def	fpFPToFP
def	fpRealToFP
def	fpSignedToFP
def	fpUnsignedToFP
def	fpToFPUnsigned
def	fpToSBV
def	fpToUBV
def	fpToReal
def	fpToIEEEBV
def	StringSort
def	CharSort
def	SeqSort (s)
def	is_seq (a)
def	is_string (a)
def	is_string_value (a)
def	StringVal
def	String
def	Strings
def	SubString (s, offset, length)
def	SubSeq (s, offset, length)
def	Empty (s)
def	Full (s)
def	Unit (a)
def	PrefixOf (a, b)
def	SuffixOf (a, b)
def	Contains (a, b)
def	Replace (s, src, dst)
def	IndexOf
def	LastIndexOf (s, substr)
def	Length (s)
def	StrToInt (s)
def	IntToStr (s)
def	Re
def	ReSort (s)
def	is_re (s)
def	InRe (s, re)
def	Union (args)
def	Intersect (args)
def	Plus (re)
def	Option (re)
def	Complement (re)
def	Star (re)
def	Loop
def	Range
def	AllChar
def	PartialOrder (a, index)
def	LinearOrder (a, index)
def	TreeOrder (a, index)
def	PiecewiseLinearOrder (a, index)
def	TransitiveClosure (f)
def	ensure_prop_closures ()
def	user_prop_push (ctx)
def	user_prop_pop (ctx, num_scopes)
def	user_prop_fresh (id, ctx)
def	user_prop_fixed (ctx, cb, id, value)
def	user_prop_final (ctx, cb)
def	user_prop_eq (ctx, cb, x, y)
def	user_prop_diseq (ctx, cb, x, y)

Variables
	Z3_DEBUG = __debug__
	_main_ctx = None
tuple	sat = CheckSatResult(Z3_L_TRUE)
tuple	unsat = CheckSatResult(Z3_L_FALSE)
tuple	unknown = CheckSatResult(Z3_L_UNDEF)
dictionary	_on_models = {}
tuple	_on_model_eh = on_model_eh_type(_global_on_model)
	_dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
	Floating-Point Arithmetic. More...
int	_dflt_fpsort_ebits = 11
int	_dflt_fpsort_sbits = 53
tuple	_ROUNDING_MODES
	_prop_closures = None
tuple	_user_prop_push = push_eh_type(user_prop_push)
tuple	_user_prop_pop = pop_eh_type(user_prop_pop)
tuple	_user_prop_fresh = fresh_eh_type(user_prop_fresh)
tuple	_user_prop_fixed = fixed_eh_type(user_prop_fixed)
tuple	_user_prop_final = final_eh_type(user_prop_final)
tuple	_user_prop_eq = eq_eh_type(user_prop_eq)
tuple	_user_prop_diseq = eq_eh_type(user_prop_diseq)