SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Namespaces | Data Structures | Typedefs | Enumerations | Functions | Variables
smtrat Namespace Reference

Class to create the formulas for axioms. More...

Namespaces

 analyzer
 
 cad
 
 cadcells
 A framework for sample-based CAD algorithms.
 
 compile_information
 Compile time generated information about compiler and system version.
 
 covering_ng
 
 execution
 
 expression
 
 fmplex
 
 groebner
 
 helper
 
 icp
 
 internal
 
 lra
 
 lve
 
 maxsmt
 Contains strategy implementations for max SMT computations.
 
 mcsat
 
 onecellcad
 
 options_detail
 
 parseformula
 
 parser
 
 qe
 
 resource
 
 sat
 
 settings
 
 statistics
 
 subtropical
 Implements data structures and encodings for the subtropical method.
 
 unsatcore
 Contains strategy implementations for unsat core computations.
 
 validation
 
 vb
 
 vs
 

Data Structures

struct  is_variant
 States whether a given type is a boost::variant. More...
 
struct  is_variant< boost::variant< BOOST_VARIANT_ENUM_PARAMS(U)> >
 States that boost::variant is indeed a boost::variant.
 
struct  is_variant< const boost::variant< BOOST_VARIANT_ENUM_PARAMS(U)> >
 States that const boost::variant is indeed a boost::variant.
 
class  VariantMap
 This class is a specialization of std::map where the keys are of arbitrary type and the values are of type boost::variant. More...
 
struct  CMakeOptionPrinter
 
class  Executor
 
class  PriorityQueue
 
class  DynamicPriorityQueue
 
class  SettingsComponents
 
class  SettingsParser
 
class  MaxSMT
 
class  BEModule
 
struct  BESettings1
 
class  BVDirectEncoder
 
class  BVModule
 
struct  BVSettings1
 
class  CNFerModule
 
class  CoCoAGBModule
 
struct  CoCoAGBSettings1
 
struct  CoCoAGBSettings2
 
class  CoveringNGModule
 
struct  CoveringNGSettingsDefault
 
class  Bimap
 Container that stores expensive to construct objects and allows the fast lookup with respect to two independent keys within the objects. More...
 
class  CSplitModule
 
struct  CSplitSettings1
 
class  CubeLIAModule
 
struct  CubeLIASettings1
 
class  CurryModule
 
struct  CurrySettings1
 
class  EMModule
 
struct  EMSettings1
 
class  ESModule
 
struct  ESSettingsDefault
 
struct  ESSettingsLimitSubstitution
 
class  FPPModule
 
struct  FPPSettings1Old
 
struct  FPPSettings1
 
struct  FPPSettings2
 
struct  FPPSettings3
 
struct  FPPSettingsPBGroebner
 
struct  FPPSettingsPB
 
struct  FPPSettingsOptimization
 
class  GBModule
 A solver module based on Groebner basis. More...
 
class  GBModuleState
 A class to save the current state of a GBModule. More...
 
struct  GBSettings5
 
struct  GBSettings3
 
struct  GBSettings1
 
struct  GBSettings4
 
struct  GBSettings6
 
struct  GBSettings41
 
struct  GBSettings51
 
struct  GBSettings51A
 
struct  GBSettings61
 
struct  GBSettings61A
 
struct  GBSettings43
 
struct  GBSettings63
 
struct  decidePassingPolynomial
 
class  InequalitiesTable
 Datastructure for the GBModule. More...
 
class  VariableRewriteRule
 
class  GBPPModule
 
struct  GBPPSettings1
 
class  ForwardHyperGraph
 This class implements a forward hypergraph. More...
 
struct  CycleEnumerator
 This class encapsulates an algorithm for enumerating all cycles. More...
 
class  ICEModule
 
struct  ICESettings1
 
class  ICPModule
 
struct  ICPSettings1
 
struct  ICPSettings2
 
struct  ICPSettings3
 
struct  ICPSettings4
 
class  IncWidthModule
 
struct  IncWidthSettings1
 
struct  IncWidthSettings2
 
struct  IncWidthSettings3
 
class  BVAnnotation
 
class  AnnotatedBVTerm
 
class  BlastedPoly
 
class  BlastedConstr
 
class  ConstrTree
 
class  ElementWithOrigins
 
class  CollectionWithOrigins
 
class  IntBlastModule
 
struct  IntBlastSettings1
 
struct  IntBlastSettings2
 
class  PolyTree
 
class  PolyTreeContent
 
class  PolyTreePool
 
class  IntEqModule
 A module which checks whether the equations contained in the received (linear integer) formula have a solution. More...
 
struct  IntEqSettings1
 
class  LRAModule
 A module which performs the Simplex method on the linear part of it's received formula. More...
 
struct  LRASettings1
 
struct  LRASettings2
 
struct  LRASettingsICP
 
class  LVEModule
 
struct  LVESettings1
 
class  MCBModule
 
struct  MCBSettings1
 
class  NewCADModule
 
struct  NewCADBaseSettings
 
struct  NewCADSettingsNaive
 
struct  NewCADSettingsNO
 
struct  NewCADSettingsNU
 
struct  NewCADSettingsSO
 
struct  NewCADSettingsSU
 
struct  NewCADSettingsFU
 
struct  NewCADBaseProjectionSettings
 
struct  NewCADSettingsCollins
 
struct  NewCADSettingsHong
 
struct  NewCADSettingsMcCallum
 
struct  NewCADSettingsMcCallumPartial
 
struct  NewCADSettingsLazard
 
struct  NewCADSettingsBrown
 
struct  NewCADBasePPSettings
 
struct  NewCADSettingsPP
 
struct  NewCADSettingsPPVE
 
struct  NewCADSettingsPPRR
 
struct  NewCADSettingsPPVERR
 
struct  NewCADBaseSettingsLO
 
struct  NewCADSettings_LOType
 
struct  NewCADSettings_LOT
 
struct  NewCADSettings_LOTLSA
 
struct  NewCADSettings_LOTSA
 
struct  NewCADSettings_LOTS
 
struct  NewCADSettings_LOLT
 
struct  NewCADSettings_LOLTA
 
struct  NewCADSettings_LOLTS
 
struct  NewCADSettings_LOLTSA
 
struct  NewCADSettings_LOLS
 
struct  NewCADSettings_LOS
 
struct  NewCADBaseSettingsPO
 
struct  NewCADSettings_POD
 
struct  NewCADSettings_POPD
 
struct  NewCADSettings_POSD
 
struct  NewCADSettings_POlD
 
struct  NewCADSettings_POLD
 
struct  NewCADSettingsF1
 
struct  NewCADSettingsFO1
 
struct  NewCADSettingsFOS
 
struct  NewCADSettingsInterleave
 
struct  NewCADSettingsEQ_B
 
struct  NewCADSettingsEQ_BD
 
struct  NewCADSettingsEQ_R
 
struct  NewCADSettingsEQ_RD
 
struct  NewCADSettingsEQ_RI
 
struct  NewCADSettingsEQ_RID
 
struct  NewCADSettingsEQ_S
 
struct  NewCADSettingsEQ_SD
 
struct  NewCADSettingsEQ_BR
 
struct  NewCADSettingsEQ_BRD
 
struct  NewCADSettingsEQ_BRI
 
struct  NewCADSettingsEQ_BRID
 
struct  NewCADSettingsEQ_BS
 
struct  NewCADSettingsEQ_BSD
 
struct  NewCADSettingsEQ_SI
 
struct  NewCADSettingsEQ_SID
 
struct  NewCADSettingsEQ_BSI
 
struct  NewCADSettingsEQ_BSID
 
struct  NewCADSettingsFV
 
struct  NewCADSettingsFOV
 
struct  NewCADSettingsMISBase
 
struct  NewCADSettingsMISTrivial
 
struct  NewCADSettingsMISGreedy
 
struct  NewCADSettingsMISGreedyPre
 
struct  NewCADSettingsMISGreedyWeighted
 
struct  NewCADSettingsMISExact
 
struct  NewCADSettingsMISHybrid
 
struct  NewCADSettingsEnumerateAll
 
class  Backend
 
struct  SampledDerivationRefCompare
 
class  LevelWiseInformation
 
class  NewCoveringModule
 
struct  NewCoveringSettings1
 
struct  NewCoveringSettings2
 
struct  NewCoveringSettings3
 
struct  NewCoveringSettings4
 
struct  sampling
 
struct  is_sample_outside
 
