Python API¶
Import the stp package. See The 3.x API (C++, C and Python) for examples and API conventions.
Classes¶
- stp.Version
- stp.Kind
- stp.SortKind
- stp.RoundingMode
- stp.UnknownReason
- stp.ErrorCode
- stp.Tier
- stp.Option
- stp.Error
- stp.ArgumentError
- stp.SortMismatch
- stp.DoesNotFit
- stp.NotAValue
- stp.NoModel
- stp.Unsupported
- stp.OptionError
- stp.UnknownOption
- stp.ParseError
- stp.StateError
- stp.ResourceError
- stp.InternalError
- stp.TermManager
- stp.SortRef
- stp.BoolSortRef
- stp.BitVecSortRef
- stp.FPSortRef
- stp.RMSortRef
- stp.RealSortRef
- stp.ArraySortRef
- stp.FuncSortRef
- stp.UninterpretedSortRef
- stp.ExprRef
- stp.BoolRef
- stp.BoolNumRef
- stp.BitVecRef
- stp.BitVecNumRef
- stp.FPRef
- stp.FPNumRef
- stp.RMRef
- stp.RMNumRef
- stp.RealRef
- stp.RatNumRef
- stp.ArrayRef
- stp.ArrayNumRef
- stp.FuncRef
- stp.FuncEntry
- stp.FuncInterp
- stp.UninterpretedRef
- stp.UninterpretedNumRef
- stp.OptionInfo
- stp.Options
- stp.CheckSatResult
- stp.EntailmentResult
- stp.Statistics
- stp.Solver
- stp.Model
Functions¶
- stp.version
- stp.capabilities
- stp.capability
- stp.has_sat_backend
- stp.sat_backends
- stp.set_internal_error_policy
- stp.get_internal_error_policy
- stp.main_tm
- stp.set_main_tm
- stp.BoolSort
- stp.BitVecSort
- stp.FPSort
- stp.Float16
- stp.Float32
- stp.Float64
- stp.Float128
- stp.FloatHalf
- stp.FloatSingle
- stp.FloatDouble
- stp.FloatQuadruple
- stp.RoundingModeSort
- stp.RealSort
- stp.ArraySort
- stp.FuncSort
- stp.DeclareSort
- stp.FreshSort
- stp.Bool
- stp.Bools
- stp.BoolVal
- stp.BitVec
- stp.BitVecs
- stp.BitVecVal
- stp.FP
- stp.FPs
- stp.FPVal
- stp.fpFromBits
- stp.fpNaN
- stp.fpPlusInfinity
- stp.fpMinusInfinity
- stp.fpInfinity
- stp.fpPlusZero
- stp.fpMinusZero
- stp.fpZero
- stp.fpFP
- stp.RNE
- stp.RNA
- stp.RTP
- stp.RTN
- stp.RTZ
- stp.RoundNearestTiesToEven
- stp.RoundNearestTiesToAway
- stp.RoundTowardPositive
- stp.RoundTowardNegative
- stp.RoundTowardZero
- stp.RMVal
- stp.Real
- stp.Reals
- stp.RealVal
- stp.Q
- stp.Array
- stp.K
- stp.ArrayFromBytes
- stp.Function
- stp.Const
- stp.Consts
- stp.FreshConst
- stp.FreshBool
- stp.FreshBitVec
- stp.And
- stp.Or
- stp.Not
- stp.Xor
- stp.Implies
- stp.If
- stp.Distinct
- stp.Sum
- stp.Product
- stp.ULT
- stp.ULE
- stp.UGT
- stp.UGE
- stp.UDiv
- stp.URem
- stp.SDiv
- stp.SRem
- stp.SMod
- stp.LShR
- stp.SLT
- stp.SLE
- stp.SGT
- stp.SGE
- stp.Extract
- stp.Bit
- stp.BoolToBV1
- stp.BV1ToBool
- stp.Concat
- stp.ZeroExt
- stp.SignExt
- stp.RepeatBitVec
- stp.RepeatBV
- stp.RotateLeft
- stp.RotateRight
- stp.BVComp
- stp.BVNand
- stp.BVNor
- stp.BVXnor
- stp.BVRedAnd
- stp.BVRedOr
- stp.bvuaddo
- stp.bvsaddo
- stp.bvumulo
- stp.bvsmulo
- stp.bvusubo
- stp.bvssubo
- stp.bvnego
- stp.bvsdivo
- stp.BVAddNoOverflow
- stp.BVAddNoUnderflow
- stp.BVSubNoOverflow
- stp.BVSubNoUnderflow
- stp.BVMulNoOverflow
- stp.BVMulNoUnderflow
- stp.BVSNegNoOverflow
- stp.BVSDivNoOverflow
- stp.Select
- stp.Store
- stp.Update
- stp.Default
- stp.fpAbs
- stp.fpNeg
- stp.fpAdd
- stp.fpSub
- stp.fpMul
- stp.fpDiv
- stp.fpFMA
- stp.fpSqrt
- stp.fpRem
- stp.fpRoundToIntegral
- stp.fpMin
- stp.fpMax
- stp.fpEQ
- stp.fpNEQ
- stp.fpLT
- stp.fpLEQ
- stp.fpGT
- stp.fpGEQ
- stp.fpIsNaN
- stp.fpIsInf
- stp.fpIsZero
- stp.fpIsNormal
- stp.fpIsSubnormal
- stp.fpIsNegative
- stp.fpIsPositive
- stp.fpToFP
- stp.fpFPToFP
- stp.fpBVToFP
- stp.fpSignedToFP
- stp.fpUnsignedToFP
- stp.fpRealToFP
- stp.fpToSBV
- stp.fpToUBV
- stp.fpToIEEEBV
- stp.fpToReal
- stp.simplify
- stp.substitute
- stp.is_true
- stp.is_false
- stp.is_expr
- stp.is_app
- stp.is_const
- stp.is_symbol
- stp.is_value
- stp.is_bv
- stp.is_bv_value
- stp.is_fp
- stp.is_fp_value
- stp.is_real
- stp.is_rational_value
- stp.is_array
- stp.is_bool
- stp.is_func_decl
- stp.is_rm
- stp.is_sort
- stp.SolverFor
- stp.SimpleSolver
- stp.solve
- stp.prove
- stp.parse_smt2_string
- stp.parse_smt2_file
- stp.stp
- stp.solver_scope
- stp.current_solver
- stp.add
- stp.check
- stp.model
