Data Structures | Namespaces | Functions | Variables
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  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  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




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


 Z3_DEBUG = __debug__
 sat = CheckSatResult(Z3_L_TRUE)
 unsat = CheckSatResult(Z3_L_FALSE)
 unknown = CheckSatResult(Z3_L_UNDEF)