Z3
Loading...
Searching...
No Matches
z3py.py File Reference

Go to the source code of this file.

Data Structures

class  Context
class  Z3PPObject
 ASTs base class. More...
class  AstRef
class  SortRef
class  TypeVarRef
class  FuncDeclRef
 Function Declarations. More...
class  ExprRef
 Expressions. More...
class  BoolSortRef
 Booleans. More...
class  BoolRef
class  PatternRef
 Patterns. More...
class  QuantifierRef
 Quantifiers. More...
class  ArithSortRef
 Arithmetic. More...
class  ArithRef
class  IntNumRef
class  RatNumRef
class  AlgebraicNumRef
class  BitVecSortRef
 Bit-Vectors. More...
class  BitVecRef
class  BitVecNumRef
class  ArraySortRef
 Arrays. More...
class  ArrayRef
class  Datatype
class  ScopedConstructor
class  ScopedConstructorList
class  DatatypeSortRef
class  DatatypeRef
class  ParamsRef
 Parameter Sets. More...
class  ParamDescrsRef
class  Goal
class  AstVector
class  AstMap
class  FuncEntry
class  FuncInterp
class  ModelRef
class  Statistics
 Statistics. More...
class  CheckSatResult
class  Solver
class  Fixedpoint
 Fixedpoint. More...
class  FiniteDomainSortRef
class  FiniteDomainRef
class  FiniteDomainNumRef
class  OptimizeObjective
 Optimize. More...
class  Optimize
class  ApplyResult
class  Simplifier
class  Tactic
class  Probe
class  ParserContext
class  FPSortRef
class  FPRMSortRef
class  FPRef
class  FPRMRef
class  FPNumRef
class  SeqSortRef
 Strings, Sequences and Regular expressions. More...
class  CharSortRef
class  SeqRef
class  CharRef
class  ReSortRef
class  ReRef
class  OnClause
class  PropClosures
class  UserPropagateBase

Namespaces

namespace  z3py

Functions

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