Z3
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  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

 z3py
 

Functions

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
 
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
 
def DeclareTypeVar
 
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
 
def Distinct (args)
 
def Const (name, sort)
 
def Consts (names, sort)
 
def FreshConst
 
def Var (idx, s)
 
def RealVar
 
def RealVarVector
 
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
 
def BoolVal
 
def Bool
 
def Bools
 
def BoolVector
 
def FreshBool
 
def Implies
 
def Xor
 
def Not
 
def mk_not (a)
 
def And (args)
 
def Or (args)
 
def is_pattern (a)
 
def MultiPattern (args)
 
def is_quantifier (a)
 
def ForAll
 
def Exists
 
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
 
def RealSort
 
def IntVal
 
def RealVal
 
def RatVal
 
def Q
 
def Int
 
def Ints
 
def IntVector
 
def FreshInt
 
def Real
 
def Reals
 
def RealVector
 
def FreshReal
 
def ToReal (a)
 
def ToInt (a)
 
def IsInt (a)
 
def Sqrt
 
def Cbrt
 
def is_bv_sort (s)
 
def is_bv (a)
 
def is_bv_value (a)
 
def BV2Int
 
def Int2BV (a, num_bits)
 
def BitVecSort
 
def BitVecVal
 
def BitVec
 
def BitVecs
 
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
 
def TupleSort
 
def DisjointSum
 
def EnumSort
 
def args2params
 
def Model
 
def is_as_array (n)
 
def get_as_array_func (n)
 
def SolverFor
 
def SimpleSolver
 
def FiniteDomainSort
 
def is_finite_domain_sort (s)
 
def is_finite_domain (a)
 
def FiniteDomainVal
 
def is_finite_domain_value (a)
 
def AndThen (ts, ks)
 
def Then (ts, ks)
 
def OrElse (ts, ks)
 
def ParOr (ts, ks)
 
def ParThen
 
def ParAndThen
 
def With (t, args, keys)
 
def WithParams (t, p)
 
def Repeat
 
def TryFor
 
def tactics
 
def tactic_description
 
def describe_tactics ()
 
def is_probe (p)
 
def probes
 
def probe_description
 
def describe_probes ()
 
def FailIf
 
def When
 
def Cond
 
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
 
def solve (args, keywords)
 
def solve_using (s, args, keywords)
 
def prove (claim, show=False, keywords)
 
def parse_smt2_string
 
def parse_smt2_file
 
def get_default_rounding_mode
 
def set_default_rounding_mode
 
def get_default_fp_sort
 
def set_default_fp_sort
 
def Float16
 
def FloatHalf
 
def Float32
 
def FloatSingle
 
def Float64
 
def FloatDouble
 
def Float128
 
def FloatQuadruple
 
def is_fp_sort (s)
 
def is_fprm_sort (s)
 
def RoundNearestTiesToEven
 
def RNE
 
def RoundNearestTiesToAway
 
def RNA
 
def RoundTowardPositive
 
def RTP
 
def RoundTowardNegative
 
def RTN
 
def RoundTowardZero
 
def RTZ
 
def is_fprm (a)
 
def is_fprm_value (a)
 
def is_fp (a)
 
def is_fp_value (a)
 
def FPSort
 
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
 
def FP
 
def FPs
 
def fpAbs
 
def fpNeg
 
def fpAdd
 
def fpSub
 
def fpMul
 
def fpDiv
 
def fpRem
 
def fpMin
 
def fpMax
 
def fpFMA
 
def fpSqrt
 
def fpRoundToIntegral
 
def fpIsNaN
 
def fpIsInf
 
def fpIsZero
 
def fpIsNormal
 
def fpIsSubnormal
 
def fpIsNegative
 
def fpIsPositive
 
def fpLT
 
def fpLEQ
 
def fpGT
 
def fpGEQ
 
def fpEQ
 
def fpNEQ
 
def fpFP
 
def fpToFP
 
def fpBVToFP
 
def fpFPToFP
 
def fpRealToFP
 
def fpSignedToFP
 
def fpUnsignedToFP
 
def fpToFPUnsigned
 
def fpToSBV
 
def fpToUBV
 
def fpToReal
 
def fpToIEEEBV
 
def StringSort
 
def CharSort
 
def SeqSort (s)
 
def CharVal
 
def CharFromBv (bv)
 
def CharToBv
 
def CharToInt
 
def CharIsDigit
 
def is_seq (a)
 
def is_string (a)
 
def is_string_value (a)
 
def StringVal
 
def String
 
def Strings
 
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
 
def LastIndexOf (s, substr)
 
def Length (s)
 
def StrToInt (s)
 
def IntToStr (s)
 
def StrToCode (s)
 
def StrFromCode (c)
 
def Re
 
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
 
def Range
 
def Diff
 
def AllChar
 
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, n, dep, 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, idx, phase)
 
def PropagateFunction (name, sig)
 

Variables

 Z3_DEBUG = __debug__
 
 _main_ctx = None
 
tuple sat = CheckSatResult(Z3_L_TRUE)
 
tuple unsat = CheckSatResult(Z3_L_FALSE)
 
tuple unknown = CheckSatResult(Z3_L_UNDEF)
 
dictionary _on_models = {}
 
tuple _on_model_eh = on_model_eh_type(_global_on_model)
 
 _dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
 Floating-Point Arithmetic. More...
 
int _dflt_fpsort_ebits = 11
 
int _dflt_fpsort_sbits = 53
 
tuple _ROUNDING_MODES
 
 _my_hacky_class = None
 
tuple _on_clause_eh = Z3_on_clause_eh(on_clause_eh)
 
 _prop_closures = None
 
tuple _user_prop_push = Z3_push_eh(user_prop_push)
 
tuple _user_prop_pop = Z3_pop_eh(user_prop_pop)
 
tuple _user_prop_fresh = Z3_fresh_eh(user_prop_fresh)
 
tuple _user_prop_fixed = Z3_fixed_eh(user_prop_fixed)
 
tuple _user_prop_created = Z3_created_eh(user_prop_created)
 
tuple _user_prop_final = Z3_final_eh(user_prop_final)
 
tuple _user_prop_eq = Z3_eq_eh(user_prop_eq)
 
tuple _user_prop_diseq = Z3_eq_eh(user_prop_diseq)
 
tuple _user_prop_decide = Z3_decide_eh(user_prop_decide)