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