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	TypeVarRef
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	Simplifier
class	Tactic
class	Probe
class	ParserContext
class	FPSortRef
class	FPRMSortRef
class	FPRef
class	FPRMRef
class	FPNumRef
class	SeqSortRef
	Strings, Sequences and Regular expressions. More...
class	CharSortRef
class	SeqRef
class	CharRef
class	ReSortRef
class	ReRef
class	OnClause
class	PropClosures
class	UserPropagateBase

Namespaces
namespace	z3py

Functions
	z3_debug ()
	_is_int (v)
	enable_trace (msg)
	disable_trace (msg)
	get_version_string ()
	get_version ()
	get_full_version ()
	_z3_assert (cond, msg)
	_z3_check_cint_overflow (n, name)
	open_log (fname)
	append_log (s)
	to_symbol (s, ctx=None)
	_symbol2py (ctx, s)
	_get_args (args)
	_get_args_ast_list (args)
	_to_param_value (val)
	z3_error_handler (c, e)
Context	main_ctx ()
Context	_get_ctx (ctx)
Context	get_ctx (ctx)
	set_param (*args, **kws)
None	reset_params ()
	set_option (*args, **kws)
	get_param (name)
bool	is_ast (Any a)
bool	eq (AstRef a, AstRef b)
int	_ast_kind (Context ctx, Any a)
	_ctx_from_ast_arg_list (args, default_ctx=None)
	_ctx_from_ast_args (*args)
	_to_func_decl_array (args)
	_to_ast_array (args)
	_to_ref_array (ref, args)
	_to_ast_ref (a, ctx)
	_sort_kind (ctx, s)
	Sorts.
bool	is_sort (Any s)
	_to_sort_ref (s, ctx)
SortRef	_sort (Context ctx, Any a)
SortRef	DeclareSort (name, ctx=None)
	DeclareTypeVar (name, ctx=None)
	is_func_decl (a)
	Function (name, *sig)
	FreshFunction (*sig)
	_to_func_decl_ref (a, ctx)
	RecFunction (name, *sig)
	RecAddDefinition (f, args, body)
	deserialize (st)
	_to_expr_ref (a, ctx)
	_coerce_expr_merge (s, a)
	_check_same_sort (a, b, ctx=None)
	_coerce_exprs (a, b, ctx=None)
	_reduce (func, sequence, initial)
	_coerce_expr_list (alist, ctx=None)
	is_expr (a)
	is_app (a)
	is_const (a)
	is_var (a)
	get_var_index (a)
	is_app_of (a, k)
	If (a, b, c, ctx=None)
	Distinct (*args)
	_mk_bin (f, a, b)
	Const (name, sort)
	Consts (names, sort)
	FreshConst (sort, prefix="c")
ExprRef	Var (int idx, SortRef s)
ExprRef	RealVar (int idx, ctx=None)
	RealVarVector (int n, ctx=None)
