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)
 
 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)
 
 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")
 
 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 (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)
 
 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)
 
 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, 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)