struct  sampling< SamplingAlgorithm::LOWER_UPPER_BETWEEN_SAMPLING >
 
struct  is_sample_outside< IsSampleOutsideAlgorithm::DEFAULT >
 
class  NewGBPPModule
 
struct  NewGBPPSettings1
 
class  RationalCapsule
 
class  VariableCapsule
 
class  AxiomFactory
 
class  LOG
 
class  MonomialMappingByVariablePool
 
class  NRAILModule
 
struct  NRAILSettings1
 
struct  NRAILSettings2
 
struct  NRAILSettings3
 
struct  NRAILSettings4
 
struct  NRAILSettings5
 
struct  NRAILSettings6
 
struct  NRAILSettings7
 
struct  NRAILSettings8
 
struct  NRAILSettings9
 
struct  NRAILSettings10
 
struct  NRAILSettings11
 
struct  NRAILSettings12
 
struct  NRAILSettings13
 
struct  NRAILSettings14
 
struct  NRAILSettings15
 
struct  NRAILSettings16
 
struct  NRAILSettings17
 
struct  NRAILSettings18
 
struct  NRAILSettings19
 
struct  NRAILSettings20
 
struct  NRAILSettings21
 
struct  NRAILSettings22
 
struct  NRAILSettings23
 
struct  NRAILSettings24
 
struct  NRAILSettings25
 
class  PBGaussModule
 
struct  PBGaussSettings1
 
class  CardinalityEncoder
 
class  ExactlyOneCommanderEncoder
 
class  LongFormulaEncoder
 
class  MixedSignEncoder
 
class  PseudoBoolEncoder
 Base class for a PseudoBoolean Encoder. More...
 
class  PseudoBoolNormalizer
 
class  RNSEncoder
 
class  ShortFormulaEncoder
 
class  TotalizerEncoder
 TotalizerEncoder implements the Totalizer encoding as described in "Incremental Cardinality Constraints for MaxSAT" by Martins et al https://doi.org/10.1007/978-3-319-10428-7_39. More...
 
class  TotalizerTree
 
class  PBPPModule
 
struct  PBPPSettingsBase
 
struct  PBPPSettingsLIAOnly
 
struct  PBPPSettings1
 
struct  PBPPSettingsLIAOnlyWithNormalize
 
struct  PBPPSettingsWithNormalize
 
struct  PBPPSettingsCardinalityOnly20
 
struct  PBPPSettingsCardinalityOnly05
 
struct  PBPPSettingsFull20
 
struct  PBPPSettingsFull05
 
struct  PBPPSettingsCardinalityOnly20Normalize
 
struct  PBPPSettingsCardinalityOnly05Normalize
 
struct  PBPPSettingsWithRNS
 
struct  PBPPSettingsWithCardConstr
 
struct  PBPPSettingsWithMixedConstr
 
struct  PBPPSettingsBasic
 
struct  PBPPSettingsMaxSMT
 
class  PFEModule
 
struct  PFESettings1
 
class  PNFerModule
 
class  VarSchedulerMcsatBase
 Base class for all MCSAT variable scheduler. More...
 
class  TheoryVarSchedulerStatic
 Schedules theory variables statically. More...
 
class  VarSchedulerMcsatBooleanFirst
 Variable scheduling that all decides Boolean variables first before deciding any theory variable. More...
 
class  VarSchedulerMcsatTheoryFirst
 Variable scheduling that all decides theory variables first before deciding any Boolean variable. More...
 
class  VarSchedulerMcsatUnivariateConstraintsOnly
 Decides only Constraints univariate in the current theory variable while the theory ordering is static. More...
 
class  VarSchedulerMcsatUnivariateClausesOnly
 Decides only Constraints occuring in clauses that are univariate in the current theory variable while the theory ordering is static. More...
 
class  VarSchedulerMcsatActivityPreferTheory
 Activity-based scheduler preferring initially theory variables. More...
 
class  SATModule
 Implements a module performing DPLL style SAT checking. More...
 
struct  SATSettings1
 
struct  SATSettings3
 
struct  SATSettingsStopAfterUnknown
 
struct  SATSettingsMCSAT
 
struct  SATSettingsMCSATDefault
 
struct  SATSettingsMCSATOC
 
struct  SATSettingsMCSATFMICPVSOC
 
struct  SATSettingsMCSATFMICPOC
 
struct  SATSettingsMCSATOCNew
 
struct  SATSettingsMCSATFMICPVSOCNew
 
struct  SATSettingsMCSATFMICPVSOCNewOC
 
struct  SATSettingsMCSATFMICPVSOCLWH12
 
struct  SATSettingsMCSATNL
 
struct  SATSettingsMCSATFMICPVSNL
 
struct  SATSettingsMCSATVSOCNew
 
struct  SATSettingsMCSATFMOCNew
 
class  VarSchedulerBase
 Base class for variable schedulers. More...
 
class  VarSchedulerMinisat
 Minisat's activity-based variable scheduling. More...
 
class  VarSchedulerFixedRandom
 
class  VarSchedulerRandom
 Random scheduler. More...
 
class  VarSchedulerSMTTheoryGuided
 Scheduler for SMT, implementing theory guided heuristics. More...
 
class  SplitSOSModule
 
struct  SplitSOSSettings1
 
class  STropModule
 
struct  STropSettings1
 Take conjunctions incrementally, construct linear formulas for LRA solver. More...
 
struct  STropSettings2
 
struct  STropSettings3
 Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve. More...
 
struct  STropSettings3b
 Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve. More...
 
struct  STropSettings2OutputOnly
 
struct  STropSettings3OutputOnly
 
struct  STropSettings3bOutputOnly
 
class  SymmetryModule
 
struct  SymmetrySettings1
 
class  VSModule
 
struct  VSSettings1
 
struct  VSSettings234
 
class  Optimization
 
class  Manager
 Base class for solvers. More...
 
struct  Branching
 Stores all necessary information of an branch, which can be used to detect probable infinite loop of branchings. More...
 
class  Module
 A base class for all kind of theory solving methods. More...
 
class  FormulaWithOrigins
 Stores a formula along with its origins. More...
 
class  ModuleInput
 The input formula a module has to consider for it's satisfiability check. More...
 
class  PModule
 
struct  AbstractModuleFactory
 
struct  ModuleFactory
 
class  BackendLink
 
class  StrategyGraph
 
class  Task
 
class  BackendSynchronisation
 
class  ThreadPool
 
class  AllModulesStrategy
 
class  BVPreprocessing
 Strategy description. More...
 
class  BVSolver
 Strategy description. More...
 
class  CoveringNG_Default
 The most efficient CoveringNG strategy with preprocessing. More...
 
class  CoveringNG_GBDefault
 
class  CoveringNG_PPBooleanExploration
 
class  CoveringNG_PPBooleanExplorationOnlyBool
 
class  CoveringNG_PPBooleanExplorationWithBool
 
class  CoveringNG_PPBooleanOff
 
class  CoveringNG_PPBooleanPartialPropagationSotd
 
class  CoveringNG_PPBooleanPartialPropagationTdeg
 
class  CoveringNG_PPBooleanPropagation
 
class  CoveringNG_PPDefault
 The most efficient CoveringNG strategy with preprocessing. More...
 
class  CoveringNG_PPFilterBoundsOnly
 
class  CoveringNG_PPFilterBoundsOnlyComplete
 
class  CoveringNG_PPFilterNoop
 
class  CoveringNG_PPGBDefault
 
class  CoveringNG_PPImplicantsLevelSize
 
class  CoveringNG_PPImplicantsLevelSotd
 
class  CoveringNG_PPImplicantsPickeringTotal
 
class  CoveringNG_PPImplicantsSizeOnly
 
class  CoveringNG_PPImplicantsSotd
 
class  CoveringNG_PPImplicantsSotdReverse
 
class  CoveringNG_PPImplicantsTdeg
 
class  CoveringNG_PPImplicantsVars
 
class  CoveringNG_PPImplicantsVarsVarorderSplitting
 
class  CoveringNG_PPInprocessingOn
 
class  CoveringNG_PPSTropDefault
 The most efficient CoveringNG strategy with preprocessing and subtropical. More...
 
class  CoveringNG_PPVarorderPickering
 
class  CoveringNG_PPVarorderUnivariate
 
class  CSplitFull
 
class  CSplitOnly
 
class  Default
 The default SMT-RAT strategy. More...
 