bool	is_bool (Any a)
bool	is_true (Any a)
bool	is_false (Any a)
bool	is_and (Any a)
bool	is_or (Any a)
bool	is_implies (Any a)
bool	is_not (Any a)
bool	is_eq (Any a)
bool	is_distinct (Any a)
	BoolSort (ctx=None)
	BoolVal (val, ctx=None)
	Bool (name, ctx=None)
	Bools (names, ctx=None)
	BoolVector (prefix, sz, ctx=None)
	FreshBool (prefix="b", ctx=None)
	Implies (a, b, ctx=None)
	Xor (a, b, ctx=None)
	Not (a, ctx=None)
	mk_not (a)
	_has_probe (args)
	And (*args)
	Or (*args)
	is_pattern (a)
	MultiPattern (*args)
	_to_pattern (arg)
	is_quantifier (a)
	_mk_quantifier (is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
	ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
	Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
	Lambda (vs, body)
bool	is_arith_sort (Any s)
	is_arith (a)
bool	is_int (a)
	is_real (a)
	_is_numeral (ctx, a)
	_is_algebraic (ctx, a)
	is_int_value (a)
	is_rational_value (a)
	is_algebraic_value (a)
bool	is_add (Any a)
bool	is_mul (Any a)
bool	is_sub (Any a)
bool	is_div (Any a)
bool	is_idiv (Any a)
bool	is_mod (Any a)
bool	is_le (Any a)
bool	is_lt (Any a)
bool	is_ge (Any a)
bool	is_gt (Any a)
bool	is_is_int (Any a)
bool	is_to_real (Any a)
bool	is_to_int (Any a)
	_py2expr (a, ctx=None)
	IntSort (ctx=None)
	RealSort (ctx=None)
	_to_int_str (val)
	IntVal (val, ctx=None)
	RealVal (val, ctx=None)
	RatVal (a, b, ctx=None)
	Q (a, b, ctx=None)
	Int (name, ctx=None)
	Ints (names, ctx=None)
	IntVector (prefix, sz, ctx=None)
	FreshInt (prefix="x", ctx=None)
	Real (name, ctx=None)
	Reals (names, ctx=None)
	RealVector (prefix, sz, ctx=None)
	FreshReal (prefix="b", ctx=None)
	ToReal (a)
	ToInt (a)
	IsInt (a)
	Sqrt (a, ctx=None)
	Cbrt (a, ctx=None)
	is_bv_sort (s)
	is_bv (a)
	is_bv_value (a)
	BV2Int (a, is_signed=False)
	Int2BV (a, num_bits)
	BitVecSort (sz, ctx=None)
	BitVecVal (val, bv, ctx=None)
	BitVec (name, bv, ctx=None)
	BitVecs (names, bv, ctx=None)
	Concat (*args)
	Extract (high, low, a)
	_check_bv_args (a, b)
	ULE (a, b)
	ULT (a, b)
	UGE (a, b)
	UGT (a, b)
	UDiv (a, b)
	URem (a, b)
	SRem (a, b)
	LShR (a, b)
	RotateLeft (a, b)
	RotateRight (a, b)
	SignExt (n, a)
	ZeroExt (n, a)
	RepeatBitVec (n, a)
	BVRedAnd (a)
	BVRedOr (a)
	BVAddNoOverflow (a, b, signed)
	BVAddNoUnderflow (a, b)
	BVSubNoOverflow (a, b)
	BVSubNoUnderflow (a, b, signed)
	BVSDivNoOverflow (a, b)
	BVSNegNoOverflow (a)
	BVMulNoOverflow (a, b, signed)
	BVMulNoUnderflow (a, b)
	_array_select (ar, arg)
	is_array_sort (a)
bool	is_array (Any a)
	is_const_array (a)
	is_K (a)
	is_map (a)
	is_default (a)
	get_map_func (a)
	ArraySort (*sig)
	Array (name, *sorts)
	Update (a, *args)
	Default (a)
	Store (a, *args)
	Select (a, *args)
	Map (f, *args)
	K (dom, v)
	Ext (a, b)
	is_select (a)
	is_store (a)
	SetSort (s)
	Sets.
	EmptySet (s)
	FullSet (s)
	SetUnion (*args)
	SetIntersect (*args)
	SetAdd (s, e)
	SetDel (s, e)
	SetComplement (s)
	SetDifference (a, b)
	IsMember (e, s)
	IsSubset (a, b)
	_valid_accessor (acc)
	Datatypes.
	CreateDatatypes (*ds)
	DatatypeSort (name, params=None, ctx=None)
	TupleSort (name, sorts, ctx=None)
	DisjointSum (name, sorts, ctx=None)
	EnumSort (name, values, ctx=None)
	args2params (arguments, keywords, ctx=None)
	Model (ctx=None, eval={})
	is_as_array (n)
	get_as_array_func (n)
	SolverFor (logic, ctx=None, logFile=None)
	SimpleSolver (ctx=None, logFile=None)
	FiniteDomainSort (name, sz, ctx=None)
	is_finite_domain_sort (s)
	is_finite_domain (a)
	FiniteDomainVal (val, sort, ctx=None)
	is_finite_domain_value (a)
	_global_on_model (ctx)
	_to_goal (a)
	_to_tactic (t, ctx=None)
	_and_then (t1, t2, ctx=None)
	_or_else (t1, t2, ctx=None)
	AndThen (*ts, **ks)
	Then (*ts, **ks)
	OrElse (*ts, **ks)
	ParOr (*ts, **ks)
	ParThen (t1, t2, ctx=None)
	ParAndThen (t1, t2, ctx=None)
	With (t, *args, **keys)
	WithParams (t, p)
	Repeat (t, max=4294967295, ctx=None)
	TryFor (t, ms, ctx=None)
	tactics (ctx=None)
	tactic_description (name, ctx=None)
	describe_tactics ()
	is_probe (p)
	_to_probe (p, ctx=None)
	probes (ctx=None)
	probe_description (name, ctx=None)
	describe_probes ()
	_probe_nary (f, args, ctx)
	_probe_and (args, ctx)
	_probe_or (args, ctx)
	FailIf (p, ctx=None)
	When (p, t, ctx=None)
	Cond (p, t1, t2, ctx=None)
	simplify (a, *arguments, **keywords)
	Utils.
	help_simplify ()
	simplify_param_descrs ()
	substitute (t, *m)
	substitute_vars (t, *m)
	substitute_funs (t, *m)
	Sum (*args)
	Product (*args)
	Abs (arg)
	AtMost (*args)
	AtLeast (*args)
	_reorder_pb_arg (arg)
	_pb_args_coeffs (args, default_ctx=None)
	PbLe (args, k)
	PbGe (args, k)
	PbEq (args, k, ctx=None)
	solve (*args, **keywords)
	solve_using (s, *args, **keywords)
	prove (claim, show=False, **keywords)
	_solve_html (*args, **keywords)
	_solve_using_html (s, *args, **keywords)
	_prove_html (claim, show=False, **keywords)
	_dict2sarray (sorts, ctx)
	_dict2darray (decls, ctx)
	parse_smt2_string (s, sorts={}, decls={}, ctx=None)
	parse_smt2_file (f, sorts={}, decls={}, ctx=None)
	get_default_rounding_mode (ctx=None)
	set_default_rounding_mode (rm, ctx=None)
	get_default_fp_sort (ctx=None)
	set_default_fp_sort (ebits, sbits, ctx=None)
	_dflt_rm (ctx=None)
	_dflt_fps (ctx=None)
	_coerce_fp_expr_list (alist, ctx)
	Float16 (ctx=None)
	FloatHalf (ctx=None)
	Float32 (ctx=None)
	FloatSingle (ctx=None)
	Float64 (ctx=None)
	FloatDouble (ctx=None)
	Float128 (ctx=None)
	FloatQuadruple (ctx=None)
	is_fp_sort (s)
	is_fprm_sort (s)
	RoundNearestTiesToEven (ctx=None)
	RNE (ctx=None)
	RoundNearestTiesToAway (ctx=None)
	RNA (ctx=None)
	RoundTowardPositive (ctx=None)
	RTP (ctx=None)
	RoundTowardNegative (ctx=None)
	RTN (ctx=None)
	RoundTowardZero (ctx=None)
	RTZ (ctx=None)
	is_fprm (a)
	is_fprm_value (a)
	is_fp (a)
	is_fp_value (a)
	FPSort (ebits, sbits, ctx=None)
	_to_float_str (val, exp=0)
	fpNaN (s)
	fpPlusInfinity (s)
	fpMinusInfinity (s)
	fpInfinity (s, negative)
	fpPlusZero (s)
	fpMinusZero (s)
	fpZero (s, negative)
	FPVal (sig, exp=None, fps=None, ctx=None)
	FP (name, fpsort, ctx=None)
	FPs (names, fpsort, ctx=None)
	fpAbs (a, ctx=None)
	fpNeg (a, ctx=None)
	_mk_fp_unary (f, rm, a, ctx)
	_mk_fp_unary_pred (f, a, ctx)
	_mk_fp_bin (f, rm, a, b, ctx)
	_mk_fp_bin_norm (f, a, b, ctx)
	_mk_fp_bin_pred (f, a, b, ctx)
	_mk_fp_tern (f, rm, a, b, c, ctx)
	fpAdd (rm, a, b, ctx=None)
	fpSub (rm, a, b, ctx=None)
	fpMul (rm, a, b, ctx=None)
	fpDiv (rm, a, b, ctx=None)
	fpRem (a, b, ctx=None)
	fpMin (a, b, ctx=None)
	fpMax (a, b, ctx=None)
	fpFMA (rm, a, b, c, ctx=None)
	fpSqrt (rm, a, ctx=None)
	fpRoundToIntegral (rm, a, ctx=None)
	fpIsNaN (a, ctx=None)
	fpIsInf (a, ctx=None)
	fpIsZero (a, ctx=None)
	fpIsNormal (a, ctx=None)
	fpIsSubnormal (a, ctx=None)
	fpIsNegative (a, ctx=None)
	fpIsPositive (a, ctx=None)
	_check_fp_args (a, b)
	fpLT (a, b, ctx=None)
	fpLEQ (a, b, ctx=None)
	fpGT (a, b, ctx=None)
	fpGEQ (a, b, ctx=None)
	fpEQ (a, b, ctx=None)
	fpNEQ (a, b, ctx=None)
	fpFP (sgn, exp, sig, ctx=None)
	fpToFP (a1, a2=None, a3=None, ctx=None)
	fpBVToFP (v, sort, ctx=None)
	fpFPToFP (rm, v, sort, ctx=None)
	fpRealToFP (rm, v, sort, ctx=None)
	fpSignedToFP (rm, v, sort, ctx=None)
	fpUnsignedToFP (rm, v, sort, ctx=None)
	fpToFPUnsigned (rm, x, s, ctx=None)
	fpToSBV (rm, x, s, ctx=None)
	fpToUBV (rm, x, s, ctx=None)
	fpToReal (x, ctx=None)
	fpToIEEEBV (x, ctx=None)
	StringSort (ctx=None)
	CharSort (ctx=None)
	SeqSort (s)
	_coerce_char (ch, ctx=None)
	CharVal (ch, ctx=None)
	CharFromBv (bv)
	CharToBv (ch, ctx=None)
	CharToInt (ch, ctx=None)
	CharIsDigit (ch, ctx=None)
	_coerce_seq (s, ctx=None)
	_get_ctx2 (a, b, ctx=None)
	is_seq (a)
bool	is_string (Any a)
bool	is_string_value (Any a)
	StringVal (s, ctx=None)
	String (name, ctx=None)
	Strings (names, ctx=None)
	SubString (s, offset, length)
	SubSeq (s, offset, length)
	Empty (s)
	Full (s)
	Unit (a)
	PrefixOf (a, b)
	SuffixOf (a, b)
	Contains (a, b)
	Replace (s, src, dst)
	IndexOf (s, substr, offset=None)
	LastIndexOf (s, substr)
	Length (s)
	SeqMap (f, s)
	SeqMapI (f, i, s)
	SeqFoldLeft (f, a, s)
	SeqFoldLeftI (f, i, a, s)
	StrToInt (s)
	IntToStr (s)
	StrToCode (s)
	StrFromCode (c)
	Re (s, ctx=None)
	ReSort (s)
	is_re (s)
	InRe (s, re)
	Union (*args)
	Intersect (*args)
	Plus (re)
	Option (re)
	Complement (re)
	Star (re)
	Loop (re, lo, hi=0)
	Range (lo, hi, ctx=None)
	Diff (a, b, ctx=None)
	AllChar (regex_sort, ctx=None)
	PartialOrder (a, index)
	LinearOrder (a, index)
	TreeOrder (a, index)
	PiecewiseLinearOrder (a, index)
	TransitiveClosure (f)
	to_Ast (ptr)
	to_ContextObj (ptr)
	to_AstVectorObj (ptr)
	on_clause_eh (ctx, p, n, dep, clause)
	ensure_prop_closures ()
	user_prop_push (ctx, cb)
	user_prop_pop (ctx, cb, num_scopes)
	user_prop_fresh (ctx, _new_ctx)
	user_prop_fixed (ctx, cb, id, value)
	user_prop_created (ctx, cb, id)
	user_prop_final (ctx, cb)
	user_prop_eq (ctx, cb, x, y)
	user_prop_diseq (ctx, cb, x, y)
	user_prop_decide (ctx, cb, t_ref, idx, phase)
	user_prop_binding (ctx, cb, q_ref, inst_ref)
	PropagateFunction (name, *sig)

Variables
	Z3_DEBUG = __debug__
	_main_ctx = None
	sat = CheckSatResult(Z3_L_TRUE)
	unsat = CheckSatResult(Z3_L_FALSE)
	unknown = CheckSatResult(Z3_L_UNDEF)
dict	_on_models = {}
	_on_model_eh = on_model_eh_type(_global_on_model)
	_dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
	Floating-Point Arithmetic.
int	_dflt_fpsort_ebits = 11
int	_dflt_fpsort_sbits = 53
	_ROUNDING_MODES
	_my_hacky_class = None
	_on_clause_eh = Z3_on_clause_eh(on_clause_eh)
	_prop_closures = None
	_user_prop_push = Z3_push_eh(user_prop_push)
	_user_prop_pop = Z3_pop_eh(user_prop_pop)
	_user_prop_fresh = Z3_fresh_eh(user_prop_fresh)
	_user_prop_fixed = Z3_fixed_eh(user_prop_fixed)
	_user_prop_created = Z3_created_eh(user_prop_created)
	_user_prop_final = Z3_final_eh(user_prop_final)
	_user_prop_eq = Z3_eq_eh(user_prop_eq)
	_user_prop_diseq = Z3_eq_eh(user_prop_diseq)
	_user_prop_decide = Z3_decide_eh(user_prop_decide)
	_user_prop_binding = Z3_on_binding_eh(user_prop_binding)