Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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  FPSortRef
 FP Sorts. More...
 
class  FPRMSortRef
 
class  FPRef
 FP Expressions. More...
 
class  FPRMRef
 
class  FPNumRef
 FP Numerals. More...
 
class  SeqSortRef
 Strings, Sequences and Regular expressions. More...
 
class  SeqRef
 
class  ReSortRef
 Regular expressions. More...
 
class  ReRef
 

Namespaces

 z3py
 

Functions

def z3_debug
 
def enable_trace
 
def disable_trace
 
def get_version_string
 
def get_version
 
def get_full_version
 
def open_log
 
def append_log
 
def to_symbol
 
def z3_error_handler
 
def main_ctx
 
def set_param
 
def reset_params
 
def set_option
 
def get_param
 
def is_ast
 
def eq
 
def is_sort
 
def DeclareSort
 
def is_func_decl
 
def Function
 
def RecFunction
 
def RecAddDefinition
 
def is_expr
 
def is_app
 
def is_const
 
def is_var
 
def get_var_index
 
def is_app_of
 
def If
 
def Distinct
 
def Const
 
def Consts
 
def FreshConst
 
def Var
 
def RealVar
 
def RealVarVector
 
def is_bool
 
def is_true
 
def is_false
 
def is_and
 
def is_or
 
def is_implies
 
def is_not
 
def is_eq
 
def is_distinct
 
def BoolSort
 
def BoolVal
 
def Bool
 
def Bools
 
def BoolVector
 
def FreshBool
 
def Implies
 
def Xor
 
def Not
 
def mk_not
 
def And
 
def Or
 
def is_pattern
 
def MultiPattern
 
def is_quantifier
 
def ForAll
 
def Exists
 
def Lambda
 
def is_arith_sort
 
def is_arith
 
def is_int
 
def is_real
 
def is_int_value
 
def is_rational_value
 
def is_algebraic_value
 
def is_add
 
def is_mul
 
def is_sub
 
def is_div
 
def is_idiv
 
def is_mod
 
def is_le
 
def is_lt
 
def is_ge
 
def is_gt
 
def is_is_int
 
def is_to_real
 
def is_to_int
 
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
 
def ToInt
 
def IsInt
 
def Sqrt
 
def Cbrt
 
def is_bv_sort
 
def is_bv
 
def is_bv_value
 
def BV2Int
 
def Int2BV
 
def BitVecSort
 
def BitVecVal
 
def BitVec
 
def BitVecs
 
def Concat
 
def Extract
 
def ULE
 
def ULT
 
def UGE
 
def UGT
 
def UDiv
 
def URem
 
def SRem
 
def LShR
 
def RotateLeft
 
def RotateRight
 
def SignExt
 
def ZeroExt
 
def RepeatBitVec
 
def BVRedAnd
 
def BVRedOr
 
def BVAddNoOverflow
 
def BVAddNoUnderflow
 
def BVSubNoOverflow
 
def BVSubNoUnderflow
 
def BVSDivNoOverflow
 
def BVSNegNoOverflow
 
def BVMulNoOverflow
 
def BVMulNoUnderflow
 
def is_array
 
def is_const_array
 
def is_K
 
def is_map
 
def is_default
 
def get_map_func
 
def ArraySort
 
def Array
 
def Update
 
def Default
 
def Store
 
def Select
 
def Map
 
def K
 
def Ext
 
def SetHasSize
 
def is_select
 
def is_store
 
def SetSort
 Sets. More...
 
def EmptySet
 
def FullSet
 
def SetUnion
 
def SetIntersect
 
def SetAdd
 
def SetDel
 
def SetComplement
 
def SetDifference
 
def IsMember
 
def IsSubset
 
def CreateDatatypes
 
def TupleSort
 
def DisjointSum
 
def EnumSort
 
def args2params
 
def Model
 
def is_as_array
 
def get_as_array_func
 
def SolverFor
 
def SimpleSolver
 
def FiniteDomainSort
 
def is_finite_domain_sort
 
def is_finite_domain
 
def FiniteDomainVal
 
def is_finite_domain_value
 
def AndThen
 
def Then
 
def OrElse
 
def ParOr
 
def ParThen
 
def ParAndThen
 
def With
 
def WithParams
 
def Repeat
 
def TryFor
 
def tactics
 
def tactic_description
 
def describe_tactics
 
def is_probe
 
def probes
 
def probe_description
 
def describe_probes
 
def FailIf
 
def When
 
def Cond
 
def simplify
 Utils. More...
 
def help_simplify
 
def simplify_param_descrs
 
def substitute
 
def substitute_vars
 
def Sum
 
def Product
 
def AtMost
 
def AtLeast
 
def PbLe
 
def PbGe
 
def PbEq
 
def solve
 
def solve_using
 
def prove
 
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
 
def is_fprm_sort
 
def RoundNearestTiesToEven
 
def RNE
 
def RoundNearestTiesToAway
 
def RNA
 
def RoundTowardPositive
 
def RTP
 
def RoundTowardNegative
 
def RTN
 
def RoundTowardZero
 
def RTZ
 
def is_fprm
 
def is_fprm_value
 
def is_fp
 
def is_fp_value
 
def FPSort
 
def fpNaN
 
def fpPlusInfinity
 
def fpMinusInfinity
 
def fpInfinity
 
def fpPlusZero
 
def fpMinusZero
 
def fpZero
 
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 SeqSort
 
def is_seq
 
def is_string
 
def is_string_value
 
def StringVal
 
def String
 
def SubString
 
def SubSeq
 
def Strings
 
def Empty
 
def Full
 
def Unit
 
def PrefixOf
 
def SuffixOf
 
def Contains
 
def Replace
 
def IndexOf
 
def IndexOf
 
def LastIndexOf
 
def Length
 
def StrToInt
 
def IntToStr
 
def Re
 
def ReSort
 
def is_re
 
def InRe
 
def Union
 
def Intersect
 
def Plus
 
def Option
 
def Complement
 
def Star
 
def Loop
 
def Range
 
def PartialOrder
 
def LinearOrder
 
def TreeOrder
 
def PiecewiseLinearOrder
 
def TransitiveClosure
 

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)
 
 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
 Floating-Point Arithmetic. More...
 
int _dflt_fpsort_ebits = 11
 
int _dflt_fpsort_sbits = 53