class  DefaultTwo
 The default SMT-RAT strategy. More...
 
class  Filter_BCAll
 
class  Filter_BCBc
 
class  Filter_BCBoundsOnly
 
class  Filter_BCDeg10
 
class  Filter_BCDeg2
 
class  Filter_BCDeg5
 
class  Filter_BCIndep
 
class  Filter_BCIntersect
 
class  Filter_BCIrred
 
class  Filter_BCIrredIndep
 
class  Filter_BCNoop
 
class  Filter_BCRational
 
class  Filter_LDBBoundsOnly
 
class  Filter_LDBNoop
 
class  LIASolver
 Strategy description. More...
 
class  LRASolver
 Strategy description. More...
 
class  MAXSATBackendStrategy
 This strategy is used as a artificial backend in the MaxSMT Module. More...
 
class  PBPPStrategy
 
class  MCSAT_FMICPOC
 
class  MCSAT_FMICPVSNL
 
class  MCSAT_FMICPVSOC
 
class  MCSAT_FMICPVSOCLWH11
 
class  MCSAT_FMICPVSOCLWH12
 
class  MCSAT_FMICPVSOCLWH13
 
class  MCSAT_FMICPVSOCNew
 
class  MCSAT_FMICPVSOCNewOC
 
class  MCSAT_FMICPVSOCNNASC
 
class  MCSAT_FMICPVSOCNNDSC
 
class  MCSAT_FMICPVSOCPARALLEL
 
class  MCSAT_FMNL
 
class  MCSAT_FMOCNew
 
class  MCSAT_FMVSNL
 
class  MCSAT_FMVSOC
 
class  MCSAT_ICPNL
 
class  MCSAT_NL
 
class  MCSAT_OC
 
class  MCSAT_OCLWH11
 
class  MCSAT_OCLWH12
 
class  MCSAT_OCLWH13
 
class  MCSAT_OCLWH21
 
class  MCSAT_OCLWH22
 
class  MCSAT_OCLWH23
 
class  MCSAT_OCLWH31
 
class  MCSAT_OCLWH32
 
class  MCSAT_OCLWH33
 
class  MCSAT_OCNew
 
class  MCSAT_OCNewBC
 
class  MCSAT_OCNewLDB
 
class  MCSAT_OCNewLDBCovering
 
class  MCSAT_OCNewLDBCoveringCache
 
class  MCSAT_OCNewLDBCoveringCacheGlobal
 
class  MCSAT_OCNN
 
class  MCSAT_OCNNASC
 
class  MCSAT_OCNNDSC
 
class  MCSAT_OCPARALLEL
 
class  MCSAT_PPDefault
 
class  MCSAT_PPNL
 
class  MCSAT_PPOC
 
class  MCSAT_PPOCNew
 
class  MCSAT_VSNL
 
class  MCSAT_VSOCNew
 
class  MIS_Exact
 
class  MIS_Greedy
 
class  MIS_Trivial
 
class  MIS_GreedyPre
 
class  MIS_GreedyWeighted
 
class  MIS_Hybrid
 
class  NewCAD_Brown
 
class  NewCAD_Collins
 
class  NewCAD_FOS
 
class  NewCAD_FU
 
class  NewCAD_FU_SC
 
class  NewCAD_FU_SI
 
class  NewCAD_FU_SInf
 
class  NewCAD_FU_SL
 
class  NewCAD_FU_SR
 
class  NewCAD_FU_SZ
 
class  NewCAD_Hong
 
class  NewCAD_LOLS
 
class  NewCAD_LOLT
 
class  NewCAD_LOLTA
 
class  NewCAD_LOLTS
 
class  NewCAD_LOLTSA
 
class  NewCAD_LOS
 
class  NewCAD_LOT
 
class  NewCAD_LOTLSA
 
class  NewCAD_LOTS
 
class  NewCAD_LOTSA
 
class  NewCAD_McCallum
 
class  NewCAD_McCallumPartial
 
class  NewCAD_Naive
 
class  NewCAD_NO
 
class  NewCAD_NU
 
class  NewCAD_Only
 
class  NewCAD_POD
 
class  NewCAD_POLD
 
class  NewCAD_POPD
 
class  NewCAD_POSD
 
class  NewCAD_PP
 
class  NewCAD_PPRR
 
class  NewCAD_PPVE
 
class  NewCAD_PPVERR
 
class  NewCAD_SAT
 
class  NewCAD_SO
 
class  NewCAD_SU
 
class  NewCADEQ_B
 
class  NewCADEQ_BD
 
class  NewCADEQ_BR
 
class  NewCADEQ_BRD
 
class  NewCADEQ_BRI
 
class  NewCADEQ_BRID
 
class  NewCADEQ_BS
 
class  NewCADEQ_BSD
 
class  NewCADEQ_BSI
 
class  NewCADEQ_BSID
 
class  NewCADEQ_R
 
class  NewCADEQ_RD
 
class  NewCADEQ_RI
 
class  NewCADEQ_RID
 
class  NewCADEQ_S
 
class  NewCADEQ_SD
 
class  NewCADEQ_SI
 
class  NewCADEQ_SID
 
class  NewCovering_Backtracking
 
class  NewCovering_FilterBoundsOnly
 
class  NewCovering_Incomplete
 
class  NewCovering_Incremental
 
class  NewCovering_IncrementalBacktracking
 
class  NewCovering_PPComplete
 
class  NewCovering_PPFilterBoundsOnly
 
class  NewCovering_PPFilterBoundsOnlyComplete
 
class  NewCovering_PPIncomplete
 
class  NewCovering_Vanilla
 
class  NIABB
 Strategy description. More...
 
class  NIABlast
 Strategy description. More...
 
class  NIASolver
 Strategy description. More...
 
class  NRA_CAD
 Strategy description. More...
 
class  NRA_ICPVSCAD
 Strategy description. More...
 
class  NRA_LRAVSCAD
 Strategy description. More...
 
class  NRA_VSCAD
 Strategy description. More...
 
class  NRARefinement_Solver
 Strategy description. More...
 
class  NRARefinement_Solver1
 Strategy description. More...
 
class  NRARefinement_Solver10
 Strategy description. More...
 
class  NRARefinement_Solver11
 Strategy description. More...
 
class  NRARefinement_Solver12
 Strategy description. More...
 
class  NRARefinement_Solver13
 Strategy description. More...
 
class  NRARefinement_Solver14
 Strategy description. More...
 
class  NRARefinement_Solver15
 Strategy description. More...
 
class  NRARefinement_Solver16
 Strategy description. More...
 
class  NRARefinement_Solver17
 Strategy description. More...
 
class  NRARefinement_Solver18
 Strategy description. More...
 
class  NRARefinement_Solver19
 Strategy description. More...
 
class  NRARefinement_Solver2
 Strategy description. More...
 
class  NRARefinement_Solver20
 Strategy description. More...
 
class  NRARefinement_Solver21
 Strategy description. More...
 
class  NRARefinement_Solver22
 Strategy description. More...
 
class  NRARefinement_Solver23
 Strategy description. More...
 
class  NRARefinement_Solver24
 Strategy description. More...
 
class  NRARefinement_Solver25
 Strategy description. More...
 
class  NRARefinement_Solver3
 Strategy description. More...
 
class  NRARefinement_Solver4
 Strategy description. More...
 
class  NRARefinement_Solver5
 Strategy description. More...
 
class  NRARefinement_Solver6
 Strategy description. More...
 
class  NRARefinement_Solver7
 Strategy description. More...
 
class  NRARefinement_Solver8
 Strategy description. More...
 
class  NRARefinement_Solver9
 Strategy description. More...
 
class  NRASolver
 Strategy description. More...
 
class  NRASolverCov
 Strategy description. More...
 
class  OnlyCAD
 
class  OnlyGB
 
class  OnlySAT
 A pure SAT solver. More...
 
class  OnlySATPP
 A pure SAT solver with preprocessing. More...
 
class  OnlyVS
 Strategy description. More...
 
class  OptimizationPreprocessing
 
class  OptimizationStrategy
 A backend compatible with optimization. More...
 
class  PBPPStrategy2
 
class  PBPPStrategyBasic
 
class  PBPPStrategyGauss
 
class  PBPPStrategyGroebner
 
class  PBPPStrategyLIAOnly
 
class  PBPPStrategyRNS
 
class  PBPPStrategyWithCardConstr
 
class  PBPPStrategyWithMixedConstr
 
class  PBPreprocessing
 Strategy description. More...
 
