Skip to index filter Skip to main content
Storm logo stormpystormpy
  • Getting Started
  • Documentation
    • Advanced Examples
    • Getting Started with Pycarl
  • API
  • Extensions API
  • Developer API
  • Storm
Search the documentation
stormpy
  • Getting Started
  • Documentation
    • Advanced Examples
    • Getting Started with Pycarl
  • API
  • Extensions API
  • Developer API
  • Storm
  • stormpy
  • Change appearance
    • Change appearance
    • Light
    • Dark
    • Automatic
  Index
Index

Contents:

  • Installation
  • Getting Started
  • Advanced Examples
    • Analysis
    • Building Models
    • Discrete-time Markov chains (DTMCs)
    • Markov decision processes (MDPs)
    • Continuous-time Markov chains (CTMCs)
    • Markov automata (MAs)
    • Engines
    • Exploring Models
    • Working with Simulators
    • Reward Models
    • Working with Schedulers
    • Working with Shortest Paths
    • Parametric Models
    • Dynamic Fault Trees
    • Generalized Stochastic Petri Nets
    • Storm(py) Information
  • Getting Started with Pycarl
  • Developer information
  • Contributors
  • API Documentation
    • stormpy
      • build_model
      • build_model_from_drn
      • build_model_from_explicit
      • build_model_from_umb
      • build_symbolic_model
      • create_filter
      • create_filter_initial_states
      • filter_initial_states
      • instantiate_constants
      • model_checking
      • parse_jani_model
      • parse_jani_model_from_string
      • parse_prism_program
      • parse_properties
      • parse_property
      • BuilderOptions
      • CheckResult
      • Engine
      • Environment
      • ExplicitModelCheckerHint
      • Interval
      • ModelCheckerHint
      • Polynomial
      • Rational
      • RationalFunction
      • RationalFunctionCoefficient
      • RationalInterval
      • RawPolynomial
      • UncertaintyResolutionMode
    • stormpy.analysis
      • compute_expected_number_of_visits
      • compute_prob01_states
      • compute_steady_state_distribution
      • get_maximal_end_components
      • shortest_path
      • topological_sort
      • MaximalEndComponent
      • MaximalEndComponentDecomposition
      • Path
    • stormpy.datastructures
      • build_sparse_matrix
      • BitVector
      • Distribution
      • JsonContainer
      • SparseMatrix
      • SparseMatrixBuilder
      • SparseMatrixEntry
      • SparseMatrixRows
    • stormpy.environments
      • default
      • exact
      • sound
      • ConditionalAlgorithmSetting
      • ConditionalModelCheckerEnvironment
      • CuddDdManagerEnvironment
      • CuddReorderingTechnique
      • DdEnvironment
      • Environment
      • EquationSolverType
      • ExplorationEnvironment
      • MinMaxMethod
      • MinMaxSolverEnvironment
      • ModelCheckerEnvironment
      • MultiObjectiveEncodingType
      • MultiObjectiveMethod
      • MultiObjectiveModelCheckerEnvironment
      • MultiObjectivePrecisionType
      • NativeLinearEquationSolverMethod
      • NativeSolverEnvironment
      • NextStateHeuristic
      • PrecomputationType
      • SolverEnvironment
      • SteadyStateDistributionAlgorithm
      • SylvanDdManagerEnvironment
    • stormpy.exceptions
      • StormError
      • StormWarning
    • stormpy.expressions
      • Expression
      • ExpressionManager
      • ExpressionParser
      • ExpressionType
      • OperatorType
      • Variable
    • stormpy.info
      • storm_build_info
      • storm_build_type
      • storm_development_version
      • storm_directory
      • storm_exact_use_cln
      • storm_from_system
      • storm_full_version
      • storm_long_version
      • storm_origin_info
      • storm_ratfunc_use_cln
      • storm_version
    • stormpy.io
      • export_jani_to_file
      • export_to_drn
      • export_to_umb
      • import_umb
      • instantiate_constants
      • parse_jani_model
      • parse_jani_model_from_string
      • parse_prism_program
      • sparse_model_to_umb
      • umb_to_archive
      • ArrayType
      • BasicType
      • BoundedType
      • ClockType
      • CompressionMode
      • ContinuousType
      • DirectEncodingExporterOptions
      • DirectEncodingParserOptions
      • ExplicitModelParserOptions
      • JaniAssignment
      • JaniAutomaton
      • JaniConstant
      • JaniEdge
      • JaniEdgeDestination
      • JaniLocation
      • JaniModel
      • JaniModelType
      • JaniOrderedAssignments
      • JaniTemplateEdge
      • JaniTemplateEdgeDestination
      • JaniType
      • JaniVariable
      • JaniVariableSet
      • PrismAssignment
      • PrismBooleanVariable
      • PrismCommand
      • PrismConstant
      • PrismIntegerVariable
      • PrismLabel
      • PrismModelType
      • PrismModule
      • PrismProgram
      • PrismRewardModel
      • PrismUpdate
      • PrismVariable
      • SymbolicModelDescription
      • UmbExportOptions
      • UmbExportValueType
      • UmbImportOptions
      • UmbImportValueType
      • UmbModel
    • stormpy.logic
      • parse_properties
      • parse_property
      • AtomicExpressionFormula
      • AtomicLabelFormula
      • BinaryBooleanOperatorType
      • BinaryBooleanStateFormula
      • BinaryPathFormula
      • BinaryStateFormula
      • BooleanLiteralFormula
      • BoundedUntilFormula
      • ComparisonType
      • ConditionalFormula
      • CumulativeRewardFormula
      • DiscountedCumulativeRewardFormula
      • DiscountedTotalRewardFormula
      • EventuallyFormula
      • Formula
      • GameFormula
      • GloballyFormula
      • InstantaneousRewardFormula
      • LongRunAverageOperatorFormula
      • LongRunAverageRewardFormula
      • MultiObjectiveFormula
      • OperatorFormula
      • OptimizationDirection
      • PathFormula
      • ProbabilityOperatorFormula
      • Property
      • RewardOperatorFormula
      • StateFormula
      • TimeOperatorFormula
      • UnaryBooleanStateFormula
      • UnaryPathFormula
      • UnaryStateFormula
      • UntilFormula
    • stormpy.models
      • ChoiceLabeling
      • ChoiceOrigins
      • DdType
      • JaniChoiceOrigins
      • MemoryStructure
      • MemoryStructureBuilder
      • ModelType
      • PrismChoiceOrigins
      • Scheduler
      • SchedulerChoice
      • SimpleValuation
      • SparseCtmc
      • SparseDtmc
      • SparseMA
      • SparseMdp
      • SparseModel
      • SparseModelAction
      • SparseModelActions
      • SparseModelComponents
      • SparseModelState
      • SparseModelStates
      • SparsePomdp
      • SparseRewardModel
      • SparseSmg
      • StateLabeling
      • SymbolicCtmc
      • SymbolicDtmc
      • SymbolicMA
      • SymbolicMdp
      • SymbolicModel
      • SymbolicRewardModel
      • ValuationClassDescription
      • ValuationDescriptionBuilder
      • Valuations
      • ValuationTransformer
    • stormpy.numbers
      • clear_pools
      • is_infinity
      • is_negative_infinity
      • variable_with_name
      • Integer
      • Interval
      • Polynomial
      • Rational
      • RationalFunction
      • RationalFunctionCoefficient
      • RationalInterval
      • RawPolynomial
      • Variable
    • stormpy.plotting
      • plot_convex_pareto_curve_demo
      • prepare_multiobjective_result_for_plotting
    • stormpy.results
      • AggregatedValue
      • BoundedValue
      • CheckResult
      • ExplicitParetoCurveCheckResult
      • ExplicitQualitativeCheckResult
      • ExplicitQuantitativeCheckResult
      • FilterType
      • HybridQuantitativeCheckResult
      • ParetoCurveCheckResult
      • QualitativeCheckResult
      • QuantitativeCheckResult
      • SolutionBounds
      • SymbolicQualitativeCheckResult
      • SymbolicQuantitativeCheckResult
    • stormpy.simulator
      • create_simulator
      • PrismSimulator
      • Simulator
      • SimulatorActionMode
      • SimulatorObservationMode
      • SparseSimulator
    • stormpy.transformations
      • add_uncertainty
      • build_submodel
      • eliminate_non_markovian_chains
      • perform_bisimulation
      • set_state_valuations
      • transform_to_discrete_time_model
      • transform_to_sparse_model
      • BisimulationOptions
      • BisimulationType
      • EliminationLabelBehavior
      • QuotientFormat
      • StateLabelPreservation
      • SubsystemBuilderOptions
      • SubsystemBuilderReturnType
  • Extensions API Documentation
    • stormpy.dft
      • analyze_dft
      • build_model
      • check_dft_validity
      • compute_relevant_events
      • export_dft_json_file
      • export_dft_json_string
      • load_dft_galileo_file
      • load_dft_json_file
      • load_dft_json_string
      • modules
      • modules_json
      • prepare_for_analysis
      • AnalysisEnvironment
      • ApproximationHeuristic
      • DFT
      • DFTBE
      • DFTDependency
      • DFTElement
      • DFTElementType
      • DftEnvironment
      • DftIndependentModule
      • DftInstantiator
      • DFTSimulator
      • DFTState
      • DftSymmetries
      • ModelBuilderEnvironment
      • RelevantEvents
      • SimulationStepResult
      • SimulationTraceResult
      • TransformationEnvironment
    • stormpy.gspn
      • build_jani_model
      • export_gspn_pnml_file
      • export_gspn_pnpro_file
      • load_gspn_file
      • GSPN
      • GspnBuilder
      • ImmediateTransition
      • LayoutInfo
      • Place
      • TimedTransition
      • Transition
      • TransitionPartition
    • stormpy.pars
      • check_feasibility
      • compute_extremal_value
      • create_region
      • gather_derivatives
      • parse_region
      • verify
      • ConstraintCollector
      • FeasibilityMethod
      • FeasibilityResult
      • FeasibilitySynthesisResult
      • ModelInstantiator
      • ParameterRegion
      • RegionCheckEngine
      • RegionResult
    • stormpy.pomdp
      • apply_unknown_fsc
      • create_iterative_policy_search
      • create_memory
      • create_monitor_verifier
      • create_nondeterministic_belief_tracker
      • create_observation_trace_unfolder
      • make_canonic
      • make_simple
      • prepare_for_qualitative_search
      • unfold_memory
      • verify_with_belief_discretization
      • verify_with_belief_unfolding
      • BeliefBasedModelCheckerResult
      • BeliefBasedModelCheckerStatistics
      • BeliefSupportTracker
      • ExplorationQueueOrder
      • IterativePolicySearch
      • MonitorVerifier
      • NondeterministicBeliefTracker
      • ObservationBasedFiniteStateController
      • ObservationTraceUnfolder
      • PomdpFscApplicationMode
      • PomdpMemory
      • PomdpMemoryPattern
      • SparseBeliefState
      • WinningRegion
      • WinningRegionQueryInterface
  • Developer API Documentation
    • stormpy.developer
      • build_explicit_drn_model
      • build_explicit_model
      • build_sparse_model
      • build_subsystem
      • build_symbolic_model
      • compute_all_transient_probabilities
      • compute_all_until_probabilities
      • compute_expected_visiting_times_with_sparse_engine
      • compute_steady_state_distribution_with_sparse_engine
      • create_weight_vector_checker
      • eliminate_non_markovian_chains
      • export_sparse_model_as_drn
      • get_exact_environment
      • get_log_level
      • get_reachable_states
      • get_sound_environment
      • install_signal_handler
      • make_explicit_model_builder
      • parse_constant_definition_string
      • parse_jani_model
      • parse_jani_model_from_string
      • parse_program
      • parse_properties
      • parse_properties_for_jani_model
      • parse_properties_for_prism_program
      • parse_properties_for_symbolic_model_description
      • perform_bisimulation_minimization
      • perform_multi_objective_model_checking
      • perform_prob01
      • perform_prob01_max
      • perform_prob01_min
      • reset_timeout_alarm
      • set_from_exploded_string
      • set_log_level
      • set_timeout_alarm
      • substitute_constants_in_properties
      • transform_continuous_to_discrete_time_sparse_model
      • transform_symbolic_to_sparse_model
      • verify_with_dd_engine
      • verify_with_hybrid_engine
      • verify_with_sparse_engine
      • ActionMask
      • AddUncertainty
      • BuilderOptions
      • CheckTask
      • Choice
      • DdBisimulationOptions
      • DiscreteTimePrismProgramSimulator
      • DiscreteTimeSparseModelSimulator
      • EndComponentEliminator
      • EndComponentEliminatorReturnType
      • EnvironmentBuilder
      • EnvironmentFactory
      • ExactEnvironmentFactory
      • ExplicitModelBuilder
      • ExplicitModelBuilderOptions
      • ExplicitStateLookup
      • ExplorationOrder
      • FlatSet
      • InitialPartitionMode
      • LogLevel
      • ModelReference
      • PcaaWeightVectorChecker
      • RefinementMode
      • ReuseMode
      • SchedulerClass
      • SchedulerMemoryPattern
      • SignatureMode
      • SmtCheckResult
      • SMTMinimalLabelSetGenerator
      • SMTMinimalLabelSetGeneratorCexInput
      • SMTMinimalLabelSetGeneratorOptions
      • SMTMinimalLabelSetGeneratorStats
      • SmtSolver
      • SmtSolverFactory
      • SoundEnvironmentFactory
      • StateValuationFunctionMask
      • Z3SmtSolver
      • Z3SmtSolverFactory
    • stormpy.developer.info
      • StormVersion
    • stormpy.developer.logic
    • stormpy.developer.storage
      • collect_model_information
      • get_topological_sort
      • import_umb
      • parameters_of_model
      • sparse_model_from_umb
      • sparse_model_to_umb
      • to_archive
      • to_value_type
      • Add
      • AddIterator
      • Bdd
      • Dd
      • DdManager
      • DdMetaVariable
      • DdMetaVariableType
      • DiceStringVisitor
      • Halfspace
      • ItemLabeling
      • JaniInformationObject
      • JaniLocationExpander
      • JaniScopeChanger
      • JsonExporter
      • MemoryStructureProduct
      • ModelBase
      • OverlappingGuardAnalyser
      • Polytope
      • RewardAccumulationEliminationVisitor
      • SparseModelMemoryProductReverseData
      • Valuation
    • stormpy.developer.utility
      • sharpen
      • MatrixFormat
      • milliseconds
      • ShortestPathsGenerator
    • stormpy.dft.developer
      • analyze_dft
      • build_model
      • compute_dependency_conflicts
      • compute_relevant_events
      • export_dft_json_file
      • get_parameters
      • has_potential_modeling_issues
      • is_well_formed
      • load_dft_galileo_file
      • load_dft_json_file
      • transform_dft
      • DftIndependentModule
      • DFTStateGenerationInfo
      • DFTTraceSimulator
      • ExplicitDFTModelBuilder
      • FailableElement
      • FailableElements
      • FailableIterator
      • RandomGenerator
    • stormpy.pars.developer
      • check_feasibility
      • initialize_region_model_checker
      • initialize_region_refinement_checker
      • parse_region
      • verify
      • GraphPreservationStatus
      • RegionModelChecker
      • RegionRefinementChecker
      • RegionResultHypothesis
      • RegionSplitEstimateKind
      • SparseDtmcParameterLiftingModelChecker
      • SparseInstantiationModelChecker
      • SparseMdpParameterLiftingModelChecker
      • SparseParametricModelSimplifier
    • stormpy.pomdp.developer
      • create_iterative_policy_search
      • prepare_pomdp_for_qualitative_search
      • verify_with_belief_discretization
      • verify_with_belief_unfolding
      • ApplyFiniteSchedulerToPomdp
      • BeliefBasedModelCheckerOptions
      • BinaryPomdpTransformer
      • GenerateMonitorVerifier
      • GenerateMonitorVerifierOptions
      • MakePOMDPCanonic
      • MemlessSearchOptions
      • NondeterministicBeliefTrackerOptions
      • ObservationTraceUnfolderOptions
      • PomdpMemoryBuilder
      • PomdpMemoryUnfolder
      • PomdpTransformationResult
    • stormpy.numbers.developer
      • abs
      • carl_version
      • ceil
      • clear_monomial_pool
      • clear_variable_pool
      • create_monomial
      • div
      • floor
      • has_cln
      • isInteger
      • pow
      • quotient
      • BoundType
      • Monomial
      • VariableType
      • NoPicklingSupport
    • stormpy.numbers.developer.convert
      • convert_to_cln
      • convert_to_gmp
    • stormpy.numbers.developer.formula
      • FormulaType
      • Relation
    • stormpy.numbers.developer.parse
      • deserialize
      • ParserError
    • stormpy.numbers.developer.cln
      • abs
      • ceil
      • create_factorized_polynomial
      • denominator
      • div
      • expand
      • floor
      • isInteger
      • numerator
      • pow
      • quotient
      • Factorization
      • Integer
      • Interval
      • RationalFunction
      • Term
    • stormpy.numbers.developer.cln.formula
      • Constraint
      • Formula
      • SimpleConstraint
      • SimpleConstraintRatFunc
    • stormpy.numbers.developer.gmp
      • abs
      • ceil
      • create_factorized_polynomial
      • denominator
      • div
      • expand
      • floor
      • isInteger
      • numerator
      • pow
      • quotient
      • Factorization
      • FactorizedPolynomial
      • FactorizedRationalFunction
      • Polynomial
      • RationalFunction
      • Term
    • stormpy.numbers.developer.gmp.formula
      • Constraint
      • Formula
      • SimpleConstraint
      • SimpleConstraintRatFunc
  1. Start
  2. Developer API Documentation
  3. stormpy.developer
  4. SmtSolverFactory

SmtSolverFactory¶

Warning

The stormpy developer API is internal and can be subject to change.

class SmtSolverFactory¶

Bases: pybind11_object

Factory for creating SMT Solvers

  On this page
  • SmtSolverFactory
    • SmtSolverFactory
  • Previous SmtSolver
  • Next SoundEnvironmentFactory
  • Documentation
  • Package
  • Repository
  • Issues
stormpy
  • 2016-2026 Storm Developers
Built with Sphinx 9.2.0 and Nefertiti 0.9.11