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)