class  PBPreprocessingGroebner
 
class  PreprocessingOne
 Strategy description. More...
 
class  PreprocessingTwo
 Strategy description. More...
 
class  PBPPStrategyGroe_Norm_PB_LIA
 
class  PBPPStrategyGroe_PB_LIA
 
class  PBPPStrategyLIA
 
class  PBPPStrategyLIA_ICP
 
class  PBPPStrategyLIA_VS
 
class  PBPPStrategyNorm_LIA
 
class  PBPPStrategyNorm_LIA_ICP
 
class  PBPPStrategyNorm_LIA_VS
 
class  PBPPStrategyNorm_PB_LIA
 
class  PBPPStrategyPB_LIA
 
class  RatIntBlast
 Strategy description. More...
 
class  SMTCOMP
 Strategy description. More...
 
class  STrop_BackendsOnly
 Strategy description. More...
 
class  STrop_CADBackendsOnly
 Strategy description. More...
 
class  STrop_Formula
 
class  STrop_FormulaAlt
 
class  STrop_FormulaAltOutputOnly
 
class  STrop_FormulaAltWCADBackends
 
class  STrop_FormulaAltWCADBackendsFull
 
class  STrop_FormulaOutputOnly
 
class  STrop_FormulaWBackends
 
class  STrop_FormulaWBackendsFull
 
class  STrop_FormulaWCADBackends
 
class  STrop_FormulaWCADBackendsFull
 
class  STrop_FormulaWMCSAT
 
class  STrop_Incremental
 
class  STrop_IncrementalWBackends
 
class  STrop_IncrementalWCADBackends
 
class  STrop_MCSATOnly
 
class  STrop_TransformationEQ
 
class  STrop_TransformationEQOutputOnly
 
class  STrop_TransformationEQWBackends
 
class  STrop_TransformationEQWCADBackends
 
class  UnsatCore
 

Typedefs

using ModelVariable = carl::ModelVariable
 
using ModelValue = carl::ModelValue< Rational, Poly >
 
using Model = carl::Model< Rational, Poly >
 
using ModelSubstitution = carl::ModelSubstitution< Rational, Poly >
 
using ModelPolynomialSubstitution = carl::ModelPolynomialSubstitution< Rational, Poly >
 
using InfinityValue = carl::InfinityValue
 
using SqrtEx = carl::SqrtEx< Poly >
 
using MultivariateRootT = carl::MultivariateRoot< Poly >
 
using DoubleInterval = carl::Interval< double >
 
using RationalInterval = carl::Interval< Rational >
 
using EvalDoubleIntervalMap = std::map< carl::Variable, DoubleInterval >
 
using EvalRationalIntervalMap = std::map< carl::Variable, RationalInterval >
 
using ObjectiveValues = std::vector< std::pair< std::variant< Poly, std::string >, Model::mapped_type > >
 
using Statistics = carl::statistics::Statistics
 
using Conditionals = std::vector< std::atomic_bool * >
 A vector of atomic bool pointers. More...
 
using Rational = mpq_class
 
using Integer = carl::IntegralType< Rational >::type
 
using TermT = carl::Term< Rational >
 
using Poly = carl::MultivariatePolynomial< Rational >
 
using Factorization = std::map< Poly, carl::uint >
 
using ConstraintT = carl::Constraint< Poly >
 
using ConstraintsT = carl::Constraints< Poly >
 
using VariableAssignmentT = carl::VariableAssignment< Poly >
 
using VariableComparisonT = carl::VariableComparison< Poly >
 
using FormulaT = carl::Formula< Poly >
 
using FormulasT = carl::Formulas< Poly >
 
using FormulaSetT = carl::FormulaSet< Poly >
 
using FormulasMultiT = std::multiset< FormulaT >
 
using RationalAssignment = carl::Assignment< Rational >
 
using RAN = carl::IntRepRealAlgebraicNumber< Rational >
 
using thread_priority = std::pair< std::size_t, std::size_t >
 
typedef expression::Expression Expression
 
typedef expression::Expressions Expressions
 
typedef carl::StdMultivariatePolynomialPolicies< carl::BVReasons > ReasonPolicy
 
typedef std::set< icp::ContractionCandidate *, icp::contractionCandidateComp > ContractionCandidates
 
typedef std::map< FormulaT, std::shared_ptr< std::vector< FormulaT > > > Formula_Origins
 
typedef std::unordered_map< carl::Variable, carl::Monomial::Arg >::iterator MonomialMapIterator
 
typedef std::unordered_map< carl::Variable, carl::Monomial::Arg > MonomialMap
 
typedef bool(* ConditionEvaluation) (carl::Condition)
 
typedef std::function< bool(carl::Condition)> ConditionFunction
 
using Priority = std::vector< std::size_t >
 

Enumerations

enum  LemmaLevel { NONE = 0 , NORMAL = 1 , ADVANCED = 2 }
 
enum  Answer {
  SAT = 0 , UNSAT = 1 , UNKNOWN = 2 , ABORTED = 3 ,
  OPTIMAL = 4
}
 An enum with the possible answers a Module can give. More...
 
enum class  MaxSMTStrategy { FU_MALIK_INCREMENTAL , MSU3 , LINEAR_SEARCH }
 
enum  pass_inequalities { AS_RECEIVED , FULL_REDUCED , FULL_REDUCED_IF }
 Only active if we check inequalities. More...
 
enum  after_firstInfeasibleSubset { RETURN_DIRECTLY , PROCEED_INFEASIBLEANDDEDUCTION , PROCEED_ALLINEQUALITIES }
 
enum  theory_deductions { NO_CONSTRAINTS , ONLY_INEQUALITIES , ALL_CONSTRAINTS }
 
enum  check_inequalities { ALWAYS , AFTER_NEW_GB , NEVER }
 
enum  transform_inequalities { ALL_INEQUALITIES , ONLY_NONSTRICT , NO_INEQUALITIES }
 
enum  backtracking_mode { CHRONOLOGICAL , NON_CHRONOLOGICAL }
 
enum class  SplittingHeuristic : unsigned { SIZE , UNSATISFIABILITY , SATISFIABILITY }
 
enum  CoveringStatus { partial = 0 , full = 1 , unknown = 2 , failed = 3 }
 
enum  SamplingAlgorithm { LOWER_UPPER_BETWEEN_SAMPLING }
 
enum  IsSampleOutsideAlgorithm { DEFAULT }
 
enum class  UNSATFormulaSelectionStrategy { ALL = 0 , FIRST = 1 , RANDOM = 2 }
 
enum class  CCES : unsigned { SECOND_LEVEL_MINIMIZER , LITERALS_BLOCKS_DISTANCE , SECOND_LEVEL_MINIMIZER_PLUS_LBD }
 
enum class  VARIABLE_ACTIVITY_STRATEGY : unsigned { NONE , MIN_COMPLEXITY_MAX_OCCURRENCES }
 
enum class  MCSAT_BOOLEAN_DOMAIN_PROPAGATION : unsigned { NONE , PARTIAL_CONFLICT , PARTIAL , FULL }
 
enum class  TheoryGuidedDecisionHeuristicLevel : unsigned { CONFLICT_FIRST , SATISFIED_FIRST , DISABLED }
 
enum class  Mode { INCREMENTAL_CONSTRAINTS , TRANSFORM_EQUATION , TRANSFORM_FORMULA , TRANSFORM_FORMULA_ALT }
 
enum class  VariableValuationStrategy : unsigned { OPTIMIZE_BEST , OPTIMIZE_AVERAGE , OPTIMIZE_WORST }
 
enum class  UnsatCoreStrategy { ModelExclusion }
 

Functions

int handle_basic_options (const SettingsParser &parser)
 
const auto & settings_parser ()
 
bool parseSMT2File (parser::InstructionHandler &handler, bool queueInstructions, std::istream &input)
 
int convert_to_cnf_dimacs (const std::string &, const std::string &)
 
int convert_to_cnf_smtlib (const std::string &, const std::string &)
 
std::ostream & operator<< (std::ostream &os, CMakeOptionPrinter cmop)
 
constexpr CMakeOptionPrinter CMakeOptions (bool advanced=false) noexcept
 
template<typename Executor >
bool parseInput (const std::string &pathToInputFile, Executor &e, bool &queueInstructions)
 
template<typename Executor >
int executeFile (const std::string &pathToInputFile, Executor &e)
 Parse the file and save it in formula. More...
 
