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) | |
main_ctx () | |
_get_ctx (ctx) | |
get_ctx (ctx) | |
set_param (*args, **kws) | |
reset_params () | |
set_option (*args, **kws) | |
get_param (name) | |
is_ast (a) | |
eq (a, b) | |
_ast_kind (ctx, 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. | |
is_sort (s) | |
_to_sort_ref (s, ctx) | |
_sort (ctx, a) | |
DeclareSort (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) | |
_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") | |
Var (idx, s) | |
RealVar (idx, ctx=None) | |
RealVarVector (n, ctx=None) | |
is_bool (a) | |
is_true (a) | |
is_false (a) | |
is_and (a) | |
is_or (a) | |
is_implies (a) | |
is_not (a) | |
is_eq (a) | |
is_distinct (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) | |
is_arith_sort (s) | |
is_arith (a) | |
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) | |
is_add (a) | |
is_mul (a) | |
is_sub (a) | |
is_div (a) | |
is_idiv (a) | |
is_mod (a) | |
is_le (a) | |
is_lt (a) | |
is_ge (a) | |
is_gt (a) | |
is_is_int (a) | |
is_to_real (a) | |
is_to_int (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) | |
is_array (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) | |
SetHasSize (a, k) | |
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, 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) | |
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 (ch, ctx=None) | |
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) | |
is_string (a) | |
is_string_value (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) | |
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, 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_ref, phase_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) | |
|
protected |
Definition at line 8329 of file z3py.py.
Referenced by AndThen().
|
protected |
Definition at line 4590 of file z3py.py.
Referenced by QuantifierRef.__getitem__(), and ArrayRef.__getitem__().
|
protected |
Definition at line 491 of file z3py.py.
Referenced by _to_ast_ref(), is_app(), and is_var().
|
protected |
Definition at line 4151 of file z3py.py.
Referenced by BVAddNoOverflow(), BVAddNoUnderflow(), BVMulNoOverflow(), BVMulNoUnderflow(), BVSDivNoOverflow(), BVSubNoOverflow(), BVSubNoUnderflow(), LShR(), RotateLeft(), RotateRight(), SRem(), UDiv(), UGE(), UGT(), ULE(), ULT(), and URem().
|
protected |
|
protected |
Definition at line 10871 of file z3py.py.
Referenced by CharRef.__le__(), CharIsDigit(), CharToBv(), and CharToInt().
|
protected |
Definition at line 1226 of file z3py.py.
Referenced by _coerce_fp_expr_list(), _pb_args_coeffs(), And(), AtLeast(), AtMost(), Distinct(), Or(), Product(), and Sum().
|
protected |
Definition at line 1179 of file z3py.py.
Referenced by _coerce_exprs().
|
protected |
Definition at line 1198 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), ArithRef.__gt__(), BitVecRef.__gt__(), ArithRef.__le__(), BitVecRef.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BVAddNoOverflow(), BVAddNoUnderflow(), BVMulNoOverflow(), BVMulNoUnderflow(), BVSDivNoOverflow(), BVSubNoOverflow(), BVSubNoUnderflow(), Extract(), If(), LShR(), RotateLeft(), RotateRight(), SRem(), UDiv(), UGE(), UGT(), ULE(), ULT(), and URem().
|
protected |
Definition at line 9390 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), _mk_fp_bin(), _mk_fp_bin_norm(), _mk_fp_bin_pred(), _mk_fp_tern(), _mk_fp_unary(), _mk_fp_unary_pred(), fpAbs(), and fpNeg().
|
protected |
Definition at line 10921 of file z3py.py.
Referenced by Concat(), Contains(), IndexOf(), InRe(), LastIndexOf(), Length(), PrefixOf(), Range(), Re(), Replace(), StrToInt(), and SuffixOf().
|
protected |
Definition at line 497 of file z3py.py.
Referenced by _ctx_from_ast_args(), _pb_args_coeffs(), And(), AtLeast(), AtMost(), Distinct(), If(), Implies(), IsMember(), IsSubset(), Not(), Or(), Product(), SetAdd(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), Sum(), and Xor().
|
protected |
|
protected |
|
protected |
Definition at line 9382 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), and FPRef.__sub__().
|
protected |
Definition at line 9255 of file z3py.py.
Referenced by parse_smt2_file(), and parse_smt2_string().
|
protected |
Definition at line 9239 of file z3py.py.
Referenced by parse_smt2_file(), and parse_smt2_string().
|
protected |
Definition at line 144 of file z3py.py.
Referenced by FuncDeclRef.__call__(), Fixedpoint.add_rule(), And(), ArraySort(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), AtLeast(), AtMost(), Solver.check(), Optimize.check(), Concat(), CreateDatatypes(), Fixedpoint.declare_var(), Distinct(), FreshFunction(), Function(), Intersect(), Map(), Or(), Product(), PropagateFunction(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), RecAddDefinition(), RecFunction(), Fixedpoint.register_relation(), Select(), Fixedpoint.set_predicate_representation(), SetIntersect(), SetUnion(), substitute(), substitute_funs(), Sum(), Union(), Update(), and Fixedpoint.update_rule().
|
protected |
Definition at line 158 of file z3py.py.
Referenced by _pb_args_coeffs().
|
protected |
Definition at line 260 of file z3py.py.
Referenced by _coerce_char(), _coerce_seq(), _mk_fp_bin(), _mk_fp_bin_norm(), _mk_fp_bin_pred(), _mk_fp_tern(), _mk_fp_unary(), _mk_fp_unary_pred(), _pb_args_coeffs(), And(), BitVec(), BitVecs(), BitVecSort(), BitVecVal(), Bool(), Bools(), BoolSort(), BoolVal(), Cbrt(), CharSort(), CharVal(), DatatypeSort(), DeclareSort(), EnumSort(), FiniteDomainSort(), Float128(), Float16(), Float32(), Float64(), FloatDouble(), FloatHalf(), FloatQuadruple(), FloatSingle(), FP(), fpAbs(), fpBVToFP(), fpFP(), fpFPToFP(), fpNeg(), fpRealToFP(), FPs(), fpSignedToFP(), FPSort(), fpToFP(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), FPVal(), FreshBool(), FreshConst(), FreshInt(), FreshReal(), get_ctx(), If(), Implies(), Int(), Ints(), IntSort(), IntVal(), IntVector(), Model(), Not(), Or(), ParOr(), parse_smt2_file(), parse_smt2_string(), probe_description(), probes(), Real(), Reals(), RealSort(), RealVal(), RealVector(), ReSort(), RNA(), RNE(), RoundNearestTiesToAway(), RoundNearestTiesToEven(), RoundTowardNegative(), RoundTowardPositive(), RoundTowardZero(), RTN(), RTP(), RTZ(), SimpleSolver(), SolverFor(), Sqrt(), String(), Strings(), StringVal(), tactic_description(), tactics(), to_symbol(), and Xor().
|
protected |
Definition at line 10932 of file z3py.py.
Referenced by Contains(), IndexOf(), LastIndexOf(), PrefixOf(), Replace(), and SuffixOf().
|
protected |
|
protected |
Return `True` if one of the elements of the given collection is a Z3 probe.
Definition at line 1837 of file z3py.py.
|
protected |
Definition at line 2724 of file z3py.py.
Referenced by _to_expr_ref(), and is_algebraic_value().
|
protected |
Definition at line 68 of file z3py.py.
Referenced by ParamDescrsRef.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), _coerce_fp_expr_list(), _py2expr(), _reorder_pb_arg(), _to_float_str(), Optimize.add_soft(), SeqRef.at(), Extract(), IndexOf(), RatVal(), RepeatBitVec(), ParamsRef.set(), SignExt(), to_symbol(), and ZeroExt().
|
protected |
Definition at line 2720 of file z3py.py.
Referenced by _to_expr_ref(), is_bv_value(), is_finite_domain_value(), is_fp_value(), is_fprm_value(), is_int_value(), and is_rational_value().
|
protected |
Definition at line 1424 of file z3py.py.
Referenced by ArithRef.__add__(), ArithRef.__mul__(), ArithRef.__radd__(), ArithRef.__rmul__(), ArithRef.__rsub__(), and ArithRef.__sub__().
|
protected |
Definition at line 10219 of file z3py.py.
|
protected |
Definition at line 10228 of file z3py.py.
|
protected |
Definition at line 10236 of file z3py.py.
|
protected |
Definition at line 10244 of file z3py.py.
Referenced by fpFMA().
|
protected |
Definition at line 10202 of file z3py.py.
Referenced by fpRoundToIntegral(), and fpSqrt().
|
protected |
Definition at line 10211 of file z3py.py.
Referenced by fpIsInf(), fpIsNaN(), fpIsNegative(), fpIsNormal(), fpIsPositive(), fpIsSubnormal(), and fpIsZero().
|
protected |
Definition at line 2183 of file z3py.py.
|
protected |
Definition at line 8337 of file z3py.py.
Referenced by OrElse().
|
protected |
Definition at line 9028 of file z3py.py.
|
protected |
|
protected |
Definition at line 8742 of file z3py.py.
Referenced by _probe_and(), and _probe_or().
|
protected |
|
protected |
Version of function `prove` that renders HTML.
Definition at line 9219 of file z3py.py.
|
protected |
Definition at line 3119 of file z3py.py.
Referenced by _coerce_expr_list(), _coerce_exprs(), IntToStr(), IsMember(), K(), Solver.next(), Solver.root(), SetAdd(), SetDel(), SetHasSize(), StrFromCode(), StrToCode(), and ModelRef.update_value().
|
protected |
Definition at line 1219 of file z3py.py.
Referenced by _coerce_expr_list(), Product(), and Sum().
|
protected |
Definition at line 9021 of file z3py.py.
Referenced by _pb_args_coeffs().
|
protected |
Version of function `solve` that renders HTML output.
Definition at line 9170 of file z3py.py.
|
protected |
Version of function `solve_using` that renders HTML.
Definition at line 9194 of file z3py.py.
|
protected |
Sorts.
Definition at line 555 of file z3py.py.
Referenced by _to_sort_ref().
|
protected |
Convert a Z3 symbol back into a Python object.
Definition at line 132 of file z3py.py.
Referenced by ParamDescrsRef.get_name(), Fixedpoint.get_rule_names_along_trace(), SortRef.name(), and QuantifierRef.var_name().
|
protected |
Definition at line 523 of file z3py.py.
Referenced by ExprRef.__ne__(), _array_select(), _mk_quantifier(), _pb_args_coeffs(), And(), AtLeast(), AtMost(), Distinct(), Map(), MultiPattern(), Or(), Product(), UserPropagateBase.propagate(), SetIntersect(), SetUnion(), Sum(), Fixedpoint.to_string(), and Update().
|
protected |
Definition at line 539 of file z3py.py.
Referenced by AstRef.__deepcopy__(), AstVector.__getitem__(), AstMap.__getitem__(), and AstRef.translate().
|
protected |
Definition at line 1129 of file z3py.py.
Referenced by FuncDeclRef.__call__(), SeqRef.__ge__(), SeqRef.__getitem__(), SeqRef.__gt__(), SeqRef.__le__(), SeqRef.__lt__(), _array_select(), _to_ast_ref(), ExprRef.arg(), FuncEntry.arg_value(), QuantifierRef.body(), CharFromBv(), CharVal(), Const(), ArrayRef.default(), FuncInterp.else_value(), ModelRef.eval(), Ext(), FreshConst(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), If(), CharRef.is_digit(), OptimizeObjective.lower(), Solver.next(), QuantifierRef.no_pattern(), on_clause_eh(), Solver.proof(), Solver.root(), SetHasSize(), simplify(), substitute(), substitute_funs(), substitute_vars(), CharRef.to_bv(), CharRef.to_int(), Update(), OptimizeObjective.upper(), user_prop_created(), user_prop_decide(), user_prop_diseq(), user_prop_eq(), user_prop_fixed(), FuncEntry.value(), and Var().
|
protected |
Definition at line 9964 of file z3py.py.
Referenced by FPVal().
|
protected |
|
protected |
Definition at line 901 of file z3py.py.
Referenced by _to_ast_ref().
|
protected |
Definition at line 8313 of file z3py.py.
Referenced by Probe.__call__(), and Tactic.apply().
|
protected |
Definition at line 3168 of file z3py.py.
Referenced by _to_float_str(), BitVecVal(), FiniteDomainVal(), and IntVal().
|
protected |
Definition at line 168 of file z3py.py.
Referenced by Context.__init__(), and set_param().
|
protected |
Definition at line 1971 of file z3py.py.
Referenced by _mk_quantifier().
|
protected |
Definition at line 8696 of file z3py.py.
Referenced by Probe.__eq__(), Probe.__ge__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), _probe_nary(), Cond(), FailIf(), and When().
|
protected |
|
protected |
Definition at line 660 of file z3py.py.
Referenced by _sort(), _to_ast_ref(), FuncDeclRef.domain(), ArraySortRef.domain_n(), ModelRef.get_sort(), FuncDeclRef.range(), ArraySortRef.range(), and QuantifierRef.var_sort().
|
protected |
Definition at line 8322 of file z3py.py.
Referenced by _and_then(), _or_else(), Cond(), ParOr(), ParThen(), Repeat(), TryFor(), When(), With(), and WithParams().
|
protected |
Datatypes.
Return `True` if acc is pair of the form (String, Datatype or Sort).
Definition at line 5029 of file z3py.py.
Referenced by Datatype.declare_core().
|
protected |
Definition at line 105 of file z3py.py.
Referenced by Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), ParamDescrsRef.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), _and_then(), _check_bv_args(), _check_fp_args(), _coerce_expr_merge(), _ctx_from_ast_arg_list(), _dict2darray(), _dict2sarray(), _mk_bin(), _mk_fp_bin(), _mk_fp_bin_norm(), _mk_fp_bin_pred(), _mk_fp_tern(), _mk_fp_unary(), _mk_fp_unary_pred(), _mk_quantifier(), _or_else(), _pb_args_coeffs(), _probe_nary(), _prove_html(), _py2expr(), _solve_using_html(), _to_float_str(), _to_sort_ref(), _z3_check_cint_overflow(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), RatNumRef.as_long(), Solver.assert_and_track(), Optimize.assert_and_track(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), Concat(), Solver.consequences(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), Distinct(), EnumSort(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpBVToFP(), fpFP(), fpFPToFP(), fpInfinity(), fpMinusInfinity(), fpMinusZero(), fpNaN(), fpPlusInfinity(), fpPlusZero(), fpRealToFP(), fpSignedToFP(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), FPVal(), fpZero(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), Intersect(), IsInt(), K(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), OrElse(), ParOr(), ParThen(), QuantifierRef.pattern(), PropagateFunction(), prove(), Fixedpoint.query_from_lvl(), RatVal(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_default_rounding_mode(), set_param(), SignExt(), simplify(), solve_using(), substitute(), substitute_funs(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Union(), Update(), ParamsRef.validate(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().
|
protected |
Abs | ( | arg | ) |
AllChar | ( | regex_sort, | |
ctx = None |
|||
) |
Create a regular expression that accepts all single character strings
Definition at line 11346 of file z3py.py.
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 1845 of file z3py.py.
Referenced by Tactic.__call__(), Fixedpoint.add_rule(), And(), AndThen(), Tactic.apply(), Goal.as_expr(), ApplyResult.as_expr(), Bool(), Bools(), BoolVector(), Distinct(), is_and(), is_bool(), is_implies(), is_or(), Lambda(), ParThen(), prove(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Repeat(), simplify(), Then(), and Fixedpoint.update_rule().
AndThen | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` in sequence. >>> x, y = Ints('x y') >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) >>> t(And(x == 0, y > x + 1)) [[Not(y <= 1)]] >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1)
Definition at line 8345 of file z3py.py.
append_log | ( | s | ) |
Append user-defined string to interaction log.
Definition at line 119 of file z3py.py.
args2params | ( | arguments, | |
keywords, | |||
ctx = None |
|||
) |
Convert python arguments into a Z3_params object. A ':' is added to the keywords, and '_' is replaced with '-' >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) (params model true relevancy 2 elim_and true)
Definition at line 5458 of file z3py.py.
Referenced by Tactic.apply(), args2params(), Solver.set(), Fixedpoint.set(), Optimize.set(), simplify(), Simplifier.using_params(), and With().
Array | ( | name, | |
* | sorts | ||
) |
Return an array constant named `name` with the given domain and range sorts. >>> a = Array('a', IntSort(), IntSort()) >>> a.sort() Array(Int, Int) >>> a[0] a[0]
Definition at line 4725 of file z3py.py.
Referenced by ArrayRef.__getitem__(), Array(), ArraySort(), ArrayRef.domain(), get_map_func(), is_array(), is_const_array(), is_K(), is_map(), is_select(), is_store(), K(), Lambda(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), ExprRef.sort_kind(), Store(), and Update().
ArraySort | ( | * | sig | ) |
Return the Z3 array sort with the given domain and range sorts. >>> A = ArraySort(IntSort(), BoolSort()) >>> A Array(Int, Bool) >>> A.domain() Int >>> A.range() Bool >>> AA = ArraySort(IntSort(), A) >>> AA Array(Int, Array(Int, Bool))
Definition at line 4692 of file z3py.py.
Referenced by Array(), ArraySort(), ArraySortRef.domain(), SortRef.kind(), SortRef.name(), ArraySortRef.range(), and SetSort().
AtLeast | ( | * | args | ) |
Create an at-most Pseudo-Boolean k constraint. >>> a, b, c = Bools('a b c') >>> f = AtLeast(a, b, c, 2)
Definition at line 9003 of file z3py.py.
Referenced by AtLeast().
AtMost | ( | * | args | ) |
Create an at-most Pseudo-Boolean k constraint. >>> a, b, c = Bools('a b c') >>> f = AtMost(a, b, c, 2)
Definition at line 8985 of file z3py.py.
Referenced by AtMost().
BitVec | ( | name, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. If `ctx=None`, then the global context is used. >>> x = BitVec('x', 16) >>> is_bv(x) True >>> x.size() 16 >>> x.sort() BitVec(16) >>> word = BitVecSort(16) >>> x2 = BitVec('x', word) >>> eq(x, x2) True
Definition at line 4029 of file z3py.py.
Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__invert__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__neg__(), BitVecRef.__or__(), BitVecRef.__pos__(), BitVecRef.__radd__(), BitVecRef.__rand__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), BitVecRef.__rrshift__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BitVec(), BitVecs(), BitVecSort(), BV2Int(), Extract(), is_bv(), is_bv_value(), RepeatBitVec(), SignExt(), BitVecRef.size(), BitVecRef.sort(), SRem(), UDiv(), URem(), and ZeroExt().
BitVecs | ( | names, | |
bv, | |||
ctx = None |
|||
) |
Return a tuple of bit-vector constants of size bv. >>> x, y, z = BitVecs('x y z', 16) >>> x.size() 16 >>> x.sort() BitVec(16) >>> Sum(x, y, z) 0 + x + y + z >>> Product(x, y, z) 1*x*y*z >>> simplify(Product(x, y, z)) x*y*z
Definition at line 4053 of file z3py.py.
Referenced by BitVecRef.__ge__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__rshift__(), BitVecs(), LShR(), RotateLeft(), RotateRight(), UGE(), UGT(), ULE(), and ULT().
BitVecSort | ( | sz, | |
ctx = None |
|||
) |
Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. >>> Byte = BitVecSort(8) >>> Word = BitVecSort(16) >>> Byte BitVec(8) >>> x = Const('x', Byte) >>> eq(x, BitVec('x', 8)) True
Definition at line 3997 of file z3py.py.
Referenced by BitVec(), BitVecSort(), BitVecVal(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), BitVecSortRef.size(), and BitVecRef.sort().
BitVecVal | ( | val, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. >>> v = BitVecVal(10, 32) >>> v 10 >>> print("0x%.8x" % v.as_long()) 0x0000000a
Definition at line 4012 of file z3py.py.
Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), BitVecVal(), Concat(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().
Bool | ( | name, | |
ctx = None |
|||
) |
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used. >>> p = Bool('p') >>> q = Bool('q') >>> And(p, q) And(p, q)
Definition at line 1724 of file z3py.py.
Referenced by SortRef.__eq__(), SortRef.__ne__(), Fixedpoint.add_rule(), Solver.assert_and_track(), Optimize.assert_and_track(), Bool(), Bools(), BoolVector(), is_bool(), is_false(), is_not(), is_true(), and Not().
Bools | ( | names, | |
ctx = None |
|||
) |
Return a tuple of Boolean constants. `names` is a single string containing all names separated by blank spaces. If `ctx=None`, then the global context is used. >>> p, q, r = Bools('p q r') >>> And(p, Or(q, r)) And(p, Or(q, r))
Definition at line 1736 of file z3py.py.
Referenced by And(), AtLeast(), AtMost(), Bools(), Solver.consequences(), Implies(), is_and(), is_implies(), is_or(), Or(), PbEq(), PbGe(), PbLe(), prove(), Solver.unsat_core(), and Xor().
BoolSort | ( | ctx = None | ) |
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. >>> BoolSort() Bool >>> p = Const('p', BoolSort()) >>> is_bool(p) True >>> r = Function('r', IntSort(), IntSort(), BoolSort()) >>> r(0, 1) r(0, 1) >>> is_bool(r(0, 1)) True
Definition at line 1687 of file z3py.py.
Referenced by FuncDeclRef.__call__(), SortRef.__eq__(), ArrayRef.__getitem__(), SortRef.__ne__(), FuncDeclRef.arity(), ArraySort(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), BoolSort(), BoolSortRef.cast(), Solver.check(), ArraySortRef.domain(), ArrayRef.domain(), FuncDeclRef.domain(), FreshBool(), If(), Implies(), IntSort(), is_arith_sort(), is_ast(), SortRef.kind(), SortRef.name(), Not(), FuncDeclRef.range(), ArraySortRef.range(), ArrayRef.range(), SetSort(), ArrayRef.sort(), Var(), and Xor().
BoolVal | ( | val, | |
ctx = None |
|||
) |
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. >>> BoolVal(True) True >>> is_true(BoolVal(True)) True >>> is_true(True) False >>> is_false(BoolVal(False)) True
Definition at line 1705 of file z3py.py.
Referenced by _mk_quantifier(), _py2expr(), Goal.as_expr(), ApplyResult.as_expr(), BoolVal(), UserPropagateBase.conflict(), is_false(), Re(), and Solver.to_smt2().
BoolVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of Boolean constants of size `sz`. The constants are named using the given prefix. If `ctx=None`, then the global context is used. >>> P = BoolVector('p', 3) >>> P [p__0, p__1, p__2] >>> And(P) And(p__0, p__1, p__2)
Definition at line 1752 of file z3py.py.
Referenced by And(), BoolVector(), and Or().
BV2Int | ( | a, | |
is_signed = False |
|||
) |
Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) >>> BV2Int(b).sort() Int >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) >>> x > BV2Int(b, is_signed=False) x > BV2Int(b) >>> x > BV2Int(b, is_signed=True) x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) >>> solve(x > BV2Int(b), b == 1, x < 3) [x = 2, b = 1]
Definition at line 3965 of file z3py.py.
Referenced by BV2Int().
BVAddNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector addition does not overflow
Definition at line 4451 of file z3py.py.
BVAddNoUnderflow | ( | a, | |
b | |||
) |
A predicate the determines that signed bit-vector addition does not underflow
Definition at line 4458 of file z3py.py.
BVMulNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector multiplication does not overflow
Definition at line 4493 of file z3py.py.
BVMulNoUnderflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector signed multiplication does not underflow
Definition at line 4500 of file z3py.py.
BVRedAnd | ( | a | ) |
Return the reduction-and expression of `a`.
Definition at line 4437 of file z3py.py.
BVRedOr | ( | a | ) |
Return the reduction-or expression of `a`.
Definition at line 4444 of file z3py.py.
BVSDivNoOverflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector signed division does not overflow
Definition at line 4479 of file z3py.py.
BVSNegNoOverflow | ( | a | ) |
A predicate the determines that bit-vector unary negation does not overflow
Definition at line 4486 of file z3py.py.
BVSubNoOverflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4465 of file z3py.py.
BVSubNoUnderflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector subtraction does not underflow
Definition at line 4472 of file z3py.py.
Cbrt | ( | a, | |
ctx = None |
|||
) |
Return a Z3 expression which represents the cubic root of a. >>> x = Real('x') >>> Cbrt(x) x**(1/3)
Definition at line 3416 of file z3py.py.
Referenced by Cbrt().
CharFromBv | ( | ch, | |
ctx = None |
|||
) |
CharIsDigit | ( | ch, | |
ctx = None |
|||
) |
CharSort | ( | ctx = None | ) |
Create a character sort >>> ch = CharSort() >>> print(ch) Char
Definition at line 10803 of file z3py.py.
Referenced by CharSort().
CharToBv | ( | ch, | |
ctx = None |
|||
) |
CharToInt | ( | ch, | |
ctx = None |
|||
) |
CharVal | ( | ch, | |
ctx = None |
|||
) |
Definition at line 10896 of file z3py.py.
Referenced by _coerce_char().
Complement | ( | re | ) |
Concat | ( | * | args | ) |
Create a Z3 bit-vector concatenation expression. >>> v = BitVecVal(1, 4) >>> Concat(v, v+1, v) Concat(Concat(1, 1 + 1), 1) >>> simplify(Concat(v, v+1, v)) 289 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 121
Definition at line 4074 of file z3py.py.
Referenced by SeqRef.__add__(), SeqRef.__radd__(), Concat(), Contains(), and BitVecRef.size().
Cond | ( | p, | |
t1, | |||
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
Definition at line 8802 of file z3py.py.
Const | ( | name, | |
sort | |||
) |
Create a constant of the given sort. >>> Const('x', IntSort()) x
Definition at line 1433 of file z3py.py.
Referenced by BitVecSort(), BoolSort(), Const(), Consts(), DeclareSort(), FPSort(), IntSort(), is_finite_domain(), is_finite_domain_value(), IsMember(), IsSubset(), RealSort(), DatatypeSortRef.recognizer(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().
Consts | ( | names, | |
sort | |||
) |
Create several constants of the given sort. `names` is a string containing the names of all constants to be created. Blank spaces separate the names of different constants. >>> x, y, z = Consts('x y z', IntSort()) >>> x + y + z x + y + z
Definition at line 1445 of file z3py.py.
Referenced by Consts(), Ext(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
Contains | ( | a, | |
b | |||
) |
Check if 'a' contains 'b' >>> s1 = Contains("abc", "ab") >>> simplify(s1) True >>> s2 = Contains("abc", "bc") >>> simplify(s2) True >>> x, y, z = Strings('x y z') >>> s3 = Contains(Concat(x,y,z), y) >>> simplify(s3) True
Definition at line 11073 of file z3py.py.
Referenced by Contains().
CreateDatatypes | ( | * | ds | ) |
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. In the following example we define a Tree-List using two mutually recursive datatypes. >>> TreeList = Datatype('TreeList') >>> Tree = Datatype('Tree') >>> # Tree has two constructors: leaf and node >>> Tree.declare('leaf', ('val', IntSort())) >>> # a node contains a list of trees >>> Tree.declare('node', ('children', TreeList)) >>> TreeList.declare('nil') >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) >>> Tree.val(Tree.leaf(10)) val(leaf(10)) >>> simplify(Tree.val(Tree.leaf(10))) 10 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) >>> n1 node(cons(leaf(10), cons(leaf(20), nil))) >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) >>> simplify(n2 == n1) False >>> simplify(TreeList.car(Tree.children(n2)) == n1) True
Definition at line 5150 of file z3py.py.
Referenced by Datatype.create(), and CreateDatatypes().
DatatypeSort | ( | name, | |
ctx = None |
|||
) |
Create a reference to a sort that was declared, or will be declared, as a recursive datatype
Definition at line 5350 of file z3py.py.
DeclareSort | ( | name, | |
ctx = None |
|||
) |
Create a new uninterpreted sort named `name`. If `ctx=None`, then the new sort is declared in the global Z3Py context. >>> A = DeclareSort('A') >>> a = Const('a', A) >>> b = Const('b', A) >>> a.sort() == A True >>> b.sort() == A True >>> a == b a == b
Definition at line 693 of file z3py.py.
Referenced by DeclareSort(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
Default | ( | a | ) |
Return a default value for array expression. >>> b = K(IntSort(), 1) >>> prove(Default(b) == 1) proved
Definition at line 4771 of file z3py.py.
Referenced by Default(), and is_default().
describe_probes | ( | ) |
Display a (tabular) description of all available probes in Z3.
Definition at line 8723 of file z3py.py.
describe_tactics | ( | ) |
Display a (tabular) description of all available tactics in Z3.
Definition at line 8517 of file z3py.py.
deserialize | ( | st | ) |
inverse function to the serialize method on ExprRef. It is made available to make it easier for users to serialize expressions back and forth between strings. Solvers can be serialized using the 'sexpr()' method.
Definition at line 1115 of file z3py.py.
Diff | ( | a, | |
b, | |||
ctx = None |
|||
) |
disable_trace | ( | msg | ) |
Definition at line 79 of file z3py.py.
DisjointSum | ( | name, | |
sorts, | |||
ctx = None |
|||
) |
Create a named tagged union sort base on a set of underlying sorts Example: >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
Definition at line 5367 of file z3py.py.
Referenced by DisjointSum().
Distinct | ( | * | args | ) |
Create a Z3 distinct expression. >>> x = Int('x') >>> y = Int('y') >>> Distinct(x, y) x != y >>> z = Int('z') >>> Distinct(x, y, z) Distinct(x, y, z) >>> simplify(Distinct(x, y, z)) Distinct(x, y, z) >>> simplify(Distinct(x, y, z), blast_distinct=True) And(Not(x == y), Not(x == z), Not(y == z))
Definition at line 1400 of file z3py.py.
Referenced by Distinct(), is_distinct(), and simplify().
Empty | ( | s | ) |
Create the empty sequence of the given sort >>> e = Empty(StringSort()) >>> e2 = StringVal("") >>> print(e.eq(e2)) True >>> e3 = Empty(SeqSort(IntSort())) >>> print(e3) Empty(Seq(Int)) >>> e4 = Empty(ReSort(SeqSort(IntSort()))) >>> print(e4) Empty(ReSort(Seq(Int)))
Definition at line 11003 of file z3py.py.
Referenced by Empty().
EmptySet | ( | s | ) |
Create the empty set >>> EmptySet(IntSort()) K(Int, False)
Definition at line 4914 of file z3py.py.
Referenced by EmptySet().
enable_trace | ( | msg | ) |
Definition at line 75 of file z3py.py.
ensure_prop_closures | ( | ) |
Definition at line 11456 of file z3py.py.
Referenced by UserPropagateBase.__init__().
EnumSort | ( | name, | |
values, | |||
ctx = None |
|||
) |
Return a new enumeration sort named `name` containing the given values. The result is a pair (sort, list of constants). Example: >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
Definition at line 5379 of file z3py.py.
Referenced by EnumSort().
eq | ( | a, | |
b | |||
) |
Return `True` if `a` and `b` are structurally identical AST nodes. >>> x = Int('x') >>> y = Int('y') >>> eq(x, y) False >>> eq(x + 1, x + 1) True >>> eq(x + 1, 1 + x) False >>> eq(simplify(x + 1), simplify(1 + x)) True
Definition at line 472 of file z3py.py.
Referenced by BitVec(), BitVecSort(), eq(), FP(), FPSort(), FreshBool(), FreshInt(), FreshReal(), get_map_func(), main_ctx(), Select(), substitute(), and Var().
Exists | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 exists formula. The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> q = Exists([x, y], f(x, y) >= x, skid="foo") >>> q Exists([x, y], f(x, y) >= x) >>> is_quantifier(q) True >>> r = Tactic('nnf')(q).as_expr() >>> is_quantifier(r) False
Definition at line 2236 of file z3py.py.
Referenced by Fixedpoint.abstract(), Exists(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), and QuantifierRef.is_lambda().
Ext | ( | a, | |
b | |||
) |
Return extensionality index for one-dimensional arrays. >> a, b = Consts('a b', SetSort(IntSort())) >> Ext(a, b) Ext(a, b)
Definition at line 4860 of file z3py.py.
Referenced by Ext().
Extract | ( | high, | |
low, | |||
a | |||
) |
Create a Z3 bit-vector extraction expression. Extract is overloaded to also work on sequence extraction. The functions SubString and SubSeq are redirected to Extract. For this case, the arguments are reinterpreted as: high - is a sequence (string) low - is an offset a - is the length to be extracted >>> x = BitVec('x', 8) >>> Extract(6, 2, x) Extract(6, 2, x) >>> Extract(6, 2, x).sort() BitVec(5) >>> simplify(Extract(StringVal("abcd"),2,1)) "c"
Definition at line 4120 of file z3py.py.
Referenced by Extract(), SubSeq(), and SubString().
FailIf | ( | p, | |
ctx = None |
|||
) |
Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 8760 of file z3py.py.
Referenced by FailIf().
FiniteDomainSort | ( | name, | |
sz, | |||
ctx = None |
|||
) |
Create a named finite domain sort of a given size sz
Definition at line 7708 of file z3py.py.
Referenced by FiniteDomainNumRef.as_long(), FiniteDomainNumRef.as_string(), FiniteDomainVal(), is_finite_domain(), is_finite_domain_sort(), and is_finite_domain_value().
FiniteDomainVal | ( | val, | |
sort, | |||
ctx = None |
|||
) |
Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. >>> s = FiniteDomainSort('S', 256) >>> FiniteDomainVal(255, s) 255 >>> FiniteDomainVal('100', s) 100
Definition at line 7778 of file z3py.py.
Referenced by FiniteDomainNumRef.as_long(), FiniteDomainNumRef.as_string(), FiniteDomainVal(), and is_finite_domain_value().
Float128 | ( | ctx = None | ) |
Floating-point 128-bit (quadruple) sort.
Definition at line 9488 of file z3py.py.
Float16 | ( | ctx = None | ) |
Float32 | ( | ctx = None | ) |
Floating-point 32-bit (single) sort.
Definition at line 9464 of file z3py.py.
Referenced by FPRef.__neg__(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), and fpUnsignedToFP().
Float64 | ( | ctx = None | ) |
Floating-point 64-bit (double) sort.
Definition at line 9476 of file z3py.py.
Referenced by fpFPToFP(), and fpToFP().
FloatDouble | ( | ctx = None | ) |
FloatHalf | ( | ctx = None | ) |
FloatQuadruple | ( | ctx = None | ) |
Floating-point 128-bit (quadruple) sort.
Definition at line 9494 of file z3py.py.
FloatSingle | ( | ctx = None | ) |
ForAll | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 forall formula. The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> ForAll([x, y], f(x, y) >= x) ForAll([x, y], f(x, y) >= x) >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ]) ForAll([x, y], f(x, y) >= x) >>> ForAll([x, y], f(x, y) >= x, weight=10) ForAll([x, y], f(x, y) >= x)
Definition at line 2218 of file z3py.py.
Referenced by Fixedpoint.abstract(), QuantifierRef.body(), QuantifierRef.children(), ForAll(), get_var_index(), is_app(), is_const(), QuantifierRef.is_exists(), is_expr(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), is_var(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
FP | ( | name, | |
fpsort, | |||
ctx = None |
|||
) |
Return a floating-point constant named `name`. `fpsort` is the floating-point sort. If `ctx=None`, then the global context is used. >>> x = FP('x', FPSort(8, 24)) >>> is_fp(x) True >>> x.ebits() 8 >>> x.sort() FPSort(8, 24) >>> word = FPSort(8, 24) >>> x2 = FP('x', word) >>> eq(x, x2) True
Definition at line 10120 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__neg__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FP(), fpAdd(), fpDiv(), fpIsInf(), fpIsNaN(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), FPs(), FPSort(), fpSub(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and FPRef.sort().
fpAbs | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point absolute value expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FPVal(1.0, s) >>> fpAbs(x) fpAbs(1) >>> y = FPVal(-20.0, s) >>> y -1.25*(2**4) >>> fpAbs(y) fpAbs(-1.25*(2**4)) >>> fpAbs(-1.25*(2**4)) fpAbs(-1.25*(2**4)) >>> fpAbs(x).sort() FPSort(8, 24)
Definition at line 10163 of file z3py.py.
Referenced by fpAbs().
fpAdd | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point addition expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpAdd(rm, x, y) x + y >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ fpAdd(RTZ(), x, y) >>> fpAdd(rm, x, y).sort() FPSort(8, 24)
Definition at line 10254 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__radd__(), fpAdd(), and FPs().
fpBVToFP | ( | v, | |
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a bit-vector term to a floating-point term. >>> x_bv = BitVecVal(0x3F800000, 32) >>> x_fp = fpBVToFP(x_bv, Float32()) >>> x_fp fpToFP(1065353216) >>> simplify(x_fp) 1
Definition at line 10576 of file z3py.py.
Referenced by fpBVToFP().
fpDiv | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point division expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpDiv(rm, x, y) x / y >>> fpDiv(rm, x, y).sort() FPSort(8, 24)
Definition at line 10301 of file z3py.py.
Referenced by FPRef.__div__(), FPRef.__rdiv__(), and fpDiv().
fpEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `fpEQ(other, self)`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpEQ(x, y) fpEQ(x, y) >>> fpEQ(x, y).sexpr() '(fp.eq x y)'
Definition at line 10484 of file z3py.py.
fpFMA | ( | rm, | |
a, | |||
b, | |||
c, | |||
ctx = None |
|||
) |
fpFP | ( | sgn, | |
exp, | |||
sig, | |||
ctx = None |
|||
) |
Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. >>> s = FPSort(8, 24) >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) >>> print(x) fpFP(1, 127, 4194304) >>> xv = FPVal(-1.5, s) >>> print(xv) -1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() sat >>> xv = FPVal(+1.5, s) >>> print(xv) 1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() unsat
Definition at line 10508 of file z3py.py.
Referenced by fpFP().
fpFPToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a floating-point term to a floating-point term of different precision. >>> x_sgl = FPVal(1.0, Float32()) >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) >>> x_dbl fpToFP(RNE(), 1) >>> simplify(x_dbl) 1 >>> x_dbl.sort() FPSort(11, 53)
Definition at line 10593 of file z3py.py.
Referenced by fpFPToFP().
fpGEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other >= self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGEQ(x, y) x >= y >>> (x >= y).sexpr() '(fp.geq x y)'
Definition at line 10472 of file z3py.py.
Referenced by FPRef.__ge__(), and fpGEQ().
fpGT | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other > self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGT(x, y) x > y >>> (x > y).sexpr() '(fp.gt x y)'
Definition at line 10460 of file z3py.py.
Referenced by FPRef.__gt__(), and fpGT().
fpInfinity | ( | s, | |
negative | |||
) |
Create a Z3 floating-point +oo or -oo term.
Definition at line 10048 of file z3py.py.
fpIsInf | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point isInfinite expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> fpIsInf(x) fpIsInf(x)
Definition at line 10390 of file z3py.py.
Referenced by fpIsInf().
fpIsNaN | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point isNaN expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> y = FP('y', s) >>> fpIsNaN(x) fpIsNaN(x)
Definition at line 10378 of file z3py.py.
Referenced by fpIsNaN().
fpIsNegative | ( | a, | |
ctx = None |
|||
) |
fpIsNormal | ( | a, | |
ctx = None |
|||
) |
fpIsPositive | ( | a, | |
ctx = None |
|||
) |
fpIsSubnormal | ( | a, | |
ctx = None |
|||
) |
fpIsZero | ( | a, | |
ctx = None |
|||
) |
fpLEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other <= self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLEQ(x, y) x <= y >>> (x <= y).sexpr() '(fp.leq x y)'
Definition at line 10448 of file z3py.py.
Referenced by FPRef.__le__(), and fpLEQ().
fpLT | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other < self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLT(x, y) x < y >>> (x < y).sexpr() '(fp.lt x y)'
Definition at line 10436 of file z3py.py.
Referenced by FPRef.__lt__(), and fpLT().
fpMax | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point maximum expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMax(x, y) fpMax(x, y) >>> fpMax(x, y).sort() FPSort(8, 24)
Definition at line 10345 of file z3py.py.
Referenced by fpMax().
fpMin | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point minimum expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMin(x, y) fpMin(x, y) >>> fpMin(x, y).sort() FPSort(8, 24)
Definition at line 10330 of file z3py.py.
Referenced by fpMin().
fpMinusInfinity | ( | s | ) |
fpMinusZero | ( | s | ) |
Create a Z3 floating-point -0.0 term.
Definition at line 10061 of file z3py.py.
Referenced by FPVal().
fpMul | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point multiplication expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMul(rm, x, y) x * y >>> fpMul(rm, x, y).sort() FPSort(8, 24)
Definition at line 10286 of file z3py.py.
Referenced by FPRef.__mul__(), FPRef.__rmul__(), fpMul(), and FPs().
fpNaN | ( | s | ) |
Create a Z3 floating-point NaN term. >>> s = FPSort(8, 24) >>> set_fpa_pretty(True) >>> fpNaN(s) NaN >>> pb = get_fpa_pretty() >>> set_fpa_pretty(False) >>> fpNaN(s) fpNaN(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 10008 of file z3py.py.
fpNeg | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point addition expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> fpNeg(x) -x >>> fpNeg(x).sort() FPSort(8, 24)
Definition at line 10186 of file z3py.py.
Referenced by FPRef.__neg__(), and fpNeg().
fpNEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `Not(fpEQ(other, self))`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpNEQ(x, y) Not(fpEQ(x, y)) >>> (x != y).sexpr() '(distinct x y)'
Definition at line 10496 of file z3py.py.
Referenced by fpNEQ().
fpPlusInfinity | ( | s | ) |
Create a Z3 floating-point +oo term. >>> s = FPSort(8, 24) >>> pb = get_fpa_pretty() >>> set_fpa_pretty(True) >>> fpPlusInfinity(s) +oo >>> set_fpa_pretty(False) >>> fpPlusInfinity(s) fpPlusInfinity(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 10025 of file z3py.py.
Referenced by fpPlusInfinity(), and FPVal().
fpPlusZero | ( | s | ) |
fpRealToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a real term to a floating-point term. >>> x_r = RealVal(1.5) >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) >>> x_fp fpToFP(RNE(), 3/2) >>> simplify(x_fp) 1.5
Definition at line 10613 of file z3py.py.
Referenced by fpRealToFP().
fpRem | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point remainder expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> y = FP('y', s) >>> fpRem(x, y) fpRem(x, y) >>> fpRem(x, y).sort() FPSort(8, 24)
Definition at line 10316 of file z3py.py.
Referenced by FPRef.__mod__(), FPRef.__rmod__(), and fpRem().
fpRoundToIntegral | ( | rm, | |
a, | |||
ctx = None |
|||
) |
FPs | ( | names, | |
fpsort, | |||
ctx = None |
|||
) |
Return an array of floating-point constants. >>> x, y, z = FPs('x y z', FPSort(8, 24)) >>> x.sort() FPSort(8, 24) >>> x.sbits() 24 >>> x.ebits() 8 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) x + y * z
Definition at line 10144 of file z3py.py.
Referenced by fpEQ(), fpGEQ(), fpGT(), fpLEQ(), fpLT(), fpNEQ(), and FPs().
fpSignedToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a signed bit-vector term (encoding an integer) to a floating-point term. >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) >>> x_fp fpToFP(RNE(), 4294967291) >>> simplify(x_fp) -1.25*(2**2)
Definition at line 10631 of file z3py.py.
Referenced by fpSignedToFP().
FPSort | ( | ebits, | |
sbits, | |||
ctx = None |
|||
) |
Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used. >>> Single = FPSort(8, 24) >>> Double = FPSort(11, 53) >>> Single FPSort(8, 24) >>> x = Const('x', Single) >>> eq(x, FP('x', FPSort(8, 24))) True
Definition at line 9949 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FPSortRef.cast(), FPSortRef.ebits(), FPRef.ebits(), FPNumRef.exponent(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpFP(), fpFPToFP(), fpGEQ(), fpGT(), fpIsInf(), fpIsNaN(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNaN(), fpNeg(), fpNEQ(), fpPlusInfinity(), fpRem(), FPs(), FPSort(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), get_default_fp_sort(), is_fp(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.significand(), FPNumRef.significand_as_bv(), and FPRef.sort().
fpSqrt | ( | rm, | |
a, | |||
ctx = None |
|||
) |
fpSub | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point subtraction expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpSub(rm, x, y) x - y >>> fpSub(rm, x, y).sort() FPSort(8, 24)
Definition at line 10271 of file z3py.py.
Referenced by FPRef.__rsub__(), FPRef.__sub__(), and fpSub().
fpToFP | ( | a1, | |
a2 = None , |
|||
a3 = None , |
|||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression from other term sorts to floating-point. From a bit-vector term in IEEE 754-2008 format: >>> x = FPVal(1.0, Float32()) >>> x_bv = fpToIEEEBV(x) >>> simplify(fpToFP(x_bv, Float32())) 1 From a floating-point term with different precision: >>> x = FPVal(1.0, Float32()) >>> x_db = fpToFP(RNE(), x, Float64()) >>> x_db.sort() FPSort(11, 53) From a real term: >>> x_r = RealVal(1.5) >>> simplify(fpToFP(RNE(), x_r, Float32())) 1.5 From a signed bit-vector term: >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> simplify(fpToFP(RNE(), x_signed, Float32())) -1.25*(2**2)
Definition at line 10537 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), and fpToFP().
fpToFPUnsigned | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.
Definition at line 10667 of file z3py.py.
Referenced by fpUnsignedToFP().
fpToIEEEBV | ( | x, | |
ctx = None |
|||
) |
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToIEEEBV(x) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10741 of file z3py.py.
Referenced by fpToFP(), and fpToIEEEBV().
fpToReal | ( | x, | |
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to real. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToReal(x) >>> print(is_fp(x)) True >>> print(is_real(y)) True >>> print(is_fp(y)) False >>> print(is_real(x)) False
Definition at line 10721 of file z3py.py.
Referenced by fpToReal().
fpToSBV | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToSBV(RTZ(), x, BitVecSort(32)) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10677 of file z3py.py.
Referenced by fpToSBV().
fpToUBV | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToUBV(RTZ(), x, BitVecSort(32)) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10699 of file z3py.py.
Referenced by fpToUBV().
fpUnsignedToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term. >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32()) >>> x_fp fpToFPUnsigned(RNE(), 4294967291) >>> simplify(x_fp) 1*(2**32)
Definition at line 10649 of file z3py.py.
Referenced by fpUnsignedToFP().
FPVal | ( | sig, | |
exp = None , |
|||
fps = None , |
|||
ctx = None |
|||
) |
Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used. >>> v = FPVal(20.0, FPSort(8, 24)) >>> v 1.25*(2**4) >>> print("0x%.8x" % v.exponent_as_long(False)) 0x00000004 >>> v = FPVal(2.25, FPSort(8, 24)) >>> v 1.125*(2**1) >>> v = FPVal(-2.25, FPSort(8, 24)) >>> v -1.125*(2**1) >>> FPVal(-0.0, FPSort(8, 24)) -0.0 >>> FPVal(0.0, FPSort(8, 24)) +0.0 >>> FPVal(+0.0, FPSort(8, 24)) +0.0
Definition at line 10074 of file z3py.py.
Referenced by _coerce_fp_expr_list(), FPNumRef.exponent(), fpAbs(), fpFP(), fpFPToFP(), fpToFP(), FPVal(), is_expr(), is_fp_value(), FPNumRef.isNegative(), FPNumRef.significand(), and FPNumRef.significand_as_bv().
fpZero | ( | s, | |
negative | |||
) |
Create a Z3 floating-point +0.0 or -0.0 term.
Definition at line 10067 of file z3py.py.
FreshBool | ( | prefix = "b" , |
|
ctx = None |
|||
) |
Return a fresh Boolean constant in the given context using the given prefix. If `ctx=None`, then the global context is used. >>> b1 = FreshBool() >>> b2 = FreshBool() >>> eq(b1, b2) False
Definition at line 1767 of file z3py.py.
Referenced by FreshBool().
FreshConst | ( | sort, | |
prefix = "c" |
|||
) |
FreshFunction | ( | * | sig | ) |
Create a new fresh Z3 uninterpreted function with the given sorts.
Definition at line 882 of file z3py.py.
FreshInt | ( | prefix = "x" , |
|
ctx = None |
|||
) |
Return a fresh integer constant in the given context using the given prefix. >>> x = FreshInt() >>> y = FreshInt() >>> eq(x, y) False >>> x.sort() Int
Definition at line 3279 of file z3py.py.
Referenced by FreshInt().
FreshReal | ( | prefix = "b" , |
|
ctx = None |
|||
) |
Return a fresh real constant in the given context using the given prefix. >>> x = FreshReal() >>> y = FreshReal() >>> eq(x, y) False >>> x.sort() Real
Definition at line 3336 of file z3py.py.
Referenced by FreshReal().
Full | ( | s | ) |
Create the regular expression that accepts the universal language >>> e = Full(ReSort(SeqSort(IntSort()))) >>> print(e) Full(ReSort(Seq(Int))) >>> e1 = Full(ReSort(StringSort())) >>> print(e1) Full(ReSort(String))
Definition at line 11023 of file z3py.py.
Referenced by Full().
FullSet | ( | s | ) |
Function | ( | name, | |
* | sig | ||
) |
Create a new Z3 uninterpreted function with the given sorts. >>> f = Function('f', IntSort(), IntSort()) >>> f(f(0)) f(f(0))
Definition at line 859 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ModelRef.__getitem__(), ModelRef.__len__(), ExprRef.arg(), FuncEntry.arg_value(), FuncDeclRef.arity(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), BoolSort(), ExprRef.children(), QuantifierRef.children(), ExprRef.decl(), ModelRef.decls(), FuncDeclRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), Function(), ModelRef.get_interp(), get_map_func(), get_var_index(), is_ast(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_func_decl(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_var(), Lambda(), Map(), MultiPattern(), FuncDeclRef.name(), ExprRef.num_args(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), parse_smt2_string(), QuantifierRef.pattern(), FuncDeclRef.range(), substitute(), substitute_vars(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
get_as_array_func | ( | n | ) |
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
Definition at line 6691 of file z3py.py.
Referenced by ModelRef.get_interp().
get_ctx | ( | ctx | ) |
get_default_fp_sort | ( | ctx = None | ) |
Definition at line 9371 of file z3py.py.
Referenced by _dflt_fps().
get_default_rounding_mode | ( | ctx = None | ) |
Retrieves the global default rounding mode.
Definition at line 9338 of file z3py.py.
Referenced by _dflt_rm().
get_full_version | ( | ) |
get_map_func | ( | a | ) |
Return the function declaration associated with a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort()) >>> b = Array('b', IntSort(), IntSort()) >>> a = Map(f, b) >>> eq(f, get_map_func(a)) True >>> get_map_func(a) f >>> get_map_func(a)(0) f(0)
Definition at line 4668 of file z3py.py.
Referenced by get_map_func().
get_param | ( | name | ) |
Return the value of a Z3 global (or module) parameter >>> get_param('nlsat.reorder') 'true'
Definition at line 307 of file z3py.py.
Referenced by get_param().
get_var_index | ( | a | ) |
Return the de-Bruijn index of the Z3 bounded variable `a`. >>> x = Int('x') >>> y = Int('y') >>> is_var(x) False >>> is_const(x) True >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> # Z3 replaces x and y with bound variables when ForAll is executed. >>> q = ForAll([x, y], f(x, y) == x + y) >>> q.body() f(Var(1), Var(0)) == Var(1) + Var(0) >>> b = q.body() >>> b.arg(0) f(Var(1), Var(0)) >>> v1 = b.arg(0).arg(0) >>> v2 = b.arg(0).arg(1) >>> v1 Var(1) >>> v2 Var(0) >>> get_var_index(v1) 1 >>> get_var_index(v2) 0
Definition at line 1331 of file z3py.py.
Referenced by get_var_index().
get_version | ( | ) |
Definition at line 92 of file z3py.py.
get_version_string | ( | ) |
Definition at line 83 of file z3py.py.
help_simplify | ( | ) |
Return a string describing all options available for Z3 `simplify` procedure.
Definition at line 8844 of file z3py.py.
If | ( | a, | |
b, | |||
c, | |||
ctx = None |
|||
) |
Create a Z3 if-then-else expression. >>> x = Int('x') >>> y = Int('y') >>> max = If(x > y, x, y) >>> max If(x > y, x, y) >>> simplify(max) If(x <= y, y, x)
Definition at line 1377 of file z3py.py.
Referenced by BoolRef.__mul__(), ArithRef.__mul__(), Abs(), BV2Int(), If(), Lambda(), and RecAddDefinition().
Implies | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 implies expression. >>> p, q = Bools('p q') >>> Implies(p, q) Implies(p, q)
Definition at line 1781 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Solver.consequences(), Implies(), is_implies(), Store(), Solver.unsat_core(), Update(), and Fixedpoint.update_rule().
IndexOf | ( | s, | |
substr, | |||
offset = None |
|||
) |
Retrieve the index of substring within a string starting at a specified offset. >>> simplify(IndexOf("abcabc", "bc", 0)) 1 >>> simplify(IndexOf("abcabc", "bc", 2)) 4
Definition at line 11107 of file z3py.py.
Referenced by IndexOf().
InRe | ( | s, | |
re | |||
) |
Create regular expression membership test >>> re = Union(Re("a"),Re("b")) >>> print (simplify(InRe("a", re))) True >>> print (simplify(InRe("b", re))) True >>> print (simplify(InRe("c", re))) False
Definition at line 11220 of file z3py.py.
Referenced by InRe(), Loop(), Option(), Plus(), Range(), Star(), and Union().
Int | ( | name, | |
ctx = None |
|||
) |
Return an integer constant named `name`. If `ctx=None`, then the global context is used. >>> x = Int('x') >>> is_int(x) True >>> is_int(x + 1) True
Definition at line 3240 of file z3py.py.
Referenced by ArithRef.__add__(), FuncDeclRef.__call__(), Probe.__call__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), Probe.__gt__(), Probe.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), Probe.__lt__(), ArithRef.__mod__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), ExprRef.arg(), Goal.as_expr(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), QuantifierRef.body(), BV2Int(), SortRef.cast(), Solver.check(), ExprRef.children(), QuantifierRef.children(), ExprRef.decl(), ModelRef.decls(), Distinct(), eq(), AstRef.eq(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), get_var_index(), AstRef.hash(), If(), Goal.insert(), Solver.insert(), Int(), Ints(), IntVector(), is_app(), is_app_of(), is_arith(), is_arith_sort(), is_ast(), is_bv(), is_const(), QuantifierRef.is_exists(), is_expr(), is_finite_domain(), QuantifierRef.is_forall(), is_fp(), is_int(), ArithSortRef.is_int(), ArithRef.is_int(), is_int_value(), QuantifierRef.is_lambda(), is_pattern(), is_probe(), is_quantifier(), is_real(), ArithSortRef.is_real(), is_select(), is_sort(), is_to_real(), is_var(), K(), AstMap.keys(), Statistics.keys(), FuncDeclRef.kind(), Solver.model(), MultiPattern(), ExprRef.num_args(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), OrElse(), ParOr(), QuantifierRef.pattern(), Solver.pop(), Solver.push(), AstVector.push(), Solver.reason_unknown(), RecAddDefinition(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), AstRef.sexpr(), Solver.sexpr(), SimpleSolver(), simplify(), Goal.simplify(), solve(), SolverFor(), ExprRef.sort(), ArithRef.sort(), Solver.statistics(), Store(), substitute(), substitute_vars(), ToReal(), AstVector.translate(), AstRef.translate(), Goal.translate(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
Int2BV | ( | a, | |
num_bits | |||
) |
Return the z3 expression Int2BV(a, num_bits). It is a bit-vector of width num_bits and represents the modulo of a by 2^num_bits
Definition at line 3988 of file z3py.py.
Intersect | ( | * | args | ) |
Create intersection of regular expressions. >>> re = Intersect(Re("a"), Re("b"), Re("c"))
Definition at line 11254 of file z3py.py.
Referenced by Intersect().
Ints | ( | names, | |
ctx = None |
|||
) |
Return a tuple of Integer constants. >>> x, y, z = Ints('x y z') >>> Sum(x, y, z) x + y + z
Definition at line 3253 of file z3py.py.
Referenced by Tactic.__call__(), ArithRef.__ge__(), Goal.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ApplyResult.__len__(), ArithRef.__lt__(), AndThen(), Tactic.apply(), Goal.convert_model(), Goal.depth(), FailIf(), Goal.get(), Goal.inconsistent(), Ints(), is_add(), is_distinct(), is_div(), is_eq(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Lambda(), parse_smt2_string(), ParThen(), Goal.prec(), Product(), Repeat(), Goal.size(), Store(), Sum(), Then(), Solver.unsat_core(), Update(), When(), With(), and WithParams().
IntSort | ( | ctx = None | ) |
Return the integer sort in the given context. If `ctx=None`, then the global context is used. >>> IntSort() Int >>> x = Const('x', IntSort()) >>> is_int(x) True >>> x.sort() == IntSort() True >>> x.sort() == BoolSort() False
Definition at line 3134 of file z3py.py.
Referenced by FuncDeclRef.__call__(), SortRef.__eq__(), ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), SortRef.__ne__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncDeclRef.arity(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), BoolSort(), ArithSortRef.cast(), ExprRef.children(), QuantifierRef.children(), Const(), DatatypeSortRef.constructor(), Consts(), Datatype.create(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), ModelRef.decls(), Default(), DisjointSum(), ArraySortRef.domain(), ArrayRef.domain(), FuncDeclRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), FreshInt(), Full(), FullSet(), Function(), ModelRef.get_interp(), get_map_func(), get_var_index(), Int(), IntSort(), IntVal(), is_app(), is_arith_sort(), is_array(), is_ast(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_exists(), is_expr(), is_finite_domain_sort(), QuantifierRef.is_forall(), is_func_decl(), is_K(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_select(), is_sort(), is_store(), SeqSortRef.is_string(), is_var(), IsMember(), IsSubset(), K(), SortRef.kind(), Lambda(), Map(), MultiPattern(), SortRef.name(), FuncDeclRef.name(), ExprRef.num_args(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), parse_smt2_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), ArrayRef.range(), RecAddDefinition(), DatatypeSortRef.recognizer(), Select(), SeqSort(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), ArrayRef.sort(), ExprRef.sort_kind(), Store(), SortRef.subsort(), substitute(), substitute_vars(), TupleSort(), Update(), FuncEntry.value(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
IntToStr | ( | s | ) |
Convert integer expression to string
Definition at line 11162 of file z3py.py.
Referenced by StrToInt().
IntVal | ( | val, | |
ctx = None |
|||
) |
Return a Z3 integer value. If `ctx=None`, then the global context is used. >>> IntVal(1) 1 >>> IntVal("100") 100
Definition at line 3180 of file z3py.py.
Referenced by SeqRef.__getitem__(), AstMap.__len__(), ArithRef.__mod__(), BoolRef.__mul__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), _py2expr(), IntNumRef.as_binary_string(), IntNumRef.as_long(), IntNumRef.as_string(), SeqRef.at(), IndexOf(), IntVal(), is_app(), is_arith(), is_ast(), is_const(), is_expr(), is_int(), is_int_value(), is_rational_value(), is_seq(), AstMap.keys(), AstMap.reset(), SeqSort(), and substitute().
IntVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of integer constants of size `sz`. >>> X = IntVector('x', 3) >>> X [x__0, x__1, x__2] >>> Sum(X) x__0 + x__1 + x__2
Definition at line 3266 of file z3py.py.
Referenced by IntVector(), Product(), and Sum().
is_add | ( | a | ) |
Return `True` if `a` is an expression of the form b + c. >>> x, y = Ints('x y') >>> is_add(x + y) True >>> is_add(x - y) False
Definition at line 2788 of file z3py.py.
Referenced by is_add().
is_algebraic_value | ( | a | ) |
Return `True` if `a` is an algebraic value of sort Real. >>> is_algebraic_value(RealVal("3/5")) False >>> n = simplify(Sqrt(2)) >>> n 1.4142135623? >>> is_algebraic_value(n) True
Definition at line 2774 of file z3py.py.
Referenced by is_algebraic_value().
is_and | ( | a | ) |
Return `True` if `a` is a Z3 and expression. >>> p, q = Bools('p q') >>> is_and(And(p, q)) True >>> is_and(Or(p, q)) False
Definition at line 1617 of file z3py.py.
Referenced by is_and().
is_app | ( | a | ) |
Return `True` if `a` is a Z3 function application. Note that, constants are function applications with 0 arguments. >>> a = Int('a') >>> is_app(a) True >>> is_app(a + 1) True >>> is_app(IntSort()) False >>> is_app(1) False >>> is_app(IntVal(1)) True >>> x = Int('x') >>> is_app(ForAll(x, x >= 0)) False
Definition at line 1261 of file z3py.py.
Referenced by _mk_quantifier(), ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app(), is_app_of(), is_const(), Lambda(), ExprRef.num_args(), and RecAddDefinition().
is_app_of | ( | a, | |
k | |||
) |
Return `True` if `a` is an application of the given kind `k`. >>> x = Int('x') >>> n = x + 1 >>> is_app_of(n, Z3_OP_ADD) True >>> is_app_of(n, Z3_OP_MUL) False
Definition at line 1364 of file z3py.py.
Referenced by is_add(), is_and(), is_app_of(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().
is_arith | ( | a | ) |
Return `True` if `a` is an arithmetical expression. >>> x = Int('x') >>> is_arith(x) True >>> is_arith(x + 1) True >>> is_arith(1) False >>> is_arith(IntVal(1)) True >>> y = Real('y') >>> is_arith(y) True >>> is_arith(y + 1) True
Definition at line 2661 of file z3py.py.
Referenced by is_algebraic_value(), is_arith(), is_int(), is_int_value(), is_rational_value(), and is_real().
is_arith_sort | ( | s | ) |
Return `True` if s is an arithmetical sort (type). >>> is_arith_sort(IntSort()) True >>> is_arith_sort(RealSort()) True >>> is_arith_sort(BoolSort()) False >>> n = Int('x') + 1 >>> is_arith_sort(n.sort()) True
Definition at line 2360 of file z3py.py.
Referenced by is_arith_sort(), and ArithSortRef.subsort().
is_array | ( | a | ) |
Return `True` if `a` is a Z3 array expression. >>> a = Array('a', IntSort(), IntSort()) >>> is_array(a) True >>> is_array(Store(a, 0, 1)) True >>> is_array(a[0]) False
Definition at line 4603 of file z3py.py.
Referenced by Ext(), is_array(), and Map().
is_as_array | ( | n | ) |
Return true if n is a Z3 expression of the form (_ as-array f).
Definition at line 6686 of file z3py.py.
Referenced by get_as_array_func(), and ModelRef.get_interp().
is_ast | ( | a | ) |
Return `True` if `a` is an AST node. >>> is_ast(10) False >>> is_ast(IntVal(10)) True >>> is_ast(Int('x')) True >>> is_ast(BoolSort()) True >>> is_ast(Function('f', IntSort(), IntSort())) True >>> is_ast("x") False >>> is_ast(Solver()) False
Definition at line 451 of file z3py.py.
Referenced by _ast_kind(), _ctx_from_ast_arg_list(), eq(), AstRef.eq(), is_ast(), and ReSort().
is_bool | ( | a | ) |
Return `True` if `a` is a Z3 Boolean expression. >>> p = Bool('p') >>> is_bool(p) True >>> q = Bool('q') >>> is_bool(And(p, q)) True >>> x = Real('x') >>> is_bool(x) False >>> is_bool(x == 0) True
Definition at line 1567 of file z3py.py.
Referenced by _mk_quantifier(), _prove_html(), BoolSort(), is_bool(), and prove().
is_bv | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector expression. >>> b = BitVec('b', 32) >>> is_bv(b) True >>> is_bv(b + 10) True >>> is_bv(Int('x')) False
Definition at line 3936 of file z3py.py.
Referenced by _check_bv_args(), BitVec(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToIEEEBV(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv(), is_bv_value(), Product(), RepeatBitVec(), SignExt(), Sum(), and ZeroExt().
is_bv_sort | ( | s | ) |
Return True if `s` is a Z3 bit-vector sort. >>> is_bv_sort(BitVecSort(32)) True >>> is_bv_sort(IntSort()) False
Definition at line 3468 of file z3py.py.
Referenced by BitVecVal(), fpToSBV(), fpToUBV(), is_bv_sort(), and BitVecSortRef.subsort().
is_bv_value | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector numeral value. >>> b = BitVec('b', 32) >>> is_bv_value(b) False >>> b = BitVecVal(10, 32) >>> b 10 >>> is_bv_value(b) True
Definition at line 3950 of file z3py.py.
Referenced by is_bv_value().
is_const | ( | a | ) |
Return `True` if `a` is Z3 constant/variable expression. >>> a = Int('a') >>> is_const(a) True >>> is_const(a + 1) False >>> is_const(1) False >>> is_const(IntVal(1)) True >>> x = Int('x') >>> is_const(ForAll(x, x >= 0)) False
Definition at line 1287 of file z3py.py.
Referenced by ModelRef.__getitem__(), _dict2darray(), _mk_quantifier(), Solver.assert_and_track(), Optimize.assert_and_track(), ModelRef.get_interp(), get_var_index(), is_const(), and is_var().
is_const_array | ( | a | ) |
Return `True` if `a` is a Z3 constant array. >>> a = K(IntSort(), 10) >>> is_const_array(a) True >>> a = Array('a', IntSort(), IntSort()) >>> is_const_array(a) False
Definition at line 4617 of file z3py.py.
Referenced by is_const_array().
is_default | ( | a | ) |
Return `True` if `a` is a Z3 default array expression. >>> d = Default(K(IntSort(), 10)) >>> is_default(d) True
Definition at line 4659 of file z3py.py.
Referenced by is_default().
is_distinct | ( | a | ) |
Return `True` if `a` is a Z3 distinct expression. >>> x, y, z = Ints('x y z') >>> is_distinct(x == y) False >>> is_distinct(Distinct(x, y, z)) True
Definition at line 1675 of file z3py.py.
Referenced by is_distinct().
is_div | ( | a | ) |
Return `True` if `a` is an expression of the form b / c. >>> x, y = Reals('x y') >>> is_div(x / y) True >>> is_div(x + y) False >>> x, y = Ints('x y') >>> is_div(x / y) False >>> is_idiv(x / y) True
Definition at line 2824 of file z3py.py.
Referenced by is_div().
is_eq | ( | a | ) |
Return `True` if `a` is a Z3 equality expression. >>> x, y = Ints('x y') >>> is_eq(x == y) True
Definition at line 1665 of file z3py.py.
Referenced by AstRef.__bool__(), and is_eq().
is_expr | ( | a | ) |
Return `True` if `a` is a Z3 expression. >>> a = Int('a') >>> is_expr(a) True >>> is_expr(a + 1) True >>> is_expr(IntSort()) False >>> is_expr(1) False >>> is_expr(IntVal(1)) True >>> x = Int('x') >>> is_expr(ForAll(x, x >= 0)) True >>> is_expr(FPVal(1.0)) True
Definition at line 1238 of file z3py.py.
Referenced by _coerce_char(), _coerce_expr_list(), _coerce_expr_merge(), _coerce_exprs(), _coerce_seq(), _get_ctx2(), _mk_quantifier(), _py2expr(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), CharFromBv(), Concat(), IndexOf(), IntToStr(), is_expr(), is_sort(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), StrFromCode(), StrToCode(), substitute(), substitute_funs(), substitute_vars(), and ModelRef.update_value().
is_false | ( | a | ) |
Return `True` if `a` is the Z3 false expression. >>> p = Bool('p') >>> is_false(p) False >>> is_false(False) False >>> is_false(BoolVal(False)) True
Definition at line 1603 of file z3py.py.
Referenced by AstRef.__bool__(), BoolVal(), and is_false().
is_finite_domain | ( | a | ) |
Return `True` if `a` is a Z3 finite-domain expression. >>> s = FiniteDomainSort('S', 100) >>> b = Const('b', s) >>> is_finite_domain(b) True >>> is_finite_domain(Int('x')) False
Definition at line 7739 of file z3py.py.
Referenced by is_finite_domain(), and is_finite_domain_value().
is_finite_domain_sort | ( | s | ) |
Return True if `s` is a Z3 finite-domain sort. >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) True >>> is_finite_domain_sort(IntSort()) False
Definition at line 7716 of file z3py.py.
Referenced by FiniteDomainVal(), and is_finite_domain_sort().
is_finite_domain_value | ( | a | ) |
Return `True` if `a` is a Z3 finite-domain value. >>> s = FiniteDomainSort('S', 100) >>> b = Const('b', s) >>> is_finite_domain_value(b) False >>> b = FiniteDomainVal(10, s) >>> b 10 >>> is_finite_domain_value(b) True
Definition at line 7793 of file z3py.py.
Referenced by is_finite_domain_value().
is_fp | ( | a | ) |
Return `True` if `a` is a Z3 floating-point expression. >>> b = FP('b', FPSort(8, 24)) >>> is_fp(b) True >>> is_fp(b + 1.0) True >>> is_fp(Int('x')) False
Definition at line 9920 of file z3py.py.
Referenced by _check_fp_args(), _coerce_fp_expr_list(), _mk_fp_bin(), _mk_fp_bin_norm(), _mk_fp_bin_pred(), _mk_fp_tern(), _mk_fp_unary(), _mk_fp_unary_pred(), FP(), fpFPToFP(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), and is_fp_value().
is_fp_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point sort. >>> is_fp_sort(FPSort(8, 24)) True >>> is_fp_sort(IntSort()) False
Definition at line 9504 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), and FPVal().
is_fp_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point numeral value. >>> b = FP('b', FPSort(8, 24)) >>> is_fp_value(b) False >>> b = FPVal(1.0, FPSort(8, 24)) >>> b 1 >>> is_fp_value(b) True
Definition at line 9934 of file z3py.py.
Referenced by is_fp_value().
is_fprm | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode expression. >>> rm = RNE() >>> is_fprm(rm) True >>> rm = 1.0 >>> is_fprm(rm) False
Definition at line 9764 of file z3py.py.
Referenced by _mk_fp_bin(), _mk_fp_tern(), _mk_fp_unary(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_fprm(), and is_fprm_value().
is_fprm_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point rounding mode sort. >>> is_fprm_sort(FPSort(8, 24)) False >>> is_fprm_sort(RNE().sort()) True
Definition at line 9515 of file z3py.py.
Referenced by is_fprm_sort().
is_fprm_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode numeral value.
Definition at line 9777 of file z3py.py.
Referenced by set_default_rounding_mode().
is_func_decl | ( | a | ) |
Return `True` if `a` is a Z3 function declaration. >>> f = Function('f', IntSort(), IntSort()) >>> is_func_decl(f) True >>> x = Real('x') >>> is_func_decl(x) False
Definition at line 846 of file z3py.py.
Referenced by _dict2darray(), is_func_decl(), Map(), substitute_funs(), and ModelRef.update_value().
is_ge | ( | a | ) |
Return `True` if `a` is an expression of the form b >= c. >>> x, y = Ints('x y') >>> is_ge(x >= y) True >>> is_ge(x == y) False
Definition at line 2889 of file z3py.py.
Referenced by is_ge().
is_gt | ( | a | ) |
Return `True` if `a` is an expression of the form b > c. >>> x, y = Ints('x y') >>> is_gt(x > y) True >>> is_gt(x == y) False
Definition at line 2901 of file z3py.py.
Referenced by is_gt().
is_idiv | ( | a | ) |
Return `True` if `a` is an expression of the form b div c. >>> x, y = Ints('x y') >>> is_idiv(x / y) True >>> is_idiv(x + y) False
Definition at line 2841 of file z3py.py.
is_implies | ( | a | ) |
Return `True` if `a` is a Z3 implication expression. >>> p, q = Bools('p q') >>> is_implies(Implies(p, q)) True >>> is_implies(And(p, q)) False
Definition at line 1641 of file z3py.py.
Referenced by is_implies().
is_int | ( | a | ) |
Return `True` if `a` is an integer expression. >>> x = Int('x') >>> is_int(x + 1) True >>> is_int(1) False >>> is_int(IntVal(1)) True >>> y = Real('y') >>> is_int(y) False >>> is_int(y + 1) False
Definition at line 2682 of file z3py.py.
Referenced by Int(), IntSort(), is_int(), and RealSort().
is_int_value | ( | a | ) |
Return `True` if `a` is an integer value of sort Int. >>> is_int_value(IntVal(1)) True >>> is_int_value(1) False >>> is_int_value(Int('x')) False >>> n = Int('x') + 1 >>> n x + 1 >>> n.arg(1) 1 >>> is_int_value(n.arg(1)) True >>> is_int_value(RealVal("1/3")) False >>> is_int_value(RealVal(1)) False
Definition at line 2728 of file z3py.py.
Referenced by is_int_value().
is_is_int | ( | a | ) |
Return `True` if `a` is an expression of the form IsInt(b). >>> x = Real('x') >>> is_is_int(IsInt(x)) True >>> is_is_int(x) False
Definition at line 2913 of file z3py.py.
Referenced by is_is_int().
is_K | ( | a | ) |
Return `True` if `a` is a Z3 constant array. >>> a = K(IntSort(), 10) >>> is_K(a) True >>> a = Array('a', IntSort(), IntSort()) >>> is_K(a) False
Definition at line 4630 of file z3py.py.
Referenced by is_K().
is_le | ( | a | ) |
Return `True` if `a` is an expression of the form b <= c. >>> x, y = Ints('x y') >>> is_le(x <= y) True >>> is_le(x < y) False
Definition at line 2865 of file z3py.py.
Referenced by is_le().
is_lt | ( | a | ) |
Return `True` if `a` is an expression of the form b < c. >>> x, y = Ints('x y') >>> is_lt(x < y) True >>> is_lt(x == y) False
Definition at line 2877 of file z3py.py.
Referenced by is_lt().
is_map | ( | a | ) |
Return `True` if `a` is a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort()) >>> b = Array('b', IntSort(), IntSort()) >>> a = Map(f, b) >>> a Map(f, b) >>> is_map(a) True >>> is_map(b) False
Definition at line 4643 of file z3py.py.
Referenced by get_map_func(), and is_map().
is_mod | ( | a | ) |
Return `True` if `a` is an expression of the form b % c. >>> x, y = Ints('x y') >>> is_mod(x % y) True >>> is_mod(x + y) False
Definition at line 2853 of file z3py.py.
Referenced by is_mod().
is_mul | ( | a | ) |
Return `True` if `a` is an expression of the form b * c. >>> x, y = Ints('x y') >>> is_mul(x * y) True >>> is_mul(x - y) False
Definition at line 2800 of file z3py.py.
Referenced by is_mul().
is_not | ( | a | ) |
Return `True` if `a` is a Z3 not expression. >>> p = Bool('p') >>> is_not(p) False >>> is_not(Not(p)) True
Definition at line 1653 of file z3py.py.
is_or | ( | a | ) |
Return `True` if `a` is a Z3 or expression. >>> p, q = Bools('p q') >>> is_or(Or(p, q)) True >>> is_or(And(p, q)) False
Definition at line 1629 of file z3py.py.
Referenced by is_or().
is_pattern | ( | a | ) |
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) >>> q ForAll(x, f(x) == 0) >>> q.num_patterns() 1 >>> is_pattern(q.pattern(0)) True >>> q.pattern(0) f(Var(0))
Definition at line 1929 of file z3py.py.
Referenced by _mk_quantifier(), _to_pattern(), is_pattern(), and MultiPattern().
is_probe | ( | p | ) |
Return `True` if `p` is a Z3 probe. >>> is_probe(Int('x')) False >>> is_probe(Probe('memory')) True
Definition at line 8685 of file z3py.py.
Referenced by _ctx_from_ast_arg_list(), _has_probe(), _to_probe(), is_probe(), and Not().
is_quantifier | ( | a | ) |
Return `True` if `a` is a Z3 quantifier. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> is_quantifier(q) True >>> is_quantifier(f(x)) False
Definition at line 2169 of file z3py.py.
Referenced by Exists(), and is_quantifier().
is_rational_value | ( | a | ) |
Return `True` if `a` is rational value of sort Real. >>> is_rational_value(RealVal(1)) True >>> is_rational_value(RealVal("3/5")) True >>> is_rational_value(IntVal(1)) False >>> is_rational_value(1) False >>> n = Real('x') + 1 >>> n.arg(1) 1 >>> is_rational_value(n.arg(1)) True >>> is_rational_value(Real('x')) False
Definition at line 2752 of file z3py.py.
Referenced by RatNumRef.denominator(), is_rational_value(), and RatNumRef.numerator().
is_re | ( | s | ) |
Definition at line 11216 of file z3py.py.
Referenced by Concat(), Intersect(), and Union().
is_real | ( | a | ) |
Return `True` if `a` is a real expression. >>> x = Int('x') >>> is_real(x + 1) False >>> y = Real('y') >>> is_real(y) True >>> is_real(y + 1) True >>> is_real(1) False >>> is_real(RealVal(1)) True
Definition at line 2701 of file z3py.py.
Referenced by fpRealToFP(), fpToFP(), fpToReal(), is_real(), Real(), and RealSort().
is_select | ( | a | ) |
Return `True` if `a` is a Z3 array select application. >>> a = Array('a', IntSort(), IntSort()) >>> is_select(a) False >>> i = Int('i') >>> is_select(a[i]) True
Definition at line 4878 of file z3py.py.
Referenced by is_select().
is_seq | ( | a | ) |
Return `True` if `a` is a Z3 sequence expression. >>> print (is_seq(Unit(IntVal(0)))) True >>> print (is_seq(StringVal("abc"))) True
Definition at line 10942 of file z3py.py.
Referenced by _coerce_seq(), Concat(), Extract(), and is_seq().
is_sort | ( | s | ) |
Return `True` if `s` is a Z3 sort. >>> is_sort(IntSort()) True >>> is_sort(Int('x')) False >>> is_expr(Int('x')) True
Definition at line 647 of file z3py.py.
Referenced by _dict2sarray(), _valid_accessor(), ArraySort(), CreateDatatypes(), FreshFunction(), Function(), is_sort(), K(), PropagateFunction(), RecFunction(), and Var().
is_store | ( | a | ) |
Return `True` if `a` is a Z3 array store application. >>> a = Array('a', IntSort(), IntSort()) >>> is_store(a) False >>> is_store(Store(a, 0, 1)) True
Definition at line 4891 of file z3py.py.
Referenced by is_store().
is_string | ( | a | ) |
Return `True` if `a` is a Z3 string expression. >>> print (is_string(StringVal("ab"))) True
Definition at line 10952 of file z3py.py.
Referenced by is_string().
is_string_value | ( | a | ) |
return 'True' if 'a' is a Z3 string constant expression. >>> print (is_string_value(StringVal("a"))) True >>> print (is_string_value(StringVal("a") + StringVal("b"))) False
Definition at line 10960 of file z3py.py.
Referenced by is_string_value().
is_sub | ( | a | ) |
Return `True` if `a` is an expression of the form b - c. >>> x, y = Ints('x y') >>> is_sub(x - y) True >>> is_sub(x + y) False
Definition at line 2812 of file z3py.py.
Referenced by is_sub().
is_to_int | ( | a | ) |
Return `True` if `a` is an expression of the form ToInt(b). >>> x = Real('x') >>> n = ToInt(x) >>> n ToInt(x) >>> is_to_int(n) True >>> is_to_int(x) False
Definition at line 2940 of file z3py.py.
Referenced by is_to_int().
is_to_real | ( | a | ) |
Return `True` if `a` is an expression of the form ToReal(b). >>> x = Int('x') >>> n = ToReal(x) >>> n ToReal(x) >>> is_to_real(n) True >>> is_to_real(x) False
Definition at line 2925 of file z3py.py.
Referenced by is_to_real().
is_true | ( | a | ) |
Return `True` if `a` is the Z3 true expression. >>> p = Bool('p') >>> is_true(p) False >>> is_true(simplify(p == p)) True >>> x = Real('x') >>> is_true(x == 0) False >>> # True is a Python Boolean expression >>> is_true(True) False
Definition at line 1585 of file z3py.py.
Referenced by AstRef.__bool__(), BoolVal(), and is_true().
is_var | ( | a | ) |
Return `True` if `a` is variable. Z3 uses de-Bruijn indices for representing bound variables in quantifiers. >>> x = Int('x') >>> is_var(x) False >>> is_const(x) True >>> f = Function('f', IntSort(), IntSort()) >>> # Z3 replaces x with bound variables when ForAll is executed. >>> q = ForAll(x, f(x) == x) >>> b = q.body() >>> b f(Var(0)) == Var(0) >>> b.arg(1) Var(0) >>> is_var(b.arg(1)) True
Definition at line 1306 of file z3py.py.
Referenced by get_var_index(), and is_var().
IsInt | ( | a | ) |
Return the Z3 predicate IsInt(a). >>> x = Real('x') >>> IsInt(x + "1/2") IsInt(x + 1/2) >>> solve(IsInt(x + "1/2"), x > 0, x < 1) [x = 1/2] >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") no solution
Definition at line 3386 of file z3py.py.
Referenced by is_is_int(), and IsInt().
IsMember | ( | e, | |
s | |||
) |
Check if e is a member of set s >>> a = Const('a', SetSort(IntSort())) >>> IsMember(1, a) a[1]
Definition at line 5001 of file z3py.py.
Referenced by IsMember().
IsSubset | ( | a, | |
b | |||
) |
Check if a is a subset of b >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> IsSubset(a, b) subset(a, b)
Definition at line 5012 of file z3py.py.
Referenced by IsSubset().
K | ( | dom, | |
v | |||
) |
Return a Z3 constant array expression. >>> a = K(IntSort(), 10) >>> a K(Int, 10) >>> a.sort() Array(Int, Int) >>> i = Int('i') >>> a[i] K(Int, 10)[i] >>> simplify(a[i]) 10
Definition at line 4838 of file z3py.py.
Referenced by Default(), EmptySet(), FullSet(), ModelRef.get_interp(), is_const_array(), is_default(), is_K(), and K().
Lambda | ( | vs, | |
body | |||
) |
Create a Z3 lambda expression. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> mem0 = Array('mem0', IntSort(), IntSort()) >>> lo, hi, e, i = Ints('lo hi e i') >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i])) >>> mem1 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
Definition at line 2257 of file z3py.py.
Referenced by QuantifierRef.is_lambda(), and Lambda().
LastIndexOf | ( | s, | |
substr | |||
) |
Retrieve the last index of substring within a string
Definition at line 11127 of file z3py.py.
Length | ( | s | ) |
Obtain the length of a sequence 's' >>> l = Length(StringVal("abc")) >>> simplify(l) 3
Definition at line 11136 of file z3py.py.
Referenced by Length().
LinearOrder | ( | a, | |
index | |||
) |
Loop | ( | re, | |
lo, | |||
hi = 0 |
|||
) |
Create the regular expression accepting between a lower and upper bound repetitions >>> re = Loop(Re("a"), 1, 3) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("aaaa", re))) False >>> print(simplify(InRe("", re))) False
Definition at line 11316 of file z3py.py.
Referenced by Loop().
LShR | ( | a, | |
b | |||
) |
Create the Z3 expression logical right shift. Use the operator >> for the arithmetical right shift. >>> x, y = BitVecs('x y', 32) >>> LShR(x, y) LShR(x, y) >>> (x >> y).sexpr() '(bvashr x y)' >>> LShR(x, y).sexpr() '(bvlshr x y)' >>> BitVecVal(4, 3) 4 >>> BitVecVal(4, 3).as_signed_long() -4 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() -2 >>> simplify(BitVecVal(4, 3) >> 1) 6 >>> simplify(LShR(BitVecVal(4, 3), 1)) 2 >>> simplify(BitVecVal(2, 3) >> 1) 1 >>> simplify(LShR(BitVecVal(2, 3), 1)) 1
Definition at line 4291 of file z3py.py.
Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), and LShR().
main_ctx | ( | ) |
Return a reference to the global Z3 context. >>> x = Real('x') >>> x.ctx == main_ctx() True >>> c = Context() >>> c == main_ctx() False >>> x2 = Real('x', c) >>> x2.ctx == c True >>> eq(x, x2) False
Definition at line 239 of file z3py.py.
Referenced by _get_ctx(), _get_ctx2(), help_simplify(), main_ctx(), simplify_param_descrs(), and Goal.translate().
Map | ( | f, | |
* | args | ||
) |
Return a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> a1 = Array('a1', IntSort(), IntSort()) >>> a2 = Array('a2', IntSort(), IntSort()) >>> b = Map(f, a1, a2) >>> b Map(f, a1, a2) >>> prove(b[0] == f(a1[0], a2[0])) proved
Definition at line 4815 of file z3py.py.
Referenced by get_map_func(), is_map(), and Map().
mk_not | ( | a | ) |
Model | ( | ctx = None | ) |
Definition at line 6681 of file z3py.py.
Referenced by Optimize.set_on_model().
MultiPattern | ( | * | args | ) |
Create a Z3 multi-pattern using the given expressions `*args` >>> f = Function('f', IntSort(), IntSort()) >>> g = Function('g', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ]) >>> q ForAll(x, f(x) != g(x)) >>> q.num_patterns() 1 >>> is_pattern(q.pattern(0)) True >>> q.pattern(0) MultiPattern(f(Var(0)), g(Var(0)))
Definition at line 1947 of file z3py.py.
Referenced by _to_pattern(), and MultiPattern().
Not | ( | a, | |
ctx = None |
|||
) |
Create a Z3 not expression or probe. >>> p = Bool('p') >>> Not(Not(p)) Not(Not(p)) >>> simplify(Not(Not(p))) p
Definition at line 1811 of file z3py.py.
Referenced by _prove_html(), AndThen(), ApplyResult.as_expr(), Solver.consequences(), Goal.convert_model(), Distinct(), FailIf(), fpNEQ(), is_not(), mk_not(), Not(), prove(), simplify(), Then(), When(), and Xor().
on_clause_eh | ( | ctx, | |
p, | |||
clause | |||
) |
open_log | ( | fname | ) |
Log interaction to a file. This function must be invoked immediately after init().
Definition at line 114 of file z3py.py.
Option | ( | re | ) |
Create the regular expression that optionally accepts the argument. >>> re = Option(Re("a")) >>> print(simplify(InRe("a", re))) True >>> print(simplify(InRe("", re))) True >>> print(simplify(InRe("aa", re))) False
Definition at line 11285 of file z3py.py.
Referenced by Option().
Or | ( | * | args | ) |
Create a Z3 or-expression or or-probe. >>> p, q, r = Bools('p q r') >>> Or(p, q, r) Or(p, q, r) >>> P = BoolVector('p', 5) >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4)
Definition at line 1878 of file z3py.py.
Referenced by ApplyResult.__getitem__(), ApplyResult.__len__(), ApplyResult.as_expr(), Bools(), Goal.convert_model(), is_and(), is_or(), Or(), OrElse(), ParThen(), prove(), Repeat(), and simplify().
OrElse | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). >>> x = Int('x') >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) >>> # Tactic split-clause fails if there is no clause in the given goal. >>> t(x == 0) [[x == 0]] >>> t(Or(x == 0, x == 1)) [[x == 0], [x == 1]]
Definition at line 8378 of file z3py.py.
ParAndThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
ParOr | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). >>> x = Int('x') >>> t = ParOr(Tactic('simplify'), Tactic('fail')) >>> t(x + 1 == 2) [[x == 1]]
Definition at line 8399 of file z3py.py.
Referenced by ParOr().
parse_smt2_file | ( | f, | |
sorts = {} , |
|||
decls = {} , |
|||
ctx = None |
|||
) |
Parse a file in SMT 2.0 format using the given sorts and decls. This function is similar to parse_smt2_string().
Definition at line 9314 of file z3py.py.
parse_smt2_string | ( | s, | |
sorts = {} , |
|||
decls = {} , |
|||
ctx = None |
|||
) |
Parse a string in SMT 2.0 format using the given sorts and decls. The arguments sorts and decls are Python dictionaries used to initialize the symbol table used for the SMT 2.0 parser. >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') [x > 0, x < 10] >>> x, y = Ints('x y') >>> f = Function('f', IntSort(), IntSort()) >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) [x + f(y) > 0] >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) [a > 0]
Definition at line 9293 of file z3py.py.
Referenced by parse_smt2_file(), and parse_smt2_string().
ParThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. >>> x, y = Ints('x y') >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) >>> t(And(Or(x == 1, x == 2), y == x + 1)) [[x == 1, y == 2], [x == 2, y == 3]]
Definition at line 8418 of file z3py.py.
Referenced by ParAndThen(), and ParThen().
PartialOrder | ( | a, | |
index | |||
) |
PbEq | ( | args, | |
k, | |||
ctx = None |
|||
) |
Create a Pseudo-Boolean equality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
Definition at line 9070 of file z3py.py.
Referenced by PbEq().
PbGe | ( | args, | |
k | |||
) |
Create a Pseudo-Boolean inequality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
Definition at line 9059 of file z3py.py.
Referenced by PbGe().
PbLe | ( | args, | |
k | |||
) |
Create a Pseudo-Boolean inequality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
Definition at line 9048 of file z3py.py.
Referenced by PbLe().
PiecewiseLinearOrder | ( | a, | |
index | |||
) |
Plus | ( | re | ) |
Create the regular expression accepting one or more repetitions of argument. >>> re = Plus(Re("a")) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("ab", re))) False >>> print(simplify(InRe("", re))) False
Definition at line 11272 of file z3py.py.
Referenced by Plus().
PrefixOf | ( | a, | |
b | |||
) |
Check if 'a' is a prefix of 'b' >>> s1 = PrefixOf("ab", "abc") >>> simplify(s1) True >>> s2 = PrefixOf("bc", "abc") >>> simplify(s2) False
Definition at line 11043 of file z3py.py.
Referenced by PrefixOf().
probe_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the probe named `name`. >>> d = probe_description('memory')
Definition at line 8714 of file z3py.py.
Referenced by describe_probes(), and probe_description().
probes | ( | ctx = None | ) |
Return a list of all available probes in Z3. >>> l = probes() >>> l.count('memory') == 1 True
Definition at line 8703 of file z3py.py.
Referenced by describe_probes(), and probes().
Product | ( | * | args | ) |
Create the product of the Z3 expressions. >>> a, b, c = Ints('a b c') >>> Product(a, b, c) a*b*c >>> Product([a, b, c]) a*b*c >>> A = IntVector('a', 5) >>> Product(A) a__0*a__1*a__2*a__3*a__4
Definition at line 8955 of file z3py.py.
PropagateFunction | ( | name, | |
* | sig | ||
) |
Create a function that gets tracked by user propagator. Every term headed by this function symbol is tracked. If a term is fixed and the fixed callback is registered a callback is invoked that the term headed by this function is fixed.
Definition at line 11549 of file z3py.py.
prove | ( | claim, | |
show = False , |
|||
** | keywords | ||
) |
Try to prove the given claim. This is a simple function for creating demonstrations. It tries to prove `claim` by showing the negation is unsatisfiable. >>> p, q = Bools('p q') >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) proved
Definition at line 9142 of file z3py.py.
Referenced by Default(), Map(), prove(), Store(), and Update().
Q | ( | a, | |
b, | |||
ctx = None |
|||
) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. >>> Q(3,5) 3/5 >>> Q(3,5).sort() Real
Definition at line 3227 of file z3py.py.
Referenced by RatNumRef.as_string(), RatNumRef.denominator(), RatNumRef.numerator(), and Q().
Range | ( | lo, | |
hi, | |||
ctx = None |
|||
) |
Create the range regular expression over two sequences of length 1 >>> range = Range("a","z") >>> print(simplify(InRe("b", range))) True >>> print(simplify(InRe("bb", range))) False
Definition at line 11329 of file z3py.py.
Referenced by Range().
RatVal | ( | a, | |
b, | |||
ctx = None |
|||
) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. >>> RatVal(3,5) 3/5 >>> RatVal(3,5).sort() Real
Definition at line 3211 of file z3py.py.
Re | ( | s, | |
ctx = None |
|||
) |
The regular expression that accepts sequence 's' >>> s1 = Re("ab") >>> s2 = Re(StringVal("ab")) >>> s3 = Re(Unit(BoolVal(True)))
Definition at line 11181 of file z3py.py.
Referenced by InRe(), Intersect(), Loop(), Option(), Plus(), Re(), Star(), and Union().
Real | ( | name, | |
ctx = None |
|||
) |
Return a real constant named `name`. If `ctx=None`, then the global context is used. >>> x = Real('x') >>> is_real(x) True >>> is_real(x + 1) True
Definition at line 3293 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), is_bool(), is_func_decl(), is_int(), ArithSortRef.is_int(), ArithRef.is_int(), is_is_int(), is_rational_value(), is_real(), ArithSortRef.is_real(), ArithRef.is_real(), is_to_int(), is_true(), IsInt(), main_ctx(), Real(), Reals(), RealVector(), Tactic.solver(), ExprRef.sort(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().
Reals | ( | names, | |
ctx = None |
|||
) |
Return a tuple of real constants. >>> x, y, z = Reals('x y z') >>> Sum(x, y, z) x + y + z >>> Sum(x, y, z).sort() Real
Definition at line 3306 of file z3py.py.
RealSort | ( | ctx = None | ) |
Return the real sort in the given context. If `ctx=None`, then the global context is used. >>> RealSort() Real >>> x = Const('x', RealSort()) >>> is_real(x) True >>> is_int(x) False >>> x.sort() == RealSort() True
Definition at line 3151 of file z3py.py.
Referenced by FuncDeclRef.__call__(), FuncDeclRef.arity(), SortRef.cast(), ArithSortRef.cast(), FuncDeclRef.domain(), FreshReal(), is_arith_sort(), FuncDeclRef.range(), Real(), RealSort(), RealVal(), RealVar(), SortRef.subsort(), and QuantifierRef.var_sort().
RealVal | ( | val, | |
ctx = None |
|||
) |
Return a Z3 real value. `val` may be a Python int, long, float or string representing a number in decimal or rational notation. If `ctx=None`, then the global context is used. >>> RealVal(1) 1 >>> RealVal(1).sort() Real >>> RealVal("3/5") 3/5 >>> RealVal("1.5") 3/2
Definition at line 3192 of file z3py.py.
Referenced by _coerce_exprs(), _py2expr(), RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), fpRealToFP(), fpToFP(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), RatNumRef.numerator_as_long(), RatVal(), RealVal(), and Sqrt().
RealVar | ( | idx, | |
ctx = None |
|||
) |
Create a real free variable. Free variables are used to create quantified formulas. They are also used to create polynomials. >>> RealVar(0) Var(0)
Definition at line 1481 of file z3py.py.
Referenced by RealVar(), and RealVarVector().
RealVarVector | ( | n, | |
ctx = None |
|||
) |
Create a list of Real free variables. The variables have ids: 0, 1, ..., n-1 >>> x0, x1, x2, x3 = RealVarVector(4) >>> x2 Var(2)
Definition at line 1492 of file z3py.py.
Referenced by RealVarVector().
RealVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of real constants of size `sz`. >>> X = RealVector('x', 3) >>> X [x__0, x__1, x__2] >>> Sum(X) x__0 + x__1 + x__2 >>> Sum(X).sort() Real
Definition at line 3321 of file z3py.py.
Referenced by RealVector().
RecAddDefinition | ( | f, | |
args, | |||
body | |||
) |
Set the body of a recursive function. Recursive definitions can be simplified if they are applied to ground arguments. >>> ctx = Context() >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) >>> n = Int('n', ctx) >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) >>> simplify(fac(5)) 120 >>> s = Solver(ctx=ctx) >>> s.add(fac(n) < 3) >>> s.check() sat >>> s.model().eval(fac(5)) 120
Definition at line 923 of file z3py.py.
Referenced by RecAddDefinition().
RecFunction | ( | name, | |
* | sig | ||
) |
Create a new Z3 recursive with the given sorts.
Definition at line 905 of file z3py.py.
Referenced by RecAddDefinition().
Repeat | ( | t, | |
max = 4294967295 , |
|||
ctx = None |
|||
) |
Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. >>> x, y = Ints('x y') >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) >>> r = t(c) >>> for subgoal in r: print(subgoal) [x == 0, y == 0, x > y] [x == 0, y == 1, x > y] [x == 1, y == 0, x > y] [x == 1, y == 1, x > y] >>> t = Then(t, Tactic('propagate-values')) >>> t(c) [[x == 1, y == 0]]
Definition at line 8467 of file z3py.py.
Referenced by Repeat().
RepeatBitVec | ( | n, | |
a | |||
) |
Return an expression representing `n` copies of `a`. >>> x = BitVec('x', 8) >>> n = RepeatBitVec(4, x) >>> n RepeatBitVec(4, x) >>> n.size() 32 >>> v0 = BitVecVal(10, 4) >>> print("%.x" % v0.as_long()) a >>> v = simplify(RepeatBitVec(4, v0)) >>> v.size() 16 >>> print("%.x" % v.as_long()) aaaa
Definition at line 4413 of file z3py.py.
Referenced by RepeatBitVec().
Replace | ( | s, | |
src, | |||
dst | |||
) |
Replace the first occurrence of 'src' by 'dst' in 's' >>> r = Replace("aaa", "a", "b") >>> simplify(r) "baa"
Definition at line 11092 of file z3py.py.
Referenced by Replace().
reset_params | ( | ) |
Reset all global (or module) parameters.
Definition at line 295 of file z3py.py.
ReSort | ( | s | ) |
Definition at line 11200 of file z3py.py.
RNA | ( | ctx = None | ) |
Definition at line 9729 of file z3py.py.
Referenced by get_default_rounding_mode().
RNE | ( | ctx = None | ) |
Definition at line 9719 of file z3py.py.
Referenced by fpAbs(), fpAdd(), fpDiv(), fpFPToFP(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRealToFP(), FPs(), fpSignedToFP(), fpSub(), fpToFP(), fpUnsignedToFP(), get_default_rounding_mode(), is_fprm(), and is_fprm_sort().
RotateLeft | ( | a, | |
b | |||
) |
Return an expression representing `a` rotated to the left `b` times. >>> a, b = BitVecs('a b', 16) >>> RotateLeft(a, b) RotateLeft(a, b) >>> simplify(RotateLeft(a, 0)) a >>> simplify(RotateLeft(a, 16)) a
Definition at line 4323 of file z3py.py.
Referenced by RotateLeft().
RotateRight | ( | a, | |
b | |||
) |
Return an expression representing `a` rotated to the right `b` times. >>> a, b = BitVecs('a b', 16) >>> RotateRight(a, b) RotateRight(a, b) >>> simplify(RotateRight(a, 0)) a >>> simplify(RotateRight(a, 16)) a
Definition at line 4339 of file z3py.py.
Referenced by RotateRight().
RoundNearestTiesToAway | ( | ctx = None | ) |
RoundNearestTiesToEven | ( | ctx = None | ) |
RoundTowardNegative | ( | ctx = None | ) |
RoundTowardPositive | ( | ctx = None | ) |
RoundTowardZero | ( | ctx = None | ) |
RTN | ( | ctx = None | ) |
Definition at line 9749 of file z3py.py.
Referenced by get_default_rounding_mode().
RTP | ( | ctx = None | ) |
Definition at line 9739 of file z3py.py.
Referenced by get_default_rounding_mode().
RTZ | ( | ctx = None | ) |
Select | ( | a, | |
* | args | ||
) |
Return a Z3 select array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i = Int('i') >>> Select(a, i) a[i] >>> eq(Select(a, i), a[i]) True
Definition at line 4799 of file z3py.py.
Referenced by Select().
SeqSort | ( | s | ) |
Create a sequence sort over elements provided in the argument >>> s = SeqSort(IntSort()) >>> s == Unit(IntVal(1)).sort() True
Definition at line 10813 of file z3py.py.
Referenced by Empty(), Full(), SeqSortRef.is_string(), and SeqSort().
set_default_fp_sort | ( | ebits, | |
sbits, | |||
ctx = None |
|||
) |
set_default_rounding_mode | ( | rm, | |
ctx = None |
|||
) |
Definition at line 9362 of file z3py.py.
set_option | ( | * | args, |
** | kws | ||
) |
set_param | ( | * | args, |
** | kws | ||
) |
Set Z3 global (or module) parameters. >>> set_param(precision=10)
Definition at line 271 of file z3py.py.
Referenced by set_option(), and set_param().
SetAdd | ( | s, | |
e | |||
) |
Add element e to set s >>> a = Const('a', SetSort(IntSort())) >>> SetAdd(a, 1) Store(a, 1, True)
Definition at line 4958 of file z3py.py.
Referenced by SetAdd().
SetComplement | ( | s | ) |
The complement of set s >>> a = Const('a', SetSort(IntSort())) >>> SetComplement(a) complement(a)
Definition at line 4980 of file z3py.py.
Referenced by SetComplement().
SetDel | ( | s, | |
e | |||
) |
Remove element e to set s >>> a = Const('a', SetSort(IntSort())) >>> SetDel(a, 1) Store(a, 1, False)
Definition at line 4969 of file z3py.py.
Referenced by SetDel().
SetDifference | ( | a, | |
b | |||
) |
The set difference of a and b >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetDifference(a, b) setminus(a, b)
Definition at line 4990 of file z3py.py.
Referenced by SetDifference().
SetHasSize | ( | a, | |
k | |||
) |
SetIntersect | ( | * | args | ) |
Take the union of sets >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetIntersect(a, b) intersection(a, b)
Definition at line 4945 of file z3py.py.
Referenced by SetIntersect().
SetSort | ( | s | ) |
Sets.
Create a set sort over element sort s
Definition at line 4909 of file z3py.py.
Referenced by Ext(), IsMember(), IsSubset(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().
SetUnion | ( | * | args | ) |
Take the union of sets >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetUnion(a, b) union(a, b)
Definition at line 4932 of file z3py.py.
Referenced by SetUnion().
SignExt | ( | n, | |
a | |||
) |
Return a bit-vector expression with `n` extra sign-bits. >>> x = BitVec('x', 16) >>> n = SignExt(8, x) >>> n.size() 24 >>> n SignExt(8, x) >>> n.sort() BitVec(24) >>> v0 = BitVecVal(2, 2) >>> v0 2 >>> v0.size() 2 >>> v = simplify(SignExt(6, v0)) >>> v 254 >>> v.size() 8 >>> print("%.x" % v.as_long()) fe
Definition at line 4355 of file z3py.py.
Referenced by SignExt().
SimpleSolver | ( | ctx = None , |
|
logFile = None |
|||
) |
Return a simple general purpose solver with limited amount of preprocessing. >>> s = SimpleSolver() >>> x = Int('x') >>> s.add(x > 0) >>> s.check() sat
Definition at line 7411 of file z3py.py.
Referenced by Solver.reason_unknown(), SimpleSolver(), and Solver.statistics().
simplify | ( | a, | |
* | arguments, | ||
** | keywords | ||
) |
Utils.
Simplify the expression `a` using the given options. This function has many options. Use `help_simplify` to obtain the complete list. >>> x = Int('x') >>> y = Int('y') >>> simplify(x + 1 + y + x + 1) 2 + 2*x + y >>> simplify((x + 1)*(y + 1), som=True) 1 + x + y + x*y >>> simplify(Distinct(x, y, 1), blast_distinct=True) And(Not(x == y), Not(x == 1), Not(y == 1)) >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1)))
Definition at line 8819 of file z3py.py.
Referenced by BitVecRef.__invert__(), BitVecRef.__lshift__(), ArithRef.__mod__(), ArithRef.__neg__(), BitVecRef.__neg__(), ArithRef.__pow__(), ArithRef.__rpow__(), BitVecRef.__rshift__(), AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), BitVecs(), Concat(), Contains(), CreateDatatypes(), Distinct(), eq(), AstRef.eq(), Extract(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), AstRef.hash(), If(), IndexOf(), InRe(), is_algebraic_value(), is_true(), K(), Length(), Loop(), LShR(), Not(), Option(), Plus(), PrefixOf(), Q(), Range(), RatVal(), RecAddDefinition(), DatatypeSortRef.recognizer(), RepeatBitVec(), Replace(), RotateLeft(), RotateRight(), SignExt(), simplify(), Star(), StrToInt(), SuffixOf(), Union(), Xor(), and ZeroExt().
simplify_param_descrs | ( | ) |
Return the set of parameter descriptions for Z3 `simplify` procedure.
Definition at line 8849 of file z3py.py.
solve | ( | * | args, |
** | keywords | ||
) |
Solve the constraints `*args`. This is a simple function for creating demonstrations. It creates a solver, configure it using the options in `keywords`, adds the constraints in `args`, and invokes check. >>> a = Int('a') >>> solve(a > 0, a < 2) [a = 1]
Definition at line 9081 of file z3py.py.
solve_using | ( | s, | |
* | args, | ||
** | keywords | ||
) |
Solve the constraints `*args` using solver `s`. This is a simple function for creating demonstrations. It is similar to `solve`, but it uses the given solver `s`. It configures solver `s` using the options in `keywords`, adds the constraints in `args`, and invokes check.
Definition at line 9111 of file z3py.py.
SolverFor | ( | logic, | |
ctx = None , |
|||
logFile = None |
|||
) |
Create a solver customized for the given logic. The parameter `logic` is a string. It should be contains the name of a SMT-LIB logic. See http://www.smtlib.org/ for the name of all available logics. >>> s = SolverFor("QF_LIA") >>> x = Int('x') >>> s.add(x > 0) >>> s.add(x < 2) >>> s.check() sat >>> s.model() [x = 1]
Definition at line 7390 of file z3py.py.
Referenced by SolverFor().
Sqrt | ( | a, | |
ctx = None |
|||
) |
Return a Z3 expression which represents the square root of a. >>> x = Real('x') >>> Sqrt(x) x**(1/2)
Definition at line 3403 of file z3py.py.
Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), is_algebraic_value(), and Sqrt().
SRem | ( | a, | |
b | |||
) |
Create the Z3 expression signed remainder. Use the operator % for signed modulus, and URem() for unsigned remainder. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> SRem(x, y) SRem(x, y) >>> SRem(x, y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> SRem(x, y).sexpr() '(bvsrem x y)'
Definition at line 4270 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), SRem(), and URem().
Star | ( | re | ) |
Create the regular expression accepting zero or more repetitions of argument. >>> re = Star(Re("a")) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("ab", re))) False >>> print(simplify(InRe("", re))) True
Definition at line 11303 of file z3py.py.
Referenced by Star().
Store | ( | a, | |
* | args | ||
) |
Return a Z3 store array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i, v = Ints('i v') >>> s = Store(a, i, v) >>> s.sort() Array(Int, Int) >>> prove(s[i] == v) proved >>> j = Int('j') >>> prove(Implies(i != j, s[j] == a[j])) proved
Definition at line 4782 of file z3py.py.
Referenced by ModelRef.get_interp(), is_array(), is_store(), SetAdd(), SetDel(), and Store().
StrFromCode | ( | c | ) |
String | ( | name, | |
ctx = None |
|||
) |
Return a string constant named `name`. If `ctx=None`, then the global context is used. >>> x = String('x')
Definition at line 10976 of file z3py.py.
Strings | ( | names, | |
ctx = None |
|||
) |
Return a tuple of String constants.
Definition at line 10985 of file z3py.py.
Referenced by Contains().
StringSort | ( | ctx = None | ) |
Create a string sort >>> s = StringSort() >>> print(s) String
Definition at line 10794 of file z3py.py.
Referenced by DisjointSum(), Empty(), Full(), SeqSortRef.is_string(), String(), and TupleSort().
StringVal | ( | s, | |
ctx = None |
|||
) |
create a string expression
Definition at line 10969 of file z3py.py.
Referenced by _coerce_exprs(), _coerce_seq(), _py2expr(), Empty(), Extract(), is_seq(), is_string(), is_string_value(), Length(), and Re().
StrToCode | ( | s | ) |
Convert a unit length string to integer code
Definition at line 11169 of file z3py.py.
StrToInt | ( | s | ) |
Convert string expression to integer >>> a = StrToInt("1") >>> simplify(1 == a) True >>> b = StrToInt("2") >>> simplify(1 == b) False >>> c = StrToInt(IntToStr(2)) >>> simplify(1 == c) False
Definition at line 11146 of file z3py.py.
Referenced by StrToInt().
SubSeq | ( | s, | |
offset, | |||
length | |||
) |
substitute | ( | t, | |
* | m | ||
) |
Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to. >>> x = Int('x') >>> y = Int('y') >>> substitute(x + 1, (x, y + 1)) y + 1 + 1 >>> f = Function('f', IntSort(), IntSort()) >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 1 + 1
Definition at line 8854 of file z3py.py.
Referenced by substitute().
substitute_funs | ( | t, | |
* | m | ||
) |
Apply substitution m on t, m is a list of pairs of a function and expression (from, to) Every occurrence in to of the function from is replaced with the expression to. The expression to can have free variables, that refer to the arguments of from. For examples, see
Definition at line 8907 of file z3py.py.
substitute_vars | ( | t, | |
* | m | ||
) |
Substitute the free variables in t with the expression in m. >>> v0 = Var(0, IntSort()) >>> v1 = Var(1, IntSort()) >>> x = Int('x') >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> # replace v0 with x+1 and v1 with x >>> substitute_vars(f(v0, v1), x + 1, x) f(x + 1, x)
Definition at line 8887 of file z3py.py.
Referenced by substitute_vars().
SubString | ( | s, | |
offset, | |||
length | |||
) |
SuffixOf | ( | a, | |
b | |||
) |
Check if 'a' is a suffix of 'b' >>> s1 = SuffixOf("ab", "abc") >>> simplify(s1) False >>> s2 = SuffixOf("bc", "abc") >>> simplify(s2) True
Definition at line 11058 of file z3py.py.
Referenced by SuffixOf().
Sum | ( | * | args | ) |
Create the sum of the Z3 expressions. >>> a, b, c = Ints('a b c') >>> Sum(a, b, c) a + b + c >>> Sum([a, b, c]) a + b + c >>> A = IntVector('a', 5) >>> Sum(A) a__0 + a__1 + a__2 + a__3 + a__4
Definition at line 8929 of file z3py.py.
Referenced by BitVecs(), Ints(), IntVector(), Reals(), RealVector(), and Sum().
tactic_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the tactic named `name`. >>> d = tactic_description('simplify')
Definition at line 8508 of file z3py.py.
Referenced by describe_tactics(), and tactic_description().
tactics | ( | ctx = None | ) |
Return a list of all available tactics in Z3. >>> l = tactics() >>> l.count('simplify') == 1 True
Definition at line 8497 of file z3py.py.
Referenced by describe_tactics(), and tactics().
Then | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). >>> x, y = Ints('x y') >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) >>> t(And(x == 0, y > x + 1)) [[Not(y <= 1)]] >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1)
Definition at line 8365 of file z3py.py.
Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), ApplyResult.__len__(), Goal.convert_model(), Goal.depth(), Statistics.get_key_value(), Statistics.keys(), Repeat(), Tactic.solver(), and Then().
to_Ast | ( | ptr | ) |
Definition at line 11377 of file z3py.py.
Referenced by on_clause_eh(), user_prop_created(), user_prop_decide(), user_prop_diseq(), user_prop_eq(), and user_prop_fixed().
to_AstVectorObj | ( | ptr | ) |
Definition at line 11387 of file z3py.py.
Referenced by on_clause_eh().
to_ContextObj | ( | ptr | ) |
Definition at line 11382 of file z3py.py.
Referenced by user_prop_fresh().
to_symbol | ( | s, | |
ctx = None |
|||
) |
Convert an integer or string into a Z3 symbol.
Definition at line 124 of file z3py.py.
Referenced by _dict2darray(), _dict2sarray(), _mk_quantifier(), Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DatatypeSort(), DeclareSort(), EnumSort(), FiniteDomainSort(), FP(), Function(), ParamDescrsRef.get_documentation(), ParamDescrsRef.get_kind(), Int(), PropagateFunction(), Real(), RecFunction(), ParamsRef.set(), Fixedpoint.set_predicate_representation(), SolverFor(), String(), and Fixedpoint.update_rule().
ToInt | ( | a | ) |
Return the Z3 expression ToInt(a). >>> x = Real('x') >>> x.sort() Real >>> n = ToInt(x) >>> n ToInt(x) >>> n.sort() Int
Definition at line 3368 of file z3py.py.
Referenced by is_to_int(), and ToInt().
ToReal | ( | a | ) |
Return the Z3 expression ToReal(a). >>> x = Int('x') >>> x.sort() Int >>> n = ToReal(x) >>> n ToReal(x) >>> n.sort() Real
Definition at line 3350 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), SortRef.cast(), is_to_real(), and ToReal().
TransitiveClosure | ( | f | ) |
Given a binary relation R, such that the two arguments have the same sort create the transitive closure relation R+. The transitive closure R+ is a new relation.
Definition at line 11370 of file z3py.py.
TreeOrder | ( | a, | |
index | |||
) |
TryFor | ( | t, | |
ms, | |||
ctx = None |
|||
) |
Return a tactic that applies `t` to a given goal for `ms` milliseconds. If `t` does not terminate in `ms` milliseconds, then it fails.
Definition at line 8488 of file z3py.py.
TupleSort | ( | name, | |
sorts, | |||
ctx = None |
|||
) |
Create a named tuple sort base on a set of underlying sorts Example: >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
Definition at line 5355 of file z3py.py.
Referenced by TupleSort().
UDiv | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) division `self / other`. Use the operator / for signed division. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> UDiv(x, y) UDiv(x, y) >>> UDiv(x, y).sort() BitVec(32) >>> (x / y).sexpr() '(bvsdiv x y)' >>> UDiv(x, y).sexpr() '(bvudiv x y)'
Definition at line 4228 of file z3py.py.
Referenced by BitVecRef.__div__(), BitVecRef.__rdiv__(), and UDiv().
UGE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other >= self`. Use the operator >= for signed greater than or equal to. >>> x, y = BitVecs('x y', 32) >>> UGE(x, y) UGE(x, y) >>> (x >= y).sexpr() '(bvsge x y)' >>> UGE(x, y).sexpr() '(bvuge x y)'
Definition at line 4192 of file z3py.py.
Referenced by BitVecRef.__ge__(), and UGE().
UGT | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other > self`. Use the operator > for signed greater than. >>> x, y = BitVecs('x y', 32) >>> UGT(x, y) UGT(x, y) >>> (x > y).sexpr() '(bvsgt x y)' >>> UGT(x, y).sexpr() '(bvugt x y)'
Definition at line 4210 of file z3py.py.
Referenced by BitVecRef.__gt__(), and UGT().
ULE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other <= self`. Use the operator <= for signed less than or equal to. >>> x, y = BitVecs('x y', 32) >>> ULE(x, y) ULE(x, y) >>> (x <= y).sexpr() '(bvsle x y)' >>> ULE(x, y).sexpr() '(bvule x y)'
Definition at line 4156 of file z3py.py.
Referenced by BitVecRef.__le__(), and ULE().
ULT | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other < self`. Use the operator < for signed less than. >>> x, y = BitVecs('x y', 32) >>> ULT(x, y) ULT(x, y) >>> (x < y).sexpr() '(bvslt x y)' >>> ULT(x, y).sexpr() '(bvult x y)'
Definition at line 4174 of file z3py.py.
Referenced by BitVecRef.__lt__(), and ULT().
Union | ( | * | args | ) |
Create union of regular expressions. >>> re = Union(Re("a"), Re("b"), Re("c")) >>> print (simplify(InRe("d", re))) False
Definition at line 11234 of file z3py.py.
Referenced by ReRef.__add__(), InRe(), and Union().
Unit | ( | a | ) |
Update | ( | a, | |
* | args | ||
) |
Return a Z3 store array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i, v = Ints('i v') >>> s = Update(a, i, v) >>> s.sort() Array(Int, Int) >>> prove(s[i] == v) proved >>> j = Int('j') >>> prove(Implies(i != j, s[j] == a[j])) proved
Definition at line 4739 of file z3py.py.
URem | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) remainder `self % other`. Use the operator % for signed modulus, and SRem() for signed remainder. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> URem(x, y) URem(x, y) >>> URem(x, y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> URem(x, y).sexpr() '(bvurem x y)'
Definition at line 4249 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), SRem(), and URem().
user_prop_created | ( | ctx, | |
cb, | |||
id | |||
) |
user_prop_decide | ( | ctx, | |
cb, | |||
t_ref, | |||
idx_ref, | |||
phase_ref | |||
) |
Definition at line 11527 of file z3py.py.
user_prop_diseq | ( | ctx, | |
cb, | |||
x, | |||
y | |||
) |
Definition at line 11517 of file z3py.py.
user_prop_eq | ( | ctx, | |
cb, | |||
x, | |||
y | |||
) |
user_prop_final | ( | ctx, | |
cb | |||
) |
user_prop_fixed | ( | ctx, | |
cb, | |||
id, | |||
value | |||
) |
Definition at line 11488 of file z3py.py.
user_prop_fresh | ( | ctx, | |
_new_ctx | |||
) |
Definition at line 11474 of file z3py.py.
user_prop_pop | ( | ctx, | |
cb, | |||
num_scopes | |||
) |
user_prop_push | ( | ctx, | |
cb | |||
) |
Var | ( | idx, | |
s | |||
) |
Create a Z3 free variable. Free variables are used to create quantified formulas. A free variable with index n is bound when it occurs within the scope of n+1 quantified declarations. >>> Var(0, IntSort()) Var(0) >>> eq(Var(0, IntSort()), Var(0, BoolSort())) False
Definition at line 1466 of file z3py.py.
Referenced by QuantifierRef.body(), QuantifierRef.children(), get_var_index(), is_pattern(), is_var(), MultiPattern(), QuantifierRef.pattern(), RealVar(), RealVarVector(), substitute_vars(), and Var().
When | ( | p, | |
t, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. >>> t = When(Probe('size') > 2, Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 8782 of file z3py.py.
Referenced by When().
With | ( | t, | |
* | args, | ||
** | keys | ||
) |
Return a tactic that applies tactic `t` using the given configuration options. >>> x, y = Ints('x y') >>> t = With(Tactic('simplify'), som=True) >>> t((x + 1)*(y + 2) == 0) [[2*x + y + x*y == -2]]
Definition at line 8439 of file z3py.py.
Referenced by Goal.prec(), and With().
WithParams | ( | t, | |
p | |||
) |
Return a tactic that applies tactic `t` using the given configuration options. >>> x, y = Ints('x y') >>> p = ParamsRef() >>> p.set("som", True) >>> t = WithParams(Tactic('simplify'), p) >>> t((x + 1)*(y + 2) == 0) [[2*x + y + x*y == -2]]
Definition at line 8453 of file z3py.py.
Referenced by WithParams().
Xor | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 Xor expression. >>> p, q = Bools('p q') >>> Xor(p, q) Xor(p, q) >>> simplify(Xor(p, q)) Not(p == q)
Definition at line 1795 of file z3py.py.
Referenced by Xor().
z3_debug | ( | ) |
Definition at line 62 of file z3py.py.
Referenced by Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), _and_then(), _check_bv_args(), _check_fp_args(), _coerce_expr_merge(), _ctx_from_ast_arg_list(), _dict2darray(), _dict2sarray(), _mk_bin(), _mk_fp_bin(), _mk_fp_bin_norm(), _mk_fp_bin_pred(), _mk_fp_tern(), _mk_fp_unary(), _mk_fp_unary_pred(), _mk_quantifier(), _or_else(), _pb_args_coeffs(), _probe_nary(), _prove_html(), _py2expr(), _solve_using_html(), _to_float_str(), _to_sort_ref(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), Distinct(), EnumSort(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), Intersect(), IsInt(), K(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), OrElse(), ParOr(), ParThen(), QuantifierRef.pattern(), PropagateFunction(), prove(), RatVal(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), simplify(), solve_using(), substitute(), substitute_funs(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Union(), Update(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().
z3_error_handler | ( | c, | |
e | |||
) |
ZeroExt | ( | n, | |
a | |||
) |
Return a bit-vector expression with `n` extra zero-bits. >>> x = BitVec('x', 16) >>> n = ZeroExt(8, x) >>> n.size() 24 >>> n ZeroExt(8, x) >>> n.sort() BitVec(24) >>> v0 = BitVecVal(2, 2) >>> v0 2 >>> v0.size() 2 >>> v = simplify(ZeroExt(6, v0)) >>> v 2 >>> v.size() 8
Definition at line 4385 of file z3py.py.
Referenced by ZeroExt().
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
sat = CheckSatResult(Z3_L_TRUE) |
unknown = CheckSatResult(Z3_L_UNDEF) |
unsat = CheckSatResult(Z3_L_FALSE) |