int analyze_file (const std::string &)
 
template<typename Strategy >
int run_dimacs_file (Strategy &, const std::string &)
 
template<typename Strategy >
int run_opb_file (Strategy &, const std::string &)
 
FormulaT parse_smtlib (const std::string &)
 
FormulaT parse_formula (const std::string &filename)
 Loads the smt2 file specified in filename and returns the formula. More...
 
int preprocess_file (const std::string &filename, const std::string &outfile)
 Loads the smt2 file specified in filename and runs the preprocessing strategy. More...
 
const auto & settings_analyzer ()
 
analyzer::AnalyzerStatistics & analyze_formula (const FormulaT &f)
 
template<typename TT , typename C >
std::ostream & operator<< (std::ostream &os, const PriorityQueue< TT, C > &pq)
 
const settings::Settings & Settings ()
 
const auto & settings_core ()
 
const auto & settings_solver ()
 
const auto & settings_module ()
 
template<typename T >
auto & statistics_get (const std::string &name)
 
const auto & settings_statistics ()
 
bool is_sat (Answer a)
 
std::ostream & operator<< (std::ostream &os, Answer a)
 
auto & validation_get (const std::string &channel, const std::string &file, int line)
 
const auto & settings_validation ()
 
void visiting (const Expression &expr)
 
void testExpression ()
 
std::ostream & operator<< (std::ostream &os, MaxSMTStrategy ucs)
 
std::ostream & operator<< (std::ostream &os, const CoveringStatus &status)
 
template<typename Settings >
std::ostream & operator<< (std::ostream &os, const LevelWiseInformation< Settings > &levelWiseInformation)
 
std::string get_name (SamplingAlgorithm samplingAlgorithm)
 
std::string get_name (IsSampleOutsideAlgorithm samplingAlgorithm)
 
FormulaT createZeroOne (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable)
 
FormulaT createZeroTwo (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable)
 
FormulaT createZeroThree (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable)
 
FormulasT createZero (smtrat::VariableCapsule variableCapsule)
 
FormulaT createTangentPlaneNEQOne (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational)
 
FormulaT createTangentPlaneNEQTwo (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational bRational)
 
FormulaT createTangentPlaneNEQThree (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational, Rational bRational)
 
FormulaT createTangentPlaneNEQFour (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational, Rational bRational)
 
FormulasT createTangentPlaneNEQ (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
 
FormulaT createTangentPlaneEQOne (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational)
 
FormulaT createTangentPlaneEQTwo (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational)
 
FormulasT createTangentPlaneEQ (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
 
const smtrat::VariableCapsule extractVariables (MonomialMapIterator monomialIterator)
 
Model createAbsoluteValuedModel (Model linearizedModel)
 
carl::Variable createAuxiliaryVariable (carl::Variable variable)
 create an auxiliary variable e.g. More...
 
FormulaT generateAbsFormula (carl::Variable variable, carl::Variable aux_variable)
 | x1 | = (and (=> (x1 >= 0) (y1 = x1)) (=> (x1 < 0) (y1 = -x1)) ) More...
 
FormulaT generateAbsFormula (carl::Variable variableLeft, carl::Variable variableRight, carl::Relation relation)
 | x1 | <= | x1 | = (and (=> (x1 >= 0) (y1 = x1)) (=> (x1 < 0) (y1 = -x1)) (=> (x2 >= 0) (y2 = x2)) (=> (x2 < 0) (y2 = -x2)) (y1 <= y2) ) More...
 
FormulaT createEquivalentToOriginalMonotonicityOne (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
 
FormulaT createEquivalentToOriginalMonotonicityTwo (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
 
FormulaT createEquivalentToOriginalMonotonicityThree (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
 
RationalCapsule extractRationalCapsule (VariableCapsule variableCapsule, Model linearizedModel)
 
FormulaT createOriginalMonotonicityOne (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
 
FormulaT createOriginalMonotonicityTwo (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
 
FormulaT createOriginalMonotonicityThree (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
 
FormulasT createMonotonicity (VariableCapsule variableCapsuleOuter, VariableCapsule variableCapsuleInner, Model absoluteValuedModel)
 
FormulaT createCongruence (smtrat::VariableCapsule variableCapsuleOuter, smtrat::VariableCapsule variableCapsuleInner)
 
FormulaT createICPGreaterOne (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
 
FormulaT createICPGreaterTwo (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
 
FormulasT createICPGreater (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
 
FormulaT createICPLess (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
 
bool abEqualcCheck (VariableCapsule variableCapsuleOuter, Model linearizedModel)
 
bool abGreatercCheck (RationalCapsule rationalCapsule)
 
bool abLesscCheck (RationalCapsule rationalCapsule)
 
RationalCapsule generateAbcPrimeForICP (RationalCapsule rationalCapsule, bool isGreater)
 
bool isAnyRationalIsZero (RationalCapsule rationalCapsule)
 
Rational factorial (Rational n)
 
Rational factorial (std::size_t)
 
std::ostream & operator<< (std::ostream &os, Module::LemmaType lt)
 
template<typename AnnotationType >
void annotateFormula (const FormulaT &, const std::vector< AnnotationType > &)
 
std::ostream & operator<< (std::ostream &os, const ModuleInput &mi)
 
bool isCondition (carl::Condition _condition)
 
template<typename Module >
std::ostream & operator<< (std::ostream &os, const ModuleFactory< Module > &mf)
 
std::ostream & operator<< (std::ostream &os, UnsatCoreStrategy ucs)
 

Variables

static const Model EMPTY_MODEL = Model()
 
static constexpr int COMMANDER_GROUP_SIZE = 4
 

Detailed Description

Class to create the formulas for axioms.

Class to create a settings object for the VSModule.

Class to create a substitution object.

Class to create a state object.

Class to create a condition object.

Author
Aklima Zaman
Since
2018-09-24
Version
2018-09-24
Author
Florian Corzilius
Since
2010-07-26
Version
2011-06-20
Author
Florian Corzilius
Since
2010-07-26
Version
2011-12-05
Author
Florian Corzilius
Since
2010-05-11
Version
2013-10-24
Author
Florian Corzilius
Since
2010-05-11
Version
2013-10-23
Author
Florian Corzilius
Since
2013-07-02
Version
2014-09-18

Typedef Documentation

◆ Conditionals

typedef std::vector< std::atomic_bool * > smtrat::Conditionals

A vector of atomic bool pointers.

Definition at line 17 of file types.h.

◆ ConditionEvaluation

typedef bool(* smtrat::ConditionEvaluation) (carl::Condition)

Definition at line 13 of file StrategyGraph.h.

◆ ConditionFunction

typedef std::function<bool(carl::Condition)> smtrat::ConditionFunction

Definition at line 39 of file StrategyGraph.h.

◆ ConstraintsT

using smtrat::ConstraintsT = typedef carl::Constraints<Poly>

Definition at line 31 of file types.h.

◆ ConstraintT

using smtrat::ConstraintT = typedef carl::Constraint<Poly>

Definition at line 29 of file types.h.

◆ ContractionCandidates

typedef std::set<icp::ContractionCandidate*, icp::contractionCandidateComp> smtrat::ContractionCandidates

Definition at line 18 of file IcpVariable.h.

◆ DoubleInterval

using smtrat::DoubleInterval = typedef carl::Interval<double>

Definition at line 26 of file model.h.

◆ EvalDoubleIntervalMap

using smtrat::EvalDoubleIntervalMap = typedef std::map<carl::Variable, DoubleInterval>

Definition at line 29 of file model.h.

◆ EvalRationalIntervalMap

using smtrat::EvalRationalIntervalMap = typedef std::map<carl::Variable, RationalInterval>

Definition at line 30 of file model.h.

◆ Expression

typedef expression::Expression smtrat::Expression

Definition at line 61 of file ExpressionTypes.h.

◆ Expressions

typedef expression::Expressions smtrat::Expressions

Definition at line 62 of file ExpressionTypes.h.

◆ Factorization

using smtrat::Factorization = typedef std::map<Poly, carl::uint>

Definition at line 27 of file types.h.

◆ Formula_Origins

typedef std::map< FormulaT, std::shared_ptr< std::vector<FormulaT> > > smtrat::Formula_Origins

Definition at line 14 of file IntEqModule.h.

◆ FormulaSetT

using smtrat::FormulaSetT = typedef carl::FormulaSet<Poly>

Definition at line 41 of file types.h.

◆ FormulasMultiT

using smtrat::FormulasMultiT = typedef std::multiset<FormulaT>

Definition at line 43 of file types.h.

◆ FormulasT

using smtrat::FormulasT = typedef carl::Formulas<Poly>

Definition at line 39 of file types.h.

◆ FormulaT

using smtrat::FormulaT = typedef carl::Formula<Poly>

Definition at line 37 of file types.h.

◆ InfinityValue

using smtrat::InfinityValue = typedef carl::InfinityValue

Definition at line 20 of file model.h.

◆ Integer

using smtrat::Integer = typedef carl::IntegralType<Rational>::type

Definition at line 21 of file types.h.

◆ Model

using smtrat::Model = typedef carl::Model<Rational, Poly>

Definition at line 13 of file model.h.

◆ ModelPolynomialSubstitution

using smtrat::ModelPolynomialSubstitution = typedef carl::ModelPolynomialSubstitution<Rational, Poly>

Definition at line 18 of file model.h.

◆ ModelSubstitution

using smtrat::ModelSubstitution = typedef carl::ModelSubstitution<Rational, Poly>

Definition at line 17 of file model.h.

◆ ModelValue

using smtrat::ModelValue = typedef carl::ModelValue<Rational, Poly>

Definition at line 12 of file model.h.

◆ ModelVariable

using smtrat::ModelVariable = typedef carl::ModelVariable

Definition at line 11 of file model.h.

◆ MonomialMap

typedef std::unordered_map<carl::Variable, carl::Monomial::Arg> smtrat::MonomialMap

Definition at line 11 of file Util.h.

◆ MonomialMapIterator

typedef std::unordered_map<carl::Variable, carl::Monomial::Arg>::iterator smtrat::MonomialMapIterator

Definition at line 10 of file Util.h.

◆ MultivariateRootT

using smtrat::MultivariateRootT = typedef carl::MultivariateRoot<Poly>

Definition at line 24 of file model.h.

◆ ObjectiveValues

using smtrat::ObjectiveValues = typedef std::vector<std::pair<std::variant<Poly,std::string>, Model::mapped_type> >

Definition at line 32 of file model.h.

◆ Poly

using smtrat::Poly = typedef carl::MultivariatePolynomial<Rational>

Definition at line 25 of file types.h.

◆ Priority

using smtrat::Priority = typedef std::vector<std::size_t>

Definition at line 24 of file ThreadPool.h.

◆ RAN

using smtrat::RAN = typedef carl::IntRepRealAlgebraicNumber<Rational>

Definition at line 47 of file types.h.

◆ Rational

using smtrat::Rational = typedef mpq_class

Definition at line 19 of file types.h.

◆ RationalAssignment

using smtrat::RationalAssignment = typedef carl::Assignment<Rational>

Definition at line 45 of file types.h.

◆ RationalInterval

using smtrat::RationalInterval = typedef carl::Interval<Rational>

Definition at line 27 of file model.h.

◆ ReasonPolicy

typedef carl::StdMultivariatePolynomialPolicies<carl::BVReasons> smtrat::ReasonPolicy

Definition at line 38 of file GBSettings.h.

◆ SqrtEx

using smtrat::SqrtEx = typedef carl::SqrtEx<Poly>

Definition at line 22 of file model.h.

◆ Statistics

using smtrat::Statistics = typedef carl::statistics::Statistics

Definition at line 7 of file Statistics.h.

◆ TermT

using smtrat::TermT = typedef carl::Term<Rational>

Definition at line 23 of file types.h.

◆ thread_priority

using smtrat::thread_priority = typedef std::pair<std::size_t, std::size_t>

Definition at line 50 of file types.h.

◆ VariableAssignmentT

using smtrat::VariableAssignmentT = typedef carl::VariableAssignment<Poly>

Definition at line 33 of file types.h.

◆ VariableComparisonT

using smtrat::VariableComparisonT = typedef carl::VariableComparison<Poly>

Definition at line 35 of file types.h.

Enumeration Type Documentation

◆ after_firstInfeasibleSubset

enum smtrat::after_firstInfeasibleSubset
Enumerator
RETURN_DIRECTLY 
PROCEED_INFEASIBLEANDDEDUCTION 
PROCEED_ALLINEQUALITIES 

Definition at line 25 of file GBSettings.h.

◆ Answer

enum smtrat::Answer

An enum with the possible answers a Module can give.

Enumerator
SAT 
UNSAT 
UNKNOWN 
ABORTED 
OPTIMAL 

Definition at line 57 of file types.h.

◆ backtracking_mode

enum smtrat::backtracking_mode
Enumerator
CHRONOLOGICAL 
NON_CHRONOLOGICAL 

Definition at line 33 of file GBSettings.h.

◆ CCES

enum smtrat::CCES : unsigned
strong
Enumerator
SECOND_LEVEL_MINIMIZER 
LITERALS_BLOCKS_DISTANCE 
SECOND_LEVEL_MINIMIZER_PLUS_LBD 

Definition at line 17 of file SATSettings.h.

◆ check_inequalities

enum smtrat::check_inequalities
Enumerator
ALWAYS 
AFTER_NEW_GB 
NEVER 

Definition at line 29 of file GBSettings.h.

◆ CoveringStatus

enum smtrat::CoveringStatus
Enumerator
partial 
full 
unknown 
failed 

Definition at line 23 of file LevelWiseInformation.h.

◆ IsSampleOutsideAlgorithm

enum smtrat::IsSampleOutsideAlgorithm
Enumerator
DEFAULT 

Definition at line 21 of file Sampling.h.

◆ LemmaLevel

enum smtrat::LemmaLevel
Enumerator
NONE 
NORMAL 
ADVANCED 

Definition at line 53 of file types.h.

◆ MaxSMTStrategy

enum smtrat::MaxSMTStrategy
strong
Enumerator
FU_MALIK_INCREMENTAL 
MSU3 
LINEAR_SEARCH 

Definition at line 9 of file MaxSMT.h.

◆ MCSAT_BOOLEAN_DOMAIN_PROPAGATION

enum smtrat::MCSAT_BOOLEAN_DOMAIN_PROPAGATION : unsigned
strong
Enumerator
NONE 
PARTIAL_CONFLICT 
PARTIAL 
FULL 

Definition at line 21 of file SATSettings.h.

◆ Mode

enum smtrat::Mode
strong
Enumerator
INCREMENTAL_CONSTRAINTS 
TRANSFORM_EQUATION 
TRANSFORM_FORMULA 
TRANSFORM_FORMULA_ALT 

Definition at line 13 of file STropSettings.h.

◆ pass_inequalities

enum smtrat::pass_inequalities

Only active if we check inequalities.

AS_RECEIVED: Do not change the received inequalities. FULL_REDUCED: Pass the fully reduced received inequalities. REDUCED: Pass the reduced received inequalities. REDUCED_ONLYSTRICT: Pass the nonstrict inequalities reduced, the others unchanged FULL_REDUCED_ONLYNEW: Do only a full reduce on the newly added received inequalities.

Enumerator
AS_RECEIVED 
FULL_REDUCED 
FULL_REDUCED_IF 

Definition at line 23 of file GBSettings.h.

◆ SamplingAlgorithm

enum smtrat::SamplingAlgorithm
Enumerator
LOWER_UPPER_BETWEEN_SAMPLING 

Definition at line 17 of file Sampling.h.

◆ SplittingHeuristic

enum smtrat::SplittingHeuristic : unsigned
strong
Enumerator
SIZE 
UNSATISFIABILITY 
SATISFIABILITY 

Definition at line 15 of file ICPSettings.h.

◆ theory_deductions

enum smtrat::theory_deductions
Enumerator
NO_CONSTRAINTS 
ONLY_INEQUALITIES 
ALL_CONSTRAINTS 

Definition at line 27 of file GBSettings.h.

◆ TheoryGuidedDecisionHeuristicLevel

enum smtrat::TheoryGuidedDecisionHeuristicLevel : unsigned
strong
Enumerator
CONFLICT_FIRST 
SATISFIED_FIRST 
DISABLED 

Definition at line 10 of file VarSchedulerForwardDeclarations.h.

◆ transform_inequalities

enum smtrat::transform_inequalities
Enumerator
ALL_INEQUALITIES 
ONLY_NONSTRICT 
NO_INEQUALITIES 

Definition at line 31 of file GBSettings.h.

◆ UnsatCoreStrategy

enum smtrat::UnsatCoreStrategy
strong
Enumerator
ModelExclusion 

Definition at line 8 of file UnsatCore.h.

◆ UNSATFormulaSelectionStrategy

enum smtrat::UNSATFormulaSelectionStrategy
strong
Enumerator
ALL 
FIRST 
RANDOM 

Definition at line 15 of file NRAILSettings.h.

◆ VARIABLE_ACTIVITY_STRATEGY

enum smtrat::VARIABLE_ACTIVITY_STRATEGY : unsigned
strong
Enumerator
NONE 
MIN_COMPLEXITY_MAX_OCCURRENCES 

Definition at line 19 of file SATSettings.h.

◆ VariableValuationStrategy

enum smtrat::VariableValuationStrategy : unsigned
strong
Enumerator
OPTIMIZE_BEST 
OPTIMIZE_AVERAGE 
OPTIMIZE_WORST 

Definition at line 14 of file VSSettings.h.

Function Documentation

◆ abEqualcCheck()

bool smtrat::abEqualcCheck ( VariableCapsule  variableCapsuleOuter,
Model  linearizedModel 
)

Definition at line 766 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ abGreatercCheck()

bool smtrat::abGreatercCheck ( RationalCapsule  rationalCapsule)

Definition at line 796 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ abLesscCheck()

bool smtrat::abLesscCheck ( RationalCapsule  rationalCapsule)

Definition at line 817 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ analyze_file()

int smtrat::analyze_file ( const std::string &  )

Definition at line 32 of file formula_analyzer.cpp.

Here is the caller graph for this function:

◆ analyze_formula()

analyzer::AnalyzerStatistics & smtrat::analyze_formula ( const FormulaT &  f)

Definition at line 10 of file smtrat-analyzer.cpp.

Here is the call graph for this function:

◆ annotateFormula()

template<typename AnnotationType >
void smtrat::annotateFormula ( const FormulaT &  ,
const std::vector< AnnotationType > &   
)

Definition at line 256 of file ModuleInput.cpp.

◆ CMakeOptions()

constexpr CMakeOptionPrinter smtrat::CMakeOptions ( bool  advanced = false)
constexprnoexcept

Definition at line 27 of file compile_information.h.

Here is the caller graph for this function:

◆ convert_to_cnf_dimacs()

int smtrat::convert_to_cnf_dimacs ( const std::string &  ,
const std::string &   
)

Definition at line 58 of file cnf_conversion.cpp.

Here is the caller graph for this function:

◆ convert_to_cnf_smtlib()

int smtrat::convert_to_cnf_smtlib ( const std::string &  ,
const std::string &   
)

Definition at line 63 of file cnf_conversion.cpp.

Here is the caller graph for this function:

◆ createAbsoluteValuedModel()

Model smtrat::createAbsoluteValuedModel ( Model  linearizedModel)

Definition at line 326 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createAuxiliaryVariable()

carl::Variable smtrat::createAuxiliaryVariable ( carl::Variable  variable)

create an auxiliary variable e.g.

aux_<Variable Name>

Parameters
variablethe variable for which auxiliary variable to be created
Returns
created auxiliary variable

Definition at line 354 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createCongruence()

FormulaT smtrat::createCongruence ( smtrat::VariableCapsule  variableCapsuleOuter,
smtrat::VariableCapsule  variableCapsuleInner 
)

Definition at line 635 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createEquivalentToOriginalMonotonicityOne()

FormulaT smtrat::createEquivalentToOriginalMonotonicityOne ( smtrat::VariableCapsule  variableCapsule,
smtrat::VariableCapsule  variableCapsuleInner 
)

Definition at line 429 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createEquivalentToOriginalMonotonicityThree()

FormulaT smtrat::createEquivalentToOriginalMonotonicityThree ( smtrat::VariableCapsule  variableCapsule,
smtrat::VariableCapsule  variableCapsuleInner 
)

Definition at line 480 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createEquivalentToOriginalMonotonicityTwo()

FormulaT smtrat::createEquivalentToOriginalMonotonicityTwo ( smtrat::VariableCapsule  variableCapsule,
smtrat::VariableCapsule  variableCapsuleInner 
)

Definition at line 453 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createICPGreater()

FormulasT smtrat::createICPGreater ( VariableCapsule  variableCapsule,
RationalCapsule  rationalCapsule 
)

Definition at line 722 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createICPGreaterOne()

FormulaT smtrat::createICPGreaterOne ( VariableCapsule  variableCapsule,
RationalCapsule  rationalCapsule 
)

Definition at line 666 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createICPGreaterTwo()

FormulaT smtrat::createICPGreaterTwo ( VariableCapsule  variableCapsule,
RationalCapsule  rationalCapsule 
)

Definition at line 694 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createICPLess()

FormulaT smtrat::createICPLess ( VariableCapsule  variableCapsule,
RationalCapsule  rationalCapsule 
)

Definition at line 729 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createMonotonicity()

FormulasT smtrat::createMonotonicity ( VariableCapsule  variableCapsuleOuter,
VariableCapsule  variableCapsuleInner,
Model  absoluteValuedModel 
)

Definition at line 613 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createOriginalMonotonicityOne()

FormulaT smtrat::createOriginalMonotonicityOne ( smtrat::VariableCapsule  variableCapsule,
smtrat::VariableCapsule  variableCapsuleInner 
)

Definition at line 514 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createOriginalMonotonicityThree()

FormulaT smtrat::createOriginalMonotonicityThree ( smtrat::VariableCapsule  variableCapsule,
smtrat::VariableCapsule  variableCapsuleInner 
)

Definition at line 579 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createOriginalMonotonicityTwo()

FormulaT smtrat::createOriginalMonotonicityTwo ( smtrat::VariableCapsule  variableCapsule,
smtrat::VariableCapsule  variableCapsuleInner 
)

Definition at line 545 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createTangentPlaneEQ()

FormulasT smtrat::createTangentPlaneEQ ( VariableCapsule  variableCapsule,
RationalCapsule  rationalCapsule 
)

Definition at line 289 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createTangentPlaneEQOne()

FormulaT smtrat::createTangentPlaneEQOne ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable,
Rational  aRational 
)

Definition at line 249 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createTangentPlaneEQTwo()

FormulaT smtrat::createTangentPlaneEQTwo ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable,
Rational  aRational 
)

Definition at line 269 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createTangentPlaneNEQ()

FormulasT smtrat::createTangentPlaneNEQ ( VariableCapsule  variableCapsule,
RationalCapsule  rationalCapsule 
)

Definition at line 240 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createTangentPlaneNEQFour()

FormulaT smtrat::createTangentPlaneNEQFour ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable,
Rational  aRational,
Rational  bRational 
)

Definition at line 198 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createTangentPlaneNEQOne()

FormulaT smtrat::createTangentPlaneNEQOne ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable,
Rational  aRational 
)

Definition at line 115 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createTangentPlaneNEQThree()

FormulaT smtrat::createTangentPlaneNEQThree ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable,
Rational  aRational,
Rational  bRational 
)

Definition at line 157 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createTangentPlaneNEQTwo()

FormulaT smtrat::createTangentPlaneNEQTwo ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable,
Rational  bRational 
)

Definition at line 136 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createZero()

FormulasT smtrat::createZero ( smtrat::VariableCapsule  variableCapsule)

Definition at line 107 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createZeroOne()

FormulaT smtrat::createZeroOne ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable 
)

Definition at line 13 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createZeroThree()

FormulaT smtrat::createZeroThree ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable 
)

Definition at line 72 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ createZeroTwo()

FormulaT smtrat::createZeroTwo ( carl::Variable  xVariable,
carl::Variable  yVariable,
carl::Variable  zVariable 
)

Definition at line 37 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ executeFile()

template<typename Executor >
int smtrat::executeFile ( const std::string &  pathToInputFile,
Executor &  e 
)

Parse the file and save it in formula.

Parameters
pathToInputFileThe path to the input smt2 file.
formulaA pointer to the formula object which holds the parsed input afterwards.
optionsSave options from the smt2 file here.

Definition at line 38 of file execute_smtlib.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ extractRationalCapsule()

RationalCapsule smtrat::extractRationalCapsule ( VariableCapsule  variableCapsule,
Model  linearizedModel 
)

Definition at line 507 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ extractVariables()

const smtrat::VariableCapsule smtrat::extractVariables ( MonomialMapIterator  monomialIterator)

Definition at line 296 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ factorial() [1/2]

Rational smtrat::factorial ( Rational  n)

Definition at line 195 of file CardinalityEncoder.cpp.

Here is the caller graph for this function:

◆ factorial() [2/2]

Rational smtrat::factorial ( std::size_t  n)

Definition at line 191 of file CardinalityEncoder.cpp.

Here is the call graph for this function:

◆ generateAbcPrimeForICP()

RationalCapsule smtrat::generateAbcPrimeForICP ( RationalCapsule  rationalCapsule,
bool  isGreater 
)

Definition at line 838 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ generateAbsFormula() [1/2]

FormulaT smtrat::generateAbsFormula ( carl::Variable  variable,
carl::Variable  aux_variable 
)

| x1 | = (and (=> (x1 >= 0) (y1 = x1)) (=> (x1 < 0) (y1 = -x1)) )

Parameters
variable
Returns

Definition at line 367 of file AxiomFactory.cpp.

Here is the caller graph for this function:

◆ generateAbsFormula() [2/2]

FormulaT smtrat::generateAbsFormula ( carl::Variable  variableLeft,
carl::Variable  variableRight,
carl::Relation  relation 
)

| x1 | <= | x1 | = (and (=> (x1 >= 0) (y1 = x1)) (=> (x1 < 0) (y1 = -x1)) (=> (x2 >= 0) (y2 = x2)) (=> (x2 < 0) (y2 = -x2)) (y1 <= y2) )

Parameters
variableLeft
variableRight
relation
Returns

Definition at line 405 of file AxiomFactory.cpp.

Here is the call graph for this function:

◆ get_name() [1/2]

std::string smtrat::get_name ( IsSampleOutsideAlgorithm  samplingAlgorithm)
inline

Definition at line 34 of file Sampling.h.

◆ get_name() [2/2]

std::string smtrat::get_name ( SamplingAlgorithm  samplingAlgorithm)
inline

Definition at line 25 of file Sampling.h.

◆ handle_basic_options()

int smtrat::handle_basic_options ( const SettingsParser &  parser)

Definition at line 42 of file handle_options.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ is_sat()

bool smtrat::is_sat ( Answer  a)
inline

Definition at line 58 of file types.h.

Here is the caller graph for this function:

◆ isAnyRationalIsZero()

bool smtrat::isAnyRationalIsZero ( RationalCapsule  rationalCapsule)

Definition at line 883 of file AxiomFactory.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isCondition()

bool smtrat::isCondition ( carl::Condition  _condition)

◆ operator<<() [1/10]

std::ostream& smtrat::operator<< ( std::ostream &  os,
Answer  a 
)
inline

Definition at line 59 of file types.h.

◆ operator<<() [2/10]

std::ostream & smtrat::operator<< ( std::ostream &  os,
CMakeOptionPrinter  cmop 
)

Definition at line 21 of file compile_information.cpp.

Here is the call graph for this function:

◆ operator<<() [3/10]

std::ostream& smtrat::operator<< ( std::ostream &  os,
const CoveringStatus &  status 
)
inline

Definition at line 317 of file LevelWiseInformation.h.

◆ operator<<() [4/10]

template<typename Settings >
std::ostream& smtrat::operator<< ( std::ostream &  os,
const LevelWiseInformation< Settings > &  levelWiseInformation 
)
inline

Definition at line 340 of file LevelWiseInformation.h.

Here is the call graph for this function:

◆ operator<<() [5/10]

template<typename Module >
std::ostream& smtrat::operator<< ( std::ostream &  os,
const ModuleFactory< Module > &  mf 
)
inline

Definition at line 35 of file StrategyGraph.h.

Here is the call graph for this function:

◆ operator<<() [6/10]

std::ostream& smtrat::operator<< ( std::ostream &  os,
const ModuleInput &  mi 
)
inline

Definition at line 448 of file ModuleInput.h.

◆ operator<<() [7/10]

template<typename TT , typename C >
std::ostream& smtrat::operator<< ( std::ostream &  os,
const PriorityQueue< TT, C > &  pq 
)

Definition at line 57 of file DynamicPriorityQueue.h.

Here is the call graph for this function:

◆ operator<<() [8/10]

std::ostream& smtrat::operator<< ( std::ostream &  os,
MaxSMTStrategy  ucs 
)
inline

Definition at line 10 of file MaxSMT.h.

◆ operator<<() [9/10]

std::ostream& smtrat::operator<< ( std::ostream &  os,
Module::LemmaType  lt 
)
inline

Definition at line 1187 of file Module.h.

◆ operator<<() [10/10]

std::ostream& smtrat::operator<< ( std::ostream &  os,
UnsatCoreStrategy  ucs 
)
inline

Definition at line 9 of file UnsatCore.h.

◆ parse_formula()

FormulaT smtrat::parse_formula ( const std::string &  filename)

Loads the smt2 file specified in filename and returns the formula.

This function ignores most SMT-LIB commands but simply accumulated all asserted formulas.

◆ parse_smtlib()

FormulaT smtrat::parse_smtlib ( const std::string &  )

Definition at line 25 of file parser_smtlib.cpp.

◆ parseInput()

template<typename Executor >
bool smtrat::parseInput ( const std::string &  pathToInputFile,
Executor &  e,
bool &  queueInstructions 
)

Definition at line 15 of file execute_smtlib.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ parseSMT2File()

bool smtrat::parseSMT2File ( parser::InstructionHandler &  handler,
bool  queueInstructions,
std::istream &  input 
)

Definition at line 6 of file ParserWrapper.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ preprocess_file()

int smtrat::preprocess_file ( const std::string &  filename,
const std::string &  outfile 
)

Loads the smt2 file specified in filename and runs the preprocessing strategy.

The resulting (simplified) problem is written to outfile (or stdout if outfile is empty).

Definition at line 121 of file preprocessor.cpp.

Here is the caller graph for this function:

◆ run_dimacs_file()

template<typename Strategy >
int smtrat::run_dimacs_file ( Strategy &  ,
const std::string &   
)

Definition at line 51 of file parser_dimacs.h.

Here is the caller graph for this function:

◆ run_opb_file()

template<typename Strategy >
int smtrat::run_opb_file ( Strategy &  ,
const std::string &   
)

Definition at line 72 of file parser_opb.h.

Here is the caller graph for this function:

◆ Settings()

const settings::Settings& smtrat::Settings ( )
inline

Definition at line 96 of file Settings.h.

◆ settings_analyzer()

const auto& smtrat::settings_analyzer ( )
inline

Definition at line 33 of file settings.h.

Here is the caller graph for this function:

◆ settings_core()

const auto& smtrat::settings_core ( )
inline

Definition at line 100 of file Settings.h.

Here is the caller graph for this function:

◆ settings_module()

const auto& smtrat::settings_module ( )
inline

Definition at line 108 of file Settings.h.

Here is the caller graph for this function:

◆ settings_parser()

const auto& smtrat::settings_parser ( )
inline

Definition at line 34 of file ParserSettings.h.

Here is the caller graph for this function:

◆ settings_solver()

const auto& smtrat::settings_solver ( )
inline

Definition at line 104 of file Settings.h.

Here is the caller graph for this function:

◆ settings_statistics()

const auto& smtrat::settings_statistics ( )
inline

Definition at line 30 of file StatisticsSettings.h.

Here is the caller graph for this function:

◆ settings_validation()

const auto& smtrat::settings_validation ( )
inline

Definition at line 41 of file ValidationSettings.h.

Here is the caller graph for this function:

◆ statistics_get()

template<typename T >
auto& smtrat::statistics_get ( const std::string &  name)

Definition at line 10 of file Statistics.h.

◆ testExpression()

void smtrat::testExpression ( )

Definition at line 14 of file ExpressionTest.h.

◆ validation_get()

auto& smtrat::validation_get ( const std::string &  channel,
const std::string &  file,
int  line 
)
inline

Definition at line 8 of file Validation.h.

Here is the call graph for this function:

◆ visiting()

void smtrat::visiting ( const Expression &  expr)

Definition at line 10 of file ExpressionTest.h.

Variable Documentation

◆ COMMANDER_GROUP_SIZE

constexpr int smtrat::COMMANDER_GROUP_SIZE = 4
staticconstexpr

Definition at line 6 of file ExactlyOneCommanderEncoder.cpp.

◆ EMPTY_MODEL

const Model smtrat::EMPTY_MODEL = Model()
static

Definition at line 15 of file